| 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
- bmcRefute :: (Queriable IO st, res ~ QueryResult st) => Maybe Int -> Bool -> Symbolic () -> (st -> SBool) -> (st -> st -> SBool) -> (st -> SBool) -> IO (Either String (Int, [res]))
- bmcRefuteWith :: (Queriable IO st, res ~ QueryResult st) => SMTConfig -> Maybe Int -> Bool -> Symbolic () -> (st -> SBool) -> (st -> st -> SBool) -> (st -> SBool) -> IO (Either String (Int, [res]))
- bmcCover :: (Queriable IO st, res ~ QueryResult st) => Maybe Int -> Bool -> Symbolic () -> (st -> SBool) -> (st -> st -> SBool) -> (st -> SBool) -> IO (Either String (Int, [res]))
- bmcCoverWith :: (Queriable IO st, res ~ QueryResult st) => SMTConfig -> Maybe Int -> Bool -> Symbolic () -> (st -> SBool) -> (st -> st -> SBool) -> (st -> SBool) -> IO (Either String (Int, [res]))
Documentation
Arguments
| :: (Queriable IO st, res ~ QueryResult st) | |
| => Maybe Int | Optional bound |
| -> Bool | Verbose: prints iteration count |
| -> Symbolic () | Setup code, if necessary. (Typically used for |
| -> (st -> SBool) | Initial condition |
| -> (st -> st -> SBool) | 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. |
Refutation using bounded model checking, using the default solver. This version tries to refute the goal in a depth-first fashion. Note that this method can find a refutation, but will never find a "proof." If it finds a refutation, it will be the shortest, though not necessarily unique.
Arguments
| :: (Queriable IO st, res ~ QueryResult st) | |
| => SMTConfig | Solver to use |
| -> Maybe Int | Optional bound |
| -> Bool | Verbose: prints iteration count |
| -> Symbolic () | Setup code, if necessary. (Typically used for |
| -> (st -> SBool) | Initial condition |
| -> (st -> st -> SBool) | 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. |
Refutation using a given solver.
Arguments
| :: (Queriable IO st, res ~ QueryResult st) | |
| => Maybe Int | Optional bound |
| -> Bool | Verbose: prints iteration count |
| -> Symbolic () | Setup code, if necessary. (Typically used for |
| -> (st -> SBool) | Initial condition |
| -> (st -> st -> SBool) | 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. |
Covers using bounded model checking, using the default solver. This version tries to cover the goal in a depth-first fashion. Note that this method can find a cover, but will never find determine that a goal is not coverable. If it finds a cover, it will be the shortest, though not necessarily unique.
Arguments
| :: (Queriable IO st, res ~ QueryResult st) | |
| => SMTConfig | Solver to use |
| -> Maybe Int | Optional bound |
| -> Bool | Verbose: prints iteration count |
| -> Symbolic () | Setup code, if necessary. (Typically used for |
| -> (st -> SBool) | Initial condition |
| -> (st -> st -> SBool) | 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. |
Cover using a given solver.