Basis of coverability graph creation

integration/code/coverability.alc

@@ -0,0 +1,93 @@
+include "primitives.alh"
+include "modelling.alh"
+include "object_operations.alh"
+
+Element function coverability_graph(params : Element, output : Element):
+	Element result
+	Element model
+	Element workset
+	String state
+
+	result = create_node()
+	out_model = instantiate_node(output["CoverabilityGraph"])
+	in_model = params["PetriNets"]
+
+	// Create a dictionary representation for each transition
+	transition_vectors_produce = create_node()
+	transition_vectors_consume = create_node()
+	all_transitions = allInstances(in_model, "Transition")
+	while (read_nr_out(all_transitions) > 0):
+		transition = set_pop(all_transitions)
+		name = read_attribute(in_model, transition, "name")
+		vector = create_node()
+
+		tv = create_node()
+		dict_add(transition_vectors_consume, name, tv)
+		links = allIncomingAssociationInstances(in_model, transition, "P2T")
+		while (read_nr_out(links) > 0):
+			link = set_pop(links)
+			name = reverseKeyLookup(in_model["model"], read_edge_src(in_model["model"][link]))
+			link_weight = read_attribute(in_model, link, "weight")
+			dict_add(tv, name, link_weight)
+
+		tv = create_node()
+		dict_add(transition_vectors_produce, name, tv)
+		links = allOutgoingAssociationInstances(in_model, transition, "T2P")
+		while (read_nr_out(links) > 0):
+			link = set_pop(links)
+			name = reverseKeyLookup(in_model["model"], read_edge_dst(in_model["model"][link]))
+			link_weight = read_attribute(in_model, link, "weight")
+			dict_add(tv, name, link_weight)
+
+	workset = create_node()
+	initial = instantiate_node(out_model, "InitialState", "")
+
+	all_places = allInstances(in_model, "Place")
+	dict_repr = create_node()
+	while (read_nr_out(all_places) > 0):
+		place = set_pop(all_places)
+		state_config = instantiate_node(out_model, "Place", "")
+		instantiate_attribute(out_model, state_config, "name", read_attribute(in_model, place, "name"))
+		instantiate_attribute(out_model, state_config, "tokens", read_attribute(in_model, place, "tokens"))
+		instantiate_link(out_model, "", "", initial, state_config)
+		dict_add(dict_repr, read_attribute(in_model, place, "name"), read_attribute(in_model, place, "tokens"))
+
+	set_add(workset, create_tuple(initial, dict_repr))
+
+	while (read_nr_out(workset) > 0):
+		work_unit = set_pop(workset)
+		state = work_unit[0]
+		dict_repr = dict_copy(work_unit[1])
+
+		// Compute how the PN behaves with this specific state
+		// For this, we fetch all transitions and check if they are enabled
+		all_transitions = allInstances(in_model, "Transition")
+		while (read_nr_out(all_transitions) > 0):
+			name = set_pop(all_transitions)
+			keys = dict_keys(transition_vectors_consume[name])
+			possible = True
+			while (read_nr_out(keys) > 0):
+				key = set_pop(keys)
+
+				// Compare the values in the state with those consumed by the transition
+				if (dict_repr[key] < transition_vectors_consume[name][key]):
+					// Impossible transition, so discard this one
+					possible = False
+					continue!
+
+			if (possible):
+				// Transition can execute, so compute and add the new state based on the consume/produce vectors
+				keys = dict_keys(transition_vectors_consume[name])
+				while (read_nr_out(keys) > 0):
+					key = set_pop(keys)
+					dict_overwrite(dict_repr, key, dict_repr[key] - transition_vectors_consume[name][key])
+				keys = dict_keys(transition_vectors_produce[name])
+				while (read_nr_out(keys) > 0):
+					key = set_pop(keys)
+					dict_overwrite(dict_repr, key, dict_repr[key] + transition_vectors_produce[name][key])
+
+				// Now write out the dictionary representation to a model!
+				// TODO
+
+	dict_add(result, "CoverabilityGraph", out_model)
+	return result!

integration/code/coverability_graph.mvc

@@ -0,0 +1,48 @@
+SimpleClassDiagrams CoverabilityGraph {
+    Class State {}
+    Class Place {
+        name : String
+        tokens : Natural
+    }
+    Association Transition (State, State) {
+        name : String
+    }
+    Association Contains (State, Place) {}
+
+    GlobalConstraint {
+        global_constraint = $
+            String 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_equals(got, expected))):
+                        return "States don't all agree on the set of places"!
+                
+                return "OK"!
+            $
+    }
+}