From 869fdd97a8bfc91d08f3b718daa80daf189a61d4 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Mon, 9 Sep 2024 10:16:49 +0000 Subject: [PATCH 1/3] Minor fixes; final review. --- exercises/Ex02-05.hs | 2 +- exercises/Ex02-06.hs | 6 +++--- exercises/Ex0207MyLib.hs | 16 +++------------- 3 files changed, 7 insertions(+), 17 deletions(-) diff --git a/exercises/Ex02-05.hs b/exercises/Ex02-05.hs index 3b451b8..fab1ba5 100644 --- a/exercises/Ex02-05.hs +++ b/exercises/Ex02-05.hs @@ -83,7 +83,7 @@ alwaysBeen n s = s && (alwaysBeen (n - 1) ([True] ++ s)) -- alwaysBeen :: Stream Word64 -> Stream Bool -> Stream Bool -- alwaysBeen n s = -- if n == 0 --- then true +-- then s -- else (s && (alwaysBeen (n - 1) [True] ++ s)) -- Re-write (4) using alwaysBeen. diff --git a/exercises/Ex02-06.hs b/exercises/Ex02-06.hs index 39ea567..6e52072 100644 --- a/exercises/Ex02-06.hs +++ b/exercises/Ex02-06.hs @@ -28,9 +28,9 @@ myProp = alwaysBeen 1 underThreshold -- Check for 1 sample ago and now underThreshold :: Stream Bool underThreshold = s < threshold -previous :: Stream Bool -> Stream Bool -previous s = [False] ++ s +previousT :: Stream Bool -> Stream Bool +previousT s = [True] ++ s alwaysBeen :: Int -> Stream Bool -> Stream Bool alwaysBeen 0 s = s -alwaysBeen n s = s && (alwaysBeen (n - 1) (previous s)) +alwaysBeen n s = s && (alwaysBeen (n - 1) (previousT s)) diff --git a/exercises/Ex0207MyLib.hs b/exercises/Ex0207MyLib.hs index ad9e9d6..a369aed 100644 --- a/exercises/Ex0207MyLib.hs +++ b/exercises/Ex0207MyLib.hs @@ -3,19 +3,9 @@ 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 +previousT :: Stream Bool -> Stream Bool +previousT s = [True] ++ s alwaysBeen :: Int -> Stream Bool -> Stream Bool alwaysBeen 0 s = s -alwaysBeen n s = s && (alwaysBeen (n - 1) (previous s)) +alwaysBeen n s = s && (alwaysBeen (n - 1) (previousT s)) From 3420c207fb6ceb1dec69250380920874139aa957 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Mon, 9 Sep 2024 10:17:08 +0000 Subject: [PATCH 2/3] Minor fixes; final review. --- exercises/Ex03.hs | 31 +++++++++++++++++++------------ 1 file changed, 19 insertions(+), 12 deletions(-) diff --git a/exercises/Ex03.hs b/exercises/Ex03.hs index 91af2d0..1fd4afa 100644 --- a/exercises/Ex03.hs +++ b/exercises/Ex03.hs @@ -24,8 +24,8 @@ spec = do prop "Example 3" (forAll a) -- An inductively defined "a or not a" proposition. - let a = [False] ++ b - b = [True] ++ a + let a = [False] ++ b -- False, True, False, True,... + b = [True] ++ a -- True, False, True, False,... prop "Example 4" (forAll (a || b)) -- A version of "a or not a" proposition which does not require any sort of @@ -40,10 +40,15 @@ spec = do 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 the monitor is always true (always fires). + -- That monitor would then be useless!! + -- + -- How would you check if the monitor is always false (never fires). + -- That monitor would then be useless!! + -- + -- How would you check if, given two monitors, they 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. @@ -101,10 +106,12 @@ main = do -- Use Z3 to prove the properties. results <- prove Z3 spec' + let printResult (propName, propRes) = do + putStr $ propName <> ": " + case propRes of + Valid -> putStrLn "valid" + Invalid -> putStrLn "invalid" + Unknown -> putStrLn "unknown" + -- Print the results. - forM_ results $ \(propName, propRes) -> do - putStr $ propName <> ": " - case propRes of - Valid -> putStrLn "valid" - Invalid -> putStrLn "invalid" - Unknown -> putStrLn "unknown" + forM_ results printResult From 9069e34a5760e1fe0fe31a642f44dc6f12ce4002 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Sun, 24 Nov 2024 20:22:13 +0000 Subject: [PATCH 3/3] Unclear what these changes were about. It's been too long. --- Links.md | 65 +++++++++++++++++++++++++++++++++ Makefile | 2 +- exercises/Ex02-02.hs | 2 +- exercises/Ex02-03.hs | 2 +- exercises/Ex02-04.hs | 4 +-- exercises/Ex02-05.hs | 27 +++++++------- exercises/Ex03.hs | 86 ++++++++++++++++++++++---------------------- 7 files changed, 128 insertions(+), 60 deletions(-) create mode 100644 Links.md diff --git a/Links.md b/Links.md new file mode 100644 index 0000000..31ac67f --- /dev/null +++ b/Links.md @@ -0,0 +1,65 @@ +# Connections to other tools and real systems. + +- (ROS, cFS, F'); Ogma + +https://github.com/nasa/ogma + +# Open problems + +## Arduino + +- https://hackage.haskell.org/package/arduino-copilot + +## Rust and other backends. + +- https://github.com/Copilot-Language/copilot-rust +- https://github.com/Copilot-Language/copilot-rust/discussions + +## New logics + +CTL, LTL, multi-valued LTL, others + +## Efficiency and performance (including FPGA) + +We have an FPGA backend. The backend relies on the bluespec language, which is +used in industrial development of FPGAs. + +Do we have a measure that the result is minimal? + +## Clocks + +- Currently, all streams advance in lockstep. What if you want to advance them + at different rates? + +## Types + +https://github.com/Copilot-Language/copilot/blob/master/copilot/examples/Array.hs +https://github.com/Copilot-Language/copilot/blob/master/copilot/examples/Structs.hs#L14-L18 +https://github.com/Copilot-Language/copilot/blob/master/copilot/examples/Structs.hs#L58-L60 + +How to use other types. + +## User interface and simulation + +https://www.tessla.io/ + +## Monitoring of distributed system or multi-level RV + +- How to install properties and how to instrument a distributed system. + +## We want users from outside + +- If you use it, and it helps you, let us know. +agoodloe@nasa.gov; ivan.perezdominguez@nasa.gov + +- If you create work based on it, also let us know. +agoodloe@nasa.gov; ivan.perezdominguez@nasa.gov + +- If you want to collaborate, please reach out: +agoodloe@nasa.gov; ivan.perezdominguez@nasa.gov + +- If you use it and something fails, create a ticket: +https://github.com/Copilot-Language/copilot + +- Whatever you choose, get involved: +https://github.com/Copilot-Language/copilot/discussions diff --git a/Makefile b/Makefile index d366bab..9efc0f5 100644 --- a/Makefile +++ b/Makefile @@ -3,7 +3,7 @@ IMAGE=formal-methods-2024-copilot-tutorial all: test build: - docker build --progress plain -t $(IMAGE) . + docker build -t $(IMAGE) . test: build bin/rundocker runhaskell exercises/Test.hs diff --git a/exercises/Ex02-02.hs b/exercises/Ex02-02.hs index 334d34d..2bcc317 100644 --- a/exercises/Ex02-02.hs +++ b/exercises/Ex02-02.hs @@ -19,7 +19,7 @@ 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 = _ +myProp = [False] ++ underThreshold underThreshold :: Stream Bool underThreshold = sensorData < threshold diff --git a/exercises/Ex02-03.hs b/exercises/Ex02-03.hs index 4dd4404..8fb0c37 100644 --- a/exercises/Ex02-03.hs +++ b/exercises/Ex02-03.hs @@ -24,7 +24,7 @@ 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 = _ +myProp = underThreshold && underThresholdBefore underThreshold :: Stream Bool underThreshold = sensorData < threshold diff --git a/exercises/Ex02-04.hs b/exercises/Ex02-04.hs index d592649..8d1d982 100644 --- a/exercises/Ex02-04.hs +++ b/exercises/Ex02-04.hs @@ -32,5 +32,5 @@ underThresholdBefore :: Stream Bool underThresholdBefore = [False] ++ underThreshold -- Use previous here -- Define previous -previous :: Stream Bool -> Stream Bool -previous = _ +previous :: Bool -> Stream Bool -> Stream Bool +previous def s = [def] ++ s diff --git a/exercises/Ex02-05.hs b/exercises/Ex02-05.hs index fab1ba5..a6aea8e 100644 --- a/exercises/Ex02-05.hs +++ b/exercises/Ex02-05.hs @@ -1,5 +1,6 @@ +{-# LANGUAGE RebindableSyntax #-} import Language.Copilot hiding (alwaysBeen, previous) -import Prelude hiding (not, (&&), (++), (<)) +import Prelude hiding (not, (&&), (++), (<), (==)) -- Part 2, exercise 5 (15 minutes). -- @@ -17,6 +18,10 @@ main = do spec :: Spec spec = do trigger "sample1" myProp [ arg sensorData ] + observer "(alwaysBeen s1 s2)" (alwaysBeen s1 s2) + +s1 = constW64 1 +s2 = true sensorData :: Stream Float sensorData = extern "sensor" (Just [5, 25, 10, 5, 15, 6, 12, 12, 12, 6, 6, 6, 13, 14, 15]) @@ -50,8 +55,6 @@ previous s = [False] ++ s - - -- Expand one step -- alwaysBeen :: Int -> Stream Bool -> Stream Bool @@ -76,15 +79,15 @@ 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 :: Stream Word64 -> Stream Bool -> Stream Bool --- alwaysBeen n s = --- if n == 0 --- then s --- else (s && (alwaysBeen (n - 1) [True] ++ s)) +-- alwaysBeen :: Int -> Stream Bool -> Stream Bool +-- alwaysBeen 0 s = s +-- alwaysBeen n s = s && (alwaysBeen (n - 1) ([True] ++ s)) + +alwaysBeen :: Stream Word64 -> Stream Bool -> Stream Bool +alwaysBeen n s = + if n == 0 + then s + else (s && (alwaysBeen (n - 1) ([True] ++ s))) -- Re-write (4) using alwaysBeen. diff --git a/exercises/Ex03.hs b/exercises/Ex03.hs index 1fd4afa..a7b0127 100644 --- a/exercises/Ex03.hs +++ b/exercises/Ex03.hs @@ -13,45 +13,44 @@ spec :: Spec spec = do -- The constant value true, which is translated as the corresponding SMT -- boolean literal. - prop "Example 1" (forAll true) + -- prop "Example 1" (forAll true) - -- The constant value false, which is translated as the corresponding SMT - -- boolean literal. - prop "Example 2" (forAll false) + -- -- 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) + -- let a = [True] ++ a + -- prop "Example 3" (forAll a) -- An inductively defined "a or not a" proposition. - let a = [False] ++ b -- False, True, False, True,... - b = [True] ++ a -- True, False, True, False,... - 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)) + --let a = [False] ++ b -- False, True, False, True,... + -- b = [True] ++ a -- True, False, True, False,... + --prop "Example 4" (forAll (a `xor` 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)) + -- -- 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)) - -- Exercises: - -- - -- How would you check if the monitor is always true (always fires). - -- That monitor would then be useless!! - -- - -- How would you check if the monitor is always false (never fires). - -- That monitor would then be useless!! - -- - -- How would you check if, given two monitors, they 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. + -- -- 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 always true (always fires). + -- -- That monitor would then be useless!! + -- -- + -- -- How would you check if the monitor is always false (never fires). + -- -- That monitor would then be useless!! + -- -- + -- -- How would you check if, given two monitors, they 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. @@ -80,22 +79,23 @@ spec = do - -- 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)) + 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 ()