remove last_tx from the monitor

freespek · Dec 5, 2024 · 7b3d551 · 7b3d551
1 parent a7495af
commit 7b3d551
Show file tree

Hide file tree

Showing 2 changed files with 10 additions and 13 deletions.
diff --git a/doc/case-studies/xycloans/MCxycloans_monitor.tla b/doc/case-studies/xycloans/MCxycloans_monitor.tla
@@ -61,7 +61,8 @@ Init ==
     /\ storage = init_stor
 
 Next ==
-    \* generate some values for the storage
+    \* Generate some values for the storage.
+    \* For value generation, we go over all addresses, not subsets of addresses.
     \E fpsu \in AMOUNTS, tid \in { "", XLM_TOKEN_SAC_TESTNET }:
       \E b, mfp, fpsp, tb \in [ ADDR -> AMOUNTS ]:
         LET new_stor == [
@@ -77,11 +78,14 @@ Next ==
             ]
         IN
         \E addr \in ADDR, amount \in AMOUNTS, success \in BOOLEAN:
-            /\  \/ initialize([ env |-> env, call |-> Initialize(XLM_TOKEN_SAC_TESTNET), status |-> success ])
-                \/ deposit([ env |-> env, call |-> Deposit(addr, amount), status |-> success ])
-                \/ borrow([ env |-> env, call |-> Borrow(addr, amount), status |-> success ])
-                \/ update_fee_rewards([ env |-> env, call |-> UpdateFeeRewards(addr), status |-> success ])
-            \* Propagate the new storage. For value generation, we go over all addresses, not subsets.
+            /\  \/ LET tx == [ env |-> env, call |-> Initialize(XLM_TOKEN_SAC_TESTNET), status |-> success ] IN
+                   initialize(tx) /\ last_tx' = tx
+                \/ LET tx == [ env |-> env, call |-> Deposit(addr, amount), status |-> success ] IN
+                   deposit(tx) /\ last_tx' = tx
+                \/ LET tx == [ env |-> env, call |-> Borrow(addr, amount), status |-> success ] IN
+                   borrow(tx) /\ last_tx' = tx
+                \/ LET tx == [ env |-> env, call |-> UpdateFeeRewards(addr), status |-> success ] IN
+                   update_fee_rewards(tx) /\ last_tx' = tx
             /\ storage' = IF success THEN new_stor ELSE storage
 
 \* restrict the executions to the successful transactions

diff --git a/doc/case-studies/xycloans/xycloans_monitor.tla b/doc/case-studies/xycloans/xycloans_monitor.tla
@@ -23,9 +23,6 @@ CONSTANT
 
 (* The internal state of our monitor (not of the contract) *)
 VARIABLES
-    \* The last monitored transaction.
-    \* @type: $tx;
-    last_tx,
     \* Shares per address.
     \* @type: Str -> Int;
     shares,
@@ -66,7 +63,6 @@ initialize(tx) ==
     \* these conditions are not required by a monitor, but needed to avoid spurious generated values
     /\ succeeds_with(tx,
         tx.env.storage.self_persistent = tx.env.old_storage.self_persistent)
-    /\ last_tx' = tx
     /\ shares' = [ addr \in {} |-> 0 ]
     /\ total_shares' = 0
     /\ fee_per_share_universal' = 0    
@@ -94,7 +90,6 @@ deposit(tx) ==
             /\ tx.env.storage.self_persistent.Balance[other] = tx.env.old_storage.self_persistent.Balance[other])
     /\ succeeds_with(tx, call.amount > 0)
     \* update the monitor state
-    /\ last_tx' = tx
     /\ shares' = new_shares
     /\ total_shares' = total_shares + call.amount
     /\ UNCHANGED fee_per_share_universal
@@ -121,7 +116,6 @@ borrow(tx) ==
     /\ succeeds_with(tx, tx.env.storage.self_persistent = tx.env.old_storage.self_persistent)
     /\ succeeds_with(tx, call.amount > 0)
     \* update the monitor state
-    /\ last_tx' = tx
     \* we update the fee per share to compute rewards later
     /\ fee_per_share_universal' = expected_fee_per_share_universal
     /\ UNCHANGED <<shares, total_shares>>
@@ -146,7 +140,6 @@ update_fee_rewards(tx) ==
     /\ succeeds_with(tx,
         tx.env.storage.self_persistent.Balance = tx.env.old_storage.self_persistent.Balance)
     \* update the monitor state
-    /\ last_tx' = tx
     /\ UNCHANGED <<shares, total_shares, fee_per_share_universal>>
 
 =============================================================================