Fix typos (#94)

Signed-off-by: Sergey Bronnikov <[email protected]>

specifications/CarTalkPuzzle/CarTalkPuzzle.toolbox/CarTalkPuzzle.tex

@@ -240,7 +240,7 @@
    }[0pt][0pt]{\rule[.5ex]{\boxrulewd}{\boxlineht}}\hspace{-\boxsep}}
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-% FORMATING COMMANDS                                                        %
+% FORMATTING COMMANDS                                                        %
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

specifications/DieHard/DieHard.tla

@@ -1,11 +1,11 @@
 ------------------------------ MODULE DieHard ------------------------------- 
 (***************************************************************************)
-(* In the movie Die Hard 3, the heros must obtain exactly 4 gallons of     *)
+(* In the movie Die Hard 3, the heroes must obtain exactly 4 gallons of     *)
 (* water using a 5 gallon jug, a 3 gallon jug, and a water faucet.  Our    *)
 (* goal: to get TLC to solve the problem for us.                           *)
 (*                                                                         *)
 (* First, we write a spec that describes all allowable behaviors of our    *)
-(* heros.                                                                  *)
+(* heroes.                                                                  *)
 (***************************************************************************)
 EXTENDS Naturals
   (*************************************************************************)
@@ -76,7 +76,7 @@ EmptyBigJug   == /\ big' = 0
 
 (***************************************************************************)
 (* We now consider pouring water from one jug into another.  Again, since  *)
