packages feed

quickcheck-dynamic 3.1.1 → 3.2.0

raw patch · 10 files changed

+667/−180 lines, 10 filesdep +quickcheck-dynamicdep +stmdep +tasty

Dependencies added: quickcheck-dynamic, stm, tasty, tasty-quickcheck, tasty-test-reporter

Files

CHANGELOG.md view
@@ -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
quickcheck-dynamic.cabal view
@@ -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 <https://github.com/input-output-hk/quickcheck-dynamic#readme> -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
src/Test/QuickCheck/DynamicLogic.hs view
@@ -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)
src/Test/QuickCheck/DynamicLogic/Internal.hs view
@@ -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.
src/Test/QuickCheck/DynamicLogic/Quantify.hs view
@@ -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) =
src/Test/QuickCheck/StateModel.hs view
@@ -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
src/Test/QuickCheck/StateModel/Variables.hs view
@@ -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
+ test/Spec.hs view
@@ -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+    ]
+ test/Spec/DynamicLogic/Registry.hs view
@@ -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 ()
+ test/Spec/DynamicLogic/RegistryModel.hs view
@@ -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+    ]