diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -9,6 +9,11 @@ ## UNRELEASED +## 3.2.0 + +* Added support for negative testing via `validFailingAction` and `postconditionOnFailure` + callbacks in `StateModel` and `RunModel`. + ## 3.1.1 - 2023-06-26 * Added instances for `HasVariables` with custom error messages to avoid the issue of diff --git a/quickcheck-dynamic.cabal b/quickcheck-dynamic.cabal --- a/quickcheck-dynamic.cabal +++ b/quickcheck-dynamic.cabal @@ -1,16 +1,15 @@ -cabal-version: 2.2 -name: quickcheck-dynamic -version: 3.1.1 -license: Apache-2.0 +cabal-version: 2.2 +name: quickcheck-dynamic +version: 3.2.0 +license: Apache-2.0 license-files: LICENSE NOTICE -maintainer: arnaud.bailly@iohk.io -author: Ulf Norell -category: Testing -synopsis: - A library for stateful property-based testing +maintainer: arnaud.bailly@iohk.io +author: Ulf Norell +category: Testing +synopsis: A library for stateful property-based testing homepage: https://github.com/input-output-hk/quickcheck-dynamic#readme @@ -20,8 +19,8 @@ description: Please see the README on GitHub at -build-type: Simple -extra-doc-files: README.md +build-type: Simple +extra-doc-files: README.md extra-source-files: CHANGELOG.md source-repository head @@ -32,54 +31,75 @@ default-language: Haskell2010 default-extensions: ConstraintKinds - QuantifiedConstraints DataKinds - DeriveFunctor + DefaultSignatures + DeriveDataTypeable DeriveFoldable + DeriveFunctor + DeriveGeneric DeriveTraversable - DeriveDataTypeable - StandaloneDeriving + DerivingVia + FlexibleContexts + FlexibleInstances + GADTs + GeneralizedNewtypeDeriving ImportQualifiedPost - TupleSections LambdaCase + MultiParamTypeClasses PatternSynonyms - GADTs - TypeApplications + QuantifiedConstraints + RankNTypes ScopedTypeVariables + StandaloneDeriving + TupleSections + TypeApplications TypeFamilies - FlexibleContexts - FlexibleInstances - MultiParamTypeClasses - RankNTypes - ViewPatterns - DefaultSignatures TypeOperators - DerivingVia - DeriveGeneric - GeneralizedNewtypeDeriving + ViewPatterns ghc-options: -Wall -Wnoncanonical-monad-instances -Wunused-packages -Wincomplete-uni-patterns -Wincomplete-record-updates - -Wredundant-constraints -Widentities - -Wno-unused-do-bind + -Wredundant-constraints -Widentities -Wno-unused-do-bind library - import: lang - hs-source-dirs: src - exposed-modules: - Test.QuickCheck.DynamicLogic - Test.QuickCheck.DynamicLogic.CanGenerate - Test.QuickCheck.DynamicLogic.Internal - Test.QuickCheck.DynamicLogic.Quantify - Test.QuickCheck.DynamicLogic.SmartShrinking - Test.QuickCheck.DynamicLogic.Utils - Test.QuickCheck.Extras - Test.QuickCheck.StateModel - Test.QuickCheck.StateModel.Variables - build-depends: - QuickCheck -any, - base >= 4.7 && <5, - random -any, - mtl -any, - containers -any, + import: lang + hs-source-dirs: src + exposed-modules: + Test.QuickCheck.DynamicLogic + Test.QuickCheck.DynamicLogic.CanGenerate + Test.QuickCheck.DynamicLogic.Internal + Test.QuickCheck.DynamicLogic.Quantify + Test.QuickCheck.DynamicLogic.SmartShrinking + Test.QuickCheck.DynamicLogic.Utils + Test.QuickCheck.Extras + Test.QuickCheck.StateModel + Test.QuickCheck.StateModel.Variables + + build-depends: + , base >=4.7 && <5 + , containers + , mtl + , QuickCheck + , random + +test-suite quickcheck-dynamic-test + import: lang + type: exitcode-stdio-1.0 + main-is: Spec.hs + hs-source-dirs: test + other-modules: + Spec.DynamicLogic.Registry + Spec.DynamicLogic.RegistryModel + + ghc-options: -rtsopts + build-depends: + , base >=4.7 && <5 + , containers + , mtl + , QuickCheck + , quickcheck-dynamic + , stm + , tasty + , tasty-quickcheck + , tasty-test-reporter diff --git a/src/Test/QuickCheck/DynamicLogic.hs b/src/Test/QuickCheck/DynamicLogic.hs --- a/src/Test/QuickCheck/DynamicLogic.hs +++ b/src/Test/QuickCheck/DynamicLogic.hs @@ -9,6 +9,7 @@ module Test.QuickCheck.DynamicLogic ( DL, action, + failingAction, anyAction, anyActions, anyActions_, @@ -62,6 +63,9 @@ action :: (Typeable a, Eq (Action s a), Show (Action s a)) => Action s a -> DL s (Var a) action cmd = DL $ \_ k -> DL.after cmd k +failingAction :: (Typeable a, Eq (Action s a), Show (Action s a)) => Action s a -> DL s () +failingAction cmd = DL $ \_ k -> DL.afterNegative cmd (k ()) + anyAction :: DL s () anyAction = DL $ \_ k -> DL.afterAny $ k () @@ -129,28 +133,28 @@ runDL :: Annotated s -> DL s () -> DL.DynFormula s runDL s dl = unDL dl s $ \_ _ -> DL.passTest -forAllUniqueDL :: - (DL.DynLogicModel s, Testable a) => - Annotated s -> - DL s () -> - (Actions s -> a) -> - Property +forAllUniqueDL + :: (DL.DynLogicModel s, Testable a) + => Annotated s + -> DL s () + -> (Actions s -> a) + -> Property forAllUniqueDL initState d = DL.forAllUniqueScripts initState (runDL initState d) -forAllDL :: - (DL.DynLogicModel s, Testable a) => - DL s () -> - (Actions s -> a) -> - Property +forAllDL + :: (DL.DynLogicModel s, Testable a) + => DL s () + -> (Actions s -> a) + -> Property forAllDL d = DL.forAllScripts (runDL initialAnnotatedState d) -forAllMappedDL :: - (DL.DynLogicModel s, Testable a) => - (rep -> DL.DynLogicTest s) -> - (DL.DynLogicTest s -> rep) -> - (Actions s -> srep) -> - DL s () -> - (srep -> a) -> - Property +forAllMappedDL + :: (DL.DynLogicModel s, Testable a) + => (rep -> DL.DynLogicTest s) + -> (DL.DynLogicTest s -> rep) + -> (Actions s -> srep) + -> DL s () + -> (srep -> a) + -> Property forAllMappedDL to from fromScript d prop = DL.forAllMappedScripts to from (runDL initialAnnotatedState d) (prop . fromScript) diff --git a/src/Test/QuickCheck/DynamicLogic/Internal.hs b/src/Test/QuickCheck/DynamicLogic/Internal.hs --- a/src/Test/QuickCheck/DynamicLogic/Internal.hs +++ b/src/Test/QuickCheck/DynamicLogic/Internal.hs @@ -33,7 +33,7 @@ | -- | After a specific action the predicate should hold forall a. (Eq (Action s a), Show (Action s a), Typeable a) => - After (Action s a) (Var a -> DynPred s) + After (ActionWithPolarity s a) (Var a -> DynPred s) | Error String (DynPred s) | -- | Adjust the probability of picking a branch Weight Double (DynLogic s) @@ -64,15 +64,32 @@ afterAny :: (Annotated s -> DynFormula s) -> DynFormula s afterAny f = DynFormula $ \n -> AfterAny $ \s -> unDynFormula (f s) n +afterPolar + :: (Typeable a, Eq (Action s a), Show (Action s a)) + => ActionWithPolarity s a + -> (Var a -> Annotated s -> DynFormula s) + -> DynFormula s +afterPolar act f = DynFormula $ \n -> After act $ \x s -> unDynFormula (f x s) n + -- | Given `f` must be `True` after /some/ action. -- `f` is passed the state resulting from executing the `Action`. -after :: - (Typeable a, Eq (Action s a), Show (Action s a)) => - Action s a -> - (Var a -> Annotated s -> DynFormula s) -> - DynFormula s -after act f = DynFormula $ \n -> After act $ \x s -> unDynFormula (f x s) n +after + :: (Typeable a, Eq (Action s a), Show (Action s a)) + => Action s a + -> (Var a -> Annotated s -> DynFormula s) + -> DynFormula s +after act f = afterPolar (ActionWithPolarity act PosPolarity) f +-- | Given `f` must be `True` after /some/ negative action. +-- `f` is passed the state resulting from executing the `Action` +-- as a negative action. +afterNegative + :: (Typeable a, Eq (Action s a), Show (Action s a)) + => Action s a + -> (Annotated s -> DynFormula s) + -> DynFormula s +afterNegative act f = afterPolar (ActionWithPolarity act NegPolarity) (const f) + -- | Disjunction for DL formulae. -- Is `True` if either formula is `True`. The choice is /angelic/, ie. it is -- always made by the "caller". This is mostly important in case a test is @@ -88,11 +105,11 @@ -- for those values. `Quantifiable` values are thus values that can be generated -- and checked and the `Test.QuickCheck.DynamicLogic.Quantify` module defines -- basic combinators to build those from building blocks. -forAllQ :: - Quantifiable q => - q -> - (Quantifies q -> DynFormula s) -> - DynFormula s +forAllQ + :: Quantifiable q + => q + -> (Quantifies q -> DynFormula s) + -> DynFormula s forAllQ q f | isEmptyQ q' = ignore | otherwise = DynFormula $ \n -> ForAll q' $ ($ n) . unDynFormula . f @@ -137,7 +154,7 @@ data FailingAction s = ErrorFail String - | forall a. (Typeable a, Eq (Action s a)) => ActionFail (Action s a) + | forall a. (Typeable a, Eq (Action s a)) => ActionFail (ActionWithPolarity s a) instance StateModel s => HasVariables (FailingAction s) where getAllVariables ErrorFail{} = mempty @@ -145,13 +162,13 @@ instance StateModel s => Eq (FailingAction s) where ErrorFail s == ErrorFail s' = s == s' - ActionFail (a :: Action s a) == ActionFail (a' :: Action s a') + ActionFail (a :: ActionWithPolarity s a) == ActionFail (a' :: ActionWithPolarity s a') | Just Refl <- eqT @a @a' = a == a' _ == _ = False instance StateModel s => Show (FailingAction s) where show (ErrorFail s) = "Error " ++ show s - show (ActionFail a) = show a + show (ActionFail (ActionWithPolarity a pol)) = show pol ++ " : " ++ show a data DynLogicTest s = BadPrecondition (TestSequence s) (FailingAction s) (Annotated s) @@ -193,8 +210,10 @@ type TestStep s = Witnesses (Step s) newtype TestSequence s = TestSeq (Witnesses (TestContinuation s)) - deriving (Show, Eq) +deriving instance StateModel s => Show (TestSequence s) +deriving instance StateModel s => Eq (TestSequence s) + data TestContinuation s = ContStep (Step s) (TestSequence s) | ContStop @@ -285,7 +304,11 @@ where prettyBad :: FailingAction s -> String prettyBad (ErrorFail e) = "assert " ++ show e ++ " False" - prettyBad (ActionFail a) = "action $ " ++ show a ++ " -- Failed precondition\n pure ()" + prettyBad (ActionFail (ActionWithPolarity a p)) = f ++ " $ " ++ show a ++ " -- Failed precondition\n pure ()" + 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" @@ -309,26 +332,29 @@ restricted :: Action s a -> Bool restricted _ = False +restrictedPolar :: DynLogicModel s => ActionWithPolarity s a -> Bool +restrictedPolar (ActionWithPolarity a _) = restricted a + -- * Generate Properties -- | Simplest "execution" function for `DynFormula`. -- Turns a given a `DynFormula` paired with an interpreter function to produce some result from an --- `Actions` sequence into a proper `Property` than can then be run by QuickCheck. -forAllScripts :: - (DynLogicModel s, Testable a) => - DynFormula s -> - (Actions s -> a) -> - Property +forAllScripts + :: (DynLogicModel s, Testable a) + => DynFormula s + -> (Actions s -> a) + -> Property forAllScripts = forAllMappedScripts id id -- | `Property` function suitable for formulae without choice. -forAllUniqueScripts :: - (DynLogicModel s, Testable a) => - Annotated s -> - DynFormula s -> - (Actions s -> a) -> - Property +forAllUniqueScripts + :: (DynLogicModel s, Testable a) + => Annotated s + -> DynFormula s + -> (Actions s -> a) + -> Property forAllUniqueScripts s f k = QC.withSize $ \sz -> let d = unDynFormula f sz @@ -338,13 +364,13 @@ Just test -> validDLTest d 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) -> - (DynLogicTest s -> rep) -> - DynFormula s -> - (Actions s -> a) -> - Property +forAllMappedScripts + :: (DynLogicModel s, Testable a) + => (rep -> DynLogicTest s) + -> (DynLogicTest s -> rep) + -> DynFormula s + -> (Actions s -> a) + -> Property forAllMappedScripts to from f k = QC.withSize $ \n -> let d = unDynFormula f n @@ -383,14 +409,14 @@ addW Do{} ss = ss addW (Witness a w') ss = TestSeqWitness a (addW w' ss) -generate :: - (Monad m, DynLogicModel s) => - (Annotated s -> Int -> DynLogic s -> m (NextStep s)) -> - DynLogic s -> - Int -> - Annotated s -> - Int -> - m (DynLogicTest s) +generate + :: (Monad m, DynLogicModel s) + => (Annotated s -> Int -> DynLogic s -> m (NextStep s)) + -> DynLogic s + -> Int + -> Annotated s + -> Int + -> m (DynLogicTest s) generate chooseNextStepFun d n s size = if n > sizeLimit size then return $ Looping TestSeqStop @@ -504,10 +530,10 @@ AfterAny k -> do m <- keepTryingUntil 100 (computeArbitraryAction s) $ \case - Some act -> computePrecondition s act && not (restricted act) + Some act -> computePrecondition s act && not (restrictedPolar act) case m of Nothing -> return NoStep - Just (Some a) -> + Just (Some a@ActionWithPolarity{}) -> return $ Stepping (Do $ mkVar n := a) @@ -563,19 +589,19 @@ nextStateStep :: StateModel s => Step s -> Annotated s -> Annotated s nextStateStep (var := act) s = computeNextState s act var -shrinkScript :: DynLogicModel s => DynLogic s -> TestSequence s -> [TestSequence s] +shrinkScript :: forall s. DynLogicModel s => DynLogic s -> TestSequence s -> [TestSequence s] shrinkScript = shrink' initialAnnotatedState where - shrink' :: DynLogicModel s => Annotated s -> DynLogic s -> TestSequence s -> [TestSequence s] + shrink' :: Annotated s -> DynLogic s -> TestSequence s -> [TestSequence s] shrink' s d ss = structural s d ss ++ nonstructural s d ss nonstructural s d (TestSeqWitness a ss) = [ TestSeqWitness a' ss' - | a' <- shrinkWitness d a + | a' <- shrinkWitness @s d a , ss' <- ss : shrink' s (stepDLSeq d s $ TestSeqWitness a TestSeqStop) ss ] nonstructural s d (TestSeqStep step@(var := act) ss) = - [TestSeqStep (unsafeCoerceVar var := act') ss | Some act' <- computeShrinkAction s act] + [TestSeqStep (unsafeCoerceVar var := act') ss | Some act'@ActionWithPolarity{} <- computeShrinkAction s act] ++ [ TestSeqStep step ss' | ss' <- shrink' @@ -608,13 +634,13 @@ -- 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 :: DynLogicModel s => DynLogic s -> TestSequence s -> TestSequence s +pruneDLTest :: forall s. DynLogicModel s => DynLogic s -> TestSequence s -> TestSequence s pruneDLTest dl = prune [dl] initialAnnotatedState where prune [] _ _ = TestSeqStop prune _ _ TestSeqStop = TestSeqStop prune ds s (TestSeqWitness a ss) = - case [d' | d <- ds, d' <- stepDLW d a] of + case [d' | d <- ds, d' <- stepDLW @s d a] of [] -> prune ds s ss ds' -> TestSeqWitness a $ prune ds' s ss prune ds s (TestSeqStep step@(_ := act) ss) @@ -630,7 +656,7 @@ -- the type variables cleanly and do `Just Refl <- eqT ...` here instead. | Some a == Some act = [k (unsafeCoerceVar var) (computeNextState s act (unsafeCoerceVar var))] stepDL (AfterAny k) s (Do (var := act)) - | not (restricted act) = [k (computeNextState s act var)] + | not (restrictedPolar act) = [k (computeNextState s act var)] stepDL (Alt _ d d') s step = stepDL d s step ++ stepDL d' s step stepDL (Stopping d) s step = stepDL d s step stepDL (Weight _ d) s step = stepDL d s step @@ -641,7 +667,7 @@ stepDL (Monitor _f d) s step = stepDL d s step stepDL _ _ _ = [] -stepDLW :: forall a s. (DynLogicModel s, Typeable a) => DynLogic s -> a -> [DynLogic s] +stepDLW :: forall s a. (DynLogicModel s, Typeable a) => DynLogic s -> a -> [DynLogic s] stepDLW (ForAll (q :: Quantification a') k) a = case eqT @a @a' of Just Refl -> [k a | isaQ q a] @@ -684,11 +710,11 @@ getScript (Stuck s _) = s getScript (DLScript s) = s -makeTestFromPruned :: DynLogicModel s => DynLogic s -> TestSequence s -> DynLogicTest s +makeTestFromPruned :: forall s. DynLogicModel s => DynLogic s -> TestSequence s -> DynLogicTest s makeTestFromPruned dl = make dl initialAnnotatedState where make d s TestSeqStop - | b : _ <- badActions d s = BadPrecondition TestSeqStop b s + | b : _ <- badActions @s d s = BadPrecondition TestSeqStop b s | stuck d s = Stuck TestSeqStop s | otherwise = DLScript TestSeqStop make d s (TestSeqWitness a ss) = @@ -728,7 +754,7 @@ ( \case Some act -> computePrecondition s act - && not (restricted act) + && not (restrictedPolar act) ) stuck (Alt Angelic d d') s = stuck d s && stuck d' s stuck (Alt Demonic d d') s = stuck d s || stuck d' s @@ -799,7 +825,7 @@ where s' = computeNextState s a' (unsafeCoerceVar var) findMonitoring (AfterAny k) s as@(TestSeqStep (_var := a) _) - | not (restricted a) = findMonitoring (After a $ const k) s as + | not (restrictedPolar a) = findMonitoring (After a $ const k) s as findMonitoring (Alt _b d d') s as = -- Give priority to monitoring matches to the left. Combining both -- results in repeated monitoring from always, which is unexpected. diff --git a/src/Test/QuickCheck/DynamicLogic/Quantify.hs b/src/Test/QuickCheck/DynamicLogic/Quantify.hs --- a/src/Test/QuickCheck/DynamicLogic/Quantify.hs +++ b/src/Test/QuickCheck/DynamicLogic/Quantify.hs @@ -205,8 +205,8 @@ from (a, b, c, d) = (a, (b, (c, d))) instance - (Quantifiable a, Quantifiable b, Quantifiable c, Quantifiable d, Quantifiable e) => - Quantifiable (a, b, c, d, e) + (Quantifiable a, Quantifiable b, Quantifiable c, Quantifiable d, Quantifiable e) + => Quantifiable (a, b, c, d, e) where type Quantifies (a, b, c, d, e) = diff --git a/src/Test/QuickCheck/StateModel.hs b/src/Test/QuickCheck/StateModel.hs --- a/src/Test/QuickCheck/StateModel.hs +++ b/src/Test/QuickCheck/StateModel.hs @@ -15,6 +15,8 @@ WithUsedVars (..), Annotated (..), Step (..), + Polarity (..), + ActionWithPolarity (..), LookUp, Actions (..), pattern Actions, @@ -34,6 +36,7 @@ computePrecondition, computeArbitraryAction, computeShrinkAction, + failureResult, ) where import Control.Monad @@ -46,6 +49,7 @@ import Data.List import Data.Set qualified as Set import GHC.Generics +import GHC.Stack import Test.QuickCheck as QC import Test.QuickCheck.DynamicLogic.SmartShrinking import Test.QuickCheck.Monadic @@ -69,6 +73,12 @@ -- the action is /rejected/ and a new one is tried. This is also useful when shrinking a trace -- in order to ensure that removing some `Action` still produces a valid trace. The `precondition` can be -- somewhat redundant with the generator's conditions, +-- * `validFailingAction`: Specifies when an action that fails it's `precondition` can still run as what is +-- called a _negative_ action. This means that the action is (1) expected to fail and (2) not expected to +-- change the model state. This is very useful for testing the checks and failure conditions in the SUT +-- are implemented correctly. Should it be necessary to update the model state with e.g. book-keeping for +-- a negative action one can define `failureNextState` - but it is generally recommended to let this be +-- as simple an action as possible. class ( forall a. Show (Action state a) , forall a. HasVariables (Action state a) @@ -123,12 +133,24 @@ nextState :: Typeable a => state -> Action state a -> Var a -> state nextState s _ _ = s + -- | Transition function for negative actions. Note that most negative testing applications + -- should not require an implementation of this function! + failureNextState :: Typeable a => state -> Action state a -> state + failureNextState s _ = s + -- | Precondition for filtering generated `Action`. -- This function is applied before the action is performed, it is useful to refine generators that -- can produce more values than are useful. precondition :: state -> Action state a -> Bool precondition _ _ = True + -- | Precondition for filtering an `Action` that can meaningfully run but is supposed to fail. + -- An action will run as a _negative_ action if the `precondition` fails and `validFailingAction` succeeds. + -- A negative action should have _no effect_ on the model state. This may not be desierable in all + -- situations - in which case one can override this semantics for book-keeping in `failureNextState`. + validFailingAction :: state -> Action state a -> Bool + validFailingAction _ _ = False + deriving instance (forall a. Show (Action state a)) => Show (Any (Action state)) -- TODO: maybe it makes sense to write @@ -172,6 +194,13 @@ postcondition :: forall a. (state, state) -> Action state a -> LookUp m -> Realized m a -> PostconditionM m Bool postcondition _ _ _ _ = pure True + -- | Postcondition on the result of running a _negative_ `Action`. + -- The result is `assert`ed and will make the property fail should it be `False`. This is useful + -- to check the implementation produces e.g. the expected errors or to check that the SUT hasn't + -- been updated during the execution of the negative action. + postconditionOnFailure :: forall a. (state, state) -> Action state a -> LookUp m -> Realized m a -> PostconditionM m Bool + postconditionOnFailure _ _ _ _ = pure True + -- | Allows the user to attach additional information to the `Property` at each step of the process. -- This function is given the full transition that's been executed, including the start and ending -- `state`, the `Action`, the current environment to `Lookup` and the value produced by `perform` @@ -179,6 +208,20 @@ monitoring :: forall a. (state, state) -> Action state a -> LookUp m -> Realized m a -> Property -> Property monitoring _ _ _ _ prop = prop +-- | Indicate that the result of an action (in `perform`) +-- should not be inspected by the postcondition or appear +-- in a positive test. Useful when we want to give a type +-- for an `Action` like `SomeAct :: Action SomeState SomeType` +-- instead of `SomeAct :: Action SomeState (Either SomeError SomeType)` +-- but still need to return something in `perform` in the failure case. +failureResult :: HasCallStack => a +failureResult = error "A result of a failing action has been erronesouly inspected" + +computePostcondition :: forall m state a. RunModel state m => (state, state) -> ActionWithPolarity state a -> LookUp m -> Realized m a -> PostconditionM m Bool +computePostcondition ss (ActionWithPolarity a p) l r + | p == PosPolarity = postcondition ss a l r + | otherwise = postconditionOnFailure ss a l r + type LookUp m = forall a. Typeable a => Var a -> Realized m a type Env m = [EnvEntry m] @@ -210,26 +253,50 @@ data WithUsedVars a = WithUsedVars VarContext a +data Polarity + = PosPolarity + | NegPolarity + deriving (Ord, Eq) + +instance Show Polarity where + show PosPolarity = "+" + show NegPolarity = "-" + +data ActionWithPolarity state a = Eq (Action state a) => + ActionWithPolarity + { polarAction :: Action state a + , polarity :: Polarity + } + +instance HasVariables (Action state a) => HasVariables (ActionWithPolarity state a) where + getAllVariables = getAllVariables . polarAction + +deriving instance Eq (Action state a) => Eq (ActionWithPolarity state a) + data Step state where - (:=) :: - (Typeable a, Eq (Action state a), Show (Action state a)) => - Var a -> - Action state a -> - Step state + (:=) + :: (Typeable a, Eq (Action state a), Show (Action state a)) + => Var a + -> ActionWithPolarity state a + -> Step state infix 5 := instance (forall a. HasVariables (Action state a)) => HasVariables (Step state) where - getAllVariables (var := act) = Set.insert (Some var) $ getAllVariables act + getAllVariables (var := act) = Set.insert (Some var) $ getAllVariables (polarAction act) +funName :: Polarity -> String +funName PosPolarity = "action" +funName _ = "failingAction" + instance Show (Step state) where - show (var := act) = show var ++ " <- action $ " ++ show act + show (var := act) = show var ++ " <- " ++ funName (polarity act) ++ " $ " ++ show (polarAction act) instance Show (WithUsedVars (Step state)) where show (WithUsedVars ctx (var := act)) = if isWellTyped var ctx - then show var ++ " <- action $ " ++ show act - else "action $ " ++ show act + then show var ++ " <- " ++ funName (polarity act) ++ " $ " ++ show (polarAction act) + else funName (polarity act) ++ " $ " ++ show (polarAction act) instance Eq (Step state) where (v := act) == (v' := act') = @@ -270,7 +337,7 @@ go :: Annotated state -> [Step state] -> VarContext go aState [] = allVariables (underlyingState aState) go aState ((var := act) : steps) = - allVariables act + allVariables (polarAction act) <> allVariables (underlyingState aState) <> go (computeNextState aState act var) steps @@ -289,7 +356,7 @@ , do (mact, rej) <- satisfyPrecondition case mact of - Just (Some act) -> do + Just (Some act@ActionWithPolarity{}) -> do let var = mkVar step (as, rejected) <- arbActions (computeNextState s act var) (step + 1) return ((var := act) : as, rej ++ rejected) @@ -307,12 +374,12 @@ Some act -> if computePrecondition s act then return (Just (Some act), rej) - else go (m + 1) n (actionName act : rej) + else go (m + 1) n (actionName (polarAction act) : rej) shrink (Actions_ rs as) = map (Actions_ rs) (shrinkSmart (map (prune . map fst) . shrinkList shrinker . withStates) as) where - shrinker (v := act, s) = [(unsafeCoerceVar v := act', s) | Some act' <- computeShrinkAction s act] + shrinker (v := act, s) = [(unsafeCoerceVar v := act', s) | Some act'@ActionWithPolarity{} <- computeShrinkAction s act] -- Running state models @@ -327,77 +394,104 @@ initialAnnotatedState :: StateModel state => Annotated state initialAnnotatedState = Metadata mempty initialState -computePrecondition :: StateModel state => Annotated state -> Action state a -> Bool -computePrecondition s a = - all (\(Some v) -> v `isWellTyped` vars s) (getAllVariables a) - && precondition (underlyingState s) a +actionWithPolarity :: (StateModel state, Eq (Action state a)) => Annotated state -> Action state a -> ActionWithPolarity state a +actionWithPolarity s a = + let p + | precondition (underlyingState s) a = PosPolarity + | validFailingAction (underlyingState s) a = NegPolarity + | otherwise = PosPolarity + in ActionWithPolarity a p -computeNextState :: - (StateModel state, Typeable a) => - Annotated state -> - Action state a -> - Var a -> - Annotated state -computeNextState s a v = Metadata (extendContext (vars s) v) (nextState (underlyingState s) a v) +computePrecondition :: StateModel state => Annotated state -> ActionWithPolarity state a -> Bool +computePrecondition s (ActionWithPolarity a p) = + let polarPrecondition + | p == PosPolarity = precondition (underlyingState s) a + | otherwise = validFailingAction (underlyingState s) a && not (precondition (underlyingState s) a) + in all (\(Some v) -> v `isWellTyped` vars s) (getAllVariables a) + && polarPrecondition -computeArbitraryAction :: - StateModel state => - Annotated state -> - Gen (Any (Action state)) -computeArbitraryAction s = arbitraryAction (vars s) (underlyingState s) +computeNextState + :: (StateModel state, Typeable a) + => Annotated state + -> ActionWithPolarity state a + -> Var a + -> Annotated state +computeNextState s a v + | polarity a == PosPolarity = Metadata (extendContext (vars s) v) (nextState (underlyingState s) (polarAction a) v) + | otherwise = Metadata (vars s) (failureNextState (underlyingState s) (polarAction a)) -computeShrinkAction :: - (Typeable a, StateModel state) => - Annotated state -> - Action state a -> - [Any (Action state)] -computeShrinkAction s = shrinkAction (vars s) (underlyingState s) +computeArbitraryAction + :: StateModel state + => Annotated state + -> Gen (Any (ActionWithPolarity state)) +computeArbitraryAction s = do + Some a <- arbitraryAction (vars s) (underlyingState s) + pure $ Some $ actionWithPolarity s a -prune :: StateModel state => [Step state] -> [Step state] +computeShrinkAction + :: forall state a + . (Typeable a, StateModel state) + => Annotated state + -> ActionWithPolarity state a + -> [Any (ActionWithPolarity state)] +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 where loop _s [] = [] loop s ((var := act) : as) - | computePrecondition s act = + | computePrecondition @state s act = (var := act) : loop (computeNextState s act var) as | otherwise = loop s as -withStates :: StateModel state => [Step state] -> [(Step state, Annotated state)] +withStates :: forall state. StateModel state => [Step state] -> [(Step state, Annotated state)] withStates = loop initialAnnotatedState where loop _s [] = [] loop s ((var := act) : as) = - (var := act, s) : loop (computeNextState s act var) as + (var := act, s) : loop (computeNextState @state s act var) as -stateAfter :: StateModel state => Actions state -> Annotated state +stateAfter :: forall state. StateModel state => Actions state -> Annotated state stateAfter (Actions actions) = loop initialAnnotatedState actions where loop s [] = s - loop s ((var := act) : as) = loop (computeNextState s act var) as + loop s ((var := act) : as) = loop (computeNextState @state s act var) as -runActions :: - forall state m. - (StateModel state, RunModel state m) => - Actions state -> - PropertyM m (Annotated state, Env m) +runActions + :: forall state m + . (StateModel state, RunModel state m) + => Actions state + -> PropertyM m (Annotated state, Env m) runActions (Actions_ rejected (Smart _ actions)) = loop initialAnnotatedState [] actions where loop :: Annotated state -> Env m -> [Step state] -> PropertyM m (Annotated state, Env m) loop _s env [] = do unless (null rejected) $ - monitor (tabulate "Actions rejected by precondition" rejected) + monitor $ + tabulate "Actions rejected by precondition" rejected return (_s, reverse env) loop s env ((v := act) : as) = do pre $ computePrecondition s act - ret <- run (perform (underlyingState s) act (lookUpVar env)) - let name = actionName act - monitor (tabulate "Actions" [name]) + ret <- run $ perform (underlyingState s) (polarAction act) (lookUpVar env) + let name = show (polarity act) ++ actionName (polarAction act) + monitor $ tabulate "Actions" [name] let var = unsafeCoerceVar v s' = computeNextState s act var env' = (var :== ret) : env - monitor (monitoring @state @m (underlyingState s, underlyingState s') act (lookUpVar env') ret) - (b, (Endo mon, Endo onFail)) <- run . runWriterT . runPost $ postcondition @state @m (underlyingState s, underlyingState s') act (lookUpVar env) ret + monitor $ tabulate "Action polarity" [show $ polarity act] + monitor $ monitoring @state @m (underlyingState s, underlyingState s') (polarAction act) (lookUpVar env') ret + (b, (Endo mon, Endo onFail)) <- + run + . runWriterT + . runPost + $ computePostcondition @m + (underlyingState s, underlyingState s') + act + (lookUpVar env) + ret monitor mon unless b $ monitor onFail assert b diff --git a/src/Test/QuickCheck/StateModel/Variables.hs b/src/Test/QuickCheck/StateModel/Variables.hs --- a/src/Test/QuickCheck/StateModel/Variables.hs +++ b/src/Test/QuickCheck/StateModel/Variables.hs @@ -141,12 +141,12 @@ instance {-# OVERLAPPABLE #-} ( Break - (TypeError ( 'Text "Missing instance of HasVariables for non-Generic type " ':<>: 'ShowType a)) + (TypeError ('Text "Missing instance of HasVariables for non-Generic type " ':<>: 'ShowType a)) (Rep a) , Generic a , GenericHasVariables (Rep a) - ) => - HasVariables a + ) + => HasVariables a where getAllVariables = genericGetAllVariables . from diff --git a/test/Spec.hs b/test/Spec.hs new file mode 100644 --- /dev/null +++ b/test/Spec.hs @@ -0,0 +1,17 @@ +{-# LANGUAGE OverloadedStrings #-} + +module Main (main) where + +import Spec.DynamicLogic.RegistryModel qualified +import Test.Tasty +import Test.Tasty.Runners.Reporter qualified as Reporter + +main :: IO () +main = defaultMainWithIngredients [Reporter.ingredient] tests + +tests :: TestTree +tests = + testGroup + "dynamic logic" + [ Spec.DynamicLogic.RegistryModel.tests + ] diff --git a/test/Spec/DynamicLogic/Registry.hs b/test/Spec/DynamicLogic/Registry.hs new file mode 100644 --- /dev/null +++ b/test/Spec/DynamicLogic/Registry.hs @@ -0,0 +1,50 @@ +-- A simple local name service for threads... behaves like the Erlang +-- process registry. +module Spec.DynamicLogic.Registry where + +import Control.Concurrent.STM +import Control.Monad +import GHC.Conc + +type Registry = TVar [(String, ThreadId)] + +isAlive :: ThreadId -> IO Bool +isAlive tid = do + s <- threadStatus tid + return $ s /= ThreadFinished && s /= ThreadDied + +setupRegistry :: IO Registry +setupRegistry = atomically $ newTVar [] + +whereis :: Registry -> String -> IO (Maybe ThreadId) +whereis registry name = do + reg <- readRegistry registry + return $ lookup name reg + +register :: Registry -> String -> ThreadId -> IO () +register registry name tid = do + ok <- isAlive tid + reg <- readRegistry registry + if ok && name `notElem` map fst reg && tid `notElem` map snd reg + then atomically $ do + reg' <- readTVar registry + if name `notElem` map fst reg' && tid `notElem` map snd reg' + then writeTVar registry ((name, tid) : reg') + else error "badarg" + else error "badarg" + +unregister :: Registry -> String -> IO () +unregister registry name = do + reg <- readRegistry registry + when (name `elem` map fst reg) $ do + atomically $ modifyTVar registry $ filter ((/= name) . fst) + +readRegistry :: Registry -> IO [(String, ThreadId)] +readRegistry registry = garbageCollect registry *> atomically (readTVar registry) + +garbageCollect :: Registry -> IO () +garbageCollect registry = do + reg <- atomically $ readTVar registry + garbage <- filterM (fmap not . isAlive) (map snd reg) + atomically $ modifyTVar registry $ filter ((`notElem` garbage) . snd) + return () diff --git a/test/Spec/DynamicLogic/RegistryModel.hs b/test/Spec/DynamicLogic/RegistryModel.hs new file mode 100644 --- /dev/null +++ b/test/Spec/DynamicLogic/RegistryModel.hs @@ -0,0 +1,271 @@ +module Spec.DynamicLogic.RegistryModel where + +import Control.Concurrent +import Control.Exception + +import GHC.Generics + +import Control.Monad.Reader +import Data.Either +import Data.List +import Data.Map (Map) +import Data.Map qualified as Map +import Test.QuickCheck +import Test.QuickCheck.Monadic hiding (assert) +import Test.QuickCheck.Monadic qualified as QC +import Test.Tasty hiding (after) + +import Test.Tasty.QuickCheck (testProperty) + +import Spec.DynamicLogic.Registry +import Test.QuickCheck.DynamicLogic +import Test.QuickCheck.Extras +import Test.QuickCheck.StateModel + +data RegState = RegState + { regs :: Map String (Var ThreadId) + , dead :: [Var ThreadId] + } + deriving (Show, Generic) + +deriving instance Show (Action RegState a) +deriving instance Eq (Action RegState a) + +instance HasVariables (Action RegState a) where + getAllVariables (Register _ v) = getAllVariables v + getAllVariables (KillThread v) = getAllVariables v + getAllVariables _ = mempty + +instance StateModel RegState where + data Action RegState a where + Spawn :: Action RegState ThreadId + WhereIs :: String -> Action RegState (Maybe ThreadId) + Register :: String -> Var ThreadId -> Action RegState (Either SomeException ()) + Unregister :: String -> Action RegState (Either SomeException ()) + KillThread :: Var ThreadId -> Action RegState () + + precondition s (Register name tid) = + name `Map.notMember` regs s + && tid `notElem` Map.elems (regs s) + && tid `notElem` dead s + precondition s (Unregister name) = + name `Map.member` regs s + precondition _ _ = True + + validFailingAction _ _ = True + + arbitraryAction ctx s = + frequency $ + [ + ( max 1 $ 10 - length (ctxAtType @ThreadId ctx) + , return $ Some Spawn + ) + , + ( 2 * Map.size (regs s) + , Some <$> (Unregister <$> probablyRegistered s) + ) + , + ( 10 + , Some <$> (WhereIs <$> probablyRegistered s) + ) + ] + ++ [ ( max 1 $ 3 - length (dead s) + , Some <$> (KillThread <$> arbitraryVar ctx) + ) + | not . null $ ctxAtType @ThreadId ctx + ] + ++ [ ( max 1 $ 10 - Map.size (regs s) + , Some <$> (Register <$> probablyUnregistered s <*> arbitraryVar ctx) + ) + | not . null $ ctxAtType @ThreadId ctx + ] + + shrinkAction ctx _ (Register name tid) = + [Some (Unregister name)] + ++ [Some (Register name' tid) | name' <- shrinkName name] + ++ [Some (Register name tid') | tid' <- shrinkVar ctx tid] + shrinkAction _ _ (Unregister name) = + Some (WhereIs name) : [Some (Unregister name') | name' <- shrinkName name] + shrinkAction _ _ (WhereIs name) = + [Some (WhereIs name') | name' <- shrinkName name] + shrinkAction _ _ Spawn = [] + shrinkAction ctx _ (KillThread tid) = + [Some (KillThread tid') | tid' <- shrinkVar ctx tid] + + initialState = RegState mempty [] + + nextState s Spawn _ = s + nextState s (Register name tid) _step = s{regs = Map.insert name tid (regs s)} + nextState s (Unregister name) _step = + s{regs = Map.delete name (regs s)} + nextState s (KillThread tid) _ = + s + { dead = tid : dead s + , regs = Map.filter (/= tid) (regs s) + } + nextState s WhereIs{} _ = s + +type RegM = ReaderT Registry IO + +instance RunModel RegState RegM where + perform _ Spawn _ = do + lift $ forkIO (threadDelay 10000000) + perform _ (Register name tid) env = do + reg <- ask + lift $ try $ register reg name (env tid) + perform _ (Unregister name) _ = do + reg <- ask + lift $ try $ unregister reg name + perform _ (WhereIs name) _ = do + reg <- ask + lift $ whereis reg name + perform _ (KillThread tid) env = do + lift $ killThread (env tid) + lift $ threadDelay 100 + + postcondition (s, _) (WhereIs name) env mtid = do + pure $ (env <$> Map.lookup name (regs s)) == mtid + postcondition _ Register{} _ res = do + pure $ isRight res + postcondition _ _ _ _ = pure True + + postconditionOnFailure (s, _) act@Register{} _ res = do + monitorPost $ + tabulate + "Reason for -Register" + [ why s act + | Left{} <- [res] + ] + pure $ isLeft res + postconditionOnFailure _s _ _ _ = pure True + + monitoring (_s, s') act@(showDictAction -> ShowDict) _ res = + counterexample (show res ++ " <- " ++ show act ++ "\n -- State: " ++ show s') + . tabulate "Registry size" [show $ Map.size (regs s')] + +data ShowDict a where + ShowDict :: Show (Realized RegM a) => ShowDict a + +showDictAction :: forall a. Action RegState a -> ShowDict a +showDictAction Spawn{} = ShowDict +showDictAction WhereIs{} = ShowDict +showDictAction Register{} = ShowDict +showDictAction Unregister{} = ShowDict +showDictAction KillThread{} = ShowDict + +instance DynLogicModel RegState where + restricted _ = False + +why :: RegState -> Action RegState a -> String +why s (Register name tid) = + unwords $ + ["name already registered" | name `Map.member` regs s] + ++ ["tid already registered" | tid `elem` Map.elems (regs s)] + ++ ["dead thread" | tid `elem` dead s] +why _ _ = "(impossible)" + +arbitraryName :: Gen String +arbitraryName = elements allNames + +probablyRegistered :: RegState -> Gen String +probablyRegistered s = oneof $ map pure (Map.keys $ regs s) ++ [arbitraryName] + +probablyUnregistered :: RegState -> Gen String +probablyUnregistered s = elements $ allNames ++ (allNames \\ Map.keys (regs s)) + +shrinkName :: String -> [String] +shrinkName name = [n | n <- allNames, n < name] + +allNames :: [String] +allNames = ["a", "b", "c", "d", "e"] + +prop_Registry :: Actions RegState -> Property +prop_Registry s = + monadicIO $ do + monitor $ counterexample "\nExecution\n" + reg <- lift setupRegistry + runPropertyReaderT (runActions s) reg + QC.assert True + +propDL :: DL RegState () -> Property +propDL d = forAllDL d prop_Registry + +-- DL helpers + +unregisterNameAndTid :: String -> Var ThreadId -> DL RegState () +unregisterNameAndTid name tid = do + s <- getModelStateDL + sequence_ + [ action $ Unregister name' + | (name', tid') <- Map.toList $ regs s + , name' == name || tid' == tid + ] + +unregisterTid :: Var ThreadId -> DL RegState () +unregisterTid tid = do + s <- getModelStateDL + sequence_ + [ action $ Unregister name + | (name, tid') <- Map.toList $ regs s + , tid' == tid + ] + +getAlive :: DL RegState [Var ThreadId] +getAlive = do + s <- getModelStateDL + ctx <- getVarContextDL + pure $ ctxAtType @ThreadId ctx \\ dead s + +pickThread :: DL RegState (Var ThreadId) +pickThread = do + tids <- ctxAtType @ThreadId <$> getVarContextDL + forAllQ $ elementsQ tids + +pickAlive :: DL RegState (Var ThreadId) +pickAlive = do + alive <- getAlive + forAllQ $ elementsQ alive + +pickFreshName :: DL RegState String +pickFreshName = do + used <- Map.keys . regs <$> getModelStateDL + forAllQ $ elementsQ (allNames \\ used) + +-- test that the registry never contains more than k processes + +regLimit :: Int -> DL RegState () +regLimit k = do + anyActions_ + assertModel "Too many processes" $ \s -> Map.size (regs s) <= k + +-- test that we can register a pid that is not dead, if we unregister the name first. + +canRegisterAlive :: String -> DL RegState () +canRegisterAlive name = do + tid <- pickAlive + unregisterNameAndTid name tid + action $ Register name tid + pure () + +canRegister :: DL RegState () +canRegister = do + anyActions_ + name <- pickFreshName + canRegisterAlive name + +canRegisterNoUnregister :: DL RegState () +canRegisterNoUnregister = do + anyActions_ + name <- pickFreshName + tid <- pickAlive + action $ Register name tid + pure () + +tests :: TestTree +tests = + testGroup + "registry model example" + [ testProperty "prop_Registry" $ prop_Registry + , testProperty "canRegister" $ propDL canRegister + , testProperty "canRegisterNoUnregister" $ expectFailure $ propDL canRegisterNoUnregister + ]