asm Ferryman
import ../STDL/StandardLibrary
import ../STDL/CTLLibrary

signature:
	enum domain Side = {LEFT | RIGHT}
	enum domain Actors = {GOAT, CABBAGE, WOLF, FERRYMAN}
	controlled position: Actors -> Side
	monitored choice: Actors
	static swap: Side -> Side
	derived completed: Boolean
	derived failed: Boolean

definitions:
	function swap($s in Side) =
		if $s = LEFT then RIGHT else LEFT endif
		
	function completed = (forall $a in Actors with position($a) = RIGHT)
	function failed = (
		position(GOAT) = position(WOLF) and position(GOAT) != position(FERRYMAN) or
	 	position(GOAT) = position(CABBAGE) and position(GOAT) != position(FERRYMAN)
	)
	
	CTLSPEC ag(position(GOAT) = position(CABBAGE) implies position(GOAT) = position(FERRYMAN))
	CTLSPEC ag(position(GOAT) = position(WOLF) implies position(GOAT) = position(FERRYMAN))
	
	main rule r_Main = 
		if not completed and not failed then
			if position(choice) = position(FERRYMAN) then
				par
					position(FERRYMAN) := swap(position(FERRYMAN))
					position(choice) := swap(position(choice))
				endpar
			endif
		endif

default init s0:
	function position($a in Actors) = LEFT