ctl[p] is never equal "req" in specifications/SpecifyingSystems/Liveness properties

[senniraf]

There are typos in the liveness properties in the folder to the chapter "Liveness" of "Specifying Systems". The ctl[p] function value in the properties should equal "req". However, this is never the case as the function range is only {"rdy", "busy", "done"}.
This occurs at least in the following lines:

Examples/specifications/SpecifyingSystems/Liveness/README

Line 39 in c7e0ca3

\A p \in Proc : (ctl[p] = "rdy") ~> (ctl[p] = "req")

Examples/specifications/SpecifyingSystems/Liveness/LiveInternalMemory.tla

Line 30 in c7e0ca3

(* issued a request, so ctl[p] = "req", then a response eventually occurs, *)

Examples/specifications/SpecifyingSystems/Liveness/LiveInternalMemory.tla

Line 35 in c7e0ca3

\A p \in Proc : (ctl[p] = "req") ~> (ctl[p] = "rdy")

IMHO "req" was meant to be "busy".

[ahelwer]

This seems strange in several ways! According to the Liveness/README the check of MCLiveInternalMemory.tla should fail. But according to manifest.json that run of TLC succeeds. But how can it succeed if ctl[p] can never equal "rdy"? Are we dealing with liveness checking finding a vacuous truth?

[muenchnerkindl]

According to what is said above and to TypeOK in InternalMemory, ctl \in [Proc -> {"rdy", "busy","done"}], so the property \A p \in Proc : (ctl[p] = "req") ~> (ctl[p] = "rdy") is indeed vacuously true. Without having looked at the spec in detail, it appears reasonable that "req" should be replaced by "busy", which is the value the action Req(p) sets ctl to. In that case the property has a chance to be wrong, in a potentially interesting way.

[senniraf]

Keep in mind that the property given in the README exercise is \A p \in Proc : (ctl[p] = "rdy") ~> (ctl[p] = "req") which is different from the property in the LiveInternalMemory specification: \A p \in Proc : (ctl[p] = "req") ~> (ctl[p] = "rdy") (The sides of the implication/"leads to" operator are swapped).
The property in the README exercise should not be implied by the specification:

1. Run TLC to check the LiveHourClock and LiveInternalMemory specifications,
   using the files above.  Use TLC to find a counterexample to show
   that the specification LISpec of LiveInternalMemory does not satisfy the 
   following property

       \A p \in Proc : (ctl[p] = "rdy") ~> (ctl[p] = "req") 

[ahelwer]

Per the Specifying Systems errata [pdf] the "rdy" -> "busy" error was reported for the textbook back in 2010 by Casey Klein. We can make the same substitution everywhere - in README, the comment of LiveInternalMemory.tla, and the definition of LivenessProperty in LiveInternalMemory.tla. Unfortunately this liveness property is not invalidated; the spec satisfies it regardless of whether the assumptions Liveness or Liveness2 in LiveInternalMemory.tla are used (which makes sense because the textbook has a proof that these assumptions are equivalent). Reading the InternalMemory.tla spec I'm not sure what similar property would be false, or even how it could be. The only thing I can see that could possibly make it invalidated is if the Reply macro in Rsp evaluates to FALSE.

So I'm not sure what to do really. I'm inclined to just make the substitution, same as the errata, but change the exercise text to say that LiveInternalMemory does satisfy the property.

[ahelwer]

Actually, an idea: perhaps the exercise formula in README is supposed to be different than the formula in LiveInternalMemory.tla. It should probably be \A p \in Proc : (ctl[p] = "rdy") ~> (ctl[p] = "busy"), using the same substitution as above, which will certainly fail because there is no fairness assumption on Req. Yes, I think that is the correct change.

[muenchnerkindl]

Sounds good to me. Of course we could add the exercise to check formula LivenessProperty from module LiveInternalMemory, but this is probably implicit, just like checking TypeInvariant in InternalMemory.