This project is read-only.
1

Closed

Model error message inconsistent with actual invariant used

description

The image shows my invariant and the error message I get. The result of the error-trace is as expected, but the error message on the top-right is incorrect.

Context: Previously I had the invariant b = 3, which I changed to b # 4 later.

file attachments

Closed Oct 7, 2016 at 5:13 PM by mku

comments

mku wrote May 25, 2015 at 7:54 AM

Hi,

did you run the model checker (TLC) after you changed b=3 to b#4?

Thanks
Markus