refactor(spec): update existing tla specs with apalache type system 1…

….2 (#193)

* update transfer spec

* update counter spec

* update reactor

* update tests

* fix cli test

* project rules ci

* update modelator version

* update deps

* update poetry lock

* update readme

* update pre-generated traces

* instructions to set up apalache

* comments in markdown

* keep consistent index style with python reactors

* remove length based counter

* informative renaming

.github/workflows/project.yml

@@ -0,0 +1,22 @@
+name: Check project rules
+
+on:
+  workflow_dispatch:
+  push:
+    paths:
+      - .github/workflows/project.yml
+      - pyproject.toml
+
+jobs:
+  dependency-version-check:
+    runs-on: "ubuntu-latest"
+    container: "archlinux"
+    steps:
+      - name: Install dependencies
+        run: |
+          pacman -Syu --needed --noconfirm git yq
+      - name: Check out repository
+        uses: actions/checkout@v3
+      - name: Check for git version
+        run: |
+          cat pyproject.toml | tomlq -r '.tool.poetry.dependencies[].git?' | (! grep --invert-match null)

examples/cosmos-sdk/transfer/transfer.tla

@@ -1,10 +1,10 @@
 ---- MODULE transfer ----
-EXTENDS Apalache, Integers, FiniteSets
+EXTENDS Variants, Integers
 
 VARIABLES
     \* @type: Str -> Int;
     balances,
-    \* @type: [tag: Str, value: [wallets: Set(Str), sender: Str, receiver: Str, amount: Int]];
+    \* @type: Init({wallets: Set(Str)}) | Transfer({sender: Str, receiver: Str, amount: Int});
     action,
     \* @type: Int;
     step
@@ -13,7 +13,7 @@ WALLETS == {"Alice", "Bob"}
 
 Init ==
     /\ balances = [wallet \in WALLETS |-> 100]
-    /\ action = [tag |-> "Init", value |-> [wallets |-> WALLETS]]
+    /\ action = Variant("Init", [wallets |-> WALLETS])
     /\ step = 0
 
 Next ==
@@ -26,13 +26,15 @@ Next ==
             ![sender] = @ - amount,
             ![receiver] = @ + amount
             ]
-        /\ action' = [tag |-> "Transfer", value |-> [sender |-> sender, receiver |-> receiver, amount |-> amount]]
+        /\ action' = Variant("Transfer", [sender |-> sender, receiver |-> receiver, amount |-> amount])
     /\ step' = step + 1
 
 View ==
-    IF action.tag = "Transfer"
-    THEN action.value
-    ELSE [sender |-> "", receiver |-> "", amount |-> 0]
+    VariantGetOrElse(
+        "Transfer",
+        action,
+        [sender |-> "", receiver |-> "", amount |-> 0]
+    )
 
 TestAliceZero == balances["Alice"] = 0
 

examples/cosmwasm/counter/README.md

@@ -21,13 +21,29 @@ git clone --depth 1 https://github.com/CosmWasm/wasmd
 ls wasmd/build/wasmd # wasmd binary
 ```
 
-### Finally run the tests
+### Make sure Atomkraft is installed and set up Apalache
+
+```
+atomkraft model apalache get # to download and set up apalache
+atomkraft model apalache info # confirm apalache distribution
+```
+
+### Generate traces
+
+```sh
+atomkraft model simulate --model-path models/counter.tla --max-trace 10 --length 10 --traces-dir traces --view=View
+```
+
+### Run tests on generated traces
 
 ```sh
-atomkraft test trace --path traces/example0.itf.json --reactor reactors/reactor.py --keypath last_msg.name
+# just one trace
+atomkraft test trace --path traces/example1.itf.json --reactor reactors/reactor.py --keypath last_msg.tag
+# or all traces in a directory
+atomkraft test trace --path traces --reactor reactors/reactor.py --keypath last_msg.tag
 ```
 
-## Recipe of this example project
+## Recipe for this example project
 
 ### Install/update `atomkraft` cli
 

examples/cosmwasm/counter/models/counter.tla

@@ -1,54 +1,48 @@
 --------------------------- MODULE counter ---------------------------------
 
-EXTENDS Integers, Apalache, Sequences
-
-
-\* CONSTANTS
-\*     \* @type: Int;
-\*     MAX_STEP,
-\*     \* @type: Int;
-\*     MAX_ACCOUNTS
+EXTENDS Integers, Variants, Sequences
 
 \* @type: () => Int;
 MAX_STEP == 20
 \* @type: () => Int;
 MAX_ACCOUNTS == 3
 
+(*
+@typeAlias: message = Instantiate({sender: Int, count: Int})
+                    | Reset({sender: Int, count: Int})
+                    | Increment({sender: Int})
+                    | GetCount({sender: Int})
+                    | StoreCwContract({sender: Int})
+                    ;
+*)
+typedef == TRUE
+
+
 VARIABLES
     \* @type: Int;
     count,
     \* @type: Int;
     owner,
     \* @type: Bool;
     instantiated,
-    \* @type: [name:Str, cnt: Int];
+    \* @type: $message;
     last_msg,
-    \* @type: Seq([name:Str, cnt: Int]);
+    \* @type: Seq($message);
     messages,
     \* @type: Int;
     stepCount
 
-\* @type: () => Str;
-INSTANTIATE == "instantiate"
-\* @type: () => Str;
-RESET == "reset"
-\* @type: () => Str;
-INCREMENT == "increment"
-\* @type: () => Str;
-GET_COUNT == "get_count"
-\* @type: () => Str;
-STORE_CW == "store_cw_contract"
-
-\* @type: (Int, Int) => [name: Str, sender: Int, cnt: Int];
-Instaniate(_sender, val) == [name |-> INSTANTIATE, sender |-> _sender, cnt |-> val]
-\* @type: (Int, Int) => [name: Str, sender: Int, cnt: Int];
-Reset(_sender, val) == [name |-> RESET, sender |-> _sender, cnt |-> val]
-\* @type: (Int) => [name: Str, sender: Int];
-Increment(_sender) == [name |-> INCREMENT, sender |-> _sender]
-\* @type: (Int) => [name: Str, sender: Int];
-GetCount(_sender) == [name |-> GET_COUNT, sender |-> _sender]
-\* @type: (Int) => [name: Str, sender: Int];
-StoreCW(_sender) == [name |-> STORE_CW, sender |-> _sender]
+
+\* @type: (Int, Int) => $message;
+Instaniate(_sender, _count) == Variant("Instantiate", [sender |-> _sender, count |-> _count])
+\* @type: (Int, Int) => $message;
+Reset(_sender, _count) == Variant("Reset", [sender |-> _sender, count |-> _count])
+\* @type: (Int) => $message;
+Increment(_sender) == Variant("Increment", [sender |-> _sender])
+\* @type: (Int) => $message;
+GetCount(_sender) == Variant("GetCount", [sender |-> _sender])
+\* @type: (Int) => $message;
+StoreCW(_sender) == Variant("StoreCwContract", [sender |-> _sender])
 
 
 \* @type: () => Set(Int);
@@ -69,9 +63,10 @@ ProcessInstantiate(_sender, _count) ==
     /\ instantiated' = TRUE
 
 InstaniateNext(_sender) ==
-    \E instantiate_cnt \in 0..100:
-        LET msg == Instaniate(_sender, instantiate_cnt) IN
-        /\ ProcessInstantiate(msg.sender, msg.cnt)
+    \E instantiate_count \in 0..100:
+        LET msg == Instaniate(_sender, instantiate_count) IN
+        LET msg_unpacked == VariantGetUnsafe("Instantiate", msg) IN
+        /\ ProcessInstantiate(msg_unpacked.sender, msg_unpacked.count)
         /\ last_msg' = msg
 
 ProcessReset(_owner, _sender, _count) ==
@@ -81,9 +76,10 @@ ProcessReset(_owner, _sender, _count) ==
     /\ UNCHANGED<<owner, instantiated>>
 
 ResetNext(_sender) ==
-    \E reset_cnt \in 0..100:
-        LET msg == Reset(_sender, reset_cnt) IN
-        /\ ProcessReset(owner, msg.sender, msg.cnt)
+    \E reset_count \in 0..100:
+        LET msg == Reset(_sender, reset_count) IN
+        LET msg_unpacked == VariantGetUnsafe("Reset", msg) IN
+        /\ ProcessReset(owner, msg_unpacked.sender, msg_unpacked.count)
         /\ last_msg' = msg
 
 ProcessIncrement ==
@@ -114,8 +110,5 @@ Next==
     /\ messages' = Append(messages, last_msg)
     /\ stepCount' = stepCount + 1
 
-Inv == stepCount < MAX_STEP
-
-View == <<count,owner,last_msg>>
-View2 == last_msg.name
+View == <<owner,VariantTag(last_msg)>>
 ===============================================================================

examples/cosmwasm/counter/reactors/reactor.py

@@ -20,9 +20,10 @@ def state():
     return {}
 
 
-@step("store_cw_contract")
+@step("StoreCwContract")
 def store_contract(testnet: Testnet, state: Dict, last_msg):
-    logging.info("Step: store_cw_contract")
+    last_msg = last_msg.value
+    logging.info("Step: StoreCwContract")
     testnet.oneshot()
     time.sleep(10)
 
@@ -65,10 +66,11 @@ def store_contract(testnet: Testnet, state: Dict, last_msg):
     time.sleep(0.5)
 
 
-@step("instantiate")
+@step("Instantiate")
 def instantiate(testnet: Testnet, state: Dict, last_msg):
-    logging.info("Step: instantiate")
-    dict_msg = {"count": last_msg["cnt"]}
+    last_msg = last_msg.value
+    logging.info("Step: Instantiate")
+    dict_msg = {"count": last_msg.count}
 
     msg = MsgInstantiateContract(
         sender=testnet.acc_addr(last_msg.sender),
@@ -100,10 +102,11 @@ def instantiate(testnet: Testnet, state: Dict, last_msg):
     state["contract_address"] = contract_address
 
 
-@step("reset")
+@step("Reset")
 def reset(testnet: Testnet, state: Dict, last_msg):
-    logging.info("Step: reset")
-    dict_msg = {"reset": {"count": last_msg["cnt"]}}
+    last_msg = last_msg.value
+    logging.info("Step: Reset")
+    dict_msg = {"reset": {"count": last_msg.count}}
     contract_address = state["contract_address"]
 
     msg = MsgExecuteContract(
@@ -125,9 +128,10 @@ def reset(testnet: Testnet, state: Dict, last_msg):
         logging.info("\tlog:  %s\n", result.raw_log)
 
 
-@step("increment")
+@step("Increment")
 def increment(testnet: Testnet, state: Dict, last_msg):
-    logging.info("Step: increment")
+    last_msg = last_msg.value
+    logging.info("Step: Increment")
     dict_msg = {"increment": {}}
     contract_address = state["contract_address"]
 
@@ -150,9 +154,9 @@ def increment(testnet: Testnet, state: Dict, last_msg):
         logging.info("\tlog:  %s\n", result.raw_log)
 
 
-@step("get_count")
+@step("GetCount")
 def get_count(testnet: Testnet, state: Dict, count):
-    logging.info("Step: get_count")
+    logging.info("Step: GetCount")
 
     dict_msg = {"get_count": {}}
     contract_address = state["contract_address"]

examples/cosmwasm/counter/tests/test_wasm.py

@@ -1,13 +1,13 @@
 from modelator.pytest.decorators import itf, mbt
 
 
-@mbt("models/counter.tla", keypath="last_msg.name", checker_params={"view", "View2"})
+@mbt("models/counter.tla", keypath="last_msg.tag", checker_params={"view", "View2"})
 def test_traces_from_model():
     print("auto-generated traces from tla file executed succesfully")
 
 
-@itf("traces/example0.itf.json", keypath="last_msg.name")
-@itf("traces/example1.itf.json", keypath="last_msg.name")
-@itf("traces/example2.itf.json", keypath="last_msg.name")
+@itf("traces/example0.itf.json", keypath="last_msg.tag")
+@itf("traces/example1.itf.json", keypath="last_msg.tag")
+@itf("traces/example2.itf.json", keypath="last_msg.tag")
 def test_use_generated_traces():
     print("itf traces executed succesfully")