Open
Description
Given
module M {
var v: int
action duplicate_update = all {
v' = 1,
v' = 0,
}
}
The effect checker correctly raises an error due to the duplicate updates of v
:
$ quint typecheck f.qnt
/quint/f.qnt:3:4 - error: [QNT202] Multiple updates of variable v
3: var v: int
^^^^^^^^^^
error: typechecking failed
However this error only points the location where the variable is declared, which is not where the error is arising, and it doesn't help identifying where the duplicate updates arise. This can be very tricky in larger specs with layers of action abstractions.
Instead, the error should give a list of all conflicting update locations.
This issue is thanks to a report from @crodriguezvega. Thanks, Carlos!