-----------------------------------------------------------------------------
-- |
-- Module    : Documentation.SBV.Examples.Puzzles.DieHard
-- Copyright : (c) Levent Erkok
-- License   : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- Solves the die-hard riddle: In the movie Die Hard 3, the heroes must obtain
-- exactly 4 gallons of water using a 5 gallon jug, a 3 gallon jug, and a water faucet.
-- We use a bounded-model-checking style search to find a solution.
-----------------------------------------------------------------------------

{-# LANGUAGE DeriveAnyClass        #-}
{-# LANGUAGE DeriveDataTypeable    #-}
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE NamedFieldPuns        #-}
{-# LANGUAGE StandaloneDeriving    #-}
{-# LANGUAGE OverloadedRecordDot   #-}
{-# LANGUAGE TemplateHaskell       #-}
{-# LANGUAGE TypeFamilies          #-}

{-# OPTIONS_GHC -Wall -Werror #-}

module Documentation.SBV.Examples.Puzzles.DieHard where

import Data.SBV
import Data.SBV.Tools.BMC

-- | Possible actions
data Action = Initial | FillBig | FillSmall | EmptyBig | EmptySmall | BigToSmall | SmallToBig

mkSymbolicEnumeration ''Action

-- | We represent the state with two quantities, the amount of water in each jug. The
-- action is how we got into this state.
data State a b = State { forall a b. State a b -> a
big    :: a
                       , forall a b. State a b -> a
small  :: a
                       , forall a b. State a b -> b
action :: b
                       }

-- | Show instance
instance (Show a, Show b) => Show (State a b) where
  show :: State a b -> String
show State a b
s = String
"Big: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show State a b
s.big String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", Small: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show State a b
s.small String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" (" String -> ShowS
forall a. [a] -> [a] -> [a]
++ b -> String
forall a. Show a => a -> String
show State a b
s.action String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"

-- | Fully symbolic state
type SState = State SInteger SAction

-- | Fully concrete state
type CState = State Integer Action

-- | 'Queriable' instance needed for running bmc
instance Queriable IO SState where
  type QueryResult SState = CState

  create :: QueryT IO SState
create                = SInteger -> SInteger -> SBV Action -> SState
forall a b. a -> a -> b -> State a b
State (SInteger -> SInteger -> SBV Action -> SState)
-> QueryT IO SInteger
-> QueryT IO (SInteger -> SBV Action -> SState)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QueryT IO SInteger
forall a (m :: * -> *).
(MonadIO m, MonadQuery m, SymVal a) =>
m (SBV a)
freshVar_ QueryT IO (SInteger -> SBV Action -> SState)
-> QueryT IO SInteger -> QueryT IO (SBV Action -> SState)
forall a b. QueryT IO (a -> b) -> QueryT IO a -> QueryT IO b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> QueryT IO SInteger
forall a (m :: * -> *).
(MonadIO m, MonadQuery m, SymVal a) =>
m (SBV a)
freshVar_ QueryT IO (SBV Action -> SState)
-> QueryT IO (SBV Action) -> QueryT IO SState
forall a b. QueryT IO (a -> b) -> QueryT IO a -> QueryT IO b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> QueryT IO (SBV Action)
forall a (m :: * -> *).
(MonadIO m, MonadQuery m, SymVal a) =>
m (SBV a)
freshVar_
  project :: SState -> QueryT IO (QueryResult SState)
project (State SInteger
b SInteger
s SBV Action
a) = Integer -> Integer -> Action -> CState
forall a b. a -> a -> b -> State a b
State (Integer -> Integer -> Action -> CState)
-> QueryT IO Integer -> QueryT IO (Integer -> Action -> CState)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SInteger -> QueryT IO (QueryResult SInteger)
forall (m :: * -> *) a.
Queriable m a =>
a -> QueryT m (QueryResult a)
project SInteger
b QueryT IO (Integer -> Action -> CState)
-> QueryT IO Integer -> QueryT IO (Action -> CState)
forall a b. QueryT IO (a -> b) -> QueryT IO a -> QueryT IO b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SInteger -> QueryT IO (QueryResult SInteger)
forall (m :: * -> *) a.
Queriable m a =>
a -> QueryT m (QueryResult a)
project SInteger
s QueryT IO (Action -> CState)
-> QueryT IO Action -> QueryT IO CState
forall a b. QueryT IO (a -> b) -> QueryT IO a -> QueryT IO b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SBV Action -> QueryT IO (QueryResult (SBV Action))
forall (m :: * -> *) a.
Queriable m a =>
a -> QueryT m (QueryResult a)
project SBV Action
a
  embed :: QueryResult SState -> QueryT IO SState
embed   (State Integer
b Integer
s Action
a) = SInteger -> SInteger -> SBV Action -> SState
forall a b. a -> a -> b -> State a b
State (SInteger -> SInteger -> SBV Action -> SState)
-> QueryT IO SInteger
-> QueryT IO (SInteger -> SBV Action -> SState)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QueryResult SInteger -> QueryT IO SInteger
forall (m :: * -> *) a.
Queriable m a =>
QueryResult a -> QueryT m a
embed   Integer
QueryResult SInteger
b QueryT IO (SInteger -> SBV Action -> SState)
-> QueryT IO SInteger -> QueryT IO (SBV Action -> SState)
forall a b. QueryT IO (a -> b) -> QueryT IO a -> QueryT IO b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> QueryResult SInteger -> QueryT IO SInteger
forall (m :: * -> *) a.
Queriable m a =>
QueryResult a -> QueryT m a
embed   Integer
QueryResult SInteger
s QueryT IO (SBV Action -> SState)
-> QueryT IO (SBV Action) -> QueryT IO SState
forall a b. QueryT IO (a -> b) -> QueryT IO a -> QueryT IO b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> QueryResult (SBV Action) -> QueryT IO (SBV Action)
forall (m :: * -> *) a.
Queriable m a =>
QueryResult a -> QueryT m a
embed   QueryResult (SBV Action)
Action
a

-- | Solve the problem using a BMC search. We have:
--
-- >>> dieHard
-- BMC Cover: Iteration: 0
-- BMC Cover: Iteration: 1
-- BMC Cover: Iteration: 2
-- BMC Cover: Iteration: 3
-- BMC Cover: Iteration: 4
-- BMC Cover: Iteration: 5
-- BMC Cover: Iteration: 6
-- BMC Cover: Satisfying state found at iteration 6
-- Big: 0, Small: 0 (Initial)
-- Big: 5, Small: 0 (FillBig)
-- Big: 2, Small: 3 (BigToSmall)
-- Big: 2, Small: 0 (EmptySmall)
-- Big: 0, Small: 2 (BigToSmall)
-- Big: 5, Small: 2 (FillBig)
-- Big: 4, Small: 3 (BigToSmall)
dieHard :: IO ()
dieHard :: IO ()
dieHard = Either String (Int, [CState]) -> IO ()
display (Either String (Int, [CState]) -> IO ())
-> IO (Either String (Int, [CState])) -> IO ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Maybe Int
-> Bool
-> Symbolic ()
-> (SState -> SBool)
-> (SState -> SState -> SBool)
-> (SState -> SBool)
-> IO (Either String (Int, [CState]))
forall st res.
(Queriable IO st, res ~ QueryResult st) =>
Maybe Int
-> Bool
-> Symbolic ()
-> (st -> SBool)
-> (st -> st -> SBool)
-> (st -> SBool)
-> IO (Either String (Int, [res]))
bmcCover Maybe Int
forall a. Maybe a
Nothing Bool
True (() -> Symbolic ()
forall a. a -> SymbolicT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()) SState -> SBool
forall {b}. (EqSymbolic b, Num b) => State b (SBV Action) -> SBool
initial SState -> SState -> SBool
trans SState -> SBool
forall {a} {b}. (EqSymbolic a, Num a) => State a b -> SBool
goal
  where -- we start from empty jugs, and try to reach a state where big has 4 gallons
        initial :: State b (SBV Action) -> SBool
initial State{b
big :: forall a b. State a b -> a
big :: b
big, b
small :: forall a b. State a b -> a
small :: b
small, SBV Action
action :: forall a b. State a b -> b
action :: SBV Action
action} = (b
big, b
small, SBV Action
action) (b, b, SBV Action) -> (b, b, SBV Action) -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== (b
0, b
0, SBV Action
sInitial)
        goal :: State a b -> SBool
goal    State{a
big :: forall a b. State a b -> a
big :: a
big}                = a
big a -> a -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== a
4

        -- Valid actions as a transition relation:
        trans :: SState -> SState -> SBool
        trans :: SState -> SState -> SBool
trans SState
fromState SState
toState = [(SBV Action, SState -> SState)] -> SBool
go [(SBV Action, SState -> SState)]
forall {b}. [(SBV Action, State SInteger b -> State SInteger b)]
actions
          where go :: [(SBV Action, SState -> SState)] -> SBool
go []                = SBool
sFalse
                go ((SBV Action
act, SState -> SState
f) : [(SBV Action, SState -> SState)]
rest) = SBool -> SBool -> SBool -> SBool
forall a. Mergeable a => SBool -> a -> a -> a
ite (SState
toState.action SBV Action -> SBV Action -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Action
act) (SState -> SState
f SState
fromState SState -> SState -> SBool
`matches` SState
toState) ([(SBV Action, SState -> SState)] -> SBool
go [(SBV Action, SState -> SState)]
rest)

                matches :: SState -> SState -> SBool
                SState
p matches :: SState -> SState -> SBool
`matches` SState
q = SState
p.big SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SState
q.big SBool -> SBool -> SBool
.&& SState
p.small SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SState
q.small

                infix 1 |=>
                a
a |=> :: a -> b -> (a, b)
|=> b
f = (a
a, b
f)

                actions :: [(SBV Action, State SInteger b -> State SInteger b)]
actions = [ SBV Action
sFillBig    SBV Action
-> (State SInteger b -> State SInteger b)
-> (SBV Action, State SInteger b -> State SInteger b)
forall {a} {b}. a -> b -> (a, b)
|=> \State SInteger b
st -> State SInteger b
st{big   = 5}
                          , SBV Action
sFillSmall  SBV Action
-> (State SInteger b -> State SInteger b)
-> (SBV Action, State SInteger b -> State SInteger b)
forall {a} {b}. a -> b -> (a, b)
|=> \State SInteger b
st -> State SInteger b
st{small = 3}

                          , SBV Action
sEmptyBig   SBV Action
-> (State SInteger b -> State SInteger b)
-> (SBV Action, State SInteger b -> State SInteger b)
forall {a} {b}. a -> b -> (a, b)
|=> \State SInteger b
st -> State SInteger b
st{big   = 0}
                          , SBV Action
sEmptySmall SBV Action
-> (State SInteger b -> State SInteger b)
-> (SBV Action, State SInteger b -> State SInteger b)
forall {a} {b}. a -> b -> (a, b)
|=> \State SInteger b
st -> State SInteger b
st{small = 0}

                          , SBV Action
sBigToSmall SBV Action
-> (State SInteger b -> State SInteger b)
-> (SBV Action, State SInteger b -> State SInteger b)
forall {a} {b}. a -> b -> (a, b)
|=> \State SInteger b
st -> let space :: SInteger
space = SInteger
3 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
- State SInteger b
st.small
                                                       xfer :: SInteger
xfer  = SInteger
space SInteger -> SInteger -> SInteger
forall a. OrdSymbolic a => a -> a -> a
`smin` State SInteger b
st.big
                                                   in State SInteger b
st{big = st.big - xfer, small = st.small + xfer}

                          , SBV Action
sSmallToBig SBV Action
-> (State SInteger b -> State SInteger b)
-> (SBV Action, State SInteger b -> State SInteger b)
forall {a} {b}. a -> b -> (a, b)
|=> \State SInteger b
st -> let space :: SInteger
space = SInteger
5 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
- State SInteger b
st.big
                                                       xfer :: SInteger
xfer  = SInteger
space SInteger -> SInteger -> SInteger
forall a. OrdSymbolic a => a -> a -> a
`smin` State SInteger b
st.small
                                                   in State SInteger b
st{big = st.big + xfer, small = st.small - xfer}
                          ]

        display :: Either String (Int, [CState]) -> IO ()
        display :: Either String (Int, [CState]) -> IO ()
display (Left String
e)        = String -> IO ()
forall a. HasCallStack => String -> a
error String
e
        display (Right (Int
_, [CState]
as)) = (CState -> IO ()) -> [CState] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ CState -> IO ()
forall a. Show a => a -> IO ()
print [CState]
as