\documentclass{report}

\usepackage{vmargin}
\usepackage[color]{circus}

\setpapersize{A4}
%\setmarginsrb{leftmargin}{topmargin}{rightmargin}{bottommargin}{headheight}{headsep}{footheight}{footskip}
%\setmarginsrb{20mm}{10mm}{20mm}{10mm}{12pt}{11mm}{0pt}{11mm}
%\setmarginsrb{25mm}{20mm}{25mm}{20mm}{12pt}{11mm}{0pt}{10mm}
\setmarginsrb{40mm}{20mm}{40mm}{20mm}{12pt}{11mm}{0pt}{10mm}

\newcommand{\HandelC}{\textsf{\slshape Handel-C}}

\newcommand{\action}[1]{\mathsl{#1}}

\newcommand{\cbegin}{\mathbf{begin}}
\newcommand{\ccon}{\mathbf{con}}
\newcommand{\cend}{\mathbf{end}}
\newcommand{\chanevents}[1]{\{\!\mid #1 \mid\!\}}
\newcommand{\channelname}[1]{\mathsl{#1}}
\newcommand{\chan}{\mathbf{channel}}
\newcommand{\compresslist}{\itemsep=0pt \parskip=0pt}
\newcommand{\cprocess}{\mathbf{process}}
\newcommand{\cvar}{\mathbf{var}}
\newcommand{\eventname}[1]{\mathsl{#1}}
\newcommand{\processname}[1]{\mathsl{#1}}

\newcommand{\boolean}{{\mathbb B}}

\newcommand{\event}[1]{\mathsl{#1}}
\renewcommand{\freetype}[1]{\mathsf{#1}}

\newcommand{\freetypecloseValve}{\freetype{closeValve}}
\newcommand{\freetypeclosed}{\freetype{closed}}
\newcommand{\freetypeclosecmd}{\freetype{closecmd}}
\newcommand{\freetypedegraded}{\freetype{degraded}}
\newcommand{\freetypeemergencyStop }{\freetype{emergencyStop}}
\newcommand{\freetypeflow}{\freetype{flow}}
\newcommand{\freetypeinitialisation}{\freetype{initialisation}}
\newcommand{\freetypelevelFailureDetection}{\freetype{levelFailureDetection}}
\newcommand{\freetypelevelRepairedAcknowledgement}%
  {\freetype{levelRepairedAcknowledgement}}
\newcommand{\freetypenoflow}{\freetype{noflow}}
\newcommand{\freetypenormal}{\freetype{normal}}
\newcommand{\freetypeopenValve}{\freetype{openValve}}
\newcommand{\freetypeopen}{\freetype{open}}
\newcommand{\freetypeopencmd}{\freetype{opencmd}}
\newcommand{\freetypepcfailed}{\freetype{pcfailed}}
\newcommand{\freetypepcfail}{\freetype{pcfail}}
\newcommand{\freetypepcflow}{\freetype{pcflow}}
\newcommand{\freetypepclosed}{\freetype{pclosed}}
\newcommand{\freetypepcnoflow}{\freetype{pcnoflow}}
\newcommand{\freetypepfailed}{\freetype{pfailed}}
\newcommand{\freetypepfail}{\freetype{pfail}}
\newcommand{\freetypephysicalUnitsReady}{\freetype{physicalUnitsReady}}
\newcommand{\freetypepopen}{\freetype{popen}}
\newcommand{\freetypeprogramReady}{\freetype{programReady}}
\newcommand{\freetypepwaiting}{\freetype{pwaiting}}
\newcommand{\freetypeqfail}{\freetype{qfail}}
\newcommand{\freetyperescue}{\freetype{rescue}}
\newcommand{\freetypesfailed}{\freetype{sfailed}}
\newcommand{\freetypesokay}{\freetype{sokay}}
\newcommand{\freetypesteamBoilerWaiting}{\freetype{steamBoilerWaiting}}
\newcommand{\freetypesteamFailureDetection}{\freetype{steamFailureDetection}}
\newcommand{\freetypesteamRepairedAcknowledgement}%
  {\freetype{steamRepairedAcknowledgement}}
\newcommand{\freetypestop}{\freetype{stop}}
\newcommand{\freetypetransmissionFailure}{\freetype{transmissionFailure}}
\newcommand{\freetypevclosed}{\freetype{vclosed}}
\newcommand{\freetypevfail}{\freetype{vfail}}
\newcommand{\freetypevopen}{\freetype{vopen}}

\newenvironment{addedstuff}{\begin{flushleft}\textbf{ADDED TO ORIGINAL BEGIN}\begin{quote}\begin{minipage}{.8\textwidth}}{\end{minipage}\end{quote}\textbf{ADDED TO ORIGINAL END}\end{flushleft}}

\newcommand{\lschexpract}{\left(\!\!\left(}
\newcommand{\rschexpract}{\right)\!\!\right)}
\newcommand{\lcircguard}{\left\langle}
\newcommand{\rcircguard}{\right\rangle}
\newcommand{\prefixcolon}{~:~}

\begin{document}

\bibliographystyle{plain}

\title{\Circus\ Example --- Parsable Steam Boiler\\ (unboxed processes)}
\author{Leonardo Freitas}
\date{June 2006}

\maketitle

\begin{abstract}
   \noindent This document is a parsable version of the original report
   back in 2002 by Jim Woodcock. We kept the text as the original, except
   from the text between basic process, as this is a unboxed version (\textit{i.e.},
   processes appear in a single circus environment).
\end{abstract}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\newpage %

\tableofcontents %

\newpage %

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\chapter{Introduction}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

This report has been prepared for the Defence Evaluation and Research
Agency, Malvern, UK, under grant number CU009-0000004344.

The research was carried out by the author at the University of
Oxford, and whilst on visits to the following institutions: the
Federal University of Pernambuco, Trinity College Dublin, the Stevens
Institute of Technology in New Jersey, and the United Nations
University, International Institute for Software Technology in Macau
(UNU/IIST).

The author has discussed the steam boiler over a long period of time
with many people, including: Jean-Raymond Abrial, Dines Bj{\o}rner,
Eerke Boiten, Christie Bolton, Egon B\"{o}rger, Andrew Butterfield,
Ana Cavalcanti, Charlie Crichton, Jim Davies, John Derrick, Lindsay
Groves, Daniel Jackson, He Jifeng, Tony Hoare, Steve King, Andrew
Martin, Alistair \hbox{McEwan}, Colin O'Halloran, Augusto Sampaio,
Anthony Smith, Ib Holm S{\o}rensen, and the Visiting Fellows at
UNU/IIST.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\section{\Circus}

The research in this report has influenced the design of \Circus, a
concurrent refinement calculus \cite{woodcock-cavalcanti-01} that
unifies the Z notation \cite{spivey-88, potter-sinclair-till-91,
  spivey-92, woodcock-davies-96}, CSP \cite{hoare-85, roscoe-98}, and
ZRC \cite{cavalcanti-97, cavalcanti-woodcock-98}, a refinement
calculus for Z.  The semantics of \Circus\ is based on Hoare \& He's
\emph{Unifying Theories of Programming} \cite{hoare-he-98}, in which
the theory of alphabetised relations is used as a common semantic
basis for many diverse paradigms of programming, including imperative
programming, concurrency, and communication, which are fundamental to
\Circus.

An objective of the design of \Circus\ is to provide a sound
development technique based on the refinement calculus \cite
{morgan-94} for parallel programming languages including
\textsf{occam} \cite{inmos-84}, \HandelC\
\cite{embedded-solutions-ltd-99}, and even Java
\cite{arnold-gosling-96, cavalcanti-sampaio-01}.  The effective use of
such a calculus requires tool support, and we use two tools together
in analysing \Circus\ specifications: Z/Eves
\cite{meisels-saaltink-97, saaltink-97} and FDR
\cite{formal-systems-97}.  The Z specifications in this document have
been parsed and type-checked using \fuzz\ \cite{spivey-95} and the FDR
scripts checked using FDR 2.78; a verification using Z/Eves was
incomplete at the date of writing.

In \cite{woodcock-cavalcanti-01}, Z is used as the concrete syntax for
the theory of alphabetised relations, so a \Circus\ specification
actually denotes a Z specification, in spite of containing terms in
the syntax of CSP.  This means that Z tools may be used to analyse
entire \Circus\ specifications, not just those parts written in Z.
This is particularly useful when it is not possible or convenient to
reduce a \Circus\ specification to the size where it may be
model-checked using FDR, and we need to verify a development with a
theorem prover.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\section{The steam boiler problem}

The \emph{steam-boiler} problem has established itself as one of the
standard problems in software engineering, alongside the library, the
lift, and the telephone exchange.  It was first posed by Bauer from
the University of Waterloo \cite{bauer-93}, and subsequently
popularised by Abrial as the subject of a Dagstuhl workshop
\cite{abrial-96-b}.  The problem description and twenty-two solutions
are contained in \cite{abrial-borger-langmaack-96}; Abrial's own
solution is published separately in \cite{abrial-96-a}.

The problem is to program the control system for a steam boiler, such
as might be found in a power station.  The control software is
supposed to exist within a physical environment with the following
elements.
{\slshape
  \begin{itemize}\compresslist
  \item The steam boiler.
  \item A sensor to detect the level of the water in the boiler.
  \item Four pumps supplying the steam boiler with water.
  \item Four pump controllers.
  \item A sensor to measure the quantity of steam being produced.
  \item An operator's desk.
  \item A message transmission system.
  \end{itemize}
}
The steam-boiler's components have various parameters that constrain
their working capacities; these are described in
table~\ref{table:parameters}.
\begin{table}[htbp]
  \bigskip %
  \begin{center}\slshape
    \begin{tabular}{c|l}
      \textbf{\slshape parameter} & \textbf{\slshape meaning}
      \\[1mm] %
      \hline %
      \\[-3mm] %
      \( C \) & the capacity of the boiler
      \\ %
      \( M_1 \) & the minimum water level; if the level remains below
      \( M_1 \)\/ while
      \\ %
      & the steam production is at its maximum, then the steam boiler
      \\ %
      & would be in danger after five seconds
      \\ %
      \( M_2 \) & the maximum water level; if the level remains above \(
      M_2 \)\/ without
      \\ %
      & steam production, then the steam boiler would be in danger
      \\ %
      & after five seconds
      \\ %
      \( N_1 \) & the minimum normal quantity of water, where \( M_1 <
      N_1 \)
      \\ %
      \( N_2 \) & the maximum normal quantity of water, where \( N_2 <
      M_2 \)
      \\ %
      \( W \) & the maximum quantity of steam at the steam-boiler exit
      \\ %
      \( U_1 \) & the maximum gradient of increase of the quantity of
      steam
      \\ %
      \( U_2 \) & the maximum gradient of decrease of the quantity of
      steam
      \\ %
      \( q \) & the measure of the water level
      \\ %
      \( P \) & the capacity of a pump
      \\ %
      \( v \) & the measure of the steam rate
    \end{tabular}
  \end{center}
  \caption{Parameters and their meanings}\label{table:parameters}
\end{table}

After a pump has been switched on, it takes five seconds before water
is pumped into the boiler, because of the need to balance pressures;
however, it can be stopped instantaneously.  A pump controller reports
on whether there is water passing through its pump.

The program communicates with the physical units through messages that
are transmitted over dedicated lines.  Transmission times may be
neglected and all messages may be regarded as arriving simultaneously.
The control program operates in five different modes.
\begin{itemize}\compresslist
\item \emph{Initialisation}.  The program checks the water and steam
  sensors for correct operation; it ensures that the water level is
  between normal operating limits.
\item \emph{Normal}.  This is the standard operating mode, where the
  program tries to maintain the water level; there are no unrepaired
  failures.
\item \emph{Degraded}.  The water sensor has not failed, but some
  other non-vital piece of equipment has; the program continues to
  operate.
\item \emph{Rescue}.  The water sensor has failed; the program
  continues to operate.
\item \emph{Emergency stop}.  The program enters this mode if it has
  been instructed to stop, if the water level is near to one of the
  overall limits, if a vital piece of equipment has failed, or if
  there is some irregularity in the protocol between the program and
  the physical equipment.
\end{itemize}
The program does not terminate and follows a cycle that takes place
every five seconds: \emph{receive messages---analyse
  information---transmit messages}.

\section{The \Circus\ solution}

Our solution to the problem consists of four processes operating in
parallel.
\begin{enumerate}\compresslist
\item The \textbf{\( \mathsl{Timer} \)}\/ makes sure that the
  program's cycle begins every five seconds.
\item The \textbf{\( \mathsl{Analyser} \)}\/ inputs messages from the
  physical units and analyses their content.  Once the analysis is
  complete, it offers an \emph{information service} to the \(
  \mathsl{Controller} \).
\item The \textbf{\( \mathsl{Controller} \)}\/ decides on the actions
  to be taken, based on the information that it receives.  It
  generates outputs for the \( \mathsl{Reporter} \).
\item The \textbf{\( \mathsl{Reporter} \)}\/ offers a \emph{reporting
    service} to the \( \mathsl{Controller} \)\/ by gathering its
  outputs and packaging them together for dispatch to the physical
  units.  It signals the completion of the cycle.
\end{enumerate}

Our solution is guided by a desire to find efficient ways of verifying
our model; in particular, we want to use the FDR model checker.  There
are two obstacles to using a model checker for a system such as this:
the state explosion problem and the presence of loose constants.  FDR
can check an impressive number of states, but the rich state of the
steam boiler exceeds this capacity by many orders of magnitude.

Loose constants complicate model checking, since they must be given
specific values; an argument is then required to extrapolate from
these specific values to arbitrary ones.  The full steam-boiler
system, described at the level of the requirements, depends on several
loosely-specified constants; any reasonable instantiation of these
constants leads to a massive number of states.

Our solution is to separate the \( \mathsl{Controller} \) and its
finite state machine from the \( \mathsl{Analyser}\) and the rich
state that it constructs from the history of input messages.  The \(
\mathsl{Analyser} \)\/ digests the incoming messages and makes this
digest available to the \( \mathsl{Controller} \)\/ as abstract
events; this makes the \( \mathsl{Controller} \)\/ amenable to fully
automatic model checking using FDR, having fewer than one million
states and no loose constants to instantiate.

Extrapolation from the abstract behaviour of the \(
\mathsl{Controller} \) to the concrete realities of the requirements
is provided by the \( \mathsl{Analyser} \).  In fact, it may be viewed
as a retrieve function from the concrete details of the state to an
abstract interpretation of those details, in the sense of data
refinement~\cite{jones-90, woodcock-davies-96}.

The sequence of messages involved in the interaction between these
five processes is described in the message sequence chart in
figure~\ref{fig:msg-seq-chart}.  In this diagram, the \(
\mathsl{ainput} \)\/ and \( \mathsl{aoutput} \)\/ channels connect to
the environment; everything else is internal.  The \( \mathsl{ainfo}
\)\/ and \( \mathsl{a}\-\mathsl{report} \)\/ represent collections of
communications between their respective processes.  To understand the
sequence of messages in a little more detail, we present an
abstraction of the \Circus\ specification as a pure CSP process.
\begin{figure}[htbp]
  \begin{center}
    \begin{picture}(250,320)(0,0)
      % five vertical coloured lines
      \put(50,280){\color{blue}\circle*{5}}
      \put(50,0){\color{blue}\line(0,1){280}}
      \put(50,0){\color{blue}\circle*{5}}
      \put(100,280){\color{red}\circle*{5}}
      \put(100,0){\color{red}\line(0,1){280}}
      \put(100,0){\color{red}\circle*{5}}
      \put(150,280){\color{blue}\circle*{5}}
      \put(150,0){\color{blue}\line(0,1){280}}
      \put(150,0){\color{blue}\circle*{5}}
      \put(200,280){\color{red}\circle*{5}}
      \put(200,0){\color{red}\line(0,1){280}}
      \put(200,0){\color{red}\circle*{5}}
      % add some coloured titles
      \put(50,295){\color{blue}\makebox(0,0)[t]{\( \mathsl{Timer} \)}}
      \put(100,295){\color{red}\makebox(0,.5)[t]{\( \mathsl{Analyser} \)}}
      \put(150,295){\color{blue}\makebox(0,.5)[t]{\( \mathsl{Controller} \)}}
      \put(200,295){\color{red}\makebox(0,0)[t]{\( \mathsl{Reporter} \)}}
      % add messages
      % --------------------------------------------------------------
      % Timer  -- startcycle -->  Sequencer
      \put(75,260){\makebox(0,0)[t]{\footnotesize\color{blue}\(
          \mathsl{startcycle} \)}}
      \put(50,250){\color{blue}\vector(1,0){50}}
      % -- ainput --> Analyser
      \put(50,240){\makebox(0,0)[t]{\footnotesize\( \mathsl{ainput} \)}}
      \put(10,230){\circle*{5}}
      \put(12,230){\vector(1,0){87.5}}
      \put(27.5,220){\makebox(0,0)[t]{\footnotesize\( \mathsl{clocktick} \)}}
      \put(12,210){\vector(1,0){37.5}}
      \put(10,210){\circle*{5}}
      \put(27.5,200){\makebox(0,0)[t]{\footnotesize\( \mathsl{clocktick} \)}}
      \put(12,190){\vector(1,0){37.5}}
      \put(10,190){\circle*{5}}
      \put(27.5,180){\makebox(0,0)[t]{\footnotesize\( \mathsl{clocktick} \)}}
      \put(12,170){\vector(1,0){37.5}}
      \put(10,170){\circle*{5}}
      \put(27.5,160){\makebox(0,0)[t]{\footnotesize\( \mathsl{clocktick} \)}}
      \put(12,150){\vector(1,0){37.5}}
      \put(10,150){\circle*{5}}
      \put(27.5,140){\makebox(0,0)[t]{\footnotesize\( \mathsl{clocktick} \)}}
      \put(12,130){\vector(1,0){37.5}}
      \put(10,130){\circle*{5}}
      % --------------------------------------------------------------
      % Analyser -- startexec --> Controller
      \put(125,220){\makebox(0,0)[t]{\footnotesize\color{red}\(
          \mathsl{startexec} \)}}
      \put(100,210){\color{red}\vector(1,0){50}}
      % Controller  -- startreport -->  Reporter
      \put(175,200){\makebox(0,0)[t]{\footnotesize\color{blue}\(
          \mathsl{startreport} \)}}
      \put(150,190){\color{blue}\vector(1,0){50}}
      % Analyser == ainfo ==> Controller
      \put(125,160){\makebox(0,0)[t]{\footnotesize\color{red}\(
          \mathsl{ainfo} \)}}
      \put(100,150){\color{red}\vector(1,0){50}}
      % Controller  -- areport -->  Reporter
      \put(175,140){\makebox(0,0)[t]{\footnotesize\color{blue}\(
          \mathsl{areport} \)}}
      \put(150,130){\color{blue}\vector(1,0){50}}
      % --------------------------------------------------------------
      % Controller  -- reportmode -->  Reporter
      \put(175,120){\makebox(0,0)[t]{\footnotesize\color{blue}\(
          \mathsl{reportmode} \)}}
      \put(150,110){\color{blue}\vector(1,0){50}}
      % Controller  -- endreport -->  Reporter
      \put(175,100){\makebox(0,0)[t]{\footnotesize\color{blue}\(
          \mathsl{endreport} \)}}
      \put(150,90){\color{blue}\vector(1,0){50}}
      % --------------------------------------------------------------
      % Analyser -- afailuresrepairs --> Reporter
      \put(150,80){\makebox(0,0)[t]{\footnotesize\color{red}\(
          \mathsl{afailuresrepairs} \)}}
      \put(100,70){\color{red}\vector(1,0){100}}
      % Reporter  -- aoutput -->
      \put(219.75,50){\makebox(0,0)[t]{\footnotesize\( \mathsl{aoutput} \)}}
      \put(239.95,40){\circle*{5}}
      \put(200,40){\vector(1,0){38.5}}
      % Analyser <-- apumps -- Controller
      \put(150,30){\makebox(0,0)[t]{\footnotesize\color{red}\(
          \mathsl{apumps} \)}}
      \put(200,20){\color{red}\vector(-1,0){100}}
      % --------------------------------------------------------------
    \end{picture}
    \caption{Message sequence chart}
    \label{fig:msg-seq-chart}
  \end{center}
\end{figure}

Both the \( \mathsl{Controller} \)\/ and the \( \mathsl{Reporter} \)\/
keep track of the current mode, which is selected from the following
data-type.
\[
  \mathbf{datatype}\ Mode = \mathsf{initialisation} \mid %
  \mathsf{normal} \mid \mathsf{degraded} \mid \mathsf{rescue} \mid
  \mathsf{emergencyStop}
  \also %
  NonEmergencyModes = \{ \mathsf{initialisation}, \mathsf{normal},
  \mathsf{degraded}, \mathsf{rescue} \}
\]
The mode is stored in a simple variable process, which starts off in
\( \mathsf{initialisation} \)\/ mode.
\[
\mathbf{channel}\ \mathsl{getmode}, \mathsl{putmode}: Mode
  \also %
  ModeStateInterface = \chanevents{\mathsl{getmode}, \mathsl{putmode}}
  \also %
  \mathsl{ModeState} =
  \\ %
  \t1
  \begin{block}
    \mathbf{let}
    \\ %
    \t1
    \begin{block}
      \mathsl{MS}(m) =
      \begin{block}
        \mathsl{putmode}\,?n \then MS(n)
        \\ %
        \extchoice
        \\ %
        \mathsl{getmode}\,!m \then \mathsl{MS}(m)
      \end{block}
    \end{block}
    \\ %
    \mathbf{within}
    \\ %
    \t1 \mathsl{MS}(\mathsf{initialisation})
  \end{block}
  \also %
  \mathsl{EnterMode}(m) = \mathsl{reportmode}\,!m \then
  \mathsl{putmode}\,!m \then \mathsl{SKIP}
\]

We must define all the channels from the message sequence chart in
figure~\ref{fig:msg-seq-chart}.  In our abstract view, channels that
carry communications have been reduced to mere synchronisations, with
the exception of the \( \mathsl{aoutput} \)\/ and \(
\mathsl{reportmode} \)\/ channels, which merely communicate the
current mode.
\[
  \mathbf{channel}\ %
  \begin{block}
    \mathsl{ainfo}, \mathsl{areport}, \mathsl{clocktick},
    \mathsl{endcycle}, \mathsl{endreport}, \mathsl{afailuresrepairs},
    \mathsl{ainput},
    \\ %
    \mathsl{apumps}, \mathsl{startcycle}, \mathsl{startexec},
    \mathsl{startreport}
  \end{block}
  \also %
  \mathbf{channel}\  \mathsl{aoutput}, \mathsl{reportmode} : Mode
\]
We describe the internal interfaces between the processes being
composed from left to right:~\( TAnalyserInterface \)\/ is the
interface between the \( \mathsl{Timer} \)\/ and the \(
\mathsl{Analyser1} \); \( TA\-Controller\-Interface1 \)\/ is the
interface between the \( \mathsl{Timer1} \)-\( \mathsl{Analyser1}\)\/
subsystem and the \( \mathsl{Controller1} \); and \(
TACReporterInterface1 \)\/ is the interface between the \(
\mathsl{Timer} \)-\( \mathsl{Analyser1}\)-\(\mathsl{Controller1} \)\/
subsystem and the \( \mathsl{Reporter1} \).  The `-1' suffix denotes a
component that is refined later in the report.
\[
  TAnalyserInterface = \{ \mathsl{startcycle} \}
  \also %
  TAControllerInterface1 = \{ \mathsl{ainfo}, \mathsl{startexec} \}
  \also %
  TACReporterInterface1 =
  \also %
  \t1 \chanevents{
    \begin{block}
      \mathsl{apumps}, \mathsl{areport}, \mathsl{endreport},
      \mathsl{afailuresrepairs}, \mathsl{reportmode},
      \mathsl{startreport}}
  \end{block}
\]
The \( \mathsl{Timer} \)\/ signals the start of the cycle and repeats
this after every fifth clock tick.
\[
  cycletime = 5 %
  \also %
  cyclelimit = cycletime - 1
  \also %
  \mathsl{TCycle}(time) =
  \\ %
  \t1
  \begin{block}
    ( \If ( time + 1 ) \mod cycletime = 0 \Then startcycle \then
    \mathsl{SKIP} \Else \mathsl{SKIP});
    \\ %
    \mathsl{clocktick} \then \mathsl{TCycle}(( time + 1 ) \mod
    cycletime)
  \end{block}
  \also %
  \mathsl{Timer} = \mathsl{TCycle}(cyclelimit)
\]
The \( \mathsl{Analyser} \)\/ cycles through its sequence of events,
offering as many \( \mathsl{ainfo} \)\/ events as required.  The
information service is terminated by the transmission of data about
outstanding failures and repair acknowledgements.  This is followed by
the receipt of information about the instructions sent to pumps, which
is needed by the \( \mathsl{Analyser} \) in order to maintain its
model of their state.
\[
  \mathsl{Analyser1} = \mathsl{startcycle} \then \mathsl{ainput} \then %
  \mathsl{startexec} \then \mathsl{InfoService1}
  \also %
  \mathsl{InfoService1} =
  \\ %
  \t1
  \begin{block}
    \mathsl{ainfo} \then \mathsl{InfoService1}
    \\ %
    \extchoice
    \\ %
    \mathsl{afailuresrepairs} \then \mathsl{apumps}
    \then \mathsl{Analyser1}
  \end{block}
\]
We add the \( \mathsl{Analyser} \)\/ to the \( \mathsl{Timer} \),
synchronising on its hidden interface.
\[
  \mathsl{TAnalyser1} = %
  \\ %
  \t1 ( \mathsl{Timer} \parallel [ TAnalyserInterface ]
  \mathsl{Analyser1} ) \hide TAnalyserInterface
\]
The assembly is free from deadlock and livelock.
\[
  \mathbf{assert}\ \mathsl{TAnalyser1} :[ \hbox{ deadlock free } [FD] ]
  \also %
  \mathbf{assert}\ \mathsl{TAnalyser1} :[ \hbox{ livelock free } [FD] ]
\]
The \( \mathsl{Controller} \)\textsl{'s}\/ behaviour is initiated by a
\( \mathsl{startexec} \)\/ event, which it passes on to the \(
\mathsl{Reporter} \)\/ as a \( \mathsl{startreport} \)\/ event.  The
\( \mathsl{Controller} \)\textsl{'s}\/ task is to generate
instructions to control the steam boiler, based on the information
made available to it by the \( \mathsl{Analyser} \).

One possibility is that the \( \mathsl{Analyser} \)\/ instructs the \(
\mathsl{Controller} \)\/ to perform an \( \mathsf{emergencyStop} \).
If this does not happen, then the \( \mathsl{Controller} \)\/ receives
a number of \( \mathsl{ainfo} \)\/ signals from the \(
\mathsl{Analyser} \)\/ and takes action on them, depending on the
current mode.
\[
  \mathsl{Controller1} =
  \\ %
  \t1
  \begin{block}
    \mathsl{startexec} \then
    \\ %
    \t1
    \begin{block}
      \mathsl{startreport} \then
      \\ %
      \t1
      \begin{block}
        \mathsl{NewModeAnalysis1};
        \\ %
        \begin{block}
          \mathsl{getmode}\,?m \then
          \\ %
          \t1
          \begin{block}
            (\
            \begin{block}
              \If m \neq \mathsf{emergencyStop} \Then
              \\ %
              \t1 \Intchoice i: \{ 0 \upto limit \} \spot
              \mathsl{PutReports}(i)
              \\ %
              \Else \mathsl{SKIP}\ );
            \end{block}
            \\ %
            \mathsl{endreport} \then \mathsl{Controller1}
          \end{block}
        \end{block}
      \end{block}
    \end{block}
  \end{block}
\]
The process \( \mathsl{NewModeAnalysis1} \)\/ decides on the next mode
to enter, given the current mode and the information made available to
it.  Once \( \mathsl{NewModeAnalysis1} \)\/ has completed its work,
the \( \mathsl{Controller} \)\/ generates some \( \mathsl{areports}
\), and passes information back to the \( \mathsl{Analyser} \)\/ on
the required state of the steam-boiler's pumps.
\[
  \mathsl{NewModeAnalysis1} =
  \\ %
  \t1
  \begin{block}
    \mathsl{ainfo} \then \mathsl{EnterMode}(emergencyStop)
    \\ %
    \intchoice
    \\ %
    (\
    \begin{block}
      ( \Intchoice i: \{ 0 \upto limit \} @
      \mathsl{GetInfomation}(i) );
      \\ %
      \mathsl{getmode}\,?mode \then
      \\ %
      \t1
      \begin{block}
        \If mode = \mathsf{initialisation} \Then
        \mathsl{InitModeAnalysis1}
        \\ %
        \Else \If mode = \mathsf{normal} \Then
        \mathsl{NormalModeAnalysis1}
        \\ %
        \Else \If mode = \mathsf{degraded} \Then
        \mathsl{DegradedModeAnalysis1}
        \\ %
        \Else \If mode = \mathsf{rescue} \Then
        \mathsl{RescueModeAnalysis1}
        \\ %
        \Else \mathsl{SKIP}
      \end{block}
      \\ %
      )
    \end{block}
  \end{block}
\]
In each nonemergency mode, it is possible to transit to other modes.
\[
  \mathsl{InitModeAnalysis1} = %
  \\ %
  \t1 \mathsl{SKIP} \intchoice \mathsl{EnterMode}(\mathsf{normal})
  \intchoice \mathsl{EnterMode}(\mathsf{degraded}) \intchoice
  \mathsl{EnterMode}(\mathsf{emergencyStop})
  \also %
  \mathsl{NormalModeAnalysis1} = \mathsl{SKIP} \intchoice
  \mathsl{EnterMode}(\mathsf{rescue}) \intchoice
  \mathsl{EnterMode}(\mathsf{degraded})
  \also %
  \mathsl{DegradedModeAnalysis1} = \mathsl{SKIP} \intchoice
  \mathsl{EnterMode}(\mathsf{normal}) \intchoice
  \mathsl{EnterMode}(\mathsf{rescue})
  \also %
  \mathsl{RescueModeAnalysis1} = \mathsl{SKIP} \intchoice
  \mathsl{EnterMode}(\mathsf{normal}) \intchoice
  \mathsl{EnterMode}(\mathsf{degraded})
\]
Since the \( \mathsl{Controller} \)\/ is responsible for demanding
information and for generating reports, it is here that we place
bounds on the number of exchanges that are possible.  If we fail to do
this, then hiding these exchanges will lead to divergence.
\[
  limit = 8
  \also %
  \mathsl{Get}(\mathsl{event},n) =\ \If n > 0 \Then \mathsl{event}
  \then \mathsl{Get}(\mathsl{event},n-1) \Else \mathsl{SKIP}
  \also %
  \mathsl{GetInformation}(n) = \mathsl{Get}(\mathsl{ainfo},n)
  \also %
  \mathsl{PutReports}(n) = \mathsl{Get}(\mathsl{areport},n)
\]
We add a simple mode variable to the \( \mathsl{Controller} \)\/ and
then add the result to the \( \mathsl{TAnalyser} \), hiding the
internal interfaces.
\[
  \mathsl{TAController1} =
  \\ %
  \t1
  \begin{block}
    (\
    \begin{block}
      \mathsl{TAnalyser1}
      \\ %
      \parallel [ TAControllerInterface1 ]
      \\ %
      (\
      \begin{block}
        \mathsl{Controller1}
        \\ %
        \parallel [ ModeStateInterface ]
        \\ %
        \mathsl{ModeState}
      \end{block}
      \\ %
      ) \hide ModeStateInterface
    \end{block}
    \\ %
    ) \hide TAControllerInterface1
  \end{block}
\]
The composition is free from livelock.
\[
  \mathbf{assert}\ \mathsl{TAController1} %
  : [ \hbox{ livelock free } [FD] ]
\]
Notice that the composition isn't deadlock free, since the \(
\mathsl{Analyser} \)\/ can perform the trace
\[
  \langle~ \mathsl{startcycle}, \mathsl{ainput}, \mathsl{startexec}, %
  \mathsl{afailuresrepairs} ~\rangle
\]
whilst at the same time, the \( \mathsl{Controller} \)\/ can perform
the trace
\[
  \langle~ \mathsl{startexec}, \mathsl{startreport} ~\rangle %
\]
This corresponds to the \( \mathsl{Analyser} \) having completed a
cycle of behaviour in which its information service was not required,
but the \( \mathsl{Controller} \) paradoxically being in a state where
it actually requires the service.  This paradox is resolved by the
interaction between the \( \mathsl{Controller} \) and the \(
\mathsl{Reporter} \), which requires that the \(
\mathsl{afailuresrepairs} \) event occurs only after the \(
\mathsl{Controller} \) has completed its requirement for the
information service.

The \( \mathsl{Reporter} \)\/ starts its cycle with a \(
\mathsl{startreport} \)\/ event.
\[
  \mathsl{Reporter1} = \mathsl{startreport} \then \mathsl{ReportService1} %
\]
Following this, it repeatedly gathers \( \mathsl{areport} \)\/ events,
paying particular attention to the mode that the \(
\mathsl{Controller} \)\/ is in, until it receives the signal to end
the report phase, whereupon it does some tidying up.  An \(
\mathsf{emergencyStop} \)\/ mode is serious enough to terminate the
cycle.
\[
  \mathsl{ReportService1} = %
  \\ %
  \t1
  \begin{block}
    \Extchoice m: NonEmergencyModes \spot \mathsl{reportmode}.m \then
    \mathsl{putmode}\,!m \then \mathsl{ReportService1}
    \\ %
    \extchoice
    \\ %
    \mathsl{areport} \then \mathsl{ReportService1}
    \\ %
    \extchoice
    \\ %
    \mathsl{reportmode}.emergencyStop \then
    \mathsl{putmode}\,!emergencyStop \then \mathsl{TidyUp1}
    \\ %
    \extchoice
    \\ %
    \mathsl{TidyUp1}
  \end{block}
\]
Tidying up involves fetching some information from the \(
\mathsl{Analyser} \)\/ about recently failed devices and
acknowledgements of information about repairs, dispatching the output
to the physical units, and informing the \( \mathsl{Analyser} \) about
the commands sent to the pumps.
\[
  \mathsl{TidyUp1} = %
  \\ %
  \t1
  \begin{block}
    \mathsl{endreport} \then
    \\ %
    \t1
    \begin{block}
      \mathsl{afailuresrepairs} \then
      \\ %
      \t1
      \begin{block}
        \mathsl{getmode}\,?m \then
        \\ %
        \t1
        \begin{block}
          \mathsl{aoutput}\,!m \then
          \\ %
          \t1
          \begin{block}
            \mathsl{apumps} \then
            \\ %
            \t1 \mathsl{Reporter1}
          \end{block}
        \end{block}
      \end{block}
    \end{block}
  \end{block}
\]
We add the \( \mathsl{Reporter} \)\/ to the rest of the components,
hiding the internal interface.
\[
  \mathsl{TACReporter1} =
  \\ %
  \t1
  \begin{block}
    (\
    \begin{block}
      \mathsl{TAController1}
      \\ %
      \parallel [ TACReporterInterface1 ]
      \\ %
      (\
      \begin{block}
        (\
        \begin{block}
          \mathsl{Reporter1}
          \\ %
          \parallel [ ModeStateInterface ]
          \\ %
          \mathsl{ModeState}
        \end{block}
        \\ %
        ) \hide ModeStateInterface
      \end{block}
      \\ %
      )
    \end{block}
    \\ %
    ) \hide TACReporterInterface1
  \end{block}
\]
The entire composition is free from deadlock and from livelock.
\[
  \mathbf{assert}\ \mathsl{TACReporter1} :[ \hbox{ deadlock free } [FD] ]
  \also %
  \mathbf{assert}\ \mathsl{TACReporter1} :[ \hbox{ livelock free } [FD] ]
\]
These communicating processes form our abstract view of the
steam boiler.
\[
  \mathsl{SteamBoiler1} = \mathsl{TACReporter1} %
\]

FDR code for the abstract steam boiler is contained in
appendix~\ref{appendix:FDR-code}.  All assertions have been
successfully checked.  The next four chapters contain the \Circus\
specification of each process.  Collectively, they refine the abstract
specification given here.  Appendix~\ref{appendix:FDR-code} contains
two pure CSP descriptions: the one described in this chapter, and
another that is derived from the \Circus\ specification by abstracting
from most of the state details.  The refinement has been checked by
FDR.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\chapter{The $\mathsl{Timer}$}

\begin{addedstuff}
For section management and inclusion of the \Circus\ language keywords
for the \LaTeX\ parser, we can include a named section importing the
appropriate toolkit. Alternatively, without any section name given (Z
standard anonymous sections), the \Circus\ toolkit is automatically loaded.
%
\begin{zsection}
  \SECTION\ unboxed\_steam\_boiler \parents\ circus\_toolkit
\end{zsection}
\end{addedstuff}

The \( \mathsl{Timer} \)\/ process is responsible for signalling to
the other processes the start of the program's cycle, and for ensuring
that the cycle is repeated every five seconds.  It keeps track of time
by counting the number of \( \event{clocktick} \)\/ events that it has
received from the environment.  The \( \mathsl{TimedSequencer} \)\/
uses two channels:
\begin{circus}
    \circchannel\ clocktick, startcycle
\end{circus}

It declares a small environment containing a variable that maintains
the current time, modulo the cycle time.

\begin{addedstuff}
   The original $Timer$ process used a complementary/total $if-then-else$ statement,
   where the last guard is not given and assumed to be the negation of all other guards.
   In the current version of \Circus\ this is not allowed, and guards must appear on every guarded command
   on an alternative command. Thus, we have introduced the negation of the first guard in the alternative below.

   Another interpretation could be that this is a Z $if-then-else$ statement. If that is the
   case, the first action would not parse as $startcycle \then Skip$ is not an expressions,
   whereas the second would parse but would be type incorrect, since $Skip$ is not an
   expression but an action.
\end{addedstuff}

%See original steam boiler for how the encoding of circus.sty
\begin{circus}
   \circprocess\ Timer ~\circdef~ \circbegin \\
     \t1 cycletime == 5 \\ %
     \t1 cyclelimit == cycletime - 1 \\ %
     \t1 Time == 0 \upto cyclelimit \\
     \t1 \circstate\ TimeState == [~ time: Time ~] \\ %
     \t1 TimeOp == [~ \Delta TimeState | time' \geq time ~] \\
     \t1 TCycle \circdef (~time := time + 1 \mod cycletime ~) \circseq \\ %
            \t3 (\circif\       time = 0 \circthen startcycle \then Skip\ \circelse\ time \neq 0 \circthen Skip\ \circfi) \circseq \\ %
            \t3 clocktick \then TCycle
            \\
      \t1 @ time := cyclelimit \circseq TCycle \\
   \circend
\end{circus}
The action \( \processname{TCycle}\, \)\/ increments the \( time \)\/
variable; if its new value is zero, then it is time to start the next
cycle; it waits for the next \( \mathsl{clocktick}\, \), before
repeating. The \( \processname{Timer}\, \)\/ initialises the \( time \)\/
variable so that the cycle can start, and then behaves like \(
\processname{TCycle}\, \).

FDR code for the \( \mathsl{Timer} \)\/ is contained in
appendix~\ref{appendix:FDR-code}.  The process is so simple that there
are no assertions to be checked.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\chapter{The $\mathsl{Analyser}$}

The \( \mathsl{Analyser} \, \)\/ provides an \emph{information
  service} for its two clients: the \( \mathsl{Controller} \, \)\/ and
the \( \mathsl{Reporter} \, \).

The \( \mathsl{Analyser} \, \)\/ acts for its \( \mathsl{Controller}
\, \)\/ client by accepting messages from the units, analysing their
information content to extract the state of the units and their
possible failures, and then enabling certain events as abstractions of
this state.  This is done in a simple way by associating each abstract
event with a state-based firing condition.

For its \( \mathsl{Reporter} \, \)\/ client, it provides details of
outstanding failures and acknowledgements for repairs carried out on
failed equipment.  These details are an essential part of the
program's output to the operator.

The \( \mathsl{Analyser} \, \)\/ provides its information service by
maintaining a model of the behaviour of the various items of equipment
in the system.  We describe each of these models, the handling of
failures and repairs, and the structure of input messages and their
analysis.

\section{Steam boiler parameters}

The requirements describe several constants that are loose parameters
of the steam-boiler's operation: \( C \)\/ is the capacity of the
boiler; \( P \)\/ is the capacity of a pump; \( U_1 \)\/ is the
maximum gradient of increase; \( U_2 \)\/ is the maximum gradient of
decrease; and \( W \)\/ is the maximum output rate for the boiler.

\begin{addedstuff}
The Z standard (section $7.3$) requires that a list of variable declarations with strokes
to contain a hard space just before the comma. Otherwise, the grammar is
ambiguous. This change is done everywhere this situation happens.
For instance, the \LaTeX\ code for the next list of variables below
changes from
%
\begin{centering}
    \begin{verbatim}
        begin{axdef}
            C, P, U_1, U_2, W: \nat
        end{axdef}
    \end{verbatim}
\end{centering}
%
to
%
\begin{centering}
    \begin{verbatim}
        begin{axdef}
            C, P, U_1~, U_2~, W: \nat
        end{axdef}
    \end{verbatim}
\end{centering}
%
Note that we have removed the leading backslash on the verbatim environment
in order to avoid this explanatory text to be caught by the parser by mistake.
\end{addedstuff}
%
\begin{axdef}
  C, P, U_1~, U_2~, W: \nat
\end{axdef}
The critical and working limits of the steam boiler are defined and
ordered appropriately.
\begin{axdef}
  M_1~, N_1~, N_2~, M_2: \nat
\where %
  M_1 \leq N_1 \leq N_2 \leq M_2
\end{axdef}
Capacities are given in litres and time intervals in seconds.

\section{Sensors}

The abstract models of the water-level sensor, the steam-rate sensor,
and the pump are all rather similar; we call this simple model a
\emph{unit}.  The record of the state of a unit is a generic
specification maintaining three quantities: lower and upper-bounds on
the unit's actual measure (\( a_1 \) and \( a_2 \)) and a record of
its operational state (\( st \)) drawn from the generic parameter (\(
X \)).

\begin{addedstuff}
In the free-types defined, \LaTeX\ commands are used. In the Z Standard,
to allow appropriate typesetting of the expected text in Unicode, we need
to provide a \LaTeX\ markup directive, which represents what the fixity
and string value of the \LaTeX\ command will be in Unicode.
%
\begin{verbatim}
   word \freetypesokay sokay
   word \freetypesfailed sfailed
\end{verbatim}
%
These directives must be encoded with a double percent sign followed by
a capital Z. Directives below are needed in order to provide a correct
typesetting of the corresponding \LaTeX\ markup function.
Otherwise, if the directive is not given, the name declared will be $freetypesokay$, rather than $sokay$. This follows
the Z standard on markup directives (Appendix A).
%%Zword \freetypesokay sokay
%%Zword \freetypesfailed sfailed

This also applies for ``beautification'' \LaTeX\ commands, such as
the use of italics or slanted font faces for event or variable names.

Moreover, according to the Z Standard, the hard spaces are needed for the names
with strokes when those appear near a $COMMA$ or a $SLASH$ token. Also,
to make the inclusion of $QSensor$ adequately, we need the hard space as well.
Otherwise, it would be the same as including a new name $QSensor'$, rather than
the dashed version of $QSensor$.
\end{addedstuff}

The abstract models of the water-level sensor, the steam-rate sensor,
and the pump are all rather similar; we call this simple model a
\emph{unit}.  The record of the state of a unit is a generic
specification maintaining three quantities: lower and upper-bounds on
the unit's actual measure (\( a_1 \) and \( a_2 \)) and a record of
its operational state (\( st \)) drawn from the generic parameter (\(
X \)).
\begin{zed}
  Unit[X] == [~ a_1~, a_2: \nat; st: X | a_1 \leq a_2 ~]
\end{zed}
The generic definition is instantiated to specify each kind of unit.
First, a sensor may be judged to be working or to have failed.
\begin{zed}
  SState ::= \freetypesokay | \freetypesfailed
\end{zed}
This free type is used as an actual parameter when we instantiate the
\( Unit \)\/ as a sensor.  The water quantity sensor maintains lower
and upper-bounds on the water level, and a record of its state.
\begin{zed}
  QSensor == Unit[SState][qa_1~/a_1~, qa_2~/a_2~, qst/st]
\end{zed}
Initially, the water-level sensor's lower and upper-bounds are set to
the extreme values and it is judged to be working.
\begin{zed}
  InitQSensor == [~ QSensor~' | qa_1' = 0 \land qa_2' = C \land qst' = \freetypesokay ~]
\end{zed}
The steam-rate volume sensor is similar.
\begin{zed}
  VSensor == Unit[SState][va_1~/a_1~, va_2~/a_2~, vst/st]
  \also %
  InitVSensor == [~ VSensor~' | va_1' = 0 \land va_2' = 0 \land vst' = \freetypesokay ~]
\end{zed}
The initial approximation assumes that there is no flow.

\section{Pumps}

A pump's state is not modelled as merely open or closed, since it
takes five seconds before water starts to pass through it; this
intermediate state is \( \freetypepwaiting \).

\begin{addedstuff}
Added \LaTeX\ markup directives for the next free type:
%%Zword \freetypepopen popen
%%Zword \freetypepwaiting pwaiting
%%Zword \freetypepclosed pclosed
%%Zword \freetypepfailed pfailed
\end{addedstuff}

\begin{zed}
  PState ::= \freetypepopen | \freetypepwaiting | \freetypepclosed | \freetypepfailed
\end{zed}
As before, the system maintains lower and upper-bounds for each pump
and a record of its current state.
\begin{zed}
  Pump0 == Unit[PState][pa_1~/a_1~, pa_2~/a_2~, pst/st]
\end{zed}
This is not the full story about the model for a pump: there are
various invariants that must also hold.

The requirements tell us that the lower-bound for the \( i \)-th pump
is zero if one of the following holds \true: the pump is closed; the
pump has failed; or the pump's controller has failed.  If none of
these holds, then the lower-bound is assumed to be \( P \).
Similarly, the upper-bound for the \( i \)-th pump is \( P \)\/ if one
of the following holds \true: the pump is open; the pump has failed; or
the pump's controller has failed.  If none of these holds, then the
upper-bound is assumed to be zero.

We capture these invariants one at a time.  First, if the pump is
open, then it is assumed to have maximal flow.
\begin{zed}
  PumpOpen == [~ Pump0 | pst = \freetypepopen \implies pa_1 = P \land pa_2 = P ~]
\end{zed}
If the pump is waiting for the pressure to balance after opening, then
there is no flow; if the pump is closed, then there is no flow.
\begin{zed}
  PumpWaitingOrClosed ==
  \\ %
  \t1 [~ Pump0 | pst = \freetypepwaiting \lor pst = \freetypepclosed \implies pa_1 = 0 \land pa_2 = 0 ~]
\end{zed}
A pump must satisfy these invariants.
\begin{zed}
  Pump == PumpOpen \land PumpWaitingOrClosed
\end{zed}
Initially, a pump is closed.
\begin{zed}
  InitPump == [~ PumpWaitingOrClosed~' | pst' = \freetypepclosed ~]
\end{zed}
The requirements give no direct guidance about the initial states of
the system's equipment.  For the initial state of a sensor, it seems
uncontroversial to assume that it is working and that it might take
any value within its range.  If this is incorrect, then the analyser
will detect that the sensor isn't working as soon as it sends a
reading that seems inappropriate.  The system is designed to cope with
this fault by deducing whether the sensor is working or not.

The initial state of a pump is rather different, since there is no
clear `don't care' value, as there is for a sensor.  We initialise the
pump to closed; if instead the pump is initially open, then the
program will deduce that it has failed.  We need to ask the customer
about the adequacy of the decision taken here.

A pump controller may detect the flow of water in its pump, providing
that it has not failed.

\begin{addedstuff}
Added \LaTeX\ markup directives for the next free type:
%%Zword \freetypepcflow pcflow
%%Zword \freetypepcnoflow pcnoflow
%%Zword \freetypepcfailed pcfailed
\end{addedstuff}
\begin{zed}
  PCState ::= \freetypepcflow | \freetypepcnoflow | \freetypepcfailed
  \also %
  PumpCtr0 == [~ Pump; pcst: PCState ~]
\end{zed}
Again, a number of invariants must hold.  First, if the pump is open,
then if the controller is okay, then it should be detecting flow.
Formally, one of the following two conditions must hold.
\begin{zed}
  POpenPCFlowOrFailed ==
  \\ %
  \t1 [~ PumpCtr0 | pst = \freetypepopen \implies pcst =
  \freetypepcflow \lor pcst = \freetypepcfailed ~]
\end{zed}
If the pump is waiting for the pressure to balance, then if the
controller is okay, then it should not be detecting flow.  So, one of
the following two conditions must hold.
\begin{zed}
  PWaitingPCNoFlowOrFailed ==
  \\ %
  \t1 [~ PumpCtr0 | pst = \freetypepwaiting \implies pcst =
  \freetypepcnoflow \lor pcst = \freetypepcfailed~]
\end{zed}
If the pump is closed, then if the controller is okay, then it should
not be detecting flow.  Again, one of the following two conditions
must hold.
\begin{zed}
  PClosedPCNoFlowOrFailed ==
  \\ %
  \t1 [~ PumpCtr0 | pst = \freetypepclosed \implies pcst =
  \freetypepcnoflow \lor pcst = \freetypepcfailed~]
\end{zed}
If the pump has failed, but its controller is okay and detects flow,
then we can assume that the pump is flowing at capacity.
\begin{zed}
  PFailedPCFlow ==
  \\ %
  \t1 [~ PumpCtr0 | pst = \freetypepfailed \land pcst
  = \freetypepcflow \implies pa_1 = P \land pa_2 = P ~]
\end{zed}
If the pump has failed, but its controller is okay and does not detect
flow, then we can assume that the pump has no flow through it.
\begin{zed}
  PFailedPCNoFlow ==
  \\ %
  \t1 [~ PumpCtr0 | pst = \freetypepfailed \land pcst
  = \freetypepcnoflow \implies pa_1 = 0 \land pa_2 = 0 ~]
\end{zed}
Finally, if both the pump and the controller have failed, then we know
nothing about the approximation, and the limits are extreme.
\begin{zed}
  PFailedPCFailed ==
  \\ %
  \t1 [~ PumpCtr0 | pst = \freetypepfailed \land pcst
  = \freetypepcfailed \implies pa_1 = 0 \land pa_2 = P ~]
\end{zed}
The pump-controller assembly is specified by these six invariants.
\begin{zed}
  PumpCtr ==
  \\ %
  \t1 POpenPCFlowOrFailed \land PWaitingPCNoFlowOrFailed \land \\ %
  \t1 PClosedPCNoFlowOrFailed \land PFailedPCFlow \land PFailedPCFlow \land  \\
  \t1 PFailedPCFailed
\end{zed}
The pump controller is in its initial state when the pump is in
\emph{its} initial state and when the controller indicates that there
is no water flowing.
\begin{zed}
  InitPumpCtr == [~ PumpCtr' | InitPump \land pcst' = \freetypepcnoflow ~]
\end{zed}
The pump-controller assembly is promoted to a system of four pumps;
the system has its own lower and upper limits, derived from those of
the individual pumps.
\begin{zed}
  PumpIndex == 1 \upto 4
\end{zed}
\vspace{-5ex}
\begin{schema}{PumpCtrSystem}
  pumpctr: PumpIndex \fun PumpCtr
  \\ %
  pa_1~, pa_2: \nat
  \where %
  pa_1 =
   %
    ( pumpctr~1 ).pa_1 + ( pumpctr~2 ).pa_1 +  %
    \\ \t1 %
    ( pumpctr~3 ).pa_1 + ( pumpctr~4 ).pa_1   %
  \also %
  pa_2 =
   %
    ( pumpctr~1 ).pa_2 + ( pumpctr~2 ).pa_2 +  %
    \\ \t1 %
    ( pumpctr~3 ).pa_2 + ( pumpctr~4 ).pa_2  %
\end{schema}
The pump-control subsystem is in its initial state when each
controller is in \emph{its} initial state.
\begin{schema}{InitPumpCtrSystem}
  PumpCtrSystem~'
  \where %
  \exists InitPumpCtr @
  \\ %
  \t1 \forall i: PumpIndex @ pumpctr'~i = \theta PumpCtr'
\end{schema}

\section{Valve}

There is no discussion in the requirements of the possible failure of
the evacuation valve.  This is a rather puzzling omission, since it
seems as unlikely to be a perfect piece of equipment as any other
device in the system.  This should be discussed with the customer.
For the time being, we do model it as a perfect device.

\begin{addedstuff}
Added \LaTeX\ markup directives for the next free type:
%%Zword \freetypevopen vopen
%%Zword \freetypevclosed vclosed
\end{addedstuff}
\begin{zed}
  VState ::= \freetypevopen | \freetypevclosed
  \also %
  Valve == [~ valve: VState ~]
  \also %
  InitValve == [~ Valve~' | valve' = \freetypevclosed ~]
\end{zed}
A valve has two states and it is initially closed.

\section{Expected values}

During each cycle, we can calculate the values that we expect the
parameters to take during the next cycle.  For the water-level and
steam-rate sensors, we calculate the range of the expected upper and
lower limits, based on our mathematical model of the steam-boiler's
dynamics.
\begin{zed}
  CValues == [~ qc_1~, qc_2~, vc_1~, vc_2: \nat ~]
\end{zed}
Initially, these calculations are as loose as possible.
\begin{zed}
  InitCValues == [~ CValues~' | qc_1' = 0 \land qc_2' = C \land vc_1' = 0 \land vc_2' = W ~]
\end{zed}
Of course, there are invariants relating to our calculations.  First,
if the valve is open, then the calculated lower-bound for the water
level must be zero.
\begin{zed}
  QLowerBoundValveOpen == [~ CValues; Valve | valve = \freetypevopen \land qc_1 = 0 ~]
\end{zed}
On the other hand, if the valve is closed, then we may calculate the
value of this lower-bound from the formula given in the requirements,
\[
  qc_1 = qa_1 - va_2 \Delta t - \frac{1}{2} U_1 \Delta t^2 + \Delta t ~ pa_1 %
\]
where \( \Delta t \)\/ is the cycle time, for us five seconds, and \(
U_1 \)\/ is the maximum gradient of increase of the quantity of
steam.\footnote{Actually, this is \emph{not} the formula given in the
  requirements, since it differs in the final term: where we have \(
  \Delta t ~ pa_1 \), the requirements state simply \( pa_1 \).  We
  believe that our formula is correct, but this should really be
  checked with the customer.} This calculation simply predicts what
the level should be at the start of the next cycle, based on the value
in this cycle: we will have lost some water due to steam, and gained
some due to the input of the pumps.  For our own convenience, we
assume that the accuracy in our calculation is good enough (integer
arithmetic on values in litres and rates in litres per second); more
accurate results would be obtained with a change to more suitable
arithmetic.

It makes no sense for the steam boiler to be less than empty, and if
our calculation produces a negative result, it is because our
approximations were too loose.

\begin{zed}
  QLowerBoundValveClosed ==
  \\ %
  \t1 [~ CValues; QSensor; VSensor; Pump; Valve | valve = \freetypevclosed \land \\
     \t2 qc_1 = max \{ 0, qa_1 - 5 * va_2 - 12 * U_1 + 5 * pa_1 \} ~]
\end{zed}
The upper-bound may be calculated in a similar fashion; of course, it
makes no sense for the steam boiler to be more than full.
\begin{zed}
  QUpperBound ==
  \\ %
  \t1 [~ CValues; QSensor; VSensor; Pump | \\ %
    \t2 qc_2 = min \{ C, qa_2 - 5 * va_1 + 12 * U_2 + 5 * pa_2 \} ~]
\end{zed}

We can also calculate the expected value of the steam rate at the
start of the next cycle:~the lower-bound cannot have changed more than
dictated by \( U_2 \), the maximum gradient of decrease.
\begin{zed}
  VLowerBound == [~ CValues; VSensor | vc_1 = max \{ 0, va_1 - 5 * U_2 \} ~]
\end{zed}
The upper-bound for the steam-rate sensor is calculated in a similar
way to its lower-bound.
\begin{zed}
  VUpperBound == [~ CValues; VSensor | vc_2 = min \{ W, va_2 - 5 * U_1 \} ~]
\end{zed}

The input tells us whether the pumps are either open or closed; it
does not tell us whether the pump is waiting to open or if it has
failed: these states come from deductions that the program may make.
\begin{zed}
  InputPState == \{ \freetypepopen, \freetypepclosed \}
\end{zed}
The input also tells us whether there is flow or not.
\begin{zed}
  InputPCState == \{ \freetypepcflow, \freetypepcnoflow \}
\end{zed}
We expect the pumps to be in certain states, depending on the command
that we issued in the last cycle.
\begin{schema}{ExpectedPumpStates}
  expectedp: PumpIndex \fun InputPState
  \\ %
  expectedpc: PumpIndex \fun InputPCState
\end{schema}
Initially, we have no expectations about the pumps' states, so the
values in the range of \( expectedp \) and \( expectedpc \) are
arbitrary.

Our equipment is modelled by the state of the water sensor, the steam
rate sensor, the pump control subsystem, the evacuation valve, and the
calculations of expected values.
\begin{zed}
  Equipment0 ==
  \\ %
  \t1
    QSensor \land VSensor \land PumpCtrSystem \land Valve \land \\ %
  \t1  CValues \land ExpectedPumpStates
\end{zed}

\section{Failures and repairs}

There is a simple protocol for failures that needs to be observed:
once a failure has been detected, it must be reported; the report is
made repeatedly until the operator acknowledges it; a failed component
may be repaired; the program should acknowledge the repair.  To follow
the protocol, we keep track of the failures and their acknowledgements

We start by extracting information on the various equipment failures:
the sensors, pumps, and controllers have been judged to have failed if
their state records this fact.
\begin{zed}
  QFailed == [~ QSensor | qst = \freetypesfailed ~]
  \also %
  VFailed == [~ VSensor | vst = \freetypesfailed ~]
  \also %
  PFailed ==
  \\ %
  \t1 [~ PumpCtrSystem | (~ \exists i: PumpIndex \spot (
  pumpctr~i).pst = \freetypepfailed ~) ~]
  \also %
  PCFailed ==
  \\ %
  \t1 [~ PumpCtrSystem | (~ \exists i: PumpIndex \spot (
  pumpctr~i).pcst = \freetypepcfailed ~) ~]
\end{zed}
The program is required to transmit messages notifying the operator of
these equipment failures; the information comes from the following
free type.
\begin{addedstuff}
Added \LaTeX\ markup directives for the next free type:
%%Zword \freetypeqfail qfail
%%Zword \freetypevfail vfail
%%Zword \freetypepfail pfail
%%Zword \freetypepcfail pcfail
\end{addedstuff}
\begin{zed}
  UnitFailure ::= \freetypeqfail | \freetypevfail | \freetypepfail \ldata PumpIndex \rdata | \freetypepcfail \ldata PumpIndex \rdata
  \also %
  Failures == [~ failures, noacks: \power UnitFailure | noacks \subseteq failures ~]
\end{zed}
The \( failures \)\/ component is derived from existing state
information; the \( noack \)\/ set records those failure reports that
have yet to be acknowledged by the operator.  These two records are
included in the analyser's model of the equipment.
\begin{schema}{EquipmentFailures}
  Equipment0
  \\ %
  Failures
  \where %
  failures =
  \\ %
  \t1
    \{~ u: UnitFailure; i: PumpIndex | \\ %
    \t2
      (~ u = \freetypeqfail \land QFailed ~) \lor {} %
      (~ u = \freetypevfail \land VFailed ~) \lor {} %
      \\ %
    \t2
      (~ u = \freetypepfail~i \land PFailed ~) \lor {} %
      (~ u = \freetypepcfail~i \land PCFailed ~) @ u ~\}
\end{schema}
Since the set of failures is derived, we don't need to describe its
initial state.  Initially, there are no unacknowledged failure
reports.
\begin{zed}
  InitFailures == [~ Failures~' | noacks' = \emptyset ~]
\end{zed}
When the operator acknowledges a failure report, the appropriate
failure had better be in the \( noacks \)\/ set; the unacknowledged
set is updated.
\begin{zed}
  FailuresExpected ==
  \\ %
  \t1 [~ Failures; failureacks: \power UnitFailure | failureacks
  \subseteq noacks ~]
  \also %
  AcceptFailureAcks ==
  \\ %
  \t1 [~ \Delta Failures; FailuresExpected | noacks' = noacks
  \setminus failureacks ~]
\end{zed}
If a repair is reported, then it had better be a repair of a failed
piece of equipment; the failures are updated accordingly.
\begin{zed}
  RepairsExpected ==
  \\ %
  \t1 [~ Failures; repairs: \power UnitFailure | repairs
  \subseteq failures ~]
  \also %
  AcceptRepairs ==
  \\ %
  \t1
   %
    [~ \Delta Failures; RepairsExpected | %
    \\ %
    \t1 failures' = failures \setminus repairs \land noacks' = noacks
    \setminus repairs ~]
\end{zed}

So, the \( \mathsl{Analyser} \, \)'s view of the state of the
equipment consists of the state of the sensors, the pumps, the valve,
the invariant calculations of the lower and upper-bounds for the
water-level and steam-production rate, the expected pump states, and
the records of failures and acknowledgements.
\begin{zed}
  Equipment ==
  \\ %
  \t1
    (~ QLowerBoundValveOpen \lor QLowerBoundValveClosed ~) \land {} %
    \\ \t1 %
    QUpperBound \land VLowerBound \land VUpperBound \land {}
    \\ \t1 %
    ExpectedPumpStates \land EquipmentFailures
\end{zed}
The initial value of the  valve is undetermined.
\begin{zed}
  InitEquipment ==
  \\ %
  \t1
   %
    Equipment~' \land InitQSensor \land InitVSensor \land {} %
    \\ \t1 %
    InitPumpCtrSystem \land InitCValues \land InitFailures
\end{zed}

\section{Input messages}

We turn now to the input messages that may be received from the
physical units.  There are four kinds of messages: signals that
instruct the program in various ways; messages that report the state
of individual physical units; messages that report the repair of
individual units; and messages that acknowledge the program's report
of failure of individual units.

An input signal is one of the following: a stop command; an indication
that the steam boiler is waiting; or an indication that the physical
units are ready; or an indication that there has been a transmission
failure.
\begin{addedstuff}
Added \LaTeX\ markup directives for the next free type:
%%Zword \freetypestop stop
%%Zword \freetypesteamBoilerWaiting steamBoilerWaiting
%%Zword \freetypephysicalUnitsReady physicalUnitsReady
%%Zword \freetypetransmissionFailure transmissionFailure
\end{addedstuff}
\begin{zed}
  InputSignal ::=
  \\ %
  \t1 \freetypestop | \freetypesteamBoilerWaiting |
  \freetypephysicalUnitsReady | \freetypetransmissionFailure
\end{zed}
\emph{Transmission failure} may be regarded as a property of the input
messages received in a particular cycle: either there has been a
failure or there has not, and we are not saying what the detection
mechanism is, but that there must be one.  We have chosen to model
this failure as another kind of signal, and to leave its precise
details to a later stage of development.

The \( \mathsl{Analyser} \, \)\/ receives from the physical units the
state of the pumps, their controllers, and the readings of each
sensor.
\begin{schema}{UnitState}
  pumpState: PumpIndex \fun InputPState
  \\ %
  pumpCtrState: PumpIndex \fun InputPCState
  \\ %
  q, v: \nat
\end{schema}
It also receives information on any repairs recently carried out.
Since all input messages may be considered to arrive simultaneously,
we describe the type of input messages as containing these three types
of messages, as well as a set of signals.
\begin{schema}{InputMsg}
  signals: \power InputSignal
  \\ %
  UnitState
  \\ %
  failureacks, repairs: \power UnitFailure
\end{schema}

\section{Analysing messages}

For a given \( InputMsg \), we are interested in whether a certain
value was in its expected range or not.
\begin{zed}
  Expected == [~ x?, a_1~, a_2 : \nat | a_1 \leq x? \leq a_2 ~]
  \also %
  Unexpected == \lnot Expected
\end{zed}
A sensor is a unit with additional calculated-bounds and an input for
consideration.
\begin{zed}
  Sensor == [~ \Delta Unit[SState]; c_1~, c_2~, c_1'~, c_2'~, x?: \nat
  ~]
\end{zed}
The program detects a sensor failure when it finds that its input is
unexpected; if there is a failure, either detected now or previously,
the sensor's value is taken to be that last calculated, rather than
the current input.
\begin{schema}{CheckAndAdjustSensor}
  Sensor
  \where %
  Expected \implies st' = st
  \\ %
  Unexpected \implies st' = \freetypesfailed
  \\ %
  st' = \freetypesokay \implies a_1' = x? \land a_2' = x?
  \\ %
  st' = \freetypesfailed \implies a_1' = c_1 \land a_2' = c_2
\end{schema}
These general definitions are instantiated for each sensor.
\begin{zed}
%  QExpected == QSensor \land Expected[q?/x?, qa_1/a_1, qa_2/a_2]
%  \\ %
%  QUnexpected == QSensor \land Unexpected[q?/x?, qa_1/a_1,
%  qa_2/a_2]
%  \also %
  CheckAndAdjustQ ==
  \\ %
  \t1
    QSensor \land {} %
    \\ \t1 %
    CheckAndAdjustSensor[
      q?/x?, qa_1~/a_1~, qa_2~/a_2~, qc_1~/c_1~, qc_2~/c_2~, qst/st, %
      \\ \t2 %
      qa_1'~/a_1'~, qa_2'~/a_2'~, qc_1'~/c_1'~, qc_2'~/c_2'~, qst'/st']
     %
   %
%  \also %
%  VExpected == VSensor \land Expected[v?/x?, va_1/a_1, va_2/a_2]
%  \\ %
%  VUnexpected == VSensor \land Unexpected[v?/x?, va_1/a_1,
%  va_2/a_2]
  \also %
  CheckAndAdjustV ==
  \\ %
  \t1
   %
    VSensor \land {} %
    \\ \t1 %
    CheckAndAdjustSensor[
    %
      v?/x?, va_1~/a_1~, va_2~/a_2~, vc_1~/c_1~, vc_2~/c_2~, vst/st,
      \\ \t2 %
      va_1'~/a_1'~, va_2'~/a_2'~, vc_1'~/c_1'~, vc_2'~/c_2'~, vst'/st']
\end{zed}

%\begin{axdef}
%  expectedPC: PState \cross InputPState \pfun InputPCState
%  \where %
%  expectedPC =
%  \\ %
%  \t1
%  \{~ %
%    ( \freetypepopen, \freetypepopen ) \mapsto \freetypepcflow,
%    \\ \t2 %
%    ( \freetypepopen, \freetypepclosed ) \mapsto \freetypepcnoflow,
%    \\ \t2%
%    ( \freetypepclosed, \freetypepopen ) \mapsto \freetypepcnoflow,
%    \\ \t2 %
%    ( \freetypepclosed, \freetypepclosed ) \mapsto \freetypepcnoflow,
%    \\ \t2 %
%    ( \freetypepwaiting, \freetypepopen ) \mapsto \freetypepcflow,
%    \\ \t2 %
%    ( \freetypepwaiting, \freetypepclosed ) \mapsto \freetypepcnoflow %
%    ~\}
%\end{axdef}

The input message tells the \( \mathsl{Analyser} \)\/ about the state
of the pumps and their controllers; the \( \mathsl{Analyser} \)\/
checks to see if this information is consistent with what it expects.
For an individual pump, we have four values: the inputs telling us the
current state of pump and controller, and the expected values.  If
either value is unexpected, then we assume that the pump has failed.
\begin{schema}{CheckAndAdjustPump}
  \Delta PumpCtr
  \\ %
  pst?, exppst: InputPState
  \\ %
  pcst?, exppcst: InputPCState
  \where %
  pst? = exppst \implies pst' = pst? \land {}
  \\ %
  pst? \neq exppst \implies pst' = \freetypepfailed \land {}
  \\ %
  pcst? = exppcst \implies pcst' = pcst? \land {}
  \\ %
  pcst? \neq exppcst \implies pcst' = \freetypepcfailed
\end{schema}
This check is promoted to the pump control system by identifying it as
a check of the \( i \)-th pump.
\begin{schema}{PromotePumpCheck}
  \Delta PumpCtr
  \\ %
  \Delta PumpCtrSystem
  \\ %
  ExpectedPumpStates
  \\ %
  pst?, exppst: InputPState
  \\ %
  pcst?, exppcst: InputPCState
  \\ %
  pumpState?: PumpIndex \fun InputPState
  \\ %
  pumpCtrState?: PumpIndex \fun InputPCState
  \\ %
  i: PumpIndex
  \where %
  \theta PumpCtr = pumpctr~i
  \\ %
  pst? = pumpState?~i
  \\ %
  pcst? = pumpCtrState?~i
  \\ %
  exppst = expectedp~i
  \\ %
  exppcst = expectedpc~i
\end{schema}
\begin{zed}
  SetPumpCtr ==
  \\ %
  \t1
   %
    \exists PumpCtr; PumpCtr' @ %
    \\
    \t2
      \forall pst?, exppst: PState; pcst?, exppcst: PCState; %
      i: PumpIndex  @
      \\ %
      \t3 PromotePumpCheck \land CheckAndAdjustPump
\end{zed}
The program keeps a running total of the \( \freetypestop \)\/ signals
received.
\begin{schema}{StopPresent}
  signals?: \power InputSignal
  \\ %
  stops, stops': \nat
  \where %
  \freetypestop \in signals?
  \\ %
  stops' = stops + 1
\end{schema}
This count is reset if \( \freetypestop \)\/ is not present and fewer
than three have been received in a row.
\begin{schema}{StopNotPresent}
  signals?: \power InputSignal
  \\ %
  stops, stops': \nat
  \where %
  \freetypestop \notin signals? \land stops < 3
  \\ %
  stops' = 0
\end{schema}
The value is preserved otherwise.
\begin{schema}{TooManyStops}
  signals?: \power InputSignal
  \\ %
  stops, stops': \nat
  \where %
  \freetypestop \notin signals? \land stops \geq 3
  \\ %
  stops' = stops
\end{schema}
\begin{zed}
  AdjustStops == StopPresent \lor StopNotPresent \lor TooManyStops
\end{zed}

\section{The $\mathsl{Analyser}$}

We replace the abstract information channel, \( \mathsl{ainfo} \),
with various channels bearing more precise information.  An informal
description of the events occurring on these channels is given in
figure~\ref{figure:events}.
\begin{table}[htbp]
  \bigskip %
  \begin{center}
    \begin{tabular}{r|l}
      \textbf{\slshape event} & \textbf{\slshape interpretation}
      \\ %
      \hline %
      \( \event{emergencystop.\true} \) & too many equipment failures
      \\ %
      & three stop-commands
      \\ %
      & water level near \( M_2 \, \)\/ or \( M_1 \)
      \\ %
      & transmission failure
      \\ %
      \( \event{sbwaiting.\true} \) & boiler waiting signal received
      \\ %
      \( \event{physicalunitsready.\true} \) & physical units ready signal
      \\ %
      \( \event{vzero.\true} \) & no steam leaving boiler
      \\ %
      \( \event{levelbelowmin} \) & water level below \( N_1 \)
      \\ %
      \( \event{levelabovemax} \) & water level above \( N_2 \)
      \\ %
      \( \event{levelokay.\true} \) & water level in normal range
      \\ %
      \( \event{failures.\false} \) & no failures
      \\ %
      \( \event{qfailure.\true} \) & level failure
      \\ %
      \( \event{nonqfailure.\true} \) & steam, pump, or controller failure
    \end{tabular}
  \end{center}
  \caption{Events and their interpretations}\label{figure:events}
\end{table}
%
\begin{addedstuff}
   The Z standard does not allow soft new lines after a comma-separated list
   of declared names, hence we cannot introduce a line break at $nonqfailure$.
   The problem is that if we want to add this, we needed to change the way that
   new lines and commas are related (see Section 7.3 of Z Standard). Or use some
   new token for the comma, which is not nice. This is a unsolved problem.
\end{addedstuff}
\begin{circus}
   \circchannel\ levelbelowmin, levelabovemax %
  \also %
  \circchannel\ emergencystop, failures, levelokay, nonqfailure: \boolean \\
  \circchannel\ physicalunitsready, qfailure, sbwaiting, vzero: \boolean
\end{circus}
The abstract channel that represents the flow of information about
failures and repairs must also be replaced.  The new \(
\mathsl{failuresrepairs} \)\/ channel is used to transmit a pair,
denoting the outstanding failures and acknowledged repairs,
respectively.
\begin{circus}
   \circchannel\ failuresrepairs: (\power UnitFailure) \cross (\power UnitFailure)
\end{circus}
Finally, the abstract channel that represents the flow of information
about pump commands must also be replaced.
\begin{circus}
  \circchannel\ pumps: PumpIndex \fun InputPState \\
  \circchannelset\ Information ==  \\ \t1
    \lchanset emergencystop, failures, levelabovemax, levelbelowmin, levelokay, \\ \t2
              nonqfailure, physicalunitsready, qfailure, sbwaiting, vzero \rchanset
\end{circus}

\begin{addedstuff}
   As this is a unboxed version of the steam-boiler, we collected all text for the
   $Analyser$ process together, where the formal text follows.
\end{addedstuff}

The \( \mathsl{Analyser} \)\textsl{'s}\/ state contains the state of
the equipment, the last input message, the number of stops received in
sequence, and a record of the past signals received.

The operation to check and adjust the pump values needs to occur
before the rest of the input analysis, and the following schema is
used to promote it.

When the \( \mathsl{Analyser} \, \)\/ starts up, it initialises the
states of its equipment; the stored input message is irrelevant; there
are no stops; and the signal history is empty.

When an input message has been received, it is stored and the sensors,
unit states, and stop-count are adjusted.

The new state calls for an emergency stop if any of the following are
\true: it contains at least three stop commands; the water level is
near one of its two danger-limit values; or there has been a
transmission failure.  The risk of reaching either \( M_1 \)\/ or \(
M_2 \)\/ is assessed by the water level having exceeded the normal
working limits.

The water level is below the minimum if its lower-bound is below \(
N_1 \), but not in the danger zone, and its upper-bound is below \(
N_2 \). Similarly, it is above the maximum, providing its upper-bound is above
\( N_2 \), but not in the danger zone, and its lower-bound is above \(
N_1 \). It is in range, providing that both the upper and lower-bounds are
within the working limits. The steam rate is zero, providing that both upper and lower-bounds are
zero. All physical units are said to be okay, providing that there are no
failures. The water-level sensor is the most sensitive component, and we can
tolerate other physical units failing more easily.

The \( \mathsl{Analyser} \, \)'s behaviour is simple.  First, the
state is initialised, and then there is a cycle of behaviour.  On each
cycle, the \( \mathsl{Analyser} \, \)\/ goes through the following
sequence of events.
\begin{enumerate}\compresslist
\item It waits for the beginning of the program's cycle.
\item It inputs the next message for the physical units.
\item It processes the inputs.
\item It waits for the beginning of the execution phase.
\item It offers its information service.
\item It stops its information service at the start of the report
  phase.
\end{enumerate}

\begin{addedstuff}
   Note that all schema inclusions which contain strokes must have a hard space between the name and the stroke.
\end{addedstuff}

\begin{circus}
   \circprocess\ Analyser \circdef\ \circbegin \\
    \t1 \circstate\ AnalyserState == \\ \t2 [~ Equipment; InputMsg;
            stops: \nat; signalhistory: \power InputSignal ~] \\
    \t1 PumpOp == \\ \t2 \Xi QSensor \land \Xi VSensor \land \Xi Valve \land
             \Xi CValues \land \Xi EquipmentFailures \\
    \t1 InitAnalyserState == \\
        \t2 [~ AnalyserState~' | InitEquipment \land stops' = 0 \land signalhistory' = \emptyset ~] \\
    \t1 Analyse == \\
        \t2 [~ \Delta AnalyserState; InputMsg~? | \theta InputMsg~' = \theta InputMsg~? \\
        \t2 CheckAndAdjustQ \land CheckAndAdjustV \land AcceptFailureAcks \\
        \t2 AcceptRepairs \land SetPumpCtr \land AdjustStops \\
        \t2 signalhistory' = signalhistory \cup signals? ~] \\
    \t1 DangerZone == \\
        \t2 [~ AnalyserState | qa_1 \geq M_1 \land qa_2 \leq M_2 \implies qa_1 < N_1 \land N_1 < qa_2 ~] \\
    \t1 EmergencyStopCond == \\
        \t2 [~ AnalyserState | stops \geq 3 \lor DangerZone \lor \lnot RepairsExpected \lor \\
            \t2 \lnot FailuresExpected \lor \freetypetransmissionFailure \in signals ~] \\
    \t1 LevelBelowMin == [~ AnalyserState | M_1 \leq qa_1 < N_1 \land qa_2 \leq N_2 ~] \\
    \t1 LevelAboveMax == [~ AnalyserState | N_1 \leq qa_1 \land N_2 < qa_2 \leq M_2 ~] \\
    \t1 LevelInRange == [~ AnalyserState | N_1 \leq qa_1 \land qa_2 \leq N_2 ~] \\
    \t1 RateZero == [~ VSensor | va_1 = 0 \land va_2 = 0 ~] \\
    \t1 AllPhysicalUnitsOkay == \\
        \t2 [~ AnalyserState | \lnot QFailed \land \lnot VFailed \land \lnot PFailed \land \lnot PCFailed ~] \\
    \t1 OtherPhysicalUnitsFail == \lnot QFailed \land \lnot AllPhysicalUnitsOkay \\
    \t1 SteamBoilerWaiting == \\
        \t2 [~ AnalyserState | \freetypesteamBoilerWaiting \in signalhistory ~] \\
    \t1 PhysicalUnitsReady == \\
        \t2 [~ AnalyserState | \freetypephysicalUnitsReady \in signalhistory ~]
    \also
    \t1 AnalyserCycle \circdef startcycle \then input~?msg \then \lschexpract SetPumpCtr \land PumpOp \rschexpract \circseq \\
            \t2 Analyse \circseq\ startexec \then InfoService \\
    \t1 InfoService \circdef (OfferInformation \circseq\ InfoService) \extchoice \\
            \t2 failuresrepairs~!(noacks, repairs) \then pumps~?pumpstate \then \\
            \t2 pumpState := pumpstate \circseq AnalyserCycle \\
    \t1 OfferInformation \circdef \\
            \t2 emergencystop.EmergencyStop \then Skip \\ \t2 \extchoice \\ %
            \t2 sbwaiting.SteamBoilerWaiting \then Skip \\ \t2 \extchoice \\
            \t2 vzero.RateZero \then Skip \\ \t2 \extchoice \\ %
            \t2 \lcircguard LevelBelowMin \rcircguard \circguard\ levelbelowmin \then Skip \\ \t2 \extchoice \\
            \t2 \lcircguard LevelAboveMax \rcircguard \circguard\ levelabovemax \then Skip \\ \t2 \extchoice \\ %
            \t2 levelokay.LevelInRange \then Skip \\ \t2 \extchoice \\ %
            \t2 physicalunitsready.PhysicalUnitsReady \then Skip \\ \t2 \extchoice  \\ %
            \t2 failures.(\lnot AllPhysicalUnitsOkay) \then Skip \\ \t2 \extchoice \\
            \t2 qfailure.QFailed \then Skip \\ \t2 \extchoice \\ %
            \t2 nonqfailure.OtherPhysicalUnitsFail \then Skip \\
    \t1 @ InitAnalyserState \circseq\ AnalyserCycle \\
    \circend
\end{circus}

The $Analyse$ reference is given as an action call. If one wants it to be a schema expression action
directly, one needs to include the schema expression fat parenthesis around it.


The \( \mathsl{Analyser} \, \)\/ is added to the \( \mathsl{Timer} \,
\), synchronising on the \( \mathsl{startcycle} \)\/ event.
%
\begin{circus}
    \circchannelset\ TAnalyserInterface == \lchanset startcycle \rchanset \\
    \circprocess\ TAnalyser \circdef \\
        \t1 Timer \lpar TAnalyserInterface \rpar Analyser \circhide TAnalyserInterface
\end{circus}
%
It is easy to see that this assembly is free from deadlock and livelock, and this is confirmed by FDR.
\[
  \mathbf{assert}\ \mathsl{TSAnalyser} :[ \hbox{ deadlock free } [FD] ] %
  \also %
  \mathbf{assert}\ \mathsl{TSAnalyser} :[ \hbox{ livelock free } [FD] ]
\]
%
FDR code for the \( \mathsl{Analyser} \)\/ is contained in appendix~\ref{appendix:FDR-code}.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\chapter{The $\mathsl{Controller}$}

The boiler \( \mathsl{Controller} \, \)\/ maintains only one state
item: the current mode, which is chosen from the free type \( Mode \).
\begin{addedstuff}
Added \LaTeX\ markup directives for the next free type:
%%Zword \freetypeinitialisation initialisation
%%Zword \freetypenormal normal
%%Zword \freetypedegraded degraded
%%Zword \freetyperescue rescue
%%Zword \freetypeemergencyStop emergencyStop
\end{addedstuff}
\begin{zed}
  Mode ::= \freetypeinitialisation | \freetypenormal | \freetypedegraded | \freetyperescue | \freetypeemergencyStop
\end{zed}

\begin{circus}
    \circchannel\ startpumps, stoppumps, openvalve, closevalve, sendprogready \\
    \circchannelset\ Reports == \\
        \t1 \lchanset startpumps, stoppumps, openvalve, closevalve, sendprogready \rchanset \\
    \circchannelset\ TAControllerInterface ==  \\
        \t1 \lchanset startexec \rchanset \cup Information
\end{circus}

The \( \mathsl{Controller} \, \)\/ starts in \(
\freetypeinitialisation \)\/ mode, where it performs various checks on
the correct operation of the physical units.  Subsequently, it has the
behaviour shown in table~\ref{tab:controller-modes}.
Each time the \( \mathsl{Controller} \, \)\/ enters a new state, it
reports this fact. The \( \mathsl{Controller} \, \)\/ starts by entering the
initialisation state, then it behaves like \( \mathsl{ControllerCycle}
\, \).

\begin{table}[htbp]
  \begin{center}
    \bigskip %
    \begin{tabular}{l|l}
      \bfseries{mode} & \bfseries{condition}
      \\ %
      \hline %
      \( \freetypenormal \) & no failures
      \\ %
      \( \freetypedegraded \) & water sensor okay, other component failures
      \\ %
      \( \freetyperescue \) & water sensor failed, all other components okay
      \\ %
      \( \freetypeemergencyStop \) & two component failures,
      \event{emergencystop.\true}, or
      \\ %
      & transmission failure
    \end{tabular}
    \caption{Boiler-controller operation modes}
    \label{tab:controller-modes}
  \end{center}
\end{table}

\begin{addedstuff}
   As before, we collected the text before the formal paragraphs.
   At this time, it spread across various sections.
\end{addedstuff}

Each cycle is started by the \( \event{startexec} \, \)\/ event.  The
first action is to determine if an emergency stop is required; if so,
it enters that mode without further delay.  Otherwise, there is a case
analysis, based on the mode left by the last cycle, to decide what to
do next.  Following this, the water level in the boiler is adjusted,
if necessary.  The end of the analysis phase is signalled by
participation in the \( \event{startreport} \, \)\/ event.

\section{Initialisation mode}

In the initialisation mode, the \( \mathsl{Controller} \, \)\/ checks
that the operation of the steam boiler can start.  If so, then it
checks that the sensor agrees that no steam is being produced, that
the water-level sensor has not failed, that the physical units are
ready for action, that the level of water in the boiler is
appropriate, and that there are no other equipment failures.  It then
enters the normal mode for operation.  In terms of the abstract events
made available by the information service, the \( \mathsl{Controller}
\, \)\/ checks for the following event-sequence, before entering
normal mode.
\[
  \langle~ %
  \begin{block}
    \event{sbwaiting.\true},
    \\ %
    \t1
    \begin{block}
      \event{vzero.\true},
      \\ %
      \t1
      \begin{block}
        \event{qfailure.\false},
        \\ %
        \t1
        \begin{block}
          \event{levelokay.\true},
          \\ %
          \t1
          \begin{block}
            \event{sendprogready},
            \\ %
            \t1 \event{physicalunitsready.\true} ~\rangle
          \end{block}
        \end{block}
      \end{block}
    \end{block}
  \end{block}
\]
If this event-sequence is not possible, then the \(
\mathsl{Controller} \, \)\/ responds accordingly.  If the
steam-boiler-waiting signal is not received, then the \(
\mathsl{Controller} \, \)\/ waits for the next cycle.  If the rate of
steam production is not zero, then the steam gauge must be defective,
since the boiler has not been put into action yet; we are required to
abort the initialisation.  If the water-level sensor has failed, then
the program is again required to stop.  If the level of water in the
boiler is not in range, then it will be adjusted on the next step
following this analysis.  If neither the steam sensor nor the water
level have failed, but some other component has, then it must be some
kind of pump failure; the \( \mathsl{Controller} \, \)\/ proceeds in
degraded mode.

\section{Normal mode}

The \( \mathsl{Controller} \, \)\/ proceeds in normal mode, providing
that nothing has failed; if the water sensor fails, it enters rescue
mode; if anything else fails, then it enters degraded mode; if there
were too many failures, then the \( \mathsl{Controller} \, \)\/ would
already have entered the emergency-stop mode.

\begin{addedstuff}
   For the dangling $else$ part, we have included the complementary guard, which one could
   argue that is equivalence to a simplified version ($mode = \freetypeemergencyStop$).
\end{addedstuff}

\section{Degraded mode}

The \( \mathsl{Controller} \, \)\/ proceeds in degraded mode,
providing that the water sensor hasn't failed and that none of the
outstanding failures have been repaired.  If there are no failures,
because the outstanding repairs have been completed and no further
failures were detected by the \( \mathsl{Analyser} \, \), then the \(
\mathsl{Controller} \, \)\/ returns to the normal mode.  If the water
sensor has failed, then the \( \mathsl{Controller} \, \)\/ enters the
rescue mode.  If there were too many failures, then the \(
\mathsl{Controller} \, \)\/ would already have entered the
emergency-stop mode.

\section{Rescue mode}

The \( \mathsl{Controller} \, \)\/ stays in the rescue mode if the
water-level sensor hasn't been repaired; if it has, then it returns
either to normal or to degraded mode, depending on whether there are
further repairs outstanding.  If there were too many failures, then
the \( \mathsl{Controller} \, \)\/ would already have entered the
emergency-stop mode.

\section{Actions}

The action that adjusts the level of water in the boiler depends on
what has to be done: raise, reduce, or retain the level.

If the level needs to be raised, then the pumps are started.  The
valve may need to be closed, but this would be in only the
initialisation mode.  We assume that closing a closed valve has no
undesirable effect.

If the level needs to be reduced, then the pumps are stopped.  The
valve may be opened in only the initialisation mode.  We assume that
opening an open valve has no undesirable effect.

To retain the level, we stop the pumps and make sure that the valve is
closed in initialisation mode.

Starting and stopping pumps and opening and closing valves are all
simple matters.

This completes the description of the \( \mathsl{Controller} \, \).

\section{The formal (unboxed) paragraphs}

\begin{circus}
    \circprocess\ Controller \circdef \circbegin \\
        \t1 \circstate\ ModeState == [~ mode: Mode ~] \\
        \t1 EnterMode \circdef m: Mode @ reportmode~!m \then mode := m \\
        \t1 ControllerCycle \circdef startexec \then startreport \then NewModeAnalysis \circseq\ \\
                \t2 AdjustLevel \circseq endreport \then ControllerCycle \\
        \t1 NewModeAnalysis \circdef emergencystop.\true \then EnterMode~(\freetypeemergencyStop)
            \\ %
            \t2 \extchoice
            emergencystop.\false \then
                \\ %
                \t3 \circif\ \ mode = \freetypeinitialisation \circthen InitModeAnalysis \\ %
                \t3\ \ \circelse\ mode = \freetypenormal \circthen NormalModeAnalysis \\
                \t3\ \ \circelse\ mode = \freetypedegraded \circthen DegradedModeAnalysis \\
                \t3\ \ \circelse\ mode = \freetyperescue \circthen RescueModeAnalysis \\
                \t3\ \ \circelse\ (mode \notin Mode \setminus \{ \freetypeemergencyStop \}) \circthen Skip \\
                \t3 \circfi \\
        \t1 InitModeAnalysis \circdef sbwaiting.\true \then (~ vzero.\true \then \\
            \t2 (~ qfailure.\false \then (~ physicalunitsready.\true \then (~ levelokay.\true \then \\
                \t3 (~ failures.\false \then EnterMode~(\freetypenormal) \extchoice \\
                \t3\ \ failures.\true \then EnterMode~(\freetypedegraded)~) \extchoice \\
                \t3 levelokay.\false \then EnterMode~(\freetypeemergencyStop)~) \extchoice \\
                \t2 physicalunitsready.\false \then (~ levelokay.\true \then \\
                \t3  sendprogready \then Skip \extchoice levelokay.\false \then Skip~) ~) \extchoice \\
                \t4 qfailure.\true \then EnterMode~(\freetypeemergencyStop)~) \extchoice \\
                \t5 vzero.\false \then EnterMode~(\freetypeemergencyStop)~) \extchoice \\
                \t2 sbwaiting.\false \then Skip \\
        \t1 NormalModeAnalysis \circdef failures.\false \then Skip \extchoice \\
            \t3 qfailure.\true \then EnterMode~(\freetyperescue) \extchoice \\
            \t3 nonqfailure.\true \then EnterMode~(\freetypedegraded) \\
        \t1 DegradedModeAnalysis \circdef qfailure.\false \then \\
                \t3 ( failures.\true \then Skip \extchoice failures.\false \then EnterMode~(\freetypenormal) ~) \\
                \t3\ \extchoice qfailure.\true \then EnterMode~(\freetyperescue) \\
        \t1 RescueModeAnalysis \circdef qfailure.\true \then Skip \extchoice \\
            \t2 qfailure.\false \then ( failures.\false \then EnterMode~(\freetypenormal) \\
                \t5 \extchoice failures.\true \then EnterMode~(\freetypedegraded)~) \\
        \t1 AdjustLevel \circdef  levelbelowmin \then RaiseLevel \extchoice \\ %
            \t2 levelabovemax \then ReduceLevel \extchoice  \\ %
            \t2 levelokay.\true \then RetainLevel \\
        \t1 RaiseLevel \circdef StartPumps \circseq\ \\
            \t2 \circif mode = \freetypeinitialisation \circthen CloseValve \\
            \t2 \circelse mode \neq \freetypeinitialisation \circthen Skip \\
            \t2 \circfi  \\
        \t1 ReduceLevel \circdef StopPumps \circseq\ \\
            \t2 \circif mode = \freetypeinitialisation \circthen OpenValve \\
            \t2\ \ \circelse mode \neq \freetypeinitialisation \circthen Skip \\
            \t2 \circfi  \\
        \t1 RetainLevel \circdef StopPumps \circseq\ \\
            \t2 \circif mode = \freetypeinitialisation \circthen CloseValve \\
            \t2\ \ \circelse mode \neq \freetypeinitialisation \circthen Skip \\
            \t2 \circfi  \\
        \t1 StartPumps \circdef startpumps \then Skip        \\ %
        \t1 StopPumps \circdef stoppumps \then Skip         \\ %
        \t1 OpenValve \circdef openvalve \then Skip         \\ %
        \t1 CloseValve \circdef closevalve \then Skip \\
        \t1 @ mode := \freetypeinitialisation \circseq ControllerCycle \\
    \circend
\end{circus}

\begin{circus}
   \circprocess\ TAController \circdef \\
    \t1 (TAnalyser \lpar TAControllerInterface \rpar Controller) \circhide TAControllerInterface
\end{circus}
\[
  \mathbf{assert}\ \mathsl{Controller} :[ \hbox{ deadlock free } [FD] ] %
  \also %
  \mathbf{assert}\ \mathsl{Controller} :[ \hbox{ livelock free } [FD] ]
\]

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\chapter{The $\mathsl{Reporter}$}

The final component is responsible for assembling the output to the
physical units, which occurs once during each cycle.  The output
contains the following information.

\begin{addedstuff}
Added \LaTeX\ markup directives for the next free type:
%%Zword \freetypeprogramReady programReady
%%Zword \freetypeopenValve openValve
%%Zword \freetypecloseValve closeValve
%%Zword \freetypelevelFailureDetection levelFailureDetection
%%Zword \freetypesteamFailureDetection steamFailureDetection
%%Zword \freetypelevelRepairedAcknowledgement levelRepairedAcknowledgement
%%Zword \freetypesteamRepairedAcknowledgement steamRepairedAcknowledgement
\end{addedstuff}
\begin{itemize}
\item The current mode.
\item Signals drawn from the following free type.
  \begin{zed}
    OutputSignal ::= \freetypeprogramReady  | \freetypeopenValve | \freetypecloseValve | \\
        \t1 \freetypelevelFailureDetection | \freetypesteamFailureDetection | \\
        \t1 \freetypelevelRepairedAcknowledgement | \freetypesteamRepairedAcknowledgement
  \end{zed}
  These inform when the program is ready for operation, whether the
  valve should be opened or closed, when the sensors have failed, and
  when their repairs have been noted.
\item Instructions on opening or closing pumps.
\item Whether pumps or their controllers have failed.
\item Acknowledgements noting the repair of pumps and their controllers.
\end{itemize}
An output is drawn from the schema type \( OutputMsg \).
\begin{schema}{OutputMsg}
  mode: Mode
  \\ %
  signals: \power OutputSignal
  \\ %
  pumpState: PumpIndex \fun InputPState
  \\ %
  pumpFailureDetection: \power Pump
  \\ %
  pumpCtrFailureDetection: \power Pump
  \\ %
  pumpRepairedAcknowledgement: \power Pump
  \\ %
  pumpCtrRepairedAcknowledgement: \power Pump
\end{schema}
It is communicated on the \( \mathsl{output} \) channel.
\begin{circus}
  \circchannel\ output: OutputMsg %
\end{circus}

\begin{addedstuff}
   Again, process related text was given in as a series of text paragraphs
   right before the actual formal (unboxed) text.
\end{addedstuff}

The process is defined as follows.
The process waits for the start of the report phase; after this, it
provides its report service.

The report service involves gathering reports until either an
emergency stop or the end of the report phase is detected, after which
some tidying up is required.

Tidying up requires obtaining information about unacknowledged
failures and new repairs from the \( \mathsl{Analyser}\), outputing
the message to the physical units, and then telling the \(
\mathsl{Analyser} \) about the commands issued to the pumps.
Reports are added to the various message components as they arrive.

\begin{addedstuff}
   The $RefName$ $FailuresRepairs$ has not been previously defined.
   It does not appear anywhere else in the text. I am assuming it is
   a schema name because of the sequential composition afterwards, but
   it could as well be an action call.

   Also, \Circus\ does not accept pattern matching on input communication,
   hence the use of $failuresrepairs~?(noacks,repairs)$ generates a parsing error.
   If those names are important, one can just appropriately rename $FailuresRepairs$
   with the use of auxiliary definitions, as in $ALTERNATIVE\_TidyUp$.
\end{addedstuff}

\begin{circus}
    \circprocess\ Reporter \circdef \circbegin \\
        \t1 ReportService \circdef GatherReports \circseq ReportService
            \\
            \t3 \extchoice  %
            \\ %
            \t3 reportmode.emergencyStop \then mode := emergencyStop \circseq TidyUp
            \\ %
            \t3 \extchoice %
            \\ %
            \t3 TidyUp \\
        \t1 TidyUp \circdef endreport \then failuresrepairs~?x \then FailuresRepairs \circseq \\
            \t3 output~!( \theta OutputMsg ) \then \\
            \t3 pumps~!pumpState \then Reporter \\
        \t1 ALTERNATIVE\_TidyUp \circdef endreport \then \\
            \t3 (\circvar\ nopairsX, repairsX: \power UnitFailure @ \\
                \t4 failuresrepairs~?x \prefixcolon x = (nopairsX, repairsX) \then \\
                \t4 \lschexpract FailuresRepairs[nopairsX/nopairs, repairsX/repairs] \rschexpract ) \circseq \\
            \t3 output~!( \theta OutputMsg ) \then \\
            \t3 pumps~!pumpState \then Reporter \\
        \t1 GatherReports \circdef \Extchoice m: Nonemergency @ reportmode.m \then mode := m
                    \\ %
                    \t3 \extchoice
                    \\ %
                    \t3 sendprogready \then signals := signals \cup \{ \freetypeprogramReady \}
                    \\ %
                    \t3 \extchoice
                    \\ %
                    \t3 startpumps \then pumpState := PumpIndex \cross \{ \freetypepopen \}
                    \\ %
                    \t3 \extchoice
                    \\ %
                    \t3 stoppumps \then pumpState := PumpIndex \cross \{ \freetypepclosed \}
                    \\ %
                    \t3 \extchoice
                    \\ %
                    \t3 openvalve \then signals := signals \cup \{ \freetypeopenValve \}
                    \\ %
                    \t3 \extchoice
                    \\ %
                    \t3 closevalve \then signals := signals \cup \{ \freetypecloseValve \} \\
        \t1 @ startreport \then ReportService \\
        \circend
\end{circus}

The reporter is added to the other components.  The result is free
from deadlock and livelock.

\begin{addedstuff}
    The $TACReporterInterface$ channel set does not appear in the text.
    It is given in the FDR script near the end of the document as:
    \begin{verbatim}
        TACReporterInterface = union( {| startreport,
            reportmode, endreport, afailuresrepairs,
            apumps |}, Reports )
    \end{verbatim}
    which is different from the value of $TACReporterInterface1$, in case one might think of a typo.
\end{addedstuff}
%
\begin{circus}
   \circchannelset\ TACReporterInterface == Reports\ \cup \\
        \t1 \lchanset startreport, reportmode, endreport, afailuresrepairs, apumps \rchanset  \\
   \circprocess\ TACReporter \circdef \\
    \t1 ( TAController \\
        \t2 \lpar TACReporterInterface \rpar \\
        \t1\ \ Reporter ) \circhide TACReporterInterface
\end{circus}
\[
  \mathbf{assert}\ \mathsl{TACReporter} :[ \mathsl{deadlock free } [FD] ]
  \also %
  \mathbf{assert}\ \mathsl{TACReporter} :[ \mathsl{livelock free } [FD] ]
\]
The steam boiler has the behaviour of the four processes:
\begin{circus}
  \circprocess\ SteamBoiler \circdef TACReporter
\end{circus}
This is a refinement of the abstract specification.
\[
  \mathsl{SteamBoiler1} \refinedby_{FD} \mathsl{SteamBoiler}
\]

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\chapter{Analysis}

Appendix~\ref{appendix:requirements} contains the informal
requirements for the program's behaviour in each of the operating
modes; these are taken verbatim
from~\cite{abrial-borger-langmaack-96}.  These requirements may be
used to verify the correct behaviour of the \( \mathsl{Controller} \).
For instance, we have that
\begin{quote}\slshape
  In the initialisation mode, the program waits for the steam-boiler
  waiting message.
\end{quote}
How should we interpret this in our model?
\begin{quote}
  The program stays in the initialisation mode at least until the
  steam-boiler waiting message has been received.
\end{quote}
The exception to this rule is that the program may always enter the
emergency-stop mode if instructed to do so.  If this does not happen,
then the \( \mathsl{Controller} \)\/ repeats the following
event-sequence whilst waiting for the steam-boiler waiting message.
\[
  \langle~ %
  \begin{block}
    startexec,
    \\ %
    \t1
    \begin{block}
      startreport,
      \\ %
      \t1
      \begin{block}
        emergencystop.\false,
        \\ %
        \t1
        \begin{block}
          sbwaiting.\false,
          \\ %
          \t1
          \begin{block}
            levelokay.\true,
            \\ %
            \t1
            \begin{block}
              stoppumps,
              \\ %
              \t1
              \begin{block}
                closevalve ~\rangle
              \end{block}
            \end{block}
          \end{block}
        \end{block}
      \end{block}
    \end{block}
  \end{block}
\]
It is easy to code this requirement in CSP.

\begin{addedstuff}
   We have encoded the CSP process using a basic Circus process.
\end{addedstuff}
\begin{circus}
   \circprocess\ WaitForSBWaiting \circdef \circbegin \\
   \t1 @ startexec \then \\
        \t2 startreport \then \\
            \t3 emergencystop.\false \then \\
                \t4 sbwaiting.\false \then \\
                    \t5 levelokay.\true \then \\
                        \t6 stoppumps \then \\
                            \t7 closevalve \then \\
                                \t8 endreport \then \\
                                    \t9 WaitForSBWaiting \\
   \circend
\end{circus}

\begin{addedstuff}
   For the analysis processes, we have included then explicitly for
   what was originally defined on-the-fly at the $assert$ statement
   used by FDR.

   Moreover, as a channel set extension is an expression (and is formed by expressions elements),
   the original syntax is slightly problematic. We cannot use $sbwaiting.\true$ because the production
   it uses is misleading (it is binding selection), which expects a $RefName$ rather than an expression
   after the dot. One way around this is by using a $\LET$ expression. Another way, would be to
   fiddle with the Z expression sub-tree to include a channel selection production.
\end{addedstuff}

\begin{circus}
   \circprocess\ Deadlock \circdef \circbegin @ Stop \circend \\
   \circprocess\ ControllerStop \circdef \\
        \t1 Controller \\
            \t2 \lpar \lchanset levelabovemax, levelbelowmin, \\
                            \t3  sbwaiting.\true, \\
                            \t3  emergencystop.\true \rchanset \rpar \\
        \t2 Deadlock %
\end{circus}
%
\begin{addedstuff}
   Also note that the channel set above generates a parsing warning about a channel set
   that seems more complicated than expected. That is because the parser accepts any Z
   expression within a Channel set expression, yet some of the expression productions
   are not valid (typecheckable) channel sets. See typechecker for details.
\end{addedstuff}
%
\[
  \mathbf{assert}\
  \begin{block}
    ControllerStop
    \\ %
    \refinedby_{FD}
    \\ %
    \mathsl{WaitForSBWaiting}
  \end{block}
  \also %
  \mathbf{assert}\
  \begin{block}
    \mathsl{WaitForSBWaiting}
    \\ %
    \refinedby_{FD}
    \\ %
    ControllerStop
  \end{block}
\]

A complete analysis of the requirements for the initialisation mode is
contained in appendix~\ref{appendix:FDR-code}.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\chapter{Conclusion}

In this report, we have demonstrated a application of \Circus\ to a
sustained case study.  Of particular interest is the architecture of
the solution, where we have separated the rich state and its analysis
from the control logic for the problem.  The result is a CSP process
that is small enough to analyse with FDR, and yet is clearly related
to the problem.

In~\cite{abrial-borger-langmaack-96}, there are some related
solutions.  In particular,~\cite{bussow-weber-96} describe the problem
using a combination of Statecharts~\cite{harel-87, harel-gery-96} and
Z~\cite{spivey-92, woodcock-davies-96}.  As in \Circus, the data
structures and their operations are described in Z, but the reactive
behaviour and proof obligations are quite informal.

Butler, Sekerinski, and Sere~\cite{butler-sekerinski-sere-96} use
action systems~\cite{back-kurki-suonio-83} to specify the steam boiler
and its physical environment as a single system.  In a refinement
step, they separate the two and introduce notions of equipment
failure.

Duvel and Cattel~\cite{duval-cattel-96} specify and verify the steam
boiler using Promela and the SPIN model checker and
simulator~\cite{holzmann-91, holzmann-93, holzmann-95}; they implement
the result in Synchronous C++.  Eight properties were specified in
linear temporal logic and then checked using SPIN.

Ledru and Potet~\cite{ledru-potet-96} use VDM-SL~\cite{jones-90,
  andrews-bruun-hansen-larsen-plat-95} in their solution.  They
develop an abstract specification of the boiler with the safety
property that it will not explode if the water level is kept between
the extreme limits.  This is then refined into an architectural
design.  The main drawback is the lack of support for concurrency in
VDM-SL.  Schinagl~\cite{schinagl-96} overcomes this problem by using
RAISE~\cite{raise-92}, a notation strongly related to VDM, but with
support for concurrency based on CCS~\cite{milner-89} and
CSP~\cite{hoare-85}.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{thebibliography}{XX}

\bibitem{abrial-96-a} J.-R.~Abrial, \emph{The B-Book: Assigning Programs
    to Meanings}, Cambridge University Press, 1996.

\bibitem{abrial-96-b} Jean-Raymond~Abrial, ``Steam-boiler control
  specification problem'', in
  \cite[pp.500-510]{abrial-borger-langmaack-96}.

\bibitem{abrial-borger-langmaack-96} Jean-Raymond Abrial, Egon
  B\"{o}rger, and Hans Langmaack (editors), \emph{Formal Methods for
  Industrial Applications: Specifying and Programming the Steam Boiler
  Control}, \emph{Lecture Notes in Computer Science}, Vol. 1165,
  Springer, 1996.

\bibitem{andrews-bruun-hansen-larsen-plat-95} D.~J.~Andrews H.~Bruun,
  B.~S.~Hansen P.~G.~Larsen, N.~Plat, et al., \emph{Information
  Technology --- Programming Languages, their environments and system
  software interfaces --- Vienna Development Method --- Specification
  Language Part 1: Base Language}, ISO, 1995.

\bibitem{arnold-gosling-96} K.~Arnold and J.~Gosling, \emph{The Java
    Programming Language}, Addison-Wesley, 1996.

\bibitem{back-kurki-suonio-83} R.~J.~R.~Back and R.~Kurki-Suonio,
  ``Decentralization of process nets with centralized control'',
  \emph{Procs 2nd ACM SIGACT-SIGOPS Symposium on Principles of
  Distributed Computing}, pp.131--142, 1983.

\bibitem{bauer-93} J.~C.~Bauer, ``Specification for a software program
  for a boiler water content monitor and control system'', Institute
  of Risk Research, University of Waterloo, 1993.

\bibitem{bussow-weber-96} Robert B\"{u}ssow and Matthias Weber, ``A
  steam-boiler control specification with Statecharts and Z'', in
  \cite[pp.109--128]{abrial-borger-langmaack-96}.

\bibitem{butler-sekerinski-sere-96} Michael Butler, Emil Sekerinski,
  and Kaisa Sere, ``An action system approach to the steam boiler
  problem'', in \cite[pp.129--148]{abrial-borger-langmaack-96}.

\bibitem{cavalcanti-97} Ana Cavalcanti, \emph{A Refinement Calculus
    for Z}, DPhil Thesis, \emph{Technical Monograph PRG-123}, Oxford
    University Computing Laboratory, 1997.

\bibitem{cavalcanti-sampaio-01} A.~L.~C.~Cavalcanti and
  A.~C.~A.~Sampaio, ``From CSP-OZ to Java with processes'', submitted
  to \emph{8th Asia-Pacific Software Engineering Conference (APSEC
    2001)}, 2001.

\bibitem{cavalcanti-woodcock-98} A.~L.~C.~Cavalcanti and
  J.~C.~P.~Woodcock, ``ZRC---A refinement calculus for Z'',
  \textsl{Formal Aspects of Computing}, 10(3): 267--289, 1998.

\bibitem{duval-cattel-96} Gregory Duval and Thierry Cattel,
  ``Specifying and verifying the steam-boiler problem with SPIN'', in
  \cite[pp.203--217]{abrial-borger-langmaack-96}.

\bibitem{embedded-solutions-ltd-99} Embedded Solutions Ltd,
  \emph{\HandelC\ Reference Manual}, 1999.

\bibitem{formal-systems-97} Formal Systems (Europe) Ltd,
  \emph{Failures-Divergences Refinement: FDR2 Manual}, 1997.

\bibitem{harel-87} D.~Harel, ``A visual formalism for complex
  systems'', \emph{Science of Computer Programming}, 8(3):231--274,
  1987.

\bibitem{harel-gery-96} D.~Harel and E.~Gery, ``Executable
  object-modeling with Statecharts'', \emph{Procs International
  Conference of Software Engineering 18}, 1996.

\bibitem{hoare-85} C.~A.~R.~Hoare, \emph{Communicating Sequential
    Processes}, Prentice Hall, 1985.

\bibitem{hoare-he-98} C.~A.~R.~Hoare and He Jifeng, \emph{Unifying
    Theories of Programming}, Prentice Hall, 1998.

\bibitem{holzmann-91} G.~J.~Holzmann, \emph{Design and Validation of
    Computer Protocols}, Prentice Hall, 1991.

\bibitem{holzmann-93} G.~J.~Holzmann, ``Design and validation of
  protocols'': a tutorial, \emph{Computer Networks}, 25(9),
  pp.981--1017, 1993.

\bibitem{holzmann-95} G.~J.~Holzmann, ``What's new in SPIN version
  2'', AT\&TBell Laboratories, May 1995.

\bibitem{inmos-84} \textsf{inmos ltd}, \emph{\textsf{occam}
    Programming Manual}, Prentice Hall, 1984.

\bibitem{jones-90} Cliff~B.~Jones, \emph{Systematic Software
    Development using VDM}, second edition, Prentice Hall, 1990.

\bibitem{ledru-potet-96} Yves Ledru and Marie-Laure Potet, ``A VDM
  specification of the steam-boiler problem'', in
  \cite[pp.283--317]{abrial-borger-langmaack-96}.

\bibitem{meisels-saaltink-97} Irwin Meisels and Mark Saaltink,
  \emph{The Z/Eves Reference Manual}, TR-97-5493-03d, ORA Canada,
  1997.

\bibitem{milner-89} Robin Milner, \emph{Communication and
    Concurrency}, Prentice Hall, 1989.

\bibitem{morgan-94} Carroll Morgan, \emph{Programming from
    Specifications}, second edition, Prentice Hall, 1994.

\bibitem{potter-sinclair-till-91} Ben Potter, Jane Sinclair, and David
  Till, \emph{An Introduction to Formal Specification and Z}, Prentice
  Hall, 1991.

\bibitem{raise-92} The RAISE Language Group, \emph{The RAISE
    Specification Language}, Prentice Hall, 1992.

\bibitem{roscoe-98} A.~W.~Roscoe, \emph{The Theory and Practice of
    Concurrency}, Prentice Hall, 1998

\bibitem{saaltink-97} Mark Saaltink, \emph{The Z/Eves User's Guide},
  TR-97-5493-06, ORA Canada, 1997.

\bibitem{schinagl-96} Christian~P.~Schinagl, ``VDM specification of
  the steam-boiler control using RSL notation'', in
  \cite[pp.428--452]{abrial-borger-langmaack-96}.

\bibitem{spivey-92} J.~M.~Spivey, \emph{The Z Notation: a Reference
    Manual}, second edition, Prentice Hall, 1992.

\bibitem{spivey-88} J.~M.~Spivey, \emph{Understanding Z: a
    specification language and its formal semantics}, Cambridge
  University Press, 1999.

\bibitem{spivey-95} Mike Spivey, \emph{The} \fuzz\ \emph{Manual}, second
  edition, The Spivey Partnership, Oxford, 1995.

\bibitem{woodcock-cavalcanti-01} Jim~Woodcock and Ana Cavalcanti,
  ``\Circus: a language for concurrent refinement'', \emph{working
    paper}, University of Oxford and Federal University of Pernambuco,
  2001.

\bibitem{woodcock-davies-96} Jim~Woodcock and Jim~Davies, \emph{Using
    Z: Specification, Refinement, and Proof}, Prentice Hall, 1996.

\end{thebibliography}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\appendix

\chapter{Requirements for the program's modes}
\label{appendix:requirements}

\section{\emph{Initialisation} mode}

The \emph{initialisation} mode is the mode to start with.  The program
enters a state in which it waits for the message STEAM-BOILER\_WAITING
to come from the physical units.  As soon as this message has been
received the program checks whether the quantity of steam coming out
of the steam-boiler is really zero.  If the unit for detection of the
level of the steam is defective---that is, when \( v \)\/ is not equal
to zero---the program enters the \emph{emergency-stop} mode.  If the
quantity of water in the steam-boiler is above \( N_2 \)\/ the program
activates the valve of the steam-boiler in order to empty it.  If the
quantity of water in the steam-boiler is below \( N_1 \)\/ then the
program activates a pump to fill the steam-boiler.  If the program
realizes a failure of the water level detection unit it enters the
\emph{emergency-stop} mode.  As soon as a level of water between \(
N_1 \)\/ and \( N_2 \)\/ has been reached the program can send
continuously the signal PROGRAM\_READY to the physical units until it
receives the signal PHYSICAL\_UNITS\_READY which must necessarily be
emitted by the physical units.  As soon as this signal has been
received, the program enters either the mode \emph{normal} if all the
physical units operate correctly or the mode \emph{degraded} if any
physical unit is defective.  A transmission failure puts the program
into the mode \emph{emergency stop}.

\section{\emph{Normal} mode}

The normal mode is the standard operating mode in which the program
tries to maintain the water level in the steam-boiler between \(N_1
\)\/ and \( N_2 \)\/ with all physical units operating correctly.  As
soon as the water level is below \( N_1 \)\/ or above \( N_2 \)\/ the
level can be adjusted by the program by switching the pumps on or off.
The corresponding decision is taken on the basis of the information
which has been received from the physical units.  As soon as the
program recognizes a failure of the water level measuring unit it goes
into \emph{degraded} mode.  If the water level is risking to reach one
of the limit values \( M_1 \)\/ or \( M_2 \)\/ the program enters the
mode \emph{emergency stop}.  This risk is evaluated on the basis of a
maximal behaviour of the physical units.  A transmission failure puts
the program into \emph{emergency stop} mode.

\section{\emph{Degraded} mode}

The \emph{degraded} mode is the mode in which the program tries to
maintain a satisfactory water level despite the presence of failure of
some physical unit.  It is assumed however that the water level
measuring unit in the steam-boiler is working correctly.  The
functionality is the same as the preceding case.  Once all the units
which were defective have been repaired, the program comes back to
\emph{normal} mode.  As soon as the program sees that the water level
is risking to reach one of the limit values \( M_1 \)\/ or \( M_2 \)\/
the program enters the mode \emph{emergency stop}.  A transmission
failure puts the program into \emph{emergency stop} mode.

\section{\emph{Rescue} mode}

The \emph{rescue} mode is the mode in which the program tries to
maintain a satisfactory water level despite of the failure of the
water level measuring unit.  The water level is then estimated by a
computation which is done taking into account the maximum dynamics of
the quantity of steam coming out of the steam-boiler.  For the sake of
simplicity, this calculation can suppose that exactly \( n \)\/ liters
of water, supplied by the pumps, do account for exactly the same
amount of boiler contents (no thermal expansion).  This calculation
can however be done only if the unit which measures the quantity of
steam is itself working and if one can rely upon the information which
comes from the units for controlling the pumps .  As soon as the water
measuring unit is repaired, the program returns into mode
\emph{degraded} or into mode \emph{normal}.  The program goes into
\emph{emergency stop} mode if it realizes that one of the following
cases holds: the unit which measures the outcome of steam has a
failure, or the units which control the pumps have a failure, or the
water level risks to reach one of the two limit values.  A
transmission failure puts the program into \emph{emergency stop} mode.

\section{\emph{Emergency stop} mode}

The \emph{emergency stop} mode is the mode into which the program has
to go, as we have seen already, when either the vital units have a
failure or when the water level risks to reach one of its two limit
values.  This mode can also be reached after detection of an
erroneous transmission between the program and the physical units.
This mode can also be set directly from outside.  Once the program has
reached the \emph{emergency stop} mode, the physical environment is
then responsible to take appropriate actions, and the program stops.


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\chapter{FDR code}
\label{appendix:FDR-code}

\begin{verbatim}
----------------------------------------------------------------------
-- Abstract steam-boiler code
--
-- checked with FDR 2.78: 15.10 14.6.01
----------------------------------------------------------------------

datatype Mode = initialisation | normal | degraded | rescue |
                emergencyStop

NonEmergencyModes = { initialisation, normal, degraded, rescue }

channel getmode, putmode: Mode

ModeStateInterface = {| getmode, putmode |}

ModeState =
  let
    MS(m) = putmode?n -> MS(n)
            []
            getmode!m -> MS(m)
  within
    MS(initialisation)

EnterMode(m) = reportmode!m -> putmode!m -> SKIP

channel ainfo, areport, clocktick, endcycle, endreport,
        afailuresrepairs, ainput, apumps, startcycle, startexec,
        startreport

channel aoutput, reportmode : Mode

TAnalyserInterface = { startcycle }

TAControllerInterface1 = { ainfo, startexec }

TACReporterInterface1 =
  {| apumps, areport, endreport, afailuresrepairs, reportmode,
     startreport |}

cycletime = 5

cyclelimit = cycletime - 1

Time = { 0 .. cyclelimit }

TCycle(time) =
  ( if ( time + 1 ) % cycletime == 0 then startcycle -> SKIP else SKIP);
  clocktick -> TCycle(( time + 1 ) % cycletime)

Timer = TCycle(cyclelimit)

Analyser1 = startcycle -> ainput -> startexec -> InfoService1

InfoService1 =
  ainfo -> InfoService1
  []
  afailuresrepairs -> apumps -> Analyser1

TAnalyser1 =
  ( Timer [| TAnalyserInterface |] Analyser1 ) \ TAnalyserInterface

assert TAnalyser1 :[  deadlock free  [FD] ]

assert TAnalyser1 :[  livelock free  [FD] ]

Controller1 =
  startexec ->
    startreport ->
      NewModeAnalysis1;
      getmode?m ->
        ( if m != emergencyStop then
             |~|i: { 0 .. limit } @ PutReports(i)
          else SKIP );
        endreport -> Controller1

NewModeAnalysis1 =
  ainfo -> EnterMode(emergencyStop)
  |~|
  (
    ( |~| i: { 0 .. limit } @ GetInformation(i) );
    getmode?mode ->
      if mode == initialisation then InitModeAnalysis1
      else if mode == normal then NormalModeAnalysis1
      else if mode == degraded then DegradedModeAnalysis1
      else if mode == rescue then RescueModeAnalysis1
      else SKIP
    )

InitModeAnalysis1 =
  SKIP |~| EnterMode(normal) |~| EnterMode(degraded) |~|
    EnterMode(emergencyStop)

NormalModeAnalysis1 =
  SKIP |~| EnterMode(rescue) |~| EnterMode(degraded)

DegradedModeAnalysis1 =
  SKIP |~| EnterMode(normal) |~| EnterMode(rescue)

RescueModeAnalysis1 =
  SKIP |~| EnterMode(normal) |~| EnterMode(degraded)

limit = 8

Get(event,n) = if n > 0 then event -> Get(event,n-1) else SKIP

GetInformation(n) = Get(ainfo,n)

PutReports(n) = Get(areport,n)

TAController1 =
  ( TAnalyser1
    [| TAControllerInterface1 |]
    ( Controller1
      [| ModeStateInterface |]
      ModeState
    ) \ ModeStateInterface
  ) \ TAControllerInterface1

assert TAController1 :[  livelock free  [FD] ]

Reporter1 = startreport -> ReportService1

ReportService1 =
  [] m: NonEmergencyModes @ reportmode.m -> putmode!m -> ReportService1
  []
  areport -> ReportService1
  []
  reportmode.emergencyStop ->
    putmode!emergencyStop ->
      TidyUp1
  []
  TidyUp1

TidyUp1 =
  endreport ->
    afailuresrepairs ->
      getmode?m ->
        aoutput!m ->
          apumps ->
            Reporter1

TACReporter1 =
  ( TAController1
     [| TACReporterInterface1 |]
    (
      ( Reporter1
         [| ModeStateInterface |]
        ModeState
      ) \ ModeStateInterface
    )
  ) \ TACReporterInterface1

assert TACReporter1 :[  deadlock free  [FD] ]

assert TACReporter1 :[  livelock free  [FD] ]

SteamBoiler1 = TACReporter1

























----------------------------------------------------------------------
-- Analyser
----------------------------------------------------------------------

channel levelbelowmin, levelabovemax

channel emergencystop, failures, levelokay, nonqfailure,
        physicalunitsready, qfailure, sbwaiting, vzero: Bool

Analyser = AnalyserCycle

AnalyserCycle = startcycle -> ainput -> startexec -> InfoService

InfoService =
  OfferInformation; InfoService
  []
  afailuresrepairs ->
    apumps ->
      AnalyserCycle

OfferInformation =
  ( |~| b: Bool @ emergencystop.b -> SKIP )
  []
  ( |~| b: Bool @ sbwaiting.b -> SKIP )
  []
  ( |~| b: Bool @ vzero.b -> SKIP )
  []
  ( levelokay.true -> SKIP
    |~|
    ( levelokay.false -> SKIP
      []
      ( levelabovemax -> SKIP
        |~|
        levelbelowmin -> SKIP
      )
    )
  )
  []
  ( |~| b: Bool @ physicalunitsready.b -> SKIP )
  []
  ( ( failures.false -> SKIP
      []
      qfailure.false -> SKIP
      []
      nonqfailure.false -> SKIP
    )
    |~|
    ( failures.true -> SKIP
      []
      ( ( qfailure.true -> SKIP
          []
          nonqfailure.true -> SKIP
        )
        |~|
        ( qfailure.true -> SKIP
          []
          nonqfailure.false -> SKIP
        )
        |~|
        ( qfailure.false -> SKIP
          []
          nonqfailure.true -> SKIP
        )
      )
    )
  )

TAnalyser =
  ( Timer
    [| TAnalyserInterface |]
    Analyser
  ) \ TAnalyserInterface

assert TAnalyser :[ deadlock free [FD] ]

assert TAnalyser :[ livelock free [FD] ]

AbsAnalyser =
  Analyser
    [[ e <- ainfo,
       c.b <- ainfo
     |
       e <- { levelbelowmin, levelabovemax },
       b <- Bool,
       c <- { emergencystop,
              failures,
              levelokay,
              nonqfailure,
              physicalunitsready,
              qfailure,
              sbwaiting,
              vzero
            }
    ]]

AbsTAnalyser =
  TAnalyser
    [[ e <- ainfo,
       c.b <- ainfo
     |
       e <- { levelbelowmin, levelabovemax },
       b <- Bool,
       c <- { emergencystop,
              failures,
              levelokay,
              nonqfailure,
              physicalunitsready,
              qfailure,
              sbwaiting,
              vzero
            }
    ]]

assert Analyser1 [FD= AbsAnalyser

assert TAnalyser1 [FD= AbsTAnalyser































----------------------------------------------------------------------
-- Controller
----------------------------------------------------------------------

channel startpumps, stoppumps, openvalve, closevalve, sendprogready

Information =
  {| emergencystop, failures, levelabovemax, levelbelowmin, levelokay,
     nonqfailure, physicalunitsready, qfailure, sbwaiting, vzero |}

Reports =
  { startpumps, stoppumps, openvalve, closevalve, sendprogready }

TAControllerInterface = union( { startexec }, Information )

Controller = ControllerCycle

ControllerCycle =
  startexec -> startreport -> NewModeAnalysis;
  AdjustLevel;
  endreport -> ControllerCycle

NewModeAnalysis =
  emergencystop.true -> EnterMode(emergencyStop)
  []
  emergencystop.false ->
    getmode?mode ->
      if mode == initialisation then InitModeAnalysis
      else if mode == normal then NormalModeAnalysis
      else if mode == degraded then DegradedModeAnalysis
      else if mode == rescue then RescueModeAnalysis
      else SKIP

InitModeAnalysis =
  sbwaiting.true ->
    ( vzero.true ->
        ( qfailure.false ->
            ( physicalunitsready.true ->
                ( levelokay.true ->
                    ( failures.false -> EnterMode(normal)
                      []
                      failures.true -> EnterMode(degraded)
                    )
                  []
                  levelokay.false -> EnterMode(emergencyStop)
                )
              []
              physicalunitsready.false ->
                ( levelokay.true -> sendprogready -> SKIP
                  []
                  levelokay.false -> SKIP
                )
            )
          []
          qfailure.true -> EnterMode(emergencyStop)
        )
      []
      vzero.false -> EnterMode(emergencyStop)
    )
  []
  sbwaiting.false -> SKIP

NormalModeAnalysis =
  failures.false -> SKIP
  []
  qfailure.true -> EnterMode(rescue)
  []
  nonqfailure.true -> EnterMode(degraded)

DegradedModeAnalysis =
  qfailure.false ->
    ( failures.true -> SKIP
      []
      failures.false -> EnterMode(normal)
    )
  []
  qfailure.true -> EnterMode(rescue)

RescueModeAnalysis =
  qfailure.true -> SKIP
  []
  qfailure.false ->
    ( failures.false -> EnterMode(normal)
      []
      failures.true -> EnterMode(degraded)
    )

AdjustLevel =
  getmode?m ->
    if m == emergencyStop then SKIP
    else
      levelbelowmin -> RaiseLevel
      []
      levelabovemax -> ReduceLevel
      []
      levelokay.true -> RetainLevel

RaiseLevel =
  StartPumps;
  getmode?mode ->
    if mode == initialisation then CloseValve else SKIP

ReduceLevel =
  StopPumps;
  getmode?mode ->
    if mode == initialisation then OpenValve else SKIP

RetainLevel =
  StopPumps;
  getmode?mode ->
    if mode == initialisation then CloseValve else SKIP

StartPumps = startpumps -> SKIP

StopPumps = stoppumps -> SKIP

OpenValve = openvalve -> SKIP

CloseValve = closevalve -> SKIP

MSController =
  ( Controller
    [| ModeStateInterface |]
    ModeState
  ) \ ModeStateInterface

assert MSController :[ deadlock free [FD] ]

assert MSController :[ livelock free [FD] ]


TAController =
  ( TAnalyser
    [| TAControllerInterface |]
    MSController
  ) \ TAControllerInterface

AbsTAController =
  TAController
    [[ f <- areport
     |
       f <- { startpumps, stoppumps, openvalve, closevalve,
              sendprogready }
    ]]



----------------------------------------------------------------------
-- Reporter
----------------------------------------------------------------------

TACReporterInterface =
  union( {| startreport, reportmode, endreport, afailuresrepairs,
            apumps |}, Reports )

Reporter = startreport -> ReportService

ReportService =
  GatherReports; ReportService
  []
  reportmode.emergencyStop ->
    putmode!emergencyStop ->
      endreport ->
        TidyUp
  []
  endreport -> TidyUp

TidyUp =
  afailuresrepairs ->
    getmode?m ->
      aoutput!m ->
        apumps ->
          Reporter

GatherReports =
  [] m: NonEmergencyModes @ reportmode.m -> putmode!m -> SKIP
  []
  sendprogready -> SKIP
  []
  startpumps -> SKIP
  []
  stoppumps -> SKIP
  []
  openvalve -> SKIP
  []
  closevalve -> SKIP

TACReporter =
  ( TAController
    [| TACReporterInterface |]
    ( ( Reporter
        [| ModeStateInterface |]
        ModeState
      ) \ ModeStateInterface
    )
  ) \ TACReporterInterface

assert TACReporter :[ deadlock free [FD] ]

assert TACReporter :[ livelock free [FD] ]

assert TACReporter1 [FD= TACReporter











































----------------------------------------------------------------------
-- Requirements checks
----------------------------------------------------------------------

-- In the initialisation mode, the program waits for the steam-boiler
-- waiting message.

WaitForSBWaiting =
  startexec ->
    startreport ->
      emergencystop.false ->
        sbwaiting.false ->
          levelokay.true ->
            stoppumps ->
              closevalve ->
                endreport ->
                  WaitForSBWaiting

assert ( MSController
         [| { levelabovemax, levelbelowmin, sbwaiting.true,
              emergencystop.true } |]
         STOP
       )
       [FD=
       WaitForSBWaiting

assert WaitForSBWaiting
       [FD=
       ( MSController
         [| { levelabovemax, levelbelowmin, sbwaiting.true,
              emergencystop.true } |]
         STOP
        )
















-- As soon as the sbwaiting message has been received, the controller
-- checks to see if the quantity of steam coming out of the boiler
-- really is zero; if it isn't, then it enters emergency stop.

alphaMoveToSBWaiting =
  { startexec, emergencystop.false, sbwaiting.true }

MoveToSBWaiting =
  startexec ->
    startreport ->
      emergencystop.false ->
        sbwaiting.true ->
          SKIP

RUN(s) =
  let
    R = [] x: s @ x -> R
  within
    R

alphaMSC =
  union( Information,
    union( Reports,
      { startexec, startreport, endreport }
    )
  )

CheckSteamRateIsZero =
  MoveToSBWaiting;
  vzero.false ->
    reportmode!emergencyStop ->
      endreport ->
        Idle

Idle =
  startexec -> startreport -> emergencystop.false -> endreport -> Idle

assert ( MSController
         [| { emergencystop.true, sbwaiting.false, vzero.true } |]
         STOP )
       [FD=
       CheckSteamRateIsZero

assert CheckSteamRateIsZero
       [FD=
       ( MSController
         [| { emergencystop.true, sbwaiting.false, vzero.true } |]
         STOP )

-- If the quantity of water in the steam boiler is above N2, then it
-- activates the valve in order to empty it.

alphaMoveToRateZero =
  union( alphaMoveToSBWaiting, { vzero.true } )

MoveToRateZero = MoveToSBWaiting; vzero.true -> SKIP

alphaMoveToPhysicalUnitsNotReady =
  union( alphaMoveToRateZero,
         { qfailure.false, physicalunitsready.false } )

MoveToPhysicalUnitsNotReady =
  MoveToRateZero;
  qfailure.false ->
    physicalunitsready.false ->
      SKIP

alphaMoveToPhysicalUnitsNotReadyLevelAboveMax =
  union( alphaMoveToPhysicalUnitsNotReady,
         { levelokay.false, levelabovemax } )

MoveToPhysicalUnitsNotReadyLevelAboveMax =
  MoveToPhysicalUnitsNotReady;
    levelokay.false ->
      levelabovemax ->
        SKIP

TestLevelAboveMaxStopPumpsOpenValve =
  MoveToPhysicalUnitsNotReadyLevelAboveMax;
  stoppumps ->
    openvalve ->
      CHAOS(alphaMSC)

alphaTest1 =
  union( alphaMoveToPhysicalUnitsNotReadyLevelAboveMax,
         { emergencystop.true,
           sbwaiting.false,
           vzero.false,
           qfailure.true,
           physicalunitsready.true,
           levelokay.true,
           levelbelowmin,
           startreport } )

assert TestLevelAboveMaxStopPumpsOpenValve
       [FD=
       ( MSController
         [| alphaTest1 |]
         MoveToPhysicalUnitsNotReadyLevelAboveMax
       )















































-- If the quantity of water in the steam boiler is below N1, then it
-- activates the pumps to fill it.

CheckInitBelowN1 =
  MoveToPhysicalUnitsNotReady;
    levelokay.false ->
      levelbelowmin ->
        startpumps ->
           closevalve ->
             STOP

assert MSController [T= CheckInitBelowN1

alphaMoveToPhysicalUnitsNotReadyLevelBelowMin =
  union( alphaMoveToPhysicalUnitsNotReady,
         { levelokay.false, levelbelowmin } )

MoveToPhysicalUnitsNotReadyLevelBelowMin =
  MoveToPhysicalUnitsNotReady;
  levelokay.false ->
    levelbelowmin ->
      SKIP

TestLevelBelowMinStartPumpsCloseValve =
  MoveToPhysicalUnitsNotReadyLevelBelowMin;
  startpumps ->
    closevalve ->
      CHAOS(alphaMSC)

alphaTest2 =
  union( alphaMoveToPhysicalUnitsNotReadyLevelBelowMin,
         { emergencystop.true,
           sbwaiting.false,
           vzero.false,
           qfailure.true,
           physicalunitsready.true,
           levelokay.true,
           levelabovemax,
           startreport } )

assert TestLevelBelowMinStartPumpsCloseValve
       [FD=
       ( MSController
         [| alphaTest2 |]
         MoveToPhysicalUnitsNotReadyLevelBelowMin
       )



-- If the program realises a failure of the water level detection unit
-- it enters the emergency stop mode.

alphaTest3 =
  union( alphaMoveToRateZero,
         { emergencystop.true,
           sbwaiting.false,
           vzero.false,
           qfailure.false,
           startreport
           } )

TestWaterLevelFailureEmergencyStop =
  MoveToRateZero;
  qfailure.true ->
    reportmode.emergencyStop ->
      CHAOS(alphaMSC)

assert TestWaterLevelFailureEmergencyStop
       [FD=
       ( MSController
         [| alphaTest3 |]
         MoveToRateZero
       )

























-- As soon as a level between N1 and N2 has been reached, the program
-- can send continuously the signal sendprogready until it receives
-- the signal physicalunitsready.true.


alphaTest4 =
  { physicalunitsready.true, emergencystop.true, sbwaiting.false,
    vzero.false, qfailure.true, levelokay.false, levelabovemax,
    levelbelowmin }

TestLevelInRangeSendProgReady =
  startexec ->
    startreport ->
      emergencystop.false ->
        sbwaiting.true ->
          vzero.true ->
            qfailure.false ->
              physicalunitsready.false ->
                levelokay.true ->
                  sendprogready ->
                    levelokay.true ->
                      stoppumps ->
                        closevalve ->
                          endreport ->
                            TestLevelInRangeSendProgReady

assert TestLevelInRangeSendProgReady
       [FD=
       ( MSController
         [| alphaTest4 |]
         STOP
       )

assert ( MSController
         [| alphaTest4 |]
         STOP
       )
       [FD=
       TestLevelInRangeSendProgReady










-- As soon as [physicalunitsready.true] signal has been received, the
-- program enters either the mode normal, if all the physical units
-- operate correctly, or the mode degraded, if any physical unit is
-- defective.

WaitForPhysicalUnitsReadyNoFailures =
  RUN(diff(alphaMSC,{physicalunitsready.true, emergencystop.true,
                     vzero.false, qfailure.true}))

InsistOnNormal =
  WaitForPhysicalUnitsReadyNoFailures
  []
  physicalunitsready.true ->
    levelokay.true ->
      failures.false ->
        reportmode.normal -> RUN(alphaMSC)

assert MSController
       [| alphaMSC |]
       InsistOnNormal :[ deadlock free [FD] ]

WaitForPhysicalUnitsReadyFailures =
  RUN(diff(alphaMSC,{physicalunitsready.true, emergencystop.true,
                     vzero.false, qfailure.true}))

InsistOnDegraded =
  WaitForPhysicalUnitsReadyFailures
  []
  physicalunitsready.true ->
    levelokay.true ->
      failures.true ->
        reportmode.degraded -> RUN(alphaMSC)

assert MSController
       [| alphaMSC |]
       InsistOnDegraded :[ deadlock free [FD] ]
\end{verbatim}

\end{document}

% LocalWords:  AcceptFailureAcks
% LocalWords:  AcceptRepairs
% LocalWords:  AdjustStops
% LocalWords:  AllPhysicalUnitsOkay
% LocalWords:  AnalyserState
% LocalWords:  CValues
% LocalWords:  CheckAndAdjustPump
% LocalWords:  CheckAndAdjustQ
% LocalWords:  CheckAndAdjustSensor
% LocalWords:  CheckAndAdjustV
% LocalWords:  DangerZone
% LocalWords:  EmergencyStopCond
% LocalWords:  EquipmentFailures
% LocalWords:  ExpectedPumpStates
% LocalWords:  FailuresExpected
% LocalWords:  InitAnalyserState
% LocalWords:  InitCValues
% LocalWords:  InitEquipment
% LocalWords:  InitFailures
% LocalWords:  InitPump
% LocalWords:  InitPumpCtr
% LocalWords:  InitPumpCtrSystem
% LocalWords:  InitQSensor
% LocalWords:  InitVSensor
% LocalWords:  InitValve
% LocalWords:  InputMsg
% LocalWords:  InputPCState
% LocalWords:  InputPState
% LocalWords:  InputSignal
% LocalWords:  LevelAboveMax
% LocalWords:  LevelBelowMin
% LocalWords:  LevelInRange
% LocalWords:  ModeState
% LocalWords:  OtherPhysicalUnitsFail
% LocalWords:  OutputMsg
% LocalWords:  OutputSignal
% LocalWords:  PCFailed
% LocalWords:  PCState
% LocalWords:  PClosedPCFailed
% LocalWords:  PClosedPCNoFlow
% LocalWords:  PFailed
% LocalWords:  PFailedPCFailed
% LocalWords:  PFailedPCFlow
% LocalWords:  PFailedPCNoFlow
% LocalWords:  POpenPCFailed
% LocalWords:  POpenPCFlow
% LocalWords:  PState
% LocalWords:  PWaitingPCFailed
% LocalWords:  PWaitingPCNoFlow
% LocalWords:  PhysicalUnitsReady
% LocalWords:  PromotePumpCheck
% LocalWords:  PumpClosed
% LocalWords:  PumpCtr
% LocalWords:  PumpCtrSystem
% LocalWords:  PumpIndex
% LocalWords:  PumpOp
% LocalWords:  PumpOpen
% LocalWords:  PumpWaiting
% LocalWords:  QExpected
% LocalWords:  QFailed
% LocalWords:  QLowerBoundValveClosed
% LocalWords:  QLowerBoundValveOpen
% LocalWords:  QSensor
% LocalWords:  QUnexpected
% LocalWords:  QUpperBound
% LocalWords:  RateZero
% LocalWords:  RepairsExpected
% LocalWords:  SState
% LocalWords:  SetPumpCtr
% LocalWords:  SteamBoilerWaiting
% LocalWords:  StopNotPresent
% LocalWords:  StopPresent
% LocalWords:  TimeState
% LocalWords:  TooManyStops
% LocalWords:  UnitFailure
% LocalWords:  UnitState
% LocalWords:  VExpected
% LocalWords:  VFailed
% LocalWords:  VLowerBound
% LocalWords:  VSensor
% LocalWords:  VState
% LocalWords:  VUnexpected
% LocalWords:  VUpperBound
% LocalWords:  afailuresrepairs
% LocalWords:  ainfo
% LocalWords:  ainput
% LocalWords:  aoutput
% LocalWords:  apumps
% LocalWords:  areport
% LocalWords:  closePump
% LocalWords:  cyclelimit
% LocalWords:  cycletime
% LocalWords:  emergencystop
% LocalWords:  endreport
% LocalWords:  expectedPC
% LocalWords:  expectedp
% LocalWords:  expectedpc
% LocalWords:  exppcst
% LocalWords:  exppst
% LocalWords:  failureacks
% LocalWords:  failureacks
% LocalWords:  infoservice
% LocalWords:  noacks
% LocalWords:  noacks
% LocalWords:  openPump
% LocalWords:  pcst
% LocalWords:  pst
% LocalWords:  pumpCtrFailureDetection
% LocalWords:  pumpCtrRepairedAcknowledgement
% LocalWords:  pumpCtrState
% LocalWords:  pumpFailureDetection
% LocalWords:  pumpRepairedAcknowledgement
% LocalWords:  pumpState
% LocalWords:  pumpctr
% LocalWords:  qa
% LocalWords:  qc
% LocalWords:  qc
% LocalWords:  qst
% LocalWords:  reportmode
% LocalWords:  reportservice
% LocalWords:  sbwaiting
% LocalWords:  signalhistory
% LocalWords:  startcycle
% LocalWords:  startexec
% LocalWords:  startinput
% LocalWords:  startreport
% LocalWords:  va
% LocalWords:  vc
% LocalWords:  vc
% LocalWords:  vst

\end{document}
