|
@@ -2,12 +2,8 @@ include "primitives.alh"
|
|
|
include "modelling.alh"
|
|
|
include "object_operations.alh"
|
|
|
|
|
|
-Element function reachability_graph(params : Element, output_mms : Element):
|
|
|
- Element result
|
|
|
- Element model
|
|
|
+Boolean function reachability_graph(model : Element):
|
|
|
Element workset
|
|
|
- Element out_model
|
|
|
- Element in_model
|
|
|
Element transition_vectors_produce
|
|
|
Element transition_vectors_consume
|
|
|
Element all_transitions
|
|
@@ -37,44 +33,40 @@ Element function reachability_graph(params : Element, output_mms : Element):
|
|
|
Element cache
|
|
|
cache = create_node()
|
|
|
|
|
|
- result = create_node()
|
|
|
- out_model = instantiate_model(output_mms["ReachabilityGraph"])
|
|
|
- in_model = params["pn"]
|
|
|
-
|
|
|
// Create a dictionary representation for each transition
|
|
|
transition_vectors_produce = create_node()
|
|
|
transition_vectors_consume = create_node()
|
|
|
- all_transitions = allInstances(in_model, "Transition")
|
|
|
+ all_transitions = allInstances(model, "PetriNets/Transition")
|
|
|
while (read_nr_out(all_transitions) > 0):
|
|
|
transition = set_pop(all_transitions)
|
|
|
|
|
|
tv = create_node()
|
|
|
- links = allIncomingAssociationInstances(in_model, transition, "P2T")
|
|
|
+ links = allIncomingAssociationInstances(model, transition, "PetriNets/P2T")
|
|
|
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")
|
|
|
+ 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(in_model, transition, "T2P")
|
|
|
+ links = allOutgoingAssociationInstances(model, transition, "PetriNets/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")
|
|
|
+ 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(in_model, "Place")
|
|
|
+ all_places = allInstances(model, "PetriNets/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(in_model, place, "tokens"))
|
|
|
+ dict_add_fast(dict_repr, place, read_attribute(model, place, "tokens"))
|
|
|
|
|
|
- all_transitions_original = allInstances(in_model, "Transition")
|
|
|
+ all_transitions_original = allInstances(model, "PetriNets/Transition")
|
|
|
|
|
|
mappings = create_node()
|
|
|
state_id = 0
|
|
@@ -85,16 +77,16 @@ Element function reachability_graph(params : Element, output_mms : Element):
|
|
|
set_add(workset, state_id)
|
|
|
|
|
|
// And add in the model itself
|
|
|
- state = instantiate_node(out_model, "InitialState", cast_i2s(state_id))
|
|
|
- instantiate_attribute(out_model, state, "name", cast_i2s(state_id))
|
|
|
- instantiate_attribute(out_model, state, "error", False)
|
|
|
+ state = instantiate_node(model, "ReachabilityGraph/InitialState", cast_i2s(state_id))
|
|
|
+ instantiate_attribute(model, state, "name", cast_i2s(state_id))
|
|
|
+ instantiate_attribute(model, state, "error", False)
|
|
|
keys = dict_keys(dict_repr)
|
|
|
while (read_nr_out(keys) > 0):
|
|
|
key = set_pop(keys)
|
|
|
- place = instantiate_node(out_model, "Place", "")
|
|
|
- instantiate_attribute(out_model, place, "name", read_attribute(in_model, key, "name"))
|
|
|
- instantiate_attribute(out_model, place, "tokens", dict_repr[key])
|
|
|
- instantiate_link(out_model, "Contains", "", state, place)
|
|
|
+ place = instantiate_node(model, "ReachabilityGraph/Place", "")
|
|
|
+ instantiate_attribute(model, place, "name", read_attribute(model, key, "name"))
|
|
|
+ instantiate_attribute(model, place, "tokens", dict_repr[key])
|
|
|
+ instantiate_link(model, "ReachabilityGraph/Contains", "", state, place)
|
|
|
|
|
|
while (read_nr_out(workset) > 0):
|
|
|
state_id = set_pop(workset)
|
|
@@ -156,35 +148,34 @@ Element function reachability_graph(params : Element, output_mms : Element):
|
|
|
set_add(workset, target_id)
|
|
|
|
|
|
// And add in the model itself
|
|
|
- state = instantiate_node(out_model, "State", cast_i2s(target_id))
|
|
|
- instantiate_attribute(out_model, state, "name", cast_i2s(target_id))
|
|
|
- instantiate_attribute(out_model, state, "error", False)
|
|
|
+ state = instantiate_node(model, "ReachabilityGraph/State", cast_i2s(target_id))
|
|
|
+ instantiate_attribute(model, state, "name", cast_i2s(target_id))
|
|
|
+ instantiate_attribute(model, state, "error", False)
|
|
|
|
|
|
keys = dict_keys(new_dict_repr)
|
|
|
Element sub
|
|
|
String name
|
|
|
while (read_nr_out(keys) > 0):
|
|
|
key = set_pop(keys)
|
|
|
- name = read_attribute(in_model, key, "name")
|
|
|
+ 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, new_dict_repr[key]))):
|
|
|
- place = instantiate_node(out_model, "Place", "")
|
|
|
- instantiate_attribute(out_model, place, "name", name)
|
|
|
- instantiate_attribute(out_model, place, "tokens", new_dict_repr[key])
|
|
|
+ place = instantiate_node(model, "ReachabilityGraph/Place", "")
|
|
|
+ instantiate_attribute(model, place, "name", name)
|
|
|
+ instantiate_attribute(model, place, "tokens", new_dict_repr[key])
|
|
|
dict_add_fast(sub, new_dict_repr[key], place)
|
|
|
else:
|
|
|
place = sub[new_dict_repr[key]]
|
|
|
- instantiate_link(out_model, "Contains", "", state, place)
|
|
|
+ instantiate_link(model, "ReachabilityGraph/Contains", "", state, place)
|
|
|
|
|
|
// 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(out_model, "Transition", "", cast_i2s(state_id), cast_i2s(target_id))
|
|
|
- instantiate_attribute(out_model, new_transition, "name", read_attribute(in_model, transition, "name"))
|
|
|
+ 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))
|
|
|
- dict_add_fast(result, "ReachabilityGraph", out_model)
|
|
|
- return result!
|
|
|
+ return True!
|