|
@@ -2,14 +2,14 @@ include "primitives.alh"
|
|
|
include "modelling.alh"
|
|
include "modelling.alh"
|
|
|
include "object_operations.alh"
|
|
include "object_operations.alh"
|
|
|
|
|
|
|
|
-Element function coverability_graph(params : Element, output : Element):
|
|
|
|
|
|
|
+Element function reachability_graph(params : Element, output : Element):
|
|
|
Element result
|
|
Element result
|
|
|
Element model
|
|
Element model
|
|
|
Element workset
|
|
Element workset
|
|
|
String state
|
|
String state
|
|
|
|
|
|
|
|
result = create_node()
|
|
result = create_node()
|
|
|
- out_model = instantiate_node(output["CoverabilityGraph"])
|
|
|
|
|
|
|
+ out_model = instantiate_node(output["ReachabilityGraph"])
|
|
|
in_model = params["PetriNets"]
|
|
in_model = params["PetriNets"]
|
|
|
|
|
|
|
|
// Create a dictionary representation for each transition
|
|
// Create a dictionary representation for each transition
|
|
@@ -40,24 +40,22 @@ Element function coverability_graph(params : Element, output : Element):
|
|
|
dict_add(tv, name, link_weight)
|
|
dict_add(tv, name, link_weight)
|
|
|
|
|
|
|
|
workset = create_node()
|
|
workset = create_node()
|
|
|
- initial = instantiate_node(out_model, "InitialState", "")
|
|
|
|
|
|
|
|
|
|
all_places = allInstances(in_model, "Place")
|
|
all_places = allInstances(in_model, "Place")
|
|
|
dict_repr = create_node()
|
|
dict_repr = create_node()
|
|
|
while (read_nr_out(all_places) > 0):
|
|
while (read_nr_out(all_places) > 0):
|
|
|
place = set_pop(all_places)
|
|
place = set_pop(all_places)
|
|
|
- state_config = instantiate_node(out_model, "Place", "")
|
|
|
|
|
- instantiate_attribute(out_model, state_config, "name", read_attribute(in_model, place, "name"))
|
|
|
|
|
- instantiate_attribute(out_model, state_config, "tokens", read_attribute(in_model, place, "tokens"))
|
|
|
|
|
- instantiate_link(out_model, "", "", initial, state_config)
|
|
|
|
|
dict_add(dict_repr, read_attribute(in_model, place, "name"), read_attribute(in_model, place, "tokens"))
|
|
dict_add(dict_repr, read_attribute(in_model, place, "name"), read_attribute(in_model, place, "tokens"))
|
|
|
|
|
|
|
|
|
|
+ initial = 0
|
|
|
|
|
+
|
|
|
set_add(workset, create_tuple(initial, dict_repr))
|
|
set_add(workset, create_tuple(initial, dict_repr))
|
|
|
|
|
+ mappings = create_node()
|
|
|
|
|
|
|
|
while (read_nr_out(workset) > 0):
|
|
while (read_nr_out(workset) > 0):
|
|
|
- work_unit = set_pop(workset)
|
|
|
|
|
- state = work_unit[0]
|
|
|
|
|
- dict_repr = dict_copy(work_unit[1])
|
|
|
|
|
|
|
+ dict_repr = set_pop(workset)
|
|
|
|
|
+ // TODO check if dict_repr is already in the set of reachable states
|
|
|
|
|
+ set_add(reachable_states, dict_repr)
|
|
|
|
|
|
|
|
// Compute how the PN behaves with this specific state
|
|
// Compute how the PN behaves with this specific state
|
|
|
// For this, we fetch all transitions and check if they are enabled
|
|
// For this, we fetch all transitions and check if they are enabled
|
|
@@ -73,9 +71,10 @@ Element function coverability_graph(params : Element, output : Element):
|
|
|
if (dict_repr[key] < transition_vectors_consume[name][key]):
|
|
if (dict_repr[key] < transition_vectors_consume[name][key]):
|
|
|
// Impossible transition, so discard this one
|
|
// Impossible transition, so discard this one
|
|
|
possible = False
|
|
possible = False
|
|
|
- continue!
|
|
|
|
|
|
|
+ break!
|
|
|
|
|
|
|
|
if (possible):
|
|
if (possible):
|
|
|
|
|
+ dict_repr = dict_copy(work_unit[1])
|
|
|
// Transition can execute, so compute and add the new state based on the consume/produce vectors
|
|
// Transition can execute, so compute and add the new state based on the consume/produce vectors
|
|
|
keys = dict_keys(transition_vectors_consume[name])
|
|
keys = dict_keys(transition_vectors_consume[name])
|
|
|
while (read_nr_out(keys) > 0):
|
|
while (read_nr_out(keys) > 0):
|
|
@@ -86,8 +85,8 @@ Element function coverability_graph(params : Element, output : Element):
|
|
|
key = set_pop(keys)
|
|
key = set_pop(keys)
|
|
|
dict_overwrite(dict_repr, key, dict_repr[key] + transition_vectors_produce[name][key])
|
|
dict_overwrite(dict_repr, key, dict_repr[key] + transition_vectors_produce[name][key])
|
|
|
|
|
|
|
|
- // Now write out the dictionary representation to a model!
|
|
|
|
|
- // TODO
|
|
|
|
|
|
|
+ // Add the target to workset
|
|
|
|
|
+ set_add(workset, dict_repr)
|
|
|
|
|
|
|
|
- dict_add(result, "CoverabilityGraph", out_model)
|
|
|
|
|
|
|
+ dict_add(result, "ReachabilityGraph", out_model)
|
|
|
return result!
|
|
return result!
|