Re: [tlaplus] Why Apalachee reports InvariantViolation for the BakeryTyped spec from its source repo?

[Igor Konnov <igor.konnov@xxxxxxxxx>]

Hi Anthony,

Apalache's support for liveness is still experimental. There were not
many people who actually tried to check temporal properties with
Apalache. The current implementation uses the standard
liveness-to-safety transformation. We have addressed a few challenges
specific to TLA+. However, the support for ENABLED, SF, and WF is
still not there.

There are several things here:

 1. By default, Apalache uses Init and Next, where liveness requires
Spec, which contains the necessary fairness constraints. Basically,
this is what the counterexample is about. Most likely, the property is
breaking due to stuttering.

 2. It's possible to tell Apalache to use Spec by defining a TLC
config like this:

     $ cat bakery.cfg
     SPECIFICATION MySpec
     PROPERTY DeadlockFree

     Then you have to run Apalache like this:

     $ apalache-mc check --cinit=ConstInit4 --config=bakery.cfg BakeryTyped.tla

     This will not work, too, as the fairness properties are decorated
with the quantifier: \A self \in Procs : WF_vars((pc[self] # "ncs") /\
p(self))

 3. WF and SF are internally using ENABLED, which happened to be hard
to deal with in the general case. We had an experimental
implementation for ENABLED, but I think it is still in the unmerged
state. The best we can do now is to manually encode WF and SF using a
hand-written replacement of ENABLED.

These are the reasons. If you would like to debug this example
further, we could do it in an issue in the Apalache repo [1].

[1] https://github.com/apalache-mc/apalache


Cheers,
Igor

On Mon, Dec 2, 2024 at 8:51 AM Anthony Lee <anthonynlee@xxxxxxxxx> wrote:
>
> I didn't change the spec.
> I ran this command to do model checking on temporal property and invariant:
> apalache-mc check  --temporal=DeadlockFree --cinit=ConstInit4 --inv=Inv --length=50 ~/git/apalache/test/tla/bakery-pluscal/BakeryTyped.tla
>
> Got error:
> State 4: state invariant 1 violated.
> Found 1 error(s)
> The outcome is: Error
> Checker has found an error
> It took me 0 days  0 hours  0 min 46 sec
> Total time: 46.900 sec
> EXITCODE: ERROR (12)
>
> It looks like DeadlockFree is violated.
> Is there anything wrong in my command?
> Could anyone help to check the attached violation.tla to explain what the cause is or point me to some document that could help to read the error?
>
>
> Thanks.
> Anthony
>
> --
> You received this message because you are subscribed to the Google Groups "tlaplus" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
> To view this discussion visit https://groups.google.com/d/msgid/tlaplus/37ddfd7e-c7a9-4c05-8a73-3d56f08e0ee2n%40googlegroups.com.

-- 
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/CACooHMBDj4O%3D5f3%2BMLhLeoYsx%3DBvyWDQQNzE7bHj5haDyFA9mg%40mail.gmail.com.