Safe Haskell | None |
---|---|
Language | Haskell2010 |
Author : Levent Erkok License : BSD3 Maintainer: erkokl@gmail.com Stability : experimental
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.
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),(0,6),(0,2),(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.