Make it work!

Author: MaximilianAlgehed

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

@@ -68,6 +68,7 @@ import Test.QuickCheck.Monadic
 import Test.QuickCheck.StateModel.Variables
 import Control.Concurrent
 import Control.Monad.Identity
+import Control.Arrow (first)
 
 -- | The typeclass users implement to define a model against which to validate some implementation.
 --
@@ -259,6 +260,9 @@ class RunModel state m => RunModelPar state m where
 
   postconditionPar :: (state, state) -> Action state a -> LookUp -> a -> PostconditionM Identity Bool
 
+  postconditionOnFailurePar :: (state, state) -> Action state a -> LookUp -> Either (Error state m) a -> PostconditionM Identity Bool
+  postconditionOnFailurePar _ _ _ _ = pure True
+
   monitoringPar :: Action state a -> LookUp -> Either (Error state m) a -> Property -> Property
   monitoringPar _ _ _ = id
 
@@ -423,10 +427,10 @@ moreActions r p =
 
 -- NOTE: indexed on state for forwards compatibility, e.g. when we
 -- want to give an explicit initial state
-data Options state = Options {actionLengthMultiplier :: Rational, negativeActions :: Bool}
+data Options state = Options {actionLengthMultiplier :: Rational}
 
 defaultOptions :: Options state
-defaultOptions = Options{actionLengthMultiplier = 1, negativeActions = True}
+defaultOptions = Options{actionLengthMultiplier = 1}
 
 -- | Generate arbitrary actions with the `GenActionsOptions`. More flexible than using the type-based
 -- modifiers.
@@ -454,15 +458,14 @@ generateActionsWithOptions Options{..} = do
               return (reverse steps, rejected)
         else return (reverse steps, rejected)
       where
-        correctPolarity polarity = negativeActions || polarity == PosPolarity
         satisfyPrecondition = sized $ \n -> go n (2 * n) [] -- idea copied from suchThatMaybe
         go m n rej
           | m > n = return (Nothing, rej)
           | otherwise = do
               a <- resize m $ computeArbitraryAction s
               case a of
                 Some act@ActionWithPolarity{..} ->
-                  if computePrecondition s act && correctPolarity polarity
+                  if computePrecondition s act
                     then return (Just (Some act), rej)
                     else go (m + 1) n (actionName polarAction : rej)
 
@@ -693,8 +696,6 @@ instance StateModel state => Show (ParallelActions state) where
             , show threadA
             , "-- Thread B"
             , show threadB
-            , "-- Indices"
-            , show (threadATags pas, threadBTags pas)
             ]
     where
       common = Actions $ commonActions pas
@@ -705,13 +706,24 @@ instance StateModel state => Arbitrary (ParallelActions state) where
   arbitrary = genParActions
 
   shrink (ParallelActions actions as bs) =
-    [ ParallelActions actions as bs | actions <- shrinkActionsWithOptions opts actions ]
-    where opts = defaultOptions{ negativeActions = False }
+    filter checkParallelActions [ ParallelActions actions as bs | actions <- QC.shrink actions ]
+
+checkParallelActions :: StateModel state => ParallelActions state -> Bool
+checkParallelActions pas = checkWellTypedness commonCtx threadA && checkWellTypedness commonCtx threadB
+  where
+    commonCtx = allVariables common
+    common = Actions $ commonActions pas
+    threadA = threadAActions pas
+    threadB = threadBActions pas
+
+checkWellTypedness :: StateModel state => VarContext -> [Step state] -> Bool
+checkWellTypedness _ [] = True
+checkWellTypedness ctx ((v := a) : ss) = a `wellTypedIn` ctx && checkWellTypedness (extendContext ctx v) ss
 
 genParActions :: forall state. StateModel state => Gen (ParallelActions state)
 genParActions = do
   -- The ~ works around a bug in ghc (https://gitlab.haskell.org/ghc/ghc/-/issues/22004) (which is not in all ghc versions ?!)
-  as@(~(Actions steps)) <- generateActionsWithOptions @state $ defaultOptions { negativeActions = False }
+  as@(~(Actions steps)) <- QC.arbitrary
   split <- QC.choose (0, length steps - 1)
   let (common, post) = splitAt split steps
       commonCtx = allVariables common
@@ -746,15 +758,14 @@ type Trace state m = [TraceStep state m]
 runTracing :: ( RunModelPar state m
               , e ~ Error state m
               , forall a. IsPerformResult e a
-              ) => Env -> [Step state] -> m (Trace state m)
-runTracing env [] = return []
+              ) => Env -> [Step state] -> m (Trace state m, Env)
+runTracing env [] = return ([], env)
 runTracing env ((v := ap):as) = do
   r <- performResultToEither <$> performPar (polarAction ap) (lookUpVar env)
   let step = TraceStep r v ap
-  case r of
-    -- Fail early because we don't support negative actions
-    Left err -> return [step]
-    Right res -> (step :) <$> runTracing ((v :== res) : env) as
+      env' | Right val <- r = (v :== val) : env
+           | otherwise      = env
+  (first (step :)) <$> runTracing env' as
 
 class Monad m => ForkYou m where
   forkThread :: m a -> m (m a)
@@ -777,40 +788,51 @@ runParActions :: ( StateModel state
                  , ForkYou m
                  ) => ParallelActions state -> PropertyM m ()
 runParActions pas = do
-  (s, env) <- runActions $ Actions $ commonActions pas
+  monitor $ counterexample "-- Monitoring main thread"
+  (trC, env) <- run $ runTracing mempty $ commonActions pas
   joinA <- run $ forkThread $ runTracing env (threadAActions pas)
   joinB <- run $ forkThread $ runTracing env (threadBActions pas)
