modelverse/integration/code/pn_semantics.alc

Element function petrinet_enabled(model : Element):
    Element set_enabled
    set_enabled = petrinet_enabled_set(model)
    output("Enabled transitions:")
    while (0 < read_nr_out(set_enabled)):
        output(set_pop(set_enabled))
    return model

Element function petrinet_enabled_set(model : Element):
    Element all_transitions
    Element enabled_transitions
    String under_study
    Element in_arcs
    String arc_under_study
    Boolean enabled

    all_transitions = allInstances(model, "Transition")
    enabled_transitions = create_node()

    while (0 < read_nr_out(all_transitions)):
        under_study = set_pop(all_transitions)
        enabled = True

        // Find all incoming transitions
        in_arcs = allIncomingAssociationInstances(model, under_study, "P2T")

        while (0 < read_nr_out(in_arcs)):
            arc_under_study = set_pop(in_arcs)

            Integer present_tokens
            Integer required_tokens
            required_tokens = read_attribute(model, arc_under_study, "weight")
            log("Weight: " + cast_i2s(required_tokens))
            present_tokens = read_attribute(model, reverseKeyLookup(model["model"], read_edge_src(model["model"][arc_under_study])), "tokens")
            log("Tokens: " + cast_i2s(present_tokens))
            if (present_tokens < required_tokens):
                // Less tokens than required, so disable the transition completely
                enabled = False

        if (enabled):
            set_add(enabled_transitions, under_study)

    log("Got all enabled transitions!")
    return enabled_transitions

Element function petrinet_fire(model : Element):
    output("Transition to fire?")
    String transition
    transition = input()
    if (dict_in(model["model"], transition)):
        if (set_in(petrinet_enabled_set(model), transition)):
            Element workset
            String working_place
            String working_arc
            Integer new_value

            // Consume tokens
            workset = allIncomingAssociationInstances(model, transition, "P2T")
            while (0 < read_nr_out(workset)):
                working_arc = set_pop(workset)
                working_place = reverseKeyLookup(model["model"], read_edge_src(model["model"][working_arc]))
                new_value = integer_subtraction(read_attribute(model, working_place, "tokens"), read_attribute(model, working_arc, "weight"))
                unset_attribute(model, working_place, "tokens")
                instantiate_attribute(model, working_place, "tokens", new_value)
                output((("  " + working_place) + ": ") + cast_i2s(read_attribute(model, working_place, "tokens")))

            // Add tokens
            workset = allOutgoingAssociationInstances(model, transition, "T2P")
            while (0 < read_nr_out(workset)):
                working_arc = set_pop(workset)
                working_place = reverseKeyLookup(model["model"], read_edge_dst(model["model"][working_arc]))
                new_value = integer_addition(read_attribute(model, working_place, "tokens"), read_attribute(model, working_arc, "weight"))
                unset_attribute(model, working_place, "tokens")
                instantiate_attribute(model, working_place, "tokens", new_value)
                output((("  " + working_place) + ": ") + cast_i2s(read_attribute(model, working_place, "tokens")))
            output("Transition fired!")
        else:
            output("Cannot fire if not enabled; aborting")
    else:
        output("Unknown transition; aborting")
    return model

Element function main():
	Element model
	String cmd

	model = read_root()
	while (element_eq(model, read_root())):
		output("Which model do you want to execute with petri net semantics?")
		model = import_node(input())

	while (True):
		output("Which operation do you want to execute?")
		cmd = input()