{-# 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, StateModel (Error))
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   = EnvF (ModelValue state)
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 =
    state -> EnvF (ModelValue state) -> Lockstep state
forall state. state -> EnvF (ModelValue state) -> Lockstep state
Lockstep state
state' (EnvF (ModelValue state) -> Lockstep state)
-> EnvF (ModelValue state) -> Lockstep state
forall a b. (a -> b) -> a -> b
$ Var a
-> ModelValue state a
-> EnvF (ModelValue state)
-> EnvF (ModelValue state)
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') = LockstepAction state a
-> ModelLookUp state -> state -> (ModelValue state a, state)
forall a.
LockstepAction state a
-> ModelLookUp state -> state -> (ModelValue state a, state)
forall state a.
InLockstep state =>
LockstepAction state a
-> ModelLookUp state -> state -> (ModelValue state a, state)
modelNextState LockstepAction state a
action (EnvF (ModelValue state)
-> GVar (ModelOp state) a -> ModelValue state a
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) =
    (AnyGVar (ModelOp state) -> Bool)
-> [AnyGVar (ModelOp state)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\(SomeGVar GVar (ModelOp state) y
var) -> EnvF (ModelValue state) -> GVar (ModelOp state) y -> Bool
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) ([AnyGVar (ModelOp state)] -> Bool)
-> (LockstepAction state a -> [AnyGVar (ModelOp state)])
-> LockstepAction state a
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LockstepAction state a -> [AnyGVar (ModelOp state)]
forall a. LockstepAction state a -> [AnyGVar (ModelOp state)]
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) =
    ModelFindVariables state
-> state -> Gen (Any (LockstepAction state))
forall state.
InLockstep state =>
ModelFindVariables state
-> state -> Gen (Any (LockstepAction state))
arbitraryWithVars (EnvF (ModelValue state) -> ModelFindVariables state
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) =
    ModelFindVariables state
-> state -> LockstepAction state a -> [Any (LockstepAction state)]
forall state a.
InLockstep state =>
ModelFindVariables state
-> state -> LockstepAction state a -> [Any (LockstepAction state)]
forall a.
ModelFindVariables state
-> state -> LockstepAction state a -> [Any (LockstepAction state)]
shrinkWithVars (EnvF (ModelValue state) -> ModelFindVariables state
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 Proxy m
-> Lockstep state
-> LockstepAction state a
-> Realized m a
-> Maybe String
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
forall (t :: * -> *). Proxy t
Proxy @m) Lockstep state
before LockstepAction state a
action Realized m a
a of
      Maybe String
Nothing -> Bool -> PostconditionM m Bool
forall a. a -> PostconditionM m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
True
      Just String
s  -> (Property -> Property) -> PostconditionM m ()
forall (m :: * -> *).
Monad m =>
(Property -> Property) -> PostconditionM m ()
monitorPost (String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
QC.counterexample String
s) PostconditionM m ()
-> PostconditionM m Bool -> PostconditionM m Bool
forall a b.
PostconditionM m a -> PostconditionM m b -> PostconditionM m b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Bool -> PostconditionM m Bool
forall a. a -> PostconditionM m a
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
  -> Either (Error (Lockstep state)) (Realized m a)
  -> Property -> Property
monitoring :: forall (m :: * -> *) state a.
RunLockstep state m =>
Proxy m
-> (Lockstep state, Lockstep state)
-> LockstepAction state a
-> LookUp m
-> Either (Error (Lockstep state)) (Realized m a)
-> Property
-> Property
monitoring Proxy m
_p (Lockstep state
before, Lockstep state
after) LockstepAction state a
action LookUp m
_lookUp Either (Error (Lockstep state)) (Realized m a)
_realResp =
      String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
QC.counterexample (String
"State: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Lockstep state -> String
forall a. Show a => a -> String
show Lockstep state
after)
    (Property -> Property)
-> (Property -> Property) -> Property -> Property
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> [String] -> Property -> Property
forall prop.
Testable prop =>
String -> [String] -> prop -> Property
QC.tabulate String
"Tags" [String]
tags
  where
    tags :: [String]
    tags :: [String]
