Safe Haskell	Safe
Language	Haskell2010

Copilot.Theorem.Kind2

Description

Copilot backend for the Kind 2 SMT based model checker.

Synopsis

module Copilot.Theorem.Kind2.Prover
data Term
- = ValueLiteral String
- | PrimedStateVar String
- | StateVar String
- | FunApp String [Term]
- | PredApp String PredType [Term]
data Type
- = Int
- | Real
- | Bool
prettyPrint :: File -> String
data File = File {
- filePreds :: [PredDef]
- fileProps :: [Prop]
}
toKind2 :: Style -> [PropId] -> [PropId] -> TransSys -> File
data Style
- = Inlined
- | Modular
data PredType
- = Init
- | Trans
data StateVarDef = StateVarDef {
- varId :: String
- varType :: Type
- varFlags :: [StateVarFlag]
}
data Prop = Prop {
- propName :: String
- propTerm :: Term
}
data PredDef = PredDef {
- predId :: String
- predStateVars :: [StateVarDef]
- predInit :: Term
- predTrans :: Term
}
data StateVarFlag = FConst

Documentation

module Copilot.Theorem.Kind2.Prover

data Term Source #

Datatype to describe a term in the Kind language.

Constructors

ValueLiteral String
PrimedStateVar String
StateVar String
FunApp String [Term]
PredApp String PredType [Term]

data Type Source #

Types used in Kind2 files to represent Copilot types.

The Kind2 backend provides functions to, additionally, constrain the range of numeric values depending on their Copilot type (Int8, Int16, etc.).

Constructors

Int
Real
Bool

prettyPrint :: File -> String Source #

Pretty print a Kind2 file.

data File Source #

A file is a sequence of predicates and propositions.

Constructors

File
Fields filePreds :: [PredDef] fileProps :: [Prop]

toKind2 Source #

Arguments

:: Style	Style of the file (modular or inlined).
-> [PropId]	Assumptions
-> [PropId]	Properties to be checked
-> TransSys	Modular transition system holding the system spec
-> File

Produce a Kind2 file that checks the properties specified.

data Style Source #

Style of the Kind2 files produced: modular (with multiple separate nodes), or all inlined (with only one node).

In the modular style, the graph is simplified to remove cycles by collapsing all nodes participating in a strongly connected components.

In the inlined style, the structure of the modular transition system is discarded and the graph is first turned into a non-modular transition system with only one node, which can be then converted into a Kind2 file.

Constructors

Inlined
Modular

data PredType Source #

Type of the predicate, either belonging to an initial state or a pair of states with a transition.

Constructors

Init
Trans

data StateVarDef Source #

A definition of a state variable.

Constructors

StateVarDef
Fields varId :: String Name of the variable. varType :: Type Type of the variable. varFlags :: [StateVarFlag] Flags for the variable.

data Prop Source #

A proposition is defined by a term.

Constructors

Prop
Fields propName :: String propTerm :: Term

data PredDef Source #

A predicate definition.

Constructors

PredDef
Fields predId :: String Identifier for the predicate. predStateVars :: [StateVarDef] Variables identifying the states in the underlying state transition system. predInit :: Term Predicate that holds for initial states. predTrans :: Term Predicate that holds for two states, if there is state transition between them.

data StateVarFlag Source #

Possible flags for a state variable.

Constructors

FConst