From 3c817ba4ef6fdd666d77314e2b4811b18f147d4d Mon Sep 17 00:00:00 2001
From: Maxwell Y Fan <maxwell.y.fan@nasa.gov>
Date: Thu, 21 Sep 2023 14:13:11 -0700
Subject: [PATCH] WIP: Future-time MLTL.

[ci skip]
---
 examples/Experiment.hs  | 383 ++++++++++++++++++++++++++++++++++++++++
 examples/Mltl.hs        | 221 +++++++++++++++++++++++
 examples/Test.hs        | 303 +++++++++++++++++++++++++++++++
 examples/examples.cabal | 174 ++++++++++++++++++
 4 files changed, 1081 insertions(+)
 create mode 100644 examples/Experiment.hs
 create mode 100644 examples/Mltl.hs
 create mode 100644 examples/Test.hs
 create mode 100644 examples/examples.cabal

diff --git a/examples/Experiment.hs b/examples/Experiment.hs
new file mode 100644
index 000000000..7688bd28a
--- /dev/null
+++ b/examples/Experiment.hs
@@ -0,0 +1,383 @@
+-- {-# OPTIONS_GHC -Wincomplete-patterns #-}
+{-# LANGUAGE GADTs #-}
+import Prelude hiding (True, False, init)
+import qualified Prelude
+
+-- import qualified Language.Copilot
+-- import qualified Copilot.Interpret
+--- import Copilot.PrettyPrint
+
+-- import Data.List
+-- import Data.String
+-- import Data.Char
+-- import System.IO
+import Debug.Trace
+
+data Truth = T | F | PT | PF
+  deriving (Eq, Ord, Read)
+
+instance Show Truth where
+  show T  = "T"
+  show F  = "F"
+  show PT  = "PT"
+  show PF  = "PF"
+
+data AbsVar where
+  Var :: String -> AbsVar
+  Add :: AbsVar -> Int -> AbsVar
+  -- Minus :: AbsVar -> Int -> AbsVar
+  deriving (Eq, Ord, Read)
+
+instance Show AbsVar where
+  -- An stream with `label` at `index` will return `future` when the value is not ready yet
+  show (Var name) = name
+  show (Add var val) | val >= 0 = show var ++ "+" ++ show val
+  show (Add var val) | val < 0 = show var ++ show val
+  -- show (Minus var val) = show var ++ "-" ++ show val
+
+type Label = Int
+
+data TFormula where
+  -- labeled variables/streams
+  Stream :: Label -> TFormula
+
+  -- standard logical operators
+  LAnd :: TFormula -> TFormula -> TFormula
+  LOr :: TFormula -> TFormula -> TFormula
+  -- Implies :: TFormula -> TFormula -> TFormula
+  LNot :: TFormula -> TFormula
+
+  -- FTLTL operators, unbounded
+  Globally :: TFormula -> TFormula         -- globally/box
+  Finally :: TFormula -> TFormula          -- will it be true in any future time step
+  Next :: TFormula -> TFormula             -- is it true in the next time step
+  Until :: TFormula -> TFormula -> TFormula -- has the first stream held until the second stream has been true
+
+  Constant :: Truth -> TFormula
+  deriving (Eq, Ord, Read)
+
+instance Show TFormula where
+  -- questions: what is zeta? should I implement equiv, xor, etc?
+  show (Stream label) = "s_" ++ show label ++ ""
+
+  show (LAnd f1 f2) = "(" ++ show f1 ++ " and " ++ show f2 ++ ")"
+  show (LOr f1 f2) = "(" ++ show f1 ++ " or " ++ show f2 ++ ")"
+  -- show (Implies f1 f2) = "IMPLIES_MTL(" ++ show f1 ++ "," ++ show f2 ++ ")"
+  show (LNot f1) = "(not" ++ show f1 ++ ")"
+
+  show (Globally f1) = "G(" ++ show f1 ++ ")"
+  show (Finally f1) = "F(" ++ show f1 ++ ")"
+  show (Next f1) = "X(" ++ show f1 ++ ")"
+  show (Until f1 f2) = "((" ++ show f1 ++ ")U(" ++ show f2 ++ "))"
+  show (Constant val) = show val
+
+type FreshVar = Int
+
+data MFormula where
+  IndexedStream :: Label -> AbsVar -> MFormula
+  Forall :: AbsVar -> AbsVar -> AbsVar -> MFormula -> MFormula
+  Exists :: AbsVar -> AbsVar -> AbsVar -> MFormula -> MFormula
+
+  And :: MFormula -> MFormula -> MFormula
+  Or :: MFormula -> MFormula -> MFormula
+  Not :: MFormula -> MFormula
+
+  Const :: Truth -> MFormula
+
+  -- casting
+  Pt :: MFormula -> MFormula
+  Pf :: MFormula -> MFormula 
+  P :: MFormula -> MFormula
+
+  deriving (Eq, Ord, Read)
+
+instance Show MFormula where
+  -- questions: what is zeta? should I implement equiv, xor, etc?
+  -- An stream with `label` at `index` will return `future` when the value is not ready yet
+  show (IndexedStream label index) = "s_" ++ show label ++ "[" ++ show index ++ "]"
+  show (Forall var lb ub formula) = "forall " ++ show var ++ " in [" ++ show lb ++ ".." ++ show ub ++ "], " ++ show formula
+  show (Exists var lb ub formula) = "exists " ++ show var ++ " in [" ++ show lb ++ ".." ++ show ub ++ "], " ++ show formula
+
+  show (And f1 f2) = "(" ++ show f1 ++ ") and (" ++ show f2 ++ ")"
+  show (Or f1 f2) = "(" ++ show f1 ++ ") or (" ++ show f2 ++ ")"
+  -- show (Implies f1 f2) = "IMPLIES_MTL(" ++ show f1 ++ "," ++ show f2 ++ ")"
+  show (Not f1) = "(not" ++ show f1 ++ ")"
+  show (Const val)  = show val
+
+  -- casting
+  show (Pt f1) = "Pt(" ++ show f1 ++ ")"
+  show (Pf f1) = "Pf(" ++ show f1 ++ ")"
+  show (P f1) = "P(" ++ show f1 ++ ")"
+
+strings :: [String]
+strings = [ c : s | s <- "": strings, c <- ['a'..'z'] ]
+
+gen :: FreshVar -> AbsVar
+gen fresh = Var (strings !! fresh)
+
+-- standard evaluation semantics
+seval :: FreshVar -> TFormula -> AbsVar -> AbsVar -> MFormula
+-- for the Stream case, we assume that n < m
+seval _   (Stream label) n m = IndexedStream label n
+seval fresh (LAnd f1 f2) n m = And (seval fresh f1 n m ) (seval fresh f2 n m)
+seval fresh (LOr f1 f2) n m = Or (seval fresh f1 n m) (seval fresh f2 n m)
+seval fresh (LNot f1) n m = Not (seval fresh f1 n m)
+-- where the *magic* happens
+seval fresh (Globally f1) n m = Forall i n (Add m (-1)) (seval (fresh+1) f1 i m) where i = gen fresh
+seval fresh (Finally f1) n m = Exists i n (Add m (-1)) (seval (fresh+1) f1 i m) where i = gen fresh
+seval fresh (Until f1 f2) n m = Exists i n (Add m (-1)) (And (Forall j n (Add i (-1)) (f1')) f2')
+  where 
+    i = gen fresh
+    j = gen (fresh+1)
+    f1' = seval (fresh+2) f1 j m
+    f2' = seval (fresh+2) f2 i m
+seval fresh (Next f1) n m = Pf (seval fresh f1 (Add n 1) m)
+seval _ (Constant n) _ _ = Const n
+
+
+sevalTestWrap :: TFormula -> String
+sevalTestWrap expr = "evaluating:\n    " ++ show expr ++ "\nat " ++ show n ++ " till " ++ show m ++ " obtains: \n    " ++ show (seval fresh expr n m)
+  where
+    n = (gen 0)
+    m = (gen 1)
+    fresh = 2
+
+sevalTest1 :: String
+sevalTest1 = sevalTestWrap (Globally (Stream 0))
+sevalTest2 :: String
+sevalTest2 = sevalTestWrap (LAnd (Globally (Until (Stream 0) (Stream 1))) (Stream 0))
+
+
+compileEval :: TFormula -> IO ()
+compileEval expr = do
+  help "compiling:"
+  putStrLn (show expr)
+  help $ "at " ++ show n ++ " till " ++ show m ++ " obtains:"
+  putStrLn (show init)
+  help "after constantFolding 1:"
+  putStrLn (show folded)
+  help "after expanding:"
+  putStrLn (show expanded)
+  help "after constantFolding 2:"
+  putStrLn (show $ constantFolding expanded)
+  help "after primitive licm:"
+  putStrLn (show $ licm $ constantFolding expanded)
+  help $ "rec call (i.e. evaluating " ++ show n ++ " till " ++ show m' ++ ") is:"
+  putStrLn (show rec)
+  help "after constantFolding (rec call)"
+  putStrLn (show $ constantFolding rec)
+  putStrLn ""
+  where
+    n = (gen 0)
+    m' = (Add (gen 1) 1)
+    m = (Add m' 1)
+    fresh = 2
+    init = (seval fresh expr n m)
+    folded = constantFolding init
+    expanded = expand folded
+    rec = seval fresh expr n m'
+    help msg = do 
+      putStrLn msg
+      putStr "    "
+
+compileEval' :: TFormula -> IO ()
+compileEval' expr = do
+  help "compiling:"
+  putStrLn (show expr)
+  help $ "at " ++ show m' ++ " till " ++ show m ++ " obtains:"
+  putStrLn (show init)
+  help "after expanding:"
+  putStrLn (show expanded)
+  help "after constantFolding:"
+  putStrLn (show $ constantFolding expanded)
+  help "after primitive licm:"
+  putStrLn (show $ licm $ constantFolding expanded)
+  -- help $ "rec call (i.e. evaluating " ++ show n ++ " till " ++ show m' ++ ") is:"
+  -- putStrLn (show rec)
+  putStrLn ""
+  where
+    n = (gen 0)
+    m' = (Add (gen 1) 1)
+    m = (Add m' 1)
+    fresh = 2
+    init = (seval fresh expr m' m)
+    expanded = expand init
+    -- rec = show (seval fresh expr m m')
+    help msg = do 
+      putStrLn msg
+      putStr "    "
+       
+
+compileEvalTest1 :: IO ()
+compileEvalTest1 = compileEval (Globally (Stream 0))
+compileEvalTest2 :: IO ()
+compileEvalTest2 = compileEval (LAnd (Globally (Until (Stream 0) (Stream 1))) (Stream 0))
+compileEvalTest3 :: IO ()
+compileEvalTest3 = compileEval (Finally (Globally (Stream 0)))
+compileEvalTest4 :: IO ()
+compileEvalTest4 = compileEval (Globally (Until (Stream 0) (Stream 1)))
+compileEvalTest5 :: IO ()
+compileEvalTest5 = compileEval (Globally (Finally (Stream 0)))
+
+main :: IO ()
+main = do
+  compileEvalTest1
+  compileEvalTest2
+  compileEvalTest3
+  compileEvalTest4
+  compileEvalTest5
+  compileEval' (Until (Stream 0) (Stream 1))
+
+-- evaluation for recusive monitor construction
+subVar :: AbsVar -> AbsVar -> AbsVar -> AbsVar -- non-recurisve, maybe it should be
+subVar val match sub | val == match = sub
+subVar (Add var val) match sub | val > 1 = Add (subVar (Add var (val-1)) match sub) 1
+subVar (Add var val) match sub | val <= 1 = Add (subVar var match sub) val
+-- subVar (Minus var val) match sub = Minus (subVar var match sub) val
+subVar val match sub | otherwise = val
+
+mapVar :: MFormula -> AbsVar -> AbsVar -> MFormula
+mapVar (IndexedStream label index) match sub = IndexedStream label (subVar index match sub)
+mapVar (Forall i n m form)         match sub = Forall i (subVar n match sub) (subVar m match sub) (mapVar form match sub)
+mapVar (Exists i n m form)         match sub = Exists i (subVar n match sub) (subVar m match sub) (mapVar form match sub)
+-- mapVar (And f1 f2)                 match sub = And (mapVar f1 match sub) (mapVar f2 match sub)
+-- mapVar (Or f1 f2)                  match sub = Or (mapVar f1 match sub) (mapVar f2 match sub)
+-- mapVar (Not f)                     match sub = Not (mapVar f match sub)
+mapVar formula                     match sub = thread formula (\x -> mapVar x match sub)
+-- mapVar formula match substitute = _
+
+optimize :: MFormula -> MFormula
+optimize = licm . constantFolding 
+
+-- recursively apply a func to each node of an AST
+thread :: MFormula -> (MFormula -> MFormula) -> MFormula
+-- not sure if these two cases are necessary, tbh
+thread (Forall i n m f1) func = Forall i n m (func f1)
+thread (Exists i n m f1) func = Exists i n m (func f1)
+thread (And f1 f2) func = And (func f1) (func f2)
+thread (Or f1 f2) func = Or (func f1) (func f2)
+thread (Not f1) func = Not (func f1)
+thread (Pt f1) func = Pt (func f1)
+thread (Pf f1) func = Pf (func f1)
+thread (P f1) func = P (func f1)
+thread f1 _ = f1
+
+-- this will return true if two vars do not reference each other and false otherwise
+-- basically, if the vars are independent of each other, then this will return true
+-- example: b and b+1 are not independent
+-- example: b+1 and b+2 are not independent
+varsInd :: AbsVar -> AbsVar -> Bool
+varsInd (Var n) (Var m) = not (n == m) -- base case
+varsInd v@(Var _) (Add var1 _) = varsInd v var1
+-- varsInd v@(Var _) (Minus var1 _) = varsInd v var1
+varsInd (Add var1 _) v@(Var _) = varsInd v var1
+-- varsInd (Minus var1 _) v@(Var _) = varsInd v var1
+-- varsInd (Minus var1 _) (Minus var2 _) = varsInd var1 var2
+-- varsInd (Minus var1 _) (Add var2 _) = varsInd var1 var2
+varsInd (Add var1 _) (Add var2 _) = varsInd var1 var2
+-- varsInd (Add var1 _) (Minus var2 _) = varsInd var1 var2
+
+-- first compiler pass
+expand :: MFormula -> MFormula
+expand (Forall i n m@(Add m' 1) f1) | varsInd n m = And (expand $ Forall i n m' (expand f1)) (Pt $ mapVar f1 i m)
+expand (Exists i n m@(Add m' 1) f1) | varsInd n m = Or  (expand $ Exists i n m' (expand f1)) (Pf $ mapVar f1 i m)
+-- expand (Forall i n m@(Add m' 1) f1) | varsInd n m = And (expand $ Forall i n m' (expand f1)) (trace ("------{" ++ show f1 ++ " / " ++ show i ++ " / " ++ show m ++ "}------") $ mapVar f1 i m)
+-- expand (Exists i n m@(Add m' 1) f1) | varsInd n m = Or  (expand $ Exists i n m' (expand f1)) (trace ("------{" ++ show f1 ++ " / " ++ show i ++ " / " ++ show m ++ "}------") $ mapVar f1 i m)
+expand f1 = thread f1 expand
+
+-- reduce (a + 1 + 1) to (a + 2) and (a + 1 -1) to (a + 0);
+normAbsVar :: AbsVar -> AbsVar
+normAbsVar v@(Var _) = v
+normAbsVar (Add var 0) = normAbsVar var
+normAbsVar v@(Add (Var _) val) = v
+normAbsVar (Add (Add var val1) val2) = normAbsVar (Add var (val1 + val2))
+
+-- if we have a forall i in [n+1...n+1], sub all occurences of i with n+1
+-- we also normalize n+1-1 to n, etc.
+constantFolding :: MFormula -> MFormula
+constantFolding (Forall i n m f1) | (normAbsVar n) == (normAbsVar m) = constantFolding $ Pt (mapVar f1 i (normAbsVar n)) -- not sure if the pt is sound
+constantFolding (Forall i n m f1) | otherwise = Forall i (normAbsVar n) (normAbsVar m) (constantFolding f1)
+constantFolding (Exists i n m f1) | (normAbsVar n) == (normAbsVar m) = constantFolding $ Pf (mapVar f1 i (normAbsVar n)) -- not sure if the pf is sound
+constantFolding (Exists i n m f1) | otherwise = Exists i (normAbsVar n) (normAbsVar m) (constantFolding f1)
+constantFolding (IndexedStream label var) = IndexedStream label (normAbsVar var)
+constantFolding (Pt (Pf f1)) = constantFolding (P f1)
+constantFolding (Pf (Pt f1)) = constantFolding (P f1)
+constantFolding (Pf (Pf f1)) = constantFolding (Pf f1)
+constantFolding (Pt (Pt f1)) = constantFolding (Pt f1)
+constantFolding (Pt (Forall i n m f1)) = constantFolding (Forall i n m f1)
+constantFolding (Pf (Forall i n m f1)) = constantFolding (Forall i n m (Pf f1))
+constantFolding (P (Forall i n m f1)) = constantFolding (Forall i n m (P f1))
+constantFolding (Pf (Exists i n m f1)) = constantFolding (Exists i n m f1)
+constantFolding (Pt (Exists i n m f1)) = constantFolding (Exists i n m (Pt f1))
+constantFolding (P (Exists i n m f1)) = constantFolding (Exists i n m (P f1))
+constantFolding (Pf (And f1 s@(IndexedStream _ _))) = constantFolding (And f1 (Pf s))
+constantFolding (Pf (And f1 f2@(Pt _))) = constantFolding (And f1 (Pf f2))
+constantFolding (Pf (And f1 f2@(Pf _))) = constantFolding (And f1 (Pf f2))
+constantFolding (Pf (And f1 f2@(P _))) = constantFolding (And f1 (Pf f2))
+constantFolding (Pt (Or f1 s@(IndexedStream _ _))) = constantFolding (Or f1 (Pt s))
+constantFolding (Pt (Or f1 f2@(Pt _))) = constantFolding (Or f1 (Pt f2))
+constantFolding (Pt (Or f1 f2@(Pf _))) = constantFolding (Or f1 (Pt f2))
+constantFolding (Pt (Or f1 f2@(P _))) = constantFolding (Or f1 (Pt f2)) -- todo: add rules for negation
+constantFolding (P (Or f1 f2)) = constantFolding (Or (P f1) (P f2))
+constantFolding (P (And f1 f2)) = constantFolding (And (P f1) (P f2))
+constantFolding (P (Not f1)) = constantFolding (Not (P f1)) -- todo: double check this
+constantFolding f1 = thread f1 constantFolding
+
+-- returns true if AbsVar is not referenced in MFormula
+depIndAnalysis :: MFormula -> AbsVar -> Bool
+depIndAnalysis (IndexedStream _ index) var = varsInd index var
+depIndAnalysis (Forall _ n m formula) var = (varsInd n var) && (varsInd m var) && depIndAnalysis formula var
+depIndAnalysis (Exists _ n m formula) var = (varsInd n var) && (varsInd m var) && depIndAnalysis formula var
+depIndAnalysis (And f1 f2) var = depIndAnalysis f1 var && depIndAnalysis f2 var
+depIndAnalysis (Or f1 f2) var = depIndAnalysis f1 var && depIndAnalysis f2 var
+depIndAnalysis (Not f1) var = depIndAnalysis f1 var
+depIndAnalysis (Pt f1) var = depIndAnalysis f1 var
+depIndAnalysis (Pf f1) var = depIndAnalysis f1 var
+depIndAnalysis (P f1) var = depIndAnalysis f1 var
+depIndAnalysis _ _ = Prelude.True
+
+-- primitive licm, cannot peek more than one ast node down but is recursively applied at each level
+licm :: MFormula -> MFormula
+licm (Forall i _ _ f1) | depIndAnalysis f1 i = f1 -- todo: insert pf/pt in here?
+licm (Forall i n m (And f1 f2)) | depIndAnalysis f1 i = And (Forall i n m f2) f1
+licm (Forall i n m (And f1 f2)) | depIndAnalysis f2 i = And (Forall i n m f1) f2
+licm (Forall i n m (Or f1 f2)) | depIndAnalysis f1 i = Or (Forall i n m f2) f1
+licm (Forall i n m (Or f1 f2)) | depIndAnalysis f2 i = Or (Forall i n m f1) f2
+licm (Exists i _ _ f1) | depIndAnalysis f1 i = f1
+licm (Exists i n m (And f1 f2)) | depIndAnalysis f1 i = And (Exists i n m f2) f1
+licm (Exists i n m (And f1 f2)) | depIndAnalysis f2 i = And (Exists i n m f1) f2
+licm (Exists i n m (Or f1 f2)) | depIndAnalysis f1 i = Or (Exists i n m f2) f1
+licm (Exists i n m (Or f1 f2)) | depIndAnalysis f2 i = Or (Exists i n m f1) f2
+licm f1 | f1 == f1' = f1'
+        | otherwise = licm f1' -- should reach a fixpoint
+  where 
+    f1' = thread f1 licm 
+
+-- meval :: FreshVar -> TFormula -> AbsVar -> AbsVar -> MFormula
+-- meval 2 form n m@(Add m' 1) = reduce $ seval fresh form n m
+
+-- reduce  
+
+{-
+meval :: FreshVar -> TFormula -> AbsVar -> AbsVar -> MFormula
+-- for the Stream case, we assume that n < m
+meval fresh (Stream label) n m@(Add _ 1) = IndexedStream label n
+meval fresh (LAnd f1 f2) n m@(Add _ 1) = And (meval fresh f1 n m ) (meval fresh f2 n m)
+meval fresh (LOr f1 f2) n m@(Add _ 1) = Or (meval fresh f1 n m) (meval fresh f2 n m)
+meval fresh (LNot f1) n m@(Add _ 1) = Not (meval fresh f1 n m)
+-- where the *magic* happens
+meval fresh (Globally f1) n m@(Add m' 1) = And (Forall i n m' (meval (fresh+1) f1 i m)) (meval fresh f1 m m) where i = gen fresh
+meval fresh (Finally f1) n m@(Add m' 1) = Or (Exists i n m' (meval (fresh+1) f1 i m)) (meval fresh f1 m m) where i = gen fresh
+-- todo: below, until case
+meval fresh (Until f1 f2) n m@(Add m' 1) = Exists i n m' (And (Forall j n (Minus i 1) (f1')) f2')
+  where 
+    i = gen fresh
+    j = gen (fresh+1)
+    f1' = meval (fresh+2) f1 j m
+    f2' = meval (fresh+2) f2 i m
+meval fresh (Next f1) n m@(Add m' 1) = Pf (meval fresh f1 (Add n 1) m)
+meval _ (Constant n) _ _ = Const n
+meval _ _ _ _ = error "you should only be passing (m+1) to this func"
+-}
+
+-- nb: a compiler correctness proof would show that seval and meval are logically equivalent
diff --git a/examples/Mltl.hs b/examples/Mltl.hs
new file mode 100644
index 000000000..16b837fca
--- /dev/null
+++ b/examples/Mltl.hs
@@ -0,0 +1,221 @@
+{-# LANGUAGE NoImplicitPrelude #-}
+{-# LANGUAGE RebindableSyntax #-}
+
+module Mltl where
+
+import Language.Copilot hiding  (alwaysBeen, eventuallyPrev, since)
+
+import qualified Prelude (take, repeat, (<), (>), (++), (==))
+
+-- FTLTL impl
+-- 0 corresponds to False
+-- 1 corresponds to Presumably False
+-- 2 corresponds to Presumably True
+-- 3 corresponds to True
+fc :: Int8 -- false
+fc = 0
+
+f :: Stream Int8
+f = constI8 fc
+
+pfc :: Int8 -- presumably false
+pfc = 1
+
+pf :: Stream Int8
+pf = constI8 pfc
+
+ptc :: Int8 -- presumably false
+ptc = 2
+
+pt :: Stream Int8
+pt = constI8 ptc
+
+tc :: Int8 -- true
+tc = 3
+
+t :: Stream Int8
+t = constI8 tc
+
+-- UB behavior, should never occur
+errC :: Int8
+errC = -1
+
+err :: Stream Int8
+err = constI8 errC
+
+and' :: Stream Int8 -> Stream Int8 -> Stream Int8
+and' s1 s2 = if (s1 < s2) then s1 else s2 -- refactor out
+
+or' :: Stream Int8 -> Stream Int8 -> Stream Int8
+or' s1 s2 = if (s1 < s2) then s2 else s1 -- refactor out
+
+not' :: Stream Int8 -> Stream Int8
+not' s1 = if (s1 == f) then t else 
+  (if (s1 == pf) then pt else 
+  (if (s1 == pt) then pf else 
+  (if (s1 == t) then (f) else err)))
+
+implies' :: Stream Int8 -> Stream Int8 -> Stream Int8
+implies' s1 s2 = not' (and' s1 (not' s2))
+
+
+-- mask everything but the first
+maskFirst :: Stream Int8 -> Stream Int8
+maskFirst s = and' mask s
+  where
+    mask = ([tc] ++ f)
+    
+maskSecond :: Stream Int8 -> Stream Int8
+maskSecond s = and' mask s
+  where
+    mask = ([fc, tc] ++ f)
+
+takeHighest :: Stream Int8 -> Stream Int8
+takeHighest s = go
+  where
+    go = or' s ([fc] ++ go)
+    
+takeHighestPf :: Stream Int8 -> Stream Int8
+takeHighestPf s = go
+  where
+    go = or' s ([pfc] ++ go)
+    
+takeLowest :: Stream Int8 -> Stream Int8
+takeLowest s = go
+  where
+    go = and' s ([tc] ++ go)
+
+-- formal spec
+-- sound but not precise (since we cannot "peek" ahead even if taut)
+eNext :: Stream Int8 -> Stream Int8
+eNext s = or' ([pfc] ++ f)
+               (takeHighest (maskSecond s))
+
+uNext :: Stream Int8 -> Stream Int8
+uNext s = or' ([ptc] ++ f)
+              (takeHighest (maskSecond s))
+
+
+-- can be falsified, but vaculously presumably true
+globally' :: Stream Int8 -> Stream Int8
+-- globally' s = and' pt (takeLowest s)
+globally' s = go s where
+  go s = and' (go ([ptc] ++ s)) (takeLowest s)
+  -- go s = and' ([ptc] ++ (go s)) (takeLowest s)
+
+-- can never be falsified, lowest is pfc, vaculously presumably false
+finally :: Stream Int8 -> Stream Int8
+finally s = or' pf (takeHighest s)
+
+-- does not need stop
+weakUntil' :: Stream Int8 -> Stream Int8 -> Stream Int8
+weakUntil' s1 s2 = globally' 
+  (or' (globally' s1) ( (takeHighest s2)))
+  -- (or' (globally' s1) (eNext s2))
+  -- maybe swap takeHighest with finally
+
+-- needs to stop
+strongUntil' :: Stream Int8 -> Stream Int8 -> Stream Int8
+strongUntil' s1 s2 = takeHighest (and' (weakUntil' s1 s2) s2)
+
+-- will mask at interval [m, n]
+maskNthTrueRange :: Int -> Int -> Stream Int8 -> Stream Int8
+maskNthTrueRange m n s = or' mask s
+    where
+      mask = ((Prelude.take m (Prelude.repeat tc)) Prelude.++ (Prelude.take (n - m) (Prelude.repeat fc))) ++ t
+
+maskNthFalseRange :: Int -> Int -> Stream Int8 -> Stream Int8
+maskNthFalseRange m n s = and' mask s
+    where
+      mask = ((Prelude.take m (Prelude.repeat fc)) Prelude.++ (Prelude.take (n - m) (Prelude.repeat tc))) ++ f
+
+globallyWithin :: Int -> Int -> Stream Int8 -> Stream Int8
+globallyWithin m n s = and' streamMask defaultPresumablyTrueMask
+  where
+    defaultPresumablyTrueMask = maskNthTrueRange 0 n pt
+    streamMask = takeLowest (maskNthTrueRange m n s)
+
+-- todo: double check below, dual to above
+finallyWithin :: Int -> Int -> Stream Int8 -> Stream Int8
+finallyWithin m n s = or' streamMask defaultPresumablyFalseMask
+  where
+    defaultPresumablyFalseMask = maskNthFalseRange 0 n pf
+    streamMask = takeHighest (maskNthFalseRange m n s)
+
+-- todo: double check the below
+weakUntilWithin :: Int -> Int -> Stream Int8 -> Stream Int8 -> Stream Int8
+weakUntilWithin m n s1 s2 = or' (globallyWithin m n s1) (finallyWithin m n s2)
+
+strongUntilWithin :: Int -> Int -> Stream Int8 -> Stream Int8 -> Stream Int8
+strongUntilWithin m n s1 s2 = finallyWithin m n (and' (weakUntilWithin m n s1 s2) s2)
+
+-- PTLTL port from Copilot lang (need to double check)
+previous :: Stream Int8 -> Stream Int8
+previous s = [ fc ] ++ s
+
+alwaysBeen :: Stream Int8 -> Stream Int8
+alwaysBeen s = and' s tmp
+    where
+      tmp = and' ([ tc ] ++ s) tmp
+
+-- ever used to be named eventuallyPre, ported from PTLTL
+ever :: Stream Int8 -> Stream Int8
+ever s = or' s tmp
+  where
+    tmp = or' ([ fc ] ++ s) tmp
+
+-- everything below is mine
+-- todo: check if equiv
+-- used to be named historically
+alwaysBeenMine :: Stream Int8 -> Stream Int8
+alwaysBeenMine s = go
+  where 
+    go = and' s ([ tc ] ++ go)
+
+everMine :: Stream Int8 -> Stream Int8
+everMine s = go
+  where
+    go = or' s ([ fc ] ++ go)
+
+sinceMine :: Stream Int8 -> Stream Int8 -> Stream Int8
+sinceMine s1 s2 = everMine (implies' s2 (alwaysBeenMine s1))
+
+
+specFTLTL = do
+  observer "s1" input1
+  observer "s2" input2
+  -- observer "weakUntil" (weakUntilWithin 1 5 input1 input2)
+  -- observer "strongUntilWithin" (strongUntilWithin 1 5 input1 input2)
+  -- observer "globallyWithin s1" (globallyWithin 3 4 input1)
+  -- observer "finallyWithin s1" (finallyWithin 2 4 input1)
+  -- observer "input2" input2
+  -- observer "not1" (not' input1)
+  -- observer "not2" (not' input2)
+  -- observer "identity1" (not' (strongUntil' input1 input2))
+  -- observer "identity2'" (weakUntil' (not' input1) (not' input2))
+  -- observer "globally input1" (globally' input1)
+  observer "implies globally" (implies' (globally' input1) input2)
+  observer "globally implies globally" (globally' (implies' (globally' input1) input2))
+  -- observer "finally input2" (finally input2)
+  -- observer "weakUntil'" (weakUntil' input1 input2)
+  -- observer "strongUntil'" (strongUntil' input1 input2)
+  -- observer "strongUntilTmp" (strongUntilTmp input1 input2)
+  -- observer "maskFirst input1" (maskFirst input1)
+  -- observer "takeHighest input1" (takeHighest input1)
+  -- observer "input2" input2
+  -- observer "universalNext' input2" (universalNext' input2)
+  where
+    input1 = [fc, tc, tc] ++ t
+    -- input1 = f
+    -- input2 = f
+    -- input2 = [fc, pfc, tc] ++ f
+    input2 = [tc, tc, fc] ++ f
+    -- input1 = pf
+    -- input1 = [3, 1, 1] ++ f
+    -- input1 = [0, 0, 3] ++ f
+    -- input1 = [0] ++ t
+    -- input1 = [3] ++ f
+    -- input1 = t
+
+-- Interpret the spec for 10 ticks
+main = interpret 10 specFTLTL
diff --git a/examples/Test.hs b/examples/Test.hs
new file mode 100644
index 000000000..0801a5ac3
--- /dev/null
+++ b/examples/Test.hs
@@ -0,0 +1,303 @@
+{-# OPTIONS_GHC -Wincomplete-patterns #-}
+{-# LANGUAGE GADTs #-}
+
+-- import Debug.Trace
+
+import Test.QuickCheck
+import Test.QuickCheck.Gen
+import Test.QuickCheck.Random
+import Test.QuickCheck.Monadic
+
+import Prelude hiding (True, False)
+import qualified Language.Copilot
+import qualified Copilot.Interpret
+import Copilot.PrettyPrint
+
+import Data.List
+import Data.String
+import Data.Char
+import System.IO
+
+import qualified Mltl
+
+data Formula where
+  -- labeled variables/streams
+  Var :: Int -> Formula
+
+  -- constants (sometimes useful in LTL formulae)
+  True :: Formula
+  False :: Formula
+  PresumablyTrue :: Formula  -- unsure if this is needed
+  PresumablyFalse :: Formula -- unsure if this is needed
+
+  -- standard logical operators
+  And :: Formula -> Formula -> Formula
+  Or :: Formula -> Formula -> Formula
+  Implies :: Formula -> Formula -> Formula
+  Not :: Formula -> Formula
+
+  -- PTLTL operators, unbounded
+  AlwaysBeen :: Formula -> Formula     -- past tense globally
+  Previous :: Formula -> Formula         -- is it true in the previous time step
+  Ever :: Formula -> Formula             -- has it ever been true in any previous time step
+  Since :: Formula -> Formula -> Formula -- has the first stream held since the second stream has been true
+
+  -- FTLTL operators, unbounded
+  Globally :: Formula -> Formula         -- globally/box
+  Next :: Formula -> Formula             -- is it true in the next time step
+  Finally :: Formula -> Formula          -- will it be true in any future time step
+  Until :: Formula -> Formula -> Formula -- has the first stream held until the second stream has been true
+
+  -- MLTL operators, bounded
+  GloballyWithin :: Int -> Int -> Formula -> Formula
+  FinallyWithin :: Int -> Int -> Formula -> Formula
+  UntilWithin :: Int -> Int -> Formula -> Formula -> Formula
+
+  deriving (Eq, Ord, Read)
+
+instance Show Formula where
+  -- questions: what is zeta? should I implement equiv, xor, etc?
+  show (Var n) = "ATOM(state_fun(" ++ show n ++ "))"
+  show True  = "TRUE"
+  show False  = "FALSE"
+  show PresumablyTrue  = "TRUE"
+  show PresumablyFalse  = "FALSE"
+
+  show (And f1 f2) = "AND_MTL(" ++ show f1 ++ "," ++ show f2 ++ ")"
+  show (Or f1 f2) = "OR_MTL(" ++ show f1 ++ "," ++ show f2 ++ ")"
+  show (Implies f1 f2) = "IMPLIES_MTL(" ++ show f1 ++ "," ++ show f2 ++ ")"
+  show (Not f1) = "NOT_MTL(" ++ show f1 ++ ")"
+
+  show (AlwaysBeen f1) = "HISTORICALLY(" ++ show f1 ++ ")"
+  show (Previous f1) = "PREVIOUS(" ++ show f1 ++ ")"
+  show (Ever f1) = "ONCE(" ++ show f1 ++ ")"
+  show (Since f1 f2) = "SINCE(" ++ show f1 ++ "," ++ show f2 ++ ")"
+
+  show (Globally f1) = "GLOBALLY(" ++ show f1 ++ ")"
+  show (Next f1) = "NEXT(" ++ show f1 ++ ")"
+  show (Finally f1) = "FINALLY(" ++ show f1 ++ ")"
+  show (Until f1 f2) = "UNTIL(" ++ show f1 ++ "," ++ show f2 ++ ")"
+   
+  show (GloballyWithin m n f1) = "GLOBALLY_BD(" ++ show f1 ++ ",[|" ++ show m ++ "," ++ show n ++ "|])"
+  show (FinallyWithin m n f1) = "FINALLY_BD(" ++ show f1 ++ ",[|" ++ show m ++ "," ++ show n ++ "|])"
+  show (UntilWithin m n f1 f2) = "UNTIL_BD(" ++ show f1 ++ "," ++ show f2 ++ ",[|" ++ show m ++ "," ++ show n ++ "|])"
+
+
+-- used for generating streams
+-- might need to switch to listOf (otherwise terms may explode, depending on how lazy the Copilot interpreter is)
+genInputs :: Int -> Gen [Language.Copilot.Int8]
+genInputs size = fmap (Prelude.take size) (infiniteListOf (elements [Mltl.fc, Mltl.tc]))
+
+genInputsP :: Int -> Gen [Language.Copilot.Int8]
+genInputsP size = fmap (Prelude.take size) (infiniteListOf (elements [Mltl.fc, Mltl.pfc, Mltl.ptc, Mltl.tc]))
+
+-- QuickCheck generators
+genConstants :: Gen Formula
+genConstants = elements [True, False]
+
+genConstantsP :: Gen Formula
+genConstantsP = elements [True, False, PresumablyTrue, PresumablyFalse]
+
+genUnary :: Gen (Formula -> Formula)
+genUnary = (elements [Not, AlwaysBeen, Previous, Ever, Globally, Next, Finally]) -- <*> f
+
+genBinary :: Gen (Formula -> Formula -> Formula)
+genBinary = elements [And, Or, Implies, Since, Until]
+
+genVars :: Int -> [Formula]
+genVars n = map (\x -> Var x) [0..n]
+
+-- generate formulae with up to n variables (nb: I removed genConstants from this list)
+genFormula :: Int -> Gen Formula
+genFormula n = oneof [vars >>= elements, genUnary <*> genFormula n, (genBinary <*> genFormula n) <*> genFormula n]
+  where
+    vars = shuffle (genVars n)
+
+genBoundedFormula :: Int -> Int -> Int -> Gen Formula -> Gen Formula
+genBoundedFormula lowerBound upperBound n generator = do 
+  lower <- chooseBoundedIntegral (lowerBound, upperBound)
+  upper <- chooseBoundedIntegral (lower, upperBound)
+  f1 <- generator
+  f2 <- generator
+  elements [
+      (GloballyWithin lower upper f1),
+      (FinallyWithin lower upper f1),
+      (UntilWithin lower upper f1 f2)
+    ]
+
+genFormulaWeightedBound :: Int -> Int -> Int ->  Gen Formula
+genFormulaWeightedBound upperBound lowerBound n = genFormulaWeightedBoundHelp upperBound lowerBound n 4
+
+genFormulaWeightedBoundHelp upperBound lowerBound n iter = frequency [
+    (2 * iter, vars >>= elements), 
+    -- (1 * iter, genConstants), 
+    (3, genUnary <*> self), 
+    (3, (genBinary <*> self) <*> self),
+    (2, genBoundedFormula upperBound lowerBound n self)
+  ] 
+  where 
+    self = genFormulaWeightedBoundHelp upperBound lowerBound n (iter+1)
+    vars = shuffle (genVars n)
+
+toCopilot :: Formula -> [(Int, Language.Copilot.Stream Language.Copilot.Int8)] -> Language.Copilot.Stream Language.Copilot.Int8
+toCopilot (Var n) varMap = case lookup n varMap of
+  Just x -> x
+  Nothing -> error "Invalid variable lookup"
+toCopilot (True) varMap = Mltl.t
+toCopilot (False) varMap = Mltl.f
+toCopilot (PresumablyTrue) varMap = Mltl.pt
+toCopilot (PresumablyFalse) varMap = Mltl.pf
+
+toCopilot (And f1 f2) varMap = Mltl.and' (toCopilot f1 varMap) (toCopilot f2 varMap)
+toCopilot (Or f1 f2) varMap = Mltl.or' (toCopilot f1 varMap) (toCopilot f2 varMap)
+toCopilot (Implies f1 f2) varMap = Mltl.implies' (toCopilot f1 varMap) (toCopilot f2 varMap)
+toCopilot (Not f1) varMap = Mltl.not' (toCopilot f1 varMap) 
+
+-- default to mine when possible
+toCopilot (AlwaysBeen f1) varMap = Mltl.alwaysBeenMine (toCopilot f1 varMap) 
+toCopilot (Previous f1) varMap = Mltl.previous (toCopilot f1 varMap) 
+toCopilot (Ever f1) varMap = Mltl.everMine (toCopilot f1 varMap) 
+toCopilot (Since f1 f2) varMap = Mltl.sinceMine (toCopilot f1 varMap) (toCopilot f2 varMap)
+
+toCopilot (Globally f1) varMap = Mltl.globally' (toCopilot f1 varMap) 
+toCopilot (Next f1) varMap = Mltl.eNext (toCopilot f1 varMap) 
+toCopilot (Finally f1) varMap = Mltl.finally (toCopilot f1 varMap) 
+toCopilot (Until f1 f2) varMap = Mltl.strongUntil' (toCopilot f1 varMap) (toCopilot f2 varMap)
+
+toCopilot (GloballyWithin m n f1) varMap = Mltl.globallyWithin m n (toCopilot f1 varMap)
+toCopilot (FinallyWithin m n f1) varMap = Mltl.finallyWithin m n (toCopilot f1 varMap)
+toCopilot (UntilWithin m n f1 f2) varMap = Mltl.strongUntilWithin m n (toCopilot f1 varMap) (toCopilot f2 varMap)
+
+
+
+formulaSpec :: Formula -> [(Int, [Language.Copilot.Int8])] -> Language.Copilot.Spec
+formulaSpec formula inputs = Language.Copilot.observer "output" output
+  where
+    output = toCopilot formula inputStreams
+    inputStreams =
+      map (\(k, v) -> (k, Language.Copilot.extern ("x" ++ show k) (Just v))) inputs
+
+data Config = Config
+    { lowerBound    :: Int -- the lowest number that a bounded temporal operator will have
+    , upperBound    :: Int -- the highest number
+    , varCount      :: Int -- the max number of vars in the random LTL formula
+    , inputSize     :: Int -- the size of the input stream that will be randomly generated
+    }
+
+defaultConfig = Config 
+    { lowerBound = 0
+    , upperBound = 10
+    , varCount = 2
+    , inputSize = 20
+    }
+
+type Seed = Int
+
+randomFormula :: Config -> QCGen -> Formula
+randomFormula config rng = Test.QuickCheck.Gen.unGen gen rng 0 -- this constant is arbitrary
+  where
+    gen :: Gen Formula
+    gen = genFormulaWeightedBound (lowerBound config) (upperBound config) (varCount config) 
+
+printFormula :: Formula -> IO ()
+printFormula f = putStrLn $ (show f) ++ " % MTL_FORMULA"
+
+randomInput :: Config -> QCGen -> [Language.Copilot.Int8]
+randomInput config rng = Test.QuickCheck.Gen.unGen gen rng 0 -- this constant is arbitrary
+  where
+    gen :: Gen [Language.Copilot.Int8]
+    gen = genInputs (inputSize config)
+
+-- printInputs :: [(Int, [Language.Copilot.Int8])] -> IO ()
+-- printInputs inputs = mapM_ putStrLn (map show inputs))
+
+printInputs :: [(Int, [Language.Copilot.Int8])] -> IO ()
+printInputs inputs = putStrLn $ "(:" ++ intercalate ", " (map prettyPrint array) ++ ":)"
+  where
+    array = (transpose (map snd inputs))
+    prettyPrint :: [Language.Copilot.Int8] -> String
+    prettyPrint l = "(:" ++ intercalate "," (map printTruth l) ++ ":)"
+
+printTruth :: Language.Copilot.Int8 -> String
+printTruth 0 = "FALSE"
+-- printTruth 1 = "PRESUMABLY_FALSE"
+printTruth 1 = "FALSE"
+-- printTruth 2 = "PRESUMABLY_TRUE"
+printTruth 2 = "TRUE"
+printTruth 3 = "TRUE"
+printTruth n = error "undefined when trying to showTruth, encountered " ++ show n
+-- printInputs inputs = mapM_ putStrLn (map show inputs)
+
+parseOutput :: String -> [Language.Copilot.Int8]
+parseOutput output = map (read . strip) (drop 1 (lines output))
+  where
+    strip x = filter (not . isSpace) x
+
+-- parses and pretty-prints output
+transformOutput :: String -> String
+transformOutput output = "(:" ++ intercalate "," (map printTruth (parseOutput output)) ++ ":)"
+
+evaluate :: Formula -> [(Int, [Language.Copilot.Int8])] -> IO String
+evaluate formula inputs = do
+    reifiedSpec <- Language.Copilot.reify spec
+    -- putStrLn $ prettyPrint reifiedSpec -- for debugging
+    return (numSamples `seq` Copilot.Interpret.interpret Copilot.Interpret.Table numSamples reifiedSpec)
+    -- Language.Copilot.interpret (fromIntegral numSamples) spec
+  where
+    numSamples :: Int
+    numSamples = maximum $ map length $ map snd inputs
+    spec = formulaSpec formula inputs
+
+runTest :: Config -> Seed -> IO ()
+runTest config seed = do
+  -- putStrLn $ show inputs
+  putStrLn "% Inputs"
+  putStrLn $ show ((inputSize config) - 1) ++ " % last timestep"
+
+  hFlush stdout
+
+  printFormula formula
+  printInputs inputs
+
+  hFlush stdout
+
+  putStrLn "% Expected value"
+  output <- evaluate formula inputs
+  -- putStrLn $ output
+  putStrLn $ transformOutput output
+
+  hFlush stdout
+  where
+    rng :: QCGen
+    rng = mkQCGen seed
+    formula = randomFormula config (integerVariant 0 rng)
+    -- formula = Var 1 -- for debugging
+    inputs = map (\n -> (fromIntegral n, randomInput config (integerVariant n rng))) [0..(fromIntegral (varCount config))]
+
+runTests :: Int -> IO()
+runTests n = do
+  mapM_ (\x -> runTest defaultConfig x) [0..n]
+
+-- main = runTests 2
+main = runTests 100000
+
+-- some properties to test
+prop_CanGen seed = randomFormula defaultConfig (mkQCGen seed) == randomFormula defaultConfig (mkQCGen seed)
+
+prop_FormulaDeterministic seed = monadicIO $ do
+  f1 <- run $ printFormula $ randomFormula defaultConfig (mkQCGen seed)
+  f2 <- run $ printFormula $ randomFormula defaultConfig (mkQCGen seed)
+  assert (f1 == f2)
+
+prop_InputDeterministic seed = monadicIO $ do
+  i1 <- run $ printInputs [(0, randomInput defaultConfig (mkQCGen seed))]
+  i2 <- run $ printInputs [(0, randomInput defaultConfig (mkQCGen seed))]
+  assert (i1 == i2)
+
+{-
+prop_DoubleNegationElim seed varCount = monadicIO $ do
+  undefined
+  where
+    rng :: QCGen
+    rng = mkQCGen seed
+-}
diff --git a/examples/examples.cabal b/examples/examples.cabal
new file mode 100644
index 000000000..471bcb128
--- /dev/null
+++ b/examples/examples.cabal
@@ -0,0 +1,174 @@
+cabal-version:      3.0
+-- The cabal-version field refers to the version of the .cabal specification,
+-- and can be different from the cabal-install (the tool) version and the
+-- Cabal (the library) version you are using. As such, the Cabal (the library)
+-- version used must be equal or greater than the version stated in this field.
+-- Starting from the specification version 2.2, the cabal-version field must be
+-- the first thing in the cabal file.
+
+-- Initial package description 'examples' generated by
+-- 'cabal init'. For further documentation, see:
+--   http://haskell.org/cabal/users-guide/
+--
+-- The name of the package.
+name:               examples
+
+-- The package version.
+-- See the Haskell package versioning policy (PVP) for standards
+-- guiding when and how versions should be incremented.
+-- https://pvp.haskell.org
+-- PVP summary:     +-+------- breaking API changes
+--                  | | +----- non-breaking API additions
+--                  | | | +--- code changes with no API change
+version:            0.1.0.0
+
+-- A short (one-line) description of the package.
+-- synopsis:
+
+-- A longer description of the package.
+-- description:
+
+-- The license under which the package is released.
+license:            NONE
+
+-- The package author(s).
+author:             Max Fan
+
+-- An email address to which users can send suggestions, bug reports, and patches.
+maintainer:         maxwell.y.fan@nasa.gov
+
+-- A copyright notice.
+-- copyright:
+build-type:         Simple
+
+-- Extra doc files to be distributed with the package, such as a CHANGELOG or a README.
+extra-doc-files:    CHANGELOG.md
+
+-- Extra source files to be distributed with the package, such as examples, or a tutorial module.
+-- extra-source-files:
+
+common warnings
+    ghc-options: -Wall
+
+library
+  exposed-modules: Mltl, Uav, Future
+  -- other-modules:
+  build-depends:    base,
+                    copilot,
+                    copilot-libraries,
+                    copilot-language,
+                    copilot-interpreter,
+                    QuickCheck
+  hs-source-dirs: .
+  default-language: Haskell2010
+
+executable setarray
+    -- Import common warning flags.
+    import:           warnings
+
+    -- .hs or .lhs file containing the Main module.
+    main-is:          SetArray.hs
+
+    -- Modules included in this executable, other than Main.
+    -- other-modules: -- Mltl
+
+    -- LANGUAGE extensions used by modules in this package.
+    -- other-extensions:
+
+    -- Other library packages from which modules are imported.
+    build-depends:    base,
+                      copilot,
+                      copilot-language,
+                      copilot-interpreter,
+                      copilot-c99,
+                      QuickCheck
+
+    -- Directories containing source files.
+    hs-source-dirs:   .
+
+    -- Base language which the package is written in.
+    default-language: Haskell2010
+
+executable temporal-test
+    -- Import common warning flags.
+    import:           warnings
+
+    -- .hs or .lhs file containing the Main module.
+    main-is:          Test.hs
+
+    -- Modules included in this executable, other than Main.
+    other-modules: Mltl
+
+    -- LANGUAGE extensions used by modules in this package.
+    -- other-extensions:
+
+    -- Other library packages from which modules are imported.
+    build-depends:    base,
+                      copilot,
+                      copilot-language,
+                      copilot-interpreter,
+                      copilot-prettyprinter,
+                      QuickCheck
+
+    -- Directories containing source files.
+    hs-source-dirs:   .
+
+    -- Base language which the package is written in.
+    default-language: Haskell2010
+    ghc-options: 
+         -O3
+
+executable uav
+    -- Import common warning flags.
+    import:           warnings
+
+    -- .hs or .lhs file containing the Main module.
+    main-is:          UavTest.hs
+
+    -- Modules included in this executable, other than Main.
+    other-modules: Mltl, Uav
+
+    -- LANGUAGE extensions used by modules in this package.
+    -- other-extensions:
+
+    -- Other library packages from which modules are imported.
+    build-depends:    base,
+                      copilot,
+                      copilot-libraries,
+                      copilot-language,
+                      copilot-interpreter,
+                      QuickCheck
+
+    -- Directories containing source files.
+    hs-source-dirs:   .
+
+    -- Base language which the package is written in.
+    default-language: Haskell2010
+
+executable experiment
+    -- Import common warning flags.
+    import:           warnings
+
+    -- .hs or .lhs file containing the Main module.
+    main-is:          Experiment.hs
+
+    -- Modules included in this executable, other than Main.
+    -- other-modules: -- Mltl, Uav
+
+    -- LANGUAGE extensions used by modules in this package.
+    -- other-extensions:
+
+    -- Other library packages from which modules are imported.
+    build-depends:    base,
+                      copilot,
+                      copilot-libraries,
+                      copilot-language,
+                      copilot-interpreter,
+                      copilot-prettyprinter,
+                      QuickCheck
+
+    -- Directories containing source files.
+    hs-source-dirs:   .
+
+    -- Base language which the package is written in.
+    default-language: Haskell2010