Finish elevator

1 files changed, 0 insertions, 102 deletions

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