copilot-language-3.3: A Haskell-embedded DSL for monitoring hard real-time distributed systems.
Safe HaskellSafe
LanguageHaskell2010

Copilot.Language

Description

Main Copilot language export file.

This is mainly a meta-module that re-exports most definitions in this library. It also provides a default pretty printer that prints a specification to stdout.

Synopsis

Documentation

data Int8 #

8-bit signed integer type

Instances

Instances details
Bounded Int8

Since: base-2.1

Instance details

Defined in GHC.Int

Enum Int8

Since: base-2.1

Instance details

Defined in GHC.Int

Methods

succ :: Int8 -> Int8 #

pred :: Int8 -> Int8 #

toEnum :: Int -> Int8 #

fromEnum :: Int8 -> Int #

enumFrom :: Int8 -> [Int8] #

enumFromThen :: Int8 -> Int8 -> [Int8] #

enumFromTo :: Int8 -> Int8 -> [Int8] #

enumFromThenTo :: Int8 -> Int8 -> Int8 -> [Int8] #

Eq Int8

Since: base-2.1

Instance details

Defined in GHC.Int

Methods

(==) :: Int8 -> Int8 -> Bool #

(/=) :: Int8 -> Int8 -> Bool #

Integral Int8

Since: base-2.1

Instance details

Defined in GHC.Int

Methods

quot :: Int8 -> Int8 -> Int8 #

rem :: Int8 -> Int8 -> Int8 #

div :: Int8 -> Int8 -> Int8 #

mod :: Int8 -> Int8 -> Int8 #

quotRem :: Int8 -> Int8 -> (Int8, Int8) #

divMod :: Int8 -> Int8 -> (Int8, Int8) #

toInteger :: Int8 -> Integer #

Num Int8

Since: base-2.1

Instance details

Defined in GHC.Int

Methods

(+) :: Int8 -> Int8 -> Int8 #

(-) :: Int8 -> Int8 -> Int8 #

(*) :: Int8 -> Int8 -> Int8 #

negate :: Int8 -> Int8 #

abs :: Int8 -> Int8 #

signum :: Int8 -> Int8 #

fromInteger :: Integer -> Int8 #

Ord Int8

Since: base-2.1

Instance details

Defined in GHC.Int

Methods

compare :: Int8 -> Int8 -> Ordering #

(<) :: Int8 -> Int8 -> Bool #

(<=) :: Int8 -> Int8 -> Bool #

(>) :: Int8 -> Int8 -> Bool #

(>=) :: Int8 -> Int8 -> Bool #

max :: Int8 -> Int8 -> Int8 #

min :: Int8 -> Int8 -> Int8 #

Read Int8

Since: base-2.1

Instance details

Defined in GHC.Int

Real Int8

Since: base-2.1

Instance details

Defined in GHC.Int

Methods

toRational :: Int8 -> Rational #

Show Int8

Since: base-2.1

Instance details

Defined in GHC.Int

Methods

showsPrec :: Int -> Int8 -> ShowS #

show :: Int8 -> String #

showList :: [Int8] -> ShowS #

Ix Int8

Since: base-2.1

Instance details

Defined in GHC.Int

Methods

range :: (Int8, Int8) -> [Int8] #

index :: (Int8, Int8) -> Int8 -> Int #

unsafeIndex :: (Int8, Int8) -> Int8 -> Int #

inRange :: (Int8, Int8) -> Int8 -> Bool #

rangeSize :: (Int8, Int8) -> Int #

unsafeRangeSize :: (Int8, Int8) -> Int #

Bits Int8

Since: base-2.1

Instance details

Defined in GHC.Int

FiniteBits Int8

Since: base-4.6.0.0

Instance details

Defined in GHC.Int

Typed Int8 
Instance details

Defined in Copilot.Core.Type

UnsafeCast Int8 Double Source #

Unsafe signed integer promotion to floating point values.

Instance details

Defined in Copilot.Language.Operators.Cast

UnsafeCast Int8 Float Source #

