{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE StandaloneDeriving #-}
-----------------------------------------------------------------------------
-- |
-- Module : DieHard
-- Copyright : (C) 2017, ATS Advanced Telematic Systems GmbH
-- License : BSD-style (see the file LICENSE)
--
-- Maintainer : Stevan Andjelkovic <stevan.andjelkovic@strath.ac.uk>
-- Stability : provisional
-- Portability : non-portable (GHC extensions)
--
-- This module contains a solution to the water jug puzzle featured in
-- /Die Hard 3/.
--
-----------------------------------------------------------------------------
module DieHard
( Command(..)
, Model(..)
, initModel
, transitions
, prop_dieHard
) where
import Data.Kind
(Type)
import GHC.Generics
(Generic, Generic1)
import Prelude
import Test.QuickCheck
(Gen, Property, oneof, (===))
import Test.QuickCheck.Monadic
(monadicIO)
import Test.StateMachine
import Test.StateMachine.TreeDiff
import qualified Test.StateMachine.Types.Rank2 as Rank2
------------------------------------------------------------------------
-- The problem is to measure exactly 4 liters of water given a 3- and
-- 5-liter jug.
-- We start of defining the different actions that are allowed:
data Command (r :: Type -> Type)
= FillBig -- Fill the 5-liter jug.
| FillSmall -- Fill the 3-liter jug.
| EmptyBig -- Empty the 5-liter jug.
| EmptySmall
| SmallIntoBig -- Pour the contents of the 3-liter jug
-- into 5-liter jug.
| BigIntoSmall
deriving stock (Eq, Show, Generic1)
deriving anyclass (Rank2.Functor, Rank2.Foldable, Rank2.Traversable, CommandNames)
data Response (r :: Type -> Type) = Done
deriving stock (Show, Generic1)
deriving anyclass (Rank2.Foldable)
------------------------------------------------------------------------
-- The model (or state) keeps track of what amount of water is in the
-- two jugs.
data Model (r :: Type -> Type) = Model
{ bigJug :: Int
, smallJug :: Int
} deriving stock (Show, Eq, Generic)
deriving anyclass instance ToExpr (Model Concrete)
initModel :: Model r
initModel = Model 0 0
------------------------------------------------------------------------
-- There are no pre-conditions for our actions. That simply means that
-- any action can happen at any state.
preconditions :: Model Symbolic -> Command Symbolic -> Logic
preconditions _ _ = Top
-- The transitions describe how the actions change the state.
transitions :: Model r -> Command r -> Response r -> Model r
transitions m FillBig _ = m { bigJug = 5 }
transitions m FillSmall _ = m { smallJug = 3 }
transitions m EmptyBig _ = m { bigJug = 0 }
transitions m EmptySmall _ = m { smallJug = 0 }
transitions (Model big small) SmallIntoBig _ =
let big' = min 5 (big + small) in
Model { bigJug = big'
, smallJug = small - (big' - big) }
transitions (Model big small) BigIntoSmall _ =
let small' = min 3 (big + small) in
Model { bigJug = big - (small' - small)
, smallJug = small'
}
-- The post-condition is used in a bit of a funny way. Recall that we
-- want to find a series of actions that leads to the big jug containing
-- 4 liters. So the idea is to state an invariant saying that the big
-- jug is NOT equal to 4 after we performed any action. If we happen to
-- find a series of actions where this is not true, i.e. the big jug
-- actually does contain 4 liters, then a minimal counter example will
-- be presented -- this will be our solution.
postconditions :: Model Concrete -> Command Concrete -> Response Concrete -> Logic
postconditions s c r = bigJug (transitions s c r) ./= 4
------------------------------------------------------------------------
-- The generator of actions is simple, with equal distribution pick an
-- action.
generator :: Model Symbolic -> Maybe (Gen (Command Symbolic))
generator _ = Just $ oneof
[ return FillBig
, return FillSmall
, return EmptyBig
, return EmptySmall
, return SmallIntoBig
, return BigIntoSmall
]
-- There's nothing to shrink.
shrinker :: Model r -> Command r -> [Command r]
shrinker _ _ = []
------------------------------------------------------------------------
-- We are not modelling an actual program here, so there's no semantics
-- for our actions. We are merely doing model checking.
semantics :: Command Concrete -> IO (Response Concrete)
semantics _ = return Done
mock :: Model Symbolic -> Command Symbolic -> GenSym (Response Symbolic)
mock _ _ = return Done
------------------------------------------------------------------------
-- Finally we have all the pieces needed to get the sequential property!
-- To make the code fit on a line, we first group all things related to
-- generation and execution of programs respectively.
sm :: StateMachine Model Command IO Response
sm = StateMachine initModel transitions preconditions postconditions
Nothing generator shrinker semantics mock noCleanup
prop_dieHard :: Property
prop_dieHard = forAllCommands sm Nothing $ \cmds -> monadicIO $ do
(hist, _model, res) <- runCommands sm cmds
prettyCommands sm hist (checkCommandNames cmds (res === Ok))
-- If we run @quickCheck prop_dieHard@ we get:
--
-- @
-- *** Failed! Falsifiable (after 43 tests and 4 shrinks):
-- Commands
-- { unCommands =
-- [ Command FillBig (fromList [])
-- , Command BigIntoSmall (fromList [])
-- , Command EmptySmall (fromList [])
-- , Command BigIntoSmall (fromList [])
-- , Command FillBig (fromList [])
-- , Command BigIntoSmall (fromList [])
-- ]
-- }
--
-- Model {bigJug = 0,smallJug = 0}
--
-- == FillBig ==> Done [ 0 ]
--
-- Model {bigJug = -0 +5
-- ,smallJug = 0}
--
-- == BigIntoSmall ==> Done [ 0 ]
--
-- Model {bigJug = -5 +2
-- ,smallJug = -0 +3}
--
-- == EmptySmall ==> Done [ 0 ]
--
-- Model {bigJug = 2
-- ,smallJug = -3 +0}
--
-- == BigIntoSmall ==> Done [ 0 ]
--
-- Model {bigJug = -2 +0
-- ,smallJug = -0 +2}
--
-- == FillBig ==> Done [ 0 ]
--
-- Model {bigJug = -0 +5
-- ,smallJug = 2}
--
-- == BigIntoSmall ==> Done [ 0 ]
--
-- Model {bigJug = -5 +4
-- ,smallJug = -2 +3}
--
-- PostconditionFailed "PredicateC (4 :== 4)" /= Ok
-- @
--
-- The counterexample is our solution.