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/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..29e90b9
--- /dev/null
+++ b/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
+
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/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/Sonar.hs b/TutorialAndDevGuide/Tutorial/Examples/Sonar.hs
new file mode 100644
index 0000000..1aedb7c
--- /dev/null
+++ b/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"
diff --git a/TutorialAndDevGuide/Tutorial/Examples/Spec.hs b/TutorialAndDevGuide/Tutorial/Examples/Spec.hs
new file mode 100644
index 0000000..ca58e8b
--- /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)
+
+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]
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 <stdint.h>
+#include <stdbool.h>
+#include <string.h>
+#include <stdlib.h>
+#include <math.h>
+
+#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 <stdint.h>
+#include <stdbool.h>
+#include <string.h>
+#include <stdlib.h>
+#include <math.h>
+
+#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 <stdint.h>
+#include <stdbool.h>
+#include <string.h>
+#include <stdlib.h>
+#include <math.h>
+
+#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..d7bfcab
--- /dev/null
+++ b/TutorialAndDevGuide/Tutorial/Examples/sonar.c
@@ -0,0 +1,53 @@
+#include <stdint.h>
+#include <stdbool.h>
+#include <string.h>
+#include <stdlib.h>
+#include <math.h>
+
+#include "sonar_types.h"
+#include "sonar.h"
+
+static int32_t distance_cpy;
+
+bool low_range_guard(void) {
+  return ((int32_t)(10)) < (distance_cpy);
+}
+
+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 low_range_arg_temp0;
+  int32_t out_of_bounds_arg_temp0;
+  int32_t upper_bound_arg_temp0;
+  (distance_cpy) = (distance);
+  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
new file mode 100644
index 0000000..5f8d30f
--- /dev/null
+++ b/TutorialAndDevGuide/Tutorial/Examples/sonar.h
@@ -0,0 +1,5 @@
+extern int32_t distance;
+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/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 2eb968c..06c1f48 100644
--- a/TutorialAndDevGuide/Tutorial/Interpret.tex
+++ b/TutorialAndDevGuide/Tutorial/Interpret.tex
@@ -1,29 +1,59 @@
 \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 \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}
+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 along. \texttt{Spec.hs} is the following Copilot program:
+%
+\lstinputlisting[language = Copilot, numbers = left]{Examples/Spec.hs}
+
+\begin{description}
+  \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{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
+  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}
+
+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}
-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]
-*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 +63,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 +84,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{<prefix>.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{<prefix>\_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{<prefix>.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..7cda70c 100644
--- a/TutorialAndDevGuide/Tutorial/Language.tex
+++ b/TutorialAndDevGuide/Tutorial/Language.tex
@@ -1,24 +1,24 @@
 
-\section{Language}~\label{sec:language}
-
-Copilot is embedded into the functional programming language Haskell
-\cite{PeytonJones02}, and a working knowledge of Haskell is necessary to use
-Copilot effectively. Copilot is a pure declarative language; i.e., expressions
-are free of side-effects and are referentially transparent.  A program written
-in Copilot, which from now on will be referred to as a \emph{specification}, has
-a cyclic behavior, where each cycle consists of a fixed series of steps:
+\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).
+\item Update observers (for debugging purposes).
 \end{itemize}
 
 \noindent We refer to a single cycle as an \emph{iteration} or a \emph{step}.
 
 All transformation of data in Copilot is propagated through streams.
+%
 A stream is an infinite, ordered sequence of values which must conform to the same type.
+%
 E.g., we have the stream of Fibonacci numbers:
 
 \begin{center}
@@ -26,36 +26,133 @@ \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.
 
-Constants as well as arithmetic, boolean, and relational operators are
-lifted to work pointwise on streams:
+\subsection{Streams as Lazy-Lists} \label{sec:stream}
 
-\noindent
-%\begin{minipage}{0.3\textwidth}
+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 are a few useful definitions of data
+streams as examples.
+%
 \begin{lstlisting}[language = Copilot, frame = single]
-x :: Stream Int32
-x = 5 + 5
+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\}$.
+%
+This function should be familiar to the function shown in {\tt Spec.hs} from
+\hyperref[interpcompile]{Section 2.1}.
+\end{example}
 
-y :: Stream Int32
-y = x * x
+If a function is required to return multiple results, we simply use plain
+Haskell tuples:
 
-z :: Stream Bool
-z = x == 10 && y < 200
+\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 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}
+\lstinputlisting[language = Copilot, frame = single, numbers = left]{Examples/Streams.hs}
+
 %\end{minipage}
 
 
 \noindent Here the streams {\tt x}, {\tt y}, and {\tt z} are simply
 \emph{constant streams}:
 