Unsafe signed integer promotion to floating point values.

Instance details

Defined in Copilot.Language.Operators.Cast

UnsafeCast Int8 Word8 Source #

Signed to unsigned casting.

Instance details

Defined in Copilot.Language.Operators.Cast

UnsafeCast Int16 Int8 Source #

Unsafe downcasting to smaller sizes.

Instance details

Defined in Copilot.Language.Operators.Cast

UnsafeCast Int32 Int8 Source #

Unsafe downcasting to smaller sizes.

Instance details

Defined in Copilot.Language.Operators.Cast

UnsafeCast Int64 Int8 Source #

Unsafe downcasting to smaller sizes.

Instance details

Defined in Copilot.Language.Operators.Cast

UnsafeCast Word8 Int8 Source #

Cast from unsigned numbers to signed numbers.

Instance details

Defined in Copilot.Language.Operators.Cast

Cast Bool Int8 Source #

Cast a boolean stream to a stream of numbers, producing 1 if the value at a point in time is True, and 0 otherwise.

Instance details

Defined in Copilot.Language.Operators.Cast

Cast Int8 Int8 Source #

Identity casting.

Instance details

Defined in Copilot.Language.Operators.Cast

Cast Int8 Int16 Source #

Cast number to bigger type.

Instance details

Defined in Copilot.Language.Operators.Cast

Cast Int8 Int32 Source #

Cast number to bigger type.

Instance details

Defined in Copilot.Language.Operators.Cast

Cast Int8 Int64 Source #

Cast number to bigger type.

Instance details

Defined in Copilot.Language.Operators.Cast

data Int16 #

16-bit signed integer type

Instances

Instances details
Bounded Int16

Since: base-2.1

Instance details

Defined in GHC.Int

Enum Int16

Since: base-2.1

Instance details

Defined in GHC.Int

Eq Int16

Since: base-2.1

Instance details

Defined in GHC.Int

Methods

(==) :: Int16 -> Int16 -> Bool #

(/=) :: Int16 -> Int16 -> Bool #

Integral Int16

Since: base-2.1

Instance details

Defined in GHC.Int

Num Int16

Since: base-2.1

Instance details

Defined in GHC.Int

Ord Int16

Since: base-2.1

Instance details

Defined in GHC.Int

Methods

compare :: Int16 -> Int16 -> Ordering #

(<) :: Int16 -> Int16 -> Bool #

(<=) :: Int16 -> Int16 -> Bool #

(>) :: Int16 -> Int16 -> Bool #

(>=) :: Int16 -> Int16 -> Bool #

max :: Int16 -> Int16 -> Int16 #

min :: Int16 -> Int16 -> Int16 #

Read Int16

Since: base-2.1

Instance details

Defined in GHC.Int

Real Int16

Since: base-2.1

Instance details

Defined in GHC.Int

Methods

toRational :: Int16 -> Rational #

Show Int16

Since: base-2.1

Instance details

Defined in GHC.Int

Methods

showsPrec :: Int -> Int16 -> ShowS #

show :: Int16 -> String #

showList :: [Int16] -> ShowS #

Ix Int16

Since: base-2.1

Instance details

Defined in GHC.Int

Bits Int16

Since: base-2.1

Instance details

Defined in GHC.Int

FiniteBits Int16

Since: base-4.6.0.0

Instance details

Defined in GHC.Int

Typed Int16 
Instance details

Defined in Copilot.Core.Type

UnsafeCast Int16 Double Source #

Unsafe signed integer promotion to floating point values.

Instance details

Defined in Copilot.Language.Operators.Cast

UnsafeCast Int16 Float Source #

Unsafe signed integer promotion to floating point values.

Instance details

Defined in Copilot.Language.Operators.Cast

UnsafeCast Int16 Int8 Source #

Unsafe downcasting to smaller sizes.

Instance details

Defined in Copilot.Language.Operators.Cast

UnsafeCast Int16 Word16 Source #

Signed to unsigned casting.

Instance details

