github-repos/tla-plus
1
0
Fork 0
mirror of https://github.com/pingcap/tla-plus.git synced 2024-12-26 04:20:10 +08:00
Code Issues Packages Projects Releases Wiki Activity

add check txn status, read key, read SI check (#37)

Browse Source 
* Add CheckTxnStatus Msgs

* Add CheckTxnStatus, haven't checked by the TLC

revert a change

DistributedTransaction: fix checkTxnStatus bugs

DistributedTransaction: CheckTxnStatus: refactor

change a var name

Co-authored-by: Andy Lok <andylokandy@hotmail.com>

DistributedTransaction: CheckTxnStatus: format spec

update CheckTxnStatus comment

Co-authored-by: Andy Lok <andylokandy@hotmail.com>

DistributedTransaction: CheckTxnStatus: update comments

* Add SI check

DistributedTransactions: upd min_commit_ts

DistributedTransactions: fix tla parse err

DistributedTransactions: upd tests

upd lock failed

DistributedTransactions: upd read write keys

DistributedTransactions: upd Test2

DistributedTransactions: fix many bugs

* DistributedTransactions: extract unlock_key function

DistributedTransactions: avoid client check txn rollback itself

DistributedTransactions: add ClientCheckTxnStatus to `Next`

DistributedTransactions: amend pessimistic lock

DistributedTransactions: add read SI check

DistributedTransactions: upd pdf version

DistributedTransactions: remove ServerCleanupLock

DistributedTransactions: refactor ClientReadFailed CheckTxnStatus

DistributedTransactions: upd server lock key

DistributedTransactions: fix ClientRetryLockKey bug

DistributedTransactions: fix ReadSI def

* DistributedTransactions: upd max read times

DistributedTransactions: upd max read times

DistributedTransactions: fix bug

DistributedTransactions: upd

DistributedTransactions: refactor, upd some comments

DistributedTransactions: refactor, upd

* DistributedTransaction: Add max client check txn times

DistributedTransaction: upd lock min_commit_ts check

DistributedTransaction: rename wrong name to current_ts

DistributedTransaction: reformat some code

* fix wrong pessimistic lock amend

DistributedTransactions: fix pessimistic lock amend bug

upd

upd

upd

upd

upd

upd

upd

upd

* upd read SI check

upd

refactor ClientRetryLockKey

upd ClientRetryCommit

upd max_lock_key_time

upd

fix bugs

upd pessimistic ReadSI check, same as optimistic one

* upd

remove some resp msgs

upd possible msg lost

* apply code review suggestion

upd

* restucture distributed transaction spec

Signed-off-by: Andy Lok <andylokandy@hotmail.com>

* fix comment

Signed-off-by: Andy Lok <andylokandy@hotmail.com>

* update comment

Signed-off-by: Andy Lok <andylokandy@hotmail.com>

* update assume

Signed-off-by: Andy Lok <andylokandy@hotmail.com>

* update comment

Signed-off-by: Andy Lok <andylokandy@hotmail.com>

* enable snapshot checks

Signed-off-by: Andy Lok <andylokandy@hotmail.com>

* fix pessimistic si check

Signed-off-by: Andy Lok <andylokandy@hotmail.com>

* add comment

Signed-off-by: Andy Lok <andylokandy@hotmail.com>

* add comment

Signed-off-by: Andy Lok <andylokandy@hotmail.com>

* add comment

Signed-off-by: Andy Lok <andylokandy@hotmail.com>

* fix typo

Signed-off-by: Andy Lok <andylokandy@hotmail.com>

* fix dead end in optimistic prewrite

Signed-off-by: Andy Lok <andylokandy@hotmail.com>

* add test5

Signed-off-by: Andy Lok <andylokandy@hotmail.com>

Co-authored-by: Andy Lok <andylokandy@hotmail.com>
This commit is contained in:
zhuo1ang 2021-08-22 22:06:49 +08:00 committed by GitHub
parent fc3c672d38
commit b80ac83420
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
17 changed files with 998 additions and 408 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
.gitignore vendored
View File

@ -5,3 +5,7 @@ states/
**/*.toolbox/*___*_SnapShot_*.launch
**/*.toolbox/.project
**/*.toolbox/.settings/
**/*.toolbox/*.aux
**/*.toolbox/*.log
**/*.toolbox/*.pdf
**/*.toolbox/*.tex

BIN
DistributedTransaction/DistributedTransaction.pdf
View File

Binary file not shown.

896
DistributedTransaction/DistributedTransaction.tla
View File

File diff suppressed because it is too large Load Diff

122
DistributedTransaction/DistributedTransaction.toolbox/DistributedTransaction___Test1.launch
View File

@ -1,60 +1,62 @@
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<launchConfiguration type="org.lamport.tla.toolbox.tool.tlc.modelCheck">
<stringAttribute key="TLCCmdLineParameters" value=""/>
<intAttribute key="collectCoverage" value="1"/>
<stringAttribute key="configurationName" value="Test1"/>
<booleanAttribute key="deferLiveness" value="false"/>
<intAttribute key="dfidDepth" value="100"/>
<booleanAttribute key="dfidMode" value="false"/>
<intAttribute key="distributedFPSetCount" value="0"/>
<stringAttribute key="distributedNetworkInterface" value="192.168.224.64"/>
<intAttribute key="distributedNodesCount" value="1"/>
<stringAttribute key="distributedTLC" value="off"/>
<stringAttribute key="distributedTLCVMArgs" value=""/>
<intAttribute key="fpBits" value="1"/>
<intAttribute key="fpIndex" value="41"/>
<booleanAttribute key="fpIndexRandom" value="true"/>
<intAttribute key="maxHeapSize" value="40"/>
<intAttribute key="maxSetSize" value="1000000"/>
<booleanAttribute key="mcMode" value="true"/>
<stringAttribute key="modelBehaviorInit" value=""/>
<stringAttribute key="modelBehaviorNext" value=""/>
<stringAttribute key="modelBehaviorSpec" value="Spec"/>
<intAttribute key="modelBehaviorSpecType" value="1"/>
<stringAttribute key="modelBehaviorVars" value="key_data, key_lock, next_ts, req_msgs, client_state, client_key, client_ts, resp_msgs, key_write"/>
<stringAttribute key="modelComments" value=""/>
<booleanAttribute key="modelCorrectnessCheckDeadlock" value="false"/>
<listAttribute key="modelCorrectnessInvariants">
<listEntry value="1TypeOK"/>
<listEntry value="1UniqueCommitOrAbort"/>
<listEntry value="1CommitConsistency"/>
<listEntry value="1AbortConsistency"/>
<listEntry value="1WriteConsistency"/>
<listEntry value="1UniqueLockOrWrite"/>
<listEntry value="1UniqueWrite"/>
<listEntry value="1MsgTsConsistency"/>
</listAttribute>
<listAttribute key="modelCorrectnessProperties">
<listEntry value="1SnapshotIsolation"/>
</listAttribute>
<intAttribute key="modelEditorOpenTabs" value="12"/>
<stringAttribute key="modelExpressionEval" value=""/>
<listAttribute key="modelParameterConstants">
<listEntry value="KEY;;{k1, k2};1;0"/>
<listEntry value="CLIENT_KEY;;c1 :&gt; {k1, k2} @@ c2 :&gt; {k1} @@ c3 :&gt; {k1, k2};0;0"/>
<listEntry value="PESSIMISTIC_CLIENT;;{c1, c2};1;0"/>
<listEntry value="OPTIMISTIC_CLIENT;;{c3};1;0"/>
<listEntry value="CLIENT_PRIMARY;;c1 :&gt; k1 @@ c2 :&gt; k1 @@ c3 :&gt; k2;0;0"/>
</listAttribute>
<intAttribute key="modelVersion" value="20191005"/>
<intAttribute key="numberOfWorkers" value="6"/>
<booleanAttribute key="recover" value="false"/>
<stringAttribute key="result.mail.address" value=""/>
<intAttribute key="simuAril" value="-1"/>
<intAttribute key="simuDepth" value="100"/>
<intAttribute key="simuSeed" value="-1"/>
<stringAttribute key="specName" value="DistributedTransaction"/>
<stringAttribute key="tlcResourcesProfile" value="local nomal"/>
<stringAttribute key="view" value=""/>
<booleanAttribute key="visualizeStateGraph" value="false"/>
</launchConfiguration>
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<launchConfiguration type="org.lamport.tla.toolbox.tool.tlc.modelCheck">
<stringAttribute key="TLCCmdLineParameters" value=""/>
<intAttribute key="collectCoverage" value="0"/>
<stringAttribute key="configurationName" value="Test1"/>
<booleanAttribute key="deferLiveness" value="false"/>
<intAttribute key="dfidDepth" value="10000"/>
<booleanAttribute key="dfidMode" value="false"/>
<intAttribute key="distributedFPSetCount" value="0"/>
<stringAttribute key="distributedNetworkInterface" value="10.33.72.47"/>
<intAttribute key="distributedNodesCount" value="1"/>
<stringAttribute key="distributedTLC" value="off"/>
<stringAttribute key="distributedTLCVMArgs" value=""/>
<intAttribute key="fpBits" value="1"/>
<intAttribute key="fpIndex" value="65"/>
<booleanAttribute key="fpIndexRandom" value="true"/>
<intAttribute key="maxHeapSize" value="75"/>
<intAttribute key="maxSetSize" value="1000000"/>
<booleanAttribute key="mcMode" value="true"/>
<stringAttribute key="modelBehaviorInit" value=""/>
<stringAttribute key="modelBehaviorNext" value=""/>
<stringAttribute key="modelBehaviorSpec" value="Spec"/>
<intAttribute key="modelBehaviorSpecType" value="1"/>
<stringAttribute key="modelBehaviorVars" value="key_data, key_lock, next_ts, req_msgs, client_state, client_key, client_ts, resp_msgs, key_write"/>
<stringAttribute key="modelComments" value=""/>
<booleanAttribute key="modelCorrectnessCheckDeadlock" value="false"/>
<listAttribute key="modelCorrectnessInvariants">
<listEntry value="1TypeOK"/>
<listEntry value="1UniqueCommitOrAbort"/>
<listEntry value="1CommitConsistency"/>
<listEntry value="1AbortConsistency"/>
<listEntry value="1WriteConsistency"/>
<listEntry value="1UniqueLockOrWrite"/>
<listEntry value="1UniqueWrite"/>
<listEntry value="1MsgTsConsistency"/>
<listEntry value="1ReadSnapshotIsolation"/>
</listAttribute>
<listAttribute key="modelCorrectnessProperties">
<listEntry value="1SnapshotIsolation"/>
</listAttribute>
<intAttribute key="modelEditorOpenTabs" value="12"/>
<stringAttribute key="modelExpressionEval" value=""/>
<listAttribute key="modelParameterConstants">
<listEntry value="KEY;;{k1, k2};1;0"/>
<listEntry value="PESSIMISTIC_CLIENT;;{c1, c2};1;0"/>
<listEntry value="OPTIMISTIC_CLIENT;;{c3};1;0"/>
<listEntry value="CLIENT_PRIMARY;;c1 :&gt; k1 @@ c2 :&gt; k1 @@ c3 :&gt; k2;0;0"/>
<listEntry value="CLIENT_WRITE_KEY;;c1 :&gt; {k1, k2} @@ c2 :&gt; {k1} @@ c3 :&gt; {k1, k2};0;0"/>
<listEntry value="CLIENT_READ_KEY;;c1 :&gt; {} @@ c2 :&gt; {} @@ c3 :&gt; {k1, k2};0;0"/>
</listAttribute>
<intAttribute key="modelVersion" value="20191005"/>
<intAttribute key="numberOfWorkers" value="7"/>
<booleanAttribute key="recover" value="false"/>
<stringAttribute key="result.mail.address" value=""/>
<intAttribute key="simuAril" value="-1"/>
<intAttribute key="simuDepth" value="10000"/>
<intAttribute key="simuSeed" value="-1"/>
<stringAttribute key="specName" value="DistributedTransaction"/>
<stringAttribute key="tlcResourcesProfile" value="local custom"/>
<stringAttribute key="view" value=""/>
<booleanAttribute key="visualizeStateGraph" value="false"/>
</launchConfiguration>

102
DistributedTransaction/DistributedTransaction.toolbox/DistributedTransaction___Test2.launch
View File

@ -1,42 +1,60 @@
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<launchConfiguration type="org.lamport.tla.toolbox.tool.tlc.modelCheck">
<stringAttribute key="configurationName" value="Test2"/>
<intAttribute key="distributedFPSetCount" value="0"/>
<stringAttribute key="distributedNetworkInterface" value="10.0.75.1"/>
<intAttribute key="distributedNodesCount" value="1"/>
<stringAttribute key="distributedTLC" value="off"/>
<intAttribute key="fpIndex" value="64"/>
<intAttribute key="maxHeapSize" value="25"/>
<stringAttribute key="modelBehaviorInit" value=""/>
<stringAttribute key="modelBehaviorNext" value=""/>
<stringAttribute key="modelBehaviorSpec" value="Spec"/>
<intAttribute key="modelBehaviorSpecType" value="1"/>
<stringAttribute key="modelBehaviorVars" value="key_data, key_lock, next_ts, req_msgs, client_state, client_key, client_ts, resp_msgs, key_write"/>
<stringAttribute key="modelComments" value=""/>
<booleanAttribute key="modelCorrectnessCheckDeadlock" value="false"/>
<listAttribute key="modelCorrectnessInvariants">
<listEntry value="1TypeOK"/>
<listEntry value="1UniqueCommitOrAbort"/>
<listEntry value="1CommitConsistency"/>
<listEntry value="1AbortConsistency"/>
<listEntry value="1WriteConsistency"/>
<listEntry value="1UniqueLockOrWrite"/>
<listEntry value="1UniqueWrite"/>
<listEntry value="1MsgTsConsistency"/>
</listAttribute>
<listAttribute key="modelCorrectnessProperties"/>
<intAttribute key="modelEditorOpenTabs" value="8"/>
<stringAttribute key="modelExpressionEval" value=""/>
<listAttribute key="modelParameterConstants">
<listEntry value="KEY;;{k1, k2, k3};1;0"/>
<listEntry value="CLIENT_KEY;;c1 :&gt; {k1, k2, k3} @@ c2 :&gt; {k1, k2} @@ c3 :&gt; {k1, k3};0;0"/>
<listEntry value="PESSIMISTIC_CLIENT;;{c1, c2};1;0"/>
<listEntry value="OPTIMISTIC_CLIENT;;{c3};1;0"/>
<listEntry value="CLIENT_PRIMARY;;c1 :&gt; k1 @@ c2 :&gt; k1 @@ c3 :&gt; k3;0;0"/>
</listAttribute>
<intAttribute key="modelVersion" value="20191005"/>
<intAttribute key="numberOfWorkers" value="6"/>
<stringAttribute key="result.mail.address" value=""/>
<stringAttribute key="specName" value="DistributedTransaction"/>
<stringAttribute key="tlcResourcesProfile" value="local custom"/>
</launchConfiguration>
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<launchConfiguration type="org.lamport.tla.toolbox.tool.tlc.modelCheck">
<stringAttribute key="TLCCmdLineParameters" value=""/>
<intAttribute key="collectCoverage" value="1"/>
<stringAttribute key="configurationName" value="Test2"/>
<booleanAttribute key="deferLiveness" value="false"/>
<intAttribute key="dfidDepth" value="100"/>
<booleanAttribute key="dfidMode" value="false"/>
<intAttribute key="distributedFPSetCount" value="0"/>
<stringAttribute key="distributedNetworkInterface" value="10.33.72.47"/>
<intAttribute key="distributedNodesCount" value="1"/>
<stringAttribute key="distributedTLC" value="off"/>
<stringAttribute key="distributedTLCVMArgs" value=""/>
<intAttribute key="fpBits" value="1"/>
<intAttribute key="fpIndex" value="59"/>
<booleanAttribute key="fpIndexRandom" value="true"/>
<intAttribute key="maxHeapSize" value="45"/>
<intAttribute key="maxSetSize" value="1000000"/>
<booleanAttribute key="mcMode" value="true"/>
<stringAttribute key="modelBehaviorInit" value=""/>
<stringAttribute key="modelBehaviorNext" value=""/>
<stringAttribute key="modelBehaviorSpec" value="Spec"/>
<intAttribute key="modelBehaviorSpecType" value="1"/>
<stringAttribute key="modelBehaviorVars" value="key_data, key_lock, next_ts, req_msgs, client_state, client_key, client_ts, resp_msgs, key_write"/>
<stringAttribute key="modelComments" value=""/>
<booleanAttribute key="modelCorrectnessCheckDeadlock" value="false"/>
<listAttribute key="modelCorrectnessInvariants">
<listEntry value="1TypeOK"/>
<listEntry value="1UniqueCommitOrAbort"/>
<listEntry value="1CommitConsistency"/>
<listEntry value="1AbortConsistency"/>
<listEntry value="1WriteConsistency"/>
<listEntry value="1UniqueLockOrWrite"/>
<listEntry value="1UniqueWrite"/>
<listEntry value="1MsgTsConsistency"/>
<listEntry value="1ReadSnapshotIsolation"/>
</listAttribute>
<listAttribute key="modelCorrectnessProperties"/>
<intAttribute key="modelEditorOpenTabs" value="12"/>
<stringAttribute key="modelExpressionEval" value=""/>
<listAttribute key="modelParameterConstants">
<listEntry value="KEY;;{k1, k2, k3};1;0"/>
<listEntry value="PESSIMISTIC_CLIENT;;{c1, c2};1;0"/>
<listEntry value="OPTIMISTIC_CLIENT;;{c3};1;0"/>
<listEntry value="CLIENT_PRIMARY;;c1 :&gt; k1 @@ c2 :&gt; k1 @@ c3 :&gt; k3;0;0"/>
<listEntry value="CLIENT_WRITE_KEY;;c1 :&gt; {k1, k2, k3} @@ c2 :&gt; {k1, k2} @@ c3 :&gt; {k1, k3};0;0"/>
<listEntry value="CLIENT_READ_KEY;;c1 :&gt; {} @@ c2 :&gt; {} @@ c3 :&gt; {k1, k3};0;0"/>
</listAttribute>
<intAttribute key="modelVersion" value="20191005"/>
<intAttribute key="numberOfWorkers" value="7"/>
<booleanAttribute key="recover" value="false"/>
<stringAttribute key="result.mail.address" value=""/>
<intAttribute key="simuAril" value="-1"/>
<intAttribute key="simuDepth" value="100"/>
<intAttribute key="simuSeed" value="-1"/>
<stringAttribute key="specName" value="DistributedTransaction"/>
<stringAttribute key="tlcResourcesProfile" value="local custom"/>
<stringAttribute key="view" value=""/>
<booleanAttribute key="visualizeStateGraph" value="false"/>
</launchConfiguration>

60
DistributedTransaction/DistributedTransaction.toolbox/DistributedTransaction___Test3.launch Normal file
View File

@ -0,0 +1,60 @@
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<launchConfiguration type="org.lamport.tla.toolbox.tool.tlc.modelCheck">
<stringAttribute key="TLCCmdLineParameters" value=""/>
<intAttribute key="collectCoverage" value="1"/>
<stringAttribute key="configurationName" value="Test3"/>
<booleanAttribute key="deferLiveness" value="true"/>
<intAttribute key="dfidDepth" value="100"/>
<booleanAttribute key="dfidMode" value="false"/>
<intAttribute key="distributedFPSetCount" value="0"/>
<stringAttribute key="distributedNetworkInterface" value="10.33.72.47"/>
<intAttribute key="distributedNodesCount" value="1"/>
<stringAttribute key="distributedTLC" value="off"/>
<stringAttribute key="distributedTLCVMArgs" value=""/>
<intAttribute key="fpBits" value="1"/>
<intAttribute key="fpIndex" value="100"/>
<booleanAttribute key="fpIndexRandom" value="true"/>
<intAttribute key="maxHeapSize" value="45"/>
<intAttribute key="maxSetSize" value="1000000"/>
<booleanAttribute key="mcMode" value="true"/>
<stringAttribute key="modelBehaviorInit" value=""/>
<stringAttribute key="modelBehaviorNext" value=""/>
<stringAttribute key="modelBehaviorSpec" value="Spec"/>
<intAttribute key="modelBehaviorSpecType" value="1"/>
<stringAttribute key="modelBehaviorVars" value="key_data, key_lock, next_ts, req_msgs, client_state, client_key, client_ts, resp_msgs, key_write"/>
<stringAttribute key="modelComments" value=""/>
<booleanAttribute key="modelCorrectnessCheckDeadlock" value="false"/>
<listAttribute key="modelCorrectnessInvariants">
<listEntry value="1TypeOK"/>
<listEntry value="1UniqueCommitOrAbort"/>
<listEntry value="1CommitConsistency"/>
<listEntry value="1AbortConsistency"/>
<listEntry value="1WriteConsistency"/>
<listEntry value="1UniqueLockOrWrite"/>
<listEntry value="1UniqueWrite"/>
<listEntry value="1MsgTsConsistency"/>
<listEntry value="1ReadSnapshotIsolation"/>
</listAttribute>
<listAttribute key="modelCorrectnessProperties"/>
<intAttribute key="modelEditorOpenTabs" value="12"/>
<stringAttribute key="modelExpressionEval" value=""/>
<listAttribute key="modelParameterConstants">
<listEntry value="KEY;;{k1, k2};1;0"/>
<listEntry value="PESSIMISTIC_CLIENT;;{c1};1;0"/>
<listEntry value="OPTIMISTIC_CLIENT;;{c2};1;0"/>
<listEntry value="CLIENT_PRIMARY;;c1 :&gt; k1 @@ c2 :&gt; k1;0;0"/>
<listEntry value="CLIENT_WRITE_KEY;;c1 :&gt; {k1, k2} @@ c2 :&gt; {k1, k2};0;0"/>
<listEntry value="CLIENT_READ_KEY;;c1 :&gt; {} @@ c2 :&gt; {k1, k2};0;0"/>
</listAttribute>
<intAttribute key="modelVersion" value="20191005"/>
<intAttribute key="numberOfWorkers" value="7"/>
<booleanAttribute key="recover" value="false"/>
<stringAttribute key="result.mail.address" value=""/>
<intAttribute key="simuAril" value="-1"/>
<intAttribute key="simuDepth" value="100"/>
<intAttribute key="simuSeed" value="-1"/>
<stringAttribute key="specName" value="DistributedTransaction"/>
<stringAttribute key="tlcResourcesProfile" value="local custom"/>
<stringAttribute key="view" value=""/>
<booleanAttribute key="visualizeStateGraph" value="false"/>
</launchConfiguration>

65
DistributedTransaction/DistributedTransaction.toolbox/DistributedTransaction___Test4.launch Normal file
View File

@ -0,0 +1,65 @@
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<launchConfiguration type="org.lamport.tla.toolbox.tool.tlc.modelCheck">
<stringAttribute key="TLCCmdLineParameters" value=""/>
<intAttribute key="collectCoverage" value="1"/>
<stringAttribute key="configurationName" value="Test4"/>
<booleanAttribute key="deferLiveness" value="false"/>
<intAttribute key="dfidDepth" value="100"/>
<booleanAttribute key="dfidMode" value="false"/>
<intAttribute key="distributedFPSetCount" value="0"/>
<stringAttribute key="distributedNetworkInterface" value="10.33.72.47"/>
<intAttribute key="distributedNodesCount" value="1"/>
<stringAttribute key="distributedTLC" value="off"/>
<stringAttribute key="distributedTLCVMArgs" value=""/>
<intAttribute key="fpBits" value="1"/>
<intAttribute key="fpIndex" value="117"/>
<booleanAttribute key="fpIndexRandom" value="true"/>
<intAttribute key="maxHeapSize" value="45"/>
<intAttribute key="maxSetSize" value="1000000"/>
<booleanAttribute key="mcMode" value="true"/>
<stringAttribute key="modelBehaviorInit" value=""/>
<stringAttribute key="modelBehaviorNext" value=""/>
<stringAttribute key="modelBehaviorSpec" value="Spec"/>
<intAttribute key="modelBehaviorSpecType" value="1"/>
<stringAttribute key="modelBehaviorVars" value="key_data, key_lock, next_ts, req_msgs, client_state, client_key, client_ts, resp_msgs, key_write"/>
<stringAttribute key="modelComments" value=""/>
<booleanAttribute key="modelCorrectnessCheckDeadlock" value="false"/>
<listAttribute key="modelCorrectnessInvariants">
<listEntry value="1TypeOK"/>
<listEntry value="1UniqueCommitOrAbort"/>
<listEntry value="1CommitConsistency"/>
<listEntry value="1AbortConsistency"/>
<listEntry value="1WriteConsistency"/>
<listEntry value="1UniqueLockOrWrite"/>
<listEntry value="1UniqueWrite"/>
<listEntry value="1MsgTsConsistency"/>
<listEntry value="1ReadSnapshotIsolation"/>
</listAttribute>
<listAttribute key="modelCorrectnessProperties"/>
<intAttribute key="modelEditorOpenTabs" value="0"/>
<stringAttribute key="modelExpressionEval" value="&#9;"/>
<stringAttribute key="modelParameterActionConstraint" value=""/>
<listAttribute key="modelParameterConstants">
<listEntry value="KEY;;{k1};1;0"/>
<listEntry value="PESSIMISTIC_CLIENT;;{c1};1;0"/>
<listEntry value="OPTIMISTIC_CLIENT;;{c2};1;0"/>
<listEntry value="CLIENT_PRIMARY;;c1 :&gt; k1 @@ c2 :&gt; k1;0;0"/>
<listEntry value="CLIENT_WRITE_KEY;;c1 :&gt; {k1} @@ c2 :&gt; {k1};0;0"/>
<listEntry value="CLIENT_READ_KEY;;c1 :&gt; {} @@ c2 :&gt; {k1};0;0"/>
</listAttribute>
<stringAttribute key="modelParameterContraint" value=""/>
<listAttribute key="modelParameterDefinitions"/>
<stringAttribute key="modelParameterModelValues" value="{}"/>
<stringAttribute key="modelParameterNewDefinitions" value=""/>
<intAttribute key="modelVersion" value="20191005"/>
<intAttribute key="numberOfWorkers" value="7"/>
<booleanAttribute key="recover" value="false"/>
<stringAttribute key="result.mail.address" value=""/>
<intAttribute key="simuAril" value="-1"/>
<intAttribute key="simuDepth" value="100"/>
<intAttribute key="simuSeed" value="-1"/>
<stringAttribute key="specName" value="DistributedTransaction"/>
<stringAttribute key="tlcResourcesProfile" value="local custom"/>
<stringAttribute key="view" value=""/>
<booleanAttribute key="visualizeStateGraph" value="false"/>
</launchConfiguration>

7
DistributedTransaction/Test1.cfg
View File

@ -6,10 +6,11 @@ CONSTANT
c3 = c3
CONSTANT
KEY <- Key
KEY <- Keys
OPTIMISTIC_CLIENT <- OptimistiicClient
PESSIMISTIC_CLIENT <- PessimisticClient
CLIENT_KEY <- ClientKey
CLIENT_READ_KEY <- ClientReadKeys
CLIENT_WRITE_KEY <- ClientWriteKeys
CLIENT_PRIMARY <- ClientPrimary
INIT
@ -26,4 +27,6 @@ INVARIANT
WriteConsistency
UniqueLockOrWrite
UniqueWrite
OptimisticReadSnapshotIsolation
PessimisticReadSnapshotIsolation
MsgTsConsistency

5
DistributedTransaction/Test1.tla
View File

@ -4,9 +4,10 @@ EXTENDS DistributedTransaction, TLC
CONSTANT k1, k2
CONSTANT c1, c2, c3
Key == {k1, k2}
Keys == {k1, k2}
OptimistiicClient == {c3}
PessimisticClient == {c1, c2}
ClientKey == c1 :> {k1, k2} @@ c2 :> {k1} @@ c3 :> {k1, k2}
ClientReadKeys == c1 :> {} @@ c2 :> {} @@ c3 :> {k1, k2}
ClientWriteKeys == c1 :> {k1, k2} @@ c2 :> {k1} @@ c3 :> {k1, k2}
ClientPrimary == c1 :> k1 @@ c2 :> k1 @@ c3 :> k2
================================================================================

7
DistributedTransaction/Test2.cfg
View File

@ -7,10 +7,11 @@ CONSTANT
c3 = c3
CONSTANT
KEY <- Key
KEY <- Keys
OPTIMISTIC_CLIENT <- OptimistiicClient
PESSIMISTIC_CLIENT <- PessimisticClient
CLIENT_KEY <- ClientKey
CLIENT_READ_KEY <- ClientReadKeys
CLIENT_WRITE_KEY <- ClientWriteKeys
CLIENT_PRIMARY <- ClientPrimary
INIT
@ -27,4 +28,6 @@ INVARIANT
WriteConsistency
UniqueLockOrWrite
UniqueWrite
OptimisticReadSnapshotIsolation
PessimisticReadSnapshotIsolation
MsgTsConsistency

5
DistributedTransaction/Test2.tla
View File

@ -4,9 +4,10 @@ EXTENDS DistributedTransaction, TLC
CONSTANT k1, k2, k3
CONSTANT c1, c2, c3
Key == {k1, k2, k3}
Keys == {k1, k2, k3}
OptimistiicClient == {c3}
PessimisticClient == {c1, c2}
ClientKey == c1 :> {k1, k2, k3} @@ c2 :> {k1, k2} @@ c3 :> {k1, k3}
ClientReadKeys == c1 :> {} @@ c2 :> {} @@ c3 :> {k1, k3}
ClientWriteKeys == c1 :> {k1, k2, k3} @@ c2 :> {k1, k2} @@ c3 :> {k1, k3}
ClientPrimary == c1 :> k1 @@ c2 :> k1 @@ c3 :> k3
================================================================================

31
DistributedTransaction/Test3.cfg Normal file
View File

@ -0,0 +1,31 @@
CONSTANT
k1 = k1
k2 = k2
c1 = c1
c2 = c2
CONSTANT
KEY <- Keys
OPTIMISTIC_CLIENT <- OptimistiicClient
PESSIMISTIC_CLIENT <- PessimisticClient
CLIENT_READ_KEY <- ClientReadKeys
CLIENT_WRITE_KEY <- ClientWriteKeys
CLIENT_PRIMARY <- ClientPrimary
INIT
Init
NEXT
Next
INVARIANT
TypeOK
UniqueCommitOrAbort
CommitConsistency
AbortConsistency
WriteConsistency
UniqueLockOrWrite
UniqueWrite
OptimisticReadSnapshotIsolation
PessimisticReadSnapshotIsolation
MsgTsConsistency

13
DistributedTransaction/Test3.tla Normal file
View File

@ -0,0 +1,13 @@
--------------------------------- MODULE Test3 ---------------------------------
EXTENDS DistributedTransaction, TLC
CONSTANT k1, k2
CONSTANT c1, c2
Keys == {k1, k2}
OptimistiicClient == {c2}
PessimisticClient == {c1}
ClientReadKeys == c1 :> {} @@ c2 :> {k1, k2}
ClientWriteKeys == c1 :> {k1, k2} @@ c2 :> {k1, k2}
ClientPrimary == c1 :> k1 @@ c2 :> k1
================================================================================

30
DistributedTransaction/Test4.cfg Normal file
View File

@ -0,0 +1,30 @@
CONSTANT
k1 = k1
c1 = c1
c2 = c2
CONSTANT
KEY <- Keys
OPTIMISTIC_CLIENT <- OptimistiicClient
PESSIMISTIC_CLIENT <- PessimisticClient
CLIENT_READ_KEY <- ClientReadKeys
CLIENT_WRITE_KEY <- ClientWriteKeys
CLIENT_PRIMARY <- ClientPrimary
INIT
Init
NEXT
Next
INVARIANT
TypeOK
UniqueCommitOrAbort
CommitConsistency
AbortConsistency
WriteConsistency
UniqueLockOrWrite
UniqueWrite
OptimisticReadSnapshotIsolation
PessimisticReadSnapshotIsolation
MsgTsConsistency

13
DistributedTransaction/Test4.tla Normal file
View File

@ -0,0 +1,13 @@
--------------------------------- MODULE Test3 ---------------------------------
EXTENDS DistributedTransaction, TLC
CONSTANT k1
CONSTANT c1, c2
Keys == {k1}
OptimistiicClient == {c2}
PessimisticClient == {c1}
ClientReadKeys == c1 :> {} @@ c2 :> {k1}
ClientWriteKeys == c1 :> {k1} @@ c2 :> {k1}
ClientPrimary == c1 :> k1 @@ c2 :> k1
================================================================================

33
DistributedTransaction/Test5.cfg Normal file
View File

@ -0,0 +1,33 @@
CONSTANT
k1 = k1
k2 = k2
k3 = k3
c1 = c1
c2 = c2
c3 = c3
CONSTANT
KEY <- Keys
OPTIMISTIC_CLIENT <- OptimistiicClient
PESSIMISTIC_CLIENT <- PessimisticClient
CLIENT_READ_KEY <- ClientReadKeys
CLIENT_WRITE_KEY <- ClientWriteKeys
CLIENT_PRIMARY <- ClientPrimary
INIT
Init
NEXT
Next
INVARIANT
TypeOK
UniqueCommitOrAbort
CommitConsistency
AbortConsistency
WriteConsistency
UniqueLockOrWrite
UniqueWrite
OptimisticReadSnapshotIsolation
PessimisticReadSnapshotIsolation
MsgTsConsistency

13
DistributedTransaction/Test5.tla Normal file
View File

@ -0,0 +1,13 @@
--------------------------------- MODULE Test5 ---------------------------------
EXTENDS DistributedTransaction, TLC
CONSTANT k1, k2, k3
CONSTANT c1, c2, c3
Keys == {k1, k2, k3}
OptimistiicClient == {c3}
PessimisticClient == {c1, c2}
ClientReadKeys == c1 :> {} @@ c2 :> {} @@ c3 :> {k1, k3}
ClientWriteKeys == c1 :> {k1, k2, k3} @@ c2 :> {k1, k2} @@ c3 :> {k2, k3}
ClientPrimary == c1 :> k1 @@ c2 :> k1 @@ c3 :> k3
================================================================================