-- | Default implementations for the @quickcheck-dynamic@ class methods
--
-- Intended for qualified import.
--
-- > import Test.QuickCheck.StateModel.Lockstep.Defaults qualified as Lockstep
module Test.QuickCheck.StateModel.Lockstep.Defaults (
    -- * Default implementations for methods of 'StateModel'
    initialState
  , nextState
  , precondition
  , arbitraryAction
  , shrinkAction
    -- * Default implementations for methods of 'RunModel'
  , postcondition
  , monitoring
  ) where

import Prelude hiding (init)

import Data.Constraint (Dict(..))
import Data.Maybe (isNothing)
import Data.Typeable

import Test.QuickCheck (Gen, Property)
import Test.QuickCheck qualified as QC
import Test.QuickCheck.StateModel (Var, Any(..), LookUp, Realized)

import Test.QuickCheck.StateModel.Lockstep.API
import Test.QuickCheck.StateModel.Lockstep.EnvF (EnvF)
import Test.QuickCheck.StateModel.Lockstep.EnvF qualified as EnvF
import Test.QuickCheck.StateModel.Lockstep.GVar

{-------------------------------------------------------------------------------
  Default implementations for members of 'StateModel'
-------------------------------------------------------------------------------}

-- | Default implementation for 'Test.QuickCheck.StateModel.initialState'
initialState :: state -> Lockstep state
initialState :: forall state. state -> Lockstep state
initialState state
state = Lockstep {
      lockstepModel :: state
lockstepModel = state
state
    , lockstepEnv :: EnvF (ModelValue state)
lockstepEnv   = forall (f :: * -> *). EnvF f
EnvF.empty
    }

-- | Default implementation for 'Test.QuickCheck.StateModel.nextState'
nextState :: forall state a.
     (InLockstep state, Typeable a)
  => Lockstep state
  -> LockstepAction state a
  -> Var a
  -> Lockstep state
nextState :: forall state a.
(InLockstep state, Typeable a) =>
Lockstep state -> LockstepAction state a -> Var a -> Lockstep state
nextState (Lockstep state
state EnvF (ModelValue state)
env) LockstepAction state a
action Var a
var =
    forall state. state -> EnvF (ModelValue state) -> Lockstep state
Lockstep state
state' forall a b. (a -> b) -> a -> b
$ forall a (f :: * -> *).
Typeable a =>
Var a -> f a -> EnvF f -> EnvF f
EnvF.insert Var a
var ModelValue state a
modelResp EnvF (ModelValue state)
env
  where
    modelResp :: ModelValue state a
    state'    :: state
    (ModelValue state a
modelResp, state
state') = forall state a.
InLockstep state =>
LockstepAction state a
-> ModelLookUp state -> state -> (ModelValue state a, state)
modelNextState LockstepAction state a
action (forall (f :: * -> *) (op :: * -> * -> *) a.
(Typeable f, InterpretOp op f) =>
EnvF f -> GVar op a -> f a
lookUpEnvF EnvF (ModelValue state)
env) state
state

-- | Default implementation for 'Test.QuickCheck.StateModel.precondition'
--
-- The default precondition only checks that all variables have a value
-- and that the operations on them are defined.
precondition ::
     InLockstep state
  => Lockstep state -> LockstepAction state a -> Bool
precondition :: forall state a.
InLockstep state =>
Lockstep state -> LockstepAction state a -> Bool
precondition (Lockstep state
_ EnvF (ModelValue state)
env) =
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\(SomeGVar GVar (ModelOp state) y
var) -> forall (f :: * -> *) (op :: * -> * -> *) a.
(Typeable f, InterpretOp op f) =>
EnvF f -> GVar op a -> Bool
definedInEnvF EnvF (ModelValue state)
env GVar (ModelOp state) y
var) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall state a.
InLockstep state =>
LockstepAction state a -> [AnyGVar (ModelOp state)]
usedVars

-- | Default implementation for 'Test.QuickCheck.StateModel.arbitraryAction'
arbitraryAction ::
     InLockstep state
  => Lockstep state -> Gen (Any (LockstepAction state))
arbitraryAction :: forall state.
InLockstep state =>
Lockstep state -> Gen (Any (LockstepAction state))
arbitraryAction (Lockstep state
state EnvF (ModelValue state)
env) =
    forall state.
