Skip to content

Commit 9aa0f67

Browse files
RunModel -> typeclass
1 parent 0ba1dbf commit 9aa0f67

File tree

2 files changed

+54
-82
lines changed

2 files changed

+54
-82
lines changed

quickcheck-dynamic-iosim/test/Spec/DynamicLogic/RegistryModel.hs

Lines changed: 24 additions & 44 deletions
Original file line numberDiff line numberDiff line change
@@ -35,7 +35,7 @@ import Test.Tasty.QuickCheck (testProperty)
3535
import Spec.DynamicLogic.Registry
3636
import Test.QuickCheck.DynamicLogic.Core
3737
import Test.QuickCheck.StateModel
38-
import Test.QuickCheck.StateModel.IOSim
38+
import Test.QuickCheck.StateModel.IOSim()
3939

4040
data RegState = RegState
4141
{ tids :: [Var ThreadId]
@@ -130,58 +130,38 @@ instance StateModel RegState where
130130

131131
type RegM s = StateT (Registry (IOSim s)) (IOSim s)
132132

133-
runModelIOSim :: forall s. RunModel RegState (RegM s)
134-
runModelIOSim = RunModel { perform = performRegistry
135-
, postcondition = post
136-
, monitoring = mon
137-
}
138-
where
139-
performRegistry :: RegState
140-
-> Action RegState a
141-
-> LookUp (IOSim s)
142-
-> RegM s (RealizeIOSim s a)
143-
performRegistry _ Init _ = do
133+
instance (m ~ RegM s) => RunModel RegState m where
134+
perform _ Init _ = do
144135
reg <- lift setupRegistry
145136
put reg
146-
performRegistry _ Spawn _ = do
137+
perform _ Spawn _ = do
147138
lift $ forkIO (threadDelay 10000000)
148-
performRegistry _ (Register name tid) env = do
139+
perform _ (Register name tid) env = do
149140
reg <- get
150141
lift $ try $ register reg name (env tid)
151-
performRegistry _ (Unregister name) _ = do
142+
perform _ (Unregister name) _ = do
152143
reg <- get
153144
lift $ try $ unregister reg name
154-
performRegistry _ (WhereIs name) _ = do
145+
perform _ (WhereIs name) _ = do
155146
reg <- get
156147
lift $ whereis reg name
157-
performRegistry _ (KillThread tid) env = do
148+
perform _ (KillThread tid) env = do
158149
lift $ killThread (env tid)
159-
performRegistry s (Successful act) env = do
160-
performRegistry s act env
161-
162-
post :: RegState
163-
-> Action RegState a
164-
-> LookUp (RegM s)
165-
-> Realized (RegM s) a
166-
-> Bool
167-
post _ Init _ _ = True
168-
post s (WhereIs name) env mtid =
169-
(env <$> lookup name (regs s)) == mtid
170-
post _s Spawn _ _ = True
171-
post s (Register name step) _ res =
172-
positive s (Register name step) == isRight res
173-
post _s (Unregister _name) _ _ = True
174-
post _s (KillThread _) _ _ = True
175-
post _s (Successful (Register _ _)) _ res = isRight res
176-
post s (Successful act) env res = post s act env res
177-
178-
mon :: (RegState, RegState)
179-
-> Action RegState a
180-
-> LookUp (RegM s)
181-
-> Realized (RegM s) a
182-
-> Property
183-
-> Property
184-
mon (_s, s') act _ res =
150+
perform s (Successful act) env = do
151+
perform s act env
152+
153+
postcondition _ Init _ _ = pure True
154+
postcondition s (WhereIs name) env mtid =
155+
pure $ (env <$> lookup name (regs s)) == mtid
156+
postcondition _s Spawn _ _ = pure True
157+
postcondition s (Register name step) _ res =
158+
pure $ positive s (Register name step) == isRight res
159+
postcondition _s (Unregister _name) _ _ = pure True
160+
postcondition _s (KillThread _) _ _ = pure True
161+
postcondition _s (Successful (Register _ _)) _ res = pure $ isRight res
162+
postcondition s (Successful act) env res = postcondition s act env res
163+
164+
monitoring (_s, s') act _ res =
185165
counterexample ("\nState: " ++ show s' ++ "\n")
186166
. tabulate "Registry size" [show $ length (regs s')]
187167
. case act of
@@ -258,7 +238,7 @@ prop_Registry s =
258238
property $
259239
runIOSimProp $ do
260240
monitor $ counterexample "\nExecution\n"
261-
_res <- runPropertyStateT (runActions runModelIOSim s) (error "don't look at uninitialized state")
241+
_res <- runPropertyStateT (runActions s) (error "don't look at uninitialized state")
262242
assert True
263243

264244
-- TODO: put this in some extras module

quickcheck-dynamic/src/Test/QuickCheck/StateModel.hs

Lines changed: 30 additions & 38 deletions
Original file line numberDiff line numberDiff line change
@@ -22,7 +22,6 @@
2222
module Test.QuickCheck.StateModel (
2323
StateModel (..),
2424
RunModel (..),
25-
defaultRunModel,
2625
Any (..),
2726
Step (..),
2827
LookUp,
@@ -134,36 +133,30 @@ type instance Realized IO a = a
134133
type instance Realized (StateT s m) a = Realized m a
135134
type instance Realized (ReaderT r m) a = Realized m a
136135

137-
-- TODO: Maybe now it's time to turn this into it's own type class
138-
data RunModel state m = RunModel { -- | Perform an `Action` in some `state` in the `Monad` `m`. This
139-
-- is the function that's used to exercise the actual stateful
140-
-- implementation, usually through various side-effects as permitted
141-
-- by `m`. It produces a value of type `a`, eg. some observable
142-
-- output from the `Action` that should later be kept in the
143-
-- environment through a `Var a` also passed to the `nextState`
144-
-- function.
145-
--
146-
-- The `Lookup` parameter provides an /environment/ to lookup `Var
147-
-- a` instances from previous steps.
148-
perform :: forall a. ActionResult a => state -> Action state a -> LookUp m -> m (Realized m a)
149-
, -- | Postcondition on the `a` value produced at some step.
150-
-- The result is `assert`ed and will make the property fail should it be `False`. This is useful
151-
-- to check the implementation produces expected values.
152-
postcondition :: forall a. state -> Action state a -> LookUp m -> Realized m a -> Bool
153-
, -- | Allows the user to attach information to the `Property` at each step of the process.
154-
-- This function is given the full transition that's been executed, including the start and ending
155-
-- `state`, the `Action`, the current environment to `Lookup` and the value produced by `perform`
156-
-- while executing this step.
157-
monitoring :: forall a. (state, state) -> Action state a -> LookUp m -> Realized m a -> Property -> Property
158-
}
159-
160-
defaultRunModel :: Monad m
161-
=> (forall a. ActionResult a => state -> Action state a -> LookUp m -> m (Realized m a))
162-
-> RunModel state m
163-
defaultRunModel perform = RunModel { perform = perform
164-
, postcondition = \ _ _ _ _ -> True
165-
, monitoring = \ _ _ _ _ prop -> prop
166-
}
136+
class Monad m => RunModel state m where
137+
-- | Perform an `Action` in some `state` in the `Monad` `m`. This
138+
-- is the function that's used to exercise the actual stateful
139+
-- implementation, usually through various side-effects as permitted
140+
-- by `m`. It produces a value of type `a`, eg. some observable
141+
-- output from the `Action` that should later be kept in the
142+
-- environment through a `Var a` also passed to the `nextState`
143+
-- function.
144+
--
145+
-- The `Lookup` parameter provides an /environment/ to lookup `Var
146+
-- a` instances from previous steps.
147+
perform :: forall a. ActionResult a => state -> Action state a -> LookUp m -> m (Realized m a)
148+
-- | Postcondition on the `a` value produced at some step.
149+
-- The result is `assert`ed and will make the property fail should it be `False`. This is useful
150+
-- to check the implementation produces expected values.
151+
postcondition :: forall a. state -> Action state a -> LookUp m -> Realized m a -> m Bool
152+
postcondition _ _ _ _ = pure True
153+
-- | Allows the user to attach information to the `Property` at each step of the process.
154+
-- This function is given the full transition that's been executed, including the start and ending
155+
-- `state`, the `Action`, the current environment to `Lookup` and the value produced by `perform`
156+
-- while executing this step.
157+
monitoring :: forall a. (state, state) -> Action state a -> LookUp m -> Realized m a -> Property -> Property
158+
monitoring _ _ _ _ prop = prop
159+
167160

168161
type LookUp m = forall a. Typeable a => Var a -> Realized m a
169162

@@ -321,20 +314,18 @@ stateAfter (Actions actions) = loop initialState actions
321314

322315
runActions ::
323316
forall state m.
324-
(StateModel state, Monad m) =>
325-
RunModel state m ->
317+
(StateModel state, RunModel state m) =>
326318
Actions state ->
327319
PropertyM m (state, Env m)
328320
runActions = runActionsInState @_ @m initialState
329321

330322
runActionsInState ::
331323
forall state m.
332-
(StateModel state, Monad m) =>
324+
(StateModel state, RunModel state m) =>
333325
state ->
334-
RunModel state m ->
335326
Actions state ->
336327
PropertyM m (state, Env m)
337-
runActionsInState state RunModel{..} (Actions_ rejected (Smart _ actions)) = loop state [] actions
328+
runActionsInState st (Actions_ rejected (Smart _ actions)) = loop st [] actions
338329
where
339330
loop _s env [] = do
340331
unless (null rejected) $
@@ -348,6 +339,7 @@ runActionsInState state RunModel{..} (Actions_ rejected (Smart _ actions)) = loo
348339
let var = Var n
349340
s' = nextState s act var
350341
env' = (var :== ret) : env
351-
monitor (monitoring (s, s') act (lookUpVar env') ret)
352-
assert $ postcondition s act (lookUpVar env) ret
342+
monitor (monitoring @state @m (s, s') act (lookUpVar env') ret)
343+
b <- run $ postcondition s act (lookUpVar env) ret
344+
assert b
353345
loop s' env' as

0 commit comments

Comments
 (0)