From 42825c9118bc6d4fdd4549ef4b01697352352645 Mon Sep 17 00:00:00 2001
From: ivan-gavran <ivan@informal.systems>
Date: Mon, 16 Dec 2024 11:56:01 +0100
Subject: [PATCH] updated the docs and cli tests

---
 docs/pages/docs/quint.md |  6 +++---
 quint/io-cli-tests.md    | 32 ++++++++++++++++----------------
 2 files changed, 19 insertions(+), 19 deletions(-)

diff --git a/docs/pages/docs/quint.md b/docs/pages/docs/quint.md
index 8947bb038..ebeef10e2 100644
--- a/docs/pages/docs/quint.md
+++ b/docs/pages/docs/quint.md
@@ -264,10 +264,10 @@ Options:
 ### The `--mbt` flag
 When this flag is given, the Quint simulator will keep track of two additional
 variables on the traces it produces:
-- `action_taken`: The first action executed by the simulator on each step, reset
+- `mbt::actionTaken`: The first action executed by the simulator on each step, reset
   at every `any` evaluation. That is, if the spec has nested `any` statements,
-  `action_taken` will correspond to the action picked in the innermost `any`.
-- `nondet_picks`: A record with all `nondet` values that were picked since the
+  `mbt::actionTaken` will correspond to the action picked in the innermost `any`.
+- `mbt::nondetPicks`: A record with all `nondet` values that were picked since the
   last `any` was called (or since the start, if there were no `any` calls in the
   step).
 
diff --git a/quint/io-cli-tests.md b/quint/io-cli-tests.md
index 46e7d4910..6ed786a8b 100644
--- a/quint/io-cli-tests.md
+++ b/quint/io-cli-tests.md
@@ -466,15 +466,15 @@ exit $exit_code
 ```
 An example execution:
 
-[State 0] { action_taken: "init", n: 1, nondet_picks: {  } }
+[State 0] { mbt::actionTaken: "init", n: 1, mbt::nondetPicks: {  } }
 
-[State 1] { action_taken: "OnPositive", n: 2, nondet_picks: {  } }
+[State 1] { mbt::actionTaken: "OnPositive", n: 2, mbt::nondetPicks: {  } }
 
-[State 2] { action_taken: "OnPositive", n: 3, nondet_picks: {  } }
+[State 2] { mbt::actionTaken: "OnPositive", n: 3, mbt::nondetPicks: {  } }
 
-[State 3] { action_taken: "OnDivByThree", n: 6, nondet_picks: {  } }
+[State 3] { mbt::actionTaken: "OnDivByThree", n: 6, mbt::nondetPicks: {  } }
 
-[State 4] { action_taken: "OnDivByThree", n: 12, nondet_picks: {  } }
+[State 4] { mbt::actionTaken: "OnDivByThree", n: 12, mbt::nondetPicks: {  } }
 
 [violation] Found an issue (duration).
 Use --verbosity=3 to show executions.
@@ -502,30 +502,30 @@ An example execution:
 
 [State 0]
 {
-  action_taken: "init",
+  mbt::actionTaken: "init",
   balances: Map("alice" -> 0, "bob" -> 0, "charlie" -> 0),
-  nondet_picks: { account: None, amount: None }
+  mbt::nondetPicks: { account: None, amount: None }
 }
 
 [State 1]
 {
-  action_taken: "deposit",
+  mbt::actionTaken: "deposit",
   balances: Map("alice" -> 0, "bob" -> 0, "charlie" -> 53),
-  nondet_picks: { account: Some("charlie"), amount: Some(53) }
+  mbt::nondetPicks: { account: Some("charlie"), amount: Some(53) }
 }
 
 [State 2]
 {
-  action_taken: "deposit",
+  mbt::actionTaken: "deposit",
   balances: Map("alice" -> 26, "bob" -> 0, "charlie" -> 53),
-  nondet_picks: { account: Some("alice"), amount: Some(26) }
+  mbt::nondetPicks: { account: Some("alice"), amount: Some(26) }
 }
 
 [State 3]
 {
-  action_taken: "withdraw",
+  mbt::actionTaken: "withdraw",
   balances: Map("alice" -> -13, "bob" -> 0, "charlie" -> 53),
-  nondet_picks: { account: Some("alice"), amount: Some(39) }
+  mbt::nondetPicks: { account: Some("alice"), amount: Some(39) }
 }
 
 [violation] Found an issue (duration).
@@ -816,7 +816,7 @@ rm out-itf-mbt-example.itf.json
   "#meta": {
     "index": 1
   },
-  "action_taken": "mint",
+  "mbt::actionTaken": "mint",
   "balances": {
     "#map": [
       [
@@ -852,7 +852,7 @@ rm out-itf-mbt-example.itf.json
     ]
   },
   "minter": "bob",
-  "nondet_picks": {
+  "mbt::nondetPicks": {
     "amount": {
       "tag": "Some",
       "value": {
@@ -896,7 +896,7 @@ rm out-itf-example.itf.json
 ```
 quint run --out-itf=out-itf-example.itf.json --n-traces=3 --mbt --max-steps=5 --seed=123  ../examples/tutorials/coin.qnt
 cat out-itf-example0.itf.json | jq '.["#meta"].status'
-cat out-itf-example1.itf.json | jq '.states[0].action_taken'
+cat out-itf-example1.itf.json | jq '.states[0].mbt::actionTaken'
 rm out-itf-example*.itf.json
 ```