module Test.DejaFu.Utils where
import Control.Exception (Exception(..), displayException)
import Data.List (intercalate, minimumBy)
import Data.Maybe (mapMaybe)
import Data.Ord (comparing)
import Test.DejaFu.Types
toTIdTrace :: Trace -> [(ThreadId, ThreadAction)]
toTIdTrace :: Trace -> [(ThreadId, ThreadAction)]
toTIdTrace =
forall a. [a] -> [a]
tail forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall b a. (b -> a -> b) -> b -> [a] -> [b]
scanl (\(ThreadId
t, ThreadAction
_) (Decision
d, [(ThreadId, Lookahead)]
_, ThreadAction
a) -> (ThreadId -> Decision -> ThreadId
tidOf ThreadId
t Decision
d, ThreadAction
a)) (ThreadId
initialThread, forall a. HasCallStack => a
undefined)
showTrace :: Trace -> String
showTrace :: Trace -> String
showTrace [] = String
"<trace discarded>"
showTrace Trace
trc = forall a. [a] -> [[a]] -> [a]
intercalate String
"\n" forall a b. (a -> b) -> a -> b
$ forall {b}. Bool -> [(Decision, b, ThreadAction)] -> String
go Bool
False Trace
trc forall a. a -> [a] -> [a]
: [String]
strkey where
go :: Bool -> [(Decision, b, ThreadAction)] -> String
go Bool
_ ((Decision
_,b
_,CommitIORef ThreadId
_ IORefId
_):[(Decision, b, ThreadAction)]
rest) = String
"C-" forall a. [a] -> [a] -> [a]
++ Bool -> [(Decision, b, ThreadAction)] -> String
go Bool
False [(Decision, b, ThreadAction)]
rest
go Bool
_ ((Start (ThreadId (Id Maybe String
_ Int
i)),b
_,ThreadAction
a):[(Decision, b, ThreadAction)]
rest) = String
"S" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
i forall a. [a] -> [a] -> [a]
++ String
"-" forall a. [a] -> [a] -> [a]
++ Bool -> [(Decision, b, ThreadAction)] -> String
go (ThreadAction -> Bool
didYield ThreadAction
a) [(Decision, b, ThreadAction)]
rest
go Bool
y ((SwitchTo (ThreadId (Id Maybe String
_ Int
i)),b
_,ThreadAction
a):[(Decision, b, ThreadAction)]
rest) = (if Bool
y then String
"p" else String
"P") forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
i forall a. [a] -> [a] -> [a]
++ String
"-" forall a. [a] -> [a] -> [a]
++ Bool -> [(Decision, b, ThreadAction)] -> String
go (ThreadAction -> Bool
didYield ThreadAction
a) [(Decision, b, ThreadAction)]
rest
go Bool
_ ((Decision
Continue,b
_,ThreadAction
a):[(Decision, b, ThreadAction)]
rest) = Char
'-' forall a. a -> [a] -> [a]
: Bool -> [(Decision, b, ThreadAction)] -> String
go (ThreadAction -> Bool
didYield ThreadAction
a) [(Decision, b, ThreadAction)]
rest
go Bool
_ [(Decision, b, ThreadAction)]
_ = String
""
strkey :: [String]
strkey =
[String
" " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
i forall a. [a] -> [a] -> [a]
++ String
": " forall a. [a] -> [a] -> [a]
++ String
name | (Int
i, String
name) <- Trace -> [(Int, String)]
threadNames Trace
trc]
didYield :: ThreadAction -> Bool
didYield ThreadAction
Yield = Bool
True
didYield (ThreadDelay Int
_) = Bool
True
didYield ThreadAction
_ = Bool
False
threadNames :: Trace -> [(Int, String)]
threadNames :: Trace -> [(Int, String)]
threadNames = forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe forall {a} {b}. (a, b, ThreadAction) -> Maybe (Int, String)
go where
go :: (a, b, ThreadAction) -> Maybe (Int, String)
go (a
_, b
_, Fork (ThreadId (Id (Just String
name) Int
i))) = forall a. a -> Maybe a
Just (Int
i, String
name)
go (a
_, b
_, ForkOS (ThreadId (Id (Just String
name) Int
i))) = forall a. a -> Maybe a
Just (Int
i, String
name)
go (a, b, ThreadAction)
_ = forall a. Maybe a
Nothing
simplestsBy :: (x -> x -> Bool) -> [(x, Trace)] -> [(x, Trace)]
simplestsBy :: forall x. (x -> x -> Bool) -> [(x, Trace)] -> [(x, Trace)]
simplestsBy x -> x -> Bool
f = forall a b. (a -> b) -> [a] -> [b]
map forall {a} {b}.
[(a, [(Decision, b, ThreadAction)])]
-> (a, [(Decision, b, ThreadAction)])
choose forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {b}. [(x, b)] -> [[(x, b)]]
collect where
collect :: [(x, b)] -> [[(x, b)]]
collect = forall {t}. [[t]] -> (t -> t -> Bool) -> [t] -> [[t]]
groupBy' [] (\(x
a,b
_) (x
b,b
_) -> x -> x -> Bool
f x
a x
b)
choose :: [(a, [(Decision, b, ThreadAction)])]
-> (a, [(Decision, b, ThreadAction)])
choose = forall (t :: * -> *) a.
Foldable t =>
(a -> a -> Ordering) -> t a -> a
minimumBy forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. Ord a => (b -> a) -> b -> b -> Ordering
comparing forall a b. (a -> b) -> a -> b
$ \(a
_, [(Decision, b, ThreadAction)]
trc) ->
let switchTos :: [(Decision, b, c)] -> Int
switchTos = forall (t :: * -> *) a. Foldable t => t a -> Int
length forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. (a -> Bool) -> [a] -> [a]
filter (\(Decision
d,b
_,c
_) -> case Decision
d of SwitchTo ThreadId
_ -> Bool
True; Decision
_ -> Bool
False)
starts :: [(Decision, b, c)] -> Int
starts = forall (t :: * -> *) a. Foldable t => t a -> Int
length forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. (a -> Bool) -> [a] -> [a]
filter (\(Decision
d,b
_,c
_) -> case Decision
d of Start ThreadId
_ -> Bool
True; Decision
_ -> Bool
False)
commits :: [(a, b, ThreadAction)] -> Int
commits = forall (t :: * -> *) a. Foldable t => t a -> Int
length forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. (a -> Bool) -> [a] -> [a]
filter (\(a
_,b
_,ThreadAction
a) -> case ThreadAction
a of CommitIORef ThreadId
_ IORefId
_ -> Bool
True; ThreadAction
_ -> Bool
False)
in (forall {b} {c}. [(Decision, b, c)] -> Int
switchTos [(Decision, b, ThreadAction)]
trc, forall {a} {b}. [(a, b, ThreadAction)] -> Int
commits [(Decision, b, ThreadAction)]
trc, forall (t :: * -> *) a. Foldable t => t a -> Int
length [(Decision, b, ThreadAction)]
trc, forall {b} {c}. [(Decision, b, c)] -> Int
starts [(Decision, b, ThreadAction)]
trc)
groupBy' :: [[t]] -> (t -> t -> Bool) -> [t] -> [[t]]
groupBy' [[t]]
res t -> t -> Bool
_ [] = [[t]]
res
groupBy' [[t]]
res t -> t -> Bool
eq (t
y:[t]
ys) = [[t]] -> (t -> t -> Bool) -> [t] -> [[t]]
groupBy' (forall {t}. (t -> t -> Bool) -> t -> [[t]] -> [[t]]
insert' t -> t -> Bool
eq t
y [[t]]
res) t -> t -> Bool
eq [t]
ys
insert' :: (t -> t -> Bool) -> t -> [[t]] -> [[t]]
insert' t -> t -> Bool
_ t
x [] = [[t
x]]
insert' t -> t -> Bool
eq t
x (ys :: [t]
ys@(t
y:[t]
_):[[t]]
yss)
| t
x t -> t -> Bool
`eq` t
y = (t
xforall a. a -> [a] -> [a]
:[t]
ys) forall a. a -> [a] -> [a]
: [[t]]
yss
| Bool
otherwise = [t]
ys forall a. a -> [a] -> [a]
: (t -> t -> Bool) -> t -> [[t]] -> [[t]]
insert' t -> t -> Bool
eq t
x [[t]]
yss
insert' t -> t -> Bool
_ t
_ ([]:[[t]]
_) = forall a. HasCallStack => a
undefined
showCondition :: Condition -> String
showCondition :: Condition -> String
showCondition Condition
Abort = String
"[abort]"
showCondition Condition
Deadlock = String
"[deadlock]"
showCondition (UncaughtException SomeException
exc) = String
"[" forall a. [a] -> [a] -> [a]
++ forall e. Exception e => e -> String
displayException SomeException
exc forall a. [a] -> [a] -> [a]
++ String
"]"
showCondition (InvariantFailure SomeException
_) = String
"[invariant failure]"
tidOf :: ThreadId -> Decision -> ThreadId
tidOf :: ThreadId -> Decision -> ThreadId
tidOf ThreadId
_ (Start ThreadId
t) = ThreadId
t
tidOf ThreadId
_ (SwitchTo ThreadId
t) = ThreadId
t
tidOf ThreadId
tid Decision
_ = ThreadId
tid
decisionOf :: Foldable f
=> Maybe ThreadId
-> f ThreadId
-> ThreadId
-> Decision
decisionOf :: forall (f :: * -> *).
Foldable f =>
Maybe ThreadId -> f ThreadId -> ThreadId -> Decision
decisionOf Maybe ThreadId
Nothing f ThreadId
_ ThreadId
chosen = ThreadId -> Decision
Start ThreadId
chosen
decisionOf (Just ThreadId
prior) f ThreadId
runnable ThreadId
chosen
| ThreadId
prior forall a. Eq a => a -> a -> Bool
== ThreadId
chosen = Decision
Continue
| ThreadId
prior forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` f ThreadId
runnable = ThreadId -> Decision
SwitchTo ThreadId
chosen
| Bool
otherwise = ThreadId -> Decision
Start ThreadId
chosen