modelverse/models/reachability.alc

include "primitives.alh"
include "modelling.alh"
include "object_operations.alh"
include "transform.alh"
include "constructors.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 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"}')
        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()
            dict_add_fast(new_breakpoint, "function", construct_function())
            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()
    while (read_nr_out(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 = 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!
            output("Please enter your command. Options: continuous, step, manual")
            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) + '}')
                        output("Please choose an enabled transition or another marking.")
                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))):
                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!
                output("Please enter your command. Options: continuous, step, manual")
                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!