Remove pluscal checksums

ahelwer · ahelwer · commit e2a100401fbf · 2024-04-14T10:47:44.000-07:00
Signed-off-by: Andrew Helwer &lt;2n8rn1w1f@mozmail.com&gt;
diff --git a/specifications/DiningPhilosophers/DiningPhilosophers.tla b/specifications/DiningPhilosophers/DiningPhilosophers.tla
@@ -113,7 +113,7 @@ Think:
 end process;
 
 end algorithm; *)
-\* BEGIN TRANSLATION (chksum(pcal) = "ea877089" /\ chksum(tla) = "16352822")
+\* BEGIN TRANSLATION
 VARIABLES forks, pc
 
 (* define statement *)
diff --git a/specifications/KeyValueStore/KVsnap.tla b/specifications/KeyValueStore/KVsnap.tla
@@ -79,7 +79,7 @@ COMMIT: \* Commit the transaction to the database if there is no conflict
 }
 *)
 
-\* BEGIN TRANSLATION (chksum(pcal) = "1adfcb46" /\ chksum(tla) = "5b28617f")
+\* BEGIN TRANSLATION
 VARIABLES store, tx, missed, pc, snapshotStore, read_keys, write_keys, ops
 
 vars == << store, tx, missed, pc, snapshotStore, read_keys, write_keys, ops
diff --git a/specifications/LearnProofs/AddTwo.tla b/specifications/LearnProofs/AddTwo.tla
@@ -17,7 +17,7 @@ EXTENDS Naturals, TLAPS
   }
 }
 ****************************************************************************)
-\* BEGIN TRANSLATION (chksum(pcal) = "b4b07666" /\ chksum(tla) = "8adfa002")
+\* BEGIN TRANSLATION
 VARIABLE x
 
 vars == << x >>
diff --git a/specifications/LearnProofs/FindHighest.tla b/specifications/LearnProofs/FindHighest.tla
@@ -23,7 +23,7 @@ lb: while (i <= Len(f)) {
   }
 }
 ****************************************************************************)
-\* BEGIN TRANSLATION (chksum(pcal) = "31f24270" /\ chksum(tla) = "819802c6")
+\* BEGIN TRANSLATION
 VARIABLES f, h, i, pc
 
 (* define statement *)
diff --git a/specifications/LeastCircularSubstring/LeastCircularSubstring.tla b/specifications/LeastCircularSubstring/LeastCircularSubstring.tla
@@ -46,7 +46,7 @@ LVR:  j := j + 1;
 end algorithm;
 
 ****************************************************************************)
-\* BEGIN TRANSLATION (chksum(pcal) = "c2e05615" /\ chksum(tla) = "81694c33")
+\* BEGIN TRANSLATION
 VARIABLES b, n, f, i, j, k, pc
 
 (* define statement *)
diff --git a/specifications/MultiPaxos-SMR/MultiPaxos.tla b/specifications/MultiPaxos-SMR/MultiPaxos.tla
@@ -424,7 +424,7 @@ end algorithm; *)
 
 ----------
 
-\* BEGIN TRANSLATION (chksum(pcal) = "2be53042" /\ chksum(tla) = "bfbfd945")
+\* BEGIN TRANSLATION
 VARIABLES msgs, node, pending, observed, pc
 
 (* define statement *)
diff --git a/specifications/chang_roberts/ChangRoberts.tla b/specifications/chang_roberts/ChangRoberts.tla
@@ -62,7 +62,7 @@ succ(n) == IF n=N THEN 1 ELSE n+1  \* successor along the ring
    } \* end process
 }  \* end algorithm
 **)
-\* BEGIN TRANSLATION (chksum(pcal) = "65c8d352" /\ chksum(tla) = "33951c89")
+\* BEGIN TRANSLATION
 VARIABLES msgs, pc, initiator, state
 
 vars == << msgs, pc, initiator, state >>
diff --git a/specifications/ewd687a/EWD687aPlusCal.tla b/specifications/ewd687a/EWD687aPlusCal.tla
@@ -88,7 +88,7 @@ l:  while (TRUE) {
   }
 }
 *)
-\* BEGIN TRANSLATION (chksum(pcal) = "d18d3150" /\ chksum(tla) = "7d13cf45")
+\* BEGIN TRANSLATION
 VARIABLES terminationDetected, network
 
 (* define statement *)
diff --git a/specifications/ewd998/EWD998PCal.tla b/specifications/ewd998/EWD998PCal.tla
@@ -81,7 +81,7 @@ l:  while (TRUE) {
   }
 }
 ********)
-\* BEGIN TRANSLATION (chksum(pcal) = "4d658e04" /\ chksum(tla) = "530581e3")
+\* BEGIN TRANSLATION
 VARIABLE network
 
 (* define statement *)

Original file line number	Diff line number	Diff line change
`@@ -79,7 +79,7 @@ COMMIT: \* Commit the transaction to the database if there is no conflict`
`79`	`79`	`}`
`80`	`80`	`*)`
`81`	`81`
`82`		`-\* BEGIN TRANSLATION (chksum(pcal) = "1adfcb46" /\ chksum(tla) = "5b28617f")`
	`82`	`+\* BEGIN TRANSLATION`
`83`	`83`	`VARIABLES store, tx, missed, pc, snapshotStore, read_keys, write_keys, ops`
`84`	`84`
`85`	`85`	`vars == << store, tx, missed, pc, snapshotStore, read_keys, write_keys, ops`
Original file line number	Diff line number	Diff line change
`@@ -17,7 +17,7 @@ EXTENDS Naturals, TLAPS`
`17`	`17`	`}`
`18`	`18`	`}`
`19`	`19`	`****************************************************************************)`
`20`		`-\* BEGIN TRANSLATION (chksum(pcal) = "b4b07666" /\ chksum(tla) = "8adfa002")`
	`20`	`+\* BEGIN TRANSLATION`
`21`	`21`	`VARIABLE x`
`22`	`22`
`23`	`23`	`vars == << x >>`
Original file line number	Diff line number	Diff line change
`@@ -23,7 +23,7 @@ lb: while (i <= Len(f)) {`
`23`	`23`	`}`
`24`	`24`	`}`
`25`	`25`	`****************************************************************************)`
`26`		`-\* BEGIN TRANSLATION (chksum(pcal) = "31f24270" /\ chksum(tla) = "819802c6")`
	`26`	`+\* BEGIN TRANSLATION`
`27`	`27`	`VARIABLES f, h, i, pc`
`28`	`28`
`29`	`29`	`(* define statement *)`
Original file line number	Diff line number	Diff line change
`@@ -88,7 +88,7 @@ l: while (TRUE) {`
`88`	`88`	`}`
`89`	`89`	`}`
`90`	`90`	`*)`
`91`		`-\* BEGIN TRANSLATION (chksum(pcal) = "d18d3150" /\ chksum(tla) = "7d13cf45")`
	`91`	`+\* BEGIN TRANSLATION`
`92`	`92`	`VARIABLES terminationDetected, network`
`93`	`93`
`94`	`94`	`(* define statement *)`
Original file line number	Diff line number	Diff line change
`@@ -81,7 +81,7 @@ l: while (TRUE) {`
`81`	`81`	`}`
`82`	`82`	`}`
`83`	`83`	`********)`
`84`		`-\* BEGIN TRANSLATION (chksum(pcal) = "4d658e04" /\ chksum(tla) = "530581e3")`
	`84`	`+\* BEGIN TRANSLATION`
`85`	`85`	`VARIABLE network`
`86`	`86`
`87`	`87`	`(* define statement *)`