diff --git a/quickcheck-dynamic/CHANGELOG.md b/quickcheck-dynamic/CHANGELOG.md index 93f0fc5..adda733 100644 --- a/quickcheck-dynamic/CHANGELOG.md +++ b/quickcheck-dynamic/CHANGELOG.md @@ -9,6 +9,16 @@ changes. ## UNRELEASED +* **BREAKING**: The `Actions` pattern now has a field for the initial state of + the actions sequence and the `runActions` function returns a triple with the + intial state, environment, and final state. + +* **BREAKING**: Made `initialState` `Gen state` instead of a `state` and + introduced `setup :: state -> m ()` to `RunModel`. + - To migrate an existing model simply replace `initialState = MyState{..}` + with `initialState = pure $ MyState{..}` and everything else should work + straight-forwardly. + * **BREAKING**: Removed `Realized` - To migrate uses of `Realized` with `IOSim`, index the state type on the choice of `RunModel` monad and index the relevant types: diff --git a/quickcheck-dynamic/src/Test/QuickCheck/DynamicLogic.hs b/quickcheck-dynamic/src/Test/QuickCheck/DynamicLogic.hs index 30713f2..942f075 100644 --- a/quickcheck-dynamic/src/Test/QuickCheck/DynamicLogic.hs +++ b/quickcheck-dynamic/src/Test/QuickCheck/DynamicLogic.hs @@ -27,6 +27,9 @@ module Test.QuickCheck.DynamicLogic ( forAllDL, forAllMappedDL, forAllUniqueDL, + forAllDLS, + forAllMappedDLS, + forAllUniqueDLS, DL.DynLogicModel (..), module Test.QuickCheck.DynamicLogic.Quantify, ) where @@ -131,22 +134,23 @@ forAllNonVariableQ :: QuantifyConstraints (HasNoVariables a) => Quantification a forAllNonVariableQ q = DL $ \s k -> DL.forAllQ (hasNoVariablesQ q) $ \(HasNoVariables x) -> k x s runDL :: Annotated s -> DL s () -> DL.DynFormula s -runDL s dl = unDL dl s $ \_ _ -> DL.passTest +runDL s dl = (unDL dl s $ \_ _ -> DL.passTest) forAllUniqueDL :: (DL.DynLogicModel s, Testable a) - => Annotated s - -> DL s () + => DL s () -> (Actions s -> a) -> Property -forAllUniqueDL initState d = DL.forAllUniqueScripts initState (runDL initState d) +forAllUniqueDL d p = + forAllBlind initialState $ \st -> forAllUniqueDLS st d p forAllDL :: (DL.DynLogicModel s, Testable a) => DL s () -> (Actions s -> a) -> Property -forAllDL d = DL.forAllScripts (runDL initialAnnotatedState d) +forAllDL d p = + forAllBlind initialState $ \st -> forAllDLS st d p forAllMappedDL :: (DL.DynLogicModel s, Testable a) @@ -157,4 +161,34 @@ forAllMappedDL -> (srep -> a) -> Property forAllMappedDL to from fromScript d prop = - DL.forAllMappedScripts to from (runDL initialAnnotatedState d) (prop . fromScript) + forAll initialState $ \st -> forAllMappedDLS st to from fromScript d prop + +forAllUniqueDLS + :: (DL.DynLogicModel s, Testable a) + => s + -> DL s () + -> (Actions s -> a) + -> Property +forAllUniqueDLS st d p = + DL.forAllUniqueScripts st (runDL (Metadata mempty st) d) p + +forAllDLS + :: (DL.DynLogicModel s, Testable a) + => s + -> DL s () + -> (Actions s -> a) + -> Property +forAllDLS st d p = + DL.forAllScripts st (runDL (Metadata mempty st) d) p + +forAllMappedDLS + :: (DL.DynLogicModel s, Testable a) + => s + -> (rep -> DL.DynLogicTest s) + -> (DL.DynLogicTest s -> rep) + -> (Actions s -> srep) + -> DL s () + -> (srep -> a) + -> Property +forAllMappedDLS st to from fromScript d prop = + DL.forAllMappedScripts st to from (runDL (Metadata mempty st) d) (prop . fromScript) diff --git a/quickcheck-dynamic/src/Test/QuickCheck/DynamicLogic/Internal.hs b/quickcheck-dynamic/src/Test/QuickCheck/DynamicLogic/Internal.hs index d838892..c25ccb9 100644 --- a/quickcheck-dynamic/src/Test/QuickCheck/DynamicLogic/Internal.hs +++ b/quickcheck-dynamic/src/Test/QuickCheck/DynamicLogic/Internal.hs @@ -171,10 +171,10 @@ instance StateModel s => Show (FailingAction s) where show (ActionFail (ActionWithPolarity a pol)) = show pol ++ " : " ++ show a data DynLogicTest s - = BadPrecondition (TestSequence s) (FailingAction s) (Annotated s) - | Looping (TestSequence s) - | Stuck (TestSequence s) (Annotated s) - | DLScript (TestSequence s) + = BadPrecondition (Annotated s) (TestSequence s) (FailingAction s) (Annotated s) + | Looping (Annotated s) (TestSequence s) + | Stuck (Annotated s) (TestSequence s) (Annotated s) + | DLScript (Annotated s) (TestSequence s) data Witnesses r where Do :: r -> Witnesses r @@ -295,8 +295,11 @@ prettyWitnesses (Witness a w) = ("_ <- forAllQ $ exactlyQ $ " ++ show a) : prett prettyWitnesses Do{} = [] instance StateModel s => Show (DynLogicTest s) where - show (BadPrecondition ss bad s) = - prettyTestSequence (usedVariables ss <> allVariables bad) ss + show (BadPrecondition is ss bad s) = + "-- Initial state: " + ++ show s + ++ "\n" + ++ prettyTestSequence (usedVariables is ss <> allVariables bad) ss ++ "\n -- In state: " ++ show s ++ "\n " @@ -309,12 +312,21 @@ instance StateModel s => Show (DynLogicTest s) where f | p == PosPolarity = "action" | otherwise = "failingAction" - show (Looping ss) = prettyTestSequence (usedVariables ss) ss ++ "\n pure ()\n -- Looping" - show (Stuck ss s) = prettyTestSequence (usedVariables ss) ss ++ "\n pure ()\n -- Stuck in state " ++ show s - show (DLScript ss) = prettyTestSequence (usedVariables ss) ss ++ "\n pure ()\n" + show (Looping is ss) = + showTest is ss + ++ "\n -- Looping" + show (Stuck is ss s) = + showTest is ss + ++ "\n -- Stuck in state " + ++ show s + show (DLScript is ss) = + showTest is ss -usedVariables :: forall s. StateModel s => TestSequence s -> VarContext -usedVariables = go initialAnnotatedState +showTest :: StateModel s => Annotated s -> TestSequence s -> String +showTest is ss = "-- Initial state: " ++ show is ++ "\n" ++ prettyTestSequence (usedVariables is ss) ss ++ "\n pure ()" + +usedVariables :: forall s. StateModel s => Annotated s -> TestSequence s -> VarContext +usedVariables s = go s where go :: Annotated s -> TestSequence s -> VarContext go aState TestSeqStop = allVariables (underlyingState aState) @@ -342,39 +354,42 @@ restrictedPolar (ActionWithPolarity a _) = restricted a -- `Actions` sequence into a proper `Property` that can be run by QuickCheck. forAllScripts :: (DynLogicModel s, Testable a) - => DynFormula s + => s + -- ^ The initial state + -> DynFormula s -> (Actions s -> a) -> Property -forAllScripts = forAllMappedScripts id id +forAllScripts s = forAllMappedScripts s id id -- | `Property` function suitable for formulae without choice. forAllUniqueScripts :: (DynLogicModel s, Testable a) - => Annotated s + => s + -- ^ The initial state -> DynFormula s -> (Actions s -> a) -> Property forAllUniqueScripts s f k = QC.withSize $ \sz -> let d = unDynFormula f sz - n = unsafeNextVarIndex $ vars s - in case generate chooseUniqueNextStep d n s 500 of + in case generate chooseUniqueNextStep d 1 (Metadata mempty s) 500 of Nothing -> counterexample "Generating Non-unique script in forAllUniqueScripts" False Just test -> validDLTest test . applyMonitoring d test . property $ k (scriptFromDL test) -- | Creates a `Property` from `DynFormula` with some specialised isomorphism for shrinking purpose. forAllMappedScripts :: (DynLogicModel s, Testable a) - => (rep -> DynLogicTest s) + => s + -> (rep -> DynLogicTest s) -> (DynLogicTest s -> rep) -> DynFormula s -> (Actions s -> a) -> Property -forAllMappedScripts to from f k = +forAllMappedScripts s to from f k = QC.withSize $ \n -> let d = unDynFormula f n in forAllShrinkBlind - (Smart 0 <$> sized ((from <$>) . generateDLTest d)) + (Smart 0 <$> sized ((from <$>) . generateDLTest (Metadata mempty s) d)) (shrinkSmart ((from <$>) . shrinkDLTest d . to)) $ \(Smart _ script) -> withDLScript d k (to script) @@ -405,17 +420,24 @@ validDLTest test prop = Stuck{} -> property Discard _other -> counterexample (show test) False -generateDLTest :: DynLogicModel s => DynLogic s -> Int -> Gen (DynLogicTest s) -generateDLTest d size = generate chooseNextStep d 0 (initialStateFor d) size +generateDLTest :: DynLogicModel s => Annotated s -> DynLogic s -> Int -> Gen (DynLogicTest s) +generateDLTest s d size = do + generate chooseNextStep d 0 s size onDLTestSeq :: (TestSequence s -> TestSequence s) -> DynLogicTest s -> DynLogicTest s -onDLTestSeq f (BadPrecondition ss bad s) = BadPrecondition (f ss) bad s -onDLTestSeq f (Looping ss) = Looping (f ss) -onDLTestSeq f (Stuck ss s) = Stuck (f ss) s -onDLTestSeq f (DLScript ss) = DLScript (f ss) +onDLTestSeq f (BadPrecondition is ss bad s) = BadPrecondition is (f ss) bad s +onDLTestSeq f (Looping is ss) = Looping is (f ss) +onDLTestSeq f (Stuck is ss s) = Stuck is (f ss) s +onDLTestSeq f (DLScript is ss) = DLScript is (f ss) -consDLTest :: TestStep s -> DynLogicTest s -> DynLogicTest s -consDLTest step = onDLTestSeq (step :>) +setDLTestState :: Annotated s -> DynLogicTest s -> DynLogicTest s +setDLTestState is (BadPrecondition _ ss bad s) = BadPrecondition is ss bad s +setDLTestState is (Looping _ ss) = Looping is ss +setDLTestState is (Stuck _ ss s) = Stuck is ss s +setDLTestState is (DLScript _ ss) = DLScript is ss + +consDLTest :: Annotated s -> TestStep s -> DynLogicTest s -> DynLogicTest s +consDLTest is step = setDLTestState is . onDLTestSeq (step :>) consDLTestW :: Witnesses () -> DynLogicTest s -> DynLogicTest s consDLTestW w = onDLTestSeq (addW w) @@ -433,15 +455,15 @@ generate -> m (DynLogicTest s) generate chooseNextStepFun d n s size = if n > sizeLimit size - then return $ Looping TestSeqStop + then return $ Looping s TestSeqStop else do let preferred = if n > size then stopping d else noStopping d - useStep (BadAction (Witnesses ws bad)) _ = return $ BadPrecondition (TestSeqStopW ws) bad s - useStep StoppingStep _ = return $ DLScript TestSeqStop + useStep (BadAction (Witnesses ws bad)) _ = return $ BadPrecondition s (TestSeqStopW ws) bad s + useStep StoppingStep _ = return $ DLScript s TestSeqStop useStep (Stepping step d') _ = case discardWitnesses step of var := act -> - consDLTest step + consDLTest s step <$> generate chooseNextStepFun d' @@ -451,15 +473,13 @@ generate chooseNextStepFun d n s size = useStep NoStep alt = alt foldr (\step k -> do try <- chooseNextStepFun s n step; useStep try k) - (return $ Stuck TestSeqStop s) + (return $ Stuck s TestSeqStop s) -- NOTE: we will cons on this `TestSeqStop` so the `s` will not be the same before + -- and after state when we get out of this function. [preferred, noAny preferred, d, noAny d] sizeLimit :: Int -> Int sizeLimit size = 2 * size + 20 -initialStateFor :: StateModel s => DynLogic s -> Annotated s -initialStateFor _ = initialAnnotatedState - stopping :: DynLogic s -> DynLogic s stopping EmptySpec = EmptySpec stopping Stop = Stop @@ -589,22 +609,28 @@ keepTryingUntil n g p = do if p x then return $ Just x else scale (+ 1) $ keepTryingUntil (n - 1) g p shrinkDLTest :: DynLogicModel s => DynLogic s -> DynLogicTest s -> [DynLogicTest s] -shrinkDLTest _ (Looping _) = [] +shrinkDLTest _ (Looping _ _) = [] shrinkDLTest d tc = - [ test | as' <- shrinkScript d (getScript tc), let pruned = pruneDLTest d as' - test = makeTestFromPruned d pruned, - -- Don't shrink a non-executable test case to an executable one. + [ test + | as' <- + shrinkScript + (underlyingState $ getInitialState tc) + d + (getScript tc) + , let pruned = pruneDLTest (getInitialState tc) d as' + test = makeTestFromPruned (getInitialState tc) d pruned + , -- Don't shrink a non-executable test case to an executable one. case (tc, test) of - (DLScript _, _) -> True - (_, DLScript _) -> False + (DLScript _ _, _) -> True + (_, DLScript _ _) -> False _ -> True ] nextStateStep :: StateModel s => Step s -> Annotated s -> Annotated s nextStateStep (var := act) s = computeNextState s act var -shrinkScript :: forall s. DynLogicModel s => DynLogic s -> TestSequence s -> [TestSequence s] -shrinkScript = shrink' initialAnnotatedState +shrinkScript :: forall s. DynLogicModel s => s -> DynLogic s -> TestSequence s -> [TestSequence s] +shrinkScript is = shrink' (Metadata mempty is) where shrink' :: Annotated s -> DynLogic s -> TestSequence s -> [TestSequence s] shrink' s d ss = structural s d ss ++ nonstructural s d ss @@ -648,8 +674,8 @@ shrinkWitness AfterAny{} _ = [] -- The result of pruning a list of actions is a prefix of a list of actions that -- could have been generated by the dynamic logic. -pruneDLTest :: forall s. DynLogicModel s => DynLogic s -> TestSequence s -> TestSequence s -pruneDLTest dl = prune [dl] initialAnnotatedState +pruneDLTest :: forall s. DynLogicModel s => Annotated s -> DynLogic s -> TestSequence s -> TestSequence s +pruneDLTest is dl = prune [dl] is where prune [] _ _ = TestSeqStop prune _ _ TestSeqStop = TestSeqStop @@ -710,27 +736,29 @@ demonicAlt ds = foldr1 (Alt Demonic) ds propPruningGeneratedScriptIsNoop :: DynLogicModel s => DynLogic s -> Property propPruningGeneratedScriptIsNoop d = - forAll (sized $ \n -> choose (1, max 1 n) >>= generateDLTest d) $ \test -> - let script = case test of - BadPrecondition s _ _ -> s - Looping s -> s - Stuck s _ -> s - DLScript s -> s - in script == pruneDLTest d script + forAll initialState $ \s -> + forAll (sized $ \n -> choose (1, max 1 n) >>= generateDLTest (Metadata mempty s) d) $ \test -> + getScript test == pruneDLTest (getInitialState test) d (getScript test) + +getInitialState :: DynLogicTest s -> Annotated s +getInitialState (BadPrecondition is _ _ _) = is +getInitialState (Looping is _) = is +getInitialState (Stuck is _ _) = is +getInitialState (DLScript is _) = is getScript :: DynLogicTest s -> TestSequence s -getScript (BadPrecondition s _ _) = s -getScript (Looping s) = s -getScript (Stuck s _) = s -getScript (DLScript s) = s +getScript (BadPrecondition _ s _ _) = s +getScript (Looping _ s) = s +getScript (Stuck _ s _) = s +getScript (DLScript _ s) = s -makeTestFromPruned :: forall s. DynLogicModel s => DynLogic s -> TestSequence s -> DynLogicTest s -makeTestFromPruned dl = make dl initialAnnotatedState +makeTestFromPruned :: forall s. DynLogicModel s => Annotated s -> DynLogic s -> TestSequence s -> DynLogicTest s +makeTestFromPruned st dl = make dl st where make d s TestSeqStop - | b : _ <- badActions @s d s = BadPrecondition TestSeqStop b s - | stuck d s = Stuck TestSeqStop s - | otherwise = DLScript TestSeqStop + | b : _ <- badActions @s d s = BadPrecondition s TestSeqStop b s + | stuck d s = Stuck s TestSeqStop s + | otherwise = DLScript s TestSeqStop make d s (TestSeqWitness a ss) = onDLTestSeq (TestSeqWitness a) $ make @@ -747,13 +775,7 @@ makeTestFromPruned dl = make dl initialAnnotatedState -- | If failed, return the prefix up to the failure. Also prunes the test in case the model has -- changed. unfailDLTest :: DynLogicModel s => DynLogic s -> DynLogicTest s -> DynLogicTest s -unfailDLTest d test = makeTestFromPruned d $ pruneDLTest d steps - where - steps = case test of - BadPrecondition as _ _ -> as - Stuck as _ -> as - DLScript as -> as - Looping as -> as +unfailDLTest d test = makeTestFromPruned (getInitialState test) d $ pruneDLTest (getInitialState test) d (getScript test) stuck :: DynLogicModel s => DynLogic s -> Annotated s -> Bool stuck EmptySpec _ = True @@ -778,8 +800,8 @@ stuck (ForAll _ _) _ = False stuck (Monitor _ d) s = stuck d s scriptFromDL :: DynLogicTest s -> Actions s -scriptFromDL (DLScript s) = Actions $ sequenceSteps s -scriptFromDL _ = Actions [] +scriptFromDL (DLScript is s) = Actions (underlyingState is) $ sequenceSteps s +scriptFromDL test = Actions (underlyingState $ getInitialState test) [] sequenceSteps :: TestSequence s -> [Step s] sequenceSteps (TestSeq ss) = @@ -818,8 +840,8 @@ badActions (ForAll _ _) _ = [] badActions (Monitor _ d) s = badActions d s applyMonitoring :: DynLogicModel s => DynLogic s -> DynLogicTest s -> Property -> Property -applyMonitoring d (DLScript s) p = - case findMonitoring d initialAnnotatedState s of +applyMonitoring d (DLScript is s) p = + case findMonitoring d is s of Just f -> f p Nothing -> p applyMonitoring _ Stuck{} p = p diff --git a/quickcheck-dynamic/src/Test/QuickCheck/StateModel.hs b/quickcheck-dynamic/src/Test/QuickCheck/StateModel.hs index 73e5fab..a533b09 100644 --- a/quickcheck-dynamic/src/Test/QuickCheck/StateModel.hs +++ b/quickcheck-dynamic/src/Test/QuickCheck/StateModel.hs @@ -32,7 +32,6 @@ module Test.QuickCheck.StateModel ( lookUpVar, lookUpVarMaybe, viewAtType, - initialAnnotatedState, computeNextState, computePrecondition, computeArbitraryAction, @@ -122,7 +121,7 @@ class shrinkAction _ _ _ = [] -- | Initial state of generated traces. - initialState :: state + initialState :: Gen state -- | Transition function for the model. -- The `Var a` parameter is useful to keep reference to actual value of type `a` produced @@ -202,6 +201,10 @@ class (forall a. Show (Action state a), Monad m) => RunModel state m where type Error state m = Void + -- | Perform setup with the generated initial state before running actions + setup :: state -> m () + setup _ = pure () + -- | Perform an `Action` in some `state` in the `Monad` `m`. This -- is the function that's used to exercise the actual stateful -- implementation, usually through various side-effects as permitted @@ -325,30 +328,34 @@ instance Eq (Step state) where -- We also collect a list of names of actions which were generated, -- but were then rejected by their precondition. -data Actions state = Actions_ [String] (Smart [Step state]) +data Actions state = Actions_ + { actionsRejected :: [String] + , actionsInitialState :: state + , actionsSteps :: Smart [Step state] + } deriving (Generic) -pattern Actions :: [Step state] -> Actions state -pattern Actions as <- - Actions_ _ (Smart _ as) +pattern Actions :: state -> [Step state] -> Actions state +pattern Actions state as <- + Actions_ _ state (Smart _ as) where - Actions as = Actions_ [] (Smart 0 as) + Actions state as = Actions_ [] state (Smart 0 as) {-# COMPLETE Actions #-} instance Semigroup (Actions state) where - Actions_ rs (Smart k as) <> Actions_ rs' (Smart _ as') = Actions_ (rs ++ rs') (Smart k (as <> as')) + Actions_ rs state (Smart k as) <> Actions_ rs' _ (Smart _ as') = Actions_ (rs ++ rs') state (Smart k (as <> as')) -instance Eq (Actions state) where - Actions as == Actions as' = as == as' +instance Eq state => Eq (Actions state) where + Actions state as == Actions state' as' = state == state' && as == as' instance StateModel state => Show (Actions state) where - show (Actions as) = - let as' = WithUsedVars (usedVariables (Actions as)) <$> as - in intercalate "\n" $ zipWith (++) ("do " : repeat " ") (map show as' ++ ["pure ()"]) + show (Actions state as) = + let as' = WithUsedVars (usedVariables (Actions state as)) <$> as + in intercalate "\n" $ ("-- initial state: " ++ show state) : zipWith (++) ("do " : repeat " ") (map show as' ++ ["pure ()"]) usedVariables :: forall state. StateModel state => Actions state -> VarContext -usedVariables (Actions as) = go initialAnnotatedState as +usedVariables (Actions state as) = go (Metadata mempty state) as where go :: Annotated state -> [Step state] -> VarContext go aState [] = allVariables (underlyingState aState) @@ -359,8 +366,9 @@ usedVariables (Actions as) = go initialAnnotatedState as instance forall state. StateModel state => Arbitrary (Actions state) where arbitrary = do - (as, rejected) <- arbActions initialAnnotatedState 1 - return $ Actions_ rejected (Smart 0 as) + state <- initialState + (as, rejected) <- arbActions (Metadata mempty state) 1 + return $ Actions_ rejected state (Smart 0 as) where arbActions :: Annotated state -> Int -> Gen ([Step state], [String]) arbActions s step = sized $ \n -> @@ -392,8 +400,8 @@ instance forall state. StateModel state => Arbitrary (Actions state) where then return (Just (Some act), rej) else go (m + 1) n (actionName (polarAction act) : rej) - shrink (Actions_ rs as) = - map (Actions_ rs) (shrinkSmart (map (prune . map fst) . concatMap customActionsShrinker . shrinkList shrinker . withStates) as) + shrink (Actions_ rs state as) = + map (Actions_ rs state) (shrinkSmart (map (prune state . map fst) . concatMap customActionsShrinker . shrinkList shrinker . withStates state) as) where shrinker :: (Step state, Annotated state) -> [(Step state, Annotated state)] shrinker (v := act, s) = [(unsafeCoerceVar v := act', s) | Some act'@ActionWithPolarity{} <- computeShrinkAction s act] @@ -419,9 +427,6 @@ data Annotated state = Metadata instance Show state => Show (Annotated state) where show (Metadata ctx s) = show ctx ++ " |- " ++ show s -initialAnnotatedState :: StateModel state => Annotated state -initialAnnotatedState = Metadata mempty initialState - actionWithPolarity :: (StateModel state, Eq (Action state a)) => Annotated state -> Action state a -> ActionWithPolarity state a actionWithPolarity s a = let p @@ -465,8 +470,8 @@ computeShrinkAction computeShrinkAction s (ActionWithPolarity a _) = [Some (actionWithPolarity s a') | Some a' <- shrinkAction (vars s) (underlyingState s) a] -prune :: forall state. StateModel state => [Step state] -> [Step state] -prune = loop initialAnnotatedState +prune :: forall state. StateModel state => state -> [Step state] -> [Step state] +prune state = loop (Metadata mempty state) where loop _s [] = [] loop s ((var := act) : as) @@ -475,15 +480,15 @@ prune = loop initialAnnotatedState | otherwise = loop s as -withStates :: forall state. StateModel state => [Step state] -> [(Step state, Annotated state)] -withStates = loop initialAnnotatedState +withStates :: forall state. StateModel state => state -> [Step state] -> [(Step state, Annotated state)] +withStates state = loop (Metadata mempty state) where loop _s [] = [] loop s ((var := act) : as) = (var := act, s) : loop (computeNextState @state s act var) as stateAfter :: forall state. StateModel state => Actions state -> Annotated state -stateAfter (Actions actions) = loop initialAnnotatedState actions +stateAfter (Actions state actions) = loop (Metadata mempty state) actions where loop s [] = s loop s ((var := act) : as) = loop (computeNextState @state s act var) as @@ -496,13 +501,14 @@ runActions , forall a. IsPerformResult e a ) => Actions state - -> PropertyM m (Annotated state, Env) -runActions (Actions_ rejected (Smart _ actions)) = do - (finalState, env) <- runSteps initialAnnotatedState [] actions + -> PropertyM m (state, Annotated state, Env) +runActions (Actions_ rejected state (Smart _ actions)) = do + run $ setup state + (finalState, env) <- runSteps (Metadata mempty state) [] actions unless (null rejected) $ monitor $ tabulate "Actions rejected by precondition" rejected - return (finalState, env) + return (state, finalState, env) -- | Core function to execute a sequence of `Step` given some initial `Env`ironment -- and `Annotated` state. diff --git a/quickcheck-dynamic/test/Spec/DynamicLogic/Counters.hs b/quickcheck-dynamic/test/Spec/DynamicLogic/Counters.hs index aa68c99..430c98e 100644 --- a/quickcheck-dynamic/test/Spec/DynamicLogic/Counters.hs +++ b/quickcheck-dynamic/test/Spec/DynamicLogic/Counters.hs @@ -25,11 +25,15 @@ instance StateModel SimpleCounter where arbitraryAction _ _ = pure $ Some IncSimple - initialState = SimpleCounter 0 + initialState = SimpleCounter <$> choose (1, 10) nextState SimpleCounter{count} IncSimple _ = SimpleCounter (count + 1) instance RunModel SimpleCounter (ReaderT (IORef Int) IO) where + setup st = do + ref <- ask + lift $ writeIORef ref (count st) + perform _ IncSimple _ = do ref <- ask lift $ atomicModifyIORef' ref (\count -> (succ count, count)) @@ -50,7 +54,7 @@ instance StateModel FailingCounter where arbitraryAction _ _ = pure $ Some Inc' - initialState = FailingCounter 0 + initialState = pure $ FailingCounter 0 nextState FailingCounter{failingCount} Inc' _ = FailingCounter (failingCount + 1) @@ -75,7 +79,7 @@ instance StateModel Counter where Inc :: Action Counter () Reset :: Action Counter Int - initialState = Counter 0 + initialState = pure $ Counter 0 arbitraryAction _ _ = frequency [(5, pure $ Some Inc), (1, pure $ Some Reset)] diff --git a/quickcheck-dynamic/test/Spec/DynamicLogic/RegistryModel.hs b/quickcheck-dynamic/test/Spec/DynamicLogic/RegistryModel.hs index f15707c..ebd4072 100644 --- a/quickcheck-dynamic/test/Spec/DynamicLogic/RegistryModel.hs +++ b/quickcheck-dynamic/test/Spec/DynamicLogic/RegistryModel.hs @@ -92,7 +92,7 @@ instance StateModel RegState where shrinkAction ctx _ (KillThread tid) = [Some (KillThread tid') | tid' <- shrinkVar ctx tid] - initialState = RegState mempty [] + initialState = pure $ RegState mempty [] nextState s Spawn _ = s nextState s (Register name tid) _step = s{regs = Map.insert name tid (regs s)} diff --git a/quickcheck-dynamic/test/Test/QuickCheck/StateModelSpec.hs b/quickcheck-dynamic/test/Test/QuickCheck/StateModelSpec.hs index 12add89..4486dbb 100644 --- a/quickcheck-dynamic/test/Test/QuickCheck/StateModelSpec.hs +++ b/quickcheck-dynamic/test/Test/QuickCheck/StateModelSpec.hs @@ -52,17 +52,18 @@ prop_counter as = monadicIO $ do assert True prop_returnsFinalState :: Actions SimpleCounter -> Property -prop_returnsFinalState actions@(Actions as) = +prop_returnsFinalState actions@(Actions _ as) = monadicIO $ do ref <- lift $ newIORef (0 :: Int) - (s, _) <- runPropertyReaderT (runActions actions) ref - assert $ count (underlyingState s) == length as + (is, s, _) <- runPropertyReaderT (runActions actions) ref + assert $ count (underlyingState s) - count is == length as prop_variablesIndicesAre1Based :: Actions SimpleCounter -> Property -prop_variablesIndicesAre1Based actions@(Actions as) = +prop_variablesIndicesAre1Based (Actions _ []) = property True +prop_variablesIndicesAre1Based actions@(Actions _ as) = noShrinking $ monadicIO $ do ref <- lift $ newIORef (0 :: Int) - (_, env) <- runPropertyReaderT (runActions actions) ref + (is, _, env) <- runPropertyReaderT (runActions actions) ref act <- pick $ choose (0, length as - 1) monitor $ counterexample $ @@ -71,7 +72,7 @@ prop_variablesIndicesAre1Based actions@(Actions as) = , "Actions: " <> show as , "Act: " <> show act ] - assert $ null as || lookUpVarMaybe env (mkVar $ act + 1) == Just act + assert $ lookUpVarMaybe env (mkVar $ act + 1) == Just (act + count is) prop_failsOnPostcondition :: Actions FailingCounter -> Property prop_failsOnPostcondition actions =