example.tex

\section{Complete example}
\label{sec:complete_example}
This section describes a complete use case example in Copilot. We will be using
one of the provided examples as our code, and focus more on using Copilot
within a project.

The code implements a simple heater, which turns on when the temperature drops
below a certain point, and turns off if the temperature is too high. The
temperature is read from a sensor returns a byte, with a range of
$-50.0\degree$C to $100.0\degree$C. For easy of use, the monitor translates the
byte to a float within this range.

\subsection{C Code}
Lets start of with the C program our monitor to connect to.
\begin{lstlisting}[language=c, numbers=left]
#include <stdlib.h>
#include <stdint.h>

#include "heater_types.h" /* Generated by our specification */
#include "heater.h" /* Generated by our specification */

uint8_t temperature;

void heaton (float temp) {
  /* Low-level code to turn heating on */
}

void heatoff (float temp) {
  /* Low-level code to turn heating off */
}

int main (int argc, char *argv[]) {
  for (;;) {
    temperature = readbyte(); /* Dummy function to read a byte from a sensor. */

    step();
  }

  return 0;
}
\end{lstlisting}

For this code we left out the low-level details for interfacing with our
hardware. Let us look at a couple of interesting lines:

\begin{description}
  \item[Line 4] Here we inclued the header types files generated by out Copilot
  specification. This file must precede the inclusion of the generated header
  file on the next line. 
  \item[Line 5] Here we include the header file generated by our Copilot
  specification (see next section).
  \item[Line 9] Global variable that stores the raw output of the temperature
  sensor. This variable should be global, so it can be read from the code
  generate from our monitor.
  \item[Line 9-15] Functions that turn on and turn off the
  heater, low-level details are provided.
  \item[Line 18-22] Our infinite main-loop:
    \begin{description}
      \item[Line 19] Update our global temperature variable by reading it from
      the sensor.
      \item[Line 21] Execute a single evaluation step of Copilot.
      \texttt{step()} is imported from the \texttt{heater.h}, and is the only
      publicly available function from the specification.
    \end{description}
\end{description}

As the code shows, the rate at which Copilot is updated is entirely up to the
programmer of the main C program. In this case it is updated as quick as
possible, but we could have opted to slow it down with a delay or a scheduler.
Theoretically there could be multiple calls to \texttt{step()} throughout the
program, but this complicated things and is highly discouraged.


\subsection{Specification}
The code for this specification can be found in the \texttt{Examples} directory
of Copilot, or from the
repository\footnote{\url{https://github.com/Copilot-Language/Copilot/blob/master/Examples/Heater.hs}}.

\begin{lstlisting}[language = Copilot, frame = single, numbers = left]
--------------------------------------------------------------------------------
-- Copyright 2019 National Institute of Aerospace / Galois, Inc.
--------------------------------------------------------------------------------

-- This is a simple example with basic usage. It implements a simple home
-- heating system: It heats when temp gets too low, and stops when it is high
-- enough. It read temperature as a byte (range -50C to 100C) and translates
-- this to Celcius.

module Heater where

import Language.Copilot
import Copilot.Compile.C99

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

-- External temperature as a byte, range of -50C to 100C
temp :: Stream Word8
temp = extern "temperature" Nothing

-- Calculate temperature in Celcius.
-- We need to cast the Word8 to a Float. Note that it is an unsafeCast, as there
-- is no direct relation between Word8 and Float.
ctemp :: Stream Float
ctemp = (unsafeCast temp) * (150.0 / 255.0) - 50.0

spec = do
  -- Triggers that fire when the ctemp is too low or too high,
  -- pass the current ctemp as an argument.
  trigger "heaton"  (ctemp < 18.0) [arg ctemp]
  trigger "heatoff" (ctemp > 21.0) [arg ctemp]

-- Compile the spec
main = reify spec >>= compile "heater"
\end{lstlisting}
The code should be pretty self explanatory. Note that we opted to use a
\texttt{main}-function, which reifies and compiles the code for us.

On line 25 we can see the \texttt{ctemp}-stream, which is the temperature
translated to Celcius. Interestingly, we need to do a manual typecast from
\texttt{Word8} to \texttt{Float} using \texttt{unsafeCast}. This is a function
provided by Copilot that can cast a stream to a different type in an unsafe
manner, i.e. there may not be an exact representation of the value in both
types. For this code, it might happen that an integer value cannot be
represented exactly with a floating point.

\subsection{Generating C code}
Because we defined the \texttt{main}-function in our specification, generating
code is now really easy:
\begin{code}
$ runhaskell Heater.hs
\end{code}
This runs our Haskell code, with compiling a binary first. It runs that
\texttt{main}-function and generates the C code of our monitor. Note that it
called the files \texttt{heater.h}, \texttt{heater\_types.h} and \texttt{heater.c}, as defined by the
prefix passed to the \texttt{compile}-function.

The next step is as easy as compiling our C code together with the monitor. We
have opted to use GCC in a C99 mode with a extended set of warnings:
\begin{code}
$ gcc -Wall -std=c99 heater.c main.c -o heater
\end{code}

If the implementations for \texttt{heaton}, \texttt{heatoff} and
\texttt{readbyte} are provided somewhere, this should give us a nicely compiled
binary called \texttt{heater}. Running this will provide us with a system that
turns the heater on, when the temperature drops below $18.0\degree$C and turns
it off once it becomes higher then $21.0\degree$C.