|
|
@@ -26,6 +26,7 @@ Element function reachability_graph(params : Element, output_mms : Element):
|
|
|
Integer link_weight
|
|
|
Integer initial
|
|
|
Integer state_id
|
|
|
+ Integer next_id
|
|
|
Boolean possible
|
|
|
Element all_places
|
|
|
Element dict_repr
|
|
|
@@ -79,16 +80,21 @@ Element function reachability_graph(params : Element, output_mms : Element):
|
|
|
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")
|
|
|
|
|
|
- set_add(workset, dict_repr)
|
|
|
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)
|
|
|
|
|
|
- log("Start!")
|
|
|
- all_transitions_original = allInstances(in_model, "Transition")
|
|
|
while (read_nr_out(workset) > 0):
|
|
|
- dict_repr = set_pop(workset)
|
|
|
+ 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
|
|
|
@@ -98,7 +104,6 @@ Element function reachability_graph(params : Element, output_mms : Element):
|
|
|
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)
|
|
|
|
|
|
@@ -122,8 +127,12 @@ Element function reachability_graph(params : Element, output_mms : Element):
|
|
|
key = set_pop(keys)
|
|
|
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)
|
|
|
+ // 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!
|
