| Copyright | (c) Levent Erkok |
|---|---|
| License | BSD3 |
| Maintainer | erkokl@gmail.com |
| Stability | experimental |
| Safe Haskell | None |
| Language | Haskell2010 |
Documentation.SBV.Examples.ProofTools.BMC
Description
A BMC example, showing how traditional state-transition reachability problems can be coded using SBV, using bounded model checking.
We imagine a system with two integer variables, x and y. At each
iteration, we can either increment x by 2, or decrement y by 4.
Can we reach a state where x and y are the same starting from x=0
and y=10?
What if y starts at 11?
System state
System state, containing the two integers.
Instances
| Functor S Source # | |||||
| Foldable S Source # | |||||
Defined in Documentation.SBV.Examples.ProofTools.BMC Methods fold :: Monoid m => S m -> m # foldMap :: Monoid m => (a -> m) -> S a -> m # foldMap' :: Monoid m => (a -> m) -> S a -> m # foldr :: (a -> b -> b) -> b -> S a -> b # foldr' :: (a -> b -> b) -> b -> S a -> b # foldl :: (b -> a -> b) -> b -> S a -> b # foldl' :: (b -> a -> b) -> b -> S a -> b # foldr1 :: (a -> a -> a) -> S a -> a # foldl1 :: (a -> a -> a) -> S a -> a # elem :: Eq a => a -> S a -> Bool # maximum :: Ord a => S a -> a # | |||||
| Traversable S Source # | |||||
| Queriable IO (S SInteger) Source # | 'Queriable instance for our state | ||||
Defined in Documentation.SBV.Examples.ProofTools.BMC Associated Types
| |||||
| Show a => Show (S a) Source # | Show the state as a pair | ||||
| EqSymbolic a => EqSymbolic (S a) Source # | Symbolic equality for | ||||
Defined in Documentation.SBV.Examples.ProofTools.BMC Methods (.==) :: S a -> S a -> SBool Source # (./=) :: S a -> S a -> SBool Source # (.===) :: S a -> S a -> SBool Source # (./==) :: S a -> S a -> SBool Source # distinct :: [S a] -> SBool Source # distinctExcept :: [S a] -> [S a] -> SBool Source # allEqual :: [S a] -> SBool Source # | |||||
| type QueryResult (S SInteger) Source # | |||||
Defined in Documentation.SBV.Examples.ProofTools.BMC | |||||
Encoding the problem
problem :: Int -> (S SInteger -> SBool) -> IO (Either String (Int, [S Integer])) Source #
We parameterize over the initial state for different variations.
Examples
ex1 :: IO (Either String (Int, [S Integer])) Source #
Example 1: We start from x=0, y=10, and search up to depth 10. We have:
>>>ex1BMC Cover: Iteration: 0 BMC Cover: Iteration: 1 BMC Cover: Iteration: 2 BMC Cover: Iteration: 3 BMC Cover: Satisfying state found at iteration 3 Right (3,[(0,10),(0,6),(2,6),(2,2)])
As expected, there's a solution in this case. Furthermore, since the BMC engine
found a solution at depth 3, we also know that there is no solution at
depths 0, 1, or 2; i.e., this is "a" shortest solution. (That is,
it may not be unique, but there isn't a shorter sequence to get us to
our goal.)
ex2 :: IO (Either String (Int, [S Integer])) Source #
Example 2: We start from x=0, y=11, and search up to depth 10. We have:
>>>ex2BMC Cover: Iteration: 0 BMC Cover: Iteration: 1 BMC Cover: Iteration: 2 BMC Cover: Iteration: 3 BMC Cover: Iteration: 4 BMC Cover: Iteration: 5 BMC Cover: Iteration: 6 BMC Cover: Iteration: 7 BMC Cover: Iteration: 8 BMC Cover: Iteration: 9 Left "BMC Cover limit of 10 reached. Cover can't be established."
As expected, there's no solution in this case. While SBV (and BMC) cannot establish
that there is no solution at a larger depth, you can see that this will never be the
case: In each step we do not change the parity of either variable. That is, x
will remain even, and y will remain odd. So, there will never be a solution at
any depth. This isn't the only way to see this result of course, but the point
remains that BMC is just not capable of establishing inductive facts.