| 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
- prettyPrint :: File -> String
- toKind2 :: Style -> [PropId] -> [PropId] -> TransSys -> File
- data Style
- data File = File {}
- data Prop = Prop {}
- data PredDef = PredDef {
- predId :: String
- predStateVars :: [StateVarDef]
- predInit :: Term
- predTrans :: Term
- data StateVarDef = StateVarDef {}
- data Type
- data StateVarFlag = FConst
- data PredType
- data Term
Documentation
module Copilot.Theorem.Kind2.Prover
prettyPrint :: File -> String Source #
Pretty print a Kind2 file.
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.
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.
A file is a sequence of predicates and propositions.
A proposition is defined by a term.
A predicate definition.
Constructors
| PredDef | |
Fields
| |
data StateVarDef Source #
A definition of a state variable.
Constructors
| StateVarDef | Flags for the variable. |
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.).
Type of the predicate, either belonging to an initial state or a pair of states with a transition.