modelverse/models/matches.mvc

include "primitives.alh"
include "modelling.alh"
include "object_operations.alh"

Composite schedule {
    {Contains} Failure failure {}
    {Contains} Success success {}
    {Contains} Query query {
        LHS {
            Pre_Query/Place {
                label = "2"
            }
            Pre_ReachabilityGraph/Place {
                label = "3"
            }

            constraint = $
                Boolean function constraint(host_model : Element, mapping : Element):
                    Boolean names_match
                    Boolean tokens_match
                    names_match = value_eq(read_attribute(host_model, mapping["2"], "name"), read_attribute(host_model, mapping["3"], "name"))
                    tokens_match = value_eq(read_attribute(host_model, mapping["2"], "tokens"), read_attribute(host_model, mapping["3"], "tokens"))
                    return bool_and(names_match, tokens_match)!
                $
        }
    }
    {Contains} ForAll match {
        LHS {
            Pre_Query/Place {
                label = "2"
            }
            Pre_ReachabilityGraph/Place pre_3 {
                label = "3"
            }
            Pre_ReachabilityGraph/State pre_4 {
                label = "4"
            }
            Pre_ReachabilityGraph/Contains (pre_4, pre_3) {
                label = "5"
            }

            constraint = $
                Boolean function constraint(host_model : Element, mapping : Element):
                    Boolean names_match
                    Boolean tokens_match
                    names_match = value_eq(read_attribute(host_model, mapping["2"], "name"), read_attribute(host_model, mapping["3"], "name"))
                    tokens_match = value_eq(read_attribute(host_model, mapping["2"], "tokens"), read_attribute(host_model, mapping["3"], "tokens"))
                    return bool_and(names_match, tokens_match)!
                $
        }
        RHS {
            Post_Query/Place {
                label = "2"
            }
            Post_ReachabilityGraph/Place post_3{
                label = "3"
            }
            Post_ReachabilityGraph/State post_4{
                label = "4"
                value_error = $
                    Boolean function value (model : Element, name : String, mapping : Element):
                        return True!
                    $
            }
            Post_ReachabilityGraph/Contains (post_4, post_3){
                label = "5"
            }
        }
    }
}
Initial (schedule, query) {}
OnSuccess (query, match) {}
OnFailure (query, failure) {}
OnSuccess (match, success) {}
OnFailure (match, failure) {}