Add follow along examples to the Copilot Tutorials.

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.

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

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) 

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) 

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"

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))  

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))  

TutorialAndDevGuide/Tutorial/Examples/Filters.hs

@@ -0,0 +1,43 @@
+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
+
+gainFilter = do 
+  observer "fib" fib
+  observer "Simple Gain" gain
+
+diffFilter = do 
+  observer "fib" fib
+  observer "fib delayed" fibdelayed
+  observer "Difference Filter" diff
+
+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
+

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"

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) 

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

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

TutorialAndDevGuide/Tutorial/Examples/Sonar.hs

@@ -0,0 +1,25 @@
+
+import Language.Copilot
+import Copilot.Compile.C99
+
+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 "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"

TutorialAndDevGuide/Tutorial/Examples/Spec.hs

@@ -0,0 +1,19 @@
+import Language.Copilot 
+
+import qualified Prelude as P
+
+nats :: Stream Int32
+nats = [0] ++ (1 + nats)
+
+evenNumber :: 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]

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

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)