***
*** River crossing example (version 3)
***
*** Essentially a renaming of the previous version
***

fmod RIVER-DATA is
	sorts Being Side Group River .
	subsorts Being Side < Group .

	ops shepherd wolf goat cabbage : -> Being [ctor] .
	ops left right : -> Side [ctor] .
	op __  : Group Group -> Group [ctor assoc comm prec 40] .
	op _|_ : Group Group -> River [ctor comm] .

	vars G1 G2 : Group .

	op initial : -> River .
	eq initial = left shepherd wolf goat cabbage | right .

	op risky : River -> Bool .
	eq risky(shepherd G1 | G2 wolf goat ) = true .
	eq risky(shepherd G1 | G2 goat cabbage) = true .
	eq risky(G1 | G2) = false [owise] .
endfm

mod RIVER is
	protecting RIVER-DATA .

	vars L R : Group .

	rl [alone]   :         shepherd L | R => L | R shepherd .
	rl [wolf]    :    shepherd wolf L | R => L | R shepherd wolf .
	rl [goat]    :    shepherd goat L | R => L | R shepherd goat .
	rl [cabbage] : shepherd cabbage L | R => L | R shepherd cabbage .

	rl [wolf-eats] :    wolf goat L | R shepherd => wolf L | R shepherd .
	rl [goat-eats] : goat cabbage L | R shepherd => goat L | R shepherd .
endm

smod RIVER-STRAT is
	protecting RIVER .

	var G : Group .

	strats oneCrossing eating eatb4cross cross&eat solved @ River .

	sd oneCrossing := alone | wolf | goat | cabbage .
	sd eating      := wolf-eats | goat-eats .
	sd eatb4cross  := eating or-else oneCrossing .
	sd cross&eat   := oneCrossing ; eating ! .
	sd solved      := match left | right shepherd wolf cabbage goat .

	strats eagerEating eagerEating2 safe @ River .

	sd eagerEating := solved ? idle : (eatb4cross ; eagerEating) .
	sd eagerEating2 := solved ? idle : (cross&eat ; eagerEating2) .
	sd safe := solved ? idle : (oneCrossing ; not(eating) ; safe) .
endsm

sload model-checker

mod RIVER-PREDS is
	protecting RIVER .
	including SATISFACTION .

	subsort River < State .
	ops goal risky death : -> Prop [ctor] .

	var  R    : River .
	var  B    : Being .
	vars G G' : Group .

	eq left | right shepherd wolf goat cabbage |= goal = true .
	eq R |= goal = false [owise] .
	eq G cabbage | G' goat |= death = false .
	eq G cabbage goat | G' |= death = false .
	eq R |= death = true [owise] .
	eq R |= risky = risky(R) .
endm

smod RIVER-CHECK is
	protecting RIVER-PREDS .
	protecting RIVER-STRAT .
	including STRATEGY-MODEL-CHECKER .
	including MODEL-CHECKER .
endsm