copilot 3.2 → 3.2.1
raw patch · 25 files changed
+858/−313 lines, 25 filesdep ~basedep ~copilotdep ~copilot-c99new-component:exe:wcvnew-component:exe:what4-arithmeticnew-component:exe:what4-propositionalnew-component:exe:what4-structsPVP ok
version bump matches the API change (PVP)
Dependency ranges changed: base, copilot, copilot-c99, copilot-core, copilot-language, copilot-libraries, copilot-theorem
API changes (from Hackage documentation)
Files
- CHANGELOG +12/−0
- Examples/AddMult.hs +0/−20
- Examples/Array.hs +0/−35
- Examples/Cast.hs +0/−29
- Examples/Clock.hs +0/−30
- Examples/Counter.hs +0/−31
- Examples/Engine.hs +0/−38
- Examples/Heater.hs +0/−34
- Examples/Voting.hs +0/−57
- README.md +14/−3
- copilot.cabal +120/−31
- examples/AddMult.hs +20/−0
- examples/Array.hs +35/−0
- examples/Cast.hs +29/−0
- examples/Clock.hs +30/−0
- examples/Counter.hs +31/−0
- examples/Engine.hs +38/−0
- examples/Heater.hs +34/−0
- examples/Voting.hs +57/−0
- examples/WCV.hs +186/−0
- examples/what4/Arithmetic.hs +55/−0
- examples/what4/Propositional.hs +63/−0
- examples/what4/Structs.hs +82/−0
- src/Language/Copilot.hs +15/−3
- src/Language/Copilot/Main.hs +37/−2
CHANGELOG view
@@ -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).
− Examples/AddMult.hs
@@ -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
− Examples/Array.hs
@@ -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
− Examples/Cast.hs
@@ -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
− Examples/Clock.hs
@@ -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
− Examples/Counter.hs
@@ -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
− Examples/Engine.hs
@@ -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
− Examples/Heater.hs
@@ -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"
− Examples/Voting.hs
@@ -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
README.md view
@@ -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
copilot.cabal view
@@ -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 <https://copilot-language.github.io>. 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
+ examples/AddMult.hs view
@@ -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
+ examples/Array.hs view
@@ -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
+ examples/Cast.hs view
@@ -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
+ examples/Clock.hs view
@@ -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
+ examples/Counter.hs view
@@ -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
+ examples/Engine.hs view
@@ -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
+ examples/Heater.hs view
@@ -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"
+ examples/Voting.hs view
@@ -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
+ examples/WCV.hs view
@@ -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"
+ examples/what4/Arithmetic.hs view
@@ -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"
+ examples/what4/Propositional.hs view
@@ -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"
+ examples/what4/Structs.hs view
@@ -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"
src/Language/Copilot.hs view
@@ -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+-- <https://hackage.haskell.org/package/copilot-c99 copilot-c99> 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
src/Language/Copilot/Main.hs view
@@ -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+-- <https://hackage.haskell.org/package/copilot-core Copilot Core>+-- 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+-- <https://hackage.haskell.org/package/copilot-core Copilot Core>+-- 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+-- <https://hackage.haskell.org/package/copilot-core Copilot Core>+-- 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