Start elevator

1 files changed, 102 insertions, 0 deletions

diff --git a/elevator.nu b/elevator.nu
new file mode 100644
index 0000000..2dc6f03
--- /dev/null
+++ b/elevator.nu
@@ -0,0 +1,102 @@
+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];