modelverse/integration/code/reachability.alc

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

Element function reachability_graph(params : Element, output : Element):
	Element result
	Element model
	Element workset
	String state

	result = create_node()
	out_model = instantiate_node(output["ReachabilityGraph"])
	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()

	all_places = allInstances(in_model, "Place")
	dict_repr = create_node()
	while (read_nr_out(all_places) > 0):
		place = set_pop(all_places)
		dict_add(dict_repr, read_attribute(in_model, place, "name"), read_attribute(in_model, place, "tokens"))

	initial = 0

	set_add(workset, create_tuple(initial, dict_repr))
	mappings = create_node()

	while (read_nr_out(workset) > 0):
		dict_repr = set_pop(workset)
		// TODO check if dict_repr is already in the set of reachable states
		set_add(reachable_states, dict_repr)

		// 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
					break!

			if (possible):
				dict_repr = dict_copy(work_unit[1])
				// 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])

				// Add the target to workset
				set_add(workset, dict_repr)

	dict_add(result, "ReachabilityGraph", out_model)
	return result!