Copy some reachability algorithms to this test in particular

models/reachability.alc

@@ -0,0 +1,186 @@
+include "primitives.alh"
+include "modelling.alh"
+include "object_operations.alh"
+
+Element function reachability_graph(params : Element, output_mms : Element):
+	Element result
+	Element model
+	Element workset
+	Element out_model
+	Element in_model
+	Element transition_vectors_produce
+	Element transition_vectors_consume
+	Element all_transitions
+	Element all_transitions_original
+	Element tv
+	Element links
+	Element mappings
+	Element reachable_states
+	Element keys
+	String transition
+	String new_transition
+	String state
+	String name
+	String link
+	String place
+	String key
+	Integer link_weight
+	Integer initial
+	Integer state_id
+	Integer next_id
+	Boolean possible
+	Element all_places
+	Element dict_repr
+	Element new_dict_repr
+	Element work_unit
+
+	Element cache
+	cache = create_node()
+
+	result = create_node()
+	out_model = instantiate_model(output_mms["ReachabilityGraph"])
+	in_model = params["pn"]
+
+	// 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)
+
+		tv = create_node()
+		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_fast(tv, name, link_weight)
+		dict_add_fast(transition_vectors_consume, transition, tv)
+
+		tv = create_node()
+		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_fast(tv, name, link_weight)
+		dict_add_fast(transition_vectors_produce, transition, tv)
+
+	workset = create_node()
+
+	all_places = allInstances(in_model, "Place")
+	dict_repr = create_node()
+	while (read_nr_out(all_places) > 0):
+		place = set_pop(all_places)
+		dict_add_fast(dict_repr, place, read_attribute(in_model, place, "tokens"))
+
+	all_transitions_original = allInstances(in_model, "Transition")
+
+	mappings = create_node()
+	state_id = 0
+	next_id = 1
+	reachable_states = create_node()
+	dict_add_fast(reachable_states, state_id, dict_repr)
+	dict_add_fast(mappings, state_id, create_node())
+	set_add(workset, state_id)
+
+	// And add in the model itself
+	state = instantiate_node(out_model, "State", cast_i2s(state_id))
+	instantiate_attribute(out_model, state, "name", cast_i2s(state_id))
+	keys = dict_keys(dict_repr)
+	while (read_nr_out(keys) > 0):
+		key = set_pop(keys)
+		place = instantiate_node(out_model, "Place", "")
+		instantiate_attribute(out_model, place, "name", read_attribute(in_model, key, "name"))
+		instantiate_attribute(out_model, place, "tokens", dict_repr[key])
+		instantiate_link(out_model, "Contains", "", state, place)
+
+	while (read_nr_out(workset) > 0):
+		state_id = set_pop(workset)
+
+		dict_repr = reachable_states[state_id]
+
+		// Compute how the PN behaves with this specific state
+		// For this, we fetch all transitions and check if they are enabled
+		all_transitions = set_copy(all_transitions_original)
+		while (read_nr_out(all_transitions) > 0):
+			transition = set_pop(all_transitions)
+
+			keys = dict_keys(transition_vectors_consume[transition])
+			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 (integer_lt(dict_repr[key], transition_vectors_consume[transition][key])):
+					// Impossible transition, so discard this one
+					possible = False
+					break!
+
+			if (possible):
+				new_dict_repr = dict_copy(dict_repr)
+				// Transition can execute, so compute and add the new state based on the consume/produce vectors
+				keys = dict_keys(transition_vectors_consume[transition])
+				while (read_nr_out(keys) > 0):
+					key = set_pop(keys)
+					dict_overwrite(new_dict_repr, key, integer_subtraction(new_dict_repr[key], transition_vectors_consume[transition][key]))
+
+				keys = dict_keys(transition_vectors_produce[transition])
+				while (read_nr_out(keys) > 0):
+					key = set_pop(keys)
+					dict_overwrite(new_dict_repr, key, integer_addition(new_dict_repr[key], transition_vectors_produce[transition][key]))
+
+				// Check if this state already has an associated ID
+				Integer other_state_id
+				Integer target_id
+
+				keys = dict_keys(reachable_states)
+				target_id = -1
+				while (read_nr_out(keys) > 0):
+					other_state_id = set_pop(keys)
+
+					if (dict_eq(reachable_states[other_state_id], new_dict_repr)):
+						target_id = other_state_id
+						break!
+
+				if (target_id == -1):
+					// New state
+					target_id = next_id
+					next_id = next_id + 1
+
+					// Add to all data structures
+					dict_add_fast(reachable_states, target_id, new_dict_repr)
+					dict_add_fast(mappings, target_id, create_node())
+					set_add(workset, target_id)
+
+					// And add in the model itself
+					state = instantiate_node(out_model, "State", cast_i2s(target_id))
+					instantiate_attribute(out_model, state, "name", cast_i2s(target_id))
+
+					keys = dict_keys(new_dict_repr)
+					Element sub
+					String name
+					while (read_nr_out(keys) > 0):
+						key = set_pop(keys)
+						name = read_attribute(in_model, key, "name")
+						if (bool_not(dict_in(cache, name))):
+							dict_add_fast(cache, name, create_node())
+						sub = cache[name]
+						if (bool_not(dict_in(sub, new_dict_repr[key]))):
+							place = instantiate_node(out_model, "Place", "")
+							instantiate_attribute(out_model, place, "name", name)
+							instantiate_attribute(out_model, place, "tokens", new_dict_repr[key])
+							dict_add_fast(sub, new_dict_repr[key], place)
+						else:
+							place = sub[new_dict_repr[key]]
+						instantiate_link(out_model, "Contains", "", state, place)
+
+				// Anyway, we have found a transition, which we should store
+				dict_add_fast(mappings[state_id], transition, target_id)
+
+				// And also store it in the model itself
+				new_transition = instantiate_link(out_model, "Transition", "", cast_i2s(state_id), cast_i2s(target_id))
+				instantiate_attribute(out_model, new_transition, "name", read_attribute(in_model, transition, "name"))
+
+	dict_add_fast(result, "ReachabilityGraph", out_model)
+	return result!

models/reachability_graph.mvc

@@ -0,0 +1,64 @@
+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"!
+            $
+    }
+}