Finish elevator

4 files changed, 301 insertions, 108 deletions

diff --git a/.gitignore b/.gitignore
index b7e21a8..fd51a7f 100644
--- a/.gitignore
+++ b/.gitignore
@@ -25,3 +25,4 @@
 *.pdf
 *.swp
 *.synctex.gz
+_minted-*/
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];
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]; 
diff --git a/elevator.tex b/elevator.tex
index c491fb3..ae3ee32 100644
--- a/elevator.tex
+++ b/elevator.tex
@@ -11,7 +11,7 @@
 \renewcommand{\headrulewidth}{0pt}
 \renewcommand{\footrulewidth}{0pt}
 \fancyhead{}
-\fancyfoot[C]{Copyright {\textcopyright} 2016 Camil Staps}
+%\fancyfoot[C]{Copyright {\textcopyright} 2016 Camil Staps}
 \pagestyle{fancy}
 
 \usepackage{sv}
@@ -20,38 +20,149 @@
 \author{Camil Staps}
 
 \usepackage{amsmath}
+\usepackage{minted}
+\setminted{fontsize=\small}
+\usepackage[hidelinks]{hyperref}
 
 \def\open#1{\mathit{open}_{#1}}
 \def\at#1{\mathit{at}_{#1}}
 \def\req#1{\mathit{req}_{#1}}
 \def\ind#1{\mathit{ind}_{#1}}
-\def\moving{\mathit{moving}}
 
 \begin{document}
 
 \maketitle
 \thispagestyle{fancy}
 
+\section{Solutions}
+
 \begin{enumerate}
   \item We define the following atomic propositions:
+    \belowdisplayskip=0pt
     \begin{align*}
       \open{i}    &\stackrel{\text{def}}{=} \text{Door at floor $i$ is open.} \\
       \at{i}      &\stackrel{\text{def}}{=} \text{Elevator is at floor $i$.} \\
       \req{i}     &\stackrel{\text{def}}{=} \text{Elevator is requested to go to floor $i$.} \\
       \ind{i}     &\stackrel{\text{def}}{=} \text{The indicator lights of floor $i$ (both at the floor and in the elevator) are on.} \\
     \end{align*}
-
     That gives the following formalisations:
     \begin{enumerate}
       \item $\always\open{i}\then\at{i}$.
-      \item $\req{i}\then\eventually\open{i}$.
-      \item %todo
-      \item $\inevitably\at0$.
+      \item $\always\req{i}\then\eventually\open{i}$.
+      \item $\forall_i[\invariantly\req{i}\then\inevitably\open{i}]$.
+      \item $\always\eventually\at0$.
       \item $\always\req3\then\next(\lnot(\open0\lor\open1\lor\open2)\until\open3)$. The $\next$ operator is here, because it may be that the elevator is requested at floor 3 when the doors elsewhere are open. This is not a violation, however, the doors should be closed as soon as possible.
       \item $\always\ind{i}\then\eventually\open{i}$.
       \item $\always\lnot(\req0\lor\req1\lor\req2\lor\req3)\then\lnot\exists_i[\at{i}\not\equiv\next\at{i}]$.
     \end{enumerate}
