-----------------------------------------------------------------------------
-- |
-- 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 { S a -> a
x :: a, S a -> a
y :: a }
         deriving (a -> S b -> S a
(a -> b) -> S a -> S b
(forall a b. (a -> b) -> S a -> S b)
-> (forall a b. a -> S b -> S a) -> Functor S
forall a b. a -> S b -> S a
forall a b. (a -> b) -> S a -> S b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: a -> S b -> S a
$c<$ :: forall a b. a -> S b -> S a
fmap :: (a -> b) -> S a -> S b
$cfmap :: forall a b. (a -> b) -> S a -> S b
Functor, S a -> Bool
(a -> m) -> S a -> m
(a -> b -> b) -> b -> S a -> b
(forall m. Monoid m => S m -> m)
-> (forall m a. Monoid m => (a -> m) -> S a -> m)
-> (forall m a. Monoid m => (a -> m) -> S a -> m)
-> (forall a b. (a -> b -> b) -> b -> S a -> b)
-> (forall a b. (a -> b -> b) -> b -> S a -> b)
-> (forall b a. (b -> a -> b) -> b -> S a -> b)
-> (forall b a. (b -> a -> b) -> b -> S a -> b)
-> (forall a. (a -> a -> a) -> S a -> a)
-> (forall a. (a -> a -> a) -> S a -> a)
-> (forall a. S a -> [a])
-> (forall a. S a -> Bool)
-> (forall a. S a -> Int)
-> (forall a. Eq a => a -> S a -> Bool)
-> (forall a. Ord a => S a -> a)
-> (forall a. Ord a => S a -> a)
-> (forall a. Num a => S a -> a)
-> (forall a. Num a => S a -> a)
-> Foldable S
forall a. Eq a => a -> S a -> Bool
forall a. Num a => S a -> a
forall a. Ord a => S a -> a
forall m. Monoid m => S m -> m
forall a. S a -> Bool
forall a. S a -> Int
forall a. S a -> [a]
forall a. (a -> a -> a) -> S a -> a
forall m a. Monoid m => (a -> m) -> S a -> m
forall b a. (b -> a -> b) -> b -> S a -> b
forall a b. (a -> b -> b) -> b -> S a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
product :: S a -> a
$cproduct :: forall a. Num a => S a -> a
sum :: S a -> a
$csum :: forall a. Num a => S a -> a
minimum :: S a -> a
$cminimum :: forall a. Ord a => S a -> a
maximum :: S a -> a
$cmaximum :: forall a. Ord a => S a -> a
elem :: a -> S a -> Bool
$celem :: forall a. Eq a => a -> S a -> Bool
length :: S a -> Int
$clength :: forall a. S a -> Int
null :: S a -> Bool
$cnull :: forall a. S a -> Bool
toList :: S a -> [a]
$ctoList :: forall a. S a -> [a]
foldl1 :: (a -> a -> a) -> S a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> S a -> a
foldr1 :: (a -> a -> a) -> S a -> a
$cfoldr1 :: forall a. (a -> a -> a) -> S a -> a
foldl' :: (b -> a -> b) -> b -> S a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> S a -> b
foldl :: (b -> a -> b) -> b -> S a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> S a -> b
foldr' :: (a -> b -> b) -> b -> S a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> S a -> b
foldr :: (a -> b -> b) -> b -> S a -> b
$cfoldr :: forall a b. (a -> b -> b) -> b -> S a -> b
foldMap' :: (a -> m) -> S a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> S a -> m
foldMap :: (a -> m) -> S a -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> S a -> m
fold :: S m -> m
$cfold :: forall m. Monoid m => S m -> m
Foldable, Functor S
Foldable S
Functor S
-> Foldable S
-> (forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> S a -> f (S b))
-> (forall (f :: * -> *) a. Applicative f => S (f a) -> f (S a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> S a -> m (S b))
-> (forall (m :: * -> *) a. Monad m => S (m a) -> m (S a))
-> Traversable S
(a -> f b) -> S a -> f (S b)
forall (t :: * -> *).
Functor t
-> Foldable t
-> (forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> t a -> f (t b))
-> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> t a -> m (t b))
-> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall (m :: * -> *) a. Monad m => S (m a) -> m (S a)
forall (f :: * -> *) a. Applicative f => S (f a) -> f (S a)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> S a -> m (S b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> S a -> f (S b)
sequence :: S (m a) -> m (S a)
$csequence :: forall (m :: * -> *) a. Monad m => S (m a) -> m (S a)
mapM :: (a -> m b) -> S a -> m (S b)
$cmapM :: forall (m :: * -> *) a b. Monad m => (a -> m b) -> S a -> m (S b)
sequenceA :: S (f a) -> f (S a)
$csequenceA :: forall (f :: * -> *) a. Applicative f => S (f a) -> f (S a)
traverse :: (a -> f b) -> S a -> f (S b)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> S a -> f (S b)
$cp2Traversable :: Foldable S
$cp1Traversable :: Functor S
Traversable)

-- | Show the state as a pair
instance Show a => Show (S a) where
  show :: S a -> String
show S{a
x :: a
x :: forall a. S a -> a
x, a
y :: a
y :: forall a. S a -> a
y} = (a, a) -> String
forall a. Show a => a -> String
show (a
x, a
y)

-- | Symbolic equality for @S@.
instance EqSymbolic a => EqSymbolic (S a) where
   S {x :: forall a. S a -> a
x = a
x1, y :: forall a. S a -> a
y = a
y1} .== :: S a -> S a -> SBool
.== S {x :: forall a. S a -> a
x = a
x2, y :: forall a. S a -> a
y = a
y2} = a
x1 a -> a -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== a
x2 SBool -> SBool -> SBool
.&& a
y1 a -> a -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== a
y2

-- | 'Fresh' instance for our state
instance Fresh IO (S SInteger) where
  fresh :: QueryT IO (S SInteger)
fresh = SInteger -> SInteger -> S SInteger
forall a. a -> a -> S a
S (SInteger -> SInteger -> S SInteger)
-> QueryT IO SInteger -> QueryT IO (SInteger -> S SInteger)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QueryT IO SInteger
forall a. SymVal a => Query (SBV a)
freshVar_ QueryT IO (SInteger -> S SInteger)
-> QueryT IO SInteger -> QueryT IO (S SInteger)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> QueryT IO SInteger
forall a. SymVal a => Query (SBV a)
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 :: Int
-> (S SInteger -> SBool) -> IO (Either String (Int, [S Integer]))
problem Int
lim S SInteger -> SBool
initial = Maybe Int
-> Bool
-> Symbolic ()
-> (S SInteger -> SBool)
-> (S SInteger -> [S SInteger])
-> (S SInteger -> SBool)
-> IO (Either String (Int, [S Integer]))
forall st res.
(EqSymbolic st, Queriable IO st res) =>
Maybe Int
-> Bool
-> Symbolic ()
-> (st -> SBool)
-> (st -> [st])
-> (st -> SBool)
-> IO (Either String (Int, [res]))
bmc (Int -> Maybe Int
forall a. a -> Maybe a
Just Int
lim) Bool
True Symbolic ()
setup S SInteger -> SBool
initial S SInteger -> [S SInteger]
trans S SInteger -> SBool
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 :: Symbolic ()
setup = () -> Symbolic ()
forall (m :: * -> *) a. Monad m => a -> m a
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 SInteger -> [S SInteger]
trans S{SInteger
x :: SInteger
x :: forall a. S a -> a
x, SInteger
y :: SInteger
y :: forall a. S a -> a
y} = [ S :: forall a. a -> a -> S a
S { x :: SInteger
x = SInteger
x SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
2, y :: SInteger
y = SInteger
y     }
                        , S :: forall a. a -> a -> S a
S { x :: SInteger
x = SInteger
x,     y :: SInteger
y = SInteger
y SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
- SInteger
4 }
                        ]

        -- Goal state is when @x@ equals @y@:
        goal :: S SInteger -> SBool
        goal :: S SInteger -> SBool
goal S{SInteger
x :: SInteger
x :: forall a. S a -> a
x, SInteger
y :: SInteger
y :: forall a. S a -> a
y} = SInteger
x SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
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),(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.)
ex1 :: IO (Either String (Int, [S Integer]))
ex1 :: IO (Either String (Int, [S Integer]))
ex1 = Int
-> (S SInteger -> SBool) -> IO (Either String (Int, [S Integer]))
problem Int
10 S SInteger -> SBool
isInitial
  where isInitial :: S SInteger -> SBool
        isInitial :: S SInteger -> SBool
isInitial S{SInteger
x :: SInteger
x :: forall a. S a -> a
x, SInteger
y :: SInteger
y :: forall a. S a -> a
y} = SInteger
x SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
0 SBool -> SBool -> SBool
.&& SInteger
y SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
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 :: IO (Either String (Int, [S Integer]))
ex2 = Int
-> (S SInteger -> SBool) -> IO (Either String (Int, [S Integer]))
problem Int
10 S SInteger -> SBool
isInitial
  where isInitial :: S SInteger -> SBool
        isInitial :: S SInteger -> SBool
isInitial S{SInteger
x :: SInteger
x :: forall a. S a -> a
x, SInteger
y :: SInteger
y :: forall a. S a -> a
y} = SInteger
x SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
0 SBool -> SBool -> SBool
.&& SInteger
y SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
11