Re: [tlaplus] Proof of Module Bakery Fails

On Fri, Dec 25, 2020 at 4:54 PM Stephan Merz <stephan.merz@xxxxxxxxx> wrote:

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

On 24 Dec 2020, at 16:32, fisherman <fisherman.dong@xxxxxxxxx> wrote:

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.

<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+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/CACRPdDRc_v4-vNJ0CE2ikXcoiyec0Kn8gpwWTz0p1dMsq1qLyA%40mail.gmail.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 on the web visit https://groups.google.com/d/msgid/tlaplus/907A4E07-EBAC-4DC7-A202-666662A89087%40gmail.com.