diff --git a/Dockerfile b/Dockerfile index 7bcde69..1809eb7 100644 --- a/Dockerfile +++ b/Dockerfile @@ -4,6 +4,3 @@ RUN apt-get update # Install Copilot from the Debian repositories. RUN apt-get install --yes libghc-copilot-dev - -# Install solver we will use with copilot-theorem. -RUN apt-get install --yes z3 diff --git a/FM24-slides.pdf b/FM24-slides.pdf new file mode 100644 index 0000000..c2033ba Binary files /dev/null and b/FM24-slides.pdf differ diff --git a/FM24-slides.pptx b/FM24-slides.pptx new file mode 100644 index 0000000..f769276 Binary files /dev/null and b/FM24-slides.pptx differ diff --git a/INSTALL.md b/INSTALL.md index 973f337..8afbdd5 100644 --- a/INSTALL.md +++ b/INSTALL.md @@ -1,6 +1,6 @@ # Installation -To run Copilot and use the exercises in this repository, we need: +In order to run Copilot and use the exercises in this repository, we need: 1. A POSIX compatible host system, e.g. most Linux or MacOS. Windows probably works as well. @@ -14,9 +14,9 @@ repository provides a `Makefile`. From the root of the repository execute: $ make ``` -This will build a Debian-testing based image containing a Copilot installation, -and run a test to check if it works correctly. If no errors are reported, the -end of the output should match: +This will build a Debian testing based image containing a Copilot installation, +and run a test to check if it works correctly. If no errors are reported, and +the end of the output should match: ``` test: @@ -34,9 +34,7 @@ test: ## Cleaning up -When, after the tutorial the docker image is not necessary anymore, it can -easily be removed from the system with: +When after the tutorial the docker image is not necessary anymore, it can +easily be removed from the system with a: -```sh $ make clean -``` diff --git a/Makefile b/Makefile index d366bab..76ffbd2 100644 --- a/Makefile +++ b/Makefile @@ -3,10 +3,10 @@ IMAGE=formal-methods-2024-copilot-tutorial all: test build: - docker build --progress plain -t $(IMAGE) . + docker build --progress plain --no-cache -t $(IMAGE) . test: build - bin/rundocker runhaskell exercises/Test.hs + bin/rundocker exercises/test/run.sh clean: docker image rm -f $(IMAGE) diff --git a/README.md b/README.md index 6c7e09a..2f9e719 100644 --- a/README.md +++ b/README.md @@ -44,18 +44,11 @@ Please see `INSTALL.md` for installation. ## Running the exercises -Each exercise comes with its own file. There are two ways to run them, either -by passing `bin/rundocker runhaskell` followed by the file to run: +Each exercise comes with its own `run.sh` script to make things easier. This +script must be ran inside Docker using `bin/rundocker` -```sh -$ bin/rundocker runhaskell exercises/Ex??-??.hs -``` - -Or, passing no arguments to open up a terminal inside the container in which we -can call `runhaskell`: +For example, to run the `test` one can: ```sh -$ bin/rundocker -# cd /exercises/ -# runhaskell Ex??-??.hs +$ bin/rundocker exercises/test/run.sh ``` diff --git a/exercises/Ex01-01.hs b/exercises/Ex01-01.hs index f34b485..42a5268 100644 --- a/exercises/Ex01-01.hs +++ b/exercises/Ex01-01.hs @@ -8,5 +8,5 @@ main :: IO () main = interpret 10 spec spec :: Spec -spec = trigger "trigger1" true [] +spec = trigger "sample1" true [] -- The name is customizable. diff --git a/exercises/Ex01-02.hs b/exercises/Ex01-02.hs index d8f465b..402ee37 100644 --- a/exercises/Ex01-02.hs +++ b/exercises/Ex01-02.hs @@ -8,4 +8,4 @@ main :: IO () main = interpret 10 spec spec :: Spec -spec = trigger "trigger1" true [arg true, arg false] +spec = trigger "sample1" true [arg true, arg false] diff --git a/exercises/Ex01-03.hs b/exercises/Ex01-03.hs index c0ea162..d1233c1 100644 --- a/exercises/Ex01-03.hs +++ b/exercises/Ex01-03.hs @@ -8,7 +8,7 @@ main :: IO () main = interpret 10 spec spec :: Spec -spec = trigger "trigger1" myTrue [arg true, arg myFalse, arg zero, arg one] +spec = trigger "sample1" myTrue [arg true, arg myFalse, arg zero, arg one] myTrue :: Stream Bool myTrue = true diff --git a/exercises/Ex01-04.hs b/exercises/Ex01-04.hs index 01461ed..f14f876 100644 --- a/exercises/Ex01-04.hs +++ b/exercises/Ex01-04.hs @@ -1,7 +1,7 @@ {-# LANGUAGE RebindableSyntax #-} import Language.Copilot --- 5 minutes +-- 5 -- Show how we can apply operators to streams. -- Additionally shows multiple triggers in a spec. @@ -9,7 +9,7 @@ main :: IO () main = interpret 10 spec spec :: Spec -spec = trigger "trigger1" myTrue [arg true, arg myFalse, arg negative_one] +spec = trigger "sample1" myTrue [arg true, arg myFalse, arg negative_one] myTrue :: Stream Bool myTrue = true @@ -21,6 +21,6 @@ myFalse = not myTrue one :: Stream Int32 one = 1 --- - :: Stream Int32 -> Stream Int32 +-- (-) :: Stream Int32 -> Stream Int32 negative_one :: Stream Int32 negative_one = - one diff --git a/exercises/Ex01-05.hs b/exercises/Ex01-05.hs index 378b65d..3d00c98 100644 --- a/exercises/Ex01-05.hs +++ b/exercises/Ex01-05.hs @@ -1,7 +1,7 @@ {-# LANGUAGE RebindableSyntax #-} import Language.Copilot --- 5 minutes +-- 5 m -- Shows binary operations. -- As a bonus, it shows how to have multiple triggers as well. @@ -10,9 +10,9 @@ main = interpret 10 spec spec :: Spec spec = do -- notice the `do` and the indentation! - trigger "trigger1" myTrue [arg myTrue, arg false] - trigger "trigger2" myFalse [] - trigger "trigger3" mySth [arg two, arg six] + trigger "sample1" myTrue [arg myTrue, arg false] + trigger "sample2" myFalse [] + trigger "sample3" mySth [arg two, arg six] myTrue :: Stream Bool myTrue = true @@ -20,7 +20,7 @@ myTrue = true myFalse :: Stream Bool myFalse = not myTrue --- || :: Stream Bool -> Stream Bool -> Stream Bool +-- (||) :: Stream Bool -> Stream Bool -> Stream Bool mySth :: Stream Bool mySth = not myTrue || myTrue diff --git a/exercises/Ex01-06.hs b/exercises/Ex01-06.hs index b587dba..4eab61f 100644 --- a/exercises/Ex01-06.hs +++ b/exercises/Ex01-06.hs @@ -1,7 +1,7 @@ {-# LANGUAGE RebindableSyntax #-} import Language.Copilot --- 10 minutes +-- 10 min -- Shows delaying of streams. main :: IO () @@ -10,10 +10,10 @@ main = interpret 10 spec mySth :: Stream Bool mySth = not true || true --- ++ ('append') delays a stream by a list of values. --- ++ :: [a] -> Stream a -> Stream a +-- ++ ('append') delays a stream by a list of values. +-- (++) :: Typed a => [a] -> Stream a -> Stream a mySth2 :: Stream Bool -mySth2 = [False] ++ (not true || true) +mySth2 = [False] ++ (not myTrue || myTrue) -- Exercise -- Define a stream that has a constant value of 12, using the ++ operator. @@ -31,4 +31,4 @@ spec :: Spec spec = do observer "twelve" twelve -- 'observer' just prints the value at every step. - trigger "trigger1" tft [arg mySth, arg mySth2] + trigger "sample1" trueFalseTrue [arg mySth, arg mySth2] diff --git a/exercises/Ex01-07.hs b/exercises/Ex01-07.hs index de5e209..b8ea7f4 100644 --- a/exercises/Ex01-07.hs +++ b/exercises/Ex01-07.hs @@ -1,7 +1,7 @@ {-# LANGUAGE RebindableSyntax #-} import Language.Copilot --- 10 minutes +-- 10 min -- Show recursion of streams. main :: IO () @@ -15,17 +15,17 @@ myFalse = [False] ++ myFalse -- Define a stream that alternates between True and False, e.g.: -- alternating :: Stream Bool -alternating = false -- remove the placeholder! +alternating = [True] ++ not alternating -- remove the placeholder! -- Exercise -- Define a stream that counters from 0 and up, e.g.; -- <0, 1, 2, 3, 4, 5, ...> counter :: Stream Int64 -counter = 0 -- remove the placeholder! +counter = 0 spec :: Spec spec = do observer "alternating" alternating observer "counter" counter - trigger "trigger1" alternating [arg counter] + trigger "sample1" alternating [arg counter] diff --git a/exercises/Ex01-08.hs b/exercises/Ex01-08.hs index 5d58088..80fc6db 100644 --- a/exercises/Ex01-08.hs +++ b/exercises/Ex01-08.hs @@ -1,18 +1,41 @@ {-# LANGUAGE RebindableSyntax #-} import Language.Copilot --- 3 minutes --- Show reading streams from an external source. +-- 7 min +-- More advanced example with custom functions. main :: IO () main = interpret 10 spec -sensorData :: Stream Float -sensorData = extern "sensor" (Just [1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12]) +-- Just a definition without arguments. +thirteen :: Stream Int32 +thirteen = 13 + +-- We can make functions as well. Arguments to the function are defined on the +-- left hand side of the = sign. +increase :: Stream Int32 -> Stream Int32 +increase n = n + 1 + +-- Functions can have multiple arguments. +myPlus :: Stream Int32 -> Stream Int32 -> Stream Int32 +myPlus l r = l + r + + +-- Exercise +-- Define a function that calculates the square root of its input. +mySqrt :: Stream Int32 -> Stream Int32 +mySqrt n = 0 + + +-- Exercise +-- Define a function that calculates the average over two integer streams. +-- Hint: use the `div` function for division in the integer space. +avg2 :: Stream Int32 -> Stream Int32 -> Stream Int32 +avg2 n m = 0 --- A property that we use to fire the trigger. -myProp :: Stream Bool -myProp = sensorData > 2 spec :: Spec -spec = trigger "trigger1" myProp [arg sensorData] +spec = do + observer "mySqrt 8" (mySqrt 8) + + observer "avg 3 5" (avg2 3 5) diff --git a/exercises/Ex01-09.hs b/exercises/Ex01-09.hs index 0b8cf78..e5ec234 100644 --- a/exercises/Ex01-09.hs +++ b/exercises/Ex01-09.hs @@ -1,22 +1,25 @@ {-# LANGUAGE RebindableSyntax #-} import Language.Copilot -import Copilot.Compile.C99 - --- 8 minutes --- Show compilation to C code, the output and how everything comes together. main :: IO () -main = do - spec' <- reify spec - compile "ex01-09" spec' +main = interpret 10 spec + +myOne :: Stream Int32 +myOne = 1 + +myTwo :: Stream Int32 +myTwo = 1 + 1 --- Note how we don't specify data anymore here. -sensorData :: Stream Float -sensorData = extern "sensor" Nothing +myCmp :: Stream Bool +myCmp = myTwo > 2 -myProp :: Stream Bool -myProp = sensorData > 2 +-- Change types to Int -- wrong +-- Change type to Word32 +-- Apply other operations (tan) +-- Recursion +-- Create a counter +-- Use counter in comparison spec :: Spec spec = do - trigger "trigger1" myProp [arg sensorData] + trigger "sample1" myCmp [arg myOne] diff --git a/exercises/Ex01-10.hs b/exercises/Ex01-10.hs index 6fe4512..4cad004 100644 --- a/exercises/Ex01-10.hs +++ b/exercises/Ex01-10.hs @@ -1,41 +1,19 @@ {-# LANGUAGE RebindableSyntax #-} import Language.Copilot --- 7 minutes --- More advanced example with custom functions. - main :: IO () main = interpret 10 spec --- Just a definition without arguments. -thirteen :: Stream Int32 -thirteen = 13 - --- We can make functions as well. Arguments to the function are defined on the --- left hand side of the = sign. -increase :: Stream Int32 -> Stream Int32 -increase n = n + 1 - --- Functions can have multiple arguments. -myPlus :: Stream Int32 -> Stream Int32 -> Stream Int32 -myPlus l r = l + r - - --- Exercise --- Define a function that calculates the square of its input. -mySquare :: Stream Int32 -> Stream Int32 -mySquare n = 0 - - --- Exercise --- Define a function that calculates the average over two integer streams. --- Hint: use the `div` function for division in the integer space. -avg2 :: Stream Int32 -> Stream Int32 -> Stream Int32 -avg2 n m = 0 +sensorData :: Stream Float +sensorData = extern "sensor" (Just [1, 2, 3, 4, 5, 6, 7]) +myProp :: Stream Bool +myProp = sensorData > 2 spec :: Spec spec = do - observer "mySqrt 8" (mySqrt 8) + trigger "sample1" myProp [arg sensorData] - observer "avg 3 5" (avg2 3 5) +-- What if we interpret too many steps. +-- Add another sensor. +-- Altitude meter (aircraft stays within range). diff --git a/exercises/Ex01-11.hs b/exercises/Ex01-11.hs new file mode 100644 index 0000000..32538c2 --- /dev/null +++ b/exercises/Ex01-11.hs @@ -0,0 +1,30 @@ +{-# LANGUAGE RebindableSyntax #-} +import Language.Copilot +import Copilot.Compile.C99 + +main :: IO () +main = do + spec' <- reify spec + compile "sample1" spec' + +sensorData :: Stream Float +sensorData = extern "sensor" (Just [1, 2, 3, 4, 5, 6, 7]) + +myProp :: Stream Bool +myProp = sensorData > 2 + +spec :: Spec +spec = do + trigger "sample1" myProp [arg sensorData] + +-- Compile this and explore header, implementation, and produce main that uses +-- this code, and run it. + +-- Average two sensors +-- Low-pass filter. +-- \x -> if x < threshold then threshold else x +-- Derivative. +-- Two-term average filter? +-- Average current value with last value. +-- (s + prevS) / 2 +-- Fibonacci diff --git a/exercises/Ex02-01.hs b/exercises/Ex02-01.hs index 54e4fa9..f66e0b5 100644 --- a/exercises/Ex02-01.hs +++ b/exercises/Ex02-01.hs @@ -16,21 +16,7 @@ spec = do trigger "sample1" myProp [arg sensorData] sensorData :: Stream Float -sensorData = extern "sensor" (Just [5, 25, 10, 5, 15, 6, 12, 12, 12, 6, 6, 6, 13, 14, 15]) - -threshold :: Stream Float -threshold = constant 10 +sensorData = extern "sensor" (Just [1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15]) myProp :: Stream Bool -myProp = _ -- ? - - - - - - - - - - --- myProp = sensorData < threshold +myProp = s < threshold diff --git a/exercises/Ex02-02.hs b/exercises/Ex02-02.hs index 334d34d..7ec7984 100644 --- a/exercises/Ex02-02.hs +++ b/exercises/Ex02-02.hs @@ -16,13 +16,7 @@ spec = do trigger "sample1" myProp [arg sensorData] sensorData :: Stream Float -sensorData = extern "sensor" (Just [5, 25, 10, 5, 15, 6, 12, 12, 12, 6, 6, 6, 13, 14, 15]) +sensorData = extern "sensor" (Just [1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15]) myProp :: Stream Bool -myProp = _ - -underThreshold :: Stream Bool -underThreshold = sensorData < threshold - -threshold :: Stream Float -threshold = constant 10 +myProp = _ -- s < threshold diff --git a/exercises/Ex02-03.hs b/exercises/Ex02-03.hs index 4dd4404..fda3af0 100644 --- a/exercises/Ex02-03.hs +++ b/exercises/Ex02-03.hs @@ -21,16 +21,7 @@ spec = do trigger "sample1" myProp [arg sensorData] sensorData :: Stream Float -sensorData = extern "sensor" (Just [5, 25, 10, 5, 15, 6, 12, 12, 12, 6, 6, 6, 13, 14, 15]) +sensorData = extern "sensor" (Just [1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15]) myProp :: Stream Bool -myProp = _ - -underThreshold :: Stream Bool -underThreshold = sensorData < threshold - -underThresholdBefore :: Stream Bool -underThresholdBefore = [False] ++ underThreshold - -threshold :: Stream Float -threshold = constant 10 +myProp = [False] ++ (s < threshold) -- ??? diff --git a/exercises/Ex02-04.hs b/exercises/Ex02-04.hs index d592649..97a13a3 100644 --- a/exercises/Ex02-04.hs +++ b/exercises/Ex02-04.hs @@ -1,5 +1,5 @@ {-# LANGUAGE RebindableSyntax #-} -import Language.Copilot hiding (previous) +import Language.Copilot -- Part 2, exercise 4 (10 minutes). -- @@ -17,20 +17,13 @@ spec = do trigger "sample1" myProp [arg sensorData] sensorData :: Stream Float -sensorData = extern "sensor" (Just [5, 25, 10, 5, 15, 6, 12, 12, 12, 6, 6, 6, 13, 14, 15]) +sensorData = extern "sensor" (Just [1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15]) myProp :: Stream Bool myProp = underThreshold && underThresholdBefore -underThreshold :: Stream Bool -underThreshold = sensorData < threshold - -threshold :: Stream Float -threshold = constant 10 - underThresholdBefore :: Stream Bool -underThresholdBefore = [False] ++ underThreshold -- Use previous here +underThresholdBefore = [False] ++ underThreshold --- Define previous -previous :: Stream Bool -> Stream Bool -previous = _ +underThreshold :: Stream Bool +underThreshold = (s < threshold) diff --git a/exercises/Ex02-05.hs b/exercises/Ex02-05.hs index 3b451b8..951129c 100644 --- a/exercises/Ex02-05.hs +++ b/exercises/Ex02-05.hs @@ -1,5 +1,5 @@ -import Language.Copilot hiding (alwaysBeen, previous) -import Prelude hiding (not, (&&), (++), (<)) +{-# LANGUAGE RebindableSyntax #-} +import Language.Copilot -- Part 2, exercise 5 (15 minutes). -- @@ -12,31 +12,28 @@ import Prelude hiding (not, (&&), (++), (<)) main :: IO () main = do - interpret 15 spec + interpret 10 spec spec :: Spec spec = do - trigger "sample1" myProp [ arg sensorData ] + trigger "sample1" myProp [arg sensorData] sensorData :: Stream Float -sensorData = extern "sensor" (Just [5, 25, 10, 5, 15, 6, 12, 12, 12, 6, 6, 6, 13, 14, 15]) +sensorData = extern "sensor" (Just [1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15]) myProp :: Stream Bool myProp = underThreshold && previous underThreshold underThreshold :: Stream Bool -underThreshold = sensorData < threshold - -threshold :: Stream Float -threshold = constant 10 +underThreshold = s < threshold previous :: Stream Bool -> Stream Bool previous s = [False] ++ s -- Try to generalize previous using the following signature: --- alwaysBeen :: Int -> Stream Bool -> Stream Bool --- alwaysBeen = _ +alwaysBeen :: Int -> Stream Bool -> Stream Bool +alwaysBeen = _ -- See below for clues. @@ -76,10 +73,11 @@ previous s = [False] ++ s -- Posible solutions -alwaysBeen :: Int -> Stream Bool -> Stream Bool -alwaysBeen 0 s = s -alwaysBeen n s = s && (alwaysBeen (n - 1) ([True] ++ s)) - +-- +-- alwaysBeen :: Word64 -> Stream Bool -> Stream Bool +-- alwaysBeen 0 s = true +-- alwaysBeen n s = s && (alwaysBeen (n - 1) [True] ++ s) +-- -- alwaysBeen :: Stream Word64 -> Stream Bool -> Stream Bool -- alwaysBeen n s = -- if n == 0 @@ -87,10 +85,3 @@ alwaysBeen n s = s && (alwaysBeen (n - 1) ([True] ++ s)) -- else (s && (alwaysBeen (n - 1) [True] ++ s)) -- Re-write (4) using alwaysBeen. - --- observer "sensorData" sensorData --- observer "underThreshold" underThreshold --- observer "(myAlwaysBeen 0 underThreshold)" (myAlwaysBeen 0 underThreshold) --- observer "(myAlwaysBeen 1 underThreshold)" (myAlwaysBeen 1 underThreshold) --- observer "(myAlwaysBeen 2 underThreshold)" (myAlwaysBeen 2 underThreshold) --- observer "(myAlwaysBeen 3 underThreshold)" (myAlwaysBeen 3 underThreshold) diff --git a/exercises/Ex02-06.hs b/exercises/Ex02-06.hs index 39ea567..f542292 100644 --- a/exercises/Ex02-06.hs +++ b/exercises/Ex02-06.hs @@ -13,14 +13,14 @@ import Language.Copilot main :: IO () main = do - interpret 15 spec + interpret 10 spec spec :: Spec spec = do trigger "sample1" myProp [arg sensorData] sensorData :: Stream Float -sensorData = extern "sensor" (Just [5, 25, 10, 5, 15, 6, 12, 12, 12, 6, 6, 6, 13, 14, 15]) +sensorData = extern "sensor" (Just [1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15]) myProp :: Stream Bool myProp = alwaysBeen 1 underThreshold -- Check for 1 sample ago and now @@ -32,5 +32,5 @@ previous :: Stream Bool -> Stream Bool previous s = [False] ++ s alwaysBeen :: Int -> Stream Bool -> Stream Bool -alwaysBeen 0 s = s +alwaysBeen 0 s = true alwaysBeen n s = s && (alwaysBeen (n - 1) (previous s)) diff --git a/exercises/Ex0207.hs b/exercises/Ex0207.hs deleted file mode 100644 index f7e2a68..0000000 --- a/exercises/Ex0207.hs +++ /dev/null @@ -1,28 +0,0 @@ -{-# LANGUAGE RebindableSyntax #-} -import Language.Copilot - -import Ex0207MyLib - --- Part 2, exercise 7 (5 minutes). --- --- Move reusable definitions to a separate module. --- Import module. --- Check copilot-libraries on hackage --- Point people to PTLTL and MTL modules. - -main :: IO () -main = do - interpret 15 spec - -spec :: Spec -spec = do - trigger "sample1" myProp [arg sensorData] - -sensorData :: Stream Float -sensorData = extern "sensor" (Just [5, 25, 10, 5, 15, 6, 12, 12, 12, 6, 6, 6, 13, 14, 15]) - -myProp :: Stream Bool -myProp = alwaysBeen 1 underThreshold -- Check for 1 sample ago and now - -underThreshold :: Stream Bool -underThreshold = s < threshold diff --git a/exercises/Ex0207MyLib.hs b/exercises/Ex0207MyLib.hs deleted file mode 100644 index ad9e9d6..0000000 --- a/exercises/Ex0207MyLib.hs +++ /dev/null @@ -1,21 +0,0 @@ -{-# LANGUAGE RebindableSyntax #-} -module Ex0207MyLib where - -import Language.Copilot - --- Part 2, exercise 6 (2 minutes). --- --- The specification using previous works for one sample, but we may want to --- check multiple samples. --- --- We have generalized checking a property for the recent past. We call that --- new *temporal* operator alwaysBeen. --- --- Re-write (5) for 10 seconds instead of 1 or 2. - -previous :: Stream Bool -> Stream Bool -previous s = [False] ++ s - -alwaysBeen :: Int -> Stream Bool -> Stream Bool -alwaysBeen 0 s = s -alwaysBeen n s = s && (alwaysBeen (n - 1) (previous s)) diff --git a/exercises/Ex03.hs b/exercises/Ex03.hs deleted file mode 100644 index 91af2d0..0000000 --- a/exercises/Ex03.hs +++ /dev/null @@ -1,110 +0,0 @@ --- | An example showing the usage of the What4 backend in copilot-theorem for --- propositional logic on boolean streams. - -module Main where - -import Control.Monad (forM_) -import qualified Prelude as P - -import Copilot.Theorem.What4 -import Language.Copilot - -spec :: Spec -spec = do - -- The constant value true, which is translated as the corresponding SMT - -- boolean literal. - prop "Example 1" (forAll true) - - -- The constant value false, which is translated as the corresponding SMT - -- boolean literal. - prop "Example 2" (forAll false) - - -- An inductively defined flavor of true, which requires induction to prove. - let a = [True] ++ a - prop "Example 3" (forAll a) - - -- An inductively defined "a or not a" proposition. - let a = [False] ++ b - b = [True] ++ a - prop "Example 4" (forAll (a || b)) - - -- A version of "a or not a" proposition which does not require any sort of - -- inductive argument. - let a = [False] ++ b - b = not a - prop "Example 5" (forAll (a || b)) - - -- A bit more convoluted version of Example 5, which is provable. - let a = [True, False] ++ b - b = [False] ++ not (drop 1 a) - prop "Example 6" (forAll (a || b)) - - -- Exercises: - -- How would you check if the monitor is vacuously true (always fires). - -- How would you check if the monitor is vacuously false (never fires). - -- How would you check if, given two monitors are exclusive (they can't - -- both fire at the same time)? - -- How would you check if, given two properties, one of them will always - -- fire. - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -- An example using external streams. - let b :: Stream Int32 - b = extern "b" Nothing - prop "Example 7" (forAll (b > 10 || b < 10)) - - -- An example using external streams. - -- - -- This points to the system under study being potentially unrealizable. If - -- one of the monitored properties will always fire at some point, that means - -- that the system will be permanently correcting an unwanted situation and - -- is never in nominal state. - let b :: Stream Int32 - b = extern "b" Nothing - p1 = b > 100 -- the temperature is too high - p2 = b <= 100 -- the temperature is too low - prop "Example 8" (forAll (p1 || p2)) - - return () - -main :: IO () -main = do - spec' <- reify spec - - -- Use Z3 to prove the properties. - results <- prove Z3 spec' - - -- Print the results. - forM_ results $ \(propName, propRes) -> do - putStr $ propName <> ": " - case propRes of - Valid -> putStrLn "valid" - Invalid -> putStrLn "invalid" - Unknown -> putStrLn "unknown" diff --git a/exercises/main01-09.c b/exercises/Main01-11.c similarity index 59% rename from exercises/main01-09.c rename to exercises/Main01-11.c index 7499164..a06b74e 100644 --- a/exercises/main01-09.c +++ b/exercises/Main01-11.c @@ -1,18 +1,20 @@ #include +#include +#include +#include #include -#include "ex01-09.h" +#include "sample1.h" float sensor = 1; -/* This function is called as the trigger. */ -void trigger1 (float arg) { +void sample1 (float arg) { printf("Monitor going off with data: %f\n", arg); } int main (int argc, char **argv) { - int i; - for (i = 0; i < 20; i++) { + int i = 0; + for (;i < 20; i++) { sensor *= 2; step(); sleep(1); diff --git a/exercises/Test.hs b/exercises/test/Main.hs similarity index 100% rename from exercises/Test.hs rename to exercises/test/Main.hs diff --git a/exercises/test/run.sh b/exercises/test/run.sh new file mode 100755 index 0000000..c021fcb --- /dev/null +++ b/exercises/test/run.sh @@ -0,0 +1,9 @@ +#!/bin/sh + +# Simple script for executing the exercise. + +set -e + +dir=`dirname $0` + +runhaskell ${dir}/Main.hs diff --git a/tutorial-fm-2024.txt b/tutorial-fm-2024.txt new file mode 100644 index 0000000..d20ae1b --- /dev/null +++ b/tutorial-fm-2024.txt @@ -0,0 +1,107 @@ +- 3h, split in two 1.5h blocks. + +- Topics / script + + Crowd: Model checking / Theorem proving / FM + folks, a bit of FP knowledge but not much. + They want to know the connection to other + formal methods. + - They don't work on mission or specific applications. + - No direct access to users (on the most part). + + Possible outcomes: + - Small experiments in their labs with their students. + - Example that gets everything running quickly and is + intuitive. + - Contributions to Copilot (62 minutes). + - Explore logics. + - Write their own combinator or library. + - Connections to other FM techniques and tools? + - Copilot-theorem (about 13 minutes) + - Examples that cover theorem. + - Copilot-verifier (about 5 minutes) + - Example with the verifier. + - Collaborations (about 10 minutes). + - Past things we explored, and mistakes we made. + - Open problems: + - Rust and other backends. + - Connections to FM tools. + spec = do + trigger "f1" (x < 10) [] + trigger "f2" (x >= 10) [] + - New logics. + - Efficiency and performance (including FPGA). + - We want users from outside. + - Experiments (ROS, cFS, F'); Ogma. + - Clocks. + - Types. + - User interface and simulation. + +1) Session 1 + First 45' + - Intro + - Basis and purpose of RV + - What Copilot is, and where Copilot is at + +import Language.Copilot + +main :: IO () +main = do + interpret 10 spec + +spec :: Spec +spec = + trigger "sample1" true [] + +Run it and see the results. + + + + - Example that gets everything running quickly and is + intuitive. + - High level view of what we want to do + - Write spec top-down. + - Use interpret + - Monitor + true + false + add arguments + - Streams of data + +myTrue :: Stream Bool +myTrue = true + +myFalse :: Stream Bool +myFalse = true ==> false + +myFalse :: Stream Int32 +myFalse = 3 > 2 + +myFalse :: Stream Int32 +myFalse = [True] ++ (3 > 2) + +alternate :: Stream Int32 +alternate = [True] ++ not alternate + +monitor :: Spec +monitor = do + trigger "recover" myFalse [ ] + trigger "recover" myFalse [ arg myFalse ] + + - Introduce externs + - End with example of altitude meter. + + Second 45' + - Compile to C. + - Provide sensor data from C. + - Handle error from C. + + Complement to existing FM, or gateway to FMs. + We provide libraries. + +- Setup / IT + - Docker? +- Who presents what. + +- https://github.com/fdedden/bobkonf-2024-copilot-tutorial +- https://github.com/fdedden/bobkonf-2024-copilot-tutorial-slides