Fix sequence diff alignment

[younes-io]

• Summary
  • Fix sequence diff alignment for inserts/deletes; addresses the issue raised by @lemmy: Correct deleted value handling #491 (comment)
• Root cause
  • Sequence diffs were index-aligned, so head/middle deletions appeared as modifications instead of deletions.
• Fix
  • Use LCS alignment for sequences when lengths differ, preserving ordered diff for equal lengths.
• Tests
  • MOCHA_GREP="Sequence diff" npm test
  • MOCHA_GREP="Check Model Test Suite" npm test

[younes-io]

@lemmy here I did not port the Toolbox diff algorithm, as this was something I realized later on in your comment. The change is limited to src/model/check.ts: it adds an LCS-based alignment only for sequences when lengths differ, while keeping the existing ordered diff for equal lengths.

I looked up the Toolbox diff algorithm and it is not LCS. It’s prefix/suffix detection for sequences and falls back to function diff (index-based) otherwise. That means this PR is not a port of the Toolbox logic.

I'm converting this to Draft, for now.

[lemmy]

@younes-io I wonder whether the extension should adopt the same behavior as the Toolbox and not display deleted items. The current behavior—showing deleted items at the bottom—is rather confusing, especially given that the extension also displays the indices of elements in the sequence. If deleted items must be shown, it would be clearer to display them at their original positions rather than moving them to the bottom.

----- MODULE SeqRem -----
EXTENDS Sequences

VARIABLES s

Init == s = << 1, 2, 3>>

Next == s # << >> /\ s' = Tail(s)

======
------ CONFIG SeqRem -----
INIT Init
NEXT Next
CHECK_DEADLOCK TRUE 
======

[younes-io]

Thanks for the repro. I’ve switched the sequence diff to match Toolbox (prefix/suffix add/remove; otherwise index diff), and I’ve hidden deleted sequence items so they don’t appear at the bottom. This should address the confusing output in your screenshots.

[lemmy]

New functionality looks good to me.