copilot-core-3.3: An intermediate representation for Copilot.

Copilot.Core.Spec

Description

Copilot specifications constitute 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, high-level Copilot Language Spec must be turned into Copilot Core's Spec. This module defines the low-level Copilot Core representations for Specs and the main types of element in a spec..

Synopsis

Documentation

data Stream Source #

A stream in an infinite succession of values of the same type.

Stream can carry different types of data. Boolean streams play a special role: they are used by other parts (e.g., Trigger) to detect when the properties being monitored are violated.

Constructors

 forall a.(Typeable a, Typed a) => Stream FieldsstreamId :: Id streamBuffer :: [a] streamExpr :: Expr a streamExprType :: Type a

data Observer Source #

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

Constructors

 forall a.Typeable a => Observer FieldsobserverName :: Name observerExpr :: Expr a observerExprType :: Type a

data Trigger Source #

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

Constructors

 Trigger FieldstriggerName :: Name triggerGuard :: Expr Bool triggerArgs :: [UExpr]

data Spec Source #

A Copilot specification is a list of streams, together with monitors on these streams implemented as observers, triggers or properties.

Constructors

 Spec FieldsspecStreams :: [Stream] specObservers :: [Observer] specTriggers :: [Trigger] specProperties :: [Property]

data Property Source #

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

Constructors

 Property FieldspropertyName :: Name propertyExpr :: Expr Bool