Inline the findSchedulePrefix predicate.

The function is only used in one place, with a constant
predicate. There was no point in it being a parameter.
This commit is contained in:
Michael Walker 2017-04-08 10:34:30 +01:00
parent 5f9ad29b1b
commit da09c2268a
2 changed files with 4 additions and 13 deletions

View File

@ -332,7 +332,7 @@ sctBound :: MonadRef r n
sctBound memtype cb conc = go initialState where
-- Repeatedly run the computation gathering all the results and
-- traces into a list until there are no schedules remaining to try.
go dp = case nextPrefix dp of
go dp = case findSchedulePrefix dp of
Just (prefix, conservative, sleep) -> do
(res, s, trace) <- runConcurrent scheduler
memtype
@ -348,9 +348,6 @@ sctBound memtype cb conc = go initialState where
Nothing -> pure []
-- Find the next schedule prefix.
nextPrefix = findSchedulePrefix (>=initialThread)
-- The DPOR scheduler.
scheduler = dporSched memtype (cBound cb)

View File

@ -116,18 +116,12 @@ initialState = DPOR
-- to-do set. The intent is to put the system into a new state when
-- executed with this initial sequence of scheduling decisions.
findSchedulePrefix
:: (ThreadId -> Bool)
-- ^ Some partitioning function, applied to the to-do decisions. If
-- there is an identifier which passes the test, it will be used,
-- rather than any which fail it. This allows a very basic way of
-- domain-specific prioritisation between otherwise equal choices,
-- which may be useful in some cases.
-> DPOR
:: DPOR
-> Maybe ([ThreadId], Bool, Map ThreadId ThreadAction)
findSchedulePrefix predicate = listToMaybe . go where
findSchedulePrefix = listToMaybe . go where
go dpor =
let prefixes = here dpor : map go' (M.toList $ dporDone dpor)
in case concatPartition (\(t:_,_,_) -> predicate t) prefixes of
in case concatPartition (\(t:_,_,_) -> t >= initialThread) prefixes of
([], choices) -> choices
(choices, _) -> choices