mirror of
https://github.com/barrucadu/dejafu.git
synced 2024-12-20 12:01:33 +03:00
Include the failed results and traces in a Result
This commit is contained in:
parent
d5afca652c
commit
2332c93cd7
@ -22,11 +22,15 @@ module Control.Monad.Conc.SCT.Tests
|
|||||||
-- * Utilities
|
-- * Utilities
|
||||||
, pAnd
|
, pAnd
|
||||||
, pNot
|
, pNot
|
||||||
|
, rForgetful
|
||||||
) where
|
) where
|
||||||
|
|
||||||
import Control.Applicative ((<$>))
|
import Control.Applicative ((<$>))
|
||||||
|
import Control.Arrow (first)
|
||||||
import Control.DeepSeq (NFData(..))
|
import Control.DeepSeq (NFData(..))
|
||||||
|
import Control.Monad (void)
|
||||||
import Control.Monad.Conc.Fixed
|
import Control.Monad.Conc.Fixed
|
||||||
|
import Control.Monad.Conc.SCT.Internal
|
||||||
import Control.Monad.Conc.SCT.PreBound
|
import Control.Monad.Conc.SCT.PreBound
|
||||||
import Data.Maybe (isJust, isNothing)
|
import Data.Maybe (isJust, isNothing)
|
||||||
|
|
||||||
@ -38,40 +42,45 @@ import qualified Control.Monad.Conc.Fixed.IO as CIO
|
|||||||
-- cases checked, and number of total cases. Be careful if using the
|
-- cases checked, and number of total cases. Be careful if using the
|
||||||
-- total number of cases, as that value may be very big, and (due to
|
-- total number of cases, as that value may be very big, and (due to
|
||||||
-- laziness) will actually force a lot more computation!.
|
-- laziness) will actually force a lot more computation!.
|
||||||
data Result = Result
|
data Result a = Result
|
||||||
{ _pass :: Bool
|
{ _pass :: Bool
|
||||||
-- ^ Whether the test passed or not.
|
-- ^ Whether the test passed or not.
|
||||||
, _casesChecked :: Int
|
, _casesChecked :: Int
|
||||||
-- ^ The number of cases checked.
|
-- ^ The number of cases checked.
|
||||||
, _casesTotal :: Int
|
, _casesTotal :: Int
|
||||||
-- ^ The total number of cases.
|
-- ^ The total number of cases.
|
||||||
} deriving (Show, Read, Eq)
|
, _failures :: [(Maybe a, SCTTrace)]
|
||||||
|
-- ^ The failed cases, if any.
|
||||||
|
} deriving (Show, Eq)
|
||||||
|
|
||||||
instance NFData Result where
|
instance NFData a => NFData (Result a) where
|
||||||
rnf r = rnf (_pass r, _casesChecked r, _casesTotal r)
|
rnf r = rnf (_pass r, _casesChecked r, _casesTotal r, _failures r)
|
||||||
|
|
||||||
|
instance Functor Result where
|
||||||
|
fmap f r = r { _failures = map (first $ fmap f) $ _failures r }
|
||||||
|
|
||||||
-- | Run a test using the pre-emption bounding scheduler, with a bound
|
-- | Run a test using the pre-emption bounding scheduler, with a bound
|
||||||
-- of 2.
|
-- of 2.
|
||||||
runTest :: Predicate a -> (forall t. Conc t a) -> Result
|
runTest :: Predicate a -> (forall t. Conc t a) -> Result a
|
||||||
runTest = runTest' 2
|
runTest = runTest' 2
|
||||||
|
|
||||||
-- | Variant of 'runTest' using 'IO'. See usual caveats about 'IO'.
|
-- | Variant of 'runTest' using 'IO'. See usual caveats about 'IO'.
|
||||||
runTestIO :: Predicate a -> (forall t. CIO.Conc t a) -> IO Result
|
runTestIO :: Predicate a -> (forall t. CIO.Conc t a) -> IO (Result a)
|
||||||
runTestIO = runTestIO' 2
|
runTestIO = runTestIO' 2
|
||||||
|
|
||||||
-- | Run a test using the pre-emption bounding scheduler.
|
-- | Run a test using the pre-emption bounding scheduler.
|
||||||
runTest' :: Int -> Predicate a -> (forall t. Conc t a) -> Result
|
runTest' :: Int -> Predicate a -> (forall t. Conc t a) -> Result a
|
||||||
runTest' pb predicate conc = predicate . map fst $ sctPreBound pb conc
|
runTest' pb predicate conc = predicate $ sctPreBound pb conc
|
||||||
|
|
||||||
-- | Variant of 'runTest'' using 'IO'. See usual caveats about 'IO'.
|
-- | Variant of 'runTest'' using 'IO'. See usual caveats about 'IO'.
|
||||||
runTestIO' :: Int -> Predicate a -> (forall t. CIO.Conc t a) -> IO Result
|
runTestIO' :: Int -> Predicate a -> (forall t. CIO.Conc t a) -> IO (Result a)
|
||||||
runTestIO' pb predicate conc = predicate . map fst <$> sctPreBoundIO pb conc
|
runTestIO' pb predicate conc = predicate <$> sctPreBoundIO pb conc
|
||||||
|
|
||||||
-- * Predicates
|
-- * Predicates
|
||||||
|
|
||||||
-- | A @Predicate@ is a function which collapses a list of results
|
-- | A @Predicate@ is a function which collapses a list of results
|
||||||
-- into a 'Result'.
|
-- into a 'Result'.
|
||||||
type Predicate a = [Maybe a] -> Result
|
type Predicate a = [(Maybe a, SCTTrace)] -> Result a
|
||||||
|
|
||||||
-- | Check that a computation never deadlocks.
|
-- | Check that a computation never deadlocks.
|
||||||
deadlocksNever :: Predicate a
|
deadlocksNever :: Predicate a
|
||||||
@ -94,37 +103,63 @@ alwaysSame = alwaysTrue2 (==)
|
|||||||
-- | Check that the result of a unary boolean predicate is always
|
-- | Check that the result of a unary boolean predicate is always
|
||||||
-- true. An empty list of results counts as 'True'.
|
-- true. An empty list of results counts as 'True'.
|
||||||
alwaysTrue :: (Maybe a -> Bool) -> Predicate a
|
alwaysTrue :: (Maybe a -> Bool) -> Predicate a
|
||||||
alwaysTrue p = pNot $ somewhereTrue (not . p)
|
alwaysTrue p xs = go xs Result { _pass = True, _casesChecked = 0, _casesTotal = len, _failures = failures } where
|
||||||
|
go [] res = res
|
||||||
|
go ((y,_):ys) res
|
||||||
|
| p y = go ys $ incCC res
|
||||||
|
| otherwise = incCC res { _pass = False }
|
||||||
|
|
||||||
|
(len, failures) = findFailures1 p xs
|
||||||
|
|
||||||
-- | Check that the result of a binary boolean predicate is always
|
-- | Check that the result of a binary boolean predicate is always
|
||||||
-- true between adjacent pairs of results. An empty list of results
|
-- true between adjacent pairs of results. An empty list of results
|
||||||
-- counts as 'True'.
|
-- counts as 'True'.
|
||||||
|
--
|
||||||
|
-- If the predicate fails, *both* (result,trace) tuples will be added
|
||||||
|
-- to the failures list.
|
||||||
alwaysTrue2 :: (Maybe a -> Maybe a -> Bool) -> Predicate a
|
alwaysTrue2 :: (Maybe a -> Maybe a -> Bool) -> Predicate a
|
||||||
alwaysTrue2 p = pNot $ somewhereTrue2 (\a b -> not $ p a b)
|
alwaysTrue2 _ [_] = Result { _pass = True, _casesChecked = 1, _casesTotal = 1, _failures = [] }
|
||||||
|
alwaysTrue2 p xs = go xs Result { _pass = True, _casesChecked = 0, _casesTotal = len, _failures = failures } where
|
||||||
|
go [] = id
|
||||||
|
go [(y1,_),(y2,_)] = check y1 y2 []
|
||||||
|
go ((y1,_):(y2,t):ys) = check y1 y2 ((y2,t) : ys)
|
||||||
|
|
||||||
|
check y1 y2 ys res
|
||||||
|
| p y1 y2 = go ys $ incCC res
|
||||||
|
| otherwise = incCC res { _pass = False }
|
||||||
|
|
||||||
|
(len, failures) = findFailures2 p xs
|
||||||
|
|
||||||
-- | Check that the result of a unary boolean predicate is true at
|
-- | Check that the result of a unary boolean predicate is true at
|
||||||
-- least once. An empty list of results counts as 'False'.
|
-- least once. An empty list of results counts as 'False'.
|
||||||
somewhereTrue :: (Maybe a -> Bool) -> Predicate a
|
somewhereTrue :: (Maybe a -> Bool) -> Predicate a
|
||||||
somewhereTrue p xs = go xs Result { _pass = False, _casesChecked = 0, _casesTotal = length xs } where
|
somewhereTrue p xs = go xs Result { _pass = False, _casesChecked = 0, _casesTotal = len, _failures = failures } where
|
||||||
go [] res = res
|
go [] res = res
|
||||||
go (y:ys) res
|
go ((y,_):ys) res
|
||||||
| p y = incCC res { _pass = True }
|
| p y = incCC res { _pass = True }
|
||||||
| otherwise = go ys $ incCC res
|
| otherwise = go ys $ incCC res
|
||||||
|
|
||||||
|
(len, failures) = findFailures1 p xs
|
||||||
|
|
||||||
-- | Check that the result of a binary boolean predicate is true
|
-- | Check that the result of a binary boolean predicate is true
|
||||||
-- between at least one adjacent pair of results. An empty list of
|
-- between at least one adjacent pair of results. An empty list of
|
||||||
-- results counts as 'False'.
|
-- results counts as 'False'.
|
||||||
|
--
|
||||||
|
-- If the predicate fails, *both* (result,trace) tuples will be added
|
||||||
|
-- to the failures list.
|
||||||
somewhereTrue2 :: (Maybe a -> Maybe a -> Bool) -> Predicate a
|
somewhereTrue2 :: (Maybe a -> Maybe a -> Bool) -> Predicate a
|
||||||
somewhereTrue2 _ [_] = Result { _pass = False, _casesChecked = 1, _casesTotal = 1 }
|
somewhereTrue2 _ [x] = Result { _pass = False, _casesChecked = 1, _casesTotal = 1, _failures = [x] }
|
||||||
somewhereTrue2 p xs = go xs Result { _pass = False, _casesChecked = 0, _casesTotal = length xs } where
|
somewhereTrue2 p xs = go xs Result { _pass = False, _casesChecked = 0, _casesTotal = len, _failures = failures } where
|
||||||
go [] = id
|
go [] = id
|
||||||
go [y1,y2] = check y1 y2 []
|
go [(y1,_),(y2,_)] = check y1 y2 []
|
||||||
go (y1:y2:ys) = check y1 y2 (y2 : ys)
|
go ((y1,_):(y2,t):ys) = check y1 y2 ((y2,t) : ys)
|
||||||
|
|
||||||
check y1 y2 ys res
|
check y1 y2 ys res
|
||||||
| p y1 y2 = incCC res { _pass = True }
|
| p y1 y2 = incCC res { _pass = True }
|
||||||
| otherwise = go ys $ incCC res
|
| otherwise = go ys $ incCC res
|
||||||
|
|
||||||
|
(len, failures) = findFailures2 p xs
|
||||||
|
|
||||||
-- * Utils
|
-- * Utils
|
||||||
|
|
||||||
-- | Compose two predicates sequentially.
|
-- | Compose two predicates sequentially.
|
||||||
@ -138,6 +173,30 @@ pNot :: Predicate a -> Predicate a
|
|||||||
pNot p xs = r { _pass = not $ _pass r } where
|
pNot p xs = r { _pass = not $ _pass r } where
|
||||||
r = p xs
|
r = p xs
|
||||||
|
|
||||||
|
-- | Throw away the failures information in a Result (useful for
|
||||||
|
-- storing them in a list).
|
||||||
|
rForgetful :: Result a -> Result ()
|
||||||
|
rForgetful = void
|
||||||
|
|
||||||
-- | Increment the cases checked
|
-- | Increment the cases checked
|
||||||
incCC :: Result -> Result
|
incCC :: Result a -> Result a
|
||||||
incCC r = r { _casesChecked = _casesChecked r + 1 }
|
incCC r = r { _casesChecked = _casesChecked r + 1 }
|
||||||
|
|
||||||
|
-- | Get the length of the list and find the failing cases in one
|
||||||
|
-- traversal.
|
||||||
|
findFailures1 :: (Maybe a -> Bool) -> [(Maybe a, SCTTrace)] -> (Int, [(Maybe a, SCTTrace)])
|
||||||
|
findFailures1 p xs = findFailures xs 0 [] where
|
||||||
|
findFailures [] l fs = (l, fs)
|
||||||
|
findFailures ((z,t):zs) l fs
|
||||||
|
| p z = findFailures zs (l+1) fs
|
||||||
|
| otherwise = findFailures zs (l+1) ((z,t):fs)
|
||||||
|
|
||||||
|
-- | Get the length of the list and find the failing cases in one
|
||||||
|
-- traversal.
|
||||||
|
findFailures2 :: (Maybe a -> Maybe a -> Bool) -> [(Maybe a, SCTTrace)] -> (Int, [(Maybe a, SCTTrace)])
|
||||||
|
findFailures2 p xs = findFailures xs 0 [] where
|
||||||
|
findFailures [] l fs = (l, fs)
|
||||||
|
findFailures [_] l fs = (l+1, fs)
|
||||||
|
findFailures ((z1,t1):(z2,t2):zs) l fs
|
||||||
|
| p z1 z2 = findFailures ((z2,t2):zs) (l+1) fs
|
||||||
|
| otherwise = findFailures ((z2,t2):zs) (l+1) ((z1,t1):(z2,t2):fs)
|
||||||
|
@ -13,6 +13,15 @@ main = do
|
|||||||
runTest :: Bool -> Test -> IO Bool
|
runTest :: Bool -> Test -> IO Bool
|
||||||
runTest verbose (Test {name = name, result = result}) = do
|
runTest verbose (Test {name = name, result = result}) = do
|
||||||
if _pass result
|
if _pass result
|
||||||
then when verbose (putStrLn $ "\27[32m[pass]\27[0m " ++ name ++ " (checked: " ++ show (_casesChecked result) ++ ")")
|
then
|
||||||
else putStrLn ("\27[31m[fail]\27[0m " ++ name ++ " (checked: " ++ show (_casesChecked result) ++ ")")
|
-- If verbose, display a pass message.
|
||||||
|
when verbose $
|
||||||
|
putStrLn $ "\27[32m[pass]\27[0m " ++ name ++ " (checked: " ++ show (_casesChecked result) ++ ")"
|
||||||
|
else do
|
||||||
|
-- Display a failure message, and the first 3 failed traces
|
||||||
|
putStrLn ("\27[31m[fail]\27[0m " ++ name ++ " (checked: " ++ show (_casesChecked result) ++ ")")
|
||||||
|
mapM_ (\fail -> putStrLn $ "\t" ++ show fail) . take 3 $ _failures result
|
||||||
|
when (length (_failures result) > 3) $
|
||||||
|
putStrLn "\t..."
|
||||||
|
|
||||||
return $ _pass result
|
return $ _pass result
|
||||||
|
@ -8,22 +8,22 @@ import Control.Monad.Conc.SCT.Tests
|
|||||||
|
|
||||||
import qualified Tests.Logger as L
|
import qualified Tests.Logger as L
|
||||||
|
|
||||||
data Test = Test { name :: String, result :: Result }
|
data Test = Test { name :: String, result :: Result String }
|
||||||
|
|
||||||
-- | List of all tests
|
-- | List of all tests
|
||||||
testCases :: [Test]
|
testCases :: [Test]
|
||||||
testCases =
|
testCases =
|
||||||
[ Test "Simple 2-Deadlock" $ runTest deadlocksSometimes simple2Deadlock
|
[ Test "Simple 2-Deadlock" . fmap show $ runTest deadlocksSometimes simple2Deadlock
|
||||||
, Test "2 Philosophers" $ runTest deadlocksSometimes $ philosophers 2
|
, Test "2 Philosophers" . fmap show $ runTest deadlocksSometimes $ philosophers 2
|
||||||
, Test "3 Philosophers" $ runTest deadlocksSometimes $ philosophers 3
|
, Test "3 Philosophers" . fmap show $ runTest deadlocksSometimes $ philosophers 3
|
||||||
, Test "4 Philosophers" $ runTest deadlocksSometimes $ philosophers 4
|
, Test "4 Philosophers" . fmap show $ runTest deadlocksSometimes $ philosophers 4
|
||||||
, Test "Threshold Value" $ runTest (pNot alwaysSame) thresholdValue
|
, Test "Threshold Value" . fmap show $ runTest (pNot alwaysSame) thresholdValue
|
||||||
, Test "Forgotten Unlock" $ runTest deadlocksAlways forgottenUnlock
|
, Test "Forgotten Unlock" . fmap show $ runTest deadlocksAlways forgottenUnlock
|
||||||
, Test "Simple 2-Race" $ runTest (pNot alwaysSame) simple2Race
|
, Test "Simple 2-Race" . fmap show $ runTest (pNot alwaysSame) simple2Race
|
||||||
, Test "Racey Stack" $ runTest (pNot alwaysSame) raceyStack
|
, Test "Racey Stack" . fmap show $ runTest (pNot alwaysSame) raceyStack
|
||||||
, Test "Logger (LA)" $ L.testLA
|
, Test "Logger (LA)" . fmap show $ L.testLA
|
||||||
, Test "Logger (LP)" $ L.testLP
|
, Test "Logger (LP)" . fmap show $ L.testLP
|
||||||
, Test "Logger (LE)" $ L.testLE
|
, Test "Logger (LE)" . fmap show $ L.testLE
|
||||||
]
|
]
|
||||||
|
|
||||||
-- | Should deadlock on a minority of schedules.
|
-- | Should deadlock on a minority of schedules.
|
||||||
|
@ -60,7 +60,7 @@ bad = do
|
|||||||
|
|
||||||
-- | Test that the result is always in the set of allowed values, and
|
-- | Test that the result is always in the set of allowed values, and
|
||||||
-- doesn't deadlock.
|
-- doesn't deadlock.
|
||||||
testLA :: Result
|
testLA :: Result [String]
|
||||||
testLA = runTest (alwaysTrue listContents) bad where
|
testLA = runTest (alwaysTrue listContents) bad where
|
||||||
listContents (Just strs) = strs `elem` [ ["Hello", "World", "Foo", "Bar", "Baz"]
|
listContents (Just strs) = strs `elem` [ ["Hello", "World", "Foo", "Bar", "Baz"]
|
||||||
, ["Hello", "World", "Foo", "Bar"]
|
, ["Hello", "World", "Foo", "Bar"]
|
||||||
@ -68,13 +68,13 @@ testLA = runTest (alwaysTrue listContents) bad where
|
|||||||
listContents Nothing = False
|
listContents Nothing = False
|
||||||
|
|
||||||
-- | Test that the "proper" result occurs at least once.
|
-- | Test that the "proper" result occurs at least once.
|
||||||
testLP :: Result
|
testLP :: Result [String]
|
||||||
testLP = runTest (somewhereTrue loggedAll) bad where
|
testLP = runTest (somewhereTrue loggedAll) bad where
|
||||||
loggedAll (Just a) = length a == 5
|
loggedAll (Just a) = length a == 5
|
||||||
loggedAll Nothing = False
|
loggedAll Nothing = False
|
||||||
|
|
||||||
-- | Test that the erroneous result occurs at least once.
|
-- | Test that the erroneous result occurs at least once.
|
||||||
testLE :: Result
|
testLE :: Result [String]
|
||||||
testLE = runTest (somewhereTrue loggedAlmostAll) bad where
|
testLE = runTest (somewhereTrue loggedAlmostAll) bad where
|
||||||
loggedAlmostAll (Just a) = length a == 4
|
loggedAlmostAll (Just a) = length a == 4
|
||||||
loggedAlmostAll Nothing = False
|
loggedAlmostAll Nothing = False
|
||||||
|
Loading…
Reference in New Issue
Block a user