search

tlaplus / CommunityModules

TLA+ snippets, operators, and modules contributed and curated by the TLA+ community
MIT License
273 stars 36 forks source link

Add Java Module Override for SequencesExt!AllSubSeqs. #97

Closed lemmy closed 10 months ago

lemmy commented 10 months ago

Add Java Module Override for SequencesExt!AllSubSeqs.

[Feature]

/cc @eddyashton

lemmy commented 10 months ago

Here are performance numbers, collected from very basic testing:

AllSubSeqsPure(s) ==
    { FoldFunction(Snoc, <<>>, [ i \in D |-> s[i] ]) : D \in SUBSET DOMAIN s }

ASSUME \A s \in BoundedSeq({"a","b","c","d"}, 9):
    AllSubSeqsPure(s) = AllSubSeqsPure(s)
Finished in 03min 31s at (2024-01-25 10:34:52)
ASSUME \A s \in BoundedSeq({"a","b","c","d"}, 9):
    AllSubSeqs(s) = AllSubSeqs(s)
Finished in 27s at (2024-01-25 10:37:06)