Add Java Module Override for SequencesExt!AllSubSeqs.

[Feature]
tlaplus · Jan 25, 2024 · 070954c · 070954c
1 parent e6a3954
commit 070954c
Show file tree

Hide file tree

Showing 2 changed files with 37 additions and 2 deletions.
diff --git a/modules/tlc2/overrides/SequencesExt.java b/modules/tlc2/overrides/SequencesExt.java
@@ -582,8 +582,8 @@ public static Value removeFirstMatch(final Value s, final OpValue test) {
 	public static Value Suffixes(final Value s) {
 		final TupleValue seq = (TupleValue) s.toTuple();
 		if (seq == null) {
-			throw new EvalException(EC.TLC_MODULE_ARGUMENT_ERROR,
-					new String[] { "first", "Suffixes", "sequence", Values.ppr(s.toString()) });
+			throw new EvalException(EC.TLC_MODULE_ONE_ARGUMENT_ERROR,
+					new String[] { "Suffixes", "sequence", Values.ppr(s.toString()) });
 		}
 
 		final Value[] vals = new Value[seq.elems.length + 1];
@@ -605,4 +605,33 @@ public static Value Suffixes(final Value s) {
 		// expensive: return new SetEnumValue(vals, false).normalize();
 		return new SetEnumValue(vals, true);
 	}
+
+	/*
+	 * AllSubSeqs(s) ==
+	 *    { FoldFunction(Snoc, <<>>, [ i \in D |-> s[i] ]) : D \in SUBSET DOMAIN s }
+	 */
+	@TLAPlusOperator(identifier = "AllSubSeqs", module = "SequencesExt", warn = false)
+	public static Value AllSubSeqs(final Value s) {
+		final TupleValue seq = (TupleValue) s.toTuple();
+		if (seq == null) {
+			throw new EvalException(EC.TLC_MODULE_ONE_ARGUMENT_ERROR,
+					new String[] { "AllSubSeqs", "sequence", Values.ppr(s.toString()) });
+		}
+
+		final int n = seq.elems.length;
+		final Value[] vals = new Value[(int) Math.pow(2, n)];
+
+        for (int i = 0; i < (1 << n); i++) {
+        	int k = 0;
+        	final Value[] subSeq = new Value[Long.bitCount(i)];
+            for (int j = 0; j < n; j++) {
+                if ((i & (1 << j)) != 0) {
+                	subSeq[k++] = seq.elems[j];
+                }
+            }
+			vals[i] = new TupleValue(subSeq);
+        }
+
+		return new SetEnumValue(vals, false);
+	}
 }
diff --git a/tests/SequencesExtTests.tla b/tests/SequencesExtTests.tla
@@ -243,6 +243,12 @@ ASSUME AllSubSeqs(<<"a","c","b","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">> }
 
+AllSubSeqsPure(s) ==
+	{ FoldFunction(Snoc, <<>>, [ i \in D |-> s[i] ]) : D \in SUBSET DOMAIN s }
+
+ASSUME \A s \in {<<>>, <<1>>, <<1,1>>, <<1,1,1>>, <<1,2,3,4>>, <<"a","c","b","d","b">>}:
+    AllSubSeqs(s) = AllSubSeqsPure(s)
+
 -----------------------------------------------------------------------------
 
 ASSUME ReplaceFirstSubSeq(<<>>,<<>>,<<>>) = <<>>