-\begin{center}
-$\mathtt{x} \leadsto \{10, 10, 10, \dots \}$,
-$\mathtt{y} \leadsto \{100, 100, 100,  \dots \}$,
-$\mathtt{z} \leadsto \{\mbox{T},\; \mbox{T},\; \mbox{T},\; \dots \}$
-\end{center}
+\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. 
+
+
+{\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 and 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
 looking into the future of streams:
 %
@@ -64,82 +161,177 @@ \section{Language}~\label{sec:language}
 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}.
+%
+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\}$.
+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
 \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\}$.
 
-\subsection{Streams as Lazy-Lists} \label{sec: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}
+%
 
-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:
+But if instead {\tt fastForwardFib} is defined as {\tt fastforwardFib = drop 4
+fib}, then the definition is disallowed.
 %
-\begin{lstlisting}[language = Copilot, frame = single]
-nats_ll :: [Int32]
-nats_ll = [0] ++ zipWith (+) (repeat 1) nats_ll
-\end{lstlisting}
+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}.
 %
-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:
+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 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.
 %
-\begin{lstlisting}[language = Copilot, frame = single]
-nats :: Stream Int32
-nats = [0] ++ (1 + nats)
-\end{lstlisting}
+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.
 %
-In the same manner, the lazy-list of Fibonacci numbers can be specified  in Haskell as follows:
+\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.
 %
-\begin{lstlisting}[language = Copilot, frame = single]
-fib_ll :: [Int32]
-fib_ll = [1, 1] ++ zipWith (+) fib_ll (drop 1 fib_ll)
-\end{lstlisting}
+\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}
+
+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] 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 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}
+
 %
-In Copilot we simply throw away {\tt zipWith}:
 \begin{lstlisting}[language = Copilot, frame = single]
-fib :: Stream Int32
-fib = [1, 1] ++ (fib + drop 1 fib)
+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}.
 
-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{example} We consider a resettable counter with two inputs, {\tt inc} and
+{\tt reset}.
 %
-\begin{lstlisting}[language = Copilot, frame = single]
-f :: Stream Word64
-f = [0,1,2] ++ f
+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.
 
-g :: Stream Word64
-g = drop 2 f
-\end{lstlisting}
+\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.
 
-But if instead {\tt g} is defined as {\tt g = drop 4 f}, then the definition is
-disallowed.  While an analogous stream is definable in a lazy language, we bar
-it in Copilot, since it requires future values of {\tt f} to be
-generated before producing values for {\tt g}.  This is not possible since
-Copilot programs may take inputs in real-time from the environment (see
-Section~\ref{subsec:interacting}).
+\lstinputlisting[language = Copilot, frame = single, numbers = left]{Examples/Counter_Problem.hs}
 
 
 \subsection{Structs}
-Structs require some special attentation in Copilot, as we cannot magically
+When monitoring embedded systems the data that needs to be observed is often in a struct.
+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
@@ -163,6 +355,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 example at the end. 
+
 \subsubsection*{Enabling compiler extensions}
 First and foremost, we need to enable the \texttt{DataKinds} extension to GHC,
 by putting:
@@ -179,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]
@@ -197,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:
@@ -207,12 +402,12 @@ \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)
                ]
 \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
@@ -224,7 +419,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:
@@ -254,212 +449,18 @@ \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}
-\begin{example}
 \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.
