Error-Trace modification/addition annotations broken

[lemmy]

The screenshot below shows an action where a node sends a RequestVote message. However, the error-trace viewer incorrectly annotates an existing AppendEntries messages as added, whereas the new RequestVote message is annotated as modified.

My guess is that the error-trace viewer compares the two sets syntactically while assuming some stable order. Related to https://github.com/tlaplus/vscode-tlaplus/issues/261

[lemmy]

Perhaps it's TLC that should provide annotations in its textual error trace to free IDEs from parsing and evaluating values.

[lemmy]

The Toolbox's set difference algorithm:

https://github.com/tlaplus/tlaplus/blob/baf6f1b4000ba72cd4ac2704d07c60ea2ae8343b/toolbox/org.lamport.tla.toolbox.tool.tlc.ui/src/org/lamport/tla/toolbox/tool/tlc/output/data/TLCSetVariableValue.java#L69-L107

[lemmy]

@afonsonf Do you have plans to re-add the functionality that shows deleted set elements in the error trace view?

https://github.com/tlaplus/vscode-tlaplus/blob/0e16f404f55a43abf6e681dce906a7c7cc34e127/resources/check-result-view.js#L334-L336

[lemmy]

Incomplete attempt to bring the rest of the Toolbox diffing over:

diff --git a/src/model/check.ts b/src/model/check.ts
index 79c015a..bf60526 100644
--- a/src/model/check.ts
+++ b/src/model/check.ts
@@ -178,6 +178,14 @@ export class Value {
     format(indent: string): string {
         return `${this.str}`;
     }
+
+    diff(other: Value): boolean {
+        if (this.str !== other.str) {
+            other.setModified();
+            return true;
+        }
+        return false;
+    }
 }

 /**
@@ -257,6 +265,63 @@ export abstract class CollectionValue extends Value {
     formatKey(indent: string, value: Value): string {
         return `${indent}${value.key}: `;
     }
+
+    // diff(other: Value): boolean {
+    //     return false;
+    // }
+    setElementArrayDiffInfo(
+        t: CollectionValue,
+        o: CollectionValue,
+        firstElts: Value[],
+        firstLHKeys: ValueKey[],
+        secondElts: Value[],
+        secondLHKeys: ValueKey[]
+    ): void {
+        const deletedItems = [];
+        for (let i = 0; i < firstElts.length; i++) {
+            let notfound = true;
+            let j = 0;
+            while (notfound && j < secondElts.length) {
+                if (firstLHKeys[i] === secondLHKeys[j]) {
+                    notfound = false;
+                    const first = firstElts[i];
+                    const second = secondElts[j];
+                    if (first.str !== second.str) {
+                        secondElts[i].setModified();
+                        second.setModified();
+                        if (first.constructor === second.constructor) {
+                            // Only diff objects of identical types
+                            first.diff(second);
+                        }
+                    }
+                }
+                j++;
+            }
+            if (notfound) {
+                deletedItems.push(firstElts[i]);
+            }
+        }
+        if (deletedItems.length > 0) {
+            o.addDeletedItems(deletedItems);
+            o.setModified();
+        }
+
+        for (let i = 0; i < secondElts.length; i++) {
+            const s = secondElts[i].str;
+            let notfound = true;
+            let j = 0;
+            while (notfound && j < firstElts.length) {
+                const f = firstElts[j].str;
+                if (f === s) {
+                    notfound = false;
+                }
+                j++;
+            }
+            if (notfound) {
+                secondElts[i].setAdded();
+            }
+        }
+    }
 }

 /**
@@ -381,6 +446,33 @@ export class StructureValue extends CollectionValue {
     formatKey(indent: string, value: Value): string {
         return `${indent}${value.key}` + this.itemSep;
     }
+
+    diff(other: Value): boolean {
+        /*
+         * RECORDS We mark a record element as added or deleted if its label
+         * does not appear in one of the elements of the other record. We
+         * mark the element as changed, and call setInnerDiffInfo on the
+         * elements' values if elements with the same label but different values
+         * appear in the two records.
+         */
+        if (!(other instanceof StructureValue)) {
+            return false;
+        }
+
+        const secondElts: StructureValue = (other as StructureValue);
+
+        const firstLHStrings: ValueKey[] = [];
+        for (let i = 0; i < this.items.length; i++) {
+            firstLHStrings[i] = this.items[i].key;
+        }
+        const secondLHStrings: ValueKey[] = [];
+        for (let i = 0; i < other.items.length; i++) {
+            secondLHStrings[i] = secondElts.items[i].key;
+        }
+
+        this.setElementArrayDiffInfo(this, other, this.items, firstLHStrings, secondElts.items, secondLHStrings);
+        return true;
+    }
 }

 /**
@@ -538,6 +630,15 @@ export function getStatusName(status: CheckStatus): string {
 /**
  * Recursively finds and marks all the changes between two collections.
  */
+export function findChangesOff(prev: CollectionValue, state: CollectionValue): boolean {
+    let i = 0;
+    while (i < prev.items.length && i < state.items.length) {
+        prev.items[i].diff(state.items[i]);
+        i++;
+    }
+    return true;
+}
+
 export function findChanges(prev: CollectionValue, state: CollectionValue): boolean {
     let pi = 0;
     let si = 0;

[lemmy]

@afonsonf Do you have plans to re-add the functionality that shows deleted set elements in the error trace view?

https://github.com/tlaplus/vscode-tlaplus/blob/0e16f404f55a43abf6e681dce906a7c7cc34e127/resources/check-result-view.js#L334-L336

A set will only be marked modified M until the webview shows deleted set elements again.

[afonsonf]

@afonsonf Do you have plans to re-add the functionality that shows deleted set elements in the error trace view?

https://github.com/tlaplus/vscode-tlaplus/blob/0e16f404f55a43abf6e681dce906a7c7cc34e127/resources/check-result-view.js#L334-L336

Hi, true I missed that part in the migration of the ui, I will add it back

[FedericoPonzi]

An MRE would be very helpful here - I tried and failed to reproduce it.