|
@@ -97,11 +97,8 @@ Element function reachability_graph(params : Element, output_mms : Element):
|
|
|
|
|
|
|
|
while (read_nr_out(workset) > 0):
|
|
while (read_nr_out(workset) > 0):
|
|
|
state_id = set_pop(workset)
|
|
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("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]
|
|
dict_repr = reachable_states[state_id]
|
|
|
|
|
|
|
|
// Compute how the PN behaves with this specific state
|
|
// Compute how the PN behaves with this specific state
|
|
@@ -109,7 +106,6 @@ Element function reachability_graph(params : Element, output_mms : Element):
|
|
|
all_transitions = set_copy(all_transitions_original)
|
|
all_transitions = set_copy(all_transitions_original)
|
|
|
while (read_nr_out(all_transitions) > 0):
|
|
while (read_nr_out(all_transitions) > 0):
|
|
|
transition = set_pop(all_transitions)
|
|
transition = set_pop(all_transitions)
|
|
|
- log("Test " + cast_v2s(read_attribute(in_model, transition, "name")))
|
|
|
|
|
|
|
|
|
|
keys = dict_keys(transition_vectors_consume[transition])
|
|
keys = dict_keys(transition_vectors_consume[transition])
|
|
|
possible = True
|
|
possible = True
|
|
@@ -176,12 +172,9 @@ Element function reachability_graph(params : Element, output_mms : Element):
|
|
|
instantiate_attribute(out_model, place, "name", name)
|
|
instantiate_attribute(out_model, place, "name", name)
|
|
|
instantiate_attribute(out_model, place, "tokens", new_dict_repr[key])
|
|
instantiate_attribute(out_model, place, "tokens", new_dict_repr[key])
|
|
|
dict_add(sub, new_dict_repr[key], place)
|
|
dict_add(sub, new_dict_repr[key], place)
|
|
|
- log("Added to cache")
|
|
|
|
|
else:
|
|
else:
|
|
|
place = sub[new_dict_repr[key]]
|
|
place = sub[new_dict_repr[key]]
|
|
|
- log("Accessed cache!")
|
|
|
|
|
instantiate_link(out_model, "Contains", "", state, place)
|
|
instantiate_link(out_model, "Contains", "", state, place)
|
|
|
- log("Total elements in out: " + cast_v2s(read_nr_out(out_model["model"])))
|
|
|
|
|
|
|
|
|
|
// Anyway, we have found a transition, which we should store
|
|
// Anyway, we have found a transition, which we should store
|
|
|
dict_add(mappings[state_id], transition, target_id)
|
|
dict_add(mappings[state_id], transition, target_id)
|