Skip to content

Commit

Permalink
Add Java Module Override for SequencesExt!AllSubSeqs.
Browse files Browse the repository at this point in the history
[Feature]
  • Loading branch information
lemmy committed Jan 25, 2024
1 parent e6a3954 commit 070954c
Show file tree
Hide file tree
Showing 2 changed files with 37 additions and 2 deletions.
33 changes: 31 additions & 2 deletions modules/tlc2/overrides/SequencesExt.java
Original file line number Diff line number Diff line change
Expand Up @@ -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];
Expand All @@ -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);
}
}
6 changes: 6 additions & 0 deletions tests/SequencesExtTests.tla
Original file line number Diff line number Diff line change
Expand Up @@ -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(<<>>,<<>>,<<>>) = <<>>
Expand Down

0 comments on commit 070954c

Please sign in to comment.