modelverse/models/bfs.alc

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

Boolean function bfs(model : Element):
	String initial
	Element options
	Element worklist
	Element work_unit
	String state
	Element path
	Element path_copy
	String option
	Element visited
	String dest
	Integer total_states

	total_states = read_nr_out(allInstances(model, "ReachabilityGraph/State"))

	worklist = create_node()
	visited = create_node()
	initial = set_pop(allInstances(model, "ReachabilityGraph/InitialState"))
	list_append(worklist, create_tuple(initial, create_node()))
	set_add(visited, initial)

	while (read_nr_out(worklist) > 0):
		work_unit = list_pop(worklist, 0)
		state = work_unit[0]
		path = work_unit[1]

		if (read_nr_out(visited) == total_states):
			log("No error path found!")
			break!

		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, "ReachabilityGraph/Transition")

		while (read_nr_out(options) > 0):
			option = set_pop(options)
			dest = readAssociationDestination(model, option)

			if (set_in(visited, dest)):
				continue!
			else:
				path_copy = dict_copy(path)
				list_append(path_copy, read_attribute(model, option, "name"))
				list_append(worklist, create_tuple(dest, path_copy))
				set_add(visited, dest)

	return True!