Merge pull request #1190 from informalsystems/gabriela/fix-repl-insta…

…nce-vars

Workaround for state vars from instances in incremental compilation (REPL)

CHANGELOG.md

@@ -17,6 +17,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 ### Removed
 ### Fixed
 
+- Fixed a problem where state variables from instances didn't work properly in the REPL (#1190)
 - Fixed a problem where referencing constants from an instance could cause a crash (#1191)
 
 ### Security

quint/io-cli-tests.md

@@ -948,3 +948,26 @@ exit $exit_code
 
 error: run failed
 ```
+
+### Repl keeps right track of variables from instances
+
+Incremental evaluation from the REPL interacting with instance flattening leads to state variables having different IDs on separate evaluations. This test ensures this case is well handled during evaluation.
+
+<!-- !test in repl with instance vars -->
+
+```
+cd ../examples/cosmos/tendermint/
+output=$(echo -e "n4_f1::Init\nn4_f1::round" | quint -r TendermintModels.qnt::TendermintModels 2>&1 | tail -n +3)
+exit_code=$?
+cd - > /dev/null
+echo "$output"
+exit $exit_code
+```
+
+<!-- !test out repl with instance vars -->
+
+```
+>>> true
+>>> Map("p1" -> 0, "p2" -> 0, "p3" -> 0)
+>>> 
+```

quint/src/runtime/impl/compilerImpl.ts

@@ -342,13 +342,24 @@ export class CompilerVisitor implements IRVisitor {
   }
 
   exitVar(vardef: ir.QuintVar) {
+    const varName = vardef.name
+
     // In the process of incremental compilation, we might revisit the same var
-    // definition. Don't overwrite the register if that happens.
-    if (this.context.has(kindName('var', vardef.id))) {
+    // definition. Don't overwrite the register if that happens. In some cases
+    // (with instances), the variable can have a different ID, but the same
+    // name. In that case, we assign the register with that name for the new ID.
+    if (this.context.has(kindName('var', varName))) {
+      const register = this.context.get(kindName('var', varName))!
+      this.context.set(kindName('var', vardef.id), register)
+
+      if (this.context.has(kindName('nextvar', varName))) {
+        const register = this.context.get(kindName('nextvar', varName))!
+        this.context.set(kindName('nextvar', vardef.id), register)
+      }
+
       return
     }
 
-    const varName = vardef.name
     // simply introduce two registers:
     //  one for the variable, and
     //  one for its next-state version