modelverse/models/matches.mvc

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

A B {
    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) {}
}