@@ -374,9 +374,6 @@ instance Eq (Actions state) where
374374instance StateModel state => Show (Actions state ) where
375375 show = showWithUsed emptyContext
376376
377- getSteps :: Actions state -> [Step state ]
378- getSteps (Actions ss) = ss
379-
380377showWithUsed :: StateModel state => VarContext -> Actions state -> String
381378showWithUsed ctx (Actions as) =
382379 let as' = WithUsedVars (combineContexts ctx $ usedVariables (Actions as)) <$> as
@@ -586,13 +583,15 @@ runActions (Actions_ rejected (Smart _ actions)) = do
586583 tabulate " Actions rejected by precondition" rejected
587584 return (finalState, env)
588585
589- bucket = \ n -> let (a, b) = go n in show a ++ " - " ++ show b
590- where
591- go n
592- | n < 100 = (d * 10 , d * 10 + 9 )
593- | otherwise = let (a, b) = go d in (a * 10 , b * 10 + 9 )
594- where
595- d = div n 10
586+ bucket :: Int -> String
587+ bucket n = show a ++ " - " ++ show b
588+ where
589+ (a, b) = go n
590+ go n
591+ | n < 100 = (d * 10 , d * 10 + 9 )
592+ | otherwise = let (a, b) = go d in (a * 10 , b * 10 + 9 )
593+ where
594+ d = div n 10
596595
597596-- | Core function to execute a sequence of `Step` given some initial `Env`ironment and `Annotated`
598597-- state. Return the list of action names and polarities to work around
@@ -735,7 +734,7 @@ genParActions = do
735734 return $ ParallelActions as threadA threadB
736735 where go :: [Step state ] -> VarContext -> VarContext -> [Int ] -> [Int ] -> Gen ([Int ], [Int ])
737736 go [] _ctxA _ctxB tA tB = return (reverse tA, reverse tB)
738- go (s @ (v := a) : ss) ctxA ctxB tA tB = do
737+ go ((v := a) : ss) ctxA ctxB tA tB = do
739738 let candidates = [ ' a' | a `wellTypedIn` ctxA ] ++ [ ' b' | a `wellTypedIn` ctxB ]
740739 i = unsafeVarIndex v
741740 if null candidates
@@ -803,7 +802,7 @@ runParActions pas = do
803802 monitorTrace env trA
804803 monitor $ counterexample " -- Monitoring thread B"
805804 monitorTrace env trB
806- let ilvs = interleavings trC trA trB
805+ let ilvs = prepend trC $ interleavings trA trB
807806 monitor $ tabulate " TraceTree size" (map (bucket . length ) ilvs)
808807 assert $ null ilvs || any (checkTrace initialAnnotatedState mempty ) ilvs
809808 -- TODO: stats collection and cleanup
@@ -839,15 +838,14 @@ checkTrace s env (Node (TraceStep r v (ActionWithPolarity a _)) trs) =
839838 r
840839 in computePrecondition s act && checkPost && (null trs || any (checkTrace s' env') trs)
841840
842- interleavings :: [a ] -> [a ] -> [a ] -> [Tree a ]
843- interleavings (p: ps) as bs = [Node p (interleavings ps as bs)]
844- interleavings _ [] bs = spine bs
845- interleavings _ as [] = spine as
846- interleavings _ (a: as) (b: bs) = [Node a (interleavings [] as (b: bs)), Node b (interleavings [] (a: as) bs)]
841+ prepend :: [a ] -> [Tree a ] -> [Tree a ]
842+ prepend [] ts = ts
843+ prepend (p: ps) ts = [Node p $ prepend ps ts]
847844
848- spine :: [a ] -> [Tree a ]
849- spine [] = []
850- spine (x: xs) = [Node x (spine xs)]
845+ interleavings :: [a ] -> [a ] -> [Tree a ]
846+ interleavings [] bs = prepend bs []
847+ interleavings as [] = prepend as []
848+ interleavings (a: as) (b: bs) = [Node a (interleavings as (b: bs)), Node b (interleavings (a: as) bs)]
851849
852850-- TODO:
853851-- - Decide how much of the old QCD interface we can afford to break
0 commit comments