diff --git a/CHANGELOG.md b/CHANGELOG.md index b9c3de7fa..06129051c 100644 --- a/CHANGELOG.md +++ b/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). 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..2e9c9427b 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", 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 ``` diff --git a/quint/src/cliCommands.ts b/quint/src/cliCommands.ts index a692e490a..a2a0b2fcb 100644 --- a/quint/src/cliCommands.ts +++ b/quint/src/cliCommands.ts @@ -517,7 +517,7 @@ export async function runSimulator(prev: TypecheckedStage): Promise 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) diff --git a/quint/src/itf.ts b/quint/src/itf.ts index b7d5bb6d4..6cc199be3 100644 --- a/quint/src/itf.ts +++ b/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 { +export function toItf(vars: string[], states: QuintEx[], mbtMetadata: boolean = false): Either { const exprToItf = (ex: QuintEx): Either => { switch (ex.kind) { case 'int': @@ -167,6 +170,9 @@ export function toItf(vars: string[], states: QuintEx[]): Either { + if (mbtMetadata) { + vars = [...vars, ACTION_TAKEN, NONDET_PICKS] + } return { vars: vars, states: s, diff --git a/quint/src/runtime/impl/VarStorage.ts b/quint/src/runtime/impl/VarStorage.ts index 78a975f0f..ed9557e57 100644 --- a/quint/src/runtime/impl/VarStorage.ts +++ b/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)