From c1e2e0dfc29f126398df4f0160abc1cf8913b671 Mon Sep 17 00:00:00 2001 From: ivan-gavran Date: Tue, 10 Dec 2024 15:38:29 +0100 Subject: [PATCH 1/6] added mbt vars --- quint/src/cliCommands.ts | 2 +- quint/src/itf.ts | 3 ++- 2 files changed, 3 insertions(+), 2 deletions(-) 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 51a8723f6..a1432f9aa 100644 --- a/quint/src/itf.ts +++ b/quint/src/itf.ts @@ -86,7 +86,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 +167,7 @@ export function toItf(vars: string[], states: QuintEx[]): Either { + if (mbtMetadata) {vars = [...vars, 'action_taken', 'nondet_picks']} return { vars: vars, states: s, From 879bedef49ab79fa78ead62e0fd1e5e00ce40ae9 Mon Sep 17 00:00:00 2001 From: ivan-gavran Date: Mon, 16 Dec 2024 10:25:42 +0100 Subject: [PATCH 2/6] camelCase var names and mbt:: prefix --- quint/src/itf.ts | 5 ++++- quint/src/runtime/impl/VarStorage.ts | 5 +++-- 2 files changed, 7 insertions(+), 3 deletions(-) diff --git a/quint/src/itf.ts b/quint/src/itf.ts index a1432f9aa..1d62238a6 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 @@ -167,7 +170,7 @@ export function toItf(vars: string[], states: QuintEx[], mbtMetadata: boolean = ) ) ).mapRight(s => { - if (mbtMetadata) {vars = [...vars, 'action_taken', 'nondet_picks']} + 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) From 6f00f7b9c08ce00bacfb1fdda9489c932552227d Mon Sep 17 00:00:00 2001 From: ivan-gavran Date: Mon, 16 Dec 2024 10:29:27 +0100 Subject: [PATCH 3/6] CHANGELOG entry --- CHANGELOG.md | 2 ++ 1 file changed, 2 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index ffcfb5ec0..5e2adefaa 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -22,6 +22,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). From 6f45a7284b4b93449eebb79f3fdd00d8def6b831 Mon Sep 17 00:00:00 2001 From: ivan-gavran Date: Mon, 16 Dec 2024 10:44:17 +0100 Subject: [PATCH 4/6] formatting --- quint/src/itf.ts | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/quint/src/itf.ts b/quint/src/itf.ts index 1d62238a6..8715b285f 100644 --- a/quint/src/itf.ts +++ b/quint/src/itf.ts @@ -170,7 +170,9 @@ export function toItf(vars: string[], states: QuintEx[], mbtMetadata: boolean = ) ) ).mapRight(s => { - if (mbtMetadata) {vars = [...vars, ACTION_TAKEN, NONDET_PICKS]} + if (mbtMetadata) { + vars = [...vars, ACTION_TAKEN, NONDET_PICKS] + } return { vars: vars, states: s, From 42825c9118bc6d4fdd4549ef4b01697352352645 Mon Sep 17 00:00:00 2001 From: ivan-gavran Date: Mon, 16 Dec 2024 11:56:01 +0100 Subject: [PATCH 5/6] 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 ``` From c06f838769fa08b8e9c1339357e1fc7ca02e2f9d Mon Sep 17 00:00:00 2001 From: ivan-gavran Date: Tue, 17 Dec 2024 22:38:33 +0100 Subject: [PATCH 6/6] updated ordering of variables in expected test output --- quint/io-cli-tests.md | 26 +++++++++++++------------- 1 file changed, 13 insertions(+), 13 deletions(-) diff --git a/quint/io-cli-tests.md b/quint/io-cli-tests.md index 6ed786a8b..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] { mbt::actionTaken: "init", n: 1, mbt::nondetPicks: { } } +[State 0] { mbt::actionTaken: "init", mbt::nondetPicks: { }, n: 1 } -[State 1] { mbt::actionTaken: "OnPositive", n: 2, mbt::nondetPicks: { } } +[State 1] { mbt::actionTaken: "OnPositive", mbt::nondetPicks: { }, n: 2 } -[State 2] { mbt::actionTaken: "OnPositive", n: 3, mbt::nondetPicks: { } } +[State 2] { mbt::actionTaken: "OnPositive", mbt::nondetPicks: { }, n: 3 } -[State 3] { mbt::actionTaken: "OnDivByThree", n: 6, mbt::nondetPicks: { } } +[State 3] { mbt::actionTaken: "OnDivByThree", mbt::nondetPicks: { }, n: 6 } -[State 4] { mbt::actionTaken: "OnDivByThree", n: 12, mbt::nondetPicks: { } } +[State 4] { mbt::actionTaken: "OnDivByThree", mbt::nondetPicks: { }, n: 12 } [violation] Found an issue (duration). Use --verbosity=3 to show executions. @@ -502,29 +502,29 @@ An example execution: [State 0] { - mbt::actionTaken: "init", balances: Map("alice" -> 0, "bob" -> 0, "charlie" -> 0), + mbt::actionTaken: "init", mbt::nondetPicks: { account: None, amount: None } } [State 1] { - mbt::actionTaken: "deposit", balances: Map("alice" -> 0, "bob" -> 0, "charlie" -> 53), + mbt::actionTaken: "deposit", mbt::nondetPicks: { account: Some("charlie"), amount: Some(53) } } [State 2] { - mbt::actionTaken: "deposit", balances: Map("alice" -> 26, "bob" -> 0, "charlie" -> 53), + mbt::actionTaken: "deposit", mbt::nondetPicks: { account: Some("alice"), amount: Some(26) } } [State 3] { - mbt::actionTaken: "withdraw", balances: Map("alice" -> -13, "bob" -> 0, "charlie" -> 53), + mbt::actionTaken: "withdraw", mbt::nondetPicks: { account: Some("alice"), amount: Some(39) } } @@ -816,7 +816,6 @@ rm out-itf-mbt-example.itf.json "#meta": { "index": 1 }, - "mbt::actionTaken": "mint", "balances": { "#map": [ [ @@ -851,7 +850,7 @@ rm out-itf-mbt-example.itf.json ] ] }, - "minter": "bob", + "mbt::actionTaken": "mint", "mbt::nondetPicks": { "amount": { "tag": "Some", @@ -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].mbt::actionTaken' +cat out-itf-example1.itf.json | jq '.states[0]["mbt::actionTaken"]' rm out-itf-example*.itf.json ```