Defined in Copilot.Language.Operators.Cast

UnsafeCast Int32 Int16 Source #

Unsafe downcasting to smaller sizes.

Instance details

Defined in Copilot.Language.Operators.Cast

UnsafeCast Int64 Int16 Source #

Unsafe downcasting to smaller sizes.

Instance details

Defined in Copilot.Language.Operators.Cast

UnsafeCast Word16 Int16 Source #

Cast from unsigned numbers to signed numbers.

Instance details

Defined in Copilot.Language.Operators.Cast

Cast Bool Int16 Source #

Cast a boolean stream to a stream of numbers, producing 1 if the value at a point in time is True, and 0 otherwise.

Instance details

Defined in Copilot.Language.Operators.Cast

Cast Int8 Int16 Source #

Cast number to bigger type.

Instance details

Defined in Copilot.Language.Operators.Cast

Cast Int16 Int16 Source #

Identity casting.

Instance details

Defined in Copilot.Language.Operators.Cast

Cast Int16 Int32 Source #

Cast number to bigger type.

Instance details

Defined in Copilot.Language.Operators.Cast

Cast Int16 Int64 Source #

Cast number to bigger type.

Instance details

Defined in Copilot.Language.Operators.Cast

Cast Word8 Int16 Source #

Cast number to bigger type.

Instance details

Defined in Copilot.Language.Operators.Cast

data Int32 #

32-bit signed integer type

Instances

Instances details
Bounded Int32

Since: base-2.1

Instance details

Defined in GHC.Int

Enum Int32

Since: base-2.1

Instance details

Defined in GHC.Int

Eq Int32

Since: base-2.1

Instance details

Defined in GHC.Int

Methods

(==) :: Int32 -> Int32 -> Bool #

(/=) :: Int32 -> Int32 -> Bool #

Integral Int32

Since: base-2.1

Instance details

Defined in GHC.Int

Num Int32

Since: base-2.1

Instance details

Defined in GHC.Int

Ord Int32

Since: base-2.1

Instance details

Defined in GHC.Int

Methods

compare :: Int32 -> Int32 -> Ordering #

(<) :: Int32 -> Int32 -> Bool #

(<=) :: Int32 -> Int32 -> Bool #

(>) :: Int32 -> Int32 -> Bool #

(>=) :: Int32 -> Int32 -> Bool #

max :: Int32 -> Int32 -> Int32 #

min :: Int32 -> Int32 -> Int32 #

Read Int32

Since: base-2.1

Instance details

Defined in GHC.Int

Real Int32

Since: base-2.1

Instance details

Defined in GHC.Int

Methods

toRational :: Int32 -> Rational #

Show Int32

Since: base-2.1

Instance details

Defined in GHC.Int

Methods

showsPrec :: Int -> Int32 -> ShowS #

show :: Int32 -> String #

showList :: [Int32] -> ShowS #

Ix Int32

Since: base-2.1

Instance details

Defined in GHC.Int

Bits Int32

Since: base-2.1

Instance details

Defined in GHC.Int

FiniteBits Int32

Since: base-4.6.0.0

Instance details

Defined in GHC.Int

Typed Int32 
Instance details

Defined in Copilot.Core.Type

UnsafeCast Int32 Double Source #

Unsafe signed integer promotion to floating point values.

Instance details

Defined in Copilot.Language.Operators.Cast

UnsafeCast Int32 Float Source #

Unsafe signed integer promotion to floating point values.

Instance details

Defined in Copilot.Language.Operators.Cast

UnsafeCast Int32 Int8 Source #

Unsafe downcasting to smaller sizes.

Instance details

Defined in Copilot.Language.Operators.Cast

UnsafeCast Int32 Int16 Source #

Unsafe downcasting to smaller sizes.

Instance details

Defined in Copilot.Language.Operators.Cast

UnsafeCast Int32 Word32 Source #

Signed to unsigned casting.

Instance details

Defined in Copilot.Language.Operators.Cast

UnsafeCast Int64 Int32 Source #