-  trA <- run joinA
-  trB <- run joinB
-  monitor $ monitorTrace env trA
-  monitor $ monitorTrace env trB
-  let ilvs = interleavings trA trB
-  assert $ any (checkTrace s env) ilvs
+  (trA, _) <- run joinA
+  (trB, _) <- run joinB
+  monitor $ counterexample "-- Monitoring thread A"
+  monitorTrace env trA
+  monitor $ counterexample "-- Monitoring thread B"
+  monitorTrace env trB
+  let ilvs = map (trC ++) $ interleavings trA trB
+  assert $ any (checkTrace initialAnnotatedState mempty) ilvs
   -- TODO: stats collection and cleanup
 
 monitorTrace :: forall state m. (StateModel state, RunModelPar state m)
-             => Env -> Trace state m -> Property -> Property
-monitorTrace _env [] = id
-monitorTrace env (TraceStep r v step : tr) =
-  monitorTrace env' tr . monitoringPar @state @m (polarAction step) (lookUpVar env) r
+             => Env -> Trace state m -> PropertyM m ()
+monitorTrace _env [] = pure ()
+monitorTrace env (TraceStep r v step : tr) = do
+  monitor $ monitoringPar @state @m (polarAction step) (lookUpVar env) r
+  monitorTrace env' tr
   where
     env' | Right val <- r = (v :== val) : env
          | otherwise      = env
 
 checkTrace :: forall state m. (StateModel state, RunModelPar state m) => Annotated state -> Env -> Trace state m -> Bool
 checkTrace _ _ [] = True
--- NOTE that we don't support negative actions
-checkTrace _ _ (TraceStep Left{} _ _ : _) = False
-checkTrace s env (TraceStep (Right val) v act : tr) =
-    let pre = computePrecondition s act
-        s' = computeNextState s act v
-        env' = (v :== val) : env
-        (b, _) = runWriter . runPost $ postconditionPar @state @m
-                                            (underlyingState s, underlyingState s')
-                                            (polarAction act)
-                                            (lookUpVar env')
-                                            val
-    in pre && b && checkTrace s' env' tr
+checkTrace s env (TraceStep r v (ActionWithPolarity a _) : tr) =
+  -- NOTE: we need to re-compute the polarity of `a` here because it may be that the failure can be explained,
+  -- but only by the action failing when it was previous successful
+  let act = actionWithPolarity s a
+      s' = computeNextState s act v
+      env' | Right val <- r = (v :== val) : env
+           | otherwise      = env
+      checkPost | Right val <- r, polarity act == PosPolarity = fst . runWriter . runPost $ postconditionPar @state @m
+                                                                (underlyingState s, underlyingState s')
+                                                                (polarAction act)
+                                                                (lookUpVar env')
+                                                                val
+                | Left{} <- r, polarity act == PosPolarity = False
+                | otherwise = fst . runWriter . runPost $ postconditionOnFailurePar @state @m
+                                      (underlyingState s, underlyingState s')
+                                      (polarAction act)
+                                      (lookUpVar env')
+                                      r
+    in computePrecondition s act && checkPost && checkTrace s' env' tr
 
 interleavings :: [a] -> [a] -> [[a]]
 interleavings [] bs = [bs]
@@ -822,6 +844,4 @@ interleavings (a:as) (b:bs) =
 -- TODO:
 -- - Negative actions (because the actual interleaving might involve legitimate failures
 --   even if the linear sequence doesn't)
---   - Remove negativeActions flag
--- - Shrinking
---    - Check scoping after shrinking linear actions
+--   - Check negative postcondition and correct precondition in `checkTrace`

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

@@ -4,10 +4,13 @@
 -- test or use examples for various behaviours of the runtime.
 module Spec.DynamicLogic.Counters where
 
+import Control.Concurrent
 import Control.Monad.Reader
 import Data.IORef
-import Test.QuickCheck (frequency)
+import Test.QuickCheck (frequency, Property)
 import Test.QuickCheck.StateModel
+import Test.QuickCheck.Extras
+import Test.QuickCheck.Monadic
 
 -- A very simple model with a single action that always succeed in
 -- predictable way. This model is useful for testing the runtime.
@@ -85,13 +88,27 @@ instance StateModel Counter where
 instance RunModel Counter (ReaderT (IORef Int) IO) where
   perform _ Inc _ = do
     ref <- ask
-    lift $ modifyIORef ref succ
+    lift $ do
+      n <- readIORef ref
+      threadDelay 1000
+      writeIORef ref (n + 1)
   perform _ Reset _ = do
     ref <- ask
     lift $ do
       n <- readIORef ref
+      threadDelay 1000
       writeIORef ref 0
       pure n
 
   postcondition (Counter n, _) Reset _ res = pure $ n == res
   postcondition _ _ _ _ = pure True
+
+
+instance RunModelPar Counter (ReaderT (IORef Int) IO) where
+  postconditionPar (Counter n, _) Reset _ res = pure $ n == res
+  postconditionPar _ _ _ _ = pure True
+
+prop_counter_par :: ParallelActions Counter -> Property
+prop_counter_par as = monadicIO $ do
+  ref <- lift $ newIORef (0 :: Int)
+  runPropertyReaderT (runParActions as) ref

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

@@ -151,6 +151,14 @@ instance RunModelPar RegState RegM where
     return $ (env <$> Map.lookup name (regs s)) == mtid
   postconditionPar _ _ _ _ = return True
 
+  postconditionOnFailurePar (s, _) act@Register{} _ res = do
+    monitorPost $
+      QC.tabulate
+        "Reason for -Register"
+        [why s act]
+    pure $ isLeft res
+  postconditionOnFailurePar _ _ _ _ = pure True
+
   monitoringPar act@(showDictAction -> ShowDict) _ res =
     QC.counterexample (show res ++ " <- " ++ show act)