|
|
@@ -1,556 +1,181 @@
|
|
|
include "primitives.alh"
|
|
|
include "modelling.alh"
|
|
|
include "object_operations.alh"
|
|
|
-include "transform.alh"
|
|
|
-include "constructors.alh"
|
|
|
-include "compiler.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 enabled_transitions_set
|
|
|
- Element tv
|
|
|
- Element links
|
|
|
- Element mappings
|
|
|
- Element reachable_states
|
|
|
- Element keys
|
|
|
- Element enabled_transitions
|
|
|
- Element enabled_copy
|
|
|
- Element workset_copy
|
|
|
- Element curr_workset_el
|
|
|
- String transition
|
|
|
- String new_transition
|
|
|
- String tmp_transition
|
|
|
- String state
|
|
|
- String name
|
|
|
- String link
|
|
|
- String place
|
|
|
- String key
|
|
|
- String curr_transition
|
|
|
- String bp_name
|
|
|
- String curr_bp_name
|
|
|
- String to_construct
|
|
|
- String disable_on_trigger_str
|
|
|
- String user_input_s
|
|
|
- Integer link_weight
|
|
|
- Integer initial
|
|
|
- Integer state_id
|
|
|
- Integer next_id
|
|
|
- Integer user_input_i
|
|
|
- Boolean possible
|
|
|
- Boolean disable_on_trigger
|
|
|
- Element all_places
|
|
|
- Element dict_repr
|
|
|
- Element new_dict_repr
|
|
|
- Element work_unit
|
|
|
- Element curr_bp
|
|
|
- Element bp_keys
|
|
|
- Boolean bp_triggered
|
|
|
- Element reachable_keys_copy
|
|
|
- Element curr_reachable
|
|
|
- Element new_breakpoint
|
|
|
- Element curr_bp_function
|
|
|
- Element place_names_to_ids
|
|
|
-
|
|
|
- Element breakpoints
|
|
|
- breakpoints = create_node()
|
|
|
-
|
|
|
- Element cache
|
|
|
- cache = create_node()
|
|
|
-
|
|
|
- String user_input
|
|
|
- user_input = ""
|
|
|
- String mode
|
|
|
- mode = "paused"
|
|
|
-
|
|
|
- while (True):
|
|
|
- output('{"msg_type": "enabled_commands", "commands": ["step", "continuous", "manual", "add_breakpoint"]}')
|
|
|
- output('{"msg_type": "mode_change", "mode": "paused"}')
|
|
|
- log('waiting for user input')
|
|
|
- user_input = input()
|
|
|
- log(user_input)
|
|
|
- if (user_input == "simulation_mode"):
|
|
|
- user_input = input()
|
|
|
- if (user_input == "step"):
|
|
|
- output('{"msg_type": "enabled_commands", "commands": ["step", "continuous", "manual"]}')
|
|
|
- break!
|
|
|
- if (user_input == "continuous"):
|
|
|
- output('{"msg_type": "enabled_commands", "commands": []}')
|
|
|
- output('{"msg_type": "mode_change", "mode": "running"}')
|
|
|
- break!
|
|
|
- if (user_input == "manual"):
|
|
|
- output('{"msg_type": "enabled_commands", "commands": ["step", "continuous", "manual"]}')
|
|
|
- break!
|
|
|
- if (user_input == "add_breakpoint"):
|
|
|
- bp_name = ""
|
|
|
- while (bool_or(bp_name == "", dict_in(breakpoints, bp_name))):
|
|
|
- output('{"msg_type": "input_required", "name": "breakpoint name", "type": "string"}')
|
|
|
- bp_name = input()
|
|
|
- output('{"msg_type": "input_required", "name": "disable on trigger?", "type": "boolean"}')
|
|
|
- disable_on_trigger_str = input()
|
|
|
- if (disable_on_trigger_str == "True"):
|
|
|
- disable_on_trigger = True
|
|
|
- else:
|
|
|
- disable_on_trigger = False
|
|
|
- output('{"msg_type": "input_required", "name": "breakpoint function", "type": "code"}')
|
|
|
- new_breakpoint = create_node()
|
|
|
- String bp_code
|
|
|
- bp_code = input()
|
|
|
- dict_add_fast(new_breakpoint, "function", compile_code(bp_code))
|
|
|
- dict_add_fast(new_breakpoint, "disable_on_trigger", disable_on_trigger)
|
|
|
- dict_add_fast(new_breakpoint, "enabled", True)
|
|
|
- dict_add_fast(breakpoints, bp_name, new_breakpoint)
|
|
|
- output(('{"msg_type": "state_change", "state": "breakpoint_added", "breakpoint_name": "' + bp_name) + '"}')
|
|
|
- mode = user_input
|
|
|
-
|
|
|
- // Create a dictionary representation for each transition
|
|
|
- transition_vectors_produce = create_node()
|
|
|
- transition_vectors_consume = create_node()
|
|
|
- all_transitions = allInstances(model, "PetriNet/Transition")
|
|
|
- while (read_nr_out(all_transitions) > 0):
|
|
|
- transition = set_pop(all_transitions)
|
|
|
- String transition_name
|
|
|
- transition_name = read_attribute(model, transition, "name")
|
|
|
-
|
|
|
- tv = create_node()
|
|
|
- links = allIncomingAssociationInstances(model, transition, "PetriNet/P2T")
|
|
|
- while (read_nr_out(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_name, tv)
|
|
|
-
|
|
|
- tv = create_node()
|
|
|
- links = allOutgoingAssociationInstances(model, transition, "PetriNet/T2P")
|
|
|
- while (read_nr_out(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_name, tv)
|
|
|
-
|
|
|
- workset = create_node()
|
|
|
-
|
|
|
- all_places = allInstances(model, "PetriNet/Place")
|
|
|
- dict_repr = create_node()
|
|
|
- place_names_to_ids = create_node()
|
|
|
- while (read_nr_out(all_places) > 0):
|
|
|
- place = set_pop(all_places)
|
|
|
- dict_add_fast(dict_repr, place, read_attribute(model, place, "tokens"))
|
|
|
- dict_add_fast(place_names_to_ids, read_attribute(model, place, "name"), place)
|
|
|
-
|
|
|
- all_transitions_original = allInstances(model, "PetriNet/Transition")
|
|
|
-
|
|
|
- mappings = create_node()
|
|
|
- state_id = 0
|
|
|
- next_id = 1
|
|
|
- reachable_states = create_node()
|
|
|
- dict_add_fast(reachable_states, state_id, dict_repr)
|
|
|
- dict_add_fast(mappings, state_id, create_node())
|
|
|
-
|
|
|
- // And add in the model itself
|
|
|
- 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(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)
|
|
|
-
|
|
|
- enabled_transitions = create_node()
|
|
|
- dict_repr = reachable_states[state_id]
|
|
|
- enabled_transitions_set = create_node()
|
|
|
- dict_add(enabled_transitions, state_id, enabled_transitions_set)
|
|
|
-
|
|
|
- // 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 (read_nr_out(all_transitions) > 0):
|
|
|
- transition = set_pop(all_transitions)
|
|
|
- String transition_name
|
|
|
- transition_name = read_attribute(model, transition, "name")
|
|
|
-
|
|
|
- keys = dict_keys(transition_vectors_consume[transition_name])
|
|
|
- possible = True
|
|
|
- while (read_nr_out(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_name][key])):
|
|
|
- // Impossible transition, so discard this one
|
|
|
- possible = False
|
|
|
- break!
|
|
|
- if (possible):
|
|
|
- set_add(enabled_transitions_set, transition_name)
|
|
|
-
|
|
|
- if (read_nr_out(enabled_transitions[state_id]) > 0):
|
|
|
- set_add(workset, state_id)
|
|
|
-
|
|
|
- if (bool_or(mode == "step", mode == "manual")):
|
|
|
- output('{"msg_type": "state_change", "state": "initialized"}')
|
|
|
-
|
|
|
- Element dict_values
|
|
|
- Element all_values
|
|
|
- String place
|
|
|
- dict_values = create_node()
|
|
|
- all_values = allAssociationDestinations(model, cast_i2s(state_id), "ReachabilityGraph/Contains")
|
|
|
- while (read_nr_out(all_values) > 0):
|
|
|
- place = set_pop(all_values)
|
|
|
- dict_add(dict_values, read_attribute(model, place, "name"), cast_v2s(read_attribute(model, place, "tokens")))
|
|
|
- String marking
|
|
|
- marking = dict_to_string(dict_values)
|
|
|
- output(((('{"msg_type": "node_added", "node_info": {"node_id": ' + cast_v2s(read_attribute(model, cast_i2s(state_id), "name"))) + ', "node_marking": ') + marking) + '}}')
|
|
|
-
|
|
|
- if (mode == "step"):
|
|
|
- mode = "paused"
|
|
|
- output('{"msg_type": "mode_change", "mode": "paused"}')
|
|
|
-
|
|
|
- while (True):
|
|
|
- if (mode == "manual"):
|
|
|
- break!
|
|
|
- user_input = input()
|
|
|
- if (user_input == "simulation_mode"):
|
|
|
- user_input = input()
|
|
|
- if (user_input == "step"):
|
|
|
- mode = user_input
|
|
|
- output('{"msg_type": "enabled_commands", "commands": ["step", "continuous", "manual"]}')
|
|
|
- break!
|
|
|
- if (user_input == "continuous"):
|
|
|
- mode = user_input
|
|
|
- output('{"msg_type": "enabled_commands", "commands": []}')
|
|
|
- break!
|
|
|
- if (user_input == "manual"):
|
|
|
- mode = user_input
|
|
|
- output('{"msg_type": "enabled_commands", "commands": ["step", "continuous", "manual"]}')
|
|
|
- break!
|
|
|
-
|
|
|
- while (read_nr_out(workset) > 0):
|
|
|
- if (mode == "manual"):
|
|
|
- String markings
|
|
|
- markings = '['
|
|
|
- workset_copy = set_copy(workset)
|
|
|
- while (read_nr_out(workset_copy) > 0):
|
|
|
- curr_workset_el = set_pop(workset_copy)
|
|
|
- markings = ((markings + '"') + cast_v2s(curr_workset_el)) + '"'
|
|
|
- if (read_nr_out(workset_copy) > 0):
|
|
|
- markings = markings + ", "
|
|
|
- markings = markings + "]"
|
|
|
- output(('{"msg_type": "unexplored_markings", "markings": ' + markings) + '}')
|
|
|
- log("Please choose a marking.")
|
|
|
- while (True):
|
|
|
- user_input_s = input()
|
|
|
- if (user_input_s == 'simulation_mode'):
|
|
|
- mode = input()
|
|
|
- if (mode != 'manual'):
|
|
|
- state_id = set_pop(workset)
|
|
|
- dict_repr = reachable_states[state_id]
|
|
|
-
|
|
|
- enabled_transitions_set = enabled_transitions[state_id]
|
|
|
- transition = set_pop(enabled_transitions_set)
|
|
|
-
|
|
|
- if (mode == 'continuous'):
|
|
|
- output('{"msg_type": "enabled_commands", "commands": []}')
|
|
|
- if (mode == "step"):
|
|
|
- output('{"msg_type": "enabled_commands", "commands": ["step", "continuous", "manual"]}')
|
|
|
-
|
|
|
- break!
|
|
|
- elif (user_input_s == 'selected_marking'):
|
|
|
- user_input_i = cast_s2i(input())
|
|
|
- if (set_in(workset, user_input_i)):
|
|
|
- state_id = user_input_i
|
|
|
- enabled_transitions_set = enabled_transitions[state_id]
|
|
|
- String enabled_transitions_output
|
|
|
- enabled_transitions_output = '['
|
|
|
- enabled_copy = set_copy(enabled_transitions_set)
|
|
|
- while (read_nr_out(enabled_copy) > 0):
|
|
|
- curr_transition = set_pop(enabled_copy)
|
|
|
- enabled_transitions_output = enabled_transitions_output + cast_v2s(curr_transition)
|
|
|
- if (read_nr_out(enabled_copy) > 0):
|
|
|
- enabled_transitions_output = enabled_transitions_output + ", "
|
|
|
- enabled_transitions_output = enabled_transitions_output + "]"
|
|
|
- output(('{"msg_type": "enabled_transitions", "transitions": ' + enabled_transitions_output) + '}')
|
|
|
- elif (user_input_s == 'selected_transition'):
|
|
|
- set_remove(workset, state_id)
|
|
|
- dict_repr = reachable_states[state_id]
|
|
|
-
|
|
|
- user_input_s = input()
|
|
|
- transition = user_input_s
|
|
|
- set_remove(enabled_transitions_set, transition)
|
|
|
-
|
|
|
- break!
|
|
|
- else:
|
|
|
- state_id = set_pop(workset)
|
|
|
- dict_repr = reachable_states[state_id]
|
|
|
-
|
|
|
- enabled_transitions_set = enabled_transitions[state_id]
|
|
|
- transition = set_pop(enabled_transitions_set)
|
|
|
-
|
|
|
- if (read_nr_out(enabled_transitions[state_id]) > 0):
|
|
|
- set_add(workset, state_id)
|
|
|
-
|
|
|
- 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 (read_nr_out(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 (read_nr_out(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 (read_nr_out(keys) > 0):
|
|
|
- other_state_id = set_pop(keys)
|
|
|
-
|
|
|
- if (dict_eq(reachable_states[other_state_id], new_dict_repr)):
|
|
|
- target_id = other_state_id
|
|
|
- break!
|
|
|
-
|
|
|
- Boolean new_node
|
|
|
- new_node = False
|
|
|
- if (target_id == -1):
|
|
|
- new_node = True
|
|
|
- // 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, create_node())
|
|
|
-
|
|
|
- // And add in the model itself
|
|
|
- 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(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(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)
|
|
|
-
|
|
|
- // Compute how the PN behaves with this specific state
|
|
|
- // For this, we fetch all transitions and check if they are enabled
|
|
|
- enabled_transitions_set = create_node()
|
|
|
- dict_add(enabled_transitions, target_id, enabled_transitions_set)
|
|
|
- all_transitions = set_copy(all_transitions_original)
|
|
|
- while (read_nr_out(all_transitions) > 0):
|
|
|
- tmp_transition = set_pop(all_transitions)
|
|
|
- String transition_name
|
|
|
- transition_name = read_attribute(model, tmp_transition, "name")
|
|
|
-
|
|
|
- keys = dict_keys(transition_vectors_consume[transition_name])
|
|
|
- possible = True
|
|
|
- while (read_nr_out(keys) > 0):
|
|
|
- key = set_pop(keys)
|
|
|
-
|
|
|
- // Compare the values in the state with those consumed by the transition
|
|
|
- if (integer_lt(new_dict_repr[key], transition_vectors_consume[transition_name][key])):
|
|
|
- // Impossible transition, so discard this one
|
|
|
- possible = False
|
|
|
- break!
|
|
|
- if (possible):
|
|
|
- set_add(enabled_transitions_set, transition_name)
|
|
|
-
|
|
|
- if (read_nr_out(enabled_transitions[target_id]) > 0):
|
|
|
- set_add(workset, target_id)
|
|
|
-
|
|
|
- // 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_i2s(state_id), cast_i2s(target_id))
|
|
|
- instantiate_attribute(model, new_transition, "name", transition)
|
|
|
-
|
|
|
- if (bool_or(mode == "step", mode == "manual")):
|
|
|
- if (new_node):
|
|
|
- Element dict_values
|
|
|
- Element all_values
|
|
|
- String place
|
|
|
- dict_values = create_node()
|
|
|
- all_values = allAssociationDestinations(model, cast_i2s(target_id), "ReachabilityGraph/Contains")
|
|
|
- while (read_nr_out(all_values) > 0):
|
|
|
- place = set_pop(all_values)
|
|
|
- dict_add(dict_values, read_attribute(model, place, "name"), read_attribute(model, place, "tokens"))
|
|
|
- String marking
|
|
|
- marking = dict_to_string(dict_values)
|
|
|
- output(((('{"msg_type": "node_added", "node_info": {"node_id": ' + cast_v2s(read_attribute(model, cast_i2s(target_id), "name"))) + ', "node_marking": ') + marking) + '}}')
|
|
|
-
|
|
|
- String link_output
|
|
|
- link_output = '{"msg_type": "link_added", "link_info": {'
|
|
|
- link_output = link_output + '"transition": '
|
|
|
- link_output = link_output + cast_v2s(transition)
|
|
|
- link_output = link_output + ', "transition_id": '
|
|
|
- link_output = link_output + cast_v2s(new_transition)
|
|
|
- link_output = link_output + ', "source": "'
|
|
|
- link_output = link_output + cast_v2s(state_id)
|
|
|
- link_output = link_output + '", "target": "'
|
|
|
- link_output = link_output + cast_v2s(target_id)
|
|
|
- link_output = link_output + '"}}'
|
|
|
- output(link_output)
|
|
|
-
|
|
|
- if (mode == "step"):
|
|
|
- mode = "paused"
|
|
|
- output('{"msg_type": "mode_change", "mode": "paused"}')
|
|
|
-
|
|
|
- output('{"msg_type": "state_change", "state": "step_done"}')
|
|
|
-
|
|
|
- bp_keys = dict_keys(breakpoints)
|
|
|
- bp_triggered = False
|
|
|
- while (read_nr_out(bp_keys) > 0):
|
|
|
- curr_bp_name = set_pop(bp_keys)
|
|
|
- curr_bp = breakpoints[curr_bp_name]
|
|
|
- curr_bp_function = curr_bp["function"]
|
|
|
- if (bool_and(curr_bp["enabled"], curr_bp_function(reachable_states, mappings, place_names_to_ids))):
|
|
|
- output(('{"msg_type": "state_change", "state": "breakpoint_triggered", "breakpoint_name": "' + curr_bp_name) + '"}')
|
|
|
- bp_triggered = True
|
|
|
- log(curr_bp["disable_on_trigger"])
|
|
|
- if (curr_bp["disable_on_trigger"]):
|
|
|
- dict_delete(curr_bp, "enabled")
|
|
|
- dict_add_fast(curr_bp, "enabled", False)
|
|
|
- if (bp_triggered):
|
|
|
- Element all_states
|
|
|
- Element curr_state
|
|
|
- all_states = allInstances(model, "ReachabilityGraph/State")
|
|
|
- to_construct = '{"msg_type": "reachable_nodes", "nodes": ['
|
|
|
- while (read_nr_out(all_states) > 0):
|
|
|
- curr_state = set_pop(all_states)
|
|
|
- to_construct = to_construct + '{"node_id": '
|
|
|
- to_construct = to_construct + cast_v2s(curr_state)
|
|
|
- to_construct = to_construct + ', "node_marking": '
|
|
|
- Element dict_values
|
|
|
- Element all_values
|
|
|
- String place
|
|
|
- dict_values = create_node()
|
|
|
- all_values = allAssociationDestinations(model, curr_state, "ReachabilityGraph/Contains")
|
|
|
- while (set_len(all_values) > 0):
|
|
|
- place = set_pop(all_values)
|
|
|
- dict_add(dict_values, read_attribute(model, place, "name"), read_attribute(model, place, "tokens"))
|
|
|
- to_construct = to_construct + dict_to_string(dict_values)
|
|
|
- to_construct = to_construct + "}"
|
|
|
- if (read_nr_out(all_states) > 0):
|
|
|
- to_construct = to_construct + ', '
|
|
|
- to_construct = to_construct + ']}'
|
|
|
- output(to_construct)
|
|
|
-
|
|
|
- Element all_links
|
|
|
- Element curr_link
|
|
|
- all_links = allInstances(model, "ReachabilityGraph/Transition")
|
|
|
- to_construct = '{"msg_type": "node_links", "links": ['
|
|
|
- while (read_nr_out(all_links) > 0):
|
|
|
- curr_link = set_pop(all_links)
|
|
|
- to_construct = to_construct + '{"transition": '
|
|
|
- to_construct = to_construct + cast_v2s(read_attribute(model, curr_link, "name"))
|
|
|
- to_construct = to_construct + ', "transition_id": '
|
|
|
- to_construct = to_construct + cast_v2s(curr_link)
|
|
|
- to_construct = to_construct + ', "source": '
|
|
|
- to_construct = to_construct + cast_v2s(reverseKeyLookup(model["model"], read_edge_src(model["model"][curr_link])))
|
|
|
- to_construct = to_construct + ', "target": '
|
|
|
- to_construct = to_construct + cast_v2s(reverseKeyLookup(model["model"], read_edge_dst(model["model"][curr_link])))
|
|
|
- to_construct = to_construct + '}'
|
|
|
- if (read_nr_out(all_links) > 0):
|
|
|
- to_construct = to_construct + ', '
|
|
|
- to_construct = to_construct + ']}'
|
|
|
- output(to_construct)
|
|
|
-
|
|
|
- output('{"msg_type": "enabled_commands", "commands": ["step", "continuous", "manual"]}')
|
|
|
- if (bool_not(mode == "paused")):
|
|
|
- mode = "paused"
|
|
|
- output('{"msg_type": "mode_change", "mode": "paused"}')
|
|
|
-
|
|
|
- if (bool_not(mode == "continuous")):
|
|
|
- while (True):
|
|
|
- if (mode == "manual"):
|
|
|
- break!
|
|
|
- user_input = input()
|
|
|
- if (user_input == "simulation_mode"):
|
|
|
- user_input = input()
|
|
|
- if (user_input == "step"):
|
|
|
- mode = user_input
|
|
|
- output('{"msg_type": "enabled_commands", "commands": ["step", "continuous", "manual"]}')
|
|
|
- break!
|
|
|
- if (user_input == "continuous"):
|
|
|
- mode = user_input
|
|
|
- output('{"msg_type": "enabled_commands", "commands": []}')
|
|
|
- break!
|
|
|
- if (user_input == "manual"):
|
|
|
- mode = user_input
|
|
|
- output('{"msg_type": "enabled_commands", "commands": ["step", "continuous", "manual"]}')
|
|
|
- break!
|
|
|
-
|
|
|
- Element all_states
|
|
|
- Element curr_state
|
|
|
- all_states = allInstances(model, "ReachabilityGraph/State")
|
|
|
- to_construct = '{"msg_type": "reachable_nodes", "nodes": ['
|
|
|
- while (read_nr_out(all_states) > 0):
|
|
|
- curr_state = set_pop(all_states)
|
|
|
- to_construct = to_construct + '{"node_id": '
|
|
|
- to_construct = to_construct + cast_v2s(curr_state)
|
|
|
- to_construct = to_construct + ', "node_marking": '
|
|
|
- Element dict_values
|
|
|
- Element all_values
|
|
|
- String place
|
|
|
- dict_values = create_node()
|
|
|
- all_values = allAssociationDestinations(model, curr_state, "ReachabilityGraph/Contains")
|
|
|
- while (set_len(all_values) > 0):
|
|
|
- place = set_pop(all_values)
|
|
|
- dict_add(dict_values, read_attribute(model, place, "name"), read_attribute(model, place, "tokens"))
|
|
|
- to_construct = to_construct + dict_to_string(dict_values)
|
|
|
- to_construct = to_construct + "}"
|
|
|
- if (read_nr_out(all_states) > 0):
|
|
|
- to_construct = to_construct + ', '
|
|
|
- to_construct = to_construct + ']}'
|
|
|
- output(to_construct)
|
|
|
-
|
|
|
- Element all_links
|
|
|
- Element curr_link
|
|
|
- all_links = allInstances(model, "ReachabilityGraph/Transition")
|
|
|
- to_construct = '{"msg_type": "node_links", "links": ['
|
|
|
- while (read_nr_out(all_links) > 0):
|
|
|
- curr_link = set_pop(all_links)
|
|
|
- to_construct = to_construct + '{"transition": '
|
|
|
- to_construct = to_construct + cast_v2s(read_attribute(model, curr_link, "name"))
|
|
|
- to_construct = to_construct + ', "transition_id": '
|
|
|
- to_construct = to_construct + cast_v2s(curr_link)
|
|
|
- to_construct = to_construct + ', "source": '
|
|
|
- to_construct = to_construct + cast_v2s(reverseKeyLookup(model["model"], read_edge_src(model["model"][curr_link])))
|
|
|
- to_construct = to_construct + ', "target": '
|
|
|
- to_construct = to_construct + cast_v2s(reverseKeyLookup(model["model"], read_edge_dst(model["model"][curr_link])))
|
|
|
- to_construct = to_construct + '}'
|
|
|
- if (read_nr_out(all_links) > 0):
|
|
|
- to_construct = to_construct + ', '
|
|
|
- to_construct = to_construct + ']}'
|
|
|
- output(to_construct)
|
|
|
-
|
|
|
- output('{"msg_type": "mode_change", "mode": "finished"}')
|
|
|
-
|
|
|
- log("# reachable states: " + cast_v2s(next_id))
|
|
|
- return True!
|
|
|
+ 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
|
|
|
+ break!
|
|
|
+
|
|
|
+ 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
|
|
|
+ break!
|
|
|
+
|
|
|
+ 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!
|