-
-\begin{lstlisting}[language=Copilot]
-{-# LANGUAGE DataKinds #-}
-
-module Struct where
-
-import Language.Copilot
-import Copilot.Compile.C99
-
-import Prelude hiding ((>), (<), div, (++))
-
-
-data Vec = Vec
-  { x :: Field "x" Float
-  , y :: Field "y" Float
-  }
-
-instance Struct Vec where
-  typename _ = "vec"  -- Name of the type in C
-
-  -- Function to translate Vec to list of Value's, order should match struct.
-  toValues v = [ Value Float (x v)
-               , Value Float (y v)
-               ]
-
--- We need to provide an instance to Typed with a bogus Vec
-instance Typed Vec where
-  typeOf = Struct (Vec (Field 0) (Field 0))
-
-
-vecs :: Stream Vec
-vecs = [ Vec (Field 1) (Field 2)
-       , Vec (Field 12) (Field 8)
-       ] ++ vecs
-
-
-spec = do
-  -- Trigger that always executes, splits the vec into seperate args.
-  trigger "split" true [arg $ vecs # x, arg $ vecs # y]
-\end{lstlisting}
-\end{example}
-
-\subsection{Functions on Streams} \label{sec:FnOnStreams}
-
-Given that constants and operators work pointwise on streams, we can use Haskell
-as a macro-language for defining functions on streams.  The idea of using
-Haskell as a macro language is powerful since Haskell is a
-general-purpose higher-order functional language.
-
-\begin{example}
-We define the function {\tt even}, which given a stream of
-integers returns a boolean stream which is true whenever the input stream
-contains an even number, as follows:
 %
-\begin{lstlisting}[language = Copilot, frame = single]
-even :: Stream Int32 -> Stream Bool
-even x = x `mod` 2 == 0
-\end{lstlisting}
-%
-Applying {\tt even} on {\tt nats} (defined above) yields the sequence
-$\{T, F, T, F, T, F, \dots\}$.
-\end{example}
-
-If a function is required to return multiple results, we simply use plain
-Haskell tuples:
-
-\begin{example}
-We define complex multiplication as follows:
-%
-\begin{lstlisting}[language = Copilot, frame = single]
-mul_comp
-  :: (Stream Double, Stream Double)
-  -> (Stream Double, Stream Double)
-  -> (Stream Double, Stream Double)
-(a, b) `mul_comp` (c, d) = (a * c - b * d, a * d + b * c)
-\end{lstlisting}
+\lstinputlisting[language = Copilot, frame = single, numbers = left]{Examples/Structs.hs}
 %
-Here {\tt a} and {\tt b} represent the real and imaginary part of the left
-operand, and {\tt c} and {\tt d} represent the real and imaginary part
-of the right operand.
-\end{example}
-
-\subsection{Stateful Functions} \label{sec:stateful}
-
-In addition to pure functions, such as {\tt even} and {\tt mul\_comp},
-Copilot also facilitates \emph{stateful} functions. A \emph{stateful} function
-is a function which has an internal state, e.g. as a latch (as in electronic
-circuits) or a low/high-pass filter (as in a DSP).
-
-\begin{figure*}
-\begin{minipage}{0.25\linewidth}
-\begin{tabular}{c|c||c}
-$\mathtt{x}_i$: & $\mathtt{y}_{i-1}$: & $\mathtt{y}_i$:\\
-\hline
-$F$ & $F$ & $F$ \\
-\hline
-$F$ & $T$ & $T$ \\
-\hline
-$T$ & $F$ & $T$ \\
-\hline
-$T$ & $T$ & $F$
-\end{tabular}
-\end{minipage}
-\begin{minipage}{0.35\linewidth}
-\begin{lstlisting}[frame=none]
-latch :: Stream Bool -> Stream Bool
-latch x = y
-  where
-  y = if x then not z else z
-  z = [False] ++ y
-\end{lstlisting}
-\end{minipage}
-\hspace{1cm}
-\begin{minipage}{0.3\linewidth}
-\begin{tabular}{c|c|c|c|c|c}
-   & 0 & 1 & 2 & 3 & 4\\
-\hline
-x & $F$ & $T$ & $T$ & $F$ & $F$ \\
-\hline
-y & $F$ & $T$ & $F$ & $F$ & $F$ \\
-\end{tabular}
-\end{minipage}
-\caption{A latch [Example 3]. The specification function is provided at the left and the
-implementation in copilot is provided in the middle. The right shows an example of
-the latch, where x is $\{F, T, T, F, F, \dots \}$ and the initial value of y (used with $x_0$ to find
-$y_0$ since there is no $y_{-1}$) is False.}
-\label{fig:jk_latch}
-\end{figure*}
-
-\begin{example}
-We consider a simple latch, as described in \cite{Farhat2004}, with a single
-input and a boolean state. A latch is a way of simulating memory in circuits by feeding
-back output gates as inputs.  Whenever the input is true the internal state is reversed.
-The operational behavior and the implementation of the latch is shown in Figure
-\ref{fig:jk_latch}.\footnote
-{In order
-to use conditionals (i.e., if-then-else) in Copilot specifications,
-as in Figures~\ref{fig:jk_latch} and~\ref{fig:counter}, the GHC
-language extension {\tt RebindableSyntax} must be set on.}
-\end{example}
-
-\begin{figure*}
-\begin{minipage}{0.4\linewidth}
-\begin{tabular}{c|c||c}
-$\mathtt{inc}_i$: & $\mathtt{reset}_i$: & $\mathtt{cnt}_i$: \\
-\hline
-$F$ & $F$ & $\mathtt{cnt}_{i-1}$ \\
-\hline
-* & $T$ & $0$ \\
-\hline
-$T$ & $F$ & $\mathtt{cnt}_{i-1} + 1$ \\
-\hline
-\end{tabular}
-\end{minipage}
-\hspace{1cm}
-\begin{minipage}{0.6\linewidth}
-\begin{lstlisting}[language = Copilot, frame = none]
-counter :: Stream Bool -> Stream Bool
-        -> Stream Int32
-counter inc reset = cnt
-  where
-  cnt = if reset then 0
-          else if inc then z + 1
-                 else z
-  z = [0] ++ cnt
-\end{lstlisting}
-\end{minipage}
-\caption{A resettable counter. The specification is provided at the left and the
-implementation is provided at the right.
-}
-\label{fig:counter}
-\end{figure*}
-
-\begin{example}
-We consider a resettable counter with two inputs, {\tt inc} and {\tt reset}.
-The input {\tt inc} increments the counter and the input {\tt reset} resets the
-counter. The internal state of the counter, {\tt cnt}, represents the value of the
-counter and is initially set to zero. At each cycle, $i$, the value of
-$\mathtt{cnt}_i$ is determined as shown in the left table in Figure
-\ref{fig:counter}.
-\end{example}
-
-%\begin{figure}
-%\begin{code}
-%fir2pole :: Double -> Double -> Double -> Double
-%  -> Double -> Sig Double -> Sig Double
-%fir2pole a1 a2 b0 b1 b2 x0 = y0
-%  where
-%    y0 = - (constant a1)*y1 - (constant a2)*y2
-%         + (constant b0)*x0 + (constant b1)*x1 + (constant b2)*x2
-%    x2 = [0, 0] ++ x0 ; x1 = drop 1 x2
-%    y2 = [0, 0] ++ y0 ; y1 = drop 1 y2
-%\end{code}
-%\caption{A $2$-pole IIR filter.}
-%\label{fig:2_pole_iir_filter}
-%\end{figure}
 
 \subsection{Types} \label{sec:types}
 
@@ -515,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}
@@ -592,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
@@ -603,7 +604,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/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 be93154..ea086bc 100644
--- a/TutorialAndDevGuide/Tutorial/example.tex
+++ b/TutorialAndDevGuide/Tutorial/example.tex
@@ -10,57 +10,90 @@ \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{C Code}
-Lets start of with the C program our monitor to connect to.
-\begin{lstlisting}[language=c, numbers=left]
-#include <stdlib.h>
-#include <stdint.h>
-
-#include "heater_types.h" /* Generated by our specification */
-#include "heater.h" /* Generated by our specification */
+\subsection{Compiling Copilot} \label{sec:compiling}
 
-uint8_t temperature;
+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:
 
-void heaton (float temp) {
-  /* Low-level code to turn heating on */
-}
+\begin{lstlisting}[language = Copilot]
+import Copilot.Compile.C99
+\end{lstlisting}
 
-void heatoff (float temp) {
-  /* Low-level code to turn heating off */
-}
+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 "heater"
+\end{lstlisting}
 
-int main (int argc, char *argv[]) {
-  for (;;) {
-    temperature = readbyte(); /* Dummy function to read a byte from a sensor. */
+This generates three output files:
+\begin{itemize}
+  \item \texttt{<prefix>.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{<prefix>\_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{<prefix>.h}: Header providing the public interface to the
+  monitor. This file should be included from your main project.
+\end{itemize}
 
-    step();
-  }
+\subsection{C Code}
+Lets start of with the C program our monitor to connect to.
 
-  return 0;
-}
-\end{lstlisting}
+\lstinputlisting[language = c, frame = single, numbers = left]{Examples/heater.c}
+%\begin{lstlisting}[language=c, numbers=left]
+%#include <stdlib.h>
+%#include <stdint.h>
+%
+%#include "heater_types.h" /* Generated by our specification */
+%#include "heater.h" /* Generated by our specification */
+%
+%uint8_t temperature;
+%
+%void heaton (float temp) {
+%  /* Low-level code to turn heating on */
+%}
+%
+%void heatoff (float temp) {
+%  /* Low-level code to turn heating off */
+%}
+%
+%int main (int argc, char *argv[]) {
+%  for (;;) {
+%    temperature = readbyte(); /* Dummy function to read a byte from a sensor. */
+%
+%    step();
+%  }
+%
+%  return 0;
+%}
+%\end{lstlisting}
 
 For this code we left out the low-level details for interfacing with our
 hardware. Let us look at a couple of interesting lines:
 
 \begin{description}
-  \item[Line 4] Here we inclued the header types files generated by out Copilot
+  \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 5] Here we include the header file generated by our Copilot
-  specification (see next section).
-  \item[Line 9] Global variable that stores the raw output of the temperature
+  \item[Line 8] Here we include the header file generated by our Copilot
+  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 9-15] Functions that turn on and turn off the
-  heater, low-level details are provided.
-  \item[Line 18-22] Our infinite main-loop:
+  \item[Line 12-26] Functions that turn on and turn off the
+  heater.
+  \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}
 
