Error-Trace modification/addition annotations broken #291 (#301)

#291
tlaplus · Sep 6, 2023 · 796576c · 796576c
1 parent 4a0d723
commit 796576c
Show file tree

Hide file tree

Showing 3 changed files with 77 additions and 5 deletions.
diff --git a/src/model/check.ts b/src/model/check.ts
@@ -207,9 +207,9 @@ export abstract class CollectionValue extends Value {
         super(key, makeCollectionValueString(items, prefix, postfix, delim, toStr || (v => v.str)));
     }
 
-    addDeletedItems(items: Value[]): void {
+    addDeletedItems(items: Value[]): CollectionValue {
         if (!items || items.length === 0) {
-            return;
+            return this;
         }
         if (!this.deletedItems) {
             this.deletedItems = [];
@@ -220,6 +220,7 @@ export abstract class CollectionValue extends Value {
             newValue.changeType = Change.DELETED;
             delItems.push(newValue);
         });
+        return this;
     }
 
     findItem(id: number): Value | undefined {
@@ -274,6 +275,53 @@ export class SetValue extends CollectionValue {
     formatKey(indent: string, _: Value): string {
         return indent;
     }
+
+    diff(other: Value): boolean {
+        if (!(other instanceof SetValue)) {
+            return false;
+        }
+
+        const o = (other as SetValue);
+
+        let modified = false;
+        const deletedItems = [];
+
+        let i = 0;
+        for (; i < this.items.length; i++) {
+            let notfound = true;
+            let j = 0;
+            while (notfound && j < o.items.length) {
+                if (this.items[i].str === o.items[j].str) {
+                    notfound = false;
+                }
+                j++;
+            }
+            if (notfound) {
+                deletedItems.push(this.items[i]);
+                modified = true;
+            }
+        }
+        if (deletedItems.length > 0) {
+            o.addDeletedItems(deletedItems);
+            o.setModified();
+        }
+
+        for (i = 0; i < o.items.length; i++) {
+            let notfound = true;
+            let j = 0;
+            while (notfound && j < this.items.length) {
+                if (this.items[j].str === o.items[i].str) {
+                    notfound = false;
+                }
+                j++;
+            }
+            if (notfound) {
+                o.items[i].setAdded();
+                o.setModified();
+            }
+        }
+        return modified;
+    }
 }
 
 /**
@@ -506,7 +554,9 @@ export function findChanges(prev: CollectionValue, state: CollectionValue): bool
             deletedItems.push(prevValue);
             pi += 1;
         } else {
-            if (prevValue instanceof CollectionValue && stateValue instanceof CollectionValue) {
+            if (prevValue instanceof SetValue && stateValue instanceof SetValue) {
+                modified = prevValue.diff(stateValue) || modified;
+            } else if (prevValue instanceof CollectionValue && stateValue instanceof CollectionValue) {
                 modified = findChanges(prevValue, stateValue) || modified;
             } else if (prevValue.str !== stateValue.str) {
                 stateValue.changeType = Change.MODIFIED;

diff --git a/tests/suite/model/check.test.ts b/tests/suite/model/check.test.ts
@@ -116,6 +116,28 @@ suite('Check Model Test Suite', () => {
         );
     });
 
+    test('Detects set primitive item deletion', () => {
+        const p = set(ROOT, v(1, 'foo'), v(2, 'bar'), v(3, 'baz'));
+        const s = set(ROOT, v(1, 'foo'), v(2, 'bar'));
+        const e = setX(ROOT, Change.MODIFIED,
+            vX(1, Change.NOT_CHANGED, 'foo'),
+            vX(2, Change.NOT_CHANGED, 'bar')
+        );
+        e.addDeletedItems([v(3, 'baz')]);
+        assertChanges(p, s, e);
+    });
+
+    test('Detects set primitive item deletion 2', () => {
+        const p = set(ROOT, v(1, 'foo'), v(2, 'bar'), v(3, 'baz'));
+        const s = set(ROOT, v(2, 'bar'), v(3, 'baz'));
+        const e = setX(ROOT, Change.MODIFIED,
+            vX(2, Change.NOT_CHANGED, 'bar'),
+            vX(3, Change.NOT_CHANGED, 'baz')
+        );
+        e.addDeletedItems([v(1, 'foo')]);
+        assertChanges(p, s, e);
+    });
+
     test('Propagates modification flag to the top', () => {
         assertChanges(
             struct(ROOT,

diff --git a/tests/suite/parsers/tlc.test.ts b/tests/suite/parsers/tlc.test.ts
@@ -206,8 +206,8 @@ suite('TLC Output Parser Test Suite', () => {
                             '/Users/bob/error_trace.tla', range(12, 8, 14, 24),
                             struct('',
                                 set('FooVar',
-                                    v(1, '4').setModified(),
-                                    v(2, 'TRUE').setAdded()).setModified(),
+                                    v(1, '4').setAdded(),
+                                    v(2, 'TRUE').setAdded()).setModified().addDeletedItems([v(1, '1')]),
                                 v('BarVar', '40').setModified()
                             ).setModified()
                         )