Why Apalachee reports InvariantViolation for the BakeryTyped spec from its source repo?

[Anthony Lee]

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

[Igor Konnov]

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

> --
> 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+u...@googlegroups.com.
> To view this discussion visit https://groups.google.com/d/msgid/tlaplus/37ddfd7e-c7a9-4c05-8a73-3d56f08e0ee2n%40googlegroups.com.

[Anthony Lee]

Thanks Igor;

I'm interested in these temporal properties that must be treated differently in Symbolic Model Checking than explicit state graph search.

I'll probably post some questions in Apalache forum later.