discard-disable=false seems buggy

[nano-o]

Hello,
I'm using the latest docker image and getting strange results with --discard-disabled=false.
Consider the following spec:

-------------------------------- MODULE Test --------------------------------
Init == TRUE
Next == TRUE
Inv == FALSE
=============================================================================

The command $APALACHE_HOME/script/run-docker.sh check --inv=Inv --discard-disabled=false Test.tla reports no errors.
Am I misunderstanding something or is this a bug?

[konnov]

Looks like a bug

[thpani]

Hi @nano-o, thanks for filing this!
Could you tell us if this is currently blocking your work?
We will have limited cycles to investigate during next week, but we'll get to it ASAP!

[thpani]

With --discard-disabled=false, checkInvariantsForPreparedTransition is not called at step 0 (isNext == false):
https://github.com/informalsystems/apalache/blob/44bd91c60e207f44a8ee4804bb9bdcd9639ab70f/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/SeqModelChecker.scala#L280-L282

Also, mayChangeAssertion is true at step 0 but false on steps >= 1.

--discard-disabled=true is unaffected because it goes into a different code path here:
https://github.com/informalsystems/apalache/blob/44bd91c60e207f44a8ee4804bb9bdcd9639ab70f/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/SeqModelChecker.scala#L226

[thpani]

@nano-o Should be fixed and included in the next release. Thanks again for filing this!