diff --git a/modules/SequencesExt.tla b/modules/SequencesExt.tla index 54b2d5f..2183f30 100644 --- a/modules/SequencesExt.tla +++ b/modules/SequencesExt.tla @@ -446,7 +446,11 @@ Interleave(s, t) == ELSE u[i-1] \o << <> >> \o << <> >> IN Last(u) \* error "Interleave: sequences must have same length" - [] Len(s) = Len(t) /\ Len(s) = 0 -> << <<>>, <<>> >> + \* <<>> is the identity of \o, which is what the arm above builds the + \* result with, so Len(Interleave(s, t)) = 2 * Len(s) holds for the empty + \* sequence as well. It also matches the other operators of this module + \* on an empty argument, such as Zip, FlattenSeq, and Reverse. + [] Len(s) = Len(t) /\ Len(s) = 0 -> << >> (**************************************************************************) (* The set of all subsequences of the sequence s . Note that the empty *) diff --git a/tests/SequencesExtTests.tla b/tests/SequencesExtTests.tla index 61a0d0f..7ac3f94 100644 --- a/tests/SequencesExtTests.tla +++ b/tests/SequencesExtTests.tla @@ -172,7 +172,7 @@ ASSUME FlattenSeq(<<"a", "b">>) = "ab" ----------------------------------------------------------------------------- -ASSUME Interleave(<<>>, <<>>) = << <<>>, <<>> >> +ASSUME Interleave(<<>>, <<>>) = << >> ASSUME Interleave(<< <<>> >>, <<1>>) = << << <<>> >>, <<1>> >> ASSUME Interleave(<<1>>, << <<>> >>) = << <<1>>, << <<>> >> >> ASSUME Interleave(<<2>>,<<2>>) = << <<2>>, <<2>> >> @@ -184,6 +184,14 @@ ASSUME AssertEq(FlattenSeq(Interleave(<<1,3>>,<<2,4>>)), <<1, 2, 3, 4>>) ASSUME Interleave(<<"a", "c">>, <<"b", "d">>) = <<<<"a">>, <<"b">>, <<"c">>, <<"d">>>> ASSUME AssertEq(FlattenSeq(Interleave(<<"a", "c">>, <<"b", "d">>)), <<"a", "b", "c", "d">>) +\* Two entries per position of s, the odd ones from s and the even ones from +\* t. The empty case is the one this used to fail, with a length of 2. +ASSUME \A s \in BoundedSeq(1..3, 3) : + \A t \in {u \in BoundedSeq(1..3, 3) : Len(u) = Len(s)} : + /\ Len(Interleave(s, t)) = 2 * Len(s) + /\ \A i \in 1..Len(s) : /\ Interleave(s, t)[2*i - 1] = <> + /\ Interleave(s, t)[2*i] = <> + ----------------------------------------------------------------------------- ASSUME Zip(<<>>, <<>>) = << >>