Skip to content

Commit d5b7f59

Browse files
MaximilianAlgehedMaximilianAlgehed
committed
Random generation of initial states
1 parent 9ab580a commit d5b7f59

File tree

6 files changed

+130
-112
lines changed

6 files changed

+130
-112
lines changed

‎quickcheck-dynamic/src/Test/QuickCheck/DynamicLogic.hs

+5-3
Original file line numberDiff line numberDiff line change
@@ -131,7 +131,7 @@ forAllNonVariableQ :: QuantifyConstraints (HasNoVariables a) => Quantification a
131131
forAllNonVariableQ q = DL $ \s k -> DL.forAllQ (hasNoVariablesQ q) $ \(HasNoVariables x) -> k x s
132132

133133
runDL :: Annotated s -> DL s () -> DL.DynFormula s
134-
runDL s dl = unDL dl s $ \_ _ -> DL.passTest
134+
runDL s dl = (unDL dl s $ \_ _ -> DL.passTest)
135135

136136
forAllUniqueDL
137137
:: (DL.DynLogicModel s, Testable a)
@@ -146,7 +146,8 @@ forAllDL
146146
=> DL s ()
147147
-> (Actions s -> a)
148148
-> Property
149-
forAllDL d = DL.forAllScripts (runDL initialAnnotatedState d)
149+
forAllDL d p =
150+
forAllBlind initialState $ \st -> DL.forAllScripts st (runDL (Metadata mempty st) d) p
150151

151152
forAllMappedDL
152153
:: (DL.DynLogicModel s, Testable a)
@@ -157,4 +158,5 @@ forAllMappedDL
157158
-> (srep -> a)
158159
-> Property
159160
forAllMappedDL to from fromScript d prop =
160-
DL.forAllMappedScripts to from (runDL initialAnnotatedState d) (prop . fromScript)
161+
forAll initialState $ \st ->
162+
DL.forAllMappedScripts st to from (runDL (Metadata mempty st) d) (prop . fromScript)

‎quickcheck-dynamic/src/Test/QuickCheck/DynamicLogic/Internal.hs

+78-69
Original file line numberDiff line numberDiff line change
@@ -171,10 +171,10 @@ instance StateModel s => Show (FailingAction s) where
171171
show (ActionFail (ActionWithPolarity a pol)) = show pol ++ " : " ++ show a
172172

173173
data DynLogicTest s
174-
= BadPrecondition (TestSequence s) (FailingAction s) (Annotated s)
175-
| Looping (TestSequence s)
176-
| Stuck (TestSequence s) (Annotated s)
177-
| DLScript (TestSequence s)
174+
= BadPrecondition (Annotated s) (TestSequence s) (FailingAction s) (Annotated s)
175+
| Looping (Annotated s) (TestSequence s)
176+
| Stuck (Annotated s) (TestSequence s) (Annotated s)
177+
| DLScript (Annotated s) (TestSequence s)
178178

179179
data Witnesses r where
180180
Do :: r -> Witnesses r
@@ -294,9 +294,10 @@ prettyWitnesses :: Witnesses () -> [String]
294294
prettyWitnesses (Witness a w) = ("_ <- forAllQ $ exactlyQ $ " ++ show a) : prettyWitnesses w
295295
prettyWitnesses Do{} = []
296296

297+
-- TODO: show initial state is
297298
instance StateModel s => Show (DynLogicTest s) where
298-
show (BadPrecondition ss bad s) =
299-
prettyTestSequence (usedVariables ss <> allVariables bad) ss
299+
show (BadPrecondition is ss bad s) =
300+
prettyTestSequence (usedVariables is ss <> allVariables bad) ss
300301
++ "\n -- In state: "
301302
++ show s
302303
++ "\n "
@@ -309,12 +310,12 @@ instance StateModel s => Show (DynLogicTest s) where
309310
f
310311
| p == PosPolarity = "action"
311312
| otherwise = "failingAction"
312-
show (Looping ss) = prettyTestSequence (usedVariables ss) ss ++ "\n pure ()\n -- Looping"
313-
show (Stuck ss s) = prettyTestSequence (usedVariables ss) ss ++ "\n pure ()\n -- Stuck in state " ++ show s
314-
show (DLScript ss) = prettyTestSequence (usedVariables ss) ss ++ "\n pure ()\n"
313+
show (Looping is ss) = prettyTestSequence (usedVariables is ss) ss ++ "\n pure ()\n -- Looping"
314+
show (Stuck is ss s) = prettyTestSequence (usedVariables is ss) ss ++ "\n pure ()\n -- Stuck in state " ++ show s
315+
show (DLScript is ss) = prettyTestSequence (usedVariables is ss) ss ++ "\n pure ()\n"
315316

