Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add async commit check #38

Open
wants to merge 30 commits into
base: master
Choose a base branch
from
Open

Add async commit check #38

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
30 commits
Select commit Hold shift + click to select a range
36b46f2
Add CheckTxnStatus Msgs
zhuo1angT Jun 2, 2021
d50703f
Add CheckTxnStatus, haven't checked by the TLC
zhuo1angT Jun 4, 2021
0a21889
Add SI check
zhuo1angT Jun 22, 2021
913a5c3
DistributedTransactions: extract unlock_key function
zhuo1angT Jul 7, 2021
2b21d14
DistributedTransactions: upd max read times
zhuo1angT Jul 10, 2021
07caa8d
DistributedTransaction: Add max client check txn times
zhuo1angT Jul 11, 2021
33cb86e
fix wrong pessimistic lock amend
zhuo1angT Jul 12, 2021
6f67db9
upd read SI check
zhuo1angT Jul 19, 2021
3a30dad
upd
zhuo1angT Jul 29, 2021
42642e3
apply code review suggestion
zhuo1angT Aug 13, 2021
959dacc
restucture distributed transaction spec
andylokandy Aug 17, 2021
6ed4051
fix comment
andylokandy Aug 17, 2021
3e2ebb4
update comment
andylokandy Aug 17, 2021
0051d7d
update assume
andylokandy Aug 17, 2021
7ee3808
update comment
andylokandy Aug 17, 2021
04e021d
enable snapshot checks
andylokandy Aug 18, 2021
fa38768
fix pessimistic si check
andylokandy Aug 18, 2021
c04c627
add comment
andylokandy Aug 18, 2021
7fff07d
add comment
andylokandy Aug 18, 2021
d21e46e
add comment
andylokandy Aug 18, 2021
37d05aa
fix typo
andylokandy Aug 18, 2021
f30aac4
fix dead end in optimistic prewrite
andylokandy Aug 19, 2021
53f3141
add test5
andylokandy Aug 19, 2021
44f333d
Add variables key_max_ts
zhuo1angT Aug 20, 2021
84d57ed
Update async lock, async prewrite msg
zhuo1angT Aug 20, 2021
bb0f92b
Update async prewrited, async client commit
zhuo1angT Aug 21, 2021
b79a5a5
Update async commit, overlap record, invarint check
zhuo1angT Aug 21, 2021
bfeb6dc
Fix a previous bug, fix check
zhuo1angT Aug 21, 2021
33a1d26
Fix many bugs
zhuo1angT Aug 22, 2021
aaa0631
Fix many bugs
zhuo1angT Aug 22, 2021
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 4 additions & 0 deletions .gitignore
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,3 +5,7 @@ states/
**/*.toolbox/*___*_SnapShot_*.launch
**/*.toolbox/.project
**/*.toolbox/.settings/
**/*.toolbox/*.aux
**/*.toolbox/*.log
**/*.toolbox/*.pdf
**/*.toolbox/*.tex
Binary file modified DistributedTransaction/DistributedTransaction.pdf
View file
Open in desktop
Binary file not shown.
1,155 changes: 820 additions & 335 deletions DistributedTransaction/DistributedTransaction.tla
View file
Open in desktop

Large diffs are not rendered by default.

122 changes: 62 additions & 60 deletions DistributedTransaction/DistributedTransaction.toolbox/DistributedTransaction___Test1.launch
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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 changes: 60 additions & 42 deletions DistributedTransaction/DistributedTransaction.toolbox/DistributedTransaction___Test2.launch
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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 changes: 60 additions & 0 deletions DistributedTransaction/DistributedTransaction.toolbox/DistributedTransaction___Test3.launch
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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 changes: 65 additions & 0 deletions DistributedTransaction/DistributedTransaction.toolbox/DistributedTransaction___Test4.launch
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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>
Loading