diff options
| -rw-r--r-- | Makefile | 2 | ||||
| -rw-r--r-- | elevator.nu | 102 | ||||
| -rw-r--r-- | elevator.tex | 57 |
3 files changed, 160 insertions, 1 deletions
@@ -1,4 +1,4 @@ -TARGET=$(subst .tex,.pdf,$(wildcard *.tex)) +TARGET=$(subst .tex,.pdf,$(wildcard *.tex)) elevator.pdf all: $(TARGET) 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]; 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} + |