diff --git a/modules/SequencesExt.tla b/modules/SequencesExt.tla index 1c47db2..9739a26 100644 --- a/modules/SequencesExt.tla +++ b/modules/SequencesExt.tla @@ -320,7 +320,7 @@ FlattenSeq(seqs) == Zip(s, t) == (**************************************************************************) (* A sequence where the i-th tuple contains the i-th element of s and *) - (* t in this order. Not defined for Len(s) # Len(t) *) + (* t in this order. *) (* *) (* Examples: *) (* *) @@ -329,10 +329,9 @@ Zip(s, t) == (* Zip(<<1, 3>>, <<2, 4>>) = <<<<1, 2>>, <<3, 4>>>> *) (* FlattenSeq(Zip(<<1, 3>>, <<2, 4>>)) = <<1, 2, 3, 4>>>> *) (**************************************************************************) - CASE Len(s) = Len(t) /\ Len(s) > 0 -> - [ i \in DOMAIN s |-> <> ] - [] Len(s) = Len(t) /\ Len(s) = 0 -> << >> - \* error "Zip: sequences must have same length" + IF Len(s) < Len(t) + THEN FoldLeft(LAMBDA acc, e: Append(acc, << e, t[Len(acc)+1] >>), <<>>, s) + ELSE FoldLeft(LAMBDA acc, e: Append(acc, << s[Len(acc)+1], e >>), <<>>, t) Interleave(s, t) == (**************************************************************************) diff --git a/tests/SequencesExtTests.tla b/tests/SequencesExtTests.tla index 4ae61fe..7005f3e 100644 --- a/tests/SequencesExtTests.tla +++ b/tests/SequencesExtTests.tla @@ -194,6 +194,13 @@ ASSUME AssertEq(FlattenSeq(Zip(<<1, 3>>, <<2, 4>>)), <<1, 2, 3, 4>>) ASSUME Zip(<<"a", "c">>, <<"b", "d">>) = << <<"a", "b">>, <<"c", "d">> >> ASSUME AssertEq(FlattenSeq(Zip(<<"a", "c">>, <<"b", "d">>)), <<"a", "b", "c", "d">>) +ASSUME Zip(<<1>>, <<>>) = << >> +ASSUME Zip(<<>>, <<1>>) = << >> +ASSUME Zip(<<2>>, <<2, 2>>) = << <<2, 2>> >> +ASSUME Zip(<<2, 3>>, <<3>>) = << <<2, 3>> >> +ASSUME Zip(<<2,3,3>>, <<2, 2>>) = << <<2, 2>>, <<3, 2>> >> +ASSUME Zip(<<2, 3>>, <<3,3,3>>) = << <<2, 3>>, <<3, 3>> >> + ----------------------------------------------------------------------------- ASSUME SubSeqs(<<>>) = {<<>>}