{-# 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
  , postconditionWith
  , monitoring
  ) where

import           Prelude hiding (init)

import           Data.Constraint (Dict (..))
import qualified Data.Set as Set
import           Data.Typeable

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

import           Test.QuickCheck.StateModel.Lockstep.API
import qualified Test.QuickCheck.StateModel.Lockstep.EnvF 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
-> EnvF (ModelValue state) -> state -> (ModelValue state a, state)
forall a.
LockstepAction state a
-> EnvF (ModelValue state) -> state -> (ModelValue state a, state)
forall state a.
InLockstep state =>
LockstepAction state a
-> ModelVarContext state -> state -> (ModelValue state a, state)
modelNextState LockstepAction state a
action 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) =
    EnvF (ModelValue state)
-> state -> Gen (Any (LockstepAction state))
forall state.
InLockstep state =>
ModelVarContext state -> state -> Gen (Any (LockstepAction state))
arbitraryWithVars 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) =
    EnvF (ModelValue state)
-> state -> LockstepAction state a -> [Any (LockstepAction state)]
forall a.
EnvF (ModelValue state)
-> state -> LockstepAction state a -> [Any (LockstepAction state)]
forall state a.
InLockstep state =>
ModelVarContext state
-> state -> LockstepAction state a -> [Any (LockstepAction state)]
shrinkWithVars 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
  -> a
  -> PostconditionM m Bool
postcondition :: forall (m :: * -> *) state a.
RunLockstep state m =>
(Lockstep state, Lockstep state)
-> LockstepAction state a -> LookUp -> a -> PostconditionM m Bool
postcondition = Bool
-> (Lockstep state, Lockstep state)
-> LockstepAction state a
-> LookUp
-> a
-> PostconditionM m Bool
forall (m :: * -> *) state a.
RunLockstep state m =>
Bool
-> (Lockstep state, Lockstep state)
-> LockstepAction state a
-> LookUp
-> a
-> PostconditionM m Bool
postconditionWith Bool
True

-- | Like 'postcondition', but with configurable verbosity.
--
-- By default, all states of the model are printed when a property
-- counterexample is printed. If verbose output is enabled, the counterexample
-- will also print all responses from the real system and the model.
postconditionWith :: forall m state a.
     RunLockstep state m
  => Bool -- ^ Verbose output
  -> (Lockstep state, Lockstep state)
  -> LockstepAction state a
  -> LookUp
  -> a
  -> PostconditionM m Bool
postconditionWith :: forall (m :: * -> *) state a.
RunLockstep state m =>
Bool
-> (Lockstep state, Lockstep state)
-> LockstepAction state a
-> LookUp
-> a
-> PostconditionM m Bool
postconditionWith Bool
verbose (Lockstep state
before, Lockstep state
_after) LockstepAction state a
action LookUp
_lookUp a
a =
    case Proxy m
-> Lockstep state
-> LockstepAction state a
-> a
-> Either String String
forall (m :: * -> *) state a.
RunLockstep state m =>
Proxy m
-> Lockstep state
-> LockstepAction state a
-> a
-> Either String String
checkResponse (forall {k} (t :: k). Proxy t
forall (t :: * -> *). Proxy t
Proxy @m) Lockstep state
before LockstepAction state a
action a
a of
      Right String
s
        | Bool
verbose -> (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
True
        | Bool
otherwise -> Bool -> PostconditionM m Bool
forall a. a -> PostconditionM m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
True
      Left 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
  -> Either (Error (Lockstep state) m) a
  -> Property -> Property
monitoring :: forall (m :: * -> *) state a.
RunLockstep state m =>
Proxy m
-> (Lockstep state, Lockstep state)
-> LockstepAction state a
-> LookUp
-> Either (Error (Lockstep state) m) a
-> Property
-> Property
monitoring Proxy m
_p (Lockstep state
before, Lockstep state
after) LockstepAction state a
action LookUp
_lookUp Either (Error (Lockstep state) 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
-> ModelVarContext state -> state -> (ModelValue state a, state)
forall a.
LockstepAction state a
-> ModelVarContext state -> state -> (ModelValue state a, state)
forall state a.
InLockstep state =>
LockstepAction state a
-> ModelVarContext state -> state -> (ModelValue state a, state)
modelNextState
                        LockstepAction state a
action
                        (Lockstep state -> ModelVarContext 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
-------------------------------------------------------------------------------}

-- | 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 -> a -> Either String String
checkResponse :: forall (m :: * -> *) state a.
RunLockstep state m =>
Proxy m
-> Lockstep state
-> LockstepAction state a
-> a
-> Either String String
checkResponse Proxy m
p (Lockstep state
state EnvF (ModelValue state)
env) LockstepAction state a
action a
a =
    (a, Observable state a)
-> (ModelValue state a, Observable state a) -> Either String String
compareEquality
      (a
a         , Proxy m -> LockstepAction state a -> a -> Observable state a
forall a.
Proxy m -> LockstepAction state a -> a -> Observable state a
forall state (m :: * -> *) a.
RunLockstep state m =>
Proxy m -> LockstepAction state a -> a -> Observable state a
observeReal Proxy m
p LockstepAction state a
action 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
-> EnvF (ModelValue state) -> state -> (ModelValue state a, state)
forall a.
LockstepAction state a
-> EnvF (ModelValue state) -> state -> (ModelValue state a, state)
forall state a.
InLockstep state =>
LockstepAction state a
-> ModelVarContext state -> state -> (ModelValue state a, state)
modelNextState LockstepAction state a
action EnvF (ModelValue state)
env state
state

    compareEquality ::
         (a, Observable state a)
      -> (ModelValue state a, Observable state a) -> Either String String
    compareEquality :: (a, Observable state a)
-> (ModelValue state a, Observable state a) -> Either String String
compareEquality (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 = String -> Either String String
forall a b. b -> Either a b
Right (String -> Either String String) -> String -> Either String String
forall a b. (a -> b) -> a -> b
$ [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [
            String
"System under test returned: "
          , String
sutReturned
          , String
"\nModel returned:             "
          , String
modelReturned
          ]
      | Bool
otherwise                  = String -> Either String String
forall a b. a -> Either a b
Left (String -> Either String String) -> String -> Either String String
forall a b. (a -> b) -> a -> b
$ [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [
            String
"System under test returned: "
          , String
sutReturned
          , String
"\nbut model returned:         "
          , String
modelReturned
          ]

      where
        sutReturned :: String
sutReturned = case Proxy m -> LockstepAction state a -> Maybe (Dict (Show a))
forall a.
Proxy m -> LockstepAction state a -> Maybe (Dict (Show a))
forall state (m :: * -> *) a.
RunLockstep state m =>
Proxy m -> LockstepAction state a -> Maybe (Dict (Show a))
showRealResponse (forall {k} (t :: k). Proxy t
forall (t :: * -> *). Proxy t
Proxy @m) LockstepAction state a
action of
            Maybe (Dict (Show a))
Nothing   -> Observable state a -> String
forall a. Show a => a -> String
show Observable state a
obsRealResp
            Just Dict (Show 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
" ("
              , a -> String
forall a. Show a => a -> String
show a
realResp
              , String
")"
              ]

        modelReturned :: String
modelReturned = [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
obsMockResp
            , String
" ("
            , ModelValue state a -> String
forall a. Show a => a -> String
show ModelValue state a
mockResp
            , String
")"
            ]