|
@@ -0,0 +1,184 @@
|
|
|
+include "primitives.alh"
|
|
|
+include "modelling.alh"
|
|
|
+include "object_operations.alh"
|
|
|
+
|
|
|
+Boolean function main(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 = create_node()
|
|
|
+
|
|
|
+ // Create a dictionary representation for each transition
|
|
|
+ transition_vectors_produce = create_node()
|
|
|
+ transition_vectors_consume = create_node()
|
|
|
+ all_transitions = allInstances(model, "PetriNet/Transition")
|
|
|
+ while (read_nr_out(all_transitions) > 0):
|
|
|
+ transition = set_pop(all_transitions)
|
|
|
+
|
|
|
+ tv = create_node()
|
|
|
+ links = allIncomingAssociationInstances(model, transition, "PetriNet/P2T")
|
|
|
+ while (read_nr_out(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 = create_node()
|
|
|
+ links = allOutgoingAssociationInstances(model, transition, "PetriNet/T2P")
|
|
|
+ while (read_nr_out(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 = create_node()
|
|
|
+
|
|
|
+ all_places = allInstances(model, "PetriNet/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(model, place, "tokens"))
|
|
|
+
|
|
|
+ all_transitions_original = allInstances(model, "PetriNet/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 = create_state(model, cast_i2s(state_id), dict_repr, cache, True)
|
|
|
+
|
|
|
+ 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
|
|
|
+ Float start
|
|
|
+ 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
|
|
|
+ create_state(model, cast_i2s(target_id), new_dict_repr, cache, False)
|
|
|
+
|
|
|
+ // 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_i2s(state_id), cast_i2s(target_id))
|
|
|
+ instantiate_attribute(model, new_transition, "name", read_attribute(model, transition, "name"))
|
|
|
+
|
|
|
+ log("# reachable states: " + cast_v2s(next_id))
|
|
|
+ return True!
|
|
|
+
|
|
|
+String function create_state(model : Element, name : String, dict_repr : Element, cache : Element, initial : Boolean):
|
|
|
+ Element state
|
|
|
+ Element keys
|
|
|
+ Element sub
|
|
|
+ String key
|
|
|
+ String place
|
|
|
+
|
|
|
+ if (initial):
|
|
|
+ state = instantiate_node(model, "ReachabilityGraph/InitialState", name)
|
|
|
+ else:
|
|
|
+ state = instantiate_node(model, "ReachabilityGraph/State", name)
|
|
|
+ instantiate_attribute(model, state, "name", name)
|
|
|
+ instantiate_attribute(model, state, "error", False)
|
|
|
+
|
|
|
+ keys = dict_keys(dict_repr)
|
|
|
+
|
|
|
+ while (read_nr_out(keys) > 0):
|
|
|
+ key = set_pop(keys)
|
|
|
+ name = read_attribute(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, dict_repr[key]))):
|
|
|
+ place = instantiate_node(model, "ReachabilityGraph/Place", "")
|
|
|
+ instantiate_attribute(model, place, "name", name)
|
|
|
+ instantiate_attribute(model, place, "tokens", dict_repr[key])
|
|
|
+ dict_add_fast(sub, dict_repr[key], place)
|
|
|
+ else:
|
|
|
+ place = sub[dict_repr[key]]
|
|
|
+ instantiate_link(model, "ReachabilityGraph/Contains", "", state, place)
|
|
|
+ return state!
|