Commit 0d3308c2 authored by Klaus Aehlig's avatar Klaus Aehlig
Browse files

Verify that extRepr-equal states behave equal on updateLocks



Add a test that verifies that extRepr-equal states cannot be
distinguished by updateLocks-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 1c362c1a
......@@ -236,6 +236,22 @@ prop_extReprPreserved =
\ must have the same extensional representation"
$ rep' == rep
-- | Verify that any state is indistinguishable from its canonical version
-- (i.e., the one obtained from the extensional representation) with respect
-- to updateLocks.
prop_SimulateUpdateLocks :: Property
prop_SimulateUpdateLocks =
forAll (arbitrary :: Gen (LockWaiting TestLock TestOwner Integer)) $ \state ->
forAll (arbitrary :: Gen TestOwner) $ \owner ->
forAll (arbitrary :: Gen [LockRequest TestLock]) $ \req ->
let state' = fromExtRepr $ extRepr state
(finState, (result, notify)) = updateLocks owner req state
(finState', (result', notify')) = updateLocks 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
......@@ -246,4 +262,5 @@ testSuite "Locking/Waiting"
, 'prop_ProgressSound
, 'prop_PendingJustified
, 'prop_extReprPreserved
, 'prop_SimulateUpdateLocks
]
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