-- ------------------------------------------------------ --
-- Bridge Crossing Problem	(N. Markey, Jan 22, 2004) --
-- ------------------------------------------------------ --

MODULE viking(time, lamp, go)
VAR
  position: 0..3; 	-- 0=left, 1=left->right, 2=right, 3=right->left
  wait: 0..25;
  changed: boolean;
INIT
  position=0 & !changed & wait=0;
TRANS
 ( (!go) -> ( ( (position mod 2=1) -> ( ( (wait>1) -> (
			next(wait)=wait - 1 & 
			next(position)=position & 
			next(changed)=0 ) ) &
					( (wait=1) -> (
			next(position)=(position+1) mod 4 & 
			next(wait)=0 & 
			next(changed)=1 ) ) ) ) &
	      ( (position mod 2=0) -> (
			next(changed)=changed & 
			next(wait)=0 & 
			next(position)=position ) ) ) ) &
 ( go -> -- necessarily, position mod 2=0
	( ( ( (lamp & position=0)|(!lamp & position=2) ) -> ( (
			next(position) = position+1 &
			next(wait) = time - 1 &
			next(changed)=0
			) | (
			next(position)=position &
			next(wait)=0 &
			next(changed)=0 ) ) ) &
	  ( ( (lamp & position=2)|(!lamp & position=0) ) -> ( (
			next(position)=position &
			next(wait)=0 &
			next(changed)=0 ) ) ) ) )

MODULE main
VAR
  v1: viking(5, lamp, go);
  v2: viking(10, lamp, go);
  v3: viking(20, lamp, go);
  v4: viking(25, lamp, go);
  lamp: boolean;

DEFINE
  go:= (v1.position=0|v1.position=2) & (v2.position=0|v2.position=2) &
       (v3.position=0|v3.position=2) & (v4.position=0|v4.position=2);
  bridge:= (v1.wait!=0) + (v2.wait!=0) + (v3.wait!=0) + (v4.wait!=0);  
  initial:= v1.position=0 & v2.position=0 & v3.position=0 & v4.position=0;
  safe:= v1.position=2 & v2.position=2 & v3.position=2 & v4.position=2;
  crossing:= (bridge!=0);

INVAR
  (bridge<=2)

INIT
  lamp;

TRANS
  (go & next(bridge)>0) <-> (next(lamp) = !lamp);

COMPUTE MIN[initial, safe]
--SPEC AG EBF 0..85 safe
--SPEC AG ( (!crossing) -> EBF 0..85 (safe & !crossing) )