From b36fb4028bd7363d4c0be65a503cf4c3c25fcfc7 Mon Sep 17 00:00:00 2001 From: Will Pogge Date: Wed, 25 Jan 2023 17:14:20 -0500 Subject: [PATCH 1/9] The start of the commits this has a lot in it but there will be more regular commits from here --- TutorialAndDevGuide/Tutorial/Interpret.tex | 119 +++++++++--------- TutorialAndDevGuide/Tutorial/Language.tex | 39 +++--- TutorialAndDevGuide/Tutorial/example.tex | 33 +++++ TutorialAndDevGuide/Tutorial/introduction.tex | 24 +--- 4 files changed, 108 insertions(+), 107 deletions(-) diff --git a/TutorialAndDevGuide/Tutorial/Interpret.tex b/TutorialAndDevGuide/Tutorial/Interpret.tex index 2eb968c..1ad4c2b 100644 --- a/TutorialAndDevGuide/Tutorial/Interpret.tex +++ b/TutorialAndDevGuide/Tutorial/Interpret.tex @@ -1,21 +1,66 @@ \newpage -\section{Interpreting and Compiling} +\section{Interpreting} \label{interpcompile} The Copilot RV framework comes with both an interpreter and a -compiler. +compiler. We will address compiling in section 4 with a complete example. +\noindent To use the language, your Haskell module should contain the following import: +% +\begin{code} +import Language.Copilot +\end{code} +% +If you need to use functions defined in the Prelude that are redefined by +Copilot (e.g., arithmetic operators), import the Prelude qualified: +% +\begin{code} +import qualified Prelude as P +\end{code} + \subsection{Interpreting Copilot} -Assume we are currently in a directory containing a \texttt{.hs} file with our -specification (\texttt{Spec.hs} in this case), and that Copilot is installed -globally. If we want to interpret the specification, we need to start the GHC -Interpreter with the file as an argument: +In the ./Examples directory we have provided you with an example +for you to follow allong. \texttt{Spec.hs} is the following Copilot program: +% +\lstinputlisting[language = Copilot, numbers = left]{Examples/Spec.hs} +%import Language.Copilot hiding (even, odd) +% +%import qualified Prelude as P hiding ((++),(==), mod, even, odd) +% +%nats :: Stream Int32 +%nats = [0] ++ (1 + nats) +% +%even :: Stream Int32 -> Stream Bool +%even n = n `mod` 2 == 0 +% +%odd :: Stream Int32 -> Stream Bool +%odd n2 = n2 `mod` 2 == 1 +% +%spec = do +% trigger "trigger1" (even nats) [arg nats, arg $ odd nats] +% trigger "trigger2" (odd nats) [arg nats] +%\end{lstlisting} +% $ +\begin{description} + \item[Line 1] Here we inclued the Copilot Language so that we gain access to the + front end language. + \item[Line 3] Here we include the Prelude so that we can hide base Haskell syntax + that we have redefined. If this is not included you will get an \texttt{Ambiguious + Occurance} error. + \item[Line 5-12] Here we define data streams as input and output data streams. We + go over defining functions as streams in Section 3 of this tutorial. + \item[Line 14-16] Here {\tt nats} is the stream of natural numbers, and {\tt even} and {\tt odd} + are the guard functions that take a stream and return whether the point-wise + values are even or odd, respectively. The lists at the end of the trigger + represent the values the trigger will output when the guard is true. + +\end{description} + +If we want to interpret the specification, we need to start the GHC Interpreter with the file as an argument: % \begin{lstlisting} $ ghci Spec.hs -GHCi, version 8.4.3: http://www.haskell.org/ghc/ :? for help -Loaded GHCi configuration from /home/user/.ghc/ghci.conf [1 of 1] Compiling Spec ( Spec.hs, interpreted ) Ok, one module loaded. -*Spec > +ghci > \end{lstlisting} % This launches \texttt{ghci}, the Haskell interpreter, with \texttt{Spec.hs} @@ -23,7 +68,7 @@ \subsection{Interpreting Copilot} assume that our file contains one specification, called \texttt{spec}. We can interpret this using the \texttt{interpret}-function: \begin{lstlisting}[language = Copilot] -*Spec > interpret 10 spec +ghci > interpret 10 spec \end{lstlisting} % The first argument to the function \emph{interpret} is the number of iterations @@ -33,25 +78,7 @@ \subsection{Interpreting Copilot} The interpreter outputs the values of the arguments passed to the trigger, if its guard is true, and {\tt --} otherwise. We will discuss triggers in more detail later, but for now, just know that they produce an output only when the -guard function is true. For example, consider the following Copilot program: -% -\begin{lstlisting}[language = Copilot] -spec = do - trigger "trigger1" (even nats) [arg nats, arg $ odd nats] - trigger "trigger2" (odd nats) [arg nats] -\end{lstlisting} -% $ -where {\tt nats} is the stream of natural numbers, and {\tt even} and {\tt odd} -are the guard functions that take a stream and return whether the point-wise -values are even or odd, respectively. The lists at the end of the trigger -represent the values the trigger will output when the guard is true. The output -of -% -\begin{lstlisting}[language = Copilot] -interpret 10 spec -\end{lstlisting} -% $ -is as follows: +guard function is true. The output is as follows: % \begin{code} trigger1: trigger2: @@ -72,38 +99,4 @@ \subsection{Interpreting Copilot} while trigger2 only outputs the number. This output reflects the arguments passed to them. -\subsection{Compiling Copilot} \label{sec:compiling} - -Compiling a Copilot specification is straightforward. Currently Copilot -supports one back-end, \texttt{copilot-c99} that creates constant-space C99 -code. Using the back-end is rather easy, as it just requires one to import it in -their Copilot specification file: - -\begin{lstlisting}[language = Copilot] -import Copilot.Compile.C99 -\end{lstlisting} - -Importing the back-end provides us with the \texttt{compile}-function, which -takes a prefix as its first parameter and a \textit{reified} specification as -its second. When inside \texttt{ghci}, with our file loaded, we can generate -output code by executing: -\footnote{Two explanations are in order: (1) {\tt reify} allows sharing in the -expressions to be compiled~\cite{DSLExtract}, and {\tt >>=} is a higher-order -operator that takes the result of reification and ``feeds'' it to the compile -function.} -\begin{lstlisting}[language = Copilot] -reify spec >>= compile "monitor" -\end{lstlisting} - -This generates three output files: -\begin{itemize} - \item \texttt{.c}: C99 file containing the generated code and the - \texttt{step()} function. This should be compiled by the C compiler, and - included in the final binary. - \item \texttt{\_types.h}: Header file containing datatypes defined in the specification and used by Copilot internally. Copilot users can opt to include these definitions in their C code, to avoid having to manually define those datatypes and keep them in sync. However, when the Copilot specification is tied to an existing codebase, including this header from user code is not recommended as the definitions in it may conflict with C types defined elsewhere in the same codebase. - \item \texttt{.h}: Header providing the public interface to the - monitor. This file should be included from your main project. -\end{itemize} -Please refer to the complete example \ref{sec:complete_example} for more on -detail to use the monitor in your C program. diff --git a/TutorialAndDevGuide/Tutorial/Language.tex b/TutorialAndDevGuide/Tutorial/Language.tex index f571b1c..6c702aa 100644 --- a/TutorialAndDevGuide/Tutorial/Language.tex +++ b/TutorialAndDevGuide/Tutorial/Language.tex @@ -1,9 +1,7 @@ \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 +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: @@ -30,20 +28,13 @@ \section{Language}~\label{sec:language} $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: +lifted to work pointwise on streams. Here we give you another example +\texttt{Streams.hs} found in the examples directory: \noindent %\begin{minipage}{0.3\textwidth} -\begin{lstlisting}[language = Copilot, frame = single] -x :: Stream Int32 -x = 5 + 5 - -y :: Stream Int32 -y = x * x +\lstinputlisting[language = Copilot, frame = single, numbers = left]{Examples/Streams.hs} -z :: Stream Bool -z = x == 10 && y < 200 -\end{lstlisting} %\end{minipage} @@ -56,6 +47,9 @@ \section{Language}~\label{sec:language} $\mathtt{z} \leadsto \{\mbox{T},\; \mbox{T},\; \mbox{T},\; \dots \}$ \end{center} +\noindent Interpret this the same way that you did in section 2 and see +the results yourself. + Two types of \emph{temporal} operators are provided, one for delaying streams and one for looking into the future of streams: % @@ -73,7 +67,9 @@ \section{Language}~\label{sec:language} \end{lstlisting} % evaluates to the sequence -$\mathtt{w} \leadsto \{5, 6, 7, 10, 10, 10, \dots\}$. +$\mathtt{w} \leadsto \{5, 6, 7, 10, 10, 10, \dots\}$. Add this to the Streams.hs +specification and add a trigger so you can see the result for yourself. + 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}: @@ -87,8 +83,10 @@ \section{Language}~\label{sec:language} \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: +This subsection is to show users that are familiar with Haskell that streams +function like lazy lists. For those that are not as familiar with Haskell this +subsection can be omitted. However, there is a few useful definitions of data +streams as examples. % \begin{lstlisting}[language = Copilot, frame = single] nats_ll :: [Int32] @@ -117,17 +115,12 @@ \subsection{Streams as Lazy-Lists} \label{sec:stream} fib = [1, 1] ++ (fib + drop 1 fib) \end{lstlisting} +\subsection{Causality} 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} +\lstinputlisting[language = Copilot, frame = single ]{Examples/Causal.hs} % But if instead {\tt g} is defined as {\tt g = drop 4 f}, then the definition is diff --git a/TutorialAndDevGuide/Tutorial/example.tex b/TutorialAndDevGuide/Tutorial/example.tex index be93154..3b9a836 100644 --- a/TutorialAndDevGuide/Tutorial/example.tex +++ b/TutorialAndDevGuide/Tutorial/example.tex @@ -10,6 +10,39 @@ \section{Complete example} $-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{Compiling Copilot} \label{sec:compiling} + +Compiling a Copilot specification is straightforward. Currently Copilot +supports one back-end, \texttt{copilot-c99} that creates constant-space C99 +code. Using the back-end is rather easy, as it just requires one to import it in +their Copilot specification file: + +\begin{lstlisting}[language = Copilot] +import Copilot.Compile.C99 +\end{lstlisting} + +Importing the back-end provides us with the \texttt{compile}-function, which +takes a prefix as its first parameter and a \textit{reified} specification as +its second. When inside \texttt{ghci}, with our file loaded, we can generate +output code by executing: +\footnote{Two explanations are in order: (1) {\tt reify} allows sharing in the +expressions to be compiled~\cite{DSLExtract}, and {\tt >>=} is a higher-order +operator that takes the result of reification and ``feeds'' it to the compile +function.} +\begin{lstlisting}[language = Copilot] +reify spec >>= compile "monitor" +\end{lstlisting} + +This generates three output files: +\begin{itemize} + \item \texttt{.c}: C99 file containing the generated code and the + \texttt{step()} function. This should be compiled by the C compiler, and + included in the final binary. + \item \texttt{\_types.h}: Header file containing datatypes defined in the specification and used by Copilot internally. Copilot users can opt to include these definitions in their C code, to avoid having to manually define those datatypes and keep them in sync. However, when the Copilot specification is tied to an existing codebase, including this header from user code is not recommended as the definitions in it may conflict with C types defined elsewhere in the same codebase. + \item \texttt{.h}: Header providing the public interface to the + monitor. This file should be included from your main project. +\end{itemize} + \subsection{C Code} Lets start of with the C program our monitor to connect to. \begin{lstlisting}[language=c, numbers=left] diff --git a/TutorialAndDevGuide/Tutorial/introduction.tex b/TutorialAndDevGuide/Tutorial/introduction.tex index cdc7c22..8e3ce0f 100644 --- a/TutorialAndDevGuide/Tutorial/introduction.tex +++ b/TutorialAndDevGuide/Tutorial/introduction.tex @@ -24,8 +24,8 @@ \section{Introduction} \label{sec:introduction} Copilot is a RV framework for specifying and generating monitors for C programs that is embedded into the functional programming language Haskell -\cite{PeytonJones02}. A working knowledge of Haskell is necessary to use -Copilot effectively; a variety of books and free web resources introduce Haskell. +\cite{PeytonJones02}. A working knowledge of Haskell is not necessary to use +Copilot at a basic level. However, knowledge of Haskell will significantly aid you in writing Copilot specifications; a variety of books and free web resources introduce Haskell. Copilot uses Haskell language extensions specific to the Glasgow Haskell Compiler (GHC). @@ -57,7 +57,7 @@ \subsection{Target Application Domain} \label{domain} \subsection{Installation} \label{sec:install} -Before downloading the copilot source code, you must first install an +Before downloading the copilot framework, you must first install an up-to-date version of GHC (the minimal required version is 8.0). The easiest way to do this is to download and install the Haskell Platform, which is freely distributed from here: @@ -99,24 +99,6 @@ \subsection{Installation} \label{sec:install} \end{code} \end{itemize} -\noindent To use the language, your Haskell module should contain the following import: -% -\begin{code} -import Language.Copilot -\end{code} -% -To use the C99 back-end, import it: -% -\begin{code} -import Copilot.Compile.C99 -\end{code} -% -If you need to use functions defined in the Prelude that are redefined by -Copilot (e.g., arithmetic operators), import the Prelude qualified: -% -\begin{code} -import qualified Prelude as P -\end{code} \subsection{Structure} \label{structure} From 562287a9251ccdc598a275d7a01dcd1e762d86c6 Mon Sep 17 00:00:00 2001 From: Will Pogge Date: Thu, 26 Jan 2023 09:58:51 -0500 Subject: [PATCH 2/9] Change the code in section 3.2 to a fibonachi series and adjusted the text around it to reflect that. --- TutorialAndDevGuide/Tutorial/Language.tex | 13 +++++++------ 1 file changed, 7 insertions(+), 6 deletions(-) diff --git a/TutorialAndDevGuide/Tutorial/Language.tex b/TutorialAndDevGuide/Tutorial/Language.tex index 6c702aa..9956164 100644 --- a/TutorialAndDevGuide/Tutorial/Language.tex +++ b/TutorialAndDevGuide/Tutorial/Language.tex @@ -117,16 +117,17 @@ \subsection{Streams as Lazy-Lists} \label{sec:stream} \subsection{Causality} Copilot specifications must be \emph{causal}, informally meaning that -stream values cannot depend on future values. For example, the following stream -definition is allowed: +stream values cannot depend on future values. Our example \texttt{Causal.hs} +in the examples directory shows the use of {\tt drop} and {\tt ++} by defining +a fibonachi series and then creates a leading and lagging stream: % \lstinputlisting[language = Copilot, frame = single ]{Examples/Causal.hs} % -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 +But if instead {\tt fastForwardFib} is defined as {\tt fastforwardFib = drop 4 fib} +, 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 fib} + to be generated before producing values for {\tt fastForwardFib}. This is not possible since Copilot programs may take inputs in real-time from the environment (see Section~\ref{subsec:interacting}). From af7f69029a15aa59eca541d4811f2407d2453a72 Mon Sep 17 00:00:00 2001 From: Will Pogge Date: Thu, 26 Jan 2023 13:00:25 -0500 Subject: [PATCH 3/9] Add in the hyperref package so that people can ref around the document --- TutorialAndDevGuide/Tutorial/Interpret.tex | 2 +- TutorialAndDevGuide/Tutorial/Language.tex | 1 - TutorialAndDevGuide/Tutorial/tutorial.tex | 12 +++++++++--- 3 files changed, 10 insertions(+), 5 deletions(-) diff --git a/TutorialAndDevGuide/Tutorial/Interpret.tex b/TutorialAndDevGuide/Tutorial/Interpret.tex index 1ad4c2b..2ab6176 100644 --- a/TutorialAndDevGuide/Tutorial/Interpret.tex +++ b/TutorialAndDevGuide/Tutorial/Interpret.tex @@ -2,7 +2,7 @@ \section{Interpreting} \label{interpcompile} The Copilot RV framework comes with both an interpreter and a -compiler. We will address compiling in section 4 with a complete example. +compiler. We will address compiling in \hyperref[sec:complete_example]{section 4} with a complete example. \noindent To use the language, your Haskell module should contain the following import: % \begin{code} diff --git a/TutorialAndDevGuide/Tutorial/Language.tex b/TutorialAndDevGuide/Tutorial/Language.tex index 9956164..fecf356 100644 --- a/TutorialAndDevGuide/Tutorial/Language.tex +++ b/TutorialAndDevGuide/Tutorial/Language.tex @@ -1,6 +1,5 @@ \section{Language}~\label{sec:language} - 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 diff --git a/TutorialAndDevGuide/Tutorial/tutorial.tex b/TutorialAndDevGuide/Tutorial/tutorial.tex index ad582d8..7f276ef 100644 --- a/TutorialAndDevGuide/Tutorial/tutorial.tex +++ b/TutorialAndDevGuide/Tutorial/tutorial.tex @@ -49,8 +49,14 @@ \usepackage{float} \floatstyle{boxed} \restylefloat{figure} - - +\usepackage{hyperref} +\hypersetup{ + colorlinks=true, + linkcolor=blue, + filecolor=magenta, + urlcolor=cyan, + menubordercolor=0 0 0, +} \DefineVerbatimEnvironment{code}{Verbatim}{fontsize=\footnotesize} % Copilot + formatting for listings @@ -308,7 +314,7 @@ \section*{Abstract} demonstrating the fundamental concepts of the language by using idiomatic expositions and examples. } - +\newpage { \small \setcounter{tocdepth}{2} From 3dd3dc10f5697f929b91c258946ed776a6f353a3 Mon Sep 17 00:00:00 2001 From: Will Pogge Date: Thu, 26 Jan 2023 14:05:04 -0500 Subject: [PATCH 4/9] Add an example for section 3.2 for them to try out --- TutorialAndDevGuide/Tutorial/Language.tex | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) diff --git a/TutorialAndDevGuide/Tutorial/Language.tex b/TutorialAndDevGuide/Tutorial/Language.tex index fecf356..4428d45 100644 --- a/TutorialAndDevGuide/Tutorial/Language.tex +++ b/TutorialAndDevGuide/Tutorial/Language.tex @@ -46,7 +46,7 @@ \section{Language}~\label{sec:language} $\mathtt{z} \leadsto \{\mbox{T},\; \mbox{T},\; \mbox{T},\; \dots \}$ \end{center} -\noindent Interpret this the same way that you did in section 2 and see +\noindent Interpret this the same way that you did in Section 2 and see the results yourself. Two types of \emph{temporal} operators are provided, one for delaying streams and one for @@ -117,7 +117,7 @@ \subsection{Streams as Lazy-Lists} \label{sec:stream} \subsection{Causality} Copilot specifications must be \emph{causal}, informally meaning that stream values cannot depend on future values. Our example \texttt{Causal.hs} -in the examples directory shows the use of {\tt drop} and {\tt ++} by defining +in the ./Examples directory shows the use of {\tt drop} and {\tt ++} by defining a fibonachi series and then creates a leading and lagging stream: % \lstinputlisting[language = Copilot, frame = single ]{Examples/Causal.hs} @@ -129,7 +129,11 @@ \subsection{Causality} to be generated before producing values for {\tt fastForwardFib}. This is not possible since Copilot programs may take inputs in real-time from the environment (see Section~\ref{subsec:interacting}). - +Being able to look ahead and behind in streams is really useful for thing like rate of change +for example if you were intrested in monitoring how fast your car was accelerating or the rate +of drain on a battery. If you would like more practice with the Copilot language try adding in +an observer that shows how much change there was between the leading and the lagging stream for +our fibonachi example. \subsection{Structs} Structs require some special attentation in Copilot, as we cannot magically From 57f978b03a3a60da010b76a4572ca926e3f6053c Mon Sep 17 00:00:00 2001 From: Will Pogge Date: Thu, 26 Jan 2023 14:45:43 -0500 Subject: [PATCH 5/9] Changed the reify from monitor to heater because that is what they will see later in the document. --- TutorialAndDevGuide/Tutorial/Language.tex | 4 ++++ TutorialAndDevGuide/Tutorial/example.tex | 2 +- 2 files changed, 5 insertions(+), 1 deletion(-) diff --git a/TutorialAndDevGuide/Tutorial/Language.tex b/TutorialAndDevGuide/Tutorial/Language.tex index 4428d45..dc598b7 100644 --- a/TutorialAndDevGuide/Tutorial/Language.tex +++ b/TutorialAndDevGuide/Tutorial/Language.tex @@ -136,6 +136,7 @@ \subsection{Causality} our fibonachi example. \subsection{Structs} +When monitoring embedded systems the data that needs to be observed is often in a struct. 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 @@ -160,6 +161,9 @@ \subsection{Structs} \item Write an instance of the \texttt{Typed} class. \end{enumerate} +If you would like to follow along with our example you can open up the Structs.hs file +in the ./Examples directory. We do show the entire thing at the end. + \subsubsection*{Enabling compiler extensions} First and foremost, we need to enable the \texttt{DataKinds} extension to GHC, by putting: diff --git a/TutorialAndDevGuide/Tutorial/example.tex b/TutorialAndDevGuide/Tutorial/example.tex index 3b9a836..823b59d 100644 --- a/TutorialAndDevGuide/Tutorial/example.tex +++ b/TutorialAndDevGuide/Tutorial/example.tex @@ -30,7 +30,7 @@ \subsection{Compiling Copilot} \label{sec:compiling} operator that takes the result of reification and ``feeds'' it to the compile function.} \begin{lstlisting}[language = Copilot] -reify spec >>= compile "monitor" +reify spec >>= compile "heater" \end{lstlisting} This generates three output files: From e365694eb5941635e9d94b17b9cb22d43aed1d19 Mon Sep 17 00:00:00 2001 From: Will Pogge Date: Tue, 31 Jan 2023 12:21:48 -0500 Subject: [PATCH 6/9] Added in examples and moved the functions on streams --- TutorialAndDevGuide/Tutorial/Language.tex | 240 ++++++++-------------- 1 file changed, 83 insertions(+), 157 deletions(-) diff --git a/TutorialAndDevGuide/Tutorial/Language.tex b/TutorialAndDevGuide/Tutorial/Language.tex index dc598b7..a770d0f 100644 --- a/TutorialAndDevGuide/Tutorial/Language.tex +++ b/TutorialAndDevGuide/Tutorial/Language.tex @@ -26,9 +26,81 @@ \section{Language}~\label{sec:language} 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. Here we give you another example -\texttt{Streams.hs} found in the examples directory: +\subsection{Streams as Lazy-Lists} \label{sec:stream} + +This subsection is to show users that are familiar with Haskell that streams +function like lazy lists. For those that are not as familiar with Haskell this +subsection can be omitted. However, there is a few useful definitions of data +streams as examples. +% +\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} + +\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} + +Here we give you another example \texttt{Streams.hs} found in the ./Examples directory: \noindent %\begin{minipage}{0.3\textwidth} @@ -49,6 +121,7 @@ \section{Language}~\label{sec:language} \noindent Interpret this the same way that you did in Section 2 and see the results yourself. +\subsection{Causality} Two types of \emph{temporal} operators are provided, one for delaying streams and one for looking into the future of streams: % @@ -80,41 +153,6 @@ \section{Language}~\label{sec:language} which yields the sequence $\mathtt{u} \leadsto \{7, 10, 10, 10, \dots\}$. -\subsection{Streams as Lazy-Lists} \label{sec:stream} - -This subsection is to show users that are familiar with Haskell that streams -function like lazy lists. For those that are not as familiar with Haskell this -subsection can be omitted. However, there is a few useful definitions of data -streams as examples. -% -\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} - -\subsection{Causality} Copilot specifications must be \emph{causal}, informally meaning that stream values cannot depend on future values. Our example \texttt{Causal.hs} in the ./Examples directory shows the use of {\tt drop} and {\tt ++} by defining @@ -129,6 +167,7 @@ \subsection{Causality} to be generated before producing values for {\tt fastForwardFib}. This is not possible since Copilot programs may take inputs in real-time from the environment (see Section~\ref{subsec:interacting}). + Being able to look ahead and behind in streams is really useful for thing like rate of change for example if you were intrested in monitoring how fast your car was accelerating or the rate of drain on a battery. If you would like more practice with the Copilot language try adding in @@ -208,7 +247,7 @@ \subsubsection*{Instance of \texttt{Struct}} 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 :: Vec -> [Value Vec] toValues v = [ Value Float (x v) , Value Float (y v) ] @@ -260,92 +299,13 @@ \subsubsection*{Simple operations} \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} +\lstinputlisting[language = Copilot, frame = single, numbers = left]{Examples/Structs.hs} % -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} @@ -354,45 +314,11 @@ \subsection{Stateful Functions} \label{sec:stateful} 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 +\lstinputlisting[language = Copilot, frame = single, numbers = left]{Examples/Latch.hs} + +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*} +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. \begin{example} We consider a simple latch, as described in \cite{Farhat2004}, with a single From f083ba04716be1ed392e70679c43405b1a8b64da Mon Sep 17 00:00:00 2001 From: Will Pogge Date: Thu, 18 May 2023 12:15:06 -0400 Subject: [PATCH 7/9] TutorialAndDevGuide: Added examples and updated most sections of the tutorial. --- .../Tutorial/Examples/Causal.hs | 17 + .../Tutorial/Examples/Counter_Answer.hs | 23 ++ .../Tutorial/Examples/Counter_Problem.hs | 21 ++ .../Tutorial/Examples/Distance_Monitor.hs | 19 ++ .../Tutorial/Examples/EvenStream_Answers.hs | 17 + .../Tutorial/Examples/EvenStream_Problem.hs | 17 + .../Tutorial/Examples/Filters.hs | 47 +++ .../Tutorial/Examples/Heater.hs | 32 ++ .../Tutorial/Examples/Latch.hs | 19 ++ .../Tutorial/Examples/Sonar.hs | 15 + TutorialAndDevGuide/Tutorial/Examples/Spec.hs | 19 ++ .../Tutorial/Examples/Streams.hs | 17 + .../Tutorial/Examples/Structs.hs | 32 ++ .../Tutorial/Examples/backup_monitor.c | 53 +++ .../Tutorial/Examples/backup_monitor.h | 5 + .../Tutorial/Examples/backup_monitor_types.h | 0 .../Tutorial/Examples/heater.c | 40 +++ .../Tutorial/Examples/heater.h | 4 + .../Tutorial/Examples/heater2.c | 40 +++ .../Tutorial/Examples/heater2.h | 4 + .../Tutorial/Examples/heater2_types.h | 0 .../Tutorial/Examples/heater_types.h | 0 TutorialAndDevGuide/Tutorial/Examples/sonar.c | 27 ++ TutorialAndDevGuide/Tutorial/Examples/sonar.h | 3 + .../Tutorial/Examples/sonar_types.h | 0 TutorialAndDevGuide/Tutorial/Interpret.tex | 28 +- TutorialAndDevGuide/Tutorial/Language.tex | 316 ++++++++++-------- TutorialAndDevGuide/Tutorial/example.tex | 143 ++++---- TutorialAndDevGuide/Tutorial/introduction.tex | 235 +++++++------ 29 files changed, 871 insertions(+), 322 deletions(-) create mode 100644 TutorialAndDevGuide/Tutorial/Examples/Causal.hs create mode 100644 TutorialAndDevGuide/Tutorial/Examples/Counter_Answer.hs create mode 100644 TutorialAndDevGuide/Tutorial/Examples/Counter_Problem.hs create mode 100644 TutorialAndDevGuide/Tutorial/Examples/Distance_Monitor.hs create mode 100644 TutorialAndDevGuide/Tutorial/Examples/EvenStream_Answers.hs create mode 100644 TutorialAndDevGuide/Tutorial/Examples/EvenStream_Problem.hs create mode 100644 TutorialAndDevGuide/Tutorial/Examples/Filters.hs create mode 100644 TutorialAndDevGuide/Tutorial/Examples/Heater.hs create mode 100644 TutorialAndDevGuide/Tutorial/Examples/Latch.hs create mode 100644 TutorialAndDevGuide/Tutorial/Examples/Sonar.hs create mode 100644 TutorialAndDevGuide/Tutorial/Examples/Spec.hs create mode 100644 TutorialAndDevGuide/Tutorial/Examples/Streams.hs create mode 100644 TutorialAndDevGuide/Tutorial/Examples/Structs.hs create mode 100644 TutorialAndDevGuide/Tutorial/Examples/backup_monitor.c create mode 100644 TutorialAndDevGuide/Tutorial/Examples/backup_monitor.h create mode 100644 TutorialAndDevGuide/Tutorial/Examples/backup_monitor_types.h create mode 100644 TutorialAndDevGuide/Tutorial/Examples/heater.c create mode 100644 TutorialAndDevGuide/Tutorial/Examples/heater.h create mode 100644 TutorialAndDevGuide/Tutorial/Examples/heater2.c create mode 100644 TutorialAndDevGuide/Tutorial/Examples/heater2.h create mode 100644 TutorialAndDevGuide/Tutorial/Examples/heater2_types.h create mode 100644 TutorialAndDevGuide/Tutorial/Examples/heater_types.h create mode 100644 TutorialAndDevGuide/Tutorial/Examples/sonar.c create mode 100644 TutorialAndDevGuide/Tutorial/Examples/sonar.h create mode 100644 TutorialAndDevGuide/Tutorial/Examples/sonar_types.h diff --git a/TutorialAndDevGuide/Tutorial/Examples/Causal.hs b/TutorialAndDevGuide/Tutorial/Examples/Causal.hs new file mode 100644 index 0000000..ef02151 --- /dev/null +++ b/TutorialAndDevGuide/Tutorial/Examples/Causal.hs @@ -0,0 +1,17 @@ +import Language.Copilot + +import Prelude hiding (drop, (++)) + +fib :: Stream Int32 +fib = [0, 1, 1] ++ ((drop 1 fib) + (drop 2 fib)) + +fastForwardFib :: Stream Int32 +fastForwardFib = drop 1 fib + +delayFib :: Stream Int32 +delayFib = [0] ++ fib + +causal = do + observer "Fibonacci" fib + observer "Leading" fastForwardFib + observer "Lagging" delayFib diff --git a/TutorialAndDevGuide/Tutorial/Examples/Counter_Answer.hs b/TutorialAndDevGuide/Tutorial/Examples/Counter_Answer.hs new file mode 100644 index 0000000..90bda54 --- /dev/null +++ b/TutorialAndDevGuide/Tutorial/Examples/Counter_Answer.hs @@ -0,0 +1,23 @@ +import Language.Copilot + +import Prelude hiding ((++), (==), mod, drop, not) + +fib :: Stream Int32 +fib = [0,1,1] ++ ((drop 1 fib) + (drop 2 fib)) + +resetStream :: Stream Bool +resetStream = 0 == (fib `mod` 4) + +incStream :: Stream Bool +incStream = [False, True, False, True, False, True] ++ incStream + +counter :: Stream Bool -> Stream Bool -> Stream Int32 +counter inc reset = cnt + where + cnt = mux reset 0 (mux inc (z + 1) z) + z = [0] ++ cnt + +spec = do + observer "inc" incStream + observer "reset" resetStream + observer "counter" (counter incStream resetStream) diff --git a/TutorialAndDevGuide/Tutorial/Examples/Counter_Problem.hs b/TutorialAndDevGuide/Tutorial/Examples/Counter_Problem.hs new file mode 100644 index 0000000..ec8a263 --- /dev/null +++ b/TutorialAndDevGuide/Tutorial/Examples/Counter_Problem.hs @@ -0,0 +1,21 @@ +import Language.Copilot + +import Prelude hiding ((++), (==), mod, drop, not) + +fib :: Stream Int32 +fib = [0,1,1] ++ ((drop 1 fib) + (drop 2 fib)) + +resetStream :: Stream Bool +resetStream = 0 == (fib `mod` 4) + +incStream :: Stream Bool +incStream = [False, True, False, True, False, True] ++ incStream + +counter :: Stream Bool -> Stream Bool -> Stream Int32 +counter + + +spec = do + observer "inc" incStream + observer "reset" resetStream + observer "counter" (counter incStream resetStream) diff --git a/TutorialAndDevGuide/Tutorial/Examples/Distance_Monitor.hs b/TutorialAndDevGuide/Tutorial/Examples/Distance_Monitor.hs new file mode 100644 index 0000000..708cc0e --- /dev/null +++ b/TutorialAndDevGuide/Tutorial/Examples/Distance_Monitor.hs @@ -0,0 +1,19 @@ + +module Main where + +import Language.Copilot +import Copilot.Compile.C99 + +import Prelude hiding ((>), (<=), (&&), (>=)) + +cm :: Stream Int32 +cm = extern "distance" Nothing + + +spec = do + trigger "green" (cm > 18) [arg cm] + trigger "yellow" ((18 >= cm) && (cm > 6)) [arg cm] + trigger "red" (cm <= 6) [arg cm] + +-- Compile the spec +main = reify spec >>= compile "backup_monitor" diff --git a/TutorialAndDevGuide/Tutorial/Examples/EvenStream_Answers.hs b/TutorialAndDevGuide/Tutorial/Examples/EvenStream_Answers.hs new file mode 100644 index 0000000..e559fa3 --- /dev/null +++ b/TutorialAndDevGuide/Tutorial/Examples/EvenStream_Answers.hs @@ -0,0 +1,17 @@ +import Language.Copilot hiding (even) + +import Prelude hiding (even, (++), (==), mod) + +nats :: Stream Int32 +nats = [1] ++ (nats + 1) + +evenStream :: Stream Int32 +evenStream = nats * 2 + +even :: Stream Int32 -> Stream Bool +even x = 0 == (x `mod` 2) + +spec = do + observer "nats" nats + observer "evens" evenStream + observer "Even?" (even (nats + evenStream)) diff --git a/TutorialAndDevGuide/Tutorial/Examples/EvenStream_Problem.hs b/TutorialAndDevGuide/Tutorial/Examples/EvenStream_Problem.hs new file mode 100644 index 0000000..3078b10 --- /dev/null +++ b/TutorialAndDevGuide/Tutorial/Examples/EvenStream_Problem.hs @@ -0,0 +1,17 @@ +import Language.Copilot hiding (even) + +import Prelude hiding (even, (++), (==), mod) + +nats :: Stream Int32 +nats = [1] ++ (nats + 1) + +evenStream :: Stream Int32 +evenStream = nats * 2 + +even :: Stream Int32 -> Stream Bool +even + +spec = do + observer "nats" nats + observer "evens" evenStream + observer "Even?" (even (nats + evenStream)) diff --git a/TutorialAndDevGuide/Tutorial/Examples/Filters.hs b/TutorialAndDevGuide/Tutorial/Examples/Filters.hs new file mode 100644 index 0000000..291ad57 --- /dev/null +++ b/TutorialAndDevGuide/Tutorial/Examples/Filters.hs @@ -0,0 +1,47 @@ +import Language.Copilot + +import Prelude hiding (drop, (++), div ) + +fib :: Stream Int32 +fib = [0,1,1] ++ (drop 1 fib + drop 2 fib) + +fibdelayed :: Stream Int32 +fibdelayed = [0] ++ fib + +diff :: Stream Int32 +diff = fib - fibdelayed + +gain :: Stream Int32 +gain = fib + 2 + +twoTermAverage :: Stream Int32 +twoTermAverage = (fib + fibdelayed) `div` 2 + +centralDifference :: Stream Int32 +centralDifference = (fib - ([0] ++ fibdelayed)) `div` 2 + +recursive :: Stream Int32 +recursive = fib - diff + +gainFilter = do + observer "fib" fib + observer "Simple Gain" gain + +diffFilter = do + observer "fib" fib + observer "fib delayed" fibdelayed + observer "Difference Filter" diff + observer "Recursive Diff" recursive + +pureDelay = do + observer "fib" fib + observer "Pure Delay" fibdelayed + +ttAverage = do + observer "fib" fib + observer "Two Term Average" twoTermAverage + +cDiff = do + observer "fib" fib + observer "Central Difference" centralDifference + diff --git a/TutorialAndDevGuide/Tutorial/Examples/Heater.hs b/TutorialAndDevGuide/Tutorial/Examples/Heater.hs new file mode 100644 index 0000000..e27c67d --- /dev/null +++ b/TutorialAndDevGuide/Tutorial/Examples/Heater.hs @@ -0,0 +1,32 @@ +-- 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 Celsius. + +module Main 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 Celsius. +-- 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 "heater2" diff --git a/TutorialAndDevGuide/Tutorial/Examples/Latch.hs b/TutorialAndDevGuide/Tutorial/Examples/Latch.hs new file mode 100644 index 0000000..2a35e22 --- /dev/null +++ b/TutorialAndDevGuide/Tutorial/Examples/Latch.hs @@ -0,0 +1,19 @@ +import Language.Copilot + +import Prelude hiding ((++), (==), mod, drop, not) + +fib :: Stream Int32 +fib = [0,1,1] ++ ((drop 1 fib) + (drop 2 fib)) + +boolStream:: Stream Bool +boolStream = 0 == (fib `mod` 4) + +latch :: Stream Bool -> Stream Bool +latch x = y + where + y = mux x (not z) z + z = [False] ++ y + +spec = do + observer "x" boolStream + observer "y" (latch boolStream) diff --git a/TutorialAndDevGuide/Tutorial/Examples/Sonar.hs b/TutorialAndDevGuide/Tutorial/Examples/Sonar.hs new file mode 100644 index 0000000..a81da34 --- /dev/null +++ b/TutorialAndDevGuide/Tutorial/Examples/Sonar.hs @@ -0,0 +1,15 @@ + +import Language.Copilot +import Copilot.Compile.C99 + +import qualified Prelude as P + +cm :: Stream Int32 +cm = extern "distance" Nothing + + +spec = do + trigger "out_of_range" (cm > 18) [arg cm] + +-- Compile the spec +main = reify spec >>= compile "sonar" diff --git a/TutorialAndDevGuide/Tutorial/Examples/Spec.hs b/TutorialAndDevGuide/Tutorial/Examples/Spec.hs new file mode 100644 index 0000000..224dc28 --- /dev/null +++ b/TutorialAndDevGuide/Tutorial/Examples/Spec.hs @@ -0,0 +1,19 @@ +import Language.Copilot + +import qualified Prelude as P + +nats :: Stream Int32 +nats = [0] ++ (1 + nats) + +evenNumberNumber :: Stream Int32 -> Stream Bool +evenNumber n = n `mod` 2 == 0 + +oddNumber :: Stream Int32 -> Stream Bool +oddNumber n2 = n2 `mod` 2 == 1 + +difEvens :: Stream Int32 +difEvens = nats - ([0] ++ nats) + +spec = do + trigger "trigger1" (evenNumber nats) [arg nats, arg (oddNumber nats)] + trigger "trigger2" (oddNumber nats) [arg nats] diff --git a/TutorialAndDevGuide/Tutorial/Examples/Streams.hs b/TutorialAndDevGuide/Tutorial/Examples/Streams.hs new file mode 100644 index 0000000..22e82eb --- /dev/null +++ b/TutorialAndDevGuide/Tutorial/Examples/Streams.hs @@ -0,0 +1,17 @@ +import Language.Copilot + +import qualified Prelude as P + +x :: Stream Int32 +x = 5 + 5 + +y :: Stream Int32 +y = x * x + +z :: Stream Bool +z = x == 10 && y < 200 + +printStreams = do + observer "x" x + observer "y" y + observer "z" z diff --git a/TutorialAndDevGuide/Tutorial/Examples/Structs.hs b/TutorialAndDevGuide/Tutorial/Examples/Structs.hs new file mode 100644 index 0000000..bd22368 --- /dev/null +++ b/TutorialAndDevGuide/Tutorial/Examples/Structs.hs @@ -0,0 +1,32 @@ +{-#LANGUAGE DataKinds #-} + +module Struct where + +import Language.Copilot + +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 + +toValues :: Vec -> [Value Vec] +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 + + +-- Trigger that always executes, splits the vec into seperate args. +spec = do + observer "split x" (vecs # x) + observer "split y" (vecs # y) diff --git a/TutorialAndDevGuide/Tutorial/Examples/backup_monitor.c b/TutorialAndDevGuide/Tutorial/Examples/backup_monitor.c new file mode 100644 index 0000000..880b4dd --- /dev/null +++ b/TutorialAndDevGuide/Tutorial/Examples/backup_monitor.c @@ -0,0 +1,53 @@ +#include +#include +#include +#include +#include + +#include "backup_monitor_types.h" +#include "backup_monitor.h" + +static int32_t distance_cpy; + +bool green_guard(void) { + return (distance_cpy) > ((int32_t)(18)); +} + +int32_t green_arg0(void) { + return distance_cpy; +} + +bool yellow_guard(void) { + return (((int32_t)(18)) >= (distance_cpy)) && ((distance_cpy) > ((int32_t)(6))); +} + +int32_t yellow_arg0(void) { + return distance_cpy; +} + +bool red_guard(void) { + return (distance_cpy) <= ((int32_t)(6)); +} + +int32_t red_arg0(void) { + return distance_cpy; +} + +void step(void) { + int32_t green_arg_temp0; + int32_t yellow_arg_temp0; + int32_t red_arg_temp0; + (distance_cpy) = (distance); + if ((green_guard)()) { + {(green_arg_temp0) = ((green_arg0)()); + (green)((green_arg_temp0));} + }; + if ((yellow_guard)()) { + {(yellow_arg_temp0) = ((yellow_arg0)()); + (yellow)((yellow_arg_temp0));} + }; + if ((red_guard)()) { + {(red_arg_temp0) = ((red_arg0)()); + (red)((red_arg_temp0));} + }; +} diff --git a/TutorialAndDevGuide/Tutorial/Examples/backup_monitor.h b/TutorialAndDevGuide/Tutorial/Examples/backup_monitor.h new file mode 100644 index 0000000..a549796 --- /dev/null +++ b/TutorialAndDevGuide/Tutorial/Examples/backup_monitor.h @@ -0,0 +1,5 @@ +extern int32_t distance; +void green(int32_t green_arg0); +void yellow(int32_t yellow_arg0); +void red(int32_t red_arg0); +void step(void); diff --git a/TutorialAndDevGuide/Tutorial/Examples/backup_monitor_types.h b/TutorialAndDevGuide/Tutorial/Examples/backup_monitor_types.h new file mode 100644 index 0000000..e69de29 diff --git a/TutorialAndDevGuide/Tutorial/Examples/heater.c b/TutorialAndDevGuide/Tutorial/Examples/heater.c new file mode 100644 index 0000000..a78ac34 --- /dev/null +++ b/TutorialAndDevGuide/Tutorial/Examples/heater.c @@ -0,0 +1,40 @@ +#include +#include +#include +#include +#include + +#include "heater_types.h" +#include "heater.h" + +static uint8_t temperature_cpy; + +bool heaton_guard(void) { +/*low level c code */ +} + +float heaton_arg0(void) { +/*low level c code */ +} + +bool heatoff_guard(void) { +/*low level c code */ +} + +float heatoff_arg0(void) { +/*low level c code */ +} + +void step(void) { + float heaton_arg_temp0; + float heatoff_arg_temp0; + (temperature_cpy) = (temperature); + if ((heaton_guard)()) { + {(heaton_arg_temp0) = ((heaton_arg0)()); + (heaton)((heaton_arg_temp0));} + }; + if ((heatoff_guard)()) { + {(heatoff_arg_temp0) = ((heatoff_arg0)()); + (heatoff)((heatoff_arg_temp0));} + }; +} diff --git a/TutorialAndDevGuide/Tutorial/Examples/heater.h b/TutorialAndDevGuide/Tutorial/Examples/heater.h new file mode 100644 index 0000000..7aaebc5 --- /dev/null +++ b/TutorialAndDevGuide/Tutorial/Examples/heater.h @@ -0,0 +1,4 @@ +extern uint8_t temperature; +void heaton(float heaton_arg0); +void heatoff(float heatoff_arg0); +void step(void); diff --git a/TutorialAndDevGuide/Tutorial/Examples/heater2.c b/TutorialAndDevGuide/Tutorial/Examples/heater2.c new file mode 100644 index 0000000..a23b749 --- /dev/null +++ b/TutorialAndDevGuide/Tutorial/Examples/heater2.c @@ -0,0 +1,40 @@ +#include +#include +#include +#include +#include + +#include "heater2_types.h" +#include "heater2.h" + +static uint8_t temperature_cpy; + +bool heaton_guard(void) { + return ((((float)(temperature_cpy)) * (((float)(150.0f)) / ((float)(255.0f)))) - ((float)(50.0f))) < ((float)(18.0f)); +} + +float heaton_arg0(void) { + return (((float)(temperature_cpy)) * (((float)(150.0f)) / ((float)(255.0f)))) - ((float)(50.0f)); +} + +bool heatoff_guard(void) { + return ((((float)(temperature_cpy)) * (((float)(150.0f)) / ((float)(255.0f)))) - ((float)(50.0f))) > ((float)(21.0f)); +} + +float heatoff_arg0(void) { + return (((float)(temperature_cpy)) * (((float)(150.0f)) / ((float)(255.0f)))) - ((float)(50.0f)); +} + +void step(void) { + float heaton_arg_temp0; + float heatoff_arg_temp0; + (temperature_cpy) = (temperature); + if ((heaton_guard)()) { + {(heaton_arg_temp0) = ((heaton_arg0)()); + (heaton)((heaton_arg_temp0));} + }; + if ((heatoff_guard)()) { + {(heatoff_arg_temp0) = ((heatoff_arg0)()); + (heatoff)((heatoff_arg_temp0));} + }; +} diff --git a/TutorialAndDevGuide/Tutorial/Examples/heater2.h b/TutorialAndDevGuide/Tutorial/Examples/heater2.h new file mode 100644 index 0000000..7aaebc5 --- /dev/null +++ b/TutorialAndDevGuide/Tutorial/Examples/heater2.h @@ -0,0 +1,4 @@ +extern uint8_t temperature; +void heaton(float heaton_arg0); +void heatoff(float heatoff_arg0); +void step(void); diff --git a/TutorialAndDevGuide/Tutorial/Examples/heater2_types.h b/TutorialAndDevGuide/Tutorial/Examples/heater2_types.h new file mode 100644 index 0000000..e69de29 diff --git a/TutorialAndDevGuide/Tutorial/Examples/heater_types.h b/TutorialAndDevGuide/Tutorial/Examples/heater_types.h new file mode 100644 index 0000000..e69de29 diff --git a/TutorialAndDevGuide/Tutorial/Examples/sonar.c b/TutorialAndDevGuide/Tutorial/Examples/sonar.c new file mode 100644 index 0000000..1aa0b0a --- /dev/null +++ b/TutorialAndDevGuide/Tutorial/Examples/sonar.c @@ -0,0 +1,27 @@ +#include +#include +#include +#include +#include + +#include "sonar_types.h" +#include "sonar.h" + +static int32_t distance_cpy; + +bool out_of_range_guard(void) { + return (distance_cpy) > ((int32_t)(18)); +} + +int32_t out_of_range_arg0(void) { + return distance_cpy; +} + +void step(void) { + int32_t out_of_range_arg_temp0; + (distance_cpy) = (distance); + if ((out_of_range_guard)()) { + {(out_of_range_arg_temp0) = ((out_of_range_arg0)()); + (out_of_range)((out_of_range_arg_temp0));} + }; +} diff --git a/TutorialAndDevGuide/Tutorial/Examples/sonar.h b/TutorialAndDevGuide/Tutorial/Examples/sonar.h new file mode 100644 index 0000000..db9f2e4 --- /dev/null +++ b/TutorialAndDevGuide/Tutorial/Examples/sonar.h @@ -0,0 +1,3 @@ +extern int32_t distance; +void out_of_range(int32_t out_of_range_arg0); +void step(void); diff --git a/TutorialAndDevGuide/Tutorial/Examples/sonar_types.h b/TutorialAndDevGuide/Tutorial/Examples/sonar_types.h new file mode 100644 index 0000000..e69de29 diff --git a/TutorialAndDevGuide/Tutorial/Interpret.tex b/TutorialAndDevGuide/Tutorial/Interpret.tex index 2ab6176..0270400 100644 --- a/TutorialAndDevGuide/Tutorial/Interpret.tex +++ b/TutorialAndDevGuide/Tutorial/Interpret.tex @@ -2,7 +2,8 @@ \section{Interpreting} \label{interpcompile} The Copilot RV framework comes with both an interpreter and a -compiler. We will address compiling in \hyperref[sec:complete_example]{section 4} with a complete example. +compiler. We will address compiling in \hyperref[sec:complete_example]{Section 4} + with a complete example. \noindent To use the language, your Haskell module should contain the following import: % \begin{code} @@ -21,30 +22,13 @@ \subsection{Interpreting Copilot} for you to follow allong. \texttt{Spec.hs} is the following Copilot program: % \lstinputlisting[language = Copilot, numbers = left]{Examples/Spec.hs} -%import Language.Copilot hiding (even, odd) -% -%import qualified Prelude as P hiding ((++),(==), mod, even, odd) -% -%nats :: Stream Int32 -%nats = [0] ++ (1 + nats) -% -%even :: Stream Int32 -> Stream Bool -%even n = n `mod` 2 == 0 -% -%odd :: Stream Int32 -> Stream Bool -%odd n2 = n2 `mod` 2 == 1 -% -%spec = do -% trigger "trigger1" (even nats) [arg nats, arg $ odd nats] -% trigger "trigger2" (odd nats) [arg nats] -%\end{lstlisting} -% $ + \begin{description} \item[Line 1] Here we inclued the Copilot Language so that we gain access to the front end language. - \item[Line 3] Here we include the Prelude so that we can hide base Haskell syntax - that we have redefined. If this is not included you will get an \texttt{Ambiguious - Occurance} error. + \item[Line 3] Here we include the Prelude. Notice that we hide base Haskell + syntax for functions that we define for use on streams . If this is not + included you will get an \texttt{Ambiguious Occurance} error. \item[Line 5-12] Here we define data streams as input and output data streams. We go over defining functions as streams in Section 3 of this tutorial. \item[Line 14-16] Here {\tt nats} is the stream of natural numbers, and {\tt even} and {\tt odd} diff --git a/TutorialAndDevGuide/Tutorial/Language.tex b/TutorialAndDevGuide/Tutorial/Language.tex index a770d0f..9f11f8d 100644 --- a/TutorialAndDevGuide/Tutorial/Language.tex +++ b/TutorialAndDevGuide/Tutorial/Language.tex @@ -1,12 +1,13 @@ -\section{Language}~\label{sec:language} -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: +\section{Language}~\label{sec:language} 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 Sample external variables, structs, and arrays. \item Update internal variables. \item Fire external triggers. (In case the specification is violated.) \item Update observers (for debugging purpose). @@ -15,7 +16,9 @@ \section{Language}~\label{sec:language} \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} @@ -23,14 +26,20 @@ \section{Language}~\label{sec:language} \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$, +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. \subsection{Streams as Lazy-Lists} \label{sec:stream} This subsection is to show users that are familiar with Haskell that streams -function like lazy lists. For those that are not as familiar with Haskell this -subsection can be omitted. However, there is a few useful definitions of data +function like lazy lists. +% +For those that are not as familiar with Haskell this +subsection can be omitted. +% +However, there is a few useful definitions of data streams as examples. % \begin{lstlisting}[language = Copilot, frame = single] @@ -62,15 +71,16 @@ \subsection{Streams as Lazy-Lists} \label{sec:stream} \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 +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: +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 @@ -79,6 +89,9 @@ \subsection{Functions on Streams} \label{sec:FnOnStreams} % Applying {\tt even} on {\tt nats} (defined above) yields the sequence $\{T, F, T, F, T, F, \dots\}$. +% +This function sould be familiar to the one that +we had shown in {\tt Spec.hs} from \hyperref[interpcompile]{Section 2.1}. \end{example} If a function is required to return multiple results, we simply use plain @@ -100,7 +113,8 @@ \subsection{Functions on Streams} \label{sec:FnOnStreams} of the right operand. \end{example} -Here we give you another example \texttt{Streams.hs} found in the ./Examples directory: +Here we give you another specification \texttt{Streams.hs} found in the ./Examples directory +that you are able to run in the interpreter to see how the operators work on the streams: \noindent %\begin{minipage}{0.3\textwidth} @@ -112,14 +126,31 @@ \subsection{Functions on Streams} \label{sec:FnOnStreams} \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} +\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} + +\noindent For more practice creating and operating on streams you can solve the +following problem. -\noindent Interpret this the same way that you did in Section 2 and see -the results yourself. + +{\tt Problem:} We have given you a specification with two streams in the +./Examples. +% +One stream is a stream of natural numbers and the other is a stream of purely +even numbers. +% +Create a function that will check if a stream of numbers is even or not, we +have given you the type specification. +% +Once you have created the function, you should be able to compile interpret the +specification. +% + +\emph{We have also provided you with the answer if you get stuck.} +% + +\lstinputlisting[language = Copilot, frame = single, numbers = left]{Examples/EvenStream_Problem.hs} \subsection{Causality} Two types of \emph{temporal} operators are provided, one for delaying streams and one for @@ -130,49 +161,151 @@ \subsection{Causality} 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}: +Here {\tt xs ++ s} prepends the list {\tt xs} at the front of the stream {\tt +s}. % -\begin{lstlisting}[language = Copilot, frame = single] -w = [5,6,7] ++ x +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\}$. Add this to the Streams.hs -specification and add a trigger so you can see the result for yourself. +evaluates to the sequence $\mathtt{w} \leadsto \{5, 6, 7, 10, 10, 10, \dots\}$. +% +Add this to the Streams.hs specification and add a trigger so you can see the +result for yourself. The expression {\tt drop k s} skips the first {\tt k} values of the stream {\tt - s}, returning the remainder of the stream. +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 +\begin{lstlisting}[language = Copilot, frame = single] u = drop 2 w \end{lstlisting} % -which yields the sequence -$\mathtt{u} \leadsto \{7, 10, 10, 10, \dots\}$. +which yields the sequence $\mathtt{u} \leadsto \{7, 10, 10, 10, \dots\}$. -Copilot specifications must be \emph{causal}, informally meaning that -stream values cannot depend on future values. Our example \texttt{Causal.hs} -in the ./Examples directory shows the use of {\tt drop} and {\tt ++} by defining -a fibonachi series and then creates a leading and lagging stream: +Copilot specifications must be \emph{causal}, informally meaning that stream +values cannot depend on future values. +% +Our example \texttt{Causal.hs} in the ./Examples directory shows the use of +{\tt drop} and {\tt ++} by defining a fibonachi series and then creates a +leading and lagging stream: % \lstinputlisting[language = Copilot, frame = single ]{Examples/Causal.hs} % -But if instead {\tt fastForwardFib} is defined as {\tt fastforwardFib = drop 4 fib} -, 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 fib} - to be generated before producing values for {\tt fastForwardFib}. This is not possible since -Copilot programs may take inputs in real-time from the environment (see -Section~\ref{subsec:interacting}). +But if instead {\tt fastForwardFib} is defined as {\tt fastforwardFib = drop 4 +fib} , 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 fib} to be generated before +producing values for {\tt fastForwardFib}. +% +This is not possible since Copilot programs may take inputs in real-time from +the environment (see Section~\ref{subsec:interacting}). + +Being able to look ahead and behind in streams is really useful for thing like +rate of change. +% +For example if you were intrested in monitoring how fast your car was +accelerating or the rate of drain on a battery. +% +If you would like more practice with the Copilot language, try adding in an +observer that shows how much change there was between the leading and the +lagging stream for our fibonachi 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{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 the +./Examples directory with Specification {\tt Latch.hs}. + +\begin{center} +\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} +\end{center} +\end{example} + +\lstinputlisting[language = Copilot, frame = single, numbers = left]{Examples/Latch.hs} + +\begin{description} + \item[Line 1-4] Standard inclueds to include the Copilot language and remove + items defined in the Copilot library from the prelude. + \item[Line 5-9] This is a set of arbitrary functions to create a stream of + trues and falses to demonstrate the latch. + \item[Lines 11-15] demonstrate the implementation of an if-then-else statement in copilot. In order to do if-then-else statements we have defined {\tt mux}. +\end{description} + +% +\begin{lstlisting}[language = Copilot, frame = single] +mux :: Typed a => Stream Bool -> Stream a -> Stream a -> Stream a +\end{lstlisting} +% + +The expression {\tt mux x y z} says that if {\tt x} is true then return {\tt +y}, but if {\tt x} is false then return {\tt z}. + +\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 +table below. + +\begin{center} +\begin{minipage}{0.25\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}$\\ +\hline +\end{tabular} +\end{minipage} +\end{center} +\end{example} + +{\tt Problem:} Now that you have an understanding of how to implement if then operations on streams. +% +Attempt to write a specification for the example above. +% +We have started the specification for you in the ./Examples directory. + +\lstinputlisting[language = Copilot, frame = single, numbers = left]{Examples/Counter_Problem.hs} -Being able to look ahead and behind in streams is really useful for thing like rate of change -for example if you were intrested in monitoring how fast your car was accelerating or the rate -of drain on a battery. If you would like more practice with the Copilot language try adding in -an observer that shows how much change there was between the leading and the lagging stream for -our fibonachi example. \subsection{Structs} When monitoring embedded systems the data that needs to be observed is often in a struct. @@ -307,87 +440,6 @@ \subsubsection*{Example code} \lstinputlisting[language = Copilot, frame = single, numbers = left]{Examples/Structs.hs} % -\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). - -\lstinputlisting[language = Copilot, frame = single, numbers = left]{Examples/Latch.hs} - -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. - -\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 diff --git a/TutorialAndDevGuide/Tutorial/example.tex b/TutorialAndDevGuide/Tutorial/example.tex index 823b59d..763f451 100644 --- a/TutorialAndDevGuide/Tutorial/example.tex +++ b/TutorialAndDevGuide/Tutorial/example.tex @@ -45,55 +45,55 @@ \subsection{Compiling Copilot} \label{sec:compiling} \subsection{C Code} Lets start of with the C program our monitor to connect to. -\begin{lstlisting}[language=c, numbers=left] -#include -#include -#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} +\lstinputlisting[language = c, frame = single, numbers = left]{Examples/heater.c} +%\begin{lstlisting}[language=c, numbers=left] +%#include +%#include +% +%#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 + \item[Line 7] 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 + \item[Line 8] 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 + \item[Line 10] 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 + \item[Line 12-26] Functions that turn on and turn off the heater, low-level details are provided. - \item[Line 18-22] Our infinite main-loop: + \item[Line 28-39] Our infinite main-loop: \begin{description} - \item[Line 19] Update our global temperature variable by reading it from + \item[Line 31] 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. + \item[Line 32-35/36-39] Check our guards that we defined above. \end{description} \end{description} @@ -109,42 +109,43 @@ \subsection{Specification} 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} +\lstinputlisting[language = Copilot, frame = single, numbers = left]{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. diff --git a/TutorialAndDevGuide/Tutorial/introduction.tex b/TutorialAndDevGuide/Tutorial/introduction.tex index 8e3ce0f..ccf29de 100644 --- a/TutorialAndDevGuide/Tutorial/introduction.tex +++ b/TutorialAndDevGuide/Tutorial/introduction.tex @@ -1,72 +1,89 @@ \section{Introduction} \label{sec:introduction} -  + Neither formal verification nor testing can ensure system reliability. +% Over 25 years ago, Butler and Finelli showed that testing alone cannot verify the reliability of ultra-critical software~\cite{butler}. -\emph{Runtime verification} (RV)~\cite{monitors}, where monitors -detect and respond to property violations at runtime, has the -potential to enable the safe operation of safety-critical systems that -are too complex to formally verify or fully test. Technically -speaking, a RV monitor takes a logical specification $\phi$ and -execution trace $\tau$ of state information of the system under -observation (SUO) and decides whether $\tau$ satisfies $\phi$. The -\emph{Simplex Architecture}~\cite{simplex} provides a model -architectural pattern for RV, where a monitor checks that the -executing SUO satisfies a specification and, if the property is -violated, the RV system will switch control to a more conservative -component that can be assured using conventional means that -\emph{steers} the system into a safe state. \emph{High-assurance} RV -provides an assured level of safety even when the SUO itself cannot be -verified by conventional means. - - -Copilot is a RV framework for specifying and generating monitors for C programs that is -embedded into the functional programming language Haskell -\cite{PeytonJones02}. A working knowledge of Haskell is not necessary to use -Copilot at a basic level. However, knowledge of Haskell will significantly aid you in writing Copilot specifications; a variety of books and free web resources introduce Haskell. -Copilot uses Haskell language extensions -specific to the Glasgow Haskell Compiler (GHC). +% +\emph{Runtime verification} (RV)~\cite{monitors}, where monitors detect and +respond to property violations at runtime, has the potential to enable the safe +operation of safety-critical systems that are too complex to formally verify or +fully test. +% +Technically speaking, a RV monitor takes a logical specification $\phi$ and +execution trace $\tau$ of state information of the system under observation +(SUO) and decides whether $\tau$ satisfies $\phi$. +% +The \emph{Simplex Architecture}~\cite{simplex} provides a model architectural +pattern for RV, where a monitor checks that the executing SUO satisfies a +specification and, if the property is violated, the RV system will switch +control to a more conservative component that can be assured using conventional +means that \emph{steers} the system into a safe state. +% +\emph{High-assurance} RV provides an assured level of safety even when the SUO +itself cannot be verified by conventional means. +%% + +Copilot is a RV framework for specifying and generating monitors for C programs +that is embedded into the functional programming language Haskell +\cite{PeytonJones02}. +% + A working knowledge of Haskell is not necessary to use Copilot at a basic +level. +% + However, knowledge of Haskell will significantly aid you in writing Copilot +specifications; a variety of books and free web resources introduce Haskell. +% + Copilot uses Haskell language extensions specific to the Glasgow Haskell +Compiler (GHC). \subsection{Target Application Domain} \label{domain} Copilot is a domain-specific language tailored to programming \emph{runtime -monitors} for \emph{hard real-time}, \emph{distributed}, \emph{reactive systems}. -Briefly, a runtime monitor is program that runs concurrently with a target program -with the sole purpose of assuring that the target program behaves in accordance with a -pre-established specification. Copilot is a language for writing such specifications. +monitors} for \emph{hard real-time}, \emph{distributed}, \emph{reactive +systems}. +% +Briefly, a runtime monitor is program that runs concurrently with a target +program with the sole purpose of assuring that the target program behaves in +accordance with a pre-established specification. +% + Copilot is a language for writing such specifications. +% A reactive system is a system that responds continuously to its environment. +% All data to and from a reactive system are communicated progressively during -execution. Reactive systems differ from transformational systems which transform -data in a single pass and then terminate, as for example compilers and numerical +execution. +% + Reactive systems differ from transformational systems which transform data in +a single pass and then terminate, as for example compilers and numerical computation software. +% -A hard real-time system is a system that has a statically bounded execution time -and memory usage. Typically, hard real-time systems are used in -mission-critical software, such as avionics, medical equipment, and nuclear power -plants; hence, occasional dropouts in the response time or crashes are not -tolerated. +A hard real-time system is a system that has a statically bounded execution +time and memory usage. +% + Typically, hard real-time systems are used in mission-critical software, such +as avionics, medical equipment, and nuclear power plants; hence, occasional +dropouts in the response time or crashes are not tolerated. -A distributed system is a system which is layered out on multiple pieces of hardware. -The distributed systems we consider are all synchronized, i.e., all components agree on -a shared global clock. +A distributed system is a system which is layered out on multiple pieces of +hardware. +% +The distributed systems we consider are all synchronized, i.e., all components +agree on a shared global clock. \subsection{Installation} \label{sec:install} Before downloading the copilot framework, you must first install an up-to-date version of GHC (the minimal required version is 8.0). -The easiest way to do this is to download and install the Haskell Platform, -which is freely distributed from here: - -\begin{center} -\url{http://hackage.haskell.org/platform} -\end{center} +% -\noindent Because Copilot compiles to C code, you must also install a C compiler such as GCC (\url{https://gcc.gnu.org/install/}). After having installed the Haskell Platform and C compiler, Copilot can be downloaded and +\noindent Copilot compiles to C code, you must install a C compiler such as GCC (\url{https://gcc.gnu.org/install/}). After having installed the Haskell Platform and C compiler, Copilot can be downloaded and installed in the following two ways: \begin{itemize} @@ -119,60 +136,84 @@ \subsection{Structure} \label{structure} \url{https://github.com/Copilot-Language/Copilot/tree/master/Examples}. \subsection{Sampling} \label{sampling} -The idea of sampling representative data from a large set of data is well -established in data science and engineering. For instance, in digital -signal processing, a signal such as music is sampled at a high enough -rate to obtain enough discrete points to represent the physical sound -wave. The fidelity of the recording is dependant on the sampling -rate. Sampling a state variable of an executing program is similar, -but variables are rarely continuous signals so they lack the nice -properties of continuity. + The idea of sampling representative data from a large set of data is well +established in data science and engineering. +% + For instance, in digital signal processing, a signal such as music is sampled +at a high enough rate to obtain enough discrete points to represent the +physical sound wave. +% + The fidelity of the recording is dependant on the sampling rate. +% + Sampling a state variable of an executing program is similar, but variables +are rarely continuous signals so they lack the nice properties of continuity. +% Monitoring based on sampling state-variables has historically been disregarded as a runtime monitoring approach, for good reason: without the assumption of -synchrony between the monitor and observed software, monitoring via sampling may -lead to false positives and false negatives~\cite{DwyerDE08}. For example, -consider the property $(0;1;1)^*$, written as a regular expression, denoting the -sequence of values a monitored variable may take. If the monitor samples the -variable at the inappropriate time, then both false negatives (the monitor -erroneously rejects the sequence of values) and false positives (the monitor -erroneously accepts the sequence) are possible. For example, if the actual -sequence of values is $0,1,1,0,1,1$, then an observation of $0,1,1,1,1$ is a -false negative by skipping a value, and if the actual sequence is $0,1,0,1,1$, -then an observation of $0,1,1,0,1,1$ is a false positive by sampling a value -twice. - - - -However, in a hard real-time context, sampling is a suitable strategy. Often, -the purpose of real-time programs is to deliver output signals at a predicable -rate and properties of interest are generally data-flow oriented. In this -context, and under the assumption that the monitor and the observed program -share a global clock and a static periodic schedule, while false positives are -possible, false negatives are not. A false positive is possible, for example, -if the program does not execute according to its schedule but just happens to -have the expected values when sampled. If a monitor samples an unacceptable -sequence of values, then either the program is in error, the monitor is in -error, or they are not synchronized, all of which are faults to be reported. - -Most of the popular runtime monitoring frameworks inline monitors in -the observed program to avoid the aforementioned problems with -sampling. However, inlining monitors changes the real-time behavior -of the observed program, perhaps in unpredicable ways. -Solutions that -introduce such unpredictability are not a viable solution for -ultra-critical hard real-time systems. In a sampling-based approach, -the monitor can be integrated as a separate scheduled process during -available time slices (this is made possible by generating efficient -constant-time monitors). Indeed, sampling-based monitors may even be -scheduled on a separate processor (albeit doing so requires additional -synchronization mechanisms), ensuring time and space partitioning from -the observed programs. Such an architecture may even be necessary if -the monitored program is physically distributed. - -When deciding whether to use Copilot to monitor systems that are not hard real-time, the user must determine if -sampling is suitable to capture the errors and faults of interest in the SUO. In many cyber-physical systems, the trace being monitored is -coming from sensors measuring physical data such as GPS coordinates, air speed, and actuation signals. These continuous signals do not -change abruptly so as long as it is sampled at a suitable rate, that usually must be determined experimentally, sampling is sufficient. +synchrony between the monitor and observed software, monitoring via sampling +may lead to false positives and false negatives~\cite{DwyerDE08}. +% + For example, consider the property $(0;1;1)^*$, written as a regular +expression, denoting the sequence of values a monitored variable may take. +% + If the monitor samples the variable at the inappropriate time, then both false +negatives (the monitor erroneously rejects the sequence of values) and false +positives (the monitor erroneously accepts the sequence) are possible. +% + For example, if the actual sequence of values is $0,1,1,0,1,1$, then an +observation of $0,1,1,1,1$ is a false negative by skipping a value, and if the +actual sequence is $0,1,0,1,1$, then an observation of $0,1,1,0,1,1$ is a false +positive by sampling a value twice. +% + + +However, in a hard real-time context, sampling is a suitable strategy. +% + Often, the purpose of real-time programs is to deliver output signals at a +predicable rate and properties of interest are generally data-flow oriented. +% + In this context, and under the assumption that the monitor and the observed +program share a global clock and a static periodic schedule, while false +positives are possible, false negatives are not. +% + A false positive is possible, for example, if the program does not execute +according to its schedule but just happens to have the expected values when +sampled. +% + If a monitor samples an unacceptable sequence of values, then either the +program is in error, the monitor is in error, or they are not synchronized, all +of which are faults to be reported. +% + +Most of the popular runtime monitoring frameworks inline monitors in the +observed program to avoid the aforementioned problems with sampling. +% + However, inlining monitors changes the real-time behavior of the observed +program, perhaps in unpredicable ways. +% +Solutions that introduce such unpredictability are not a viable solution for +ultra-critical hard real-time systems. +% + In a sampling-based approach, the monitor can be integrated as a separate +scheduled process during available time slices (this is made possible by +generating efficient constant-time monitors). +% + Indeed, sampling-based monitors may even be scheduled on a separate processor +(albeit doing so requires additional synchronization mechanisms), ensuring time +and space partitioning from the observed programs. +% + Such an architecture may even be necessary if the monitored program is +physically distributed. + +When deciding whether to use Copilot to monitor systems that are not hard +real-time, the user must determine if sampling is suitable to capture the +errors and faults of interest in the SUO. In many cyber-physical systems, the +trace being monitored is coming from sensors measuring physical data such as +GPS coordinates, air speed, and actuation signals. +% + These continuous signals do not change abruptly so as long as it is sampled at +a suitable rate, that usually must be determined experimentally, sampling is +sufficient. From 47c4326508161cb7657090181febd7597a1ed463 Mon Sep 17 00:00:00 2001 From: Will Pogge Date: Thu, 20 Jul 2023 12:28:23 -0400 Subject: [PATCH 8/9] Tutorial rewrite --- .../Tutorial/Examples/Sonar.hs | 12 +++- TutorialAndDevGuide/Tutorial/Examples/sonar.c | 40 +++++++++++--- TutorialAndDevGuide/Tutorial/Examples/sonar.h | 4 +- TutorialAndDevGuide/Tutorial/Interpret.tex | 2 +- TutorialAndDevGuide/Tutorial/Language.tex | 12 ++-- TutorialAndDevGuide/Tutorial/example.tex | 10 ++-- TutorialAndDevGuide/Tutorial/introduction.tex | 55 ++++++------------- 7 files changed, 78 insertions(+), 57 deletions(-) diff --git a/TutorialAndDevGuide/Tutorial/Examples/Sonar.hs b/TutorialAndDevGuide/Tutorial/Examples/Sonar.hs index a81da34..1aedb7c 100644 --- a/TutorialAndDevGuide/Tutorial/Examples/Sonar.hs +++ b/TutorialAndDevGuide/Tutorial/Examples/Sonar.hs @@ -7,9 +7,19 @@ import qualified Prelude as P cm :: Stream Int32 cm = extern "distance" Nothing +lowerBound :: Stream Int32 -> Stream Int32 -> Stream Bool +lowerBound value low = low < value + +bounds :: Stream Int32 -> Stream Int32 -> Stream Int32 -> Stream Bool +bounds value low high = low < value && value < high + +upperBound :: Stream Int32 -> Stream Int32 -> Stream Bool +upperBound value high = value < high spec = do - trigger "out_of_range" (cm > 18) [arg cm] + trigger "low_range" (lowerBound cm 10) [arg cm] + trigger "out_of_bounds" (bounds cm 10 18) [arg cm] + trigger "upper_bound" (upperBound cm 18) [arg cm] -- Compile the spec main = reify spec >>= compile "sonar" diff --git a/TutorialAndDevGuide/Tutorial/Examples/sonar.c b/TutorialAndDevGuide/Tutorial/Examples/sonar.c index 1aa0b0a..d7bfcab 100644 --- a/TutorialAndDevGuide/Tutorial/Examples/sonar.c +++ b/TutorialAndDevGuide/Tutorial/Examples/sonar.c @@ -9,19 +9,45 @@ static int32_t distance_cpy; -bool out_of_range_guard(void) { - return (distance_cpy) > ((int32_t)(18)); +bool low_range_guard(void) { + return ((int32_t)(10)) < (distance_cpy); } -int32_t out_of_range_arg0(void) { +int32_t low_range_arg0(void) { + return distance_cpy; +} + +bool out_of_bounds_guard(void) { + return (((int32_t)(10)) < (distance_cpy)) && ((distance_cpy) < ((int32_t)(18))); +} + +int32_t out_of_bounds_arg0(void) { + return distance_cpy; +} + +bool upper_bound_guard(void) { + return (distance_cpy) < ((int32_t)(18)); +} + +int32_t upper_bound_arg0(void) { return distance_cpy; } void step(void) { - int32_t out_of_range_arg_temp0; + int32_t low_range_arg_temp0; + int32_t out_of_bounds_arg_temp0; + int32_t upper_bound_arg_temp0; (distance_cpy) = (distance); - if ((out_of_range_guard)()) { - {(out_of_range_arg_temp0) = ((out_of_range_arg0)()); - (out_of_range)((out_of_range_arg_temp0));} + if ((low_range_guard)()) { + {(low_range_arg_temp0) = ((low_range_arg0)()); + (low_range)((low_range_arg_temp0));} + }; + if ((out_of_bounds_guard)()) { + {(out_of_bounds_arg_temp0) = ((out_of_bounds_arg0)()); + (out_of_bounds)((out_of_bounds_arg_temp0));} + }; + if ((upper_bound_guard)()) { + {(upper_bound_arg_temp0) = ((upper_bound_arg0)()); + (upper_bound)((upper_bound_arg_temp0));} }; } diff --git a/TutorialAndDevGuide/Tutorial/Examples/sonar.h b/TutorialAndDevGuide/Tutorial/Examples/sonar.h index db9f2e4..5f8d30f 100644 --- a/TutorialAndDevGuide/Tutorial/Examples/sonar.h +++ b/TutorialAndDevGuide/Tutorial/Examples/sonar.h @@ -1,3 +1,5 @@ extern int32_t distance; -void out_of_range(int32_t out_of_range_arg0); +void low_range(int32_t low_range_arg0); +void out_of_bounds(int32_t out_of_bounds_arg0); +void upper_bound(int32_t upper_bound_arg0); void step(void); diff --git a/TutorialAndDevGuide/Tutorial/Interpret.tex b/TutorialAndDevGuide/Tutorial/Interpret.tex index 0270400..40941ea 100644 --- a/TutorialAndDevGuide/Tutorial/Interpret.tex +++ b/TutorialAndDevGuide/Tutorial/Interpret.tex @@ -27,7 +27,7 @@ \subsection{Interpreting Copilot} \item[Line 1] Here we inclued the Copilot Language so that we gain access to the front end language. \item[Line 3] Here we include the Prelude. Notice that we hide base Haskell - syntax for functions that we define for use on streams . If this is not + syntax for functions that we define for use on streams. If this is not included you will get an \texttt{Ambiguious Occurance} error. \item[Line 5-12] Here we define data streams as input and output data streams. We go over defining functions as streams in Section 3 of this tutorial. diff --git a/TutorialAndDevGuide/Tutorial/Language.tex b/TutorialAndDevGuide/Tutorial/Language.tex index 9f11f8d..9718222 100644 --- a/TutorialAndDevGuide/Tutorial/Language.tex +++ b/TutorialAndDevGuide/Tutorial/Language.tex @@ -167,7 +167,8 @@ \subsection{Causality} 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 +\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\}$. @@ -180,7 +181,8 @@ \subsection{Causality} % For example we can skip the first two values of {\tt w}: % -\begin{lstlisting}[language = Copilot, frame = single] u = drop 2 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\}$. @@ -196,7 +198,7 @@ \subsection{Causality} % But if instead {\tt fastForwardFib} is defined as {\tt fastforwardFib = drop 4 -fib} , then the definition is disallowed. +fib}, 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 fib} to be generated before @@ -397,7 +399,7 @@ \subsubsection*{Instance of \texttt{Struct}} \subsubsection*{Instance of \texttt{Typed}} -In Copilot, streams can only of types that are instances of the \texttt{Typed} +In Copilot, streams can only be 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: @@ -582,7 +584,7 @@ \subsection{Interacting With the Target Program} 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, +Copilot needs 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) diff --git a/TutorialAndDevGuide/Tutorial/example.tex b/TutorialAndDevGuide/Tutorial/example.tex index 763f451..38c72f8 100644 --- a/TutorialAndDevGuide/Tutorial/example.tex +++ b/TutorialAndDevGuide/Tutorial/example.tex @@ -83,12 +83,12 @@ \subsection{C Code} specification. This file must precede the inclusion of the generated header file on the next line. \item[Line 8] Here we include the header file generated by our Copilot - specification (see next section). + specification. \item[Line 10] 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 12-26] Functions that turn on and turn off the - heater, low-level details are provided. + heater. \item[Line 28-39] Our infinite main-loop: \begin{description} \item[Line 31] Update our global temperature variable by reading it from @@ -149,7 +149,7 @@ \subsection{Specification} 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 +On line 23 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 @@ -163,9 +163,9 @@ \subsection{Generating C code} \begin{code} $ runhaskell Heater.hs \end{code} -This runs our Haskell code, with compiling a binary first. It runs that +This runs our Haskell code, with compiling a binary first. It runs the \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 +created 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 diff --git a/TutorialAndDevGuide/Tutorial/introduction.tex b/TutorialAndDevGuide/Tutorial/introduction.tex index ccf29de..c8725e9 100644 --- a/TutorialAndDevGuide/Tutorial/introduction.tex +++ b/TutorialAndDevGuide/Tutorial/introduction.tex @@ -47,8 +47,8 @@ \subsection{Target Application Domain} \label{domain} systems}. % Briefly, a runtime monitor is program that runs concurrently with a target -program with the sole purpose of assuring that the target program behaves in -accordance with a pre-established specification. +program of the SUO with the sole purpose of assuring that the target program +behaves in accordance with a pre-established specification. % Copilot is a language for writing such specifications. % @@ -59,8 +59,7 @@ \subsection{Target Application Domain} \label{domain} execution. % Reactive systems differ from transformational systems which transform data in -a single pass and then terminate, as for example compilers and numerical -computation software. +a single pass and then terminate. % A hard real-time system is a system that has a statically bounded execution @@ -80,40 +79,20 @@ \subsection{Target Application Domain} \label{domain} \subsection{Installation} \label{sec:install} Before downloading the copilot framework, you must first install an -up-to-date version of GHC (the minimal required version is 8.0). +up-to-date version of GHC (the minimal required version is 8.6.4). % \noindent Copilot compiles to C code, you must install a C compiler such as GCC (\url{https://gcc.gnu.org/install/}). After having installed the Haskell Platform and C compiler, Copilot can be downloaded and installed in the following two ways: \begin{itemize} -\item \textbf{Hackage (Prefered Method): } Copilot is available from Hackage, +\item \textbf{Hackage (Prefered Method): } Copilot is available from +\href{https://hackage.haskell.org/package/copilot-3.16#table-of-contents}{Hackage}, and the latest version can be installed easily: \begin{code} -cabal install copilot +cabal v2-install --lib copilot \end{code} -\item \textbf{From source: } Alternatively one can download and install it from -the repositories as well. Typically one would only go this route to develop -Copilot. For regular users the hackage method above is highly recommended. -\begin{code} -git clone https://github.com/Copilot-Language/copilot.git -cd copilot -git submodule update --init --remote -\end{code} -Compiling can either be done in a Nix-style build, or a traditional one: - -\noindent\emph{Nix-Style build (Cabal $\ge$ 2.x):} -\begin{code} -cabal build # For Cabal 3.x -cabal v2-build # For Cabal 2.x -\end{code} - -\noindent\emph{Traditional build (Cabal 1.x):} -\begin{code} -cabal install --dependencies-only -cabal build -\end{code} \end{itemize} @@ -185,6 +164,17 @@ \subsection{Sampling} \label{sampling} of which are faults to be reported. % +When deciding whether to use Copilot to monitor systems that are not hard +real-time, the user must determine if sampling is suitable to capture the +errors and faults of interest in the SUO. In many cyber-physical systems, the +trace being monitored is coming from sensors measuring physical data such as +GPS coordinates, air speed, and actuation signals. +% + These continuous signals do not change abruptly so as long as it is sampled at +a suitable rate, that usually must be determined experimentally, sampling is +sufficient. +% + Most of the popular runtime monitoring frameworks inline monitors in the observed program to avoid the aforementioned problems with sampling. % @@ -205,15 +195,6 @@ \subsection{Sampling} \label{sampling} Such an architecture may even be necessary if the monitored program is physically distributed. -When deciding whether to use Copilot to monitor systems that are not hard -real-time, the user must determine if sampling is suitable to capture the -errors and faults of interest in the SUO. In many cyber-physical systems, the -trace being monitored is coming from sensors measuring physical data such as -GPS coordinates, air speed, and actuation signals. -% - These continuous signals do not change abruptly so as long as it is sampled at -a suitable rate, that usually must be determined experimentally, sampling is -sufficient. From b0af9e6cc92c041057d8f333bcc4bded3c7e7cdf Mon Sep 17 00:00:00 2001 From: Will Pogge Date: Mon, 11 Sep 2023 11:31:16 -0400 Subject: [PATCH 9/9] Update the majority vote examples. --- TutorialAndDevGuide/Tutorial/Conclusion.tex | 11 +++ .../Tutorial/Examples/Filters.hs | 6 +- .../Tutorial/Examples/MajVoteExample.hs | 23 ++++++ .../Examples/MajVoteExampleCopilot.hs | 25 ++++++ TutorialAndDevGuide/Tutorial/Examples/Spec.hs | 2 +- TutorialAndDevGuide/Tutorial/Interpret.tex | 17 ++-- TutorialAndDevGuide/Tutorial/Language.tex | 80 ++++++++++++------- .../Tutorial/MajVoteExample.tex | 37 +-------- TutorialAndDevGuide/Tutorial/example.tex | 8 +- TutorialAndDevGuide/Tutorial/introduction.tex | 27 ++++--- TutorialAndDevGuide/Tutorial/mybib.bib | 5 ++ TutorialAndDevGuide/Tutorial/tutorial.tex | 1 + 12 files changed, 147 insertions(+), 95 deletions(-) create mode 100644 TutorialAndDevGuide/Tutorial/Conclusion.tex create mode 100644 TutorialAndDevGuide/Tutorial/Examples/MajVoteExample.hs create mode 100644 TutorialAndDevGuide/Tutorial/Examples/MajVoteExampleCopilot.hs diff --git a/TutorialAndDevGuide/Tutorial/Conclusion.tex b/TutorialAndDevGuide/Tutorial/Conclusion.tex new file mode 100644 index 0000000..948d308 --- /dev/null +++ b/TutorialAndDevGuide/Tutorial/Conclusion.tex @@ -0,0 +1,11 @@ + +\newpage +\section{Conclusion} +\label{conclusion} + With that example we come to the end of out tutorial. Hopefully, now +you are able to write some simple monitors. Take the exaples above and try +implementing them into projects of your own. If you need any assistance or have +any questions about the material above or help with a project the authors would +be happy to help. Aditionally, if there are any issues that arrise or +fuctionallity that would be helpful please contact the authors of this paper. +Have a nice day. diff --git a/TutorialAndDevGuide/Tutorial/Examples/Filters.hs b/TutorialAndDevGuide/Tutorial/Examples/Filters.hs index 291ad57..29e90b9 100644 --- a/TutorialAndDevGuide/Tutorial/Examples/Filters.hs +++ b/TutorialAndDevGuide/Tutorial/Examples/Filters.hs @@ -12,7 +12,7 @@ diff :: Stream Int32 diff = fib - fibdelayed gain :: Stream Int32 -gain = fib + 2 +gain = fib * 2 twoTermAverage :: Stream Int32 twoTermAverage = (fib + fibdelayed) `div` 2 @@ -20,9 +20,6 @@ twoTermAverage = (fib + fibdelayed) `div` 2 centralDifference :: Stream Int32 centralDifference = (fib - ([0] ++ fibdelayed)) `div` 2 -recursive :: Stream Int32 -recursive = fib - diff - gainFilter = do observer "fib" fib observer "Simple Gain" gain @@ -31,7 +28,6 @@ diffFilter = do observer "fib" fib observer "fib delayed" fibdelayed observer "Difference Filter" diff - observer "Recursive Diff" recursive pureDelay = do observer "fib" fib diff --git a/TutorialAndDevGuide/Tutorial/Examples/MajVoteExample.hs b/TutorialAndDevGuide/Tutorial/Examples/MajVoteExample.hs new file mode 100644 index 0000000..ef066b1 --- /dev/null +++ b/TutorialAndDevGuide/Tutorial/Examples/MajVoteExample.hs @@ -0,0 +1,23 @@ +--First pass of the majority vote. +majorityPure :: Eq a => [a] -> a +majorityPure [] = error "majorityPure: empty list!" +majorityPure (x:xs) = majorityPure' xs x 1 + +majorityPure' [] can _ = can +majorityPure' (x:xs) can cnt = + let + can' = if cnt == 0 then x else can + cnt' = if cnt == 0 || x == can then succ cnt else pred cnt + in + majorityPure' xs can' cnt' + +-- Second pass of the majority vote algorithm verifying the result of the first pass. +aMajorityPure :: Eq a => [a] -> a -> Bool +aMajorityPure xs can = aMajorityPure' 0 xs can > length xs `div` 2 + +aMajorityPure' cnt [] _ = cnt +aMajorityPure' cnt (x:xs) can = + let + cnt' = if x == can then cnt+1 else cnt + in + aMajorityPure' cnt' xs can diff --git a/TutorialAndDevGuide/Tutorial/Examples/MajVoteExampleCopilot.hs b/TutorialAndDevGuide/Tutorial/Examples/MajVoteExampleCopilot.hs new file mode 100644 index 0000000..ce7705c --- /dev/null +++ b/TutorialAndDevGuide/Tutorial/Examples/MajVoteExampleCopilot.hs @@ -0,0 +1,25 @@ +import Language.Copilot +import qualified Prelude as P + +majority :: (Eq a, Typed a) => [Stream a] -> Stream a +majority [] = error "majority: empty list!" +majority (x:xs) = majority' xs x 1 + +majority' [] can _ = can +majority' (x:xs) can cnt = + local + (if cnt == 0 then x else can) $ + \ can' -> + local (if cnt == 0 || x == can then cnt+1 else cnt-1) $ + \ cnt' -> + majority' xs can' cnt' + +aMajority :: (Eq a, Typed a) => [Stream a] -> Stream a -> Stream Bool +aMajority xs can = aMajority' 0 xs can > (fromIntegral (length xs) `div` 2) + +aMajority' cnt [] _ = cnt +aMajority' cnt (x:xs) can = + local + (if x == can then cnt+1 else cnt) $ + \ cnt' -> + aMajority' cnt' xs can diff --git a/TutorialAndDevGuide/Tutorial/Examples/Spec.hs b/TutorialAndDevGuide/Tutorial/Examples/Spec.hs index 224dc28..ca58e8b 100644 --- a/TutorialAndDevGuide/Tutorial/Examples/Spec.hs +++ b/TutorialAndDevGuide/Tutorial/Examples/Spec.hs @@ -5,7 +5,7 @@ import qualified Prelude as P nats :: Stream Int32 nats = [0] ++ (1 + nats) -evenNumberNumber :: Stream Int32 -> Stream Bool +evenNumber :: Stream Int32 -> Stream Bool evenNumber n = n `mod` 2 == 0 oddNumber :: Stream Int32 -> Stream Bool diff --git a/TutorialAndDevGuide/Tutorial/Interpret.tex b/TutorialAndDevGuide/Tutorial/Interpret.tex index 40941ea..06c1f48 100644 --- a/TutorialAndDevGuide/Tutorial/Interpret.tex +++ b/TutorialAndDevGuide/Tutorial/Interpret.tex @@ -19,22 +19,23 @@ \section{Interpreting} \subsection{Interpreting Copilot} In the ./Examples directory we have provided you with an example -for you to follow allong. \texttt{Spec.hs} is the following Copilot program: +for you to follow along. \texttt{Spec.hs} is the following Copilot program: % \lstinputlisting[language = Copilot, numbers = left]{Examples/Spec.hs} \begin{description} - \item[Line 1] Here we inclued the Copilot Language so that we gain access to the + \item[Line 1] Here we include the Copilot Language so that we gain access to the front end language. \item[Line 3] Here we include the Prelude. Notice that we hide base Haskell syntax for functions that we define for use on streams. If this is not - included you will get an \texttt{Ambiguious Occurance} error. + included you will get an \texttt{Ambiguous Occurrence} error. \item[Line 5-12] Here we define data streams as input and output data streams. We go over defining functions as streams in Section 3 of this tutorial. - \item[Line 14-16] Here {\tt nats} is the stream of natural numbers, and {\tt even} and {\tt odd} - are the guard functions that take a stream and return whether the point-wise - values are even or odd, respectively. The lists at the end of the trigger - represent the values the trigger will output when the guard is true. + \item[Line 14-16] Here {\tt nats} is the stream of natural numbers, and {\tt + evenNumber} and {\tt oddNumber} are the guard functions that take a stream and + return whether the point-wise values are even or odd, respectively. The lists + at the end of the trigger represent the values the trigger will output when the + guard is true. \end{description} @@ -48,7 +49,7 @@ \subsection{Interpreting Copilot} \end{lstlisting} % This launches \texttt{ghci}, the Haskell interpreter, with \texttt{Spec.hs} -loaded. It provides us with a prompt, recognisable by the \texttt{>} sign. Lets +loaded. It provides us with a prompt, recognizable by the \texttt{>} sign. Lets assume that our file contains one specification, called \texttt{spec}. We can interpret this using the \texttt{interpret}-function: \begin{lstlisting}[language = Copilot] diff --git a/TutorialAndDevGuide/Tutorial/Language.tex b/TutorialAndDevGuide/Tutorial/Language.tex index 9718222..7cda70c 100644 --- a/TutorialAndDevGuide/Tutorial/Language.tex +++ b/TutorialAndDevGuide/Tutorial/Language.tex @@ -10,7 +10,7 @@ \section{Language}~\label{sec:language} Copilot is a pure declarative language; \item Sample external variables, structs, and arrays. \item Update internal variables. \item Fire external triggers. (In case the specification is violated.) -\item Update observers (for debugging purpose). +\item Update observers (for debugging purposes). \end{itemize} \noindent We refer to a single cycle as an \emph{iteration} or a \emph{step}. @@ -39,7 +39,7 @@ \subsection{Streams as Lazy-Lists} \label{sec:stream} For those that are not as familiar with Haskell this subsection can be omitted. % -However, there is a few useful definitions of data +However, there are a few useful definitions of data streams as examples. % \begin{lstlisting}[language = Copilot, frame = single] @@ -90,8 +90,8 @@ \subsection{Functions on Streams} \label{sec:FnOnStreams} Applying {\tt even} on {\tt nats} (defined above) yields the sequence $\{T, F, T, F, T, F, \dots\}$. % -This function sould be familiar to the one that -we had shown in {\tt Spec.hs} from \hyperref[interpcompile]{Section 2.1}. +This function should be familiar to the function shown in {\tt Spec.hs} from +\hyperref[interpcompile]{Section 2.1}. \end{example} If a function is required to return multiple results, we simply use plain @@ -143,7 +143,7 @@ \subsection{Functions on Streams} \label{sec:FnOnStreams} Create a function that will check if a stream of numbers is even or not, we have given you the type specification. % -Once you have created the function, you should be able to compile interpret the +Once you have created the function, you should be able to compile and interpret the specification. % @@ -191,7 +191,7 @@ \subsection{Causality} values cannot depend on future values. % Our example \texttt{Causal.hs} in the ./Examples directory shows the use of -{\tt drop} and {\tt ++} by defining a fibonachi series and then creates a +{\tt drop} and {\tt ++} by defining a Fibonachi series and then creates a leading and lagging stream: % \lstinputlisting[language = Copilot, frame = single ]{Examples/Causal.hs} @@ -207,15 +207,36 @@ \subsection{Causality} This is not possible since Copilot programs may take inputs in real-time from the environment (see Section~\ref{subsec:interacting}). -Being able to look ahead and behind in streams is really useful for thing like -rate of change. -% -For example if you were intrested in monitoring how fast your car was +Being able to look ahead and behind in streams is really useful for applications like +rate of change, for example if you were interested in monitoring how fast your car was accelerating or the rate of drain on a battery. % If you would like more practice with the Copilot language, try adding in an observer that shows how much change there was between the leading and the -lagging stream for our fibonachi example. +lagging stream for our Fibonachi example. +% +\subsection{Filtering} \label{sec:filter} + +Filtering is useful when utilizing stream data becasue occationally the data +brought in by the sensors will have errors. We have made some example filters +from Introduction To Digital Filters \cite{Tyson2013} to demonstrate how to create the filters in the Copilot +language. +% +\lstinputlisting[language = Copilot, frame = single, numbers = left]{Examples/Filters.hs} +% + +\begin{description} + \item[Line 1-3] Copilot language standard include and remove + items defined in the Copilot library from the prelude. + \item[Line 5-6] Create a Fibonachi stream that we demonstrated in the last section. + \item[Line 8-9] Delaying the Fibonachi stream by one value. + \item[Lines 11-12] Difference filter shows the change from the previous signal. + \item[Lines 14-15] Gain filter: x > 1 makes the filter an amplifier, while 0 < x < 1 makes it an attenuator x < 0 corresponds to an inverting amplifier. + \item[Lines 17-18] Two term average filter is a simple type of low pass filter as it tends to smooth out high-frequency variations in a signal + \item[Lines 20-21] Central difference filter is half the change of the previous two signals. + \item[Lines 23-42] Observers to show how the filters functionality and how they operate on the stream. + +\end{description} \subsection{Stateful Functions} \label{sec:stateful} @@ -256,10 +277,10 @@ \subsection{Stateful Functions} \label{sec:stateful} \lstinputlisting[language = Copilot, frame = single, numbers = left]{Examples/Latch.hs} \begin{description} - \item[Line 1-4] Standard inclueds to include the Copilot language and remove + \item[Line 1-4] Copilot language standard include and remove items defined in the Copilot library from the prelude. - \item[Line 5-9] This is a set of arbitrary functions to create a stream of - trues and falses to demonstrate the latch. + \item[Line 5-9] This is a set of arbitrary functions to create streams of + True/False outputs to demonstrate the latch. \item[Lines 11-15] demonstrate the implementation of an if-then-else statement in copilot. In order to do if-then-else statements we have defined {\tt mux}. \end{description} @@ -300,9 +321,8 @@ \subsection{Stateful Functions} \label{sec:stateful} \end{center} \end{example} -{\tt Problem:} Now that you have an understanding of how to implement if then operations on streams. -% -Attempt to write a specification for the example above. +{\tt Problem:} Now that you have an understanding of how to implement if then +operations on streams, attempt to write a specification for the example above. % We have started the specification for you in the ./Examples directory. @@ -311,7 +331,7 @@ \subsection{Stateful Functions} \label{sec:stateful} \subsection{Structs} When monitoring embedded systems the data that needs to be observed is often in a struct. -Structs require some special attentation in Copilot, as we cannot magically +Structs require some special attention 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 @@ -336,7 +356,7 @@ \subsection{Structs} \end{enumerate} If you would like to follow along with our example you can open up the Structs.hs file -in the ./Examples directory. We do show the entire thing at the end. +in the ./Examples directory. We do show the entire example at the end. \subsubsection*{Enabling compiler extensions} First and foremost, we need to enable the \texttt{DataKinds} extension to GHC, @@ -354,7 +374,7 @@ \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} +names of the fields in our C code. Therefore we introduce the \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] @@ -372,7 +392,7 @@ \subsubsection*{Defining the datatype} \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 +write an 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: @@ -387,7 +407,7 @@ \subsubsection*{Instance of \texttt{Struct}} , Value Float (y v) ] \end{lstlisting} -Both definitions should be pretty self-explanatory. Note however that +Both definitions should be 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 @@ -429,13 +449,13 @@ \subsubsection*{Simple operations} vx :: Stream Float vx = v # x \end{lstlisting} -Note the we use the Haskell level accessor \texttt{x} to retrieve the field +Note that we use the Haskell level accessor \texttt{x} to retrieve the field from the stream of vectors. \subsubsection*{Example code} \label{exm:struct} -Now that we defined all there is, we can make streams of structs. The following +Once everything has been 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. % @@ -496,12 +516,12 @@ \subsection{Interacting With the Target Program} 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. +those work as well: nested arrays, arrays of structs, structs containing arrays +etc. All of these variables are passed by value, as references, or pointers, +are not supported by Copilot. -Copilot has both an interpreter and a compiler.The compiler must be +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} @@ -573,8 +593,8 @@ \subsection{Interacting With the Target Program} \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. +Just like regular variables, arrays can be sampled as well. Copilot treats +arrays the same way it treats scalars. \begin{example} \label{exmp:pitot} Lets take the example where we diff --git a/TutorialAndDevGuide/Tutorial/MajVoteExample.tex b/TutorialAndDevGuide/Tutorial/MajVoteExample.tex index a74a5f9..47dbdbf 100644 --- a/TutorialAndDevGuide/Tutorial/MajVoteExample.tex +++ b/TutorialAndDevGuide/Tutorial/MajVoteExample.tex @@ -33,44 +33,13 @@ \subsection{The Boyer-Moore Majority-Vote Algorithm} This algorithm will produce an output even if there is no majority, which is why the second pass is needed to verify that the output of the first pass is valid. -\begin{figure*}[!htb] -\begin{lstlisting}[language = Copilot, frame = none] -majorityPure :: Eq a => [a] -> a -majorityPure [] = error "majorityPure: empty list!" -majorityPure (x:xs) = majorityPure' xs x 1 - -majorityPure' [] can _ = can -majorityPure' (x:xs) can cnt = - let - can' = if cnt == 0 then x else can - cnt' = if cnt == 0 || x == can then succ cnt else pred cnt - in - majorityPure' xs can' cnt' -\end{lstlisting} -\caption{The first pass of the majority vote algorithm in Haskell.} -\label{fig:majority_pure} -\end{figure*} -\begin{figure*}[!htb] -\begin{lstlisting}[language = Copilot, frame = none] -aMajorityPure :: Eq a => [a] -> a -> Bool -aMajorityPure xs can = aMajorityPure' 0 xs can > length xs `div` 2 - -aMajorityPure' cnt [] _ = cnt -aMajorityPure' cnt (x:xs) can = - let - cnt' = if x == can then cnt+1 else cnt - in - aMajorityPure' cnt' xs can -\end{lstlisting} -\caption{The second pass of the majority vote algorithm in Haskell.} -\label{fig:amajority_pure} -\end{figure*} +\lstinputlisting[language = Copilot, numbers = left]{Examples/MajVoteExample.hs} The first pass can be implemented -in Haskell as shown in Figure \ref{fig:majority_pure}. The second pass, which +in Haskell as shown in lines 2-13. The second pass, which simply checks that a candidate has more than half of the votes, is -straightforward to implement and is shown in Figure \ref{fig:amajority_pure}. +straightforward to implement and is shown in lines 15-23. E.g. applying {\tt majorityPure} on the string {\tt AAACCBBCCCBCC} yields {\tt C}, which {\tt aMajorityPure} can confirm is in fact a majority. diff --git a/TutorialAndDevGuide/Tutorial/example.tex b/TutorialAndDevGuide/Tutorial/example.tex index 38c72f8..ea086bc 100644 --- a/TutorialAndDevGuide/Tutorial/example.tex +++ b/TutorialAndDevGuide/Tutorial/example.tex @@ -79,7 +79,7 @@ \subsection{C Code} hardware. Let us look at a couple of interesting lines: \begin{description} - \item[Line 7] Here we inclued the header types files generated by out Copilot + \item[Line 7] Here we include 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 8] Here we include the header file generated by our Copilot @@ -101,7 +101,7 @@ \subsection{C Code} 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. +program, but this complicates things and is highly discouraged. \subsection{Specification} @@ -146,11 +146,11 @@ \subsection{Specification} %-- Compile the spec %main = reify spec >>= compile "heater" %\end{lstlisting} -The code should be pretty self explanatory. Note that we opted to use a +The code should be self explanatory. Note that we opted to use a \texttt{main}-function, which reifies and compiles the code for us. On line 23 we can see the \texttt{ctemp}-stream, which is the temperature -translated to Celcius. Interestingly, we need to do a manual typecast from +translated to Celsius. 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 diff --git a/TutorialAndDevGuide/Tutorial/introduction.tex b/TutorialAndDevGuide/Tutorial/introduction.tex index c8725e9..5498e09 100644 --- a/TutorialAndDevGuide/Tutorial/introduction.tex +++ b/TutorialAndDevGuide/Tutorial/introduction.tex @@ -46,7 +46,7 @@ \subsection{Target Application Domain} \label{domain} monitors} for \emph{hard real-time}, \emph{distributed}, \emph{reactive systems}. % -Briefly, a runtime monitor is program that runs concurrently with a target +Briefly, a runtime monitor is a program that runs concurrently with a target program of the SUO with the sole purpose of assuring that the target program behaves in accordance with a pre-established specification. % @@ -58,8 +58,9 @@ \subsection{Target Application Domain} \label{domain} All data to and from a reactive system are communicated progressively during execution. % - Reactive systems differ from transformational systems which transform data in -a single pass and then terminate. +Transformational systems, in contrast to reactive systems like Copilot, +transform data in a single pass and then terminate (examples are compilers and +numerical computation software). % A hard real-time system is a system that has a statically bounded execution @@ -69,7 +70,7 @@ \subsection{Target Application Domain} \label{domain} as avionics, medical equipment, and nuclear power plants; hence, occasional dropouts in the response time or crashes are not tolerated. -A distributed system is a system which is layered out on multiple pieces of +A distributed system is a system that is layered out on multiple pieces of hardware. % The distributed systems we consider are all synchronized, i.e., all components @@ -78,15 +79,15 @@ \subsection{Target Application Domain} \label{domain} \subsection{Installation} \label{sec:install} -Before downloading the copilot framework, you must first install an +Before downloading the Copilot framework, you must first install an up-to-date version of GHC (the minimal required version is 8.6.4). % -\noindent Copilot compiles to C code, you must install a C compiler such as GCC (\url{https://gcc.gnu.org/install/}). After having installed the Haskell Platform and C compiler, Copilot can be downloaded and +\noindent Copilot compiles to C code, therefor you must install a C compiler such as GCC (\url{https://gcc.gnu.org/install/}). After having installed the Haskell Platform and C compiler, Copilot can be downloaded and installed in the following two ways: \begin{itemize} -\item \textbf{Hackage (Prefered Method): } Copilot is available from +\item \textbf{Hackage (Preferred Method): } Copilot is available from \href{https://hackage.haskell.org/package/copilot-3.16#table-of-contents}{Hackage}, and the latest version can be installed easily: \begin{code} @@ -122,7 +123,7 @@ \subsection{Sampling} \label{sampling} at a high enough rate to obtain enough discrete points to represent the physical sound wave. % - The fidelity of the recording is dependant on the sampling rate. + The fidelity of the recording is dependent on the sampling rate. % Sampling a state variable of an executing program is similar, but variables are rarely continuous signals so they lack the nice properties of continuity. @@ -135,7 +136,7 @@ \subsection{Sampling} \label{sampling} For example, consider the property $(0;1;1)^*$, written as a regular expression, denoting the sequence of values a monitored variable may take. % - If the monitor samples the variable at the inappropriate time, then both false + If the monitor samples the variable at an inappropriate time, then both false negatives (the monitor erroneously rejects the sequence of values) and false positives (the monitor erroneously accepts the sequence) are possible. % @@ -149,11 +150,11 @@ \subsection{Sampling} \label{sampling} However, in a hard real-time context, sampling is a suitable strategy. % Often, the purpose of real-time programs is to deliver output signals at a -predicable rate and properties of interest are generally data-flow oriented. +predictable rate and properties of interest are generally data-flow oriented. % In this context, and under the assumption that the monitor and the observed program share a global clock and a static periodic schedule, while false -positives are possible, false negatives are not. +positives are possible, and false negatives are not. % A false positive is possible, for example, if the program does not execute according to its schedule but just happens to have the expected values when @@ -175,11 +176,11 @@ \subsection{Sampling} \label{sampling} sufficient. % -Most of the popular runtime monitoring frameworks inline monitors in the +Most of the popular runtime monitoring frameworks utilize inline monitors in the observed program to avoid the aforementioned problems with sampling. % However, inlining monitors changes the real-time behavior of the observed -program, perhaps in unpredicable ways. +program, perhaps in unpredictable ways. % Solutions that introduce such unpredictability are not a viable solution for ultra-critical hard real-time systems. diff --git a/TutorialAndDevGuide/Tutorial/mybib.bib b/TutorialAndDevGuide/Tutorial/mybib.bib index 781022c..9f47ada 100644 --- a/TutorialAndDevGuide/Tutorial/mybib.bib +++ b/TutorialAndDevGuide/Tutorial/mybib.bib @@ -514,6 +514,11 @@ @Article{HavelundR04B +@misc{Tyson2013, + title = {Introduction To Digital Filters}, + author = {Tony Tyson}, + year = {2013} +} @Misc{framac, diff --git a/TutorialAndDevGuide/Tutorial/tutorial.tex b/TutorialAndDevGuide/Tutorial/tutorial.tex index 7f276ef..07a7483 100644 --- a/TutorialAndDevGuide/Tutorial/tutorial.tex +++ b/TutorialAndDevGuide/Tutorial/tutorial.tex @@ -337,6 +337,7 @@ \section*{Acknowledgement} \input{Interpret} \input{Language} \input{example} +\input{Conclusion} \addcontentsline{toc}{section}{References} \bibliographystyle{alpha} \bibliography{mybib}