tags = (state, state)
-> LockstepAction state a -> ModelValue state a -> [String]
forall a.
(state, state)
-> LockstepAction state a -> ModelValue state a -> [String]
forall state a.
InLockstep state =>
(state, state)
-> LockstepAction state a -> ModelValue state a -> [String]
tagStep (Lockstep state -> state
forall state. Lockstep state -> state
lockstepModel Lockstep state
before, Lockstep state -> state
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 = (ModelValue state a, state) -> ModelValue state a
forall a b. (a, b) -> a
fst ((ModelValue state a, state) -> ModelValue state a)
-> (ModelValue state a, state) -> ModelValue state a
forall a b. (a -> b) -> a -> b
$ LockstepAction state a
-> ModelLookUp state -> state -> (ModelValue state a, state)
forall a.
LockstepAction state a
-> ModelLookUp state -> state -> (ModelValue state a, state)
forall state a.
InLockstep state =>
LockstepAction state a
-> ModelLookUp state -> state -> (ModelValue state a, state)
modelNextState
                        LockstepAction state a
action
                        (EnvF (ModelValue state)
-> GVar (ModelOp state) a -> ModelValue state a
forall (f :: * -> *) (op :: * -> * -> *) a.
(Typeable f, InterpretOp op f) =>
EnvF f -> GVar op a -> f a
lookUpEnvF (EnvF (ModelValue state)
 -> GVar (ModelOp state) a -> ModelValue state a)
-> EnvF (ModelValue state)
-> GVar (ModelOp state) a
-> ModelValue state a
forall a b. (a -> b) -> a -> b
$ Lockstep state -> EnvF (ModelValue state)
forall state. Lockstep state -> EnvF (ModelValue state)
lockstepEnv Lockstep state
before)
                        (Lockstep state -> state
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
_ = Set (Any Var)
forall a. Set a
Set.empty

-- | Do not ignore variables for lockstep actions.
--
-- @quickcheck-dynamic@ prints counterexamples as code that is more or less
-- runnable, which requires a sensible 'HasVariables' instance for lockstep
-- actions.
instance InLockstep state => HasVariables (Action (Lockstep state) a) where
  getAllVariables :: Action (Lockstep state) a -> Set (Any Var)
getAllVariables = [Set (Any Var)] -> Set (Any Var)
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions ([Set (Any Var)] -> Set (Any Var))
-> (Action (Lockstep state) a -> [Set (Any Var)])
-> Action (Lockstep state) a
-> Set (Any Var)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (AnyGVar (ModelOp state) -> Set (Any Var))
-> [AnyGVar (ModelOp state)] -> [Set (Any Var)]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap AnyGVar (ModelOp state) -> Set (Any Var)
forall a. HasVariables a => a -> Set (Any Var)
getAllVariables ([AnyGVar (ModelOp state)] -> [Set (Any Var)])
-> (Action (Lockstep state) a -> [AnyGVar (ModelOp state)])
-> Action (Lockstep state) a
-> [Set (Any Var)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Action (Lockstep state) a -> [AnyGVar (ModelOp state)]
forall a. LockstepAction state a -> [AnyGVar (ModelOp state)]
forall state a.
InLockstep state =>
LockstepAction state a -> [AnyGVar (ModelOp state)]
usedVars

{-------------------------------------------------------------------------------
  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
_ = (Var a -> GVar (ModelOp state) a)
-> [Var a] -> [GVar (ModelOp state) a]
forall a b. (a -> b) -> [a] -> [b]
map Var a -> GVar (ModelOp state) a
forall (op :: * -> * -> *) a.
(Operation op, Typeable a) =>
Var a -> GVar op a
fromVar ([Var a] -> [GVar (ModelOp state) a])
-> [Var a] -> [GVar (ModelOp state) a]
forall a b. (a -> b) -> a -> b
$ EnvF (ModelValue state) -> [Var a]
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         , Proxy m
-> LockstepAction state a -> Realized m a -> Observable state a
forall a.
Proxy m
-> LockstepAction state a -> Realized m a -> Observable state 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 , ModelValue state a -> Observable state a
forall state a.
InLockstep state =>
ModelValue state a -> Observable state a
forall a. ModelValue state a -> Observable state a
observeModel ModelValue state a
modelResp)
  where
    modelResp :: ModelValue state a
    modelResp :: ModelValue state a
modelResp = (ModelValue state a, state) -> ModelValue state a
forall a b. (a, b) -> a
fst ((ModelValue state a, state) -> ModelValue state a)
-> (ModelValue state a, state) -> ModelValue state a
forall a b. (a -> b) -> a -> b
$ LockstepAction state a
-> ModelLookUp state -> state -> (ModelValue state a, state)
forall a.
LockstepAction state a
-> ModelLookUp state -> state -> (ModelValue state a, state)
forall state a.
InLockstep state =>
LockstepAction state a
-> ModelLookUp state -> state -> (ModelValue state a, state)
modelNextState LockstepAction state a
action (EnvF (ModelValue state)
-> GVar (ModelOp state) a -> ModelValue state a
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 Observable state a -> Observable state a -> Bool
forall a. Eq a => a -> a -> Bool
== Observable state a
obsMockResp = Maybe String
forall a. Maybe a
Nothing
      | Bool
otherwise                  = String -> Maybe String
forall a. a -> Maybe a
Just (String -> Maybe String) -> String -> Maybe String
forall a b. (a -> b) -> a -> b
$ [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [
            String
"System under test returned: "
          , case Proxy m
-> LockstepAction state a -> Maybe (Dict (Show (Realized m a)))
forall a.
Proxy m
-> LockstepAction state a -> Maybe (Dict (Show (Realized m a)))
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
forall (t :: * -> *). Proxy t
Proxy @m) LockstepAction state a
action of
              Maybe (Dict (Show (Realized m a)))
Nothing   -> Observable state a -> String
forall a. Show a => a -> String
show Observable state a
obsRealResp
              Just Dict (Show (Realized m a))
Dict -> [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [
                  Observable state a -> String
forall a. Show a => a -> String
show Observable state a
obsRealResp
                , String
" ("
                , Realized m a -> String
forall a. Show a => a -> String
show Realized m a
realResp
                , String
")"
                ]
          , String
"\nbut model returned:         "
          , Observable state a -> String
forall a. Show a => a -> String
show Observable state a
obsMockResp
          , String
" ("
          , ModelValue state a -> String
forall a. Show a => a -> String
show ModelValue state a
mockResp
          , String
")"
          ]