Conforming specs containing PlusCal code to the recommendation for co…

…mment blocks so that folding regions can be made.
Remit · Aug 27, 2019 · 152615e · 152615e
1 parent 1201b7c
commit 152615e
Show file tree

Hide file tree

Showing 6 changed files with 458 additions and 452 deletions.
diff --git a/specifications/Bakery-Boulangerie/Bakery.tla b/specifications/Bakery-Boulangerie/Bakery.tla
diff --git a/specifications/Bakery-Boulangerie/Boulanger.tla b/specifications/Bakery-Boulangerie/Boulanger.tla
@@ -164,7 +164,8 @@ a \prec b == \/ a[1] < b[1]
     }
 }
 
-***     this ends the comment containg the pluscal code      **********)
+    this ends the comment containing the PlusCal code
+*************)
 
 \* BEGIN TRANSLATION  (this begins the translation of the PlusCal code)
 VARIABLES num, flag, pc, unchecked, max, nxt, previous
@@ -530,6 +531,7 @@ DeadlockFree == (\E i \in Procs : Trying(i)) ~> (\E i \in Procs : InCS(i))
 StarvationFree == \A i \in Procs : Trying(i) ~> InCS(i)
 =============================================================================
 \* Modification History
+\* Last modified Tue Aug 27 12:22:38 PDT 2019 by loki
 \* Last modified Thu May 24 20:03:58 CEST 2018 by merz
 \* Last modified Thu May 24 13:49:22 CEST 2018 by merz
 \* Last modified Tue Jul 21 17:55:23 PDT 2015 by lamport

diff --git a/specifications/LoopInvariance/BinarySearch.tla b/specifications/LoopInvariance/BinarySearch.tla
@@ -35,7 +35,7 @@ SortedSeqs == {ss \in Seq(Values) :
             if (mval = val) { result := mid}
             else if (val < mval) { high := mid - 1}
             else {low := mid + 1}                    } } } }
- ***************************************************************************)
+***************************************************************************)
 \* BEGIN TRANSLATION
 VARIABLES seq, val, low, high, result, pc
 
@@ -249,6 +249,7 @@ THEOREM Spec => []resultCorrect
 <1>4. QED
   BY <1>1, <1>2, <1>3, PTL DEF Spec
 =============================================================================
-\* Modification History
+\* Modification History
+\* Last modified Tue Aug 27 12:59:52 PDT 2019 by loki
 \* Last modified Fri May 03 16:28:58 PDT 2019 by lamport
 \* Created Wed Apr 17 15:15:12 PDT 2019 by lamport
diff --git a/specifications/LoopInvariance/SumSequence.tla b/specifications/LoopInvariance/SumSequence.tla
@@ -53,7 +53,7 @@ with the variable sum equal to the sum of the elements of seq.
              n := n+1 ;           }
     }
 }
- ***************************************************************************)
+***************************************************************************)
 \* BEGIN TRANSLATION
 VARIABLES seq, sum, n, pc
 
@@ -542,6 +542,7 @@ LEMMA Lemma5_Proof ==
 <1>4. QED
   BY <1>3
 =============================================================================
-\* Modification History
+\* Modification History
+\* Last modified Tue Aug 27 12:59:10 PDT 2019 by loki
 \* Last modified Fri May 03 16:40:42 PDT 2019 by lamport
 \* Created Fri Apr 19 14:13:06 PDT 2019 by lamport
diff --git a/specifications/MisraReachability/ParReach.tla b/specifications/MisraReachability/ParReach.tla
@@ -88,9 +88,9 @@ simpler.
 }
 
 
-Here is the TLA+ translation of the PlusCal code.
- ***************************************************************************)
-\* BEGIN TRANSLATION
+
+***************************************************************************)
+\* BEGIN TRANSLATION   Here is the TLA+ translation of the PlusCal code.
 VARIABLES marked, vroot, pc, u, toVroot
 
 vars == << marked, vroot, pc, u, toVroot >>
@@ -230,6 +230,8 @@ THEOREM Spec => R!Spec
 THEOREM Spec => R!Init /\ [][R!Next]_R!vars
 THEOREM Spec => WF_R!vars(R!Next)
 =============================================================================
-\* Modification History
+\* Modification History
+\* Last modified Tue Aug 27 14:58:47 PDT 2019 by loki
+\* Last modified Fri Jun 28 16:26:24 PDT 2019 by loki
 \* Last modified Sun Apr 14 16:53:23 PDT 2019 by lamport
 \* Created Mon Apr 08 10:48:52 PDT 2019 by lamport
diff --git a/specifications/MisraReachability/Reachable.tla b/specifications/MisraReachability/Reachable.tla
@@ -76,10 +76,9 @@ node and does the following:
 }
 
 
-Here is the TLA+ translation of the PlusCal code.
 ***************************************************************************)
 
-\* BEGIN TRANSLATION  
+\* BEGIN TRANSLATION    Here is the TLA+ translation of the PlusCal code.
 VARIABLES marked, vroot, pc
 
 \*Reachable == ReachableFrom(marked)  (* added for a test *)
@@ -234,7 +233,8 @@ THEOREM  ASSUME IsFiniteSet(Reachable)
  (* dozen nodes.                                                           *)
  (**************************************************************************)
 =============================================================================
-\* Modification History
+\* Modification History
+\* Last modified Tue Aug 27 14:46:36 PDT 2019 by loki
 \* Last modified Wed Apr 17 12:21:22 PDT 2019 by lamport
 \* Created Thu Apr 04 10:11:51 PDT 2019 by lamport