[BUG] Invariant referring only to unchanged variables is not checked

apalache-mc / apalache

APALACHE: symbolic model checker for TLA+ and Quint

https://apalache-mc.org/

Apache License 2.0

440 stars 40 forks source link

Closed andrey-kuprianov closed 4 years ago

andrey-kuprianov commented 4 years ago

When checking the following spec

----- MODULE bug -----
VARIABLE a
Init == a = 1
Next == a' = a
Inv == FALSE
===============

e.g. with these parameters

apalache-mc --debug check --length=2 --inv=Inv bug.tla

no error is reported, and the following message can be seen in detailed.log:

The invariant is referring only to the UNCHANGED variables. Skipped.

konnov commented 4 years ago

This is a bug in an optimization. Will fix it asap.