| Hello, I am assuming that you took the Bakery specification from the Github examples [1]? However, the proof for the step that doesn't pass for you is in fact <3>2. CASE /\ flag' = [flag EXCEPT ![self] = FALSE] /\ unchecked' = [unchecked EXCEPT ![self] = Procs \ {self}] /\ pc' = [pc EXCEPT ![self] = "w1"] BY <3>2, Z3T(30) DEF Inv Note the directive "Z3T(30)", which invokes the Z3 (SMT) back-end prover with a timeout of 30 seconds, indicating that the step may take longer than the default timeout of 5 seconds. This passes on my machine. If you have a really slow system, you may need to increase the timeout further. In general, when a proof fails, it is a good idea to decompose it into smaller steps, such as proving each conjunct of the invariant separately, to understand which step causes problems. Also note that there is a somewhat different version of the Bakery spec in the distribution of TLAPS, usually located in /usr/local/lib/tlaps/examples/Bakery.tla that should work out of the box. Stephan [1] https://github.com/tlaplus/Examples/blob/master/specifications/Bakery-Boulangerie/Bakery.tla
--
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 on the web visit https://groups.google.com/d/msgid/tlaplus/907A4E07-EBAC-4DC7-A202-666662A89087%40gmail.com. |