+
+    As you can see, I'm using quantifiers here to make claims about all or some floors. In the NuSMV model to be discussed below, these properties are represented by several specifications, one for each $i\in\{0,1,2,3\}$.
+
+  \item The source code is given in \autoref{sec:model}.
+
+    Especially requirement 5, that floor 3 always has priority, is problematic: it conflicts with 2 (because when floor 3 is continuously requested, some other floor may never be handled), 3 and 4 (for similar reasons). However, without the top floor priority, it is straightforward to implement a FIFO queue where floors requested first are handled first. Only property 4 is then not yet satisfied: we would also need to go back to floor 0 every now and then.
+
+    Things get more interesting when one floor has the priority. The model given in \autoref{sec:model} gives priority to floor 3, while assuring that (as long as floor 3 is not requested over and over again) other floors will always be handled: for floor 0, 1 and 2 we maintain a simple FIFO queue (in \mintinline{nusmv}{_prio}).
+    
+    I rewrote properties 2 and 3 to the following, to prove that the properties just claimed indeed hold:
+
+    \begin{enumerate}[start=2]
+      \item $\always (\req{i}\then\eventually\open{i}\lor\always\eventually\open3)$.
+      \item $\forall_i[\invariantly\req{i}\then\inevitably\open{i}\lor\inevitably\open3]$.
+    \end{enumerate}
+
+    Property 4 is also in conflict with property 7, and for energy saving reasons, priority has been given to the latter.
+
+  \item All the properties hold. The properties that should not don't hold (and are commented out at the bottom of the file). The rewritten properties do hold.
+
+    There's something strange though. The LTL properties that should not hold, don't hold (a counterexample is given). The LTL properties that should hold are reported true, however, when increasing the verbosity level (\texttt{-v 1}) it says for all LTL properties:
+
+    \begin{minted}[gobble=6]{text}
+      ********   WARNING   ********
+      Fair states set of the finite state machine is empty.
+      This might make results of model checking not trustable.
+      ******** END WARNING ********
+    \end{minted}
+
+    According to the NuSMV FAQ\footnote{\url{http://nusmv.fbk.eu/faq.html\#010}}, this can mean a deadlock in the system. However, this is not the case, because \texttt{check\_fsm} doesn't mention any problems:
+
+    \begin{minted}[gobble=6]{text}
+      NuSMV > check_fsm 
+      Checking totality and deadlock states.
+      
+      ##########################################################
+      The transition relation is total: No deadlock state exists
+      ##########################################################
+    \end{minted}
+
+    CTL properties work fine (both those that hold and those that don't hold). Even simple LTL properties, like \mintinline{nusmv}{G TRUE} give the above warning. Hence, I'm not sure what to do with this warning. Since all properties that should be false are deemed false, I'm tempted to think this is some bug (or something I don't understand) with NuSMV, and that the properties that yield this warning are still true. But I would like to get some feedback on this.
+
+  \item Enabling reordering of BDD variables with the \texttt{-reorder} flag is a huge performance improvement (it runs almost 10 times as fast):
+
+    \begin{minted}[gobble=6]{text}
+      $ time NuSMV elevator.smv >/dev/null
+      NuSMV elevator.smv  32.84s user 0.02s system 100% cpu 32.835 total
+      $ time NuSMV -reorder elevator.smv >/dev/null
+      NuSMV -reorder elevator.smv  3.91s user 0.02s system 99% cpu 3.928 total
+    \end{minted}
+
+    I had anticipated an improvement, but a factor 10 is impressive.
+
 \end{enumerate}
 
+\clearpage
+\section{Evaluation}
+This was a nice assignment to work on. I liked that there was the freedom to satisfy the requirements you found most interesting. NuSMV is, in my opinion, a much nicer tool than UPPAAL. It is easier to work with and to automate things.
+
+On the other hand, NuSMV seems to be rather minimal. Perhaps I missed it in the manual, but I would like to be able to do something like:
+
+\medskip
+\begin{minipage}{.3\linewidth}
+  \begin{minted}[gobble=4]{nusmv}
+    for i=0 to 3:
+      CTLSPEC AG EF open[i];
+    rof;
+  \end{minted}
+\end{minipage}
+\begin{minipage}{.39\linewidth}
+  \parindent10pt
+  which would be equivalent to:
+\end{minipage}
+\begin{minipage}{.3\linewidth}
+  \begin{minted}[gobble=4]{nusmv}
+    CTLSPEC AG EF open[0];
+    CTLSPEC AG EF open[1];
+    CTLSPEC AG EF open[2];
+    CTLSPEC AG EF open[3];
+  \end{minted}
+\end{minipage}
+\medskip
+
+It is also a pity that \mintinline{nusmv}{next} cannot be used in \texttt{simple\_expression}s -- although I expect that changing this would actually mean changing the way NuSMV works (while the above suggestion is merely syntactic sugar).
+
+I now worked around this problem by introducing a helper variable, \mintinline{nusmv}{_next_at}, which is completely determined using an \mintinline{nusmv}{INVAR} statement, and with \mintinline{nusmv}{next(_at) := _next_at}. I realise this is not the neatest approach. However, since \mintinline{nusmv}{_at} is always entirely determined by the model (i.e., it is `program logic' and cannot be externally influenced like \mintinline{nusmv}{req}), we aren't cheating (peeking into the future) here.
+
+So, perhaps NuSMV could be extended to allow the \mintinline{nusmv}{next} operator in \texttt{simple\_expression}s as long as its argument is entirely determined by the model (for example through \mintinline{nusmv}{INVAR} statements).
+
+\medskip
+Considering my approach: it was quite unfortunate that I was away the whole week before the deadline, and didn't have the time to work on the project beforehand. This is typically an assignment for which it pays of to think about a good solution for several days.
+
+Since I worked alone, I cannot reflect upon the task division in my group. Being away the whole week before the deadline, I didn't want to burden other students with my strange schedule. Surely working together this assignment would have taken less time, and some mistakes that are still here now would not have been there (two sets of eyes are better than one), but that's the way it is.
+
+\medskip
+The assignment did provide additional insight. There were several properties that I had to change later on, because when working on the actual model I realised my formalisation was not correct. For example, the addition of the $\next$ operator in property 5 was such a change.
+
+It was also really helpful to have the model checker to verify my properties. This aided significantly in writing a good model, I believe. The only thing that was sometimes difficult was to understand the counter examples given by NuSMV. The semantics are clear, they are just not very user friendly. Perhaps at this point a graphical interface could pay off, to be able to step through the counter example.
+
+\clearpage
+\appendix
+\section{NuSMV model}
+\label{sec:model}
+This is \texttt{elevator.smv}, the NuSMV model for the elevator described above. Properties that do not hold (at the very bottom) are commented out, for output brevity reasons. Some properties were added for testing the model (the test properties), they can safely be ignored.
+
+In case you're interested: syntax highlighting is done using \texttt{minted}\footnote{\url{https://www.ctan.org/pkg/minted}}, which uses \texttt{pygments}\footnote{\url{http://pygments.org/}}. I have written a NuSMV lexer for pygments which, at the time of writing, has not yet been merged into master\footnote{\url{https://bitbucket.org/birkenfeld/pygments-main/pull-requests/564}} -- however, cloning \texttt{pygments-main} from my fork\footnote{\url{https://bitbucket.org/camilstaps/pygments-main/overview}} would allow you to work with it.
+
+\inputminted[linenos]{nusmv}{elevator.smv}
+
 \end{document}