copilot-theorem-3.3: k-induction for Copilot.
Safe HaskellSafe
LanguageHaskell2010

Copilot.Theorem.Kind2

Description

Copilot backend for the Kind 2 SMT based model checker.

Synopsis

Documentation

prettyPrint :: File -> String Source #

Pretty print a Kind2 file.

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 File Source #

A file is a sequence of predicates and propositions.

Constructors

File 

Fields

data Prop Source #

A proposition is defined by a term.

Constructors

Prop 

Fields

data PredDef Source #

A predicate definition.

Constructors

PredDef 

Fields

data StateVarDef Source #

A definition of a state variable.

Constructors

StateVarDef

Flags for the variable.

Fields

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 

data StateVarFlag Source #

Possible flags for a state variable.

Constructors

FConst 

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 Term Source #

Datatype to describe a term in the Kind language.