Applied Specifying Systems errata fix to exercises (#102)

Changed all instances of "req" to "busy" Signed-off-by: Andrew Helwer <[email protected]>
tlaplus · Jan 14, 2024 · 9194122 · 9194122
1 parent c7e0ca3
commit 9194122
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 3 deletions.
diff --git a/specifications/SpecifyingSystems/Liveness/LiveInternalMemory.tla b/specifications/SpecifyingSystems/Liveness/LiveInternalMemory.tla
@@ -27,12 +27,12 @@ LISpec == ISpec /\ Liveness2
 
 (***************************************************************************)
 (* The following property asserts that, whenever any processor p has       *)
-(* issued a request, so ctl[p] = "req", then a response eventually occurs, *)
+(* issued a request, so ctl[p] = "busy", then a response eventually occurs,*)
 (* setting ctl[p] to "rdy".                                                *)
 (***************************************************************************)
 
 LivenessProperty == 
-   \A p \in Proc : (ctl[p] = "req") ~> (ctl[p] = "rdy")
+   \A p \in Proc : (ctl[p] = "busy") ~> (ctl[p] = "rdy")
 
 -----------------------------------------------------------------------------
 (***************************************************************************)

diff --git a/specifications/SpecifyingSystems/Liveness/README b/specifications/SpecifyingSystems/Liveness/README
@@ -36,7 +36,7 @@ Exercises:
    that the specification LISpec of LiveInternalMemory does not satisfy the 
    following property
 
-       \A p \in Proc : (ctl[p] = "rdy") ~> (ctl[p] = "req") 
+       \A p \in Proc : (ctl[p] = "rdy") ~> (ctl[p] = "busy")
 
 2. Determine which of the following formulas are temporal
    tautologies.  For each one that isn't, give a counterexample.