InLockstep state =>
ModelFindVariables state
-> state -> Gen (Any (LockstepAction state))
arbitraryWithVars (forall state.
InLockstep state =>
EnvF (ModelValue state) -> ModelFindVariables state
varsOfType EnvF (ModelValue state)
env) state
state

-- | Default implementation for 'Test.QuickCheck.StateModel.shrinkAction'
shrinkAction ::
     InLockstep state
  => Lockstep state
  -> LockstepAction state a -> [Any (LockstepAction state)]
shrinkAction :: forall state a.
InLockstep state =>
Lockstep state
-> LockstepAction state a -> [Any (LockstepAction state)]
shrinkAction (Lockstep state
state EnvF (ModelValue state)
env) =
    forall state a.
InLockstep state =>
ModelFindVariables state
-> state -> LockstepAction state a -> [Any (LockstepAction state)]
shrinkWithVars (forall state.
InLockstep state =>
EnvF (ModelValue state) -> ModelFindVariables state
varsOfType EnvF (ModelValue state)
env) state
state

{-------------------------------------------------------------------------------
  Default implementations for methods of 'RunModel'
-------------------------------------------------------------------------------}

-- | Default implementation for 'Test.QuickCheck.StateModel.postcondition'
--
-- The default postcondition verifies that the real system and the model
-- return the same results, up to " observability ".
postcondition :: forall m state a.
     RunLockstep state m
  => (Lockstep state, Lockstep state)
  -> LockstepAction state a
  -> LookUp m
  -> Realized m a
  -> m Bool
postcondition :: forall (m :: * -> *) state a.
RunLockstep state m =>
(Lockstep state, Lockstep state)
-> LockstepAction state a -> LookUp m -> Realized m a -> m Bool
postcondition (Lockstep state
before, Lockstep state
_after) LockstepAction state a
action LookUp m
_lookUp Realized m a
a =
    forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall a. Maybe a -> Bool
isNothing forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) state a.
RunLockstep state m =>
Proxy m
-> Lockstep state
-> LockstepAction state a
-> Realized m a
-> Maybe String
checkResponse (forall {k} (t :: k). Proxy t
Proxy @m) Lockstep state
before LockstepAction state a
action Realized m a
a

monitoring :: forall m state a.
     RunLockstep state m
  => Proxy m
  -> (Lockstep state, Lockstep state)
  -> LockstepAction state a
  -> LookUp m
  -> Realized m a
  -> Property -> Property
monitoring :: forall (m :: * -> *) state a.
RunLockstep state m =>
Proxy m
-> (Lockstep state, Lockstep state)
-> LockstepAction state a
-> LookUp m
-> Realized m a
-> Property
-> Property
monitoring Proxy m
p (Lockstep state
before, Lockstep state
after) LockstepAction state a
action LookUp m
_lookUp Realized m a
realResp =
      forall prop. Testable prop => String -> prop -> Property
QC.counterexample (String
"State: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Lockstep state
after)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall b a. b -> (a -> b) -> Maybe a -> b
maybe forall a. a -> a
id forall prop. Testable prop => String -> prop -> Property
QC.counterexample (forall (m :: * -> *) state a.
RunLockstep state m =>
Proxy m
-> Lockstep state
-> LockstepAction state a
-> Realized m a
-> Maybe String
checkResponse Proxy m
p Lockstep state
before LockstepAction state a
action Realized m a
realResp)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall prop.
Testable prop =>
String -> [String] -> prop -> Property
QC.tabulate String
"Tags" [String]
tags
  where
    tags :: [String]
    tags :: [String]
tags = forall state a.
InLockstep state =>
(state, state)
-> LockstepAction state a -> ModelValue state a -> [String]
tagStep (forall state. Lockstep state -> state
lockstepModel Lockstep state
before, forall state. Lockstep state -> state
lockstepModel Lockstep state
after) LockstepAction state a
action ModelValue state a
modelResp

    modelResp :: ModelValue state a
    modelResp :: ModelValue state a
modelResp = forall a b. (a, b) -> a
fst forall a b. (a -> b) -> a -> b
$ forall state a.
InLockstep state =>
LockstepAction state a
-> ModelLookUp state -> state -> (ModelValue state a, state)
modelNextState
                        LockstepAction state a
