1 files changed, 57 insertions, 0 deletions
diff --git a/elevator.tex b/elevator.tex
new file mode 100644
index 0000000..c491fb3
--- /dev/null
+++ b/elevator.tex
@@ -0,0 +1,57 @@
+\documentclass[a4paper]{article}
+
+\usepackage{geometry}
+\usepackage[english]{babel}
+
+\usepackage{enumitem}
+\setenumerate[1]{label=\alph*)}
+\setenumerate[2]{label=\arabic*.}
+
+\usepackage{fancyhdr}
+\renewcommand{\headrulewidth}{0pt}
+\renewcommand{\footrulewidth}{0pt}
+\fancyhead{}
+\fancyfoot[C]{Copyright {\textcopyright} 2016 Camil Staps}
+\pagestyle{fancy}
+
+\usepackage{sv}
+
+\title{Software Verification - Elevator}
+\author{Camil Staps}
+
+\usepackage{amsmath}
+
+\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}
+
+\begin{enumerate}
+  \item We define the following atomic propositions:
+    \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\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}
+\end{enumerate}
+
+\end{document}
+