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

  -- Helper
  moving : boolean;

  -- Program logic
  _at : 0..3;
  _next_at : 0..3;
  _prio : array 0..2 of 0..2;

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

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[_prio[0]] : case                -- go to requested floor & stay
      _at > _prio[0] : _at - 1;
      _at < _prio[0] : _at + 1;
      _at = _prio[0] : _at;
    esac;
    req[_prio[1]] : case
      _at > _prio[1] : _at - 1;
      _at < _prio[1] : _at + 1;
      _at = _prio[1] : _at;
    esac;
    req[_prio[2]] : case
      _at > _prio[2] : _at - 1;
      _at < _prio[2] : _at + 1;
      _at = _prio[2] : _at;
    esac;
    TRUE : _at;                         -- no request; stay
  esac;

-- Help variables
-- Can't use next(_at) here, because this is a simple_expression
INVAR moving = !(_at = _next_at)

ASSIGN
  next(_at) := _next_at;
  
  -- A request holds until the elevator opens on that floor
  -- Any floor can be requested at any moment
  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] & !moving & !req[3] & _prio[0] = 0;
  next(open[1]) := req[1] & at[1] & !moving & !req[3] & _prio[0] = 1;
  next(open[2]) := req[2] & at[2] & !moving & !req[3] & _prio[0] = 2;
  next(open[3]) := req[3] & at[3] & !moving;

  next(ind[0]) := req[0];
  next(ind[1]) := req[1];
  next(ind[2]) := req[2];
  next(ind[3]) := req[3];

  -- Priorities
  next(_prio[0]) := case
    !(open[0] | open[1] | open[2] | open[3]) : case
      req[_prio[0]] : _prio[0];
      req[_prio[1]] : _prio[1];
      req[_prio[2]] : _prio[2];
      TRUE : _prio[0]; 
    esac;
    open[_prio[0]] : _prio[1];
    TRUE : _prio[0];
  esac;
  next(_prio[1]) := case
    open[_prio[0]] | open[_prio[1]] : _prio[2];
    req[_prio[0]] & req[_prio[1]] : _prio[1];
    req[_prio[0]] & req[_prio[2]] : _prio[2];
    req[_prio[1]] & req[_prio[2]] : _prio[2];
    req[_prio[1]] : _prio[2];
    TRUE : _prio[1];
  esac;

-- Every floor has only one priority
INVAR !(_prio[0] = _prio[1] | _prio[0] = _prio[2] | _prio[1] = _prio[2])

-- The last priority is the remaining floor
INVAR !(_prio[0] = 0 | _prio[1] = 0) -> _prio[2] = 0;
INVAR !(_prio[0] = 1 | _prio[1] = 1) -> _prio[2] = 1;
INVAR !(_prio[0] = 2 | _prio[1] = 2) -> _prio[2] = 2;
  
-- Physical constraint: elevator is at only 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];

-- Test properties
-- There is always some possibility for the elevator to move
CTLSPEC AG EF moving;
-- The elevator isn't moving all the time
LTLSPEC !F G moving;
-- It is always possible that the doors at any floor will eventually open
CTLSPEC AG EF open[0];
CTLSPEC AG EF open[1];
CTLSPEC AG EF open[2];
CTLSPEC AG EF open[3];
-- It is always possible that the elevator will be at any floor at some point
CTLSPEC AG EF at[0];
CTLSPEC AG EF at[1];
CTLSPEC AG EF at[2];
CTLSPEC AG EF at[3];
-- One step at a time
LTLSPEC G (_at = _next_at | _at + 1 = _next_at | _at - 1 = _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, unless 3 will be served
-- invariantly
LTLSPEC G (req[0] -> F open[0] | G F open[3]);
LTLSPEC G (req[1] -> F open[1] | G F open[3]);
LTLSPEC G (req[2] -> F open[2] | G F open[3]);
LTLSPEC G (req[3] -> F open[3]);
-- Same, in CTL
CTLSPEC AG (req[0] -> AF open[0] | EF open[3]);
CTLSPEC AG (req[1] -> AF open[1] | EF open[3]);
CTLSPEC AG (req[2] -> AF open[2] | EF open[3]);
CTLSPEC AG (req[3] -> AF open[3]);

-- Property 3: it is always possible to go to any floor, unless floor 3 will be
-- served invariantly
CTLSPEC AG (req[0] -> AF open[0] | EF AF open[3]);
CTLSPEC AG (req[1] -> AF open[1] | EF AF open[3]);
CTLSPEC AG (req[2] -> AF open[2] | EF AF open[3]);
CTLSPEC AG (req[3] -> AF open[3]);

-- 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[3] -> F open[3];
-- Since the top floor has priority, it is also possible that this floor will
-- be served invariantly and the other floors suffer starvation. The next oper-
-- ator is here, because the indicator lights are updated only the next step.
LTLSPEC G (X ind[0] -> F open[0] | G F open[3]);
LTLSPEC G (X ind[1] -> F open[1]) | G F open[3];
LTLSPEC G (X ind[2] -> F open[2]) | G F open[3];

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

-- Properties that do not hold
-- Property 2: requested floor, if not 3, will be served sometime (floor 3 may
-- be served invariantly)
--LTLSPEC G (req[0] -> F open[0]);
--LTLSPEC G (req[1] -> F open[1]);
--LTLSPEC G (req[2] -> F open[2]);

-- Property 3: it is always possible to go to any floor (does not hold for any
-- floor except 3)
--CTLSPEC AF (req[0] -> open[0]);
--CTLSPEC AF (req[1] -> open[1]);
--CTLSPEC AF (req[2] -> open[2]);

-- Property 4: elevator will invariantly return to floor 0 (if floor 0 is never
-- requested but other floors are, elevator will never go to floor 0)
--LTLSPEC G F at[0];