Copyright  (c) Levent Erkok 

License  BSD3 
Maintainer  erkokl@gmail.com 
Stability  experimental 
Safe Haskell  None 
Language  Haskell2010 
A BMC example, showing how traditional statetransition 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 fold :: Monoid m => S m > 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 #  
Fresh IO (S SInteger) Source # 

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 (.==) :: 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 # 
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:
>>>
ex1
BMC: Iteration: 0 BMC: Iteration: 1 BMC: Iteration: 2 BMC: Iteration: 3 BMC: Solution found at iteration 3 Right (3,[(0,10),(2,10),(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:
>>>
ex2
BMC: Iteration: 0 BMC: Iteration: 1 BMC: Iteration: 2 BMC: Iteration: 3 BMC: Iteration: 4 BMC: Iteration: 5 BMC: Iteration: 6 BMC: Iteration: 7 BMC: Iteration: 8 BMC: Iteration: 9 Left "BMC limit of 10 reached"
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.