typos

specs/quint/specs/reset/resetFunc.qnt

@@ -254,7 +254,7 @@ pure def newL2Block (chain: List[L2Block], regs: Set[Registration], provable: bo
 //           The current encoding allows unstale registrations, as long as there are no gaps.
 pure def forkBlock (prev: L2Block, regs: Set[Registration], h: Height, fID: ForkID, provable: bool) : L2Block =
     val allRegs = prev.unstagedUpdates.union(prev.stagedUpdates).union(regs) 
-        // we clarified this point with Matan on the Google doc, that initially only taked about 
+        // we clarified this point with Matan on the Google doc, that initially only talked about 
         // staged and stale, but didn't consider unstaged
     val toApplyNow = allRegs.denseSubset(prev.highest_staged_seq_num)
     val highest = if (toApplyNow == Set()) prev.highest_staged_seq_num else toApplyNow.maxSeqNum()

specs/quint/specs/reset/resetSystem.qnt

@@ -409,7 +409,7 @@ def valid (b: L2Block) : bool =
 
 // The following temporal properties below are just here for documentation. Apalache
 // has some basic temporal model checking capabilities, but does not support the 
-// logic fragement in which these properties are expressed, e.g., alternations of
+// logic fragment in which these properties are expressed, e.g., alternations of
 // temporal operators (i.e., always and eventually), and set quantifieres (forall).
 // We should
 // either find human arguments to support them, or write some test cases to capture