action
                        (forall (f :: * -> *) (op :: * -> * -> *) a.
(Typeable f, InterpretOp op f) =>
EnvF f -> GVar op a -> f a
lookUpEnvF forall a b. (a -> b) -> a -> b
$ forall state. Lockstep state -> EnvF (ModelValue state)
lockstepEnv Lockstep state
before)
                        (forall state. Lockstep state -> state
lockstepModel Lockstep state
before)

{-------------------------------------------------------------------------------
  Internal auxiliary
-------------------------------------------------------------------------------}

varsOfType ::
     InLockstep state
  => EnvF (ModelValue state) -> ModelFindVariables state
varsOfType :: forall state.
InLockstep state =>
EnvF (ModelValue state) -> ModelFindVariables state
varsOfType EnvF (ModelValue state)
env Proxy a
_ = forall a b. (a -> b) -> [a] -> [b]
map forall (op :: * -> * -> *) a.
(Operation op, Typeable a) =>
Var a -> GVar op a
fromVar forall a b. (a -> b) -> a -> b
$ forall a (f :: * -> *). Typeable a => EnvF f -> [Var a]
EnvF.keysOfType EnvF (ModelValue state)
env

-- | Check the response of the system under test against the model
--
-- This is used in 'postcondition', where we can however only return a 'Bool',
-- and in 'monitoring', to give the user more detailed feedback.
checkResponse :: forall m state a.
     RunLockstep state m
  => Proxy m
  -> Lockstep state -> LockstepAction state a -> Realized m a -> Maybe String
checkResponse :: forall (m :: * -> *) state a.
RunLockstep state m =>
Proxy m
-> Lockstep state
-> LockstepAction state a
-> Realized m a
-> Maybe String
checkResponse Proxy m
p (Lockstep state
state EnvF (ModelValue state)
env) LockstepAction state a
action Realized m a
a =
    (Realized m a, Observable state a)
-> (ModelValue state a, Observable state a) -> Maybe String
compareEquality
      (Realized m a
a         , forall state (m :: * -> *) a.
RunLockstep state m =>
Proxy m
-> LockstepAction state a -> Realized m a -> Observable state a
observeReal Proxy m
p LockstepAction state a
action Realized m a
a)
      (ModelValue state a
modelResp , forall state a.
InLockstep state =>
ModelValue state a -> Observable state a
observeModel ModelValue state a
modelResp)
  where
    modelResp :: ModelValue state a
    modelResp :: ModelValue state a
modelResp = forall a b. (a, b) -> a
fst forall a b. (a -> b) -> a -> b
$ forall state a.
InLockstep state =>
LockstepAction state a
-> ModelLookUp state -> state -> (ModelValue state a, state)
modelNextState LockstepAction state a
action (forall (f :: * -> *) (op :: * -> * -> *) a.
(Typeable f, InterpretOp op f) =>
EnvF f -> GVar op a -> f a
lookUpEnvF EnvF (ModelValue state)
env) state
state

    compareEquality ::
         (Realized m a, Observable state a)
      -> (ModelValue state a, Observable state a) -> Maybe String
    compareEquality :: (Realized m a, Observable state a)
-> (ModelValue state a, Observable state a) -> Maybe String
compareEquality (Realized m a
realResp, Observable state a
obsRealResp) (ModelValue state a
mockResp, Observable state a
obsMockResp)
      | Observable state a
obsRealResp forall a. Eq a => a -> a -> Bool
== Observable state a
obsMockResp = forall a. Maybe a
Nothing
      | Bool
otherwise                  = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [
            String
"System under test returned: "
          , case forall state (m :: * -> *) a.
RunLockstep state m =>
Proxy m
-> LockstepAction state a -> Maybe (Dict (Show (Realized m a)))
showRealResponse (forall {k} (t :: k). Proxy t
Proxy @m) LockstepAction state a
action of
              Maybe (Dict (Show (Realized m a)))
Nothing   -> forall a. Show a => a -> String
show Observable state a
obsRealResp
              Just Dict (Show (Realized m a))
Dict -> forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [
                  forall a. Show a => a -> String
show Observable state a
obsRealResp
                , String
" ("
                , forall a. Show a => a -> String
show Realized m a
realResp
                , String
")"
                ]
          , String
"\nbut model returned:         "
          , forall a. Show a => a -> String
show Observable state a
obsMockResp
          , String
" ("
          , forall a. Show a => a -> String
show ModelValue state a
mockResp
          , String
")"
          ]