From 5e02db1bfb3656819197a1a9ca41911d084cc9c6 Mon Sep 17 00:00:00 2001
From: Yilin Chen <sticnarf@gmail.com>
Date: Mon, 21 Oct 2019 17:36:20 +0800
Subject: [PATCH] add start action

Signed-off-by: Yilin Chen <sticnarf@gmail.com>
---
 .../PessimisticTransaction.tla                | 42 +++++++++++++------
 .../PessimisticTransaction___Test1.launch     |  2 +-
 2 files changed, 30 insertions(+), 14 deletions(-)

diff --git a/PessimisticTransaction/PessimisticTransaction.tla b/PessimisticTransaction/PessimisticTransaction.tla
index 6c1beff..8cf7394 100644
--- a/PessimisticTransaction/PessimisticTransaction.tla
+++ b/PessimisticTransaction/PessimisticTransaction.tla
@@ -65,22 +65,39 @@ Pos == {x \in Nat : x > 0}
 
 -----------------------------------------------------------------------------
 
+Start(c) ==
+  /\ client_state[c] = "init"
+  /\ next_ts' = next_ts + 1
+  /\ \E ks \in SUBSET KEY:
+       \E primary \in ks:
+         client_key' =
+           [client_key EXCEPT 
+             ![c] = [primary |-> primary,
+                     secondary |-> ks \ {primary},
+                     pessimistic |-> ks,
+                     pending |-> ks]
+           ]
+  /\ client_state' = [client_state EXCEPT ![c] = "working"]
+  /\ client_ts' = [client_ts EXCEPT ![c].start_ts = next_ts']
+  /\ UNCHANGED <<key_vars, msg>>
+
 Init ==
     /\ next_ts = 1
     /\ client_state = [c \in CLIENT |-> "init"]
     /\ client_ts = [c \in CLIENT |-> [start_ts |-> 0,
                                       for_update_ts |-> 0,
-                                      commit_ts |-> 0]
-                   ]
+                                      commit_ts |-> 0]]
     /\ client_key = [c \in CLIENT |-> {}]
     /\ key_lock = [k \in KEY |-> {}]
     /\ key_data = [k \in KEY |-> {}]
     /\ key_write = [k \in KEY |-> {}]
     /\ key_last_read_ts = [k \in KEY |-> 0]
     /\ msg = {}
-    
-Next ==
-  UNCHANGED <<client_vars, key_vars, vars>>
+
+ClientOp(c) ==
+  \/ Start(c)
+      
+Next == \E c \in CLIENT : ClientOp(c)
 
 -----------------------------------------------------------------------------
 
@@ -97,14 +114,13 @@ ClientTsTypeInv ==
   [CLIENT -> [start_ts : Nat, for_update_ts: Nat, commit_ts : Nat]]
   
 ClientKeyTypeInv ==
-  client_key \in [
-    CLIENT -> {{}} \union [
-      primary: KEY,
-      secondary: SUBSET KEY,
-      pessimistic: SUBSET KEY,
-      pending : SUBSET KEY
-    ]
-  ]
+  \A c \in CLIENT:
+    \/ client_state[c] = "init"
+    \/ client_key[c] \in [primary: KEY,
+                secondary: SUBSET KEY,
+                pessimistic: SUBSET KEY,
+                pending : SUBSET KEY
+               ]
   
 KeyDataTypeInv ==
   key_data \in [KEY -> SUBSET [ts: Pos]]
diff --git a/PessimisticTransaction/PessimisticTransaction.toolbox/PessimisticTransaction___Test1.launch b/PessimisticTransaction/PessimisticTransaction.toolbox/PessimisticTransaction___Test1.launch
index ff25b25..6447acc 100644
--- a/PessimisticTransaction/PessimisticTransaction.toolbox/PessimisticTransaction___Test1.launch
+++ b/PessimisticTransaction/PessimisticTransaction.toolbox/PessimisticTransaction___Test1.launch
@@ -5,7 +5,7 @@
     <stringAttribute key="distributedNetworkInterface" value="192.168.220.40"/>
     <intAttribute key="distributedNodesCount" value="1"/>
     <stringAttribute key="distributedTLC" value="off"/>
-    <intAttribute key="fpIndex" value="80"/>
+    <intAttribute key="fpIndex" value="37"/>
     <intAttribute key="maxHeapSize" value="25"/>
     <stringAttribute key="modelBehaviorInit" value="Init"/>
     <stringAttribute key="modelBehaviorNext" value="Next"/>