{-# OPTIONS_GHC -Wno-orphans #-}

-- | 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.Set qualified as Set
import Data.Typeable

import Test.QuickCheck (Gen, Property)
import Test.QuickCheck qualified as QC
import Test.QuickCheck.StateModel ( Var, Any(..), LookUp, Realized, PostconditionM
                                  , Action, monitorPost)
import Test.QuickCheck.StateModel.Variables (VarContext, HasVariables (..))

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
  => VarContext -> Lockstep state -> Gen (Any (LockstepAction state))
arbitraryAction :: forall state.
InLockstep state =>
VarContext -> Lockstep state -> Gen (Any (LockstepAction state))
arbitraryAction VarContext
_ (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
  => VarContext
  -> Lockstep state
  -> LockstepAction state a -> [Any (LockstepAction state)]
shrinkAction :: forall state a.
InLockstep state =>
VarContext
-> Lockstep state
-> LockstepAction state a
-> [Any (LockstepAction state)]
shrinkAction VarContext
_ (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
  -> PostconditionM m Bool
postcondition :: forall (m :: * -> *) state a.
RunLockstep state m =>
(Lockstep state, Lockstep state)
-> LockstepAction state a
-> LookUp m
-> Realized m a
-> PostconditionM m Bool
postcondition (Lockstep state
before, Lockstep state
_after) LockstepAction state a
action LookUp m
_lookUp Realized m a
a =
    case 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 of
      Maybe String
Nothing -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
True
      Just String
s  -> forall (m :: * -> *).
Monad m =>
(Property -> Property) -> PostconditionM m ()
monitorPost (forall prop. Testable prop => String -> prop -> Property
QC.counterexample String
s) forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
False

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 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)

{-------------------------------------------------------------------------------
  Default class instances
-------------------------------------------------------------------------------}

-- | Ignore variables for lockstep state.
--
-- We largely ignore @quickcheck-dynamic@'s variables in the lockstep framework,
-- since it does its own accounting of model variables.
instance HasVariables (Lockstep state) where
  getAllVariables :: Lockstep state -> Set (Any Var)
getAllVariables Lockstep state
_ = forall a. Set a
Set.empty

-- | Ignore variables for lockstep actions.
--
-- We largely ignore @quickcheck-dynamic@'s variables in the lockstep framework,
-- since it does its own accounting of model variables.
instance HasVariables (Action (Lockstep state) a) where
  getAllVariables :: Action (Lockstep state) a -> Set (Any Var)
getAllVariables Action (Lockstep state) a
_ = forall a. Set a
Set.empty

{-------------------------------------------------------------------------------
  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
")"
          ]