modelverse/models/bfs.alc

include "primitives.alh"
include "modelling.alh"
include "object_operations.alh"

Element function bfs(params : Element, output_mms : Element):
	Element model
	String initial
	Element options
	Element worklist
	Element work_unit
	String state
	Element path
	Element path_copy
	Element visited
	Element visited_copy
	String option
	String dest

	model = params["reachability_graph"]

	worklist = create_node()
	initial = set_pop(allInstances(model, "InitialState"))
	work_unit = create_node()
	list_append(work_unit, initial)
	path = create_node()
	list_append(work_unit, path)
	visited = create_node()
	set_add(visited, initial)
	list_append(work_unit, visited)

	list_append(worklist, work_unit)

	while (read_nr_out(worklist) > 0):
		work_unit = list_pop(worklist, 0)
		state = work_unit[0]
		path = work_unit[1]
		visited = work_unit[2]
		log("Searching for length " + cast_v2s(read_nr_out(path)))

		if (value_eq(read_attribute(model, state, "error"), True)):
			// Found an error path!
			log("Found error path!")
			log(list_to_string(path))
			output("Found error path:")
			output(list_to_string(path))
			break!

		options = allOutgoingAssociationInstances(model, state, "Transition")
		while (read_nr_out(options) > 0):
			option = set_pop(options)
			dest = readAssociationDestination(model, option)
			
			if (set_in(visited, dest)):
				// Already visited this node, so skip
				continue!

			path_copy = dict_copy(path)
			visited_copy = set_copy(visited)

			set_add(visited_copy, dest)
			list_append(path_copy, read_attribute(model, option, "name"))

			work_unit = create_node()
			list_append(work_unit, dest)
			list_append(work_unit, path_copy)
			list_append(work_unit, visited_copy)
			list_append(worklist, work_unit)

	return create_node()!