camelCase var names and mbt:: prefix

informalsystems · Dec 16, 2024 · 879bede · 879bede
1 parent c1e2e0d
commit 879bede
Show file tree

Hide file tree

Showing 2 changed files with 7 additions and 3 deletions.
diff --git 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
@@ -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)