-(* the jugs are not callibrated, when pouring from jug A to jug B, it      *)
+(* the jugs are not calibrated, when pouring from jug A to jug B, it      *)
 (* makes sense only to either fill B or empty A. And there's no point in   *)
 (* emptying A if this will cause B to overflow, since that could be        *)
 (* accomplished by the two actions of first filling B and then emptying A. *)
@@ -119,7 +119,7 @@ Spec == Init /\ [][Next]_<<big, small>>
 -----------------------------------------------------------------------------
 
 (***************************************************************************)
-(* Remember that our heros must measure out 4 gallons of water.            *)
+(* Remember that our heroes must measure out 4 gallons of water.            *)
 (* Obviously, those 4 gallons must be in the 5 gallon jug.  So, they have  *)
 (* solved their problem when they reach a state with big = 4.  So, we      *)
 (* define NotSolved to be the predicate asserting that big # 4.            *)

specifications/DieHard/DieHarder.tla

@@ -11,7 +11,7 @@ EXTENDS Naturals
 
 CONSTANT Jug,      \* The set of all jugs.
          Capacity, \* A function, where Capacity[j] is the capacity of jug j.
-         Goal      \* The quantity of water our heros must measure.
+         Goal      \* The quantity of water our heroes must measure.
 (***************************************************************************)
 (* We make an assumption about these constants--namely, that Capacity is a *)
 (* function from jugs to positive integers, and Goal is a natural number.  *)

specifications/KeyValueStore/ClientCentric.tla

@@ -31,7 +31,7 @@ ExecutionElem == [parentState: State, transaction: Transaction]
 \* resultState is the parentState of the next transaction, but not used in the isolation definitions.
 \* ExecutionElem == [parentState: State, transaction: Transaction, resultState: State]
 \* We represent an `Execution` as a sequence of `Transaction`s with their corresponding parent state.
-\* Note: This execution does therefor not contain the "final state" of the execution, since it is not a parent state of a transaction.
+\* Note: This execution does therefore not contain the "final state" of the execution, since it is not a parent state of a transaction.
 Execution == Seq(ExecutionElem)
 
 \* Seq
@@ -107,12 +107,12 @@ effects(state, transaction) ==
 executions(initialState, transactions) == 
   \* All possible permutations
   LET orderings == PermSeqs(transactions)
-\*      initialState == [k \in Keys |-> InitValue] \* makes it level-1 therefor pass it in
+\*      initialState == [k \in Keys |-> InitValue] \* makes it level-1 therefore pass it in
       accummulator == [ execution |-> <<>>, nextState |-> initialState ]
   IN { LET executionAcc == ReduceSeq(
          \*                                store ExecutionElem in accumulator
                             LAMBDA t, acc: [ execution |-> Append(acc.execution, [parentState |-> acc.nextState, transaction |-> t])
-  \*                                         calcultate next state
+  \*                                         calculate next state
                                            , nextState |-> effects(acc.nextState,t) 
                             ],
                             ordering, accummulator)
@@ -139,7 +139,7 @@ CT_SER(transaction, execution) ==
 Serializability(initialState, transactions) == satisfyIsolationLevel(initialState, transactions, CT_SER)
 
 \*SerializabilityDebug(initialState, transactions) == 
-\*  \* if no executions satify commit test, print all executions
+\*  \* if no executions satisfy commit test, print all executions
 \*  \/ (~\E execution \in executions(initialState, transactions): \A transaction \in transactions:
 \*       CT_SER(transaction, execution)) => \A execution \in executions(initialState, transactions): PrintT(<<"Execution not Serializable:",execution>>)
 \*  \* fall back to normal check

specifications/KeyValueStore/KVsnap.tla

@@ -1,6 +1,6 @@
 --------------------------- MODULE KVsnap ---------------------------------
 (**************************************************************************)
-(* Pluscal algoritm for a simple key-value store with snapshot isolation  *)
+(* Pluscal algorithm for a simple key-value store with snapshot isolation  *)
 (* This version has atomic updates of store and missed sets of txns       *)
 (**************************************************************************)
 EXTENDS Integers, Sequences, FiniteSets, Util

specifications/KeyValueStore/Util.tla

@@ -19,7 +19,7 @@ Index(seq, e) ==  CHOOSE i \in 1..Len(seq): seq[i] = e
 SeqToSet(s) == {s[i] : i \in DOMAIN s}
 Last(seq) == seq[Len(seq)]
 IsEmpty(seq) == Len(seq) = 0
-\* Remove all occurences of `elem` from `seq`
+\* Remove all occurrences of `elem` from `seq`
 Remove(seq, elem) == SelectSeq(seq, LAMBDA e: e /= elem)
 
 \* Dual to UNION on intersect

specifications/KnuthYao/SimKnuthYao.tla

@@ -34,7 +34,7 @@ SimInit ==
     /\ flip  \in Flip
 
 SimNext ==
-    \* Need an artifical initial state to be able to model a crooked coin.  Otherwise,
+    \* Need an artificial initial state to be able to model a crooked coin.  Otherwise,
     \* the first flip will always be fair. 
     \/ /\ state = "init"
        /\ state' = "s0"

specifications/MisraReachability/ParReachProofs.tla

@@ -2,7 +2,7 @@
 (***************************************************************************)
 (* This module contains TLAPS checked proofs of the safety properties      *)
 (* asserted in module ParReach--namely, the invariance of Inv and that the *)
-(* parallel alorithm implements the safety part of Misra's algorithm under *)
+(* parallel algorithm implements the safety part of Misra's algorithm under *)
 (* the refinement mapping defined there.                                   *)
 (***************************************************************************)
 EXTENDS ParReach, Integers, TLAPS

specifications/PaxosHowToWinATuringAward/Consensus.tla

@@ -49,7 +49,7 @@ Init == chosen = {}
 (***************************************************************************)
 (* The next-state relation describing how 'chosen' can change from one     *)
 (* step to the next.  Note that is enabled (equals true for some next      *)
-(* value chosen' of choseen) if and only if chosen equals the empty set.   *)
+(* value chosen' of chosen) if and only if chosen equals the empty set.   *)
 (***************************************************************************)
 Next == /\ chosen = {}
         /\ \E v \in Value : chosen' = {v}
@@ -69,7 +69,7 @@ Inv == /\ TypeOK
        /\ Cardinality(chosen) \leq 1
 
 (***************************************************************************)
-(* The following theorem asserts the desired safety propert.  Its proof    *)
+(* The following theorem asserts the desired safety property.  Its proof    *)
 (* appears after the theorem.  This proof is easily checked by the TLAPS   *)
 (* prover.                                                                 *)
 (***************************************************************************)