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)