1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
|
-----------------------------------------------------------------------------
-- |
-- Module : Documentation.SBV.Examples.ProofTools.BMC
-- Copyright : (c) 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@?
-----------------------------------------------------------------------------
{-# LANGUAGE DeriveTraversable #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# OPTIONS_GHC -Wall -Werror #-}
module Documentation.SBV.Examples.ProofTools.BMC where
import Data.SBV
import Data.SBV.Tools.BMC
import Data.SBV.Control
-- * System state
-- | System state, containing the two integers.
data S a = S { x :: a, y :: a }
deriving (Functor, Foldable, Traversable)
-- | Show the state as a pair
instance Show a => Show (S a) where
show S{x, y} = show (x, y)
-- | Symbolic equality for @S@.
instance EqSymbolic a => EqSymbolic (S a) where
S {x = x1, y = y1} .== S {x = x2, y = y2} = x1 .== x2 .&& y1 .== y2
-- | 'Fresh' instance for our state
instance Fresh IO (S SInteger) where
fresh = S <$> freshVar_ <*> freshVar_
-- * Encoding the problem
-- | We parameterize over the initial state for different variations.
problem :: Int -> (S SInteger -> SBool) -> IO (Either String (Int, [S Integer]))
problem lim initial = bmc (Just lim) True setup initial trans goal
where
-- This is where we would put solver options, typically via
-- calls to 'Data.SBV.setOption'. We do not need any for this problem,
-- so we simply do nothing.
setup :: Symbolic ()
setup = return ()
-- Transition relation: At each step we either
-- get to increase @x@ by 2, or decrement @y@ by 4:
trans :: S SInteger -> [S SInteger]
trans S{x, y} = [ S { x = x + 2, y = y }
, S { x = x, y = y - 4 }
]
-- Goal state is when @x@ equals @y@:
goal :: S SInteger -> SBool
goal S{x, y} = x .== y
-- * Examples
-- | 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.)
ex1 :: IO (Either String (Int, [S Integer]))
ex1 = problem 10 isInitial
where isInitial :: S SInteger -> SBool
isInitial S{x, y} = x .== 0 .&& y .== 10
-- | 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.
ex2 :: IO (Either String (Int, [S Integer]))
ex2 = problem 10 isInitial
where isInitial :: S SInteger -> SBool
isInitial S{x, y} = x .== 0 .&& y .== 11
|
