store interleavings in a tree

Author: MaximilianAlgehed

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

@@ -69,6 +69,7 @@ import Test.QuickCheck.StateModel.Variables
 import Control.Concurrent
 import Control.Monad.Identity
 import Control.Arrow (first)
+import Data.Tree
 
 -- | The typeclass users implement to define a model against which to validate some implementation.
 --
@@ -576,13 +577,6 @@ runActions
   => Actions state
   -> PropertyM m (Annotated state, Env)
 runActions (Actions_ rejected (Smart _ actions)) = do
-  let bucket = \n -> let (a, b) = go n in show a ++ " - " ++ show b
-        where
-          go n
-            | n < 100 = (d * 10, d * 10 + 9)
-            | otherwise = let (a, b) = go d in (a * 10, b * 10 + 9)
-            where
-              d = div n 10
   monitor $ tabulate "# of actions" [show $ bucket $ length actions]
   (finalState, env, names, polars) <- runSteps initialAnnotatedState [] actions
   monitor $ tabulate "Actions" names
@@ -592,6 +586,14 @@ runActions (Actions_ rejected (Smart _ actions)) = do
       tabulate "Actions rejected by precondition" rejected
   return (finalState, env)
 
+bucket = \n -> let (a, b) = go n in show a ++ " - " ++ show b
+        where
+          go n
+            | n < 100 = (d * 10, d * 10 + 9)
+            | otherwise = let (a, b) = go d in (a * 10, b * 10 + 9)
+            where
+              d = div n 10
+
 -- | Core function to execute a sequence of `Step` given some initial `Env`ironment and `Annotated`
 -- state. Return the list of action names and polarities to work around
 -- https://github.com/nick8325/quickcheck/issues/416 causing repeated calls to tabulate being slow.
@@ -727,7 +729,7 @@ 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)) <- QC.arbitrary
   split <- QC.choose (0, length steps - 1)
-  let (common, post) = splitAt split steps
+  let (common, take 10 -> post) = splitAt split steps
       commonCtx = allVariables common
   (threadA, threadB) <- go post commonCtx commonCtx [] []
   return $ ParallelActions as threadA threadB
@@ -756,6 +758,7 @@ data TraceStep state m where
             -> TraceStep state m
 
 type Trace state m = [TraceStep state m]
+type TraceTree state m = Tree (TraceStep state m)
 
 runTracing :: ( RunModelPar state m
               , e ~ Error state m
@@ -800,8 +803,9 @@ runParActions pas = do
   monitorTrace env trA
   monitor $ counterexample "-- Monitoring thread B"
   monitorTrace env trB
-  let ilvs = map (trC ++) $ interleavings trA trB
-  assert $ any (checkTrace initialAnnotatedState mempty) ilvs
+  let ilvs = interleavings trC trA trB
+  monitor $ tabulate "TraceTree size" (map (bucket . length) ilvs)
+  assert $ null ilvs || any (checkTrace initialAnnotatedState mempty) ilvs
   -- TODO: stats collection and cleanup
 
 monitorTrace :: forall state m. (StateModel state, RunModelPar state m)
@@ -814,9 +818,8 @@ monitorTrace env (TraceStep r v step : tr) = do
     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
-checkTrace s env (TraceStep r v (ActionWithPolarity a _) : tr) =
+checkTrace :: forall state m. (StateModel state, RunModelPar state m) => Annotated state -> Env -> TraceTree state m -> Bool
+checkTrace s env (Node (TraceStep r v (ActionWithPolarity a _)) trs) =
   -- 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
@@ -834,14 +837,17 @@ checkTrace s env (TraceStep r v (ActionWithPolarity a _) : tr) =
                                       (polarAction act)
                                       (lookUpVar env')
                                       r
-    in computePrecondition s act && checkPost && checkTrace s' env' tr
-
-interleavings :: [a] -> [a] -> [[a]]
-interleavings [] bs = [bs]
-interleavings as [] = [as]
-interleavings (a:as) (b:bs) =
-  map (a:) (interleavings as (b:bs)) ++
-  map (b:) (interleavings (a:as) bs)
+    in computePrecondition s act && checkPost && (null trs || any (checkTrace s' env') trs)
+
+interleavings :: [a] -> [a] -> [a] -> [Tree a]
+interleavings (p:ps) as bs = [Node p (interleavings ps as bs)]
+interleavings _ [] bs = spine bs
+interleavings _ as [] = spine as
+interleavings _ (a:as) (b:bs) = [Node a (interleavings [] as (b:bs)), Node b (interleavings [] (a:as) bs)]
+
+spine :: [a] -> [Tree a]
+spine [] = []
+spine (x:xs) = [Node x (spine xs)]
 
 -- TODO:
 --  - Decide how much of the old QCD interface we can afford to break

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

@@ -107,11 +107,11 @@ instance RunModel Counter (ReaderT (IORef Int) IO) where
 instance RunModelPar Counter (ReaderT (IORef Int) IO) where
   performPar Inc _ = do
     ref <- ask
-    lift $ atomicModifyIORef ref (\ c -> (c+1, ()))
-    -- lift $ do
-    --   n <- readIORef ref
-    --   threadDelay 50000
-    --   writeIORef ref (n + 1)
+    -- lift $ atomicModifyIORef ref (\ c -> (c+1, ()))
+    lift $ do
+      n <- readIORef ref
+      threadDelay 5000
+      writeIORef ref (n + 1)
   performPar Reset _ = do
     ref <- ask
     lift $ atomicModifyIORef ref (\ c -> (0, c))