diff --git a/CHANGELOG b/CHANGELOG --- a/CHANGELOG +++ b/CHANGELOG @@ -1,3 +1,15 @@ +2021-03-07 + * Version bump (3.2.1). (#85) + * Renamed Examples directory to examples. (#44) + * Remove version bounds for copilot package in examples. (#86) + * Remove unnecessary duplicates from field in cabal file. (#87) + * Added how to run examples to README. (#48) + * Added flag to prevent examples from being built by default. (#48) + * Fix typo in README. (#49) + * Completed the documentation. (#67) + * Merged and updated examples from + benjaminselfridge:feature/what4-updates. (#63) + 2020-12-06 * Update optparse-applicative dependency version for newer base versions. (#61). diff --git a/Examples/AddMult.hs b/Examples/AddMult.hs deleted file mode 100644 --- a/Examples/AddMult.hs +++ /dev/null @@ -1,20 +0,0 @@ --------------------------------------------------------------------------------- --- Copyright © 2019 National Institute of Aerospace / Galois, Inc. --------------------------------------------------------------------------------- - --- | Another small example that calculates a constant value using a recursive --- function. - -module Main where - -import Language.Copilot - -spec :: Spec -spec = trigger "f" true [ arg $ mult 5 ] - where - mult :: Word64 -> Stream Word64 - mult 0 = 1 - mult i = constant i * mult (i-1) - -main :: IO () -main = interpret 100 spec diff --git a/Examples/Array.hs b/Examples/Array.hs deleted file mode 100644 --- a/Examples/Array.hs +++ /dev/null @@ -1,35 +0,0 @@ --------------------------------------------------------------------------------- --- Copyright © 2019 National Institute of Aerospace / Galois, Inc. --------------------------------------------------------------------------------- - --- | This is a simple example for arrays. As a program, it does not make much --- sense, however it shows of the features of arrays nicely. - --- | Enable compiler extension for type-level data, necesary for the array --- length. - -{-# LANGUAGE RebindableSyntax #-} -{-# LANGUAGE DataKinds #-} - -module Main where - -import Language.Copilot - --- Lets define an array of length 2. --- Make the buffer of the streams 3 elements long. -arr :: Stream (Array 2 Bool) -arr = [ array [True, False] - , array [True, True] - , array [False, False]] ++ arr - -spec :: Spec -spec = do - -- A trigger that fires 'func' when the first element of 'arr' is True. - -- It passes the current value of arr as an argument. - -- The prototype of 'func' would be: - -- void func (int8_t arg[3]); - trigger "func" (arr .!! 0) [arg arr] - --- Compile the spec -main :: IO () -main = interpret 30 spec diff --git a/Examples/Cast.hs b/Examples/Cast.hs deleted file mode 100644 --- a/Examples/Cast.hs +++ /dev/null @@ -1,29 +0,0 @@ --------------------------------------------------------------------------------- --- Copyright © 2019 National Institute of Aerospace / Galois, Inc. --------------------------------------------------------------------------------- - --- | Examples of casting types. - -{-# LANGUAGE RebindableSyntax #-} - -module Main where - -import Language.Copilot - -b :: Stream Bool -b = [True] ++ not b - -i :: Stream Int8 -i = cast b - -x :: Stream Word16 -x = [0] ++ x + 1 - -y :: Stream Int32 -y = 1 + cast x - -spec :: Spec -spec = trigger "trigger" true [arg y, arg i] - -main :: IO () -main = interpret 30 spec diff --git a/Examples/Clock.hs b/Examples/Clock.hs deleted file mode 100644 --- a/Examples/Clock.hs +++ /dev/null @@ -1,30 +0,0 @@ --------------------------------------------------------------------------------- --- Copyright © 2019 National Institute of Aerospace / Galois, Inc. --------------------------------------------------------------------------------- - --- | Example showing usage of clocks to generate periodically recurring truth --- values. - -module Main where - -import Language.Copilot -import Copilot.Library.Clocks - --- | We need to force a type for the argument of `period`. -p :: Word8 -p = 5 - --- | Both have the same period, but a different phase. -clkStream :: Stream Bool -clkStream = clk (period p) (phase 0) - -clkStream' :: Stream Bool -clkStream' = clk (period p) (phase 2) - -spec :: Spec -spec = do - observer "clk" clkStream - observer "clk'" clkStream' - -main :: IO () -main = interpret 30 spec diff --git a/Examples/Counter.hs b/Examples/Counter.hs deleted file mode 100644 --- a/Examples/Counter.hs +++ /dev/null @@ -1,31 +0,0 @@ --------------------------------------------------------------------------------- --- Copyright © 2019 National Institute of Aerospace / Galois, Inc. --------------------------------------------------------------------------------- - --- | Example showing an implementation of a resettable counter. - -{-# LANGUAGE RebindableSyntax #-} - -module Main where - -import Language.Copilot - --- A resettable counter -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 - --- Counter that resets when it reaches 256 -bytecounter :: Stream Int32 -bytecounter = counter true reset where - reset = counter true false == 256 - -spec :: Spec -spec = trigger "counter" true [arg $ bytecounter] - -main :: IO () -main = interpret 270 spec diff --git a/Examples/Engine.hs b/Examples/Engine.hs deleted file mode 100644 --- a/Examples/Engine.hs +++ /dev/null @@ -1,38 +0,0 @@ --------------------------------------------------------------------------------- --- Copyright © 2011 National Institute of Aerospace / Galois, Inc. --------------------------------------------------------------------------------- - --- | Example implementing an engine cooling control system. - -{-# LANGUAGE RebindableSyntax #-} - -module Main where - -import Language.Copilot -import qualified Prelude as P - -{- If the majority of the engine temperature probes exeeds 250 degrees, then - - the cooler is engaged and remains engaged until the majority of the engine - - temperature probes drop to 250 or below. Otherwise, trigger an immediate - - shutdown of the engine. --} - -engineMonitor :: Spec -engineMonitor = do - trigger "shutoff" (not ok) [arg maj] - - where - vals = [ externW8 "tmp_probe_0" two51 - , externW8 "tmp_probe_1" two51 - , externW8 "tmp_probe_2" zero] - exceed = map (> 250) vals - maj = majority exceed - checkMaj = aMajority exceed maj - ok = alwaysBeen ((maj && checkMaj) ==> extern "cooler" cooler) - - two51 = Just $ [251, 251] P.++ repeat (250 :: Word8) - zero = Just $ repeat (0 :: Word8) - cooler = Just $ [True, True] P.++ repeat False - -main :: IO () -main = interpret 10 engineMonitor diff --git a/Examples/Heater.hs b/Examples/Heater.hs deleted file mode 100644 --- a/Examples/Heater.hs +++ /dev/null @@ -1,34 +0,0 @@ --------------------------------------------------------------------------------- --- 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 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 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" diff --git a/Examples/Voting.hs b/Examples/Voting.hs deleted file mode 100644 --- a/Examples/Voting.hs +++ /dev/null @@ -1,57 +0,0 @@ --------------------------------------------------------------------------------- --- Copyright © 2019 National Institute of Aerospace / Galois, Inc. --------------------------------------------------------------------------------- - --- | Fault-tolerant voting examples. - -{-# LANGUAGE RebindableSyntax #-} - -module Main where - -import Language.Copilot - -vote :: Spec -vote = do - -- majority selects element with the biggest occurance. - trigger "maj" true [arg maj] - - -- aMajority checks if the selected element has a majority. - trigger "aMaj" true [arg $ aMajority inputs maj] - - where - maj = majority inputs - - -- 26 input streams to vote on - inputs :: [Stream Word32] - inputs = [ a, b, c, d, e, f, g, h, i, j, k, l, m - , n, o, p, q, r, s, t, u, v, w, x, y, z - ] - a = [0] ++ a + 1 - b = [0] ++ b + 1 - c = [0] ++ c + 1 - d = [0] ++ d + 1 - e = [1] ++ e + 1 - f = [1] ++ f + 1 - g = [1] ++ g + 1 - h = [1] ++ h + 1 - i = [1] ++ i + 1 - j = [1] ++ j + 1 - k = [1] ++ k + 1 - l = [1] ++ l + 1 - m = [1] ++ m + 1 - n = [1] ++ n + 1 - o = [1] ++ o + 1 - p = [1] ++ p + 1 - q = [1] ++ q + 1 - r = [1] ++ r + 1 - s = [1] ++ s + 1 - t = [1] ++ t + 1 - u = [1] ++ u + 1 - v = [1] ++ v + 1 - w = [1] ++ w + 1 - x = [1] ++ x + 1 - y = [1] ++ y + 1 - z = [1] ++ z + 1 - -main :: IO () -main = interpret 30 vote diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -8,7 +8,7 @@ approach. Programs can be interpreted for testing, or translated into C99 code to be -incorporated in a project, or as a standalone application. The C99 backend +incorporated in a project or as a standalone application. The C99 backend output is constant in memory and time, making it suitable for systems with hard realtime requirements. @@ -74,8 +74,8 @@ ## Example Here follows a simple example of a heating system. Other examples can be found -in the [Examples -directory](https://github.com/Copilot-Language/Copilot/tree/master/Examples) +in the [examples +directory](https://github.com/Copilot-Language/Copilot/tree/master/examples) of the main repository. ```haskell @@ -109,6 +109,17 @@ -- Compile the spec main = reify spec >>= compile "heater" +``` + +The examples located in the `examples/` directory can be run from the root of +the project. Each example has a name. As a rule of thumb, the examples are +named after the filename (without extension) in lowercase letters, and +directory seperators replaced with a '-'. For example: + +```sh +cabal run addmult -f examples +cabal run counter -f examples +cabal run what4-arithmetic -f examples ``` ## Contributions diff --git a/copilot.cabal b/copilot.cabal --- a/copilot.cabal +++ b/copilot.cabal @@ -1,5 +1,5 @@ name: copilot -version: 3.2 +version: 3.2.1 cabal-version: >= 1.10 license: BSD3 license-file: LICENSE @@ -12,26 +12,31 @@ bug-reports: https://github.com/Copilot-Language/copilot/issues stability: Experimental description: - This package is the main entry-point for using Copilot. + Copilot is a stream-based runtime verification framewor implemented as an + embedded domain-specific language (EDSL) in Haskell. Programs can be + interpreted for testing, or translated into C99 code to be incorporated in a + project, or as a standalone application. The C99 backend output is constant + in memory and time, making it suitable for systems with hard realtime + requirements. . - Copilot is a stream (i.e., infinite lists) domain-specific language (DSL) in - Haskell that compiles into embedded C. Copilot contains an interpreter, - multiple back-end compilers, and other verification tools. + This package is the main entry-point for using Copilot. . A tutorial, examples, and other information are available at . extra-source-files: README.md - Examples/Heater.hs - Examples/Array.hs - Examples/Counter.hs CHANGELOG source-repository head type: git location: https://github.com/Copilot-Language/Copilot.git +flag examples + description: Enable examples + default: False + manual: True + library hs-source-dirs: src default-language: Haskell2010 @@ -45,70 +50,154 @@ , directory >= 1.3 && < 1.4 , filepath >= 1.4 && < 1.5 - , copilot-core >= 3.2 && < 3.3 - , copilot-theorem >= 3.2 && < 3.3 - , copilot-language >= 3.2 && < 3.3 - , copilot-libraries >= 3.2 && < 3.3 - , copilot-c99 >= 3.2 && < 3.3 + , copilot-core >= 3.2.1 && < 3.3 + , copilot-theorem >= 3.2.1 && < 3.3 + , copilot-language >= 3.2.1 && < 3.3 + , copilot-libraries >= 3.2.1 && < 3.3 + , copilot-c99 >= 3.2.1 && < 3.3 exposed-modules: Language.Copilot, Language.Copilot.Main +executable what4-propositional + main-is: Propositional.hs + hs-source-dirs: examples/what4 + build-depends: base + , copilot + , copilot-theorem + default-language: Haskell2010 + if flag(examples) + buildable: True + else + buildable: False +executable what4-arithmetic + main-is: Arithmetic.hs + hs-source-dirs: examples/what4 + build-depends: base + , copilot + , copilot-theorem + default-language: Haskell2010 + if flag(examples) + buildable: True + else + buildable: False + +executable what4-structs + main-is: Structs.hs + hs-source-dirs: examples/what4 + build-depends: base + , copilot + , copilot-theorem + default-language: Haskell2010 + if flag(examples) + buildable: True + else + buildable: False + +executable wcv + main-is: WCV.hs + hs-source-dirs: examples + build-depends: base >= 4.9 && < 5 + , copilot + , copilot-core + , copilot-theorem + default-language: Haskell2010 + if flag(examples) + buildable: True + else + buildable: False + executable addmult main-is: AddMult.hs - hs-source-dirs: Examples + hs-source-dirs: examples build-depends: base >= 4.9 && < 5 - , copilot >= 3.2 && < 3.3 + , copilot + , copilot-core + , copilot-theorem default-language: Haskell2010 + if flag(examples) + buildable: True + else + buildable: False executable array main-is: Array.hs - hs-source-dirs: Examples + hs-source-dirs: examples build-depends: base >= 4.9 && < 5 - , copilot >= 3.2 && < 3.3 + , copilot default-language: Haskell2010 + if flag(examples) + buildable: True + else + buildable: False executable cast main-is: Cast.hs - hs-source-dirs: Examples + hs-source-dirs: examples build-depends: base >= 4.9 && < 5 - , copilot >= 3.2 && < 3.3 + , copilot default-language: Haskell2010 + if flag(examples) + buildable: True + else + buildable: False executable clock main-is: Clock.hs - hs-source-dirs: Examples + hs-source-dirs: examples build-depends: base >= 4.9 && < 5 - , copilot >= 3.2 && < 3.3 - , copilot-libraries >= 3.2 && < 3.3 + , copilot + , copilot-libraries + , copilot-core + , copilot-theorem default-language: Haskell2010 + if flag(examples) + buildable: True + else + buildable: False executable counter main-is: Counter.hs - hs-source-dirs: Examples + hs-source-dirs: examples build-depends: base >= 4.9 && < 5 - , copilot >= 3.2 && < 3.3 + , copilot default-language: Haskell2010 + if flag(examples) + buildable: True + else + buildable: False executable engine main-is: Engine.hs - hs-source-dirs: Examples + hs-source-dirs: examples build-depends: base >= 4.9 && < 5 - , copilot >= 3.2 && < 3.3 + , copilot default-language: Haskell2010 + if flag(examples) + buildable: True + else + buildable: False executable heater main-is: Heater.hs - hs-source-dirs: Examples + hs-source-dirs: examples build-depends: base >= 4.9 && < 5 - , copilot >= 3.2 && < 3.3 - , copilot-c99 >= 3.2 && < 3.3 + , copilot + , copilot-c99 default-language: Haskell2010 + if flag(examples) + buildable: True + else + buildable: False executable voting main-is: Voting.hs - hs-source-dirs: Examples + hs-source-dirs: examples build-depends: base >= 4.9 && < 5 - , copilot >= 3.2 && < 3.3 + , copilot default-language: Haskell2010 + if flag(examples) + buildable: True + else + buildable: False diff --git a/examples/AddMult.hs b/examples/AddMult.hs new file mode 100644 --- /dev/null +++ b/examples/AddMult.hs @@ -0,0 +1,20 @@ +-------------------------------------------------------------------------------- +-- Copyright © 2019 National Institute of Aerospace / Galois, Inc. +-------------------------------------------------------------------------------- + +-- | Another small example that calculates a constant value using a recursive +-- function. + +module Main where + +import Language.Copilot + +spec :: Spec +spec = trigger "f" true [ arg $ mult 5 ] + where + mult :: Word64 -> Stream Word64 + mult 0 = 1 + mult i = constant i * mult (i-1) + +main :: IO () +main = interpret 100 spec diff --git a/examples/Array.hs b/examples/Array.hs new file mode 100644 --- /dev/null +++ b/examples/Array.hs @@ -0,0 +1,35 @@ +-------------------------------------------------------------------------------- +-- Copyright © 2019 National Institute of Aerospace / Galois, Inc. +-------------------------------------------------------------------------------- + +-- | This is a simple example for arrays. As a program, it does not make much +-- sense, however it shows of the features of arrays nicely. + +-- | Enable compiler extension for type-level data, necesary for the array +-- length. + +{-# LANGUAGE RebindableSyntax #-} +{-# LANGUAGE DataKinds #-} + +module Main where + +import Language.Copilot + +-- Lets define an array of length 2. +-- Make the buffer of the streams 3 elements long. +arr :: Stream (Array 2 Bool) +arr = [ array [True, False] + , array [True, True] + , array [False, False]] ++ arr + +spec :: Spec +spec = do + -- A trigger that fires 'func' when the first element of 'arr' is True. + -- It passes the current value of arr as an argument. + -- The prototype of 'func' would be: + -- void func (int8_t arg[3]); + trigger "func" (arr .!! 0) [arg arr] + +-- Compile the spec +main :: IO () +main = interpret 30 spec diff --git a/examples/Cast.hs b/examples/Cast.hs new file mode 100644 --- /dev/null +++ b/examples/Cast.hs @@ -0,0 +1,29 @@ +-------------------------------------------------------------------------------- +-- Copyright © 2019 National Institute of Aerospace / Galois, Inc. +-------------------------------------------------------------------------------- + +-- | Examples of casting types. + +{-# LANGUAGE RebindableSyntax #-} + +module Main where + +import Language.Copilot + +b :: Stream Bool +b = [True] ++ not b + +i :: Stream Int8 +i = cast b + +x :: Stream Word16 +x = [0] ++ x + 1 + +y :: Stream Int32 +y = 1 + cast x + +spec :: Spec +spec = trigger "trigger" true [arg y, arg i] + +main :: IO () +main = interpret 30 spec diff --git a/examples/Clock.hs b/examples/Clock.hs new file mode 100644 --- /dev/null +++ b/examples/Clock.hs @@ -0,0 +1,30 @@ +-------------------------------------------------------------------------------- +-- Copyright © 2019 National Institute of Aerospace / Galois, Inc. +-------------------------------------------------------------------------------- + +-- | Example showing usage of clocks to generate periodically recurring truth +-- values. + +module Main where + +import Language.Copilot +import Copilot.Library.Clocks + +-- | We need to force a type for the argument of `period`. +p :: Word8 +p = 5 + +-- | Both have the same period, but a different phase. +clkStream :: Stream Bool +clkStream = clk (period p) (phase 0) + +clkStream' :: Stream Bool +clkStream' = clk (period p) (phase 2) + +spec :: Spec +spec = do + observer "clk" clkStream + observer "clk'" clkStream' + +main :: IO () +main = interpret 30 spec diff --git a/examples/Counter.hs b/examples/Counter.hs new file mode 100644 --- /dev/null +++ b/examples/Counter.hs @@ -0,0 +1,31 @@ +-------------------------------------------------------------------------------- +-- Copyright © 2019 National Institute of Aerospace / Galois, Inc. +-------------------------------------------------------------------------------- + +-- | Example showing an implementation of a resettable counter. + +{-# LANGUAGE RebindableSyntax #-} + +module Main where + +import Language.Copilot + +-- A resettable counter +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 + +-- Counter that resets when it reaches 256 +bytecounter :: Stream Int32 +bytecounter = counter true reset where + reset = counter true false == 256 + +spec :: Spec +spec = trigger "counter" true [arg $ bytecounter] + +main :: IO () +main = interpret 270 spec diff --git a/examples/Engine.hs b/examples/Engine.hs new file mode 100644 --- /dev/null +++ b/examples/Engine.hs @@ -0,0 +1,38 @@ +-------------------------------------------------------------------------------- +-- Copyright © 2011 National Institute of Aerospace / Galois, Inc. +-------------------------------------------------------------------------------- + +-- | Example implementing an engine cooling control system. + +{-# LANGUAGE RebindableSyntax #-} + +module Main where + +import Language.Copilot +import qualified Prelude as P + +{- If the majority of the engine temperature probes exeeds 250 degrees, then + - the cooler is engaged and remains engaged until the majority of the engine + - temperature probes drop to 250 or below. Otherwise, trigger an immediate + - shutdown of the engine. +-} + +engineMonitor :: Spec +engineMonitor = do + trigger "shutoff" (not ok) [arg maj] + + where + vals = [ externW8 "tmp_probe_0" two51 + , externW8 "tmp_probe_1" two51 + , externW8 "tmp_probe_2" zero] + exceed = map (> 250) vals + maj = majority exceed + checkMaj = aMajority exceed maj + ok = alwaysBeen ((maj && checkMaj) ==> extern "cooler" cooler) + + two51 = Just $ [251, 251] P.++ repeat (250 :: Word8) + zero = Just $ repeat (0 :: Word8) + cooler = Just $ [True, True] P.++ repeat False + +main :: IO () +main = interpret 10 engineMonitor diff --git a/examples/Heater.hs b/examples/Heater.hs new file mode 100644 --- /dev/null +++ b/examples/Heater.hs @@ -0,0 +1,34 @@ +-------------------------------------------------------------------------------- +-- 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 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 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" diff --git a/examples/Voting.hs b/examples/Voting.hs new file mode 100644 --- /dev/null +++ b/examples/Voting.hs @@ -0,0 +1,57 @@ +-------------------------------------------------------------------------------- +-- Copyright © 2019 National Institute of Aerospace / Galois, Inc. +-------------------------------------------------------------------------------- + +-- | Fault-tolerant voting examples. + +{-# LANGUAGE RebindableSyntax #-} + +module Main where + +import Language.Copilot + +vote :: Spec +vote = do + -- majority selects element with the biggest occurance. + trigger "maj" true [arg maj] + + -- aMajority checks if the selected element has a majority. + trigger "aMaj" true [arg $ aMajority inputs maj] + + where + maj = majority inputs + + -- 26 input streams to vote on + inputs :: [Stream Word32] + inputs = [ a, b, c, d, e, f, g, h, i, j, k, l, m + , n, o, p, q, r, s, t, u, v, w, x, y, z + ] + a = [0] ++ a + 1 + b = [0] ++ b + 1 + c = [0] ++ c + 1 + d = [0] ++ d + 1 + e = [1] ++ e + 1 + f = [1] ++ f + 1 + g = [1] ++ g + 1 + h = [1] ++ h + 1 + i = [1] ++ i + 1 + j = [1] ++ j + 1 + k = [1] ++ k + 1 + l = [1] ++ l + 1 + m = [1] ++ m + 1 + n = [1] ++ n + 1 + o = [1] ++ o + 1 + p = [1] ++ p + 1 + q = [1] ++ q + 1 + r = [1] ++ r + 1 + s = [1] ++ s + 1 + t = [1] ++ t + 1 + u = [1] ++ u + 1 + v = [1] ++ v + 1 + w = [1] ++ w + 1 + x = [1] ++ x + 1 + y = [1] ++ y + 1 + z = [1] ++ z + 1 + +main :: IO () +main = interpret 30 vote diff --git a/examples/WCV.hs b/examples/WCV.hs new file mode 100644 --- /dev/null +++ b/examples/WCV.hs @@ -0,0 +1,186 @@ +-- | This example shows an implementation of the Well-Clear Violation +-- algorithm, it follows the implementation described in 'Analysis of +-- Well-Clear Bounday Models for the Integration of UAS in the NAS', +-- https://ntrs.nasa.gov/citations/20140010078. + +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE RebindableSyntax #-} + +module Main where + +import Language.Copilot +import qualified Copilot.Theorem.What4 as CT +import qualified Prelude as P +import Data.Foldable (forM_) +import qualified Control.Monad as Monad + + +-- | `dthr` is the horizontal distance threshold. +dthr :: Stream Double +dthr = extern "dthr" Nothing + +-- | `tthr` is the horizontal time threshold. +tthr :: Stream Double +tthr = extern "tthr" Nothing + +-- | `zthr` is the vertical distance / altitude threshold. +zthr :: Stream Double +zthr = extern "zthr" Nothing + +-- | `tcoathr` is the vertical time threshold. +tcoathr :: Stream Double +tcoathr = extern "tcoathr" Nothing + +type Vect2 = (Stream Double, Stream Double) + + +-------------------------------- +-- External streams for relative position and velocity. +-------------------------------- + +-- | The relative x velocity between ownship and the intruder. +vx :: Stream Double +vx = extern "relative_velocity_x" Nothing + +-- | The relative y velocity between ownship and the intruder. +vy :: Stream Double +vy = extern "relative_velocity_y" Nothing + +-- | The relative z velocity between ownship and the intruder. +vz :: Stream Double +vz = extern "relative_velocity_z" Nothing + +-- | The relative velocity as a 2D vector. +v :: (Stream Double, Stream Double) +v = (vx, vy) + + +-- | The relative x position between ownship and the intruder. +sx :: Stream Double +sx = extern "relative_position_x" Nothing + +-- | The relative y position between ownship and the intruder. +sy :: Stream Double +sy = extern "relative_position_y" Nothing + +-- | The relative z position between ownship and the intruder. +sz :: Stream Double +sz = extern "relative_position_z" Nothing + +-- | The relative position as a 2D vector. +s :: (Stream Double, Stream Double) +s = (sx, sy) + + +------------------ +-- The following section contains basic libraries for working with vectors. +------------------ + +-- | Multiply two Vectors. +(|*|) :: Vect2 -> Vect2 -> Stream Double +(|*|) (x1, y1) (x2, y2) = (x1 * x2) + (y1 * y2) + +-- | Calculate the square of a vector. +sq :: Vect2 -> Stream Double +sq x = x |*| x + +-- | Calculate the length of a vector. +norm :: Vect2 -> Stream Double +norm = sqrt . sq + +-- | Calculate the determinant of two vectors. +det :: Vect2 -> Vect2 -> Stream Double +det (x1, y1) (x2, y2) = (x1 * y2) - (x2 * y1) + +-- | Compare two vectors, taking into account the small error that is +-- introduced by the usage of `Double`s. +(~=) :: Stream Double -> Stream Double -> Stream Bool +a ~= b = (abs (a - b)) < 0.001 + +-- | Negate a vector. +neg :: Vect2 -> Vect2 +neg (x, y) = (negate x, negate y) + + +-------------------- +-- From here on the algorithm, as described by the paper mentioned on the top +-- of this file, is implemented. Please refer to the paper for details. +-------------------- + +tau :: Vect2 -> Vect2 -> Stream Double +tau s v = if s |*| v < 0 + then (-(sq s)) / (s |*| v) + else -1 + +tcpa :: Vect2 -> Vect2 -> Stream Double +tcpa s v@(vx, vy) = if vx ~= 0 && vy ~= 0 + then 0 + else -(s |*| v)/(sq v) + +taumod :: Vect2 -> Vect2 -> Stream Double +taumod s v = if s |*| v < 0 + then (dthr * dthr - (sq s))/(s |*| v) + else -1 + +tep :: Vect2 -> Vect2 -> Stream Double +tep s v = if (s |*| v < 0) && ((delta s v dthr) >= 0) + then theta s v dthr (-1) + else -1 + +delta :: Vect2 -> Vect2 -> Stream Double -> Stream Double +delta s v d = (d*d) * (sq v) - ((det s v)*(det s v)) +-- Here the formula says : (s . orth v)^2 which is the same as det(s,v)^2 + +theta :: Vect2 -> Vect2 -> Stream Double -> Stream Double -> Stream Double +theta s v d e = (-(s |*| v) + e * (sqrt $ delta s v d)) / (sq v) + + +tcoa :: Stream Double -> Stream Double -> Stream Double +tcoa sz vz = if (sz * vz) < 0 + then (-sz) / vz + else -1 + +dcpa :: Vect2 -> Vect2 -> Stream Double +dcpa s@(sx, sy) v@(vx, vy) = norm (sx + (tcpa s v) * vx, sy + (tcpa s v) * vy) + + +-------------------------- +-- Well clear Violation -- +-------------------------- + +-- | Determines if the well clear property is violated or not. +wcv :: (Vect2 -> Vect2 -> Stream Double) -> + Vect2 -> Stream Double -> + Vect2 -> Stream Double -> + Stream Bool +wcv tvar s sz v vz = (horizontalWCV tvar s v) && (verticalWCV sz vz) + +verticalWCV :: Stream Double -> Stream Double -> Stream Bool +verticalWCV sz vz = + ((abs $ sz) <= zthr) || + (0 <= (tcoa sz vz) && (tcoa sz vz) <= tcoathr) + +horizontalWCV :: (Vect2 -> Vect2 -> Stream Double) -> Vect2 -> Vect2 -> Stream Bool +horizontalWCV tvar s v = + (norm s <= dthr) || + (((dcpa s v) <= dthr) && (0 <= (tvar s v)) && ((tvar s v) <= tthr)) + +spec = do + Monad.void $ prop "1a" (forall $ (tau s v) ~= (tau (neg s) (neg v))) + -- Monad.void $ prop "3d" (forall $ (wcv tep s sz v vz) == (wcv tep (neg s) (-sz) (neg v) (-vz))) + + +main :: IO () +main = do + spec' <- reify spec + + -- Use Z3 to prove the properties. + results <- CT.prove CT.Z3 spec' + + -- Print the results. + forM_ results $ \(nm, res) -> do + putStr $ nm <> ": " + case res of + CT.Valid -> putStrLn "valid" + CT.Invalid -> putStrLn "invalid" + CT.Unknown -> putStrLn "unknown" diff --git a/examples/what4/Arithmetic.hs b/examples/what4/Arithmetic.hs new file mode 100644 --- /dev/null +++ b/examples/what4/Arithmetic.hs @@ -0,0 +1,55 @@ +-- | An example showing the usage of the What4 backend in copilot-theorem for +-- simple arithmetic. + +module Main where + +import qualified Prelude as P +import Control.Monad (void, forM_) + +import Language.Copilot +import Copilot.Theorem.What4 + +spec :: Spec +spec = do + -- Define some external streams. Their values are not important, so external + -- streams suffice. + let eint8 :: Stream Int8 + eint8 = extern "eint8" Nothing + eword8 :: Stream Word8 + eword8 = extern "eword8" Nothing + efloat :: Stream Float + efloat = extern "efloat" Nothing + + -- The simplest example involving numbers: equality on constant values. + void $ prop "Example 1" (forall ((constant (1 :: Int8)) == (constant 1))) + + -- Testing "a < a + 1". This should fail, because it isn't true. + void $ prop "Example 2" (forall (eint8 < (eint8 + 1))) + + -- Adding another condition to the above property to make it true. + void $ prop "Example 3" (forall ((eint8 < (eint8 + 1)) || (eint8 == 127))) + + -- Just like the previous example, but with words. + void $ prop "Example 4" (forall ((eword8 < (eword8 + 1)) || (eword8 == 255))) + + -- An example with floats. + void $ prop "Example 5" (forall ((2 * efloat) == (efloat + efloat))) + + -- Another example with floats. This fails, because it isn't true. + void $ prop "Example 6" (forall ((efloat + 1) /= efloat)) + + +main :: IO () +main = do + spec' <- reify spec + + -- Use Z3 to prove the properties. + results <- prove Z3 spec' + + -- Print the results. + forM_ results $ \(nm, res) -> do + putStr $ nm <> ": " + case res of + Valid -> putStrLn "valid" + Invalid -> putStrLn "invalid" + Unknown -> putStrLn "unknown" diff --git a/examples/what4/Propositional.hs b/examples/what4/Propositional.hs new file mode 100644 --- /dev/null +++ b/examples/what4/Propositional.hs @@ -0,0 +1,63 @@ +-- | An example showing the usage of the What4 backend in copilot-theorem for +-- propositional logic on boolean streams. + +module Main where + +import qualified Prelude as P +import Control.Monad (void, forM_) + +import Language.Copilot +import Copilot.Theorem.What4 + +spec :: Spec +spec = do + -- The constant value true, which is translated as the corresponding SMT + -- boolean literal. + void $ prop "Example 1" (forall true) + + -- The constant value false, which is translated as the corresponding SMT + -- boolean literal. + void $ prop "Example 2" (forall false) + + -- An inductively defined flavor of true, which requires induction to prove, + -- and hence is found to be invalid by the SMT solver (since no inductive + -- hypothesis is made). + let a = [True] ++ a + void $ prop "Example 3" (forall a) + + -- An inductively defined "a or not a" proposition, which is unprovable by + -- the SMT solver. + let a = [False] ++ b + b = [True] ++ a + void $ prop "Example 4" (forall (a || b)) + + -- A version of "a or not a" proposition which does not require any sort of + -- inductive argument, and hence is provable. + let a = [False] ++ b + b = not a + void $ 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) + void $ prop "Example 6" (forall (a || b)) + + -- An example using external streams. + let a = extern "a" Nothing + void $ prop "Example 7" (forall (a || not a)) + + +main :: IO () +main = do + spec' <- reify spec + + -- Use Z3 to prove the properties. + results <- prove Z3 spec' + + -- Print the results. + forM_ results $ \(nm, res) -> do + putStr $ nm <> ": " + case res of + Valid -> putStrLn "valid" + Invalid -> putStrLn "invalid" + Unknown -> putStrLn "unknown" diff --git a/examples/what4/Structs.hs b/examples/what4/Structs.hs new file mode 100644 --- /dev/null +++ b/examples/what4/Structs.hs @@ -0,0 +1,82 @@ +-- | An example showing the usage of the What4 backend in copilot-theorem for +-- structs and arrays. Particular focus is on nested structs. +-- For general usage of structs, refer to the general structs example. + +{-# LANGUAGE DataKinds #-} + +module Main where + +import qualified Prelude as P +import Control.Monad (void, forM_) + +import Language.Copilot +import Copilot.Theorem.What4 + + +-- | Definition for `Volts`. +data Volts = Volts + { numVolts :: Field "numVolts" Word16 + , flag :: Field "flag" Bool + } + +-- | `Struct` instance for `Volts`. +instance Struct Volts where + typename _ = "volts" + toValues volts = [ Value Word16 (numVolts volts) + , Value Bool (flag volts) + ] + +-- | `Volts` instance for `Typed`. +instance Typed Volts where + typeOf = Struct (Volts (Field 0) (Field False)) + +data Battery = Battery + { temp :: Field "temp" Word16 + , volts :: Field "volts" (Array 10 Volts) + , other :: Field "other" (Array 10 (Array 5 Word32)) + } + +-- | `Battery` instance for `Struct`. +instance Struct Battery where + typename _ = "battery" + toValues battery = [ Value typeOf (temp battery) + , Value typeOf (volts battery) + , Value typeOf (other battery) + ] + +-- | `Battery` instance for `Typed`. Note that `undefined` is used as an +-- argument to `Field`. This argument is never used, so `undefined` will never +-- throw an error. +instance Typed Battery where + typeOf = Struct (Battery (Field 0) (Field undefined) (Field undefined)) + +spec :: Spec +spec = do + let battery :: Stream Battery + battery = extern "battery" Nothing + + -- Check equality, indexing into nested structs and arrays. Note that this is + -- trivial by equality. + void $ prop "Example 1" $ forall $ + (((battery#volts) .!! 0)#numVolts) == (((battery#volts) .!! 0)#numVolts) + + -- Same as previous example, but get a different array index (so should be + -- false). + void $ prop "Example 2" $ forall $ + (((battery#other) .!! 2) .!! 3) == (((battery#other) .!! 2) .!! 4) + + +main :: IO () +main = do + spec' <- reify spec + + -- Use Z3 to prove the properties. + results <- prove Z3 spec' + + -- Print the results. + forM_ results $ \(nm, res) -> do + putStr $ nm <> ": " + case res of + Valid -> putStrLn "valid" + Invalid -> putStrLn "invalid" + Unknown -> putStrLn "unknown" diff --git a/src/Language/Copilot.hs b/src/Language/Copilot.hs --- a/src/Language/Copilot.hs +++ b/src/Language/Copilot.hs @@ -1,7 +1,19 @@ -module Language.Copilot +-- | Copilot is a stream-based runtime verification framework. Programs can be +-- interpreted for testing, or translated into C99 code to be incorporated in a +-- project, or as a standalone application. The C99 backend output is constant +-- in memory and time, making it suitable for systems with hard realtime +-- requirements. +-- +-- This module is the main entry point for the Copilot language. The +-- expectation is that most Copilot users will only need to import this module, +-- together with one of the backend modules (at present, only +-- 'Copilot.Compile.C99' from the +-- library is +-- available). +module Language.Copilot ( module Copilot.Language - , module Copilot.Language.Prelude + , module Copilot.Language.Prelude , module Copilot.Language.Reify -- Code generators @@ -23,7 +35,7 @@ ) where import Copilot.Language -import Copilot.Language.Prelude +import Copilot.Language.Prelude import Copilot.Language.Reify -- Code generators diff --git a/src/Language/Copilot/Main.hs b/src/Language/Copilot/Main.hs --- a/src/Language/Copilot/Main.hs +++ b/src/Language/Copilot/Main.hs @@ -1,3 +1,5 @@ +-- | Create Copilot executables that generate code or interpret streams and +-- print the results to stdout. module Language.Copilot.Main ( copilotMain, defaultMain ) where import qualified Copilot.Core as C (Spec) @@ -9,12 +11,19 @@ import Data.Semigroup ((<>)) import Control.Monad (when) - +-- | An interpreter of Copilot specifications for a given +-- number of simulation steps. type Interpreter = Integer -> Spec -> IO () + +-- | A compiler from +-- +-- specifications. type Compiler = FilePath -> C.Spec -> IO () -type Printer = Spec -> IO () +-- | A pretty printer of Copilot specifications. +type Printer = Spec -> IO () +-- | Command line arguments supported by all commands in 'cmdargs'. data CmdArgs = CmdArgs { aoutput :: String , acompile :: Bool @@ -22,6 +31,7 @@ , ainterpret :: Int } +-- | Command line arguments handled by the Copilot main function. cmdargs :: Parser CmdArgs cmdargs = CmdArgs <$> strOption (long "output" <> short 'o' <> value "." @@ -35,6 +45,23 @@ <> help "Interpret specification and write result to output") +-- | Create a main to either compile or interpret a copilot specification. +-- +-- This function must be provided an auxiliary function capable of compiling +-- +-- specifications for some target. +-- +-- The command line program supports four main commands: +-- +-- * @--output/-o@: use the given compiler to produce C code. +-- +-- * @--justrun/-c@: execute a dry-run, which parses and converts the +-- specification to core but does not produce any output. +-- +-- * @--print/-p@: pretty print the specification. +-- +-- * @--interpret/-i NUM@: interpret the specification for a given number +-- of steps. copilotMain :: Interpreter -> Printer -> Compiler -> Spec -> IO () copilotMain interp pretty comp spec = main =<< execParser opts where opts = info (cmdargs <**> helper) fullDesc @@ -49,5 +76,13 @@ spec' <- reify spec comp (aoutput args) spec' +-- | Create a main function with a default interpreter and pretty printer. +-- +-- This function must be provided an auxiliary function capable of compiling +-- +-- specifications for some target. +-- +-- This function relies on 'copilotMain', please refer to that function for the +-- command line options. defaultMain :: Compiler -> Spec -> IO () defaultMain = copilotMain interpret prettyPrint