Finish elevator

1 files changed, 183 insertions, 0 deletions

diff --git a/elevator.smv b/elevator.smv
new file mode 100644
index 0000000..5f70472
--- /dev/null
+++ b/elevator.smv
@@ -0,0 +1,183 @@
+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];