diff --git a/CHANGELOG.md b/CHANGELOG.md index 5b8e0326d..8a1898443 100644 --- a/CHANGELOG.md +++ b/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 diff --git a/quint/io-cli-tests.md b/quint/io-cli-tests.md index ce0428be5..63adb94fc 100644 --- a/quint/io-cli-tests.md +++ b/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. + + + +``` +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 +``` + + + +``` +>>> true +>>> Map("p1" -> 0, "p2" -> 0, "p3" -> 0) +>>> +``` diff --git a/quint/src/runtime/impl/compilerImpl.ts b/quint/src/runtime/impl/compilerImpl.ts index dbf5dac6e..632a2ee7a 100644 --- a/quint/src/runtime/impl/compilerImpl.ts +++ b/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