|
@@ -11,7 +11,7 @@ Element function reachability_graph(params : Element, output_mms : Element):
|
|
|
Element transition_vectors_produce
|
|
|
Element transition_vectors_consume
|
|
|
Element all_transitions
|
|
|
- Element vector
|
|
|
+ Element all_transitions_original
|
|
|
Element tv
|
|
|
Element links
|
|
|
Element mappings
|
|
@@ -33,63 +33,77 @@ Element function reachability_graph(params : Element, output_mms : Element):
|
|
|
|
|
|
result = create_node()
|
|
|
out_model = instantiate_model(output_mms["ReachabilityGraph"])
|
|
|
- in_model = params["PetriNets"]
|
|
|
+ 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)
|
|
|
- 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")
|
|
|
+ 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()
|
|
|
- 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)
|
|
|
+ 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, read_attribute(in_model, place, "name"), read_attribute(in_model, place, "tokens"))
|
|
|
+ dict_add(dict_repr, place, read_attribute(in_model, place, "tokens"))
|
|
|
+
|
|
|
+ log("Representation of first state: " + dict_to_string(dict_repr))
|
|
|
|
|
|
set_add(workset, dict_repr)
|
|
|
mappings = create_node()
|
|
|
|
|
|
+ log("Start!")
|
|
|
+ all_transitions_original = allInstances(in_model, "Transition")
|
|
|
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")
|
|
|
+ all_transitions = set_copy(all_transitions_original)
|
|
|
while (read_nr_out(all_transitions) > 0):
|
|
|
- name = set_pop(all_transitions)
|
|
|
- keys = dict_keys(transition_vectors_consume[name])
|
|
|
+ transition = set_pop(all_transitions)
|
|
|
+ log("Compute if possible for " + transition)
|
|
|
+ keys = dict_keys(transition_vectors_consume[transition])
|
|
|
possible = True
|
|
|
+ log("Read keys")
|
|
|
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[name][key])):
|
|
|
+ if (integer_lt(dict_repr[key], transition_vectors_consume[transition][key])):
|
|
|
// Impossible transition, so discard this one
|
|
|
possible = False
|
|
|
break!
|
|
@@ -97,14 +111,16 @@ Element function reachability_graph(params : Element, output_mms : Element):
|
|
|
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[name])
|
|
|
+ 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[name][key]))
|
|
|
- keys = dict_keys(transition_vectors_produce[name])
|
|
|
+ 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[name][key]))
|
|
|
+ dict_overwrite(dict_repr, key, integer_addition(dict_repr[key], transition_vectors_produce[transition][key]))
|
|
|
|
|
|
// Add the target to workset
|
|
|
set_add(workset, dict_repr)
|