added mbt vars

informalsystems · Dec 10, 2024 · c1e2e0d · c1e2e0d
1 parent 7b968e5
commit c1e2e0d
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 2 deletions.
diff --git a/quint/src/cliCommands.ts b/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)

diff --git 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<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 +167,7 @@ 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,