11{-# LANGUAGE RecordWildCards #-}
22{-# LANGUAGE AllowAmbiguousTypes #-}
3- module Test.QuickCheck.ParallelActions where
3+ module Test.QuickCheck.ParallelActions
4+ ( RunModelPar (.. )
5+ , Forking (.. )
6+ , ParallelActions
7+ , runParActions
8+ ) where
49
510import Data.Set qualified as Set
611import Control.Monad
@@ -39,6 +44,12 @@ threadActions ParallelActions{linearActions = Actions steps, ..} =
3944 | thread <- threads
4045 ]
4146
47+ firstParAction :: ParallelActions state -> Maybe Int
48+ firstParAction ParallelActions {.. }
49+ | null idxs = Nothing
50+ | otherwise = Just $ minimum idxs
51+ where idxs = concat threads
52+
4253instance StateModel state => Show (ParallelActions state ) where
4354 show pas =
4455 unlines $ [ " -- Common Prefix:"
@@ -55,13 +66,13 @@ instance StateModel state => Show (ParallelActions state) where
5566instance StateModel state => Arbitrary (ParallelActions state ) where
5667 arbitrary = genParActions
5768
58- shrink (ParallelActions actions trs) =
59- filter checkParallelActions $ [ ParallelActions actions $ filter ( not . null ) $ map (filter (`Set.member` vars )) trs
60- | actions <- shrink actions
61- , let vars = unsafeIndexSet $ allVariables actions
62- ] ++
63- [ ParallelActions actions $ trs ++ [ tr | not $ null tr ] ++ trs'
64- | (trs, _ : tr, trs') <- holes' trs ]
69+ shrink pas @ (ParallelActions actions trs) =
70+ [ ParallelActions actions $ map (filter (/= i )) trs | Just i <- [firstParAction pas]] ++
71+ filter checkParallelActions
72+ [ ParallelActions actions $ filter ( not . null ) $ map ( filter ( `Set.member` vars)) trs
73+ | actions <- shrink actions
74+ , let vars = unsafeIndexSet $ allVariables actions
75+ ]
6576
6677checkParallelActions :: StateModel state => ParallelActions state -> Bool
6778checkParallelActions pas = all (checkWellTypedness commonCtx) (threadActions pas)
@@ -151,7 +162,7 @@ runParActions pas = do
151162 monitor $ counterexample $ " \n -- Thread " ++ [n, ' :' ]
152163 monitorTrace used env tr
153164 let ilvs = prepend trC $ interleavings trs
154- monitor $ tabulate " TraceTree size" (map (bucket . length ) ilvs)
165+ monitor $ tabulate " Trace tree size" (map (bucket . length ) ilvs)
155166 assert $ null ilvs || any (checkTrace initialAnnotatedState mempty ) ilvs
156167 -- TODO: stats collection and cleanup
157168
@@ -204,10 +215,6 @@ holes :: [a] -> [(a, [a])]
204215holes [] = []
205216holes (a: as) = (a, as) : map (second (a: )) (holes as)
206217
207- holes' :: [a ] -> [([a ], a , [a ])]
208- holes' [] = []
209- holes' (a: as) = ([] , a, as) : [ (a: bs, a', as') | (bs, a', as') <- holes' as ]
210-
211218-- TODO:
212219-- - More examples
213220-- - Refactor normal QCD so that you don't have two implementations
0 commit comments