Commit f8d6da22 authored by Klaus Aehlig's avatar Klaus Aehlig
Browse files

Verify extRepr-equal states are equal on updateLocksWaiting



Add a test that verifies that extRepr-equal states cannot be
distinguished by updateLocksWaiting-transitions. To obtain
extRepr-equal states, we compare each state to the one computed
from its extensional representation.
Signed-off-by: default avatarKlaus Aehlig <aehlig@google.com>
Reviewed-by: default avatarPetr Pudlak <pudlak@google.com>
parent 0d3308c2
......@@ -252,6 +252,23 @@ prop_SimulateUpdateLocks =
, notify == notify'
, extRepr finState == extRepr finState'
]
-- | Verify that any state is indistinguishable from its canonical version
-- (i.e., the one obtained from the extensional representation) with respect
-- to updateLocksWaiting.
prop_SimulateUpdateLocksWaiting :: Property
prop_SimulateUpdateLocksWaiting =
forAll (arbitrary :: Gen (LockWaiting TestLock TestOwner Integer)) $ \state ->
forAll (arbitrary :: Gen TestOwner) $ \owner ->
forAll (arbitrary :: Gen Integer) $ \prio ->
forAll (arbitrary :: Gen [LockRequest TestLock]) $ \req ->
let state' = fromExtRepr $ extRepr state
(finState, (result, notify)) = updateLocksWaiting prio owner req state
(finState', (result', notify')) = updateLocksWaiting prio owner req state'
in printTestCase "extRepr-equal states must behave equal on updateLocks"
$ and [ result == result'
, notify == notify'
, extRepr finState == extRepr finState'
]
testSuite "Locking/Waiting"
[ 'prop_NoActionWithPendingRequests
......@@ -263,4 +280,5 @@ testSuite "Locking/Waiting"
, 'prop_PendingJustified
, 'prop_extReprPreserved
, 'prop_SimulateUpdateLocks
, 'prop_SimulateUpdateLocksWaiting
]
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment