timelock_mon_txs/tests.tla

doc/case-studies/timelock/timelock_mon_tests.tla

@@ -0,0 +1,51 @@
+---- MODULE timelock_mon_tests ----
+
+EXTENDS timelock_mon_txs
+
+
+\****************************************************************************************
+\* Monitor tests
+\* Each monitor test is a tuple of 
+\* (Init, TxRes, Mon) which should be produced / filled 
+\* by fetcher / verifier, where:
+\* - Init is any initial predicate
+\* - TxRes is a conjunction of any of Tx and Res predicates
+\* - Mon is any monitor predicate; produced from monitor specs
+\*
+\* A monitor test is validated via running
+\* apalache-mc check --length=1 --init=Init --next=TxRes --inv=Mon timelock_mon_tests.tla
+\* 
+\****************************************************************************************
+
+
+\*****************************
+\* Monitor predicates
+\* Produced from monitor specs
+\*****************************
+
+Mon_MustFail_deposit_TooManyClaimants == 
+    MustFail_deposit_TooManyClaimants => tx'.status = FALSE
+
+Mon_MustFail_deposit_Unauthorized ==
+    MustFail_deposit_Unauthorized => tx'.status = FALSE
+
+Mon_MustFail_deposit_NotEnoughBalance ==
+    MustFail_deposit_NotEnoughBalance => tx'.status = FALSE
+
+
+
+\******************************
+\* Tx & Result combined
+\* Used here for manual testing
+\******************************
+
+TxRes_Deposit1_Pass == 
+    /\ Tx_Deposit1
+    /\ Res_Pass
+
+TxRes_Deposit1_Fail == 
+    /\ Tx_Deposit1
+    /\ Res_Fail
+
+
+===========================================

doc/case-studies/timelock/timelock_mon_txs.tla

@@ -0,0 +1,64 @@
+---- MODULE timelock_mon_txs ----
+
+EXTENDS timelock_mon
+
+\************************
+\* Initial states
+\************************
+
+\* A completely non-deterministic initial state
+
+Init_Nondet == 
+    /\ env = Gen(10)
+    /\ tx = Gen(10)
+    /\ args = Gen(11)
+    /\ Balance = Gen(10)
+    /\ token_balances = Gen(10)
+
+
+Init_NoTokens == Init_Nondet
+    /\ token_balances =  SetAsFun({})
+    /\ env.instance_storage = {}
+
+Init_AliceHasTokens_NoBalance == Init_Nondet
+    /\ token_balances =  SetAsFun({
+        << "TOK", SetAsFun({ <<"alice", 100>>}) >>
+       })
+    /\ env.instance_storage = {}
+
+\************************
+\* Transactions
+\************************
+
+\* A completely non-deterministic transaction state
+
+Tx_Nondet == 
+    /\ env' = Gen(10)
+    /\ tx' = Gen(10)
+    /\ args' = args
+    /\ Balance' = Gen(10)
+    /\ token_balances' = Gen(10)
+
+
+Tx_Deposit1 == Tx_Nondet
+    /\ tx.method_name = "deposit"
+    /\ tx.signatures = { "alice", "bob", "carol" }
+    /\ args.token = "TOK"
+    /\ args.amount = 100
+    /\ args.from = "alice"
+    /\ args.claimants = << "alice", "bob", "carol" >>
+    /\ args.time_bound = [ kind |-> "Before", timestamp |-> 42 ]
+
+
+\************************
+\* Resulting states
+\************************
+
+Res_Pass == Tx_Nondet
+    /\ tx'.status = TRUE
+
+Res_Fail == Tx_Nondet
+    /\ tx'.status = FALSE
+
+
+===========================================