modelverse/integration/code/pn_semantics.alc

include "primitives.alh"
include "modelling.alh"
include "object_operations.alh"
include "library.alh"
include "conformance_scd.alh"

Void 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!

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!

Void 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!

Void function petrinet_list(model : Element):
	Element keys 
	Element typemap
	Element place
	String name

	keys = dict_keys(model["model"])
	typemap = model["type_mapping"]
	place = model["metamodel"]["model"]["Place"]

	while (list_len(keys) > 0):
		name = set_pop(keys)
		if (element_eq(dict_read_node(typemap, model["model"][name]), place)):
			// Found a place
			output((name + ": ") + cast_i2s(read_attribute(model, name, "tokens")))
	return!

Void function main():
	Element model
	String verify_result

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

		if (element_eq(model, read_root())):
			output("Could not find model; aborting")
		elif (element_neq(model["metamodel"], import_node("models/PetriNets"))):
			output("Not a PetriNets model; aborting")
		else:
			verify_result = conformance_scd(model)
			if (verify_result == "OK"):
				output("Model OK!")
				execute_petrinet(model)
			else:
				output("Non-conforming model: " + verify_result)

	return!

Void function execute_petrinet(model : Element):
	String cmd
	while (True):
		output("Which operation do you want to execute?")
		cmd = input()

		if (cmd == "help"):
			output("Supported operations:")
			output("  help    -- this information")
			output("  enabled -- list the enabled transitions")
			output("  fire    -- fire a transition")
			output("  list    -- list the state of the petrinet")
			output("  exit    -- select another model")
		elif (cmd == "enabled"):
			petrinet_enabled(model)
		elif (cmd == "fire"):
			petrinet_fire(model)
		elif (cmd == "list"):
			petrinet_list(model)
		elif (cmd == "exit"):
			return!
		else:
			output("Did not understand command!")
			output("Use 'help' for a list of available options")

	return!