modelverse/models/reachability_graph.mvc

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

SimpleAttribute String {
    name = "String"
}
SimpleAttribute Natural {
    name = "Natural"
}
SimpleAttribute Boolean {
    name = "Boolean"
}

Class State {
    name = "State"
    name : String
    error : Boolean
}
Class InitialState : State {
    name = "InitialState"
    lower_cardinality = 1
    upper_cardinality = 1
}

Class Place {
    name = "Place"
    name : String
    tokens : Natural
}
Association Transition (State, State) {
    name = "Transition"
    name : String
}
Association Contains (State, Place) {
    name = "Contains"
}

GlobalConstraint {
    global_constraint = $
        String function constraint(model : Element):
            Element states
            Element places
            String state
            String place
            Element expected
            Element got

            states = allInstances(model, "State")

            if (set_len(states) > 0):
                expected = create_node()
                state = set_pop(states)
                places = allAssociationDestinations(model, state, "Contains")
                while (set_len(places)):
                    place = set_pop(places)
                    set_add(expected, read_attribute(model, place, "name"))
            else:
                return "OK"!
            
            while (set_len(states) > 0):
                got = create_node()
                state = set_pop(states)
                places = allAssociationDestinations(model, state, "Contains")
                while (set_len(places) > 0):
                    place = set_pop(places)
                    set_add(got, read_attribute(model, place, "name"))

                if (bool_not(set_equality(got, expected))):
                    return "States don't all agree on the set of places"!
            
            return "OK"!
        $
}