Add ReplaceAll operator to SequencesExt.

modules/SequencesExt.tla

@@ -39,13 +39,30 @@ SetToSeq(S) ==
 
 -----------------------------------------------------------------------------
 
+Contains(s, e) ==
+  (**************************************************************************)
+  (* TRUE iff the element e \in ToSet(s).                                   *)
+  (**************************************************************************)
+  \E i \in 1..Len(s) : s[i] = e
+
 Reverse(s) ==
   (**************************************************************************)
   (* Reverse the given sequence s:  Let l be Len(s) (length of s).          *)
   (* Equals a sequence s.t. << S[l], S[l-1], ..., S[1]>>                    *)
   (**************************************************************************)
   [ i \in 1..Len(s) |-> s[(Len(s) - i) + 1] ]
 
+ReplaceAll(s, old, new) ==
+  (*************************************************************************)
+  (* Equals the sequence s except that all occurrences of element old are  *)
+  (* replaced with the element new.                                        *)
+  (*************************************************************************)
+  LET F[i \in 0..Len(s)] == 
+        IF i = 0 THEN << >>
+                 ELSE IF s[i] = old THEN Append(F[i-1], new)
+                                    ELSE Append(F[i-1], s[i])
+  IN F[Len(s)]
+
 -----------------------------------------------------------------------------
 
 \* The operators below have been extracted from the TLAPS module 

tests/SequencesExtTests.tla

@@ -34,6 +34,9 @@ ASSUME(Reverse(<<"a","a","b">>) = <<"b","a","a">>)
 
 -----------------------------------------------------------------------------
 
+ASSUME(ReplaceAll(<<>>, 1, 4) = <<>>)
+ASSUME(ReplaceAll(<<1,1,2,1,1,3>>, 1, 4) = <<4,4,2,4,4,3>>)
+
 ASSUME(ReplaceAt(<<1>>, 1, 2) = <<2>>) 
 ASSUME(ReplaceAt(<<1,1,1>>, 1, 2) = <<2,1,1>>)