{-# OPTIONS_GHC -Wno-orphans #-}
module Test.QuickCheck.StateModel.Lockstep.Defaults (
initialState
, nextState
, precondition
, arbitraryAction
, shrinkAction
, 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
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
}
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
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
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
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
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)
instance HasVariables (Lockstep state) where
getAllVariables :: Lockstep state -> Set (Any Var)
getAllVariables Lockstep state
_ = Set (Any Var)
forall a. Set a
Set.empty
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
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
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
")"
]