Proof of Module Bakery Fails

[fisherman]

Hello,

    I am learning TLAPS, I run "Prove Step or Modules" for "THEOREM Spec => []MutualExclusion" in Bakery.tla, and failed.

  The failed step is <2>5, detailed as below. Can anyone help me on it?

  Thanks a lot.

 

[Stephan Merz]

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

<image.png>

--
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 on the web visit https://groups.google.com/d/msgid/tlaplus/CACRPdDRc_v4-vNJ0CE2ikXcoiyec0Kn8gpwWTz0p1dMsq1qLyA%40mail.gmail.com.

[fisherman]

Hi Stephan,

  Thank you for your kind reply. 

  The spec is from Github examples, and it works after adding Z3T(30).

Best regards

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/907A4E07-EBAC-4DC7-A202-666662A89087%40gmail.com.