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

Copilot.Language.Spec

Description

Copilot specifications consistute the main declaration of Copilot modules.

A specification normally contains the association between streams to monitor and their handling functions, or streams to observe, or a theorem that must be proved.

In order to be executed, Specs must be turned into Copilot Core (see Reify) and either simulated or converted into C99 code to be executed.

Synopsis

# Documentation

type Spec = Writer [SpecItem] () Source #

A specification is a list of declarations of triggers, observers, properties and theorems.

Specifications are normally declared in monadic style, for example:

monitor1 :: Stream Bool
monitor1 = [False] ++ not monitor1

counter :: Stream Int32
counter = [0] ++ not counter

spec :: Spec
spec = do
trigger "handler_1" monitor1 []
trigger "handler_2" (counter > 10) [arg counter]


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

An action in a specification (e.g., a declaration) that returns a value that can be used in subsequent actions.

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

Return the complete list of declarations inside a Spec or Spec'.

The word run in this function is unrelated to running the underlying specifications or monitors, and is merely related to the monad defined by a Spec

data SpecItem Source #

An item of a Copilot specification.

data Observer where Source #

An observer, representing a stream that we observe during execution at every sample.

Constructors

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

Arguments

 :: Typed a => String Name used to identify the stream monitored in the output produced during interpretation. -> Stream a The stream being monitored. -> Spec

Define a new observer as part of a specification. This allows someone to print the value at every iteration during interpretation. Observers do not have any functionality outside the interpreter.

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

Filter a list of spec items to keep only the observers.

data Trigger where Source #

A trigger, representing a function we execute when a boolean stream becomes true at a sample.

Constructors

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

Arguments

 :: String Name of the handler to be called. -> Stream Bool The stream used as the guard for the trigger. -> [Arg] List of arguments to the handler. -> Spec

Define a new trigger as part of a specification. A trigger declares which external function, or handler, will be called when a guard defined by a boolean stream becomes true.

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

Filter a list of spec items to keep only the triggers.

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

Construct a function argument from a stream.

Args can be used to pass arguments to handlers or trigger functions, to provide additional information to monitor handlers in order to address property violations. At any given point (e.g., when the trigger must be called due to a violation), the arguments passed using arg will contain the current samples of the given streams.

data Property where Source #

A property, representing a boolean stream that is existentially or universally quantified over time.

Constructors

 Property :: String -> Stream Bool -> Property

data Prop a where Source #

A proposition, representing the quantification of a boolean streams over time.

Constructors

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

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

A proposition, representing a boolean stream that is existentially or universally quantified over time, as part of a specification.

This function returns, in the monadic context, a reference to the proposition.

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

Filter a list of spec items to keep only the properties.

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

A theorem, or proposition together with a proof.

This function returns, in the monadic context, a reference to the proposition.

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

Filter a list of spec items to keep only the theorems.

Universal quantification of boolean streams over time.

Existential quantification of boolean streams over time.

Extract the underlying stream from a quantified proposition.