elevator.tex


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
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}