asm FerrymanSimulated
import ../STDL/StandardLibrary
import ../STDL/CTLLibrary

signature:
	enum domain Side = {LEFT | RIGHT}
	enum domain Actors = {GOAT, CABBAGE, WOLF, FERRYMAN}
	controlled position: Actors -> Side
	static swap: Side -> Side
	derived completed: Boolean
	static danger: Prod(Actors, Actors) -> 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 danger($a1 in Actors, $a2 in Actors) = (
		$a1 = GOAT and $a2 = WOLF or
		$a1 = WOLF and $a2 = GOAT or
	 	$a1 = GOAT and $a2 = CABBAGE or
	 	$a1 = CABBAGE and $a2 = GOAT
	)
	
	CTLSPEC ag(position(GOAT) = position(CABBAGE) implies position(GOAT) = position(FERRYMAN)) // safety
	CTLSPEC ag(position(GOAT) = position(WOLF) implies position(GOAT) = position(FERRYMAN)) // safety
	CTLSPEC ef(completed) // reachability
	CTLSPEC ef(position(GOAT) = LEFT and (forall $a in Actors with $a != GOAT implies position($a) = RIGHT)) // reachability 
	CTLSPEC ef(position(CABBAGE) = RIGHT and (forall $a in Actors with $a != CABBAGE implies position($a) = LEFT)) // reachability
	
	main rule r_Main = 
		if not completed then
			choose $a1 in Actors with position($a1) = position(FERRYMAN) and 
				(forall $a2 in Actors, $a3 in Actors with 
					($a1 != $a2 and $a1 != $a3 and position($a2) = position(FERRYMAN) and position($a3) = position(FERRYMAN) implies 
					not(danger($a2, $a3))))
			do
				par
					position(FERRYMAN) := swap(position(FERRYMAN))
					position($a1) := swap(position($a1))
				endpar
		endif

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