copilot-language-3.0.1: A Haskell-embedded DSL for monitoring hard real-time distributed systems.
Copilot.Language.Spec
Description
Copilot specifications.
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 -> Spec Source #
observers :: [SpecItem] -> [Observer] Source #
data Trigger where Source #
trigger :: String -> Stream Bool -> [Arg] -> Spec Source #
triggers :: [SpecItem] -> [Trigger] Source #
arg :: Typed a => Stream a -> Arg Source #
data Property where Source #
data Prop a where Source #
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 #