Unsafe downcasting to smaller sizes.

Instance details

Defined in Copilot.Language.Operators.Cast

UnsafeCast Word32 Int32 Source #

Cast from unsigned numbers to signed numbers.

Instance details

Defined in Copilot.Language.Operators.Cast

Cast Bool Int32 Source #

Cast a boolean stream to a stream of numbers, producing 1 if the value at a point in time is True, and 0 otherwise.

Instance details

Defined in Copilot.Language.Operators.Cast

Cast Int8 Int32 Source #

Cast number to bigger type.

Instance details

Defined in Copilot.Language.Operators.Cast

Cast Int16 Int32 Source #

Cast number to bigger type.

Instance details

Defined in Copilot.Language.Operators.Cast

Cast Int32 Int32 Source #

Identity casting.

Instance details

Defined in Copilot.Language.Operators.Cast

Cast Int32 Int64 Source #

Cast number to bigger type.

Instance details

Defined in Copilot.Language.Operators.Cast

Cast Word8 Int32 Source #

Cast number to bigger type.

Instance details

Defined in Copilot.Language.Operators.Cast

Cast Word16 Int32 Source #

Cast number to bigger type.

Instance details

Defined in Copilot.Language.Operators.Cast

data Int64 #

64-bit signed integer type

Instances

Instances details
Bounded Int64

Since: base-2.1

Instance details

Defined in GHC.Int

Enum Int64

Since: base-2.1

Instance details

Defined in GHC.Int

Eq Int64

Since: base-2.1

Instance details

Defined in GHC.Int

Methods

(==) :: Int64 -> Int64 -> Bool #

(/=) :: Int64 -> Int64 -> Bool #

Integral Int64

Since: base-2.1

Instance details

Defined in GHC.Int

Num Int64

Since: base-2.1

Instance details

Defined in GHC.Int

Ord Int64

Since: base-2.1

Instance details

Defined in GHC.Int

Methods

compare :: Int64 -> Int64 -> Ordering #

(<) :: Int64 -> Int64 -> Bool #

(<=) :: Int64 -> Int64 -> Bool #

(>) :: Int64 -> Int64 -> Bool #

(>=) :: Int64 -> Int64 -> Bool #

max :: Int64 -> Int64 -> Int64 #

min :: Int64 -> Int64 -> Int64 #

Read Int64

Since: base-2.1

Instance details

Defined in GHC.Int

Real Int64

Since: base-2.1

Instance details

Defined in GHC.Int

Methods

toRational :: Int64 -> Rational #

Show Int64

Since: base-2.1

Instance details

Defined in GHC.Int

Methods

showsPrec :: Int -> Int64 -> ShowS #

show :: Int64 -> String #

showList :: [Int64] -> ShowS #

Ix Int64

Since: base-2.1

Instance details

Defined in GHC.Int

Bits Int64

Since: base-2.1

Instance details

Defined in GHC.Int

FiniteBits Int64

Since: base-4.6.0.0

Instance details

Defined in GHC.Int

Typed Int64 
Instance details

Defined in Copilot.Core.Type

UnsafeCast Int64 Double Source #

Unsafe signed integer promotion to floating point values.

Instance details

Defined in Copilot.Language.Operators.Cast

UnsafeCast Int64 Float Source #

Unsafe signed integer promotion to floating point values.

Instance details

Defined in Copilot.Language.Operators.Cast

UnsafeCast Int64 Int8 Source #

Unsafe downcasting to smaller sizes.

Instance details

Defined in Copilot.Language.Operators.Cast

UnsafeCast Int64 Int16 Source #

Unsafe downcasting to smaller sizes.

Instance details

Defined in Copilot.Language.Operators.Cast

UnsafeCast Int64 Int32 Source #

Unsafe downcasting to smaller sizes.

Instance details

Defined in Copilot.Language.Operators.Cast

UnsafeCast Int64 Word64 Source #

Signed to unsigned casting.

Instance details

Defined in Copilot.Language.Operators.Cast

UnsafeCast Word64 Int64 Source #

Cast from unsigned numbers to signed numbers.

Instance details

Defined in Copilot.Language.Operators.Cast

Cast Bool Int64 Source #

Cast a boolean stream to a stream of numbers, producing 1 if the value at a point in time is True, and 0 otherwise.

Instance details

Defined in Copilot.Language.Operators.Cast

Cast Int8 Int64 Source #

Cast number to bigger type.

Instance details

Defined in Copilot.Language.Operators.Cast

Cast Int16 Int64 Source #

Cast number to bigger type.

Instance details

Defined in Copilot.Language.Operators.Cast

Cast Int32 Int64 Source #

Cast number to bigger type.

Instance details

Defined in Copilot.Language.Operators.Cast

Cast Int64 Int64 Source #

Identity casting.

Instance details

Defined in Copilot.Language.Operators.Cast

Cast Word8 Int64 Source #

Cast number to bigger type.

Instance details

Defined in Copilot.Language.Operators.Cast

Cast Word16 Int64 Source #

Cast number to bigger type.

Instance details

Defined in Copilot.Language.Operators.Cast

Cast Word32 Int64 Source #

Cast number to bigger type.

Instance details

Defined in Copilot.Language.Operators.Cast

module Data.Word

type Name = String #

A name of a trigger, an external variable, or an external function.

class (Show a, Typeable a) => Typed a #

A typed expression, from which we can obtain the two type representations used by Copilot: Type and SimpleType.

Minimal complete definition

typeOf

Instances

Instances details
Typed Bool 
Instance details

Defined in Copilot.Core.Type

Typed Double 
Instance details

Defined in Copilot.Core.Type

Typed Float 
Instance details

Defined in Copilot.Core.Type

Typed Int8 
Instance details

Defined in Copilot.Core.Type

Typed Int16 
Instance details

Defined in Copilot.Core.Type

Typed Int32 
Instance details

Defined in Copilot.Core.Type

Typed Int64 
Instance details

Defined in Copilot.Core.Type

Typed Word8 
Instance details

Defined in Copilot.Core.Type

Typed Word16 
Instance details

Defined in Copilot.Core.Type

Typed Word32 
Instance details

Defined in Copilot.Core.Type

Typed Word64 
Instance details

Defined in Copilot.Core.Type

(Typeable t, Typed t, KnownNat n, Flatten t (InnerType t), Typed (InnerType t)) => Typed (Array n t) 
Instance details

Defined in Copilot.Core.Type

Methods

typeOf :: Type (Array n t) #

simpleType :: Type (Array n t) -> SimpleType #

impossible Source #

Arguments

:: String

Name of the function in which the error was detected.

-> String

Name of the package in which the function is located.

-> a 

Report an error due to a bug in Copilot.

badUsage Source #

Arguments

:: String

Description of the error.

-> a 

Report an error due to an error detected by Copilot (e.g., user error).

csv :: Integer -> Spec -> IO () Source #

Simulate a number of steps of a given specification, printing the results in a table in comma-separated value (CSV) format.

interpret :: Integer -> Spec -> IO () Source #

Simulate a number of steps of a given specification, printing the results in a table in readable format.

Compared to csv, this function is slower but the output may be more readable.

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]

data Stream :: * -> * Source #

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

Streams can be built using simple primities (e.g., Const), by applying step-wise (e.g., Op1) or temporal transformations (e.g., Append, Drop) to streams, or by combining existing streams to form new streams (e.g., Op2, Op3).

Instances

Instances details
Eq (Stream a) Source #

Dummy instance in order to make Stream an instance of Num.

Instance details

Defined in Copilot.Language.Stream

Methods

(==) :: Stream a -> Stream a -> Bool #

(/=) :: Stream a -> Stream a -> Bool #

(Typed a, Eq a, Floating a) => Floating (Stream a) Source #

Streams carrying floating point numbers are instances of Floating, and you can apply to them the Floating functions, point-wise.

Instance details

Defined in Copilot.Language.Stream

Methods

pi :: Stream a #

exp :: Stream a -> Stream a #

log :: Stream a -> Stream a #

sqrt :: Stream a -> Stream a #

(**) :: Stream a -> Stream a -> Stream a #

logBase :: Stream a -> Stream a -> Stream a #

sin :: Stream a -> Stream a #

cos :: Stream a -> Stream a #

tan :: Stream a -> Stream a #

asin :: Stream a -> Stream a #

acos :: Stream a -> Stream a #

atan :: Stream a -> Stream a #

sinh :: Stream a -> Stream a #

cosh :: Stream a -> Stream a #

tanh :: Stream a -> Stream a #

asinh :: Stream a -> Stream a #

acosh :: Stream a -> Stream a #

atanh :: Stream a -> Stream a #

log1p :: Stream a -> Stream a #

expm1 :: Stream a -> Stream a #

log1pexp :: Stream a -> Stream a #

log1mexp :: Stream a -> Stream a #

(Typed a, Eq a, Fractional a) => Fractional (Stream a) Source #

Streams carrying fractional numbers are instances of Fractional, and you can apply to them the Fractional functions, point-wise.

Instance details

Defined in Copilot.Language.Stream

Methods

(/) :: Stream a -> Stream a -> Stream a #

recip :: Stream a -> Stream a #

fromRational :: Rational -> Stream a #

(Typed a, Eq a, Num a) => Num (Stream a) Source #

Streams carrying numbers are instances of Num, and you can apply to them the Num functions, point-wise.

Instance details

Defined in Copilot.Language.Stream

Methods

(+) :: Stream a -> Stream a -> Stream a #

(-) :: Stream a -> Stream a -> Stream a #

(*) :: Stream a -> Stream a -> Stream a #

negate :: Stream a -> Stream a #

abs :: Stream a -> Stream a #

signum :: Stream a -> Stream a #

fromInteger :: Integer -> Stream a #

Show (Stream a) Source #

Dummy instance in order to make Stream an instance of Num.

Instance details

Defined in Copilot.Language.Stream

Methods

showsPrec :: Int -> Stream a -> ShowS #

show :: Stream a -> String #

showList :: [Stream a] -> ShowS #

(Typed a, Bits a) => Bits (Stream a) Source #

Instance of the Bits class for Streams.

Only the methods .&., complement, .|. and xor are defined.

Instance details

Defined in Copilot.Language.Operators.BitWise

Methods

(.&.) :: Stream a -> Stream a -> Stream a #

(.|.) :: Stream a -> Stream a -> Stream a #

xor :: Stream a -> Stream a -> Stream a #

complement :: Stream a -> Stream a #

shift :: Stream a -> Int -> Stream a #

rotate :: Stream a -> Int -> Stream a #

zeroBits :: Stream a #

bit :: Int -> Stream a #

setBit :: Stream a -> Int -> Stream a #

clearBit :: Stream a -> Int -> Stream a #

complementBit :: Stream a -> Int -> Stream a #

testBit :: Stream a -> Int -> Bool #

bitSizeMaybe :: Stream a -> Maybe Int #

bitSize :: Stream a -> Int #

isSigned :: Stream a -> Bool #

shiftL :: Stream a -> Int -> Stream a #

unsafeShiftL :: Stream a -> Int -> Stream a #

shiftR :: Stream a -> Int -> Stream a #

unsafeShiftR :: Stream a -> Int -> Stream a #

rotateL :: Stream a -> Int -> Stream a #

rotateR :: Stream a -> Int -> Stream a #

popCount :: Stream a -> Int #

observer Source #

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.

trigger Source #

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.

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.

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.

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.

forall :: Stream Bool -> Prop Universal Source #

Universal quantification of boolean streams over time.

exists :: Stream Bool -> Prop Existential Source #

Existential quantification of boolean streams over time.

prettyPrint :: Spec -> IO () Source #

Transform a high-level Copilot Language specification into a low-level Copilot Core specification and pretty-print it to stdout.