Adding errors to actions to help negative testing (#58)

Also:

* Better error message for `lookUpVar`
* Fix bug in computePostcondition
* remove `failureResult` as it is no longer relevant
* A monitoring callback called when a positive action fails
* More human-friendly semantics for negative actions
* Add simplest possible model for a counter example (not a counterexample)
* updated changelog

---------

Co-authored-by: Ulf Norell <ulf.norell@gmail.com>

Author: MaximilianAlgehed

quickcheck-dynamic/CHANGELOG.md

@@ -10,6 +10,9 @@ changes.
 ## UNRELEASED
 
 * Added some lightweight negative-shrinking based on a simple dependency analysis.
+* Added the option to return errors from actions by defining `type Error state`.
+  When this is defined `perform` has return type `m (Either (Error state) (Realized m a))`,
+  when it is left as the default the type remains `m (Realized m a)`.
 
 ## 3.3.1
 

quickcheck-dynamic/quickcheck-dynamic.cabal

@@ -46,6 +46,7 @@ common lang
     ImportQualifiedPost
     LambdaCase
     MultiParamTypeClasses
+    MultiWayIf
     PatternSynonyms
     QuantifiedConstraints
     RankNTypes
@@ -89,6 +90,7 @@ test-suite quickcheck-dynamic-test
   main-is:        Spec.hs
   hs-source-dirs: test
   other-modules:
+    Spec.DynamicLogic.CounterModel
     Spec.DynamicLogic.Registry
     Spec.DynamicLogic.RegistryModel
 

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

@@ -162,7 +162,7 @@ instance StateModel s => HasVariables (FailingAction s) where
 
 instance StateModel s => Eq (FailingAction s) where
   ErrorFail s == ErrorFail s' = s == s'
-  ActionFail (a :: ActionWithPolarity s a) == ActionFail (a' :: ActionWithPolarity s a')
+  ActionFail (a :: ActionWithPolarity s a) == ActionFail (a' :: ActionWithPolarity s' a')
     | Just Refl <- eqT @a @a' = a == a'
   _ == _ = False
 

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

@@ -36,7 +36,6 @@ module Test.QuickCheck.StateModel (
   computePrecondition,
   computeArbitraryAction,
   computeShrinkAction,
-  failureResult,
 ) where
 
 import Control.Monad
@@ -49,8 +48,8 @@ import Data.Kind
 import Data.List
 import Data.Monoid (Endo (..))
 import Data.Set qualified as Set
+import Data.Void
 import GHC.Generics
-import GHC.Stack
 import Test.QuickCheck as QC
 import Test.QuickCheck.DynamicLogic.SmartShrinking
 import Test.QuickCheck.Monadic
@@ -97,14 +96,21 @@ class
   -- @
   --   data Action RegState a where
   --     Spawn      ::                           Action RegState ThreadId
-  --     Register   :: String -> Var ThreadId -> Action RegState (Either ErrorCall ())
+  --     Register   :: String -> Var ThreadId -> Action RegState ()
   --     KillThread :: Var ThreadId           -> Action RegState ()
   -- @
   --
   -- The @Spawn@ action should produce a @ThreadId@, whereas the @KillThread@ action does not return
   -- anything.
   data Action state a
 
+  -- | The type of errors that actions can throw. If this is defined as anything
+  -- other than `Void` `perform` is required to return `Either (Error state) a`
+  -- instead of `a`.
+  type Error state
+
+  type Error state = Void
+
   -- | Display name for `Action`.
   -- This is useful to provide sensible statistics about the distribution of `Action`s run
   -- when checking a property.
@@ -154,6 +160,22 @@ class
 
 deriving instance (forall a. Show (Action state a)) => Show (Any (Action state))
 
+-- | The result required of `perform` depending on the `Error` type
+-- of a state model. If there are no errors, `Error state = Void`, and
+-- so we don't need to specify if the action failed or not.
+type family PerformResult e a where
+  PerformResult Void a = a
+  PerformResult e a = Either e a
+
+class IsPerformResult e a where
+  performResultToEither :: PerformResult e a -> Either e a
+
+instance {-# OVERLAPPING #-} IsPerformResult Void a where
+  performResultToEither = Right
+
+instance {-# OVERLAPPABLE #-} (PerformResult e a ~ Either e a) => IsPerformResult e a where
+  performResultToEither = id
+
 -- TODO: maybe it makes sense to write
 -- out a long list of these instances
 type family Realized (m :: Type -> Type) a :: Type
@@ -179,7 +201,7 @@ monitorPost m = PostconditionM $ tell (Endo m, mempty)
 counterexamplePost :: Monad m => String -> PostconditionM m ()
 counterexamplePost c = PostconditionM $ tell (mempty, Endo $ counterexample c)
 
-class Monad m => RunModel state m where
+class (forall a. Show (Action state a), Monad m) => RunModel state m where
   -- | 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
@@ -190,40 +212,47 @@ class Monad m => RunModel state m where
   --
   -- The `Lookup` parameter provides an /environment/ to lookup `Var
   -- a` instances from previous steps.
-  perform :: forall a. Typeable a => state -> Action state a -> LookUp m -> m (Realized m a)
+  perform :: Typeable a => state -> Action state a -> LookUp m -> m (PerformResult (Error state) (Realized m a))
 
   -- | Postcondition on the `a` value produced at some step.
   -- The result is `assert`ed and will make the property fail should it be `False`. This is useful
   -- to check the implementation produces expected values.
-  postcondition :: forall a. (state, state) -> Action state a -> LookUp m -> Realized m a -> PostconditionM m Bool
+  postcondition :: (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 :: (state, state) -> Action state a -> LookUp m -> Either (Error state) (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`
   -- while executing this step.
-  monitoring :: forall a. (state, state) -> Action state a -> LookUp m -> Realized m a -> Property -> Property
+  monitoring :: (state, state) -> Action state a -> LookUp m -> Either (Error state) (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"
+  -- | Allows the user to attach additional information to the `Property` if a positive action fails.
+  monitoringFailure :: state -> Action state a -> LookUp m -> Error state -> Property -> Property
+  monitoringFailure _ _ _ _ prop = prop
 
-computePostcondition :: forall m state a. RunModel state m => (state, state) -> ActionWithPolarity state a -> LookUp m -> Realized m a -> PostconditionM m Bool
+computePostcondition
+  :: forall m state a
+   . RunModel state m
+  => (state, state)
+  -> ActionWithPolarity state a
+  -> LookUp m
+  -> Either (Error state) (Realized m a)
+  -> PostconditionM m Bool
 computePostcondition ss (ActionWithPolarity a p) l r
-  | p == PosPolarity = postcondition ss a l r
+  | p == PosPolarity = case r of
+      Right ra -> postcondition ss a l ra
+      -- NOTE: this is actually redundant as this handled
+      -- at the call site for this function, but this is
+      -- good hygiene?
+      Left _ -> pure False
   | otherwise = postconditionOnFailure ss a l r
 
 type LookUp m = forall a. Typeable a => Var a -> Realized m a
@@ -252,7 +281,7 @@ lookUpVarMaybe (((v' :: Var b) :== a) : env) v =
 
 lookUpVar :: Typeable a => Env m -> Var a -> Realized m a
 lookUpVar env v = case lookUpVarMaybe env v of
-  Nothing -> error $ "Variable " ++ show v ++ " is not bound!"
+  Nothing -> error $ "Variable " ++ show v ++ " is not bound at type " ++ show (typeRep v) ++ "!"
   Just a -> a
 
 data WithUsedVars a = WithUsedVars VarContext a
@@ -477,8 +506,12 @@ stateAfter (Actions actions) = loop initialAnnotatedState actions
     loop s ((var := act) : as) = loop (computeNextState @state s act var) as
 
 runActions
-  :: forall state m
-   . (StateModel state, RunModel state m)
+  :: forall state m e
+   . ( StateModel state
+     , RunModel state m
+     , e ~ Error state
+     , forall a. IsPerformResult e a
+     )
   => Actions state
   -> PropertyM m (Annotated state, Env m)
 runActions (Actions_ rejected (Smart _ actions)) = loop initialAnnotatedState [] actions
@@ -491,24 +524,37 @@ runActions (Actions_ rejected (Smart _ actions)) = loop initialAnnotatedState []
       return (_s, reverse env)
     loop s env ((v := act) : as) = do
       pre $ computePrecondition s act
-      ret <- run $ perform (underlyingState s) (polarAction act) (lookUpVar env)
+      ret <- run $ performResultToEither <$> 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 $ 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
-      loop s' env' as
+      if
+        | polarity act == PosPolarity
+        , Left err <- ret -> do
+            monitor $
+              monitoringFailure @state @m
+                (underlyingState s)
+                (polarAction act)
+                (lookUpVar env)
+                err
+            stop False
+        | otherwise -> do
+            let var = unsafeCoerceVar v
+                s' = computeNextState s act var
+                env'
+                  | Right val <- ret = (var :== val) : env
+                  | otherwise = env
+            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
+            loop s' env' as

quickcheck-dynamic/test/Spec.hs

@@ -2,6 +2,7 @@
 
 module Main (main) where
 
+import Spec.DynamicLogic.CounterModel qualified
 import Spec.DynamicLogic.RegistryModel qualified
 import Test.Tasty
 
@@ -13,4 +14,5 @@ tests =
   testGroup
     "dynamic logic"
     [ Spec.DynamicLogic.RegistryModel.tests
+    , Spec.DynamicLogic.CounterModel.tests
     ]

quickcheck-dynamic/test/Spec/DynamicLogic/CounterModel.hs

@@ -0,0 +1,57 @@
+module Spec.DynamicLogic.CounterModel where
+
+import Control.Monad.Reader
+import Data.IORef
+import Test.QuickCheck
+import Test.QuickCheck.Extras
+import Test.QuickCheck.Monadic
+import Test.QuickCheck.StateModel
+import Test.Tasty hiding (after)
+import Test.Tasty.QuickCheck
+
+data Counter = Counter Int
+  deriving (Show, Generic)
+
+deriving instance Show (Action Counter a)
+deriving instance Eq (Action Counter a)
+instance HasVariables (Action Counter a) where
+  getAllVariables _ = mempty
+
+instance StateModel Counter where
+  data Action Counter a where
+    Inc :: Action Counter ()
+    Reset :: Action Counter Int
+
+  initialState = Counter 0
+
+  arbitraryAction _ _ = frequency [(5, pure $ Some Inc), (1, pure $ Some Reset)]
+
+  nextState (Counter n) Inc _ = Counter (n + 1)
+  nextState _ Reset _ = Counter 0
+
+instance RunModel Counter (ReaderT (IORef Int) IO) where
+  perform _ Inc _ = do
+    ref <- ask
+    lift $ modifyIORef ref succ
+  perform _ Reset _ = do
+    ref <- ask
+    lift $ do
+      n <- readIORef ref
+      writeIORef ref 0
+      pure n
+
+  postcondition (Counter n, _) Reset _ res = pure $ n == res
+  postcondition _ _ _ _ = pure True
+
+prop_counter :: Actions Counter -> Property
+prop_counter as = monadicIO $ do
+  ref <- lift $ newIORef (0 :: Int)
+  runPropertyReaderT (runActions as) ref
+  assert True
+
+tests :: TestTree
+tests =
+  testGroup
+    "counter tests"
+    [ testProperty "prop_conter" $ prop_counter
+    ]

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

@@ -40,10 +40,12 @@ 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 ())
+    Register :: String -> Var ThreadId -> Action RegState ()
+    Unregister :: String -> Action RegState ()
     KillThread :: Var ThreadId -> Action RegState ()
 
+  type Error RegState = SomeException
+
   precondition s (Register name tid) =
     name `Map.notMember` regs s
       && tid `notElem` Map.elems (regs s)
@@ -109,7 +111,8 @@ type RegM = ReaderT Registry IO
 
 instance RunModel RegState RegM where
   perform _ Spawn _ = do
-    lift $ forkIO (threadDelay 10000000)
+    tid <- lift $ forkIO (threadDelay 10000000)
+    pure $ Right tid
   perform _ (Register name tid) env = do
     reg <- ask
     lift $ try $ register reg name (env tid)
@@ -118,24 +121,22 @@ instance RunModel RegState RegM where
     lift $ try $ unregister reg name
   perform _ (WhereIs name) _ = do
     reg <- ask
-    lift $ whereis reg name
+    res <- lift $ whereis reg name
+    pure $ Right res
   perform _ (KillThread tid) env = do
     lift $ killThread (env tid)
     lift $ threadDelay 100
+    pure $ Right ()
 
   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]
-        ]
+        [why s act]
     pure $ isLeft res
   postconditionOnFailure _s _ _ _ = pure True