From 22baed538163243fc2a0dc5d1ea0f55237d06f2d Mon Sep 17 00:00:00 2001 From: Markus Alexander Kuppe Date: Sat, 3 Oct 2026 13:25:10 -0700 Subject: [PATCH 1/2] Add tests for SequencesExt SelectInSubSeq and SelectLastInSubSeq Check the TLC overrides exhaustively against pure TLA+ definitions over all sequences in BoundedSeq(1..3, 4) and all ranges from..to, including empty ones (from > to). The overrides return an index into seq whereas the TLA+ definitions return an index into SubSeq(seq, from, to), so the tests fail whenever from > 1. Related to Github issue #131 https://github.com/tlaplus/CommunityModules/issues/131 [Tests] Co-authored-by: Claude Opus 5.5 Signed-off-by: Markus Alexander Kuppe --- tests/SequencesExtTests.tla | 22 ++++++++++++++++++++++ 1 file changed, 22 insertions(+) diff --git a/tests/SequencesExtTests.tla b/tests/SequencesExtTests.tla index 7ac3f94..26e0cb5 100644 --- a/tests/SequencesExtTests.tla +++ b/tests/SequencesExtTests.tla @@ -447,6 +447,28 @@ ASSUME AssertEq(SelectLastInSubSeq(<<>>, 1, Len(<<>>), Op), 0) ASSUME AssertEq(SelectLastInSubSeq(<<1,1,2>> , 1, 3, LAMBDA e : e = 1), 2) ASSUME AssertEq(SelectLastInSubSeq(<<1,1,2,2>>, 2, 4, LAMBDA e : e = 2), 4) +SelectInSubSeqPure(seq, from, to, Test(_)) == + LET sub == SubSeq(seq, from, to) + I == { i \in 1..Len(sub) : Test(sub[i]) } + IN IF I # {} THEN CHOOSE i \in I : \A j \in I : i <= j ELSE 0 + +SelectLastInSubSeqPure(seq, from, to, Test(_)) == + LET sub == SubSeq(seq, from, to) + I == { i \in 1..Len(sub) : Test(sub[i]) } + IN IF I # {} THEN CHOOSE i \in I : \A j \in I : i >= j ELSE 0 + +ASSUME AssertEq(SelectInSubSeq(<<1,1,2>>, 2, 3, LAMBDA e : e = 1), SelectInSubSeqPure(<<1,1,2>>, 2, 3, LAMBDA e : e = 1)) +ASSUME AssertEq(SelectInSubSeq(<<1,1,2,2>>, 2, 4, LAMBDA e : e = 2), SelectInSubSeqPure(<<1,1,2,2>>, 2, 4, LAMBDA e : e = 2)) +ASSUME AssertEq(SelectLastInSubSeq(<<1,1,2,2>>, 2, 4, LAMBDA e : e = 2), SelectLastInSubSeqPure(<<1,1,2,2>>, 2, 4, LAMBDA e : e = 2)) + +ASSUME \A seq \in BoundedSeq(1..3, 4): + \A from \in 1..Len(seq) + 1, to \in 0..Len(seq): + \A v \in 1..3: + /\ AssertEq(SelectInSubSeq(seq, from, to, LAMBDA e : e = v), + SelectInSubSeqPure(seq, from, to, LAMBDA e : e = v)) + /\ AssertEq(SelectLastInSubSeq(seq, from, to, LAMBDA e : e = v), + SelectLastInSubSeqPure(seq, from, to, LAMBDA e : e = v)) + ----------------------------------------------------------------------------- ASSUME AssertEq(Suffixes(<<>>), {<<>>}) From 674d3992861f537e06444089ce7247baf63e42ab Mon Sep 17 00:00:00 2001 From: Markus Alexander Kuppe Date: Sat, 3 Oct 2026 13:31:24 -0700 Subject: [PATCH 2/2] Make SelectInSubSeq and SelectLastInSubSeq return indices into seq The TLA+ definitions returned an index into SubSeq(seq, from, to), whereas the doc comments and the TLC overrides return an index into seq. Align the definitions with the overrides, which most users rely on. This is a breaking change for users of the plain TLA+ definitions, but no other operator in the module and no proof depends on them. Fixes Github issue #131 https://github.com/tlaplus/CommunityModules/issues/131 [Bug] Co-authored-by: Claude Opus 5.5 Signed-off-by: Markus Alexander Kuppe --- modules/SequencesExt.tla | 6 ++++-- tests/SequencesExtTests.tla | 6 ++---- 2 files changed, 6 insertions(+), 6 deletions(-) diff --git a/modules/SequencesExt.tla b/modules/SequencesExt.tla index 2183f30..b828acb 100644 --- a/modules/SequencesExt.tla +++ b/modules/SequencesExt.tla @@ -167,7 +167,8 @@ SelectInSeq(seq, Test(_)) == (* FALSE for all elements. *) (*************************************************************************) SelectInSubSeq(seq, from, to, Test(_)) == - SelectInSeq(SubSeq(seq, from, to), Test) + LET I == { i \in from..to : Test(seq[i]) } + IN IF I # {} THEN Min(I) ELSE 0 (*************************************************************************) (* Selects the index of the last element such that Test(seq[i]) is true *) @@ -183,7 +184,8 @@ SelectLastInSeq(seq, Test(_)) == (* FALSE for all elements. *) (*************************************************************************) SelectLastInSubSeq(seq, from, to, Test(_)) == - SelectLastInSeq(SubSeq(seq, from, to), Test) + LET I == { i \in from..to : Test(seq[i]) } + IN IF I # {} THEN Max(I) ELSE 0 ----------------------------------------------------------------------------- diff --git a/tests/SequencesExtTests.tla b/tests/SequencesExtTests.tla index 26e0cb5..3ab2732 100644 --- a/tests/SequencesExtTests.tla +++ b/tests/SequencesExtTests.tla @@ -448,13 +448,11 @@ ASSUME AssertEq(SelectLastInSubSeq(<<1,1,2>> , 1, 3, LAMBDA e : e = 1), 2) ASSUME AssertEq(SelectLastInSubSeq(<<1,1,2,2>>, 2, 4, LAMBDA e : e = 2), 4) SelectInSubSeqPure(seq, from, to, Test(_)) == - LET sub == SubSeq(seq, from, to) - I == { i \in 1..Len(sub) : Test(sub[i]) } + LET I == { i \in from..to : Test(seq[i]) } IN IF I # {} THEN CHOOSE i \in I : \A j \in I : i <= j ELSE 0 SelectLastInSubSeqPure(seq, from, to, Test(_)) == - LET sub == SubSeq(seq, from, to) - I == { i \in 1..Len(sub) : Test(sub[i]) } + LET I == { i \in from..to : Test(seq[i]) } IN IF I # {} THEN CHOOSE i \in I : \A j \in I : i >= j ELSE 0 ASSUME AssertEq(SelectInSubSeq(<<1,1,2>>, 2, 3, LAMBDA e : e = 1), SelectInSubSeqPure(<<1,1,2>>, 2, 3, LAMBDA e : e = 1))