Commit 1c362c1a authored by Klaus Aehlig's avatar Klaus Aehlig
Browse files

Verify decoding from extensional representation is sound



Verify that, on the image of extRepr, it holds extRepr . fromExtrRepr = id.
In other words, verify that when obtain a lock waiting from an extensional
representation, it has the same extensional representation.
Signed-off-by: default avatarKlaus Aehlig <aehlig@google.com>
Reviewed-by: default avatarPetr Pudlak <pudlak@google.com>
parent b2a8f6ac
......@@ -225,6 +225,18 @@ prop_PendingJustified =
in printTestCase "Pebding requests must be good and not fulfillable"
. all isJustified . S.toList $ getPendingRequests state
-- | Verify that extRepr . fromExtRepr = id for all valid extensional
-- representations.
prop_extReprPreserved :: Property
prop_extReprPreserved =
forAll (arbitrary :: Gen (LockWaiting TestLock TestOwner Integer)) $ \state ->
let rep = extRepr state
rep' = extRepr $ fromExtRepr rep
in printTestCase "a lock waiting obtained from an extensional representation\
\ must have the same extensional representation"
$ rep' == rep
testSuite "Locking/Waiting"
[ 'prop_NoActionWithPendingRequests
, 'prop_WaitingRequestsGetPending
......@@ -233,4 +245,5 @@ testSuite "Locking/Waiting"
, 'prop_Progress
, 'prop_ProgressSound
, 'prop_PendingJustified
, 'prop_extReprPreserved
]
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