mirror of
https://github.com/barrucadu/dejafu.git
synced 2024-12-18 11:01:50 +03:00
Push fmap inside checkDiscard
This seems to improve matters significantly. Laziness!
This commit is contained in:
parent
552a0f3816
commit
100c2d3ab9
@ -504,7 +504,7 @@ sctBoundDiscard discard memtype cb conc = go initialState where
|
|||||||
|
|
||||||
if schedIgnore s
|
if schedIgnore s
|
||||||
then go newDPOR
|
then go newDPOR
|
||||||
else checkDiscard discard res trace <$> go (addBacktracks bpoints newDPOR)
|
else checkDiscard discard res trace $ go (addBacktracks bpoints newDPOR)
|
||||||
|
|
||||||
Nothing -> pure []
|
Nothing -> pure []
|
||||||
|
|
||||||
@ -563,7 +563,7 @@ sctUniformRandomDiscard discard memtype g0 lim0 conc = go g0 (max 0 lim0) where
|
|||||||
memtype
|
memtype
|
||||||
(initialRandSchedState Nothing g)
|
(initialRandSchedState Nothing g)
|
||||||
conc
|
conc
|
||||||
checkDiscard discard res trace <$> go (schedGen s) (n-1)
|
checkDiscard discard res trace $ go (schedGen s) (n-1)
|
||||||
|
|
||||||
-- | SCT via weighted random scheduling.
|
-- | SCT via weighted random scheduling.
|
||||||
--
|
--
|
||||||
@ -613,7 +613,7 @@ sctWeightedRandomDiscard discard memtype g0 lim0 use0 conc = go g0 (max 0 lim0)
|
|||||||
memtype
|
memtype
|
||||||
(initialRandSchedState (Just ws) g)
|
(initialRandSchedState (Just ws) g)
|
||||||
conc
|
conc
|
||||||
checkDiscard discard res trace <$> go (schedGen s) (n-1) (use-1) (schedWeights s)
|
checkDiscard discard res trace $ go (schedGen s) (n-1) (use-1) (schedWeights s)
|
||||||
|
|
||||||
-------------------------------------------------------------------------------
|
-------------------------------------------------------------------------------
|
||||||
-- Utilities
|
-- Utilities
|
||||||
@ -677,8 +677,8 @@ trueBound _ _ = True
|
|||||||
(&+&) b1 b2 ts dl = b1 ts dl && b2 ts dl
|
(&+&) b1 b2 ts dl = b1 ts dl && b2 ts dl
|
||||||
|
|
||||||
-- | Apply the discard function.
|
-- | Apply the discard function.
|
||||||
checkDiscard :: (a -> Maybe Discard) -> a -> [b] -> [(a, [b])] -> [(a, [b])]
|
checkDiscard :: Functor f => (a -> Maybe Discard) -> a -> [b] -> f [(a, [b])] -> f [(a, [b])]
|
||||||
checkDiscard discard res trace = case discard res of
|
checkDiscard discard res trace rest = case discard res of
|
||||||
Just DiscardResultAndTrace -> id
|
Just DiscardResultAndTrace -> rest
|
||||||
Just DiscardTrace -> ((res, []):)
|
Just DiscardTrace -> ((res, []):) <$> rest
|
||||||
Nothing -> ((res, trace):)
|
Nothing -> ((res, trace):) <$> rest
|
||||||
|
Loading…
Reference in New Issue
Block a user