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

[Anthony Lee <anthonynlee@xxxxxxxxx>]

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.

Attachment: violation.tla
Description: Binary data