MODULE main
VAR
  open : array 0..3 of boolean;
  at : array 0..3 of boolean;
  req : array 0..3 of boolean;
  ind : array 0..3 of boolean;
  moving : boolean;

  _at : 0..3;
  _next_at : 0..3;
  --_open : -1..3;

INVAR
  -- Setting next(at) in a variable itself enables us to use it in the moving 
  -- variable below.
  _next_at = case
    req[3] : _at=3 ? 3 : _at + 1;             -- top floor priority
    req[_at] : _at;                           -- stay on requested floor
    req[2] : _at=0 ? 1 : 2;                   -- go to requested floor
    req[1] : _at=3 ? 2 : 1;
    req[0] : _at=0 ? 0 : _at - 1;
    TRUE : 0;
  esac;

ASSIGN
  init(_at)   := 0;
  --init(_open) := -1;
  init(open[0]) := FALSE;
  init(open[1]) := FALSE;
  init(open[2]) := FALSE;
  init(open[3]) := FALSE;

  next(_at) := _next_at;
  
  next(req[0]) := req[0] & !open[0] ? TRUE : {TRUE, FALSE};
  next(req[1]) := req[1] & !open[1] ? TRUE : {TRUE, FALSE};
  next(req[2]) := req[2] & !open[2] ? TRUE : {TRUE, FALSE};
  next(req[3]) := req[3] & !open[3] ? TRUE : {TRUE, FALSE};

  next(open[0]) := req[0] & at[0] & !req[3];
  next(open[1]) := req[1] & at[1] & !req[3];
  next(open[2]) := req[2] & at[2] & !req[3];
  next(open[3]) := req[3] & at[3];

  next(ind[0]) := req[0];
  next(ind[1]) := req[1];
  next(ind[2]) := req[2];
  next(ind[3]) := req[3];
  
-- physical constraint: one place at a time
INVAR at[0] -> !(at[1] | at[2] | at[3]); INVAR at[1] -> !(at[0] | at[2] | at[3]);
INVAR at[2] -> !(at[0] | at[1] | at[3]); INVAR at[3] -> !(at[0] | at[1] | at[2]);

-- link between program logic and APs
INVAR _at = 0 <-> at[0]; INVAR _at = 1 <-> at[1];
INVAR _at = 2 <-> at[2]; INVAR _at = 3 <-> at[3];

--INVAR _open = 0 <-> open[0]; INVAR _open = 1 <-> open[1];
--INVAR _open = 2 <-> open[2]; INVAR _open = 3 <-> open[3];

-- Help variables
INVAR moving = !(_at = _next_at)

-- Property 1: door is never open if the elevator is not at that floor
LTLSPEC G (open[0] -> at[0]);
LTLSPEC G (open[1] -> at[1]);
LTLSPEC G (open[2] -> at[2]);
LTLSPEC G (open[3] -> at[3]);

-- Property 2: requested floor will be served sometime
--LTLSPEC G (req[0] -> F open[0]);
--LTLSPEC G (req[1] -> F open[1]);
--LTLSPEC G (req[2] -> F open[2]);
LTLSPEC G (req[3] -> F open[3]);
-- Same, in CTL
--CTLSPEC AG (req[0] -> AF open[0]);
--CTLSPEC AG (req[1] -> AF open[1]);
--CTLSPEC AG (req[2] -> AF open[2]);
CTLSPEC AG (req[3] -> AF open[3]);

-- Property 4: elevator will invariantly return to floor 0
CTLSPEC AF at[0];

-- Property 5: top floor priority
LTLSPEC G (req[3] -> (!X(open[0] | open[1] | open[2]) U open[3]));

-- Property 6: lights are correct
--LTLSPEC G ind[0] -> F open[0];
--LTLSPEC G ind[1] -> F open[1];
--LTLSPEC G ind[2] -> F open[2];
LTLSPEC G ind[3] -> F open[3];

-- Property 7: no move when no request
LTLSPEC G !(req[0] | req[1] | req[2] | req[3]) -> !moving

-- Test properties
CTLSPEC AG EF moving; -- always eventually exists a state where elevator is moving
LTLSPEC !F G moving; -- elevator isn't moving all the time
CTLSPEC AG EF open[0]; -- it is always possible that any door will open at some point
CTLSPEC AG EF open[1];
CTLSPEC AG EF open[2];
CTLSPEC AG EF open[3];