316-
usedVariables :: forall s. StateModel s => TestSequence s -> VarContext
317-
usedVariables = go initialAnnotatedState
317+
usedVariables :: forall s. StateModel s => Annotated s -> TestSequence s -> VarContext
318+
usedVariables s = go s
318319
where
319320
go :: Annotated s -> TestSequence s -> VarContext
320321
go aState TestSeqStop = allVariables (underlyingState aState)
@@ -342,10 +343,11 @@ restrictedPolar (ActionWithPolarity a _) = restricted a
342343
-- `Actions` sequence into a proper `Property` that can be run by QuickCheck.
343344
forAllScripts
344345
:: (DynLogicModel s, Testable a)
345-
=> DynFormula s
346+
=> s
347+
-> DynFormula s
346348
-> (Actions s -> a)
347349
-> Property
348-
forAllScripts = forAllMappedScripts id id
350+
forAllScripts s = forAllMappedScripts s id id
349351

350352
-- | `Property` function suitable for formulae without choice.
351353
forAllUniqueScripts
@@ -365,16 +367,17 @@ forAllUniqueScripts s f k =
365367
-- | Creates a `Property` from `DynFormula` with some specialised isomorphism for shrinking purpose.
366368
forAllMappedScripts
367369
:: (DynLogicModel s, Testable a)
368-
=> (rep -> DynLogicTest s)
370+
=> s
371+
-> (rep -> DynLogicTest s)
369372
-> (DynLogicTest s -> rep)
370373
-> DynFormula s
371374
-> (Actions s -> a)
372375
-> Property
373-
forAllMappedScripts to from f k =
376+
forAllMappedScripts s to from f k =
374377
QC.withSize $ \n ->
375378
let d = unDynFormula f n
376379
in forAllShrinkBlind
377-
(Smart 0 <$> sized ((from <$>) . generateDLTest d))
380+
(Smart 0 <$> sized ((from <$>) . generateDLTest (Metadata mempty s) d))
378381
(shrinkSmart ((from <$>) . shrinkDLTest d . to))
379382
$ \(Smart _ script) ->
380383
withDLScript d k (to script)
@@ -405,17 +408,24 @@ validDLTest test prop =
405408
Stuck{} -> property Discard
406409
_other -> counterexample (show test) False
407410

408-
generateDLTest :: DynLogicModel s => DynLogic s -> Int -> Gen (DynLogicTest s)
409-
generateDLTest d size = generate chooseNextStep d 0 (initialStateFor d) size
411+
generateDLTest :: DynLogicModel s => Annotated s -> DynLogic s -> Int -> Gen (DynLogicTest s)
412+
generateDLTest s d size = do
413+
generate chooseNextStep d 0 s size
410414

411415
onDLTestSeq :: (TestSequence s -> TestSequence s) -> DynLogicTest s -> DynLogicTest s
412-
onDLTestSeq f (BadPrecondition ss bad s) = BadPrecondition (f ss) bad s
413-
onDLTestSeq f (Looping ss) = Looping (f ss)
414-
onDLTestSeq f (Stuck ss s) = Stuck (f ss) s
415-
onDLTestSeq f (DLScript ss) = DLScript (f ss)
416+
onDLTestSeq f (BadPrecondition is ss bad s) = BadPrecondition is (f ss) bad s
417+
onDLTestSeq f (Looping is ss) = Looping is (f ss)
418+
onDLTestSeq f (Stuck is ss s) = Stuck is (f ss) s
419+
onDLTestSeq f (DLScript is ss) = DLScript is (f ss)
420+
421+
setDLTestState :: Annotated s -> DynLogicTest s -> DynLogicTest s
422+
setDLTestState is (BadPrecondition _ ss bad s) = BadPrecondition is ss bad s
423+
setDLTestState is (Looping _ ss) = Looping is ss
424+
setDLTestState is (Stuck _ ss s) = Stuck is ss s
425+
setDLTestState is (DLScript _ ss) = DLScript is ss
416426

417-
consDLTest :: TestStep s -> DynLogicTest s -> DynLogicTest s
418-
consDLTest step = onDLTestSeq (step :>)
427+
consDLTest :: Annotated s -> TestStep s -> DynLogicTest s -> DynLogicTest s
428+
consDLTest is step = setDLTestState is . onDLTestSeq (step :>)
419429

