|
|
@@ -34,6 +34,9 @@ Element function reachability_graph(params : Element, output_mms : Element):
|
|
|
Element new_dict_repr
|
|
|
Element work_unit
|
|
|
|
|
|
+ Element cache
|
|
|
+ cache = create_node()
|
|
|
+
|
|
|
result = create_node()
|
|
|
out_model = instantiate_model(output_mms["ReachabilityGraph"])
|
|
|
in_model = params["pn"]
|
|
|
@@ -160,13 +163,25 @@ 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?
|
|
|
+ Element sub
|
|
|
+ String name
|
|
|
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", new_dict_repr[key])
|
|
|
+ name = read_attribute(in_model, key, "name")
|
|
|
+ if (bool_not(dict_in(cache, name))):
|
|
|
+ dict_add(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])
|
|
|
+ dict_add(sub, new_dict_repr[key], place)
|
|
|
+ log("Added to cache")
|
|
|
+ else:
|
|
|
+ place = sub[new_dict_repr[key]]
|
|
|
+ log("Accessed cache!")
|
|
|
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
|
|
|
dict_add(mappings[state_id], transition, target_id)
|
