Add SequencesExt!Snoc and SequencesExt!AllSubSeqs.

tlaplus · Jan 20, 2024 · e6a3954 · e6a3954
1 parent 243fa67
commit e6a3954
Show file tree

Hide file tree

Showing 2 changed files with 42 additions and 0 deletions.
diff --git a/modules/SequencesExt.tla b/modules/SequencesExt.tla
@@ -195,6 +195,15 @@ Cons(elt, seq) ==
     (************************************************************************)
     <<elt>> \o seq
 
+Snoc(elt, seq) == 
+    (************************************************************************)
+    (* Reverses the operands of Sequences!Append for better compatibility   *)
+    (* with FoldFunction below.                                             *)
+    (* Example:                                                             *)
+    (*  FoldSeq(LAMBDA x,y: {x} \cup y, {}, <<1,2,1>>) = Range(<<1,2,1>>)   *)
+    (************************************************************************)
+    Append(seq, elt)
+
 Front(s) == 
   (**************************************************************************)
   (* The sequence formed by removing its last element.                      *)
@@ -386,6 +395,21 @@ SubSeqs(s) ==
   (**************************************************************************)
   { SubSeq(s, i+1, j) : i, j \in 0..Len(s) }
 
+AllSubSeqs(s) ==
+  (**************************************************************************)
+  (* SubSeqs(s)                                                             *)
+  (*      \cup                                                              *)
+  (*         { subsequences of s, with arbitrarily many elts removed }      *)
+  (*                                                                        *)
+  (* Example:                                                               *)
+  (*  AllSubSeqs(<<1,2,3,4>>) =                                             *)
+  (*       {<<>>, <<1>>, <<2>>, <<3>>, <<4>>,                               *)
+  (*        <<1, 2>>, <<1, 3>>, <<1, 4>>,                                   *)
+  (*        <<2, 3>>, <<2, 4>>, <<3, 4>>,                                   *)
+  (*        <<1, 2, 3>>, <<1, 2, 4>>, <<1, 3, 4>>, <<2, 3, 4>>,             *)
+  (*        <<1, 2, 3, 4>>}                                                 *)
+  (**************************************************************************)
+  { FoldFunction(Snoc, <<>>, [ i \in D |-> s[i] ]) : D \in SUBSET DOMAIN s }
 
 IndexFirstSubSeq(s, t) ==
   (**************************************************************************)

diff --git a/tests/SequencesExtTests.tla b/tests/SequencesExtTests.tla
@@ -227,6 +227,24 @@ ASSUME \A seq \in BoundedSeq(1..5, 5) :
 
 -----------------------------------------------------------------------------
 
+ASSUME AllSubSeqs(<<>>) = {<<>>}
+ASSUME AllSubSeqs(<<1>>) = {<<>>, <<1>>}
+ASSUME AllSubSeqs(<<1,1>>) = {<<>>, <<1>>, <<1,1>>}
+ASSUME AllSubSeqs(<<1,1,1>>) = {<<>>, <<1>>, <<1,1>>, <<1,1,1>>}
+
+ASSUME AllSubSeqs(<<1,2,3,4>>) = {<<>>, <<1>>, <<2>>, <<3>>, <<4>>, 
+                                <<1, 2>>, <<1, 3>>, <<1, 4>>, <<2, 3>>, <<2, 4>>, <<3, 4>>,
+                                <<1, 2, 3>>, <<1, 2, 4>>, <<1, 3, 4>>, <<2, 3, 4>>, <<1, 2, 3, 4>>}
+
+ASSUME AllSubSeqs(<<"a","c","b","d","b">>) = 
+  { <<>>, <<"d">>, <<"a">>, <<"c">>, <<"b">>,
+    <<"d","b">>, <<"a","d">>, <<"a","c">>, <<"a","b">>, <<"c","d">>, <<"c","b">>, <<"b","d">>, <<"b","b">>,
+    <<"a","d","b">>, <<"a","c","d">>, <<"a","c","b">>, <<"a","b","d">>, <<"a","b","b">>, <<"c","d","b">>,
+    <<"c","b","d">>, <<"c","b","b">>, <<"b","d","b">>, <<"a","c","d","b">>, <<"a","c","b","d">>, <<"a","c","b","b">>, <<"a","b","d","b">>,
+    <<"c","b","d","b">>, <<"a","c","b","d","b">> }
+
+-----------------------------------------------------------------------------
+
 ASSUME ReplaceFirstSubSeq(<<>>,<<>>,<<>>) = <<>>
 ASSUME ReplaceFirstSubSeq(<<4>>,<<>>,<<>>) = <<4>>
 ASSUME ReplaceFirstSubSeq(<<4>>,<<4>>,<<>>) = <<>>