Fix invalid utf8 in SimpleRegular.tla and invalid syntax in Specifying Systems modules

specifications/SpecifyingSystems/Standard/Naturals.tla

@@ -3,11 +3,11 @@ LOCAL R == INSTANCE ProtoReals
 
 Nat == R!Nat
 
-a + b == a R!+ b
-a - b == a R!- b
-a * b == a R!* b
-a ^ b == a R!^ b
-a \leq b == a R!\leq b
+a + b == R!+(a, b)
+a - b == R!-(a, b)
+a * b == R!*(a, b)
+a ^ b == R!^(a, b)
+a \leq b == R!\leq(a, b)
 a \geq b == b \leq a
 a < b == (a \leq b) /\ (a # b)
 a > b == b < a

specifications/SpecifyingSystems/Standard/Reals.tla

@@ -3,6 +3,6 @@ EXTENDS Integers
 LOCAL R == INSTANCE ProtoReals
 
 Real  ==  R!Real
-a / b == a R!/ b
+a / b == R!/(a, b)
 Infinity == R!Infinity
-=============================================================================
+=============================================================================

specifications/TeachingConcurrency/SimpleRegular.tla

@@ -48,7 +48,7 @@
 (* The problem of generalizing the algorithm of module Simple to use       *)
 (* regular registers was proposed by Yuri Abraham in                       *)
 (*                                                                         *)
-(*    On Lamport�s �Teaching Concurrency�                                  *)
+(*    On Lamport's "Teaching Concurrency"                                  *)
 (*    Bulletin of EATS (European Association for Theoretical Computer      *)
 (*      Science) No. 127, February 2019                                    *)
 (*    http://bulletin.eatcs.org/index.php/beatcs/article/view/569          *)
@@ -142,31 +142,31 @@ THEOREM Spec => []PCorrect
 <1>1. Init => Inv
   BY DEF Init, Inv, TypeOK, ProcSet 
 <1>2. Inv /\ [Next]_vars => Inv'
-  <2> SUFFICES ASSUME Inv,
-                      [Next]_vars
-               PROVE  Inv'
-    OBVIOUS
-  <2>1. ASSUME NEW self \in 0..N-1,
-               a1(self)
-        PROVE  Inv'
+  <2> SUFFICES ASSUME Inv,
+                      [Next]_vars
+               PROVE  Inv'
+    OBVIOUS
+  <2>1. ASSUME NEW self \in 0..N-1,
+               a1(self)
+        PROVE  Inv'
     BY <2>1 DEF a1, Inv, TypeOK
-  <2>2. ASSUME NEW self \in 0..N-1,
-               a2(self)
-        PROVE  Inv'
+  <2>2. ASSUME NEW self \in 0..N-1,
+               a2(self)
+        PROVE  Inv'
     BY <2>2 DEF a2, Inv, TypeOK
-  <2>3. ASSUME NEW self \in 0..N-1,
-               b(self)
-        PROVE  Inv'
-    <3> SUFFICES ASSUME NEW v \in x[(self-1) % N],
-                        y' = [y EXCEPT ![self] = v]
-                 PROVE  Inv'
-      BY <2>3 DEF b
-    <3> QED
-        BY <2>3, Z3 DEF b, Inv, TypeOK  
-  <2>4. CASE UNCHANGED vars
+  <2>3. ASSUME NEW self \in 0..N-1,
+               b(self)
+        PROVE  Inv'
+    <3> SUFFICES ASSUME NEW v \in x[(self-1) % N],
+                        y' = [y EXCEPT ![self] = v]
+                 PROVE  Inv'
+      BY <2>3 DEF b
+    <3> QED
+        BY <2>3, Z3 DEF b, Inv, TypeOK  
+  <2>4. CASE UNCHANGED vars
     BY <2>4 DEF TypeOK, Inv, vars
-  <2>5. QED
-    BY <2>1, <2>2, <2>3, <2>4 DEF Next, proc
+  <2>5. QED
+    BY <2>1, <2>2, <2>3, <2>4 DEF Next, proc
 <1>3. Inv => PCorrect
   BY DEF Inv, TypeOK, PCorrect
 <1>4. QED

specifications/diskpaxos/Synod.tla

@@ -16,9 +16,9 @@ VARIABLES input, output
 VARIABLES allInput, chosen
 
 IInit == /\ input \in [Proc -> Inputs]
-        /\ output = [p \in Proc |-> NotAnInput]
-        /\ chosen = NotAnInput
-        /\ allInput = {input[p] : p \in Proc}
+         /\ output = [p \in Proc |-> NotAnInput]
+         /\ chosen = NotAnInput
+         /\ allInput = {input[p] : p \in Proc}
 
 IChoose(p) ==
   /\ output[p] = NotAnInput