dejafu 0.7.0.0 → 0.7.0.1
raw patch · 3 files changed
+64/−18 lines, 3 filesPVP ok
version bump matches the API change (PVP)
API changes (from Hackage documentation)
Files
- CHANGELOG.markdown +17/−0
- Test/DejaFu/Refinement.hs +45/−16
- dejafu.cabal +2/−2
CHANGELOG.markdown view
@@ -7,6 +7,23 @@ *de facto* standard Haskell versioning scheme. +0.7.0.1 [2017-06-09] (git tag: [dejafu-0.7.0.1][])+-------++https://hackage.haskell.org/package/dejafu-0.7.0.1++### Test.DejaFu.Refinement++- `check`, `check'`, and `checkFor` are now faster if there are multiple counterexamples.+- The above and `counterExamples` are now faster even if there is only a single counterexample in+ some cases.++[dejafu-0.7.0.1]: https://github.com/barrucadu/dejafu/releases/tag/dejafu-0.7.0.1+++---------------------------------------------------------------------------------------------------++ 0.7.0.0 [2017-06-07] (git tag: [dejafu-0.7.0.0][]) -------
Test/DejaFu/Refinement.hs view
@@ -1,6 +1,7 @@ {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE GADTs #-}+{-# LANGUAGE MultiWayIf #-} {-# LANGUAGE TupleSections #-} {-# LANGUAGE TypeFamilies #-} @@ -10,7 +11,7 @@ -- License : MIT -- Maintainer : Michael Walker <mike@barrucadu.co.uk> -- Stability : experimental--- Portability : FlexibleContexts, FlexibleInstances, GADTs, TupleSections, TypeFamilies+-- Portability : FlexibleContexts, FlexibleInstances, GADTs, MultiWayIf, TupleSections, TypeFamilies -- -- Properties about the side-effects of concurrent functions on some -- shared state.@@ -304,6 +305,9 @@ -- | Like 'check', but take a number of cases to try, also returns the -- counter example found rather than printing it. --+-- If multiple counterexamples exist, this will be faster than+-- @listToMaybe@ composed with @counterExamples@.+-- -- @since 0.7.0.0 checkFor :: (Testable p, Listable (X p), Eq (X p), Show (X p)) => Int@@ -313,7 +317,17 @@ -> p -- ^ The property to check. -> IO (Maybe (FailedProperty (O p) (X p)))-checkFor sn vn p = listToMaybe <$> counterExamples sn vn p+checkFor sn vn p = do+ let seeds = take sn $ concat tiers+ let cases = take vn $ concat (rpropTiers p)+ go seeds cases+ where+ go seeds ((vs, p'):rest) = do+ r <- checkWithSeeds seeds p'+ case r of+ Just cf -> pure (Just (cf vs))+ Nothing -> go seeds rest+ go _ [] = pure Nothing -- | Find all counterexamples up to a limit. --@@ -336,6 +350,9 @@ ------------------------------------------------------------------------------- -- Internal +-- | Three-valued sum, used in checking strict refinement.+data F x = Failing x | Unknown | Refuted+ -- | Check a refinement property with given seed values. Returns the -- counterexample if the property is false. checkWithSeeds@@ -344,21 +361,33 @@ -> RefinementProperty o x -- ^ The property to check. -> IO (Maybe ([String] -> FailedProperty o x))-checkWithSeeds seeds (RP how l r) = do- ls <- mapM (\x -> (x,) <$> evalSigWithSeed l x) seeds- rs <- mapM (evalSigWithSeed r) seeds- let resultsf f = zipWith (\(x, l') r' -> (l' `f` r', x, l', r')) ls rs- pure . listToMaybe $ case how of- Weak -> ces (resultsf S.isSubsetOf)- Strict ->- -- strict fails if (a) any left result-set is not a subset of- -- the corresponding right result-set, or (b) every left- -- result-set is equal to the corresponding right result-set- let equiv = null (ces (resultsf (==)))- in ces (resultsf S.isSubsetOf) ++ if equiv then ces (resultsf S.isProperSubsetOf) else []- Equiv -> ces (resultsf (==))+checkWithSeeds seeds (RP how l r) = case how of+ Weak -> go1 S.isSubsetOf seeds+ Equiv -> go1 (==) seeds+ Strict -> go2 Unknown seeds where- ces results = [toCE x lrs rrs | (False, x, lrs, rrs) <- results]+ -- weak and equiv need every set of pairwise result-sets to match+ -- some predicate.+ go1 f (x:xs) = do+ lrs <- evalSigWithSeed l x+ rrs <- evalSigWithSeed r x+ if lrs `f` rrs+ then go1 f xs+ else pure (Just $ toCE x lrs rrs)+ go1 _ [] = pure Nothing++ -- strict fails if (a) any left result-set is not a subset of the+ -- corresponding right result-set, or (b) every left result-set is+ -- equal to the corresponding right result-set+ go2 eq (x:xs) = do+ lrs <- evalSigWithSeed l x+ rrs <- evalSigWithSeed r x+ let ce = toCE x lrs rrs+ if | lrs == rrs -> go2 (case eq of Unknown -> Failing ce; _ -> eq) xs+ | lrs `S.isSubsetOf` rrs -> go2 Refuted xs+ | otherwise -> pure (Just ce)+ go2 (Failing cf) [] = pure (Just cf)+ go2 _ [] = pure Nothing toCE x lrs rrs args = CounterExample { failingSeed = x
dejafu.cabal view
@@ -2,7 +2,7 @@ -- documentation, see http://haskell.org/cabal/users-guide/ name: dejafu-version: 0.7.0.0+version: 0.7.0.1 synopsis: Systematic testing for Haskell concurrency. description:@@ -37,7 +37,7 @@ source-repository this type: git location: https://github.com/barrucadu/dejafu.git- tag: dejafu-0.7.0.0+ tag: dejafu-0.7.0.1 library exposed-modules: Test.DejaFu