Language.tex

\section{Language}~\label{sec:language}

Copilot is embedded into the functional programming language Haskell
\cite{PeytonJones02}, and a working knowledge of Haskell is necessary to use
Copilot effectively. Copilot is a pure declarative language; i.e., expressions
are free of side-effects and are referentially transparent.  A program written
in Copilot, which from now on will be referred to as a \emph{specification}, has
a cyclic behavior, where each cycle consists of a fixed series of steps:

\begin{itemize}
\item Sample external variables and arrays.
\item Update internal variables.
\item Fire external triggers. (In case the specification is violated.)
\item Update observers (for debugging purpose).
\end{itemize}

\noindent We refer to a single cycle as an \emph{iteration} or a \emph{step}.

All transformation of data in Copilot is propagated through streams.
A stream is an infinite, ordered sequence of values which must conform to the same type.
E.g., we have the stream of Fibonacci numbers:

\begin{center}
$s_{fib} = \{0, 1, 1, 2, 3, 5, 8, 13, 21, \dots \}$
\end{center}

\noindent We denote the $n$th value of the stream $s$ as $s(n)$, and the first
value in a sequence $s$ as $s(0)$. For example, for $s_{fib}$ we have that $s_{fib}(0) = 0$,
$s_{fib}(1) = 1$, $s_{fib}(2) = 1$, and so forth.

Constants as well as arithmetic, boolean, and relational operators are
lifted to work pointwise on streams:

\noindent
%\begin{minipage}{0.3\textwidth}
\begin{lstlisting}[language = Copilot, frame = single]
x :: Stream Int32
x = 5 + 5

y :: Stream Int32
y = x * x

z :: Stream Bool
z = x == 10 && y < 200
\end{lstlisting}
%\end{minipage}


\noindent Here the streams {\tt x}, {\tt y}, and {\tt z} are simply
\emph{constant streams}:

\begin{center}
$\mathtt{x} \leadsto \{10, 10, 10, \dots \}$,
$\mathtt{y} \leadsto \{100, 100, 100,  \dots \}$,
$\mathtt{z} \leadsto \{\mbox{T},\; \mbox{T},\; \mbox{T},\; \dots \}$
\end{center}

Two types of \emph{temporal} operators are provided, one for delaying streams and one for
looking into the future of streams:
%
\begin{lstlisting}[language = Copilot, frame = single]
(++) :: [a] -> Stream a -> Stream a
drop :: Int -> Stream a -> Stream a
\end{lstlisting}
%
Here {\tt xs ++ s} prepends the list {\tt xs} at the front of the stream {\tt s}.
For example the stream {\tt w} defined as follows, given our previous definition
of {\tt x}:
%
\begin{lstlisting}[language = Copilot, frame = single]
w = [5,6,7] ++ x
\end{lstlisting}
%
evaluates to the sequence
$\mathtt{w} \leadsto \{5, 6, 7, 10, 10, 10, \dots\}$.
The expression {\tt drop k s} skips the first {\tt k} values of the stream {\tt
  s}, returning the remainder of the stream.
For example we can skip the first two values of {\tt w}:
%
\begin{lstlisting}[language = Copilot, frame = single]
u = drop 2 w
\end{lstlisting}
%
which yields the sequence
$\mathtt{u} \leadsto \{7, 10, 10, 10, \dots\}$.

\subsection{Streams as Lazy-Lists} \label{sec:stream}

A key design choice in Copilot is that streams should mimic \emph{lazy lists}.
In Haskell, the lazy-list of natural numbers can be programmed like this:
%
\begin{lstlisting}[language = Copilot, frame = single]
nats_ll :: [Int32]
nats_ll = [0] ++ zipWith (+) (repeat 1) nats_ll
\end{lstlisting}
%
As both constants and arithmetic operators are lifted to work pointwise on
streams in Copilot, there is no need for {\tt zipWith} and {\tt repeat} when
specifying the stream of natural numbers:
%
\begin{lstlisting}[language = Copilot, frame = single]
nats :: Stream Int32
nats = [0] ++ (1 + nats)
\end{lstlisting}
%
In the same manner, the lazy-list of Fibonacci numbers can be specified  in Haskell as follows:
%
\begin{lstlisting}[language = Copilot, frame = single]
fib_ll :: [Int32]
fib_ll = [1, 1] ++ zipWith (+) fib_ll (drop 1 fib_ll)
\end{lstlisting}
%
In Copilot we simply throw away {\tt zipWith}:
\begin{lstlisting}[language = Copilot, frame = single]
fib :: Stream Int32
fib = [1, 1] ++ (fib + drop 1 fib)
\end{lstlisting}

Copilot specifications must be \emph{causal}, informally meaning that
stream values cannot depend on future values.  For example, the following stream
definition is allowed:
%
\begin{lstlisting}[language = Copilot, frame = single]
f :: Stream Word64
f = [0,1,2] ++ f

g :: Stream Word64
g = drop 2 f
\end{lstlisting}
%

But if instead {\tt g} is defined as {\tt g = drop 4 f}, then the definition is
disallowed.  While an analogous stream is definable in a lazy language, we bar
it in Copilot, since it requires future values of {\tt f} to be
generated before producing values for {\tt g}.  This is not possible since
Copilot programs may take inputs in real-time from the environment (see
Section~\ref{subsec:interacting}).


\subsection{Structs}
Structs require some special attentation in Copilot, as we cannot magically
import the definition of the struct in Copilot. In this section we discuss the
steps that need to be taken by following the code of \texttt{Struct.hs} in the
\texttt{Examples} directory of the Copilot distribution, or the repository
\footnote{\url{https://github.com/Copilot-Language/Copilot/blob/master/Examples/Struct.hs}}.

Let's assume that we have defined a 2d-vector type in our C code:
\begin{lstlisting}
struct vec {
	float x;
	float y;
};
\end{lstlisting}
For us to be able to use this vector inside Copilot, we need to follow a number
of steps:
\begin{enumerate}
  \item Enable \texttt{DataKinds} compiler extension.
  \item Define a datatype to mimic the C definition.
  \item Write an instance of the \texttt{Struct} class, containing a definition
  for the struct name and function to translate the fields to a heterogeneous
    list.
  \item Write an instance of the \texttt{Typed} class.
\end{enumerate}

\subsubsection*{Enabling compiler extensions}
First and foremost, we need to enable the \texttt{DataKinds} extension to GHC,
by putting:
\begin{lstlisting}[language=Copilot]
{-# LANGUAGE DataKinds #-}
\end{lstlisting}
at the top of our specification file. This allows us to define \emph{kinds},
which are the types of types. Our datatype needs to carry the names of the
fields in C as well. Using the \texttt{DataKinds} extension we are able to
write the names of the fields as part of our types.


\subsubsection*{Defining the datatype}
A suitable representation of structs in Haskell is provided by the
\emph{record-syntax}, this allows us to use named fields as part of the
datatype. For Copilot this is not enough though: we still need to define the
names of the fields in our C code. Therefore we introduce new \texttt{Field}
datatype, which takes two arguments: the name of field, and it's type. Now we
can mimic our vector struct in Copilot as follows:
\begin{lstlisting}[language=Copilot]
data Vec = Vec
  { x :: Field "x" Float
  , y :: Field "y" Float
  }
\end{lstlisting}
Here we created two fields, $x$ and $y$, each with their corresponding C names
and types. Note that the name inside Haskell and the C names do not necessarily
need to match, nor is it always possible to have them match. For type-safety,
inside Copilot we will typically only use the Haskell level names (i.e. the
unquoted ones). The C names are only used by Copilot internally.


\subsubsection*{Instance of \texttt{Struct}}
Our next task is to inform Copilot about our new type, therefore we need to
write and instance of the \texttt{Struct}-class. This class has the purpose of
defining the datatype as a struct, it provides the code generator of Copilot the
name of struct in C, and provides a function to translate the struct to a list
of values:
\begin{lstlisting}[language=Copilot]
instance Struct Vec where
  -- typename :: Vec -> String
  typename _ = "vec"  -- Name of the type in C

  -- Function to translate Vec to list of Value's, order should match struct.
  -- tovalues :: Vec -> [Value Vec]
  toValues v = [ Value Float (x v)
               , Value Float (y v)
               ]
\end{lstlisting}
Both definitions should be pretty self-explanatory. Note however that
\texttt{Value a} is a wrapper around the \texttt{Field} datatype to hide the
actual type of \texttt{Field}. It takes the type of the field, and the field
itself as its arguments. The elements in the list should be in the same order
as the fields in the struct.

Both \texttt{typename} and \texttt{toValues} have to be defined by the user,
but neither should ever be used by the user. Both functions are only used by
the code generator of Copilot.


\subsubsection*{Instance of \texttt{Typed}}
In Copilot, streams can only of types that are instances of the \texttt{Typed}
class. To be able to create streams of vectors, \texttt{Vec} needs to be an
instance of \texttt{Typed} as well. The class only provides a \texttt{typeOf}
function, returning the type:
\begin{lstlisting}[language=Copilot]
instance Typed Vec where
  typeOf = Struct (Vec (Field 0) (Field 0))
\end{lstlisting}
For \texttt{Vec} this means we need to return something of the \texttt{Vec}
type wrapped in the \texttt{Struct} constructor. In this case it does not
matter what the values of the fields are, we just need to return something of
the correct type.


\subsubsection*{Simple operations}
Building streams of structs works like building any other stream, but we need
to wrap the values of a struct using the \texttt{Field} constructor. The reason
for this is quite straightforward: the fields of our struct are defined in
terms of \texttt{Field}:
\begin{lstlisting}[language=Copilot]
v :: Stream Vec
v = [ Vec (Field 0) (Field 1) ] ++ v
\end{lstlisting}

We can also turn a field of a struct into its own stream using the
\texttt{(\#)}-operator:
\begin{lstlisting}[language=Copilot]
vx :: Stream Float
vx = v # x
\end{lstlisting}
Note the we use the Haskell level accessor \texttt{x} to retrieve the field
from the stream of vectors.


\subsubsection*{Example code}
\begin{example}
\label{exm:struct}
Now that we defined all there is, we can make streams of structs. The following
code has been taken from the \texttt{Struct.hs} example, and shows the basic
usage of structs.

\begin{lstlisting}[language=Copilot]
{-# LANGUAGE DataKinds #-}

module Struct where

import Language.Copilot
import Copilot.Compile.C99

import Prelude hiding ((>), (<), div, (++))


data Vec = Vec
  { x :: Field "x" Float
  , y :: Field "y" Float
  }

instance Struct Vec where
  typename _ = "vec"  -- Name of the type in C

  -- Function to translate Vec to list of Value's, order should match struct.
  toValues v = [ Value Float (x v)
               , Value Float (y v)
               ]

-- We need to provide an instance to Typed with a bogus Vec
instance Typed Vec where
  typeOf = Struct (Vec (Field 0) (Field 0))


vecs :: Stream Vec
vecs = [ Vec (Field 1) (Field 2)
       , Vec (Field 12) (Field 8)
       ] ++ vecs


spec = do
  -- Trigger that always executes, splits the vec into seperate args.
  trigger "split" true [arg $ vecs # x, arg $ vecs # y]
\end{lstlisting}
\end{example}

\subsection{Functions on Streams} \label{sec:FnOnStreams}

Given that constants and operators work pointwise on streams, we can use Haskell
as a macro-language for defining functions on streams.  The idea of using
Haskell as a macro language is powerful since Haskell is a
general-purpose higher-order functional language.

\begin{example}
We define the function {\tt even}, which given a stream of
integers returns a boolean stream which is true whenever the input stream
contains an even number, as follows:
%
\begin{lstlisting}[language = Copilot, frame = single]
even :: Stream Int32 -> Stream Bool
even x = x `mod` 2 == 0
\end{lstlisting}
%
Applying {\tt even} on {\tt nats} (defined above) yields the sequence
$\{T, F, T, F, T, F, \dots\}$.
\end{example}

If a function is required to return multiple results, we simply use plain
Haskell tuples:

\begin{example}
We define complex multiplication as follows:
%
\begin{lstlisting}[language = Copilot, frame = single]
mul_comp
  :: (Stream Double, Stream Double)
  -> (Stream Double, Stream Double)
  -> (Stream Double, Stream Double)
(a, b) `mul_comp` (c, d) = (a * c - b * d, a * d + b * c)
\end{lstlisting}
%
Here {\tt a} and {\tt b} represent the real and imaginary part of the left
operand, and {\tt c} and {\tt d} represent the real and imaginary part
of the right operand.
\end{example}

\subsection{Stateful Functions} \label{sec:stateful}

In addition to pure functions, such as {\tt even} and {\tt mul\_comp},
Copilot also facilitates \emph{stateful} functions. A \emph{stateful} function
is a function which has an internal state, e.g. as a latch (as in electronic
circuits) or a low/high-pass filter (as in a DSP).

\begin{figure*}
\begin{minipage}{0.25\linewidth}
\begin{tabular}{c|c||c}
$\mathtt{x}_i$: & $\mathtt{y}_{i-1}$: & $\mathtt{y}_i$:\\
\hline
$F$ & $F$ & $F$ \\
\hline
$F$ & $T$ & $T$ \\
\hline
$T$ & $F$ & $T$ \\
\hline
$T$ & $T$ & $F$
\end{tabular}
\end{minipage}
\begin{minipage}{0.35\linewidth}
\begin{lstlisting}[frame=none]
latch :: Stream Bool -> Stream Bool
latch x = y
  where
  y = if x then not z else z
  z = [False] ++ y
\end{lstlisting}
\end{minipage}
\hspace{1cm}
\begin{minipage}{0.3\linewidth}
\begin{tabular}{c|c|c|c|c|c}
   & 0 & 1 & 2 & 3 & 4\\
\hline
x & $F$ & $T$ & $T$ & $F$ & $F$ \\
\hline
y & $F$ & $T$ & $F$ & $F$ & $F$ \\
\end{tabular}
\end{minipage}
\caption{A latch [Example 3]. The specification function is provided at the left and the
implementation in copilot is provided in the middle. The right shows an example of
the latch, where x is $\{F, T, T, F, F, \dots \}$ and the initial value of y (used with $x_0$ to find
$y_0$ since there is no $y_{-1}$) is False.}
\label{fig:jk_latch}
\end{figure*}

\begin{example}
We consider a simple latch, as described in \cite{Farhat2004}, with a single
input and a boolean state. A latch is a way of simulating memory in circuits by feeding
back output gates as inputs.  Whenever the input is true the internal state is reversed.
The operational behavior and the implementation of the latch is shown in Figure
\ref{fig:jk_latch}.\footnote
{In order
to use conditionals (i.e., if-then-else) in Copilot specifications,
as in Figures~\ref{fig:jk_latch} and~\ref{fig:counter}, the GHC
language extension {\tt RebindableSyntax} must be set on.}
\end{example}

\begin{figure*}
\begin{minipage}{0.4\linewidth}
\begin{tabular}{c|c||c}
$\mathtt{inc}_i$: & $\mathtt{reset}_i$: & $\mathtt{cnt}_i$: \\
\hline
$F$ & $F$ & $\mathtt{cnt}_{i-1}$ \\
\hline
* & $T$ & $0$ \\
\hline
$T$ & $F$ & $\mathtt{cnt}_{i-1} + 1$ \\
\hline
\end{tabular}
\end{minipage}
\hspace{1cm}
\begin{minipage}{0.6\linewidth}
\begin{lstlisting}[language = Copilot, frame = none]
counter :: Stream Bool -> Stream Bool
        -> Stream Int32
counter inc reset = cnt
  where
  cnt = if reset then 0
          else if inc then z + 1
                 else z
  z = [0] ++ cnt
\end{lstlisting}
\end{minipage}
\caption{A resettable counter. The specification is provided at the left and the
implementation is provided at the right.
}
\label{fig:counter}
\end{figure*}

\begin{example}
We consider a resettable counter with two inputs, {\tt inc} and {\tt reset}.
The input {\tt inc} increments the counter and the input {\tt reset} resets the
counter. The internal state of the counter, {\tt cnt}, represents the value of the
counter and is initially set to zero. At each cycle, $i$, the value of
$\mathtt{cnt}_i$ is determined as shown in the left table in Figure
\ref{fig:counter}.
\end{example}

%\begin{figure}
%\begin{code}
%fir2pole :: Double -> Double -> Double -> Double
%  -> Double -> Sig Double -> Sig Double
%fir2pole a1 a2 b0 b1 b2 x0 = y0
%  where
%    y0 = - (constant a1)*y1 - (constant a2)*y2
%         + (constant b0)*x0 + (constant b1)*x1 + (constant b2)*x2
%    x2 = [0, 0] ++ x0 ; x1 = drop 1 x2
%    y2 = [0, 0] ++ y0 ; y1 = drop 1 y2
%\end{code}
%\caption{A $2$-pole IIR filter.}
%\label{fig:2_pole_iir_filter}
%\end{figure}

\subsection{Types} \label{sec:types}

Copilot is a typed language, where types are enforced by the Haskell type system
to ensure generated C programs are well-typed.  Copilot is \emph{strongly typed}
(i.e., type-incorrect function application is not possible) and \emph{statically
  typed} (i.e., type-checking is done at compile-time).  The base types are
Booleans, unsigned and signed words of width 8, 16, 32, and 64, floats, and
doubles.  All elements of a stream must belong to the same base
type.  These types have instances for the class {\tt Typed a}, used to constrain
Copilot programs.

We provide a {\tt cast} operator
%
\begin{lstlisting}[language = Copilot, frame = single]
cast :: (Typed a, Typed b) => Stream a -> Stream b
\end{lstlisting}
%
that casts from one type to another.  The cast operator is only defined for
casts that do not lose information, so an unsigned word type {\tt a} can only be
cast to another unsigned  type at least as large as {\tt a} or to a signed word
type strictly larger than {\tt a}.  Signed types cannot be cast to unsigned
types but can be cast to signed types at least as large.

There also exists an {\tt unsafeCast} operator which allows casting from any
type to any other (except from floating point numbers to integer types):

\begin{lstlisting}[language = Copilot, frame = single]
unsafeCast :: (Typed a, Typed b) => Stream a -> Stream b
\end{lstlisting}

\subsection{Interacting With the Target Program}
\label{subsec:interacting}

All interaction with the outside world is done by sampling \emph{external
  symbols} and by evoking \emph{triggers}.  External symbols are symbols that
are defined outside Copilot and which reflect the visible state of the target
program that we are monitoring.  They include variables and arrays.
Analogously, triggers are functions that are defined outside Copilot and which
are evoked when Copilot needs to report that the target program has violated a
specification constraint.

\paragraph{External Variables.}


As discussed in Section~\ref{sampling}, \emph{sampling} is an approach
for monitoring the state of an executing system based on sampling
state-variables, while assuming synchrony between the monitor and the
observed software. Copilot targets hard real-time embedded C programs
so the state variables that are observed by the monitors are variables
of C programs. Copilot monitors run either in the same thread or a
separate thread as the system under observation and the only variables
that can be observed are those that are made available through shared
memory. This means local variables cannot be observed. Currently,
Copilot supports basic C datatypes, arrays and structs. Combinations of each of
those work as well: nested arrays, arrays of structs, structs containg arrays
etc. All of these variables containing actual data; pointers to data are not
supported by design.


Copilot has both an interpreter and a compiler.The compiler must be
used to monitor an executing program. The Copilot reification process
generates a C monitor from a Copilot specification. The variables that
are observed in the C code must be declared as \emph{external}
variables in the monitor. The external variables have the same name as
the variables being monitored in the C code are treated as shared
memory. The interpreter is intended for exploring ideas and algorithms
and is not intended to monitor executing  C
programs. It may seem external variables would have no meaning if the
monitor was run in the interpreter, but Copilot gives the user the
ability to specify default stream values for an external variable that
get used when the monitor interpreted.

 A Copilot specification is \emph{open} if defined with external symbols in the
sense that values must be provided externally at runtime.  To simplify writing
Copilot specifications that can be interpreted and tested, constructs for
external symbols take an optional environment for interpretation.

External variables are similar to global variables in other languages. They
are defined by using the {\tt extern} construct:
%
\begin{lstlisting}[language = Copilot, frame = single]
extern :: Typed a => String -> Maybe [a] -> Stream a
\end{lstlisting}
%
\noindent
It takes the name of an external variable, a possible Haskell list to serve as
the environment for the interpreter, and generates a stream by sampling the
variable at each clock cycle.  For example,
%
\begin{lstlisting}[language = Copilot, frame = single]
sumExterns :: Stream Word64
sumExterns = let ex1 = extern "e1" (Just [0..])
                 ex2 = extern "e2" Nothing
             in  ex1 + ex2
\end{lstlisting}
%
is a stream that takes two external variables {\tt e1} and {\tt e2} and adds
them.  The first external variable contains the infinite list {\tt [0,1,2,...]}
of values for use when interpreting a Copilot specification containing the
stream.  The other variable contains no environment ({\tt sumExterns} must have
an environment for both of its variables to be interpreted).

Sometimes, type inference cannot infer the type of an external variable.  For
example, in the stream definition
%
\begin{lstlisting}[language = Copilot, frame = single]
extEven :: Stream Bool
extEven = e0 `mod` 2 == 0
  where e0 = externW8 "x" Nothing
\end{lstlisting}
%
\noindent
the type of {\tt extern "x"} is ambiguous, since it cannot be inferred from a
Boolean stream and we have not given an explicit type signature.  For
convenience, typed {\tt extern} functions are provided, e.g., {\tt externW8} or
{\tt externI64} denoting an external unsigned 8-bit word or signed 64-bit word,
respectively.
% Please see the grammar in Appendix~\ref{sec:BNF} for the list of
% all sampling functions.

In general it is best practice to define external symbols with
top-level definitions, e.g.,
%
\begin{lstlisting}[language = Copilot, frame = single]
e0 :: Stream Word8
e0 = extern  "e0" (Just [2,4..])
\end{lstlisting}

\noindent
so that the symbol name and its environment can be shared between streams.

Just like regular variables, arrays can be sampled as well. Copilot threats
arrays in the same way as it does for scalars. 
\begin{example}
\label{exmp:pitot}
Lets take the example where we
have the readouts of four pitot tubes, giving us the measured airspeed:
\begin{code}[frame=single]
/* Array containing readouts of 4 pitot tubes. */
double airspeeds[4] = ... ;
\end{code}
In our Copilot specification, we need to provide the type of our array, because
Copilot need to know the length of the array we refer to. Apart from that,
referring to an external array is like referring to any other variable:
\begin{lstlisting}[language=Copilot, frame=single]
airspeeds :: Stream (Array 4 Double)
airspeeds = extern "airspeeds" Nothing
\end{lstlisting}
\end{example}


\paragraph{Triggers.}
Triggers, the only mechanism for Copilot streams to effect the outside world,
are defined by using the {\tt trigger construct}:
%
\begin{lstlisting}[language = Copilot, frame = single]
trigger :: String -> Stream Bool -> [TriggerArg] -> Spec
\end{lstlisting}
%
The first parameter is the name of the external function, the second parameter is the
guard which determines when the trigger should be evoked, and the third parameter
is a list of arguments which is passed to the trigger when evoked.
Triggers can be combined into a specification by using the \emph{do}-notation:
%
\begin{lstlisting}[language = Copilot, frame = single]
spec :: Spec
spec = do
  trigger "f" (even nats) [arg fib, arg (nats * nats)]
  trigger "g" (fib > 10) []
  let x = externW64 "x" (Just [1..])
  trigger "h" (x < 10) [arg x]
\end{lstlisting}
%
The order in which the triggers are defined is irrelevant. To interpret this spec we run:
%
\begin{lstlisting}[language = Copilot, frame = single]
interpret 10 spec
\end{lstlisting}
%
which will yield the following output:
%
\begin{code}
f:        g:	 h:
(1,0)     ()        (1)
--        ()        (2)
(2,4)     ()        (3)
--        ()        (4)
(5,16)    ()        (5)
--        ()        (6)
(13,36)   --	(7)
--        --        (8)
(34,64)   --	(9)
--        --         --
\end{code}
%

\begin{example}
\label{exm:engine}
We consider an engine controller with the following property: If the temperature
rises more than 2.3 degrees within 0.2 seconds, then the fuel injector should
not be running.  Assuming that the global sample rate is 0.1 seconds, we can
define a monitor that surveys the above property:
%
\begin{lstlisting}[language = Copilot, frame = single]
propTempRiseShutOff :: Spec
propTempRiseShutOff =
  trigger "over_temp_rise"
    (overTempRise && running) []

  where
  max = 500 -- maximum engine temperature

  temps :: Stream Float
  temps = [max, max, max] ++ temp

  temp = extern "temp" Nothing

  overTempRise :: Stream Bool
  overTempRise = drop 2 temps > (2.3 + temps)

  running :: Stream Bool
  running = extern "running" Nothing
\end{lstlisting}
%

Here, we assume that the external variable {\tt temp} denotes the temperature of
the engine and the external variable {\tt running} indicates whether the fuel
injector is running.  The external function {\tt over\_temp\_rise} is called
without any arguments if the temperature rises more than 2.3 degrees within 0.2
seconds and the engine is not shut off.  Notice there is a latency of one tick between when the property is violated and when the guard becomes true.
\end{example}