420430
consDLTestW :: Witnesses () -> DynLogicTest s -> DynLogicTest s
421431
consDLTestW w = onDLTestSeq (addW w)
@@ -433,15 +443,15 @@ generate
433443
-> m (DynLogicTest s)
434444
generate chooseNextStepFun d n s size =
435445
if n > sizeLimit size
436-
then return $ Looping TestSeqStop
446+
then return $ Looping s TestSeqStop
437447
else do
438448
let preferred = if n > size then stopping d else noStopping d
439-
useStep (BadAction (Witnesses ws bad)) _ = return $ BadPrecondition (TestSeqStopW ws) bad s
440-
useStep StoppingStep _ = return $ DLScript TestSeqStop
449+
useStep (BadAction (Witnesses ws bad)) _ = return $ BadPrecondition s (TestSeqStopW ws) bad s
450+
useStep StoppingStep _ = return $ DLScript s TestSeqStop
441451
useStep (Stepping step d') _ =
442452
case discardWitnesses step of
443453
var := act ->
444-
consDLTest step
454+
consDLTest s step
445455
<$> generate
446456
chooseNextStepFun
447457
d'
@@ -451,15 +461,12 @@ generate chooseNextStepFun d n s size =
451461
useStep NoStep alt = alt
452462
foldr
453463
(\step k -> do try <- chooseNextStepFun s n step; useStep try k)
454-
(return $ Stuck TestSeqStop s)
464+
(return $ Stuck s TestSeqStop s)
455465
[preferred, noAny preferred, d, noAny d]
456466

457467
sizeLimit :: Int -> Int
458468
sizeLimit size = 2 * size + 20
459469

460-
initialStateFor :: StateModel s => DynLogic s -> Annotated s
461-
initialStateFor _ = initialAnnotatedState
462-
463470
stopping :: DynLogic s -> DynLogic s
464471
stopping EmptySpec = EmptySpec
465472
stopping Stop = Stop
@@ -589,22 +596,28 @@ keepTryingUntil n g p = do
589596
if p x then return $ Just x else scale (+ 1) $ keepTryingUntil (n - 1) g p
590597

591598
shrinkDLTest :: DynLogicModel s => DynLogic s -> DynLogicTest s -> [DynLogicTest s]
592-
shrinkDLTest _ (Looping _) = []
599+
shrinkDLTest _ (Looping _ _) = []
593600
shrinkDLTest d tc =
594-
[ test | as' <- shrinkScript d (getScript tc), let pruned = pruneDLTest d as'
595-
test = makeTestFromPruned d pruned,
596-
-- Don't shrink a non-executable test case to an executable one.
601+
[ test
602+
| as' <-
603+
shrinkScript
604+
(underlyingState $ getInitialState tc)
605+
d
606+
(getScript tc)
607+
, let pruned = pruneDLTest (getInitialState tc) d as'
608+
test = makeTestFromPruned (getInitialState tc) d pruned
609+
, -- Don't shrink a non-executable test case to an executable one.
597610
case (tc, test) of
598-
(DLScript _, _) -> True
599-
(_, DLScript _) -> False
611+
(DLScript _ _, _) -> True
612+
(_, DLScript _ _) -> False
600613
_ -> True
601614
]
602615

603616
nextStateStep :: StateModel s => Step s -> Annotated s -> Annotated s
604617
nextStateStep (var := act) s = computeNextState s act var
605618

606-
shrinkScript :: forall s. DynLogicModel s => DynLogic s -> TestSequence s -> [TestSequence s]
607-
shrinkScript = shrink' initialAnnotatedState
619+
shrinkScript :: forall s. DynLogicModel s => s -> DynLogic s -> TestSequence s -> [TestSequence s]
620+
shrinkScript is = shrink' (Metadata mempty is)
608621
where
609622
shrink' :: Annotated s -> DynLogic s -> TestSequence s -> [TestSequence s]
610623
shrink' s d ss = structural s d ss ++ nonstructural s d ss
@@ -648,8 +661,8 @@ shrinkWitness AfterAny{} _ = []
648661

649662
-- The result of pruning a list of actions is a prefix of a list of actions that
650663
-- could have been generated by the dynamic logic.
651-
pruneDLTest :: forall s. DynLogicModel s => DynLogic s -> TestSequence s -> TestSequence s
652-
pruneDLTest dl = prune [dl] initialAnnotatedState
664+
pruneDLTest :: forall s. DynLogicModel s => Annotated s -> DynLogic s -> TestSequence s -> TestSequence s
665+
pruneDLTest is dl = prune [dl] is
653666
where
654667
prune [] _ _ = TestSeqStop
655668
prune _ _ TestSeqStop = TestSeqStop
@@ -710,27 +723,29 @@ demonicAlt ds = foldr1 (Alt Demonic) ds
710723

711724
propPruningGeneratedScriptIsNoop :: DynLogicModel s => DynLogic s -> Property
712725
propPruningGeneratedScriptIsNoop d =
713-
forAll (sized $ \n -> choose (1, max 1 n) >>= generateDLTest d) $ \test ->
714-
let script = case test of
715-
BadPrecondition s _ _ -> s
716-
Looping s -> s
717-
Stuck s _ -> s
718-
DLScript s -> s
719-
in script == pruneDLTest d script
726+
forAll initialState $ \s ->
727+
forAll (sized $ \n -> choose (1, max 1 n) >>= generateDLTest (Metadata mempty s) d) $ \test ->
728+
getScript test == pruneDLTest (getInitialState test) d (getScript test)
729+
730+
getInitialState :: DynLogicTest s -> Annotated s
731+
getInitialState (BadPrecondition is _ _ _) = is
732+
getInitialState (Looping is _) = is
733+
getInitialState (Stuck is _ _) = is
734+
getInitialState (DLScript is _) = is
720735

721736
getScript :: DynLogicTest s -> TestSequence s
722-
getScript (BadPrecondition s _ _) = s
723-
getScript (Looping s) = s
724-
getScript (Stuck s _) = s
725-
getScript (DLScript s) = s
737+
getScript (BadPrecondition _ s _ _) = s
738+
getScript (Looping _ s) = s
739+
getScript (Stuck _ s _) = s
740+
getScript (DLScript _ s) = s
726741

727-
makeTestFromPruned :: forall s. DynLogicModel s => DynLogic s -> TestSequence s -> DynLogicTest s
728-
makeTestFromPruned dl = make dl initialAnnotatedState
742+
makeTestFromPruned :: forall s. DynLogicModel s => Annotated s -> DynLogic s -> TestSequence s -> DynLogicTest s
743+
makeTestFromPruned st dl = make dl st
729744
where
730745
make d s TestSeqStop
731-
| b : _ <- badActions @s d s = BadPrecondition TestSeqStop b s
732-
| stuck d s = Stuck TestSeqStop s
733-
| otherwise = DLScript TestSeqStop
746+
| b : _ <- badActions @s d s = BadPrecondition s TestSeqStop b s
747+
| stuck d s = Stuck s TestSeqStop s
748+
| otherwise = DLScript s TestSeqStop
734749
make d s (TestSeqWitness a ss) =
735750
onDLTestSeq (TestSeqWitness a) $
736751
make
@@ -747,13 +762,7 @@ makeTestFromPruned dl = make dl initialAnnotatedState
747762
-- | If failed, return the prefix up to the failure. Also prunes the test in case the model has
748763
-- changed.
749764
unfailDLTest :: DynLogicModel s => DynLogic s -> DynLogicTest s -> DynLogicTest s
750-
unfailDLTest d test = makeTestFromPruned d $ pruneDLTest d steps
751-
where
752-
steps = case test of
753-
BadPrecondition as _ _ -> as
754-
Stuck as _ -> as
755-
DLScript as -> as
756-
Looping as -> as
765+
unfailDLTest d test = makeTestFromPruned (getInitialState test) d $ pruneDLTest (getInitialState test) d (getScript test)
757766

758767
stuck :: DynLogicModel s => DynLogic s -> Annotated s -> Bool
759768
stuck EmptySpec _ = True
@@ -778,8 +787,8 @@ stuck (ForAll _ _) _ = False
778787
stuck (Monitor _ d) s = stuck d s
779788

780789
scriptFromDL :: DynLogicTest s -> Actions s
781-
scriptFromDL (DLScript s) = Actions $ sequenceSteps s
782-
scriptFromDL _ = Actions []
790+
scriptFromDL (DLScript is s) = Actions (underlyingState is) $ sequenceSteps s
791+
scriptFromDL test = Actions (underlyingState $ getInitialState test) []
783792

784793
sequenceSteps :: TestSequence s -> [Step s]
785794
sequenceSteps (TestSeq ss) =
@@ -818,8 +827,8 @@ badActions (ForAll _ _) _ = []
818827
badActions (Monitor _ d) s = badActions d s
819828

820829
applyMonitoring :: DynLogicModel s => DynLogic s -> DynLogicTest s -> Property -> Property
821-
applyMonitoring d (DLScript s) p =
822-
case findMonitoring d initialAnnotatedState s of
830+
applyMonitoring d (DLScript is s) p =
831+
case findMonitoring d is s of
823832
Just f -> f p
824833
Nothing -> p
825834
applyMonitoring _ Stuck{} p = p

0 commit comments

Comments
 (0)