modelverse/models/reachability.alc

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

Boolean function reachability_graph(model : Element):
	Element workset
	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 = dict_create()

	// Create a dictionary representation for each transition
	transition_vectors_produce = dict_create()
	transition_vectors_consume = dict_create()
	all_transitions = allInstances(model, "PetriNet/Transition")
	while (set_len(all_transitions) > 0):
		transition = set_pop(all_transitions)

		tv = dict_create()
		links = allIncomingAssociationInstances(model, transition, "PetriNet/P2T")
		while (set_len(links) > 0):
			link = set_pop(links)
			name = reverseKeyLookup(model["model"], read_edge_src(model["model"][link]))
			link_weight = read_attribute(model, link, "weight")
			dict_add_fast(tv, name, link_weight)
		dict_add_fast(transition_vectors_consume, transition, tv)

		tv = dict_create()
		links = allOutgoingAssociationInstances(model, transition, "PetriNet/T2P")
		while (set_len(links) > 0):
			link = set_pop(links)
			name = reverseKeyLookup(model["model"], read_edge_dst(model["model"][link]))
			link_weight = read_attribute(model, link, "weight")
			dict_add_fast(tv, name, link_weight)
		dict_add_fast(transition_vectors_produce, transition, tv)

	workset = set_create()

	all_places = allInstances(model, "PetriNet/Place")
	dict_repr = dict_create()
	while (set_len(all_places) > 0):
		place = set_pop(all_places)
		dict_add_fast(dict_repr, place, read_attribute(model, place, "tokens"))

	all_transitions_original = allInstances(model, "PetriNet/Transition")

	mappings = dict_create()
	state_id = 0
	next_id = 1
	reachable_states = dict_create()
	dict_add_fast(reachable_states, state_id, dict_repr)
	dict_add_fast(mappings, state_id, dict_create())
	set_add(workset, state_id)

	// And add in the model itself
	state = instantiate_node(model, "ReachabilityGraph/InitialState", cast_string(state_id))
	instantiate_attribute(model, state, "name", cast_string(state_id))
	instantiate_attribute(model, state, "error", False)
	keys = dict_keys(dict_repr)
	while (set_len(keys) > 0):
		key = set_pop(keys)
		place = instantiate_node(model, "ReachabilityGraph/Place", "")
		instantiate_attribute(model, place, "name", read_attribute(model, key, "name"))
		instantiate_attribute(model, place, "tokens", dict_repr[key])
		instantiate_link(model, "ReachabilityGraph/Contains", "", state, place)

	while (set_len(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 (set_len(all_transitions) > 0):
			transition = set_pop(all_transitions)

			keys = dict_keys(transition_vectors_consume[transition])
			possible = True
			while (set_len(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 (set_len(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 (set_len(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
				Float start
				while (set_len(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, dict_create())
					set_add(workset, target_id)

					// And add in the model itself
					state = instantiate_node(model, "ReachabilityGraph/State", cast_string(target_id))
					instantiate_attribute(model, state, "name", cast_string(target_id))
					instantiate_attribute(model, state, "error", False)

					keys = dict_keys(new_dict_repr)
					Element sub
					String name
					while (set_len(keys) > 0):
						key = set_pop(keys)
						name = read_attribute(model, key, "name")
						if (bool_not(dict_in(cache, name))):
							dict_add_fast(cache, name, dict_create())
						sub = cache[name]
						if (bool_not(dict_in(sub, new_dict_repr[key]))):
							place = instantiate_node(model, "ReachabilityGraph/Place", "")
							instantiate_attribute(model, place, "name", name)
							instantiate_attribute(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(model, "ReachabilityGraph/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(model, "ReachabilityGraph/Transition", "", cast_string(state_id), cast_string(target_id))
				instantiate_attribute(model, new_transition, "name", read_attribute(model, transition, "name"))

	log("# reachable states: " + cast_value(next_id))
	return True!