modelverse/models/reachability_graph.mvc

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

SimpleClassDiagrams ReachabilityGraph {
    SimpleAttribute String {}
    SimpleAttribute Natural {}
    SimpleAttribute Boolean {}

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

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

    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 (read_nr_out(states) > 0):
                    expected = create_node()
                    state = set_pop(states)
                    places = allAssociationDestinations(model, state, "Contains")
                    while (read_nr_out(places)):
                        place = set_pop(places)
                        set_add(expected, read_attribute(model, place, "name"))
                else:
                    return "OK"!
                
                while (read_nr_out(states) > 0):
                    got = create_node()
                    state = set_pop(states)
                    places = allAssociationDestinations(model, state, "Contains")
                    while (read_nr_out(places)):
                        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"!
            $
    }
}