modelverse/integration/code/reachability.alc

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 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 work_unit

	result = create_node()
	out_model = instantiate_model(output_mms["ReachabilityGraph"])
	in_model = params["PetriNet"]
	log("Got in_model: " + cast_e2s(in_model))
	log("Params: " + dict_to_string(params))
	log("Params: " + cast_e2s(in_model))
	log("Keys in type: " + set_to_string(dict_keys(in_model["metamodel"]["model"])))

	// Create a dictionary representation for each transition
	transition_vectors_produce = create_node()
	transition_vectors_consume = create_node()
	all_transitions = allInstances(in_model, "Transition")
	log("Got all transitions: " + set_to_string(all_transitions))
	while (read_nr_out(all_transitions) > 0):
		transition = set_pop(all_transitions)

		tv = create_node()
		links = allIncomingAssociationInstances(in_model, transition, "P2T")
		log("All links: " + set_to_string(links))
		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)
		dict_add(transition_vectors_consume, transition, tv)
		log("Consume OK: " + dict_to_string(transition_vectors_consume[transition]))

		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(tv, name, link_weight)
		dict_add(transition_vectors_produce, transition, tv)
		log("Produce OK: " + dict_to_string(transition_vectors_produce[transition]))

	log("Ready for work!")
	workset = create_node()

	all_places = allInstances(in_model, "Place")
	log("All places: " + set_to_string(all_places))
	dict_repr = create_node()
	while (read_nr_out(all_places) > 0):
		place = set_pop(all_places)
		dict_add(dict_repr, place, read_attribute(in_model, place, "tokens"))

	log("Representation of first state: " + dict_to_string(dict_repr))
	all_transitions_original = allInstances(in_model, "Transition")

	mappings = create_node()
	state_id = 0
	next_id = 1
	reachable_states = create_node()
	dict_add(reachable_states, state_id, dict_repr)
	dict_add(mappings, state_id, create_node())
	set_add(workset, state_id)

	while (read_nr_out(workset) > 0):
		state_id = set_pop(workset)

		// TODO check if dict_repr is already in the set of reachable states
		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)
			log("Compute if possible for " + transition)
			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):
				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])
				log("Deduct")
				while (read_nr_out(keys) > 0):
					key = set_pop(keys)
					dict_overwrite(dict_repr, key, integer_subtraction(dict_repr[key], transition_vectors_consume[transition][key]))
				keys = dict_keys(transition_vectors_produce[transition])
				log("Increment")
				while (read_nr_out(keys) > 0):
					key = set_pop(keys)
					dict_overwrite(dict_repr, key, integer_addition(dict_repr[key], transition_vectors_produce[transition][key]))

				// Add the target to workset, as it is new
				dict_add(reachable_states, next_id, dict_repr)
				dict_add(mappings, next_id, create_node())
				dict_add(mappings[state_id], transition, next_id)
				set_add(workset, next_id)
				next_id = next_id + 1

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