|
@@ -44,7 +44,6 @@ Element function reachability_graph(params : Element, output_mms : Element):
|
|
|
all_transitions = allInstances(in_model, "Transition")
|
|
|
while (read_nr_out(all_transitions) > 0):
|
|
|
transition = set_pop(all_transitions)
|
|
|
- log("Consider transition " + transition)
|
|
|
|
|
|
tv = create_node()
|
|
|
links = allIncomingAssociationInstances(in_model, transition, "P2T")
|
|
@@ -95,6 +94,9 @@ Element function reachability_graph(params : Element, output_mms : Element):
|
|
|
|
|
|
while (read_nr_out(workset) > 0):
|
|
|
state_id = set_pop(workset)
|
|
|
+ log("Work on state ID " + cast_v2s(state_id))
|
|
|
+ log("Reachable states: " + cast_i2s(read_nr_out(reachable_states)))
|
|
|
+ log("Workset: " + cast_i2s(read_nr_out(workset)))
|
|
|
|
|
|
// TODO check if dict_repr is already in the set of reachable states
|
|
|
dict_repr = reachable_states[state_id]
|
|
@@ -104,8 +106,7 @@ Element function reachability_graph(params : Element, output_mms : Element):
|
|
|
all_transitions = set_copy(all_transitions_original)
|
|
|
while (read_nr_out(all_transitions) > 0):
|
|
|
transition = set_pop(all_transitions)
|
|
|
-
|
|
|
- log("Test transition: " + cast_v2s(read_attribute(in_model, transition, "name")))
|
|
|
+ log("Test " + cast_v2s(read_attribute(in_model, transition, "name")))
|
|
|
|
|
|
keys = dict_keys(transition_vectors_consume[transition])
|
|
|
possible = True
|
|
@@ -116,14 +117,11 @@ Element function reachability_graph(params : Element, output_mms : Element):
|
|
|
if (integer_lt(dict_repr[key], transition_vectors_consume[transition][key])):
|
|
|
// Impossible transition, so discard this one
|
|
|
possible = False
|
|
|
- log("Not applicable!")
|
|
|
break!
|
|
|
|
|
|
if (possible):
|
|
|
- log("Applicable!")
|
|
|
new_dict_repr = dict_copy(dict_repr)
|
|
|
// Transition can execute, so compute and add the new state based on the consume/produce vectors
|
|
|
- log("Before transition: " + dict_to_string(new_dict_repr))
|
|
|
keys = dict_keys(transition_vectors_consume[transition])
|
|
|
while (read_nr_out(keys) > 0):
|
|
|
key = set_pop(keys)
|
|
@@ -133,7 +131,6 @@ Element function reachability_graph(params : Element, output_mms : Element):
|
|
|
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]))
|
|
|
- log("After transition: " + dict_to_string(new_dict_repr))
|
|
|
|
|
|
// Check if this state already has an associated ID
|
|
|
Integer other_state_id
|
|
@@ -163,6 +160,7 @@ Element function reachability_graph(params : Element, output_mms : Element):
|
|
|
instantiate_attribute(out_model, state, "name", cast_i2s(target_id))
|
|
|
|
|
|
keys = dict_keys(new_dict_repr)
|
|
|
+ // TODO optimize this part?
|
|
|
while (read_nr_out(keys) > 0):
|
|
|
key = set_pop(keys)
|
|
|
place = instantiate_node(out_model, "Place", "")
|
|
@@ -176,7 +174,6 @@ Element function reachability_graph(params : Element, output_mms : Element):
|
|
|
// And also store it in the model itself
|
|
|
new_transition = instantiate_link(out_model, "Transition", "", cast_i2s(state_id), cast_i2s(target_id))
|
|
|
instantiate_attribute(out_model, new_transition, "name", read_attribute(in_model, transition, "name"))
|
|
|
- log("Add transition name: " + cast_v2s(read_attribute(in_model, transition, "name")))
|
|
|
|
|
|
dict_add(result, "ReachabilityGraph", out_model)
|
|
|
return result!
|