copilot-language-3.0: A Haskell-embedded DSL for monitoring hard real-time distributed systems.

Safe HaskellSafe
LanguageHaskell2010

Copilot.Language.Spec

Description

Copilot specifications.

Documentation

type Spec = Writer [SpecItem] () Source #

type Spec' a = Writer [SpecItem] a Source #

runSpec :: Spec' a -> [SpecItem] Source #

data SpecItem Source #

data Observer where Source #

Constructors

Observer :: Typed a => String -> Stream a -> Observer 

observer :: Typed a => String -> Stream a -> Spec Source #

observers :: [SpecItem] -> [Observer] Source #

data Trigger where Source #

Constructors

Trigger :: Name -> Stream Bool -> [Arg] -> Trigger 

trigger :: String -> Stream Bool -> [Arg] -> Spec Source #

triggers :: [SpecItem] -> [Trigger] Source #

arg :: Typed a => Stream a -> Arg Source #

data Property where Source #

Constructors

Property :: String -> Stream Bool -> Property 

data Prop a where Source #

Constructors

Forall :: Stream Bool -> Prop Universal 
Exists :: Stream Bool -> Prop Existential 

prop :: String -> Prop a -> Writer [SpecItem] (PropRef a) Source #

properties :: [SpecItem] -> [Property] Source #

theorem :: String -> Prop a -> Proof a -> Writer [SpecItem] (PropRef a) Source #

theorems :: [SpecItem] -> [(Property, UProof)] Source #

forall :: Stream Bool -> Prop Universal Source #

exists :: Stream Bool -> Prop Existential Source #

extractProp :: Prop a -> Stream Bool Source #

data Universal #

data Existential #