mirror of
https://github.com/barrucadu/dejafu.git
synced 2024-12-18 11:01:50 +03:00
94e22a765e
New coverage report, as there have been a bunch of new tests since the
one in the CONTRIBUTING file was generated:
54% expressions used (4311/7948)
51% boolean coverage (67/131)
47% guards (50/106), 31 always True, 6 always False, 19 unevaluated
57% 'if' conditions (11/19), 2 always True, 1 always False, 5 unevaluated
100% qualifiers (6/6)
61% alternatives used (413/671)
83% local declarations used (212/254)
28% top-level declarations used (313/1099)
85 lines
3.5 KiB
Haskell
85 lines
3.5 KiB
Haskell
module Cases.Refinement where
|
|
|
|
import Control.Concurrent.Classy.MVar
|
|
import Control.Monad (void)
|
|
import Test.DejaFu.Conc (ConcIO)
|
|
import Test.DejaFu.Refinement
|
|
import Test.Framework (Test, testGroup)
|
|
import Test.Framework.Providers.HUnit (hUnitTestToTests)
|
|
import Test.HUnit (test)
|
|
import Test.HUnit.DejaFu (testProperty)
|
|
|
|
import Utils
|
|
|
|
tests :: [Test]
|
|
tests =
|
|
[ testGroup "MVar" . hUnitTestToTests . test $
|
|
[ testProperty "read_idempotent_s" prop_mvar_read_idempotent_s
|
|
, testProperty "read_idempotent_c" prop_mvar_read_idempotent_c
|
|
, testProperty "read_neq_take_put" prop_mvar_read_neq_take_put
|
|
, testProperty "read_sr_take_put" prop_mvar_read_sr_take_put
|
|
, testProperty "take_eq_read_take_s" prop_mvar_take_eq_read_take_s
|
|
, testProperty "take_neq_read_take_c" prop_mvar_take_neq_read_take_c
|
|
, testProperty "take_sr_read_take_c" prop_mvar_take_sr_read_take_c
|
|
, testProperty "prop_mvar_put_neq_put_read_s" prop_mvar_put_neq_put_read_s
|
|
, testProperty "prop_mvar_put_sr_put_read_s" prop_mvar_put_sr_put_read_s
|
|
, testProperty "prop_mvar_put_neq_put_read_c" prop_mvar_put_neq_put_read_c
|
|
, testProperty "prop_mvar_put_sr_put_read_c" prop_mvar_put_sr_put_read_c
|
|
]
|
|
]
|
|
|
|
-------------------------------------------------------------------------------
|
|
-- MVars
|
|
|
|
mvar :: (MVar ConcIO Int -> ConcIO a) -> Sig (MVar ConcIO Int) (Maybe Int) (Maybe Int)
|
|
mvar e = Sig
|
|
{ initialise = maybe newEmptyMVar newMVar
|
|
, observe = const . tryTakeMVar
|
|
, interfere = \v mi -> tryTakeMVar v >> maybe (pure ()) (void . tryPutMVar v) mi
|
|
, expression = void . e
|
|
}
|
|
|
|
-- | @readMVar@ is idempotent when composed sequentially.
|
|
prop_mvar_read_idempotent_s =
|
|
mvar readMVar === mvar (\v -> readMVar v >> readMVar v)
|
|
|
|
-- | @readMVar@ is idempotent when composed concurrently.
|
|
prop_mvar_read_idempotent_c =
|
|
mvar readMVar === mvar (\v -> readMVar v ||| readMVar v)
|
|
|
|
-- | @readMVar@ is not equivalent to a take followed by a put.
|
|
prop_mvar_read_neq_take_put = expectFailure $
|
|
mvar readMVar === mvar (\v -> takeMVar v >>= putMVar v)
|
|
|
|
-- | @readMVar@ is a strict refinement of a take followed by a put.
|
|
prop_mvar_read_sr_take_put =
|
|
mvar readMVar ->- mvar (\v -> takeMVar v >>= putMVar v)
|
|
|
|
-- | @takeMVar@ is equivalent to a read followed by a take.
|
|
prop_mvar_take_eq_read_take_s =
|
|
mvar takeMVar === mvar (\v -> readMVar v >> takeMVar v)
|
|
|
|
-- | @takeMVar@ is not equivalent to a read concurrently composed with a take.
|
|
prop_mvar_take_neq_read_take_c = expectFailure $
|
|
mvar takeMVar === mvar (\v -> readMVar v ||| takeMVar v)
|
|
|
|
-- | @takeMVar@ is a strict refinement of a read concurrently composed with a take.
|
|
prop_mvar_take_sr_read_take_c =
|
|
mvar takeMVar ->- mvar (\v -> readMVar v ||| takeMVar v)
|
|
|
|
-- | @putMVar@ is not equivalent to a put followed by a read.
|
|
prop_mvar_put_neq_put_read_s x = expectFailure $
|
|
mvar (\v -> putMVar v x) === mvar (\v -> putMVar v x >> readMVar v)
|
|
|
|
-- | @putMVar@ is a strict refinement of a put followed by a read.
|
|
prop_mvar_put_sr_put_read_s x =
|
|
mvar (\v -> putMVar v x) ->- mvar (\v -> putMVar v x >> readMVar v)
|
|
|
|
-- | @putMVar@ is not equivalent to a put concurrently composed with a read.
|
|
prop_mvar_put_neq_put_read_c x = expectFailure $
|
|
mvar (\v -> putMVar v x) === mvar (\v -> putMVar v x ||| readMVar v)
|
|
|
|
-- | @putMVar@ is a strict refinement of a put concurrently composed with a read.
|
|
prop_mvar_put_sr_put_read_c x =
|
|
mvar (\v -> putMVar v x) ->- mvar (\v -> putMVar v x ||| readMVar v)
|