@@ -68,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}
@@ -76,47 +109,48 @@ \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}
-The code should be pretty self explanatory. Note that we opted to use a
+\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 self explanatory. Note that we opted to use a
 \texttt{main}-function, which reifies and compiles the code for us.
 
-On line 25 we can see the \texttt{ctemp}-stream, which is the temperature
-translated to Celcius. Interestingly, we need to do a manual typecast from
+On line 23 we can see the \texttt{ctemp}-stream, which is the temperature
+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
@@ -129,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 cdc7c22..5498e09 100644
--- a/TutorialAndDevGuide/Tutorial/introduction.tex
+++ b/TutorialAndDevGuide/Tutorial/introduction.tex
@@ -1,122 +1,101 @@
 
 \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 necessary to use
-Copilot effectively; 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 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.
+%
+ 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
-computation software.
+execution.
+%
+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 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 that 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 source code, 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}
+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 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, 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 Hackage,
+\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}
-cabal install 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
+cabal v2-install --lib copilot
 \end{code}
 
-\noindent\emph{Traditional build (Cabal 1.x):}
-\begin{code}
-cabal install --dependencies-only
-cabal build
-\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}
 
@@ -137,60 +116,86 @@ \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 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.
+%
 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 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. 
+%
+ 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
+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, 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
+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.
+%
+
+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 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 unpredictable  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.
+
 
 
 
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 ad582d8..07a7483 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}
@@ -331,6 +337,7 @@ \section*{Acknowledgement}
 \input{Interpret}
 \input{Language}
 \input{example}
+\input{Conclusion}
 \addcontentsline{toc}{section}{References}
 \bibliographystyle{alpha}
 \bibliography{mybib}