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:

`>>>`

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)])`ex1`

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:

`>>>`

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"`ex2`

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.