From 148cd0a351fba6e340d6efd1ceaf907136e7c5bd Mon Sep 17 00:00:00 2001 From: Michael Walker Date: Tue, 21 Jul 2015 14:16:34 +0100 Subject: [PATCH] Gradually accumulate allThreads in findBacktrack. Recomputing it every single time is a waste of effort. --- Test/DejaFu/SCT/Internal.hs | 38 ++++++++++++++++++------------------- 1 file changed, 19 insertions(+), 19 deletions(-) diff --git a/Test/DejaFu/SCT/Internal.hs b/Test/DejaFu/SCT/Internal.hs index d4f8a28..9b45226 100755 --- a/Test/DejaFu/SCT/Internal.hs +++ b/Test/DejaFu/SCT/Internal.hs @@ -102,28 +102,28 @@ findBacktrack :: ([BacktrackStep] -> Int -> ThreadId -> [BacktrackStep]) -> [(NonEmpty (ThreadId, ThreadAction'), [ThreadId])] -> Trace' -> [BacktrackStep] -findBacktrack backtrack = go [] where - go bs ((e,i):is) ((d,_,a):ts) = - let this = BacktrackStep { _decision = (d, a), _runnable = map fst . toList $ e, _backtrack = map (\i' -> (i', False)) i } - bs' = doBacktrack (toList e) bs - in go (bs' ++ [this]) is ts - go bs _ _ = bs +findBacktrack backtrack = go [] [] where + go allThreads bs ((e,i):is) ((d,_,a):ts) = + let this = BacktrackStep { _decision = (d, a), _runnable = map fst . toList $ e, _backtrack = map (\i' -> (i', False)) i } + bs' = doBacktrack allThreads (toList e) bs + allThreads' = nub $ allThreads ++ _runnable this + in go allThreads' (bs' ++ [this]) is ts + go _ bs _ _ = bs - doBacktrack enabledThreads bs = - let idxs = [ (maximum is, u) - | (u, n) <- enabledThreads - , v <- allThreads bs - , u /= v - , let is = [ i - | (i, (t, b)) <- zip [0..] $ tidTag (fst . _decision) 0 bs - , t == v - , dependent' (snd $ _decision b) (u, n) - ] - , not $ null is] :: [(Int, ThreadId)] + doBacktrack allThreads enabledThreads bs = + let tagged = zip [0..] $ tidTag (fst . _decision) 0 bs + idxs = [ (maximum is, u) + | (u, n) <- enabledThreads + , v <- allThreads + , u /= v + , let is = [ i + | (i, (t, b)) <- tagged + , t == v + , dependent' (snd $ _decision b) (u, n) + ] + , not $ null is] :: [(Int, ThreadId)] in foldl' (\bs (i, u) -> backtrack bs i u) bs idxs - allThreads = nub . concatMap _runnable - -- | Add a new trace to the tree, creating a new subtree. grow :: Bool -> Trace' -> BPOR -> BPOR grow conservative = grow' initialCVState 0 where