Merge pull request #1559 from informalsystems/ivan/mbtVars

Variables of the flag --mbt included into the ITF trace

CHANGELOG.md

@@ -28,6 +28,8 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 ### Removed
 ### Fixed
 
+- Changed the `--mbt` variables representation into `mbt::actionTaken` and `mbt::nondetPicks`. 
+Added those variables to the `vars` field of the ITF json so that they are displayed correctly in the trace viewer.
 - Fixed a problem where traces other than the first one when `--n-traces` > 1
   and `--mbt` is true had the incorrect `action_taken` and `nondet_picks` values
   (#1553).

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).
 

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", mbt::nondetPicks: {  }, n: 1 }
 
-[State 1] { action_taken: "OnPositive", n: 2, nondet_picks: {  } }
+[State 1] { mbt::actionTaken: "OnPositive", mbt::nondetPicks: {  }, n: 2 }
 
-[State 2] { action_taken: "OnPositive", n: 3, nondet_picks: {  } }
+[State 2] { mbt::actionTaken: "OnPositive", mbt::nondetPicks: {  }, n: 3 }
 
-[State 3] { action_taken: "OnDivByThree", n: 6, nondet_picks: {  } }
+[State 3] { mbt::actionTaken: "OnDivByThree", mbt::nondetPicks: {  }, n: 6 }
 
-[State 4] { action_taken: "OnDivByThree", n: 12, nondet_picks: {  } }
+[State 4] { mbt::actionTaken: "OnDivByThree", mbt::nondetPicks: {  }, n: 12 }
 
 [violation] Found an issue (duration).
 Use --verbosity=3 to show executions.
@@ -502,30 +502,30 @@ An example execution:
 
 [State 0]
 {
-  action_taken: "init",
   balances: Map("alice" -> 0, "bob" -> 0, "charlie" -> 0),
-  nondet_picks: { account: None, amount: None }
+  mbt::actionTaken: "init",
+  mbt::nondetPicks: { account: None, amount: None }
 }
 
 [State 1]
 {
-  action_taken: "deposit",
   balances: Map("alice" -> 0, "bob" -> 0, "charlie" -> 53),
-  nondet_picks: { account: Some("charlie"), amount: Some(53) }
+  mbt::actionTaken: "deposit",
+  mbt::nondetPicks: { account: Some("charlie"), amount: Some(53) }
 }
 
 [State 2]
 {
-  action_taken: "deposit",
   balances: Map("alice" -> 26, "bob" -> 0, "charlie" -> 53),
-  nondet_picks: { account: Some("alice"), amount: Some(26) }
+  mbt::actionTaken: "deposit",
+  mbt::nondetPicks: { account: Some("alice"), amount: Some(26) }
 }
 
 [State 3]
 {
-  action_taken: "withdraw",
   balances: Map("alice" -> -13, "bob" -> 0, "charlie" -> 53),
-  nondet_picks: { account: Some("alice"), amount: Some(39) }
+  mbt::actionTaken: "withdraw",
+  mbt::nondetPicks: { account: Some("alice"), amount: Some(39) }
 }
 
 [violation] Found an issue (duration).
@@ -816,7 +816,6 @@ rm out-itf-mbt-example.itf.json
   "#meta": {
     "index": 1
   },
-  "action_taken": "mint",
   "balances": {
     "#map": [
       [
@@ -851,8 +850,8 @@ rm out-itf-mbt-example.itf.json
       ]
     ]
   },
-  "minter": "bob",
-  "nondet_picks": {
+  "mbt::actionTaken": "mint",
+  "mbt::nondetPicks": {
     "amount": {
       "tag": "Some",
       "value": {
@@ -867,7 +866,8 @@ rm out-itf-mbt-example.itf.json
       "tag": "Some",
       "value": "bob"
     }
-  }
+  },
+  "minter": "bob"
 }
 ```
 
@@ -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
 ```
 

quint/src/cliCommands.ts

@@ -517,7 +517,7 @@ export async function runSimulator(prev: TypecheckedStage): Promise<CLIProcedure
       const itfFile: string | undefined = prev.args.outItf
       if (itfFile) {
         const filename = expandOutputTemplate(itfFile, index, { autoAppend: prev.args.nTraces > 1 })
-        const trace = toItf(vars, states)
+        const trace = toItf(vars, states, prev.args.mbt)
         if (trace.isRight()) {
           const jsonObj = addItfHeader(prev.args.input, status, trace.value)
           writeToJson(filename, jsonObj)

quint/src/itf.ts

@@ -25,6 +25,9 @@ export type ItfTrace = {
   loop?: number
 }
 
+export const ACTION_TAKEN = 'mbt::actionTaken'
+export const NONDET_PICKS = 'mbt::nondetPicks'
+
 export type ItfState = {
   '#meta'?: any
   // Mapping of state variables to their values in a state
@@ -86,7 +89,7 @@ function isUnserializable(v: ItfValue): v is ItfUnserializable {
  * @param states an array of expressions that represent the states
  * @returns an object that represent the trace in the ITF format
  */
-export function toItf(vars: string[], states: QuintEx[]): Either<string, ItfTrace> {
+export function toItf(vars: string[], states: QuintEx[], mbtMetadata: boolean = false): Either<string, ItfTrace> {
   const exprToItf = (ex: QuintEx): Either<string, ItfValue> => {
     switch (ex.kind) {
       case 'int':
@@ -167,6 +170,9 @@ export function toItf(vars: string[], states: QuintEx[]): Either<string, ItfTrac
       )
     )
   ).mapRight(s => {
+    if (mbtMetadata) {
+      vars = [...vars, ACTION_TAKEN, NONDET_PICKS]
+    }
     return {
       vars: vars,
       states: s,

quint/src/runtime/impl/VarStorage.ts

@@ -17,6 +17,7 @@ import { QuintError } from '../../quintError'
 import { RuntimeValue, rv } from './runtimeValue'
 import { Map as ImmutableMap } from 'immutable'
 import { CachedValue, Register } from './Context'
+import { ACTION_TAKEN, NONDET_PICKS } from '../../itf'
 
 /**
  * A named pointer to a value, so we can use the same reference in multiple places, and just update the value.
@@ -125,8 +126,8 @@ export class VarStorage {
           return [name, valueVariant]
         })
       )
-      map.push(['nondet_picks', nondetPicksRecord])
-      map.push(['action_taken', rv.mkStr(this.actionTaken ?? '')])
+      map.push([NONDET_PICKS, nondetPicksRecord])
+      map.push([ACTION_TAKEN, rv.mkStr(this.actionTaken ?? '')])
     }
 
     return rv.mkRecord(map)