123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186 |
- include "primitives.alh"
- include "modelling.alh"
- include "object_operations.alh"
- Boolean function reachability_graph(model : Element):
- Element workset
- Element transition_vectors_produce
- Element transition_vectors_consume
- Element all_transitions
- Element all_transitions_original
- Element tv
- Element links
- Element mappings
- Element reachable_states
- Element keys
- String transition
- String new_transition
- String state
- String name
- String link
- String place
- String key
- Integer link_weight
- Integer initial
- Integer state_id
- Integer next_id
- Boolean possible
- Element all_places
- Element dict_repr
- Element new_dict_repr
- Element work_unit
- Element cache
- cache = dict_create()
- // Create a dictionary representation for each transition
- transition_vectors_produce = dict_create()
- transition_vectors_consume = dict_create()
- all_transitions = allInstances(model, "PetriNet/Transition")
- while (set_len(all_transitions) > 0):
- transition = set_pop(all_transitions)
- tv = dict_create()
- links = allIncomingAssociationInstances(model, transition, "PetriNet/P2T")
- while (set_len(links) > 0):
- link = set_pop(links)
- 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 = dict_create()
- links = allOutgoingAssociationInstances(model, transition, "PetriNet/T2P")
- while (set_len(links) > 0):
- link = set_pop(links)
- 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 = set_create()
- all_places = allInstances(model, "PetriNet/Place")
- dict_repr = dict_create()
- while (set_len(all_places) > 0):
- place = set_pop(all_places)
- dict_add_fast(dict_repr, place, read_attribute(model, place, "tokens"))
- all_transitions_original = allInstances(model, "PetriNet/Transition")
- mappings = dict_create()
- state_id = 0
- next_id = 1
- reachable_states = dict_create()
- dict_add_fast(reachable_states, state_id, dict_repr)
- dict_add_fast(mappings, state_id, dict_create())
- set_add(workset, state_id)
- // And add in the model itself
- state = instantiate_node(model, "ReachabilityGraph/InitialState", cast_string(state_id))
- instantiate_attribute(model, state, "name", cast_string(state_id))
- instantiate_attribute(model, state, "error", False)
- keys = dict_keys(dict_repr)
- while (set_len(keys) > 0):
- key = set_pop(keys)
- 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 (set_len(workset) > 0):
- state_id = set_pop(workset)
- dict_repr = reachable_states[state_id]
- // Compute how the PN behaves with this specific state
- // For this, we fetch all transitions and check if they are enabled
- all_transitions = set_copy(all_transitions_original)
- while (set_len(all_transitions) > 0):
- transition = set_pop(all_transitions)
- keys = dict_keys(transition_vectors_consume[transition])
- possible = True
- while (set_len(keys) > 0):
- key = set_pop(keys)
- // Compare the values in the state with those consumed by the transition
- if (integer_lt(dict_repr[key], transition_vectors_consume[transition][key])):
- // Impossible transition, so discard this one
- possible = False
- // Alternative implementation of break, which seems to crash JIT sometimes
- //break!
- keys = set_create()
- if (possible):
- new_dict_repr = dict_copy(dict_repr)
- // Transition can execute, so compute and add the new state based on the consume/produce vectors
- keys = dict_keys(transition_vectors_consume[transition])
- while (set_len(keys) > 0):
- key = set_pop(keys)
- dict_overwrite(new_dict_repr, key, integer_subtraction(new_dict_repr[key], transition_vectors_consume[transition][key]))
- keys = dict_keys(transition_vectors_produce[transition])
- while (set_len(keys) > 0):
- key = set_pop(keys)
- dict_overwrite(new_dict_repr, key, integer_addition(new_dict_repr[key], transition_vectors_produce[transition][key]))
- // Check if this state already has an associated ID
- Integer other_state_id
- Integer target_id
- keys = dict_keys(reachable_states)
- target_id = -1
- Float start
- while (set_len(keys) > 0):
- other_state_id = set_pop(keys)
- if (dict_eq(reachable_states[other_state_id], new_dict_repr)):
- target_id = other_state_id
- // Alternative implementation of break, which seems to crash JIT sometimes
- //break!
- keys = set_create()
- if (target_id == -1):
- // New state
- target_id = next_id
- next_id = next_id + 1
- // Add to all data structures
- dict_add_fast(reachable_states, target_id, new_dict_repr)
- dict_add_fast(mappings, target_id, dict_create())
- set_add(workset, target_id)
- // And add in the model itself
- state = instantiate_node(model, "ReachabilityGraph/State", cast_string(target_id))
- instantiate_attribute(model, state, "name", cast_string(target_id))
- instantiate_attribute(model, state, "error", False)
- keys = dict_keys(new_dict_repr)
- Element sub
- String name
- while (set_len(keys) > 0):
- key = set_pop(keys)
- name = read_attribute(model, key, "name")
- if (bool_not(dict_in(cache, name))):
- dict_add_fast(cache, name, dict_create())
- sub = cache[name]
- if (bool_not(dict_in(sub, 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(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(model, "ReachabilityGraph/Transition", "", cast_string(state_id), cast_string(target_id))
- instantiate_attribute(model, new_transition, "name", read_attribute(model, transition, "name"))
- log("# reachable states: " + cast_value(next_id))
- return True!
|