| Copyright | (c) Levent Erkok |
|---|---|
| License | BSD3 |
| Maintainer | erkokl@gmail.com |
| Stability | experimental |
| Safe Haskell | None |
| Language | Haskell2010 |
Data.SBV.Tools.BMC
Description
Bounded model checking interface. See Documentation.SBV.Examples.ProofTools.BMC for an example use case.
Synopsis
- bmc :: (EqSymbolic st, Queriable IO st res) => Maybe Int -> Bool -> Symbolic () -> (st -> SBool) -> (st -> [st]) -> (st -> SBool) -> IO (Either String (Int, [res]))
- bmcWith :: (EqSymbolic st, Queriable IO st res) => SMTConfig -> Maybe Int -> Bool -> Symbolic () -> (st -> SBool) -> (st -> [st]) -> (st -> SBool) -> IO (Either String (Int, [res]))
Documentation
Arguments
| :: (EqSymbolic st, Queriable IO st res) | |
| => Maybe Int | Optional bound |
| -> Bool | Verbose: prints iteration count |
| -> Symbolic () | Setup code, if necessary. (Typically used for |
| -> (st -> SBool) | Initial condition |
| -> (st -> [st]) | Transition relation |
| -> (st -> SBool) | Goal to cover, i.e., we find a set of transitions that satisfy this predicate. |
| -> IO (Either String (Int, [res])) | Either a result, or a satisfying path of given length and intermediate observations. |
Bounded model checking, using the default solver. See Documentation.SBV.Examples.ProofTools.BMC for an example use case.
Note that the BMC engine does *not* guarantee that the solution is unique. However, if it does
find a solution at depth i, it is guaranteed that there are no shorter solutions.