From fa56512a37421631ee140e86429e095c532a6904 Mon Sep 17 00:00:00 2001 From: Markus Alexander Kuppe Date: Thu, 25 Jan 2024 10:41:57 -0800 Subject: [PATCH] Add Java Module Override for SequencesExt!AllSubSeqs. (#97) [Feature] Signed-off-by: Markus Alexander Kuppe --- modules/tlc2/overrides/SequencesExt.java | 33 ++++++++++++++++++++++-- tests/SequencesExtTests.tla | 6 +++++ 2 files changed, 37 insertions(+), 2 deletions(-) diff --git a/modules/tlc2/overrides/SequencesExt.java b/modules/tlc2/overrides/SequencesExt.java index 4c6cb19..b28a570 100644 --- 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 index 995cce9..22e4b0d 100644 --- 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(<<>>,<<>>,<<>>) = <<>>