add comments

informalsystems · Sep 14, 2023 · 5ead02c · 5ead02c
1 parent f5852ca
commit 5ead02c
Show file tree

Hide file tree

Showing 3 changed files with 6 additions and 4 deletions.
diff --git a/quint/io-cli-tests.md b/quint/io-cli-tests.md
@@ -689,11 +689,11 @@ exit $exit_code
 ]
 ```
 
-### Test does not mean assignments (#1133)
+### Test does not skip assignments (#1133)
 
 See: https://github.com/informalsystems/quint/issues/1133
 
-FIXME
+FIXME: fix the traces found by the simulator once #1133 is resolved.
 
 <!-- !test in test1133 -->
 ```

diff --git a/quint/src/runtime/impl/compilerImpl.ts b/quint/src/runtime/impl/compilerImpl.ts
@@ -260,7 +260,7 @@ export class CompilerVisitor implements IRVisitor {
         eval: () => {
           if (app.opcode === inputDefName) {
             this.execListener.onUserOperatorCall(evalApp)
-            // do not return from '_', as it may span over multiple frames
+            // do not call onUserOperatorReturn on '_' later, as it may span over multiple frames
           } else {
             this.execListener.onUserOperatorCall(app)
           }

diff --git a/quint/src/runtime/trace.ts b/quint/src/runtime/trace.ts
@@ -227,7 +227,9 @@ class TraceRecorderImpl implements TraceRecorder {
     if (verbosity.hasUserOpTracking(this.verbosityLevel)) {
       const newFrame = { app: app, args: [], result: none(), subframes: [] }
       if (this.frameStack.length == 0) {
-        // this should not happen, as there is always bottomFrame, but let's handle it
+        // this should not happen, as there is always bottomFrame,
+        // but we do not throw here, as trace collection is not the primary
+        // function of the simulator.
         this.frameStack = [newFrame]
       } else if (this.frameStack.length === 2 && this.frameStack[1].app.opcode === '_') {
         // A placeholder frame created from `q::input` or `then`. Modify in place.