-- -------------------------------------------------------
--            Bridge crossing at night                  --
-- -------------------------------------------------------

MODULE person(time,lamp,duration)
-- knows its time for crossing, the position of the lamp, 
-- and may impose the value for duration

VAR 
  state: boolean;               -- true = left of the bridge, false = right
  changed: boolean;             -- true if the person just crossed the bridge

INIT
  !state & !changed

TRANS
  -- we have the lamp. We can cross...
  ((!state & !lamp) -> ((next(state) & next(duration)>=time & next(changed)) | 
  -- ... or not
                          (next(!state) & next(!changed))))
&
  ((state & lamp) -> ((next(!state) & next(duration)>=time & next(changed)) | 
                           (next(state) & next(!changed))))
&
  -- we don't have the lamp... Just seat and wait here!
  ((!state & lamp) -> (next(!state) & next(!changed)))
&
  ((state & !lamp) -> (next(state) & next(!changed)))

MODULE main
-- We define the persons here, 
-- and control the moves of the lamp.

VAR 
  v1: person(5,lamp,duration);
  v2: person(10,lamp,duration);
  v3: person(20,lamp,duration);
  v4: person(25,lamp,duration);
  lamp: boolean;                -- true = left of the bridge, false = right
  duration: 0..25;              -- the duration variable

DEFINE
  bridge:=v1.changed+v2.changed+v3.changed+v4.changed;
  safe:=(v1.state)&(v2.state)&(v3.state)&(v4.state);
  initial:=(!v1.state)&(!v2.state)&(!v3.state)&(!v4.state);

INIT
  !lamp & duration=0

INVAR
  bridge<=2;

TRANS
 ( (v1.state=next(v1.state) & 
    v2.state=next(v2.state) & 
    v3.state=next(v3.state) & 
    v4.state=next(v4.state)  ) <-> (next(lamp)=lamp) )
 &
  next(duration mod 5 = 0)

COMPUTE MIN[initial, safe]

SPEC  EBF 60..60 safe
SPEC  EF<= 59 safe
SPEC  (AG EF<=85 safe) & !(AG EF<=84 safe)