[DO NOT MERGE] Formal verification reference: TLA+/Lean models, defect catalogue and fix plans

com.avaloq.tools.ddk.xtext.test/META-INF/MANIFEST.MF

@@ -32,7 +32,8 @@ Require-Bundle: com.avaloq.tools.ddk.xtext,
  junit-platform-suite-engine,
  org.eclipse.xtext.testing,
  org.opentest4j
-Import-Package: com.avaloq.tools.ddk.check.runtime.test.core,
+Import-Package: com.avaloq.tools.ddk.caching,
+ com.avaloq.tools.ddk.check.runtime.test.core,
  com.avaloq.tools.ddk.check.test.core,
  com.avaloq.tools.ddk.check.test.runtime.tests,
  com.avaloq.tools.ddk.check.ui.test,

com.avaloq.tools.ddk.xtext.test/src/com/avaloq/tools/ddk/xtext/XtextTestSuite.java

@@ -14,9 +14,12 @@
 import org.junit.platform.suite.api.Suite;
 
 import com.avaloq.tools.ddk.xtext.builder.XtextBuildTriggerTest;
+import com.avaloq.tools.ddk.xtext.builder.resourceloader.ParallelResourceLoaderTest;
+import com.avaloq.tools.ddk.xtext.formatting.ExtendedFormattingConfigBasedStreamSortLocatorsTest;
 import com.avaloq.tools.ddk.xtext.jupiter.formatter.FormatterTest;
 import com.avaloq.tools.ddk.xtext.linking.AbstractFragmentProviderTest;
 import com.avaloq.tools.ddk.xtext.linking.ShortFragmentProviderTest;
+import com.avaloq.tools.ddk.xtext.naming.QualifiedNameLookupFormalTest;
 import com.avaloq.tools.ddk.xtext.naming.QualifiedNamePatternTest;
 import com.avaloq.tools.ddk.xtext.naming.QualifiedNameSegmentTreeLookupTest;
 import com.avaloq.tools.ddk.xtext.resource.AbstractSelectorFragmentProviderTest;
@@ -37,12 +40,15 @@
   AbstractSelectorFragmentProviderTest.class,
   ResourceDescriptionDeltaTest.class,
   XtextBuildTriggerTest.class,
+  ParallelResourceLoaderTest.class,
   FormatterTest.class,
   QualifiedNamePatternTest.class,
   BugAig1084.class,
   RuntimeProjectUtilTest.class,
   QualifiedNameSegmentTreeLookupTest.class,
-  PatternAwareEObjectDescriptionLookUpTest.class})
+  QualifiedNameLookupFormalTest.class,
+  PatternAwareEObjectDescriptionLookUpTest.class,
+  ExtendedFormattingConfigBasedStreamSortLocatorsTest.class})
 // @Format-On
 public class XtextTestSuite {
 }

com.avaloq.tools.ddk.xtext.test/src/com/avaloq/tools/ddk/xtext/builder/resourceloader/ParallelResourceLoaderTest.java

@@ -0,0 +1,94 @@
+/*******************************************************************************
+ * Copyright (c) 2026 Avaloq Group AG and others.
+ * All rights reserved. This program and the accompanying materials
+ * are made available under the terms of the Eclipse Public License v1.0
+ * which accompanies this distribution, and is available at
+ * http://www.eclipse.org/legal/epl-v10.html
+ *
+ * Contributors:
+ *     Avaloq Group AG - initial API and implementation
+ *******************************************************************************/
+package com.avaloq.tools.ddk.xtext.builder.resourceloader;
+
+import static org.junit.jupiter.api.Assertions.assertInstanceOf;
+import static org.junit.jupiter.api.Assertions.assertSame;
+import static org.junit.jupiter.api.Assertions.assertThrows;
+import static org.junit.jupiter.api.Assertions.assertTrue;
+import static org.mockito.ArgumentMatchers.any;
+import static org.mockito.Mockito.mock;
+import static org.mockito.Mockito.when;
+
+import java.util.Collections;
+import java.util.List;
+import java.util.concurrent.CountDownLatch;
+import java.util.concurrent.TimeUnit;
+import java.util.concurrent.TimeoutException;
+
+import org.eclipse.emf.common.util.URI;
+import org.eclipse.emf.ecore.resource.Resource;
+import org.eclipse.emf.ecore.resource.ResourceSet;
+import org.eclipse.emf.ecore.resource.impl.ResourceImpl;
+import org.eclipse.emf.ecore.resource.impl.ResourceSetImpl;
+import org.eclipse.xtext.builder.resourceloader.IResourceLoader.LoadOperation;
+import org.eclipse.xtext.builder.resourceloader.IResourceLoader.LoadOperationException;
+import org.eclipse.xtext.builder.resourceloader.IResourceLoader.Sorter;
+import org.eclipse.xtext.resource.IResourceServiceProvider;
+import org.eclipse.xtext.resource.persistence.SourceLevelURIsAdapter;
+import org.eclipse.xtext.ui.resource.IResourceSetProvider;
+import org.junit.jupiter.api.Disabled;
+import org.junit.jupiter.api.Test;
+
+import com.google.common.util.concurrent.Uninterruptibles;
+import com.google.inject.Guice;
+
+
+/**
+ * Tests for {@link ParallelResourceLoader}.
+ */
+@SuppressWarnings("nls")
+public class ParallelResourceLoaderTest {
+
+  private static final URI SLOW_URI = URI.createURI("platform:/resource/project/slow.test");
+  private static final long TIMEOUT_MILLIS = 50;
+
+  @Disabled("Documents LDR-1, see formal/BUGS.md; enable with the fix")
+  @Test
+  public void timeoutKeepsPendingResultAvailable() {
+    CountDownLatch loadReleased = new CountDownLatch(1);
+    Resource slowResource = new ResourceImpl(SLOW_URI);
+    ParallelResourceLoader loader = new ParallelResourceLoader(resourceSetProvider(), new Sorter.NoSorting(), 1, -1) {
+      @Override
+      protected Resource loadResource(final URI uri, final ResourceSet localResourceSet, final ResourceSet parentResourceSet) {
+        Uninterruptibles.awaitUninterruptibly(loadReleased);
+        return slowResource;
+      }
+    };
+    IResourceServiceProvider.Registry registry = mock(IResourceServiceProvider.Registry.class);
+    Guice.createInjector(binder -> binder.bind(IResourceServiceProvider.Registry.class).toInstance(registry)).injectMembers(loader);
+    loader.setTimeout(TIMEOUT_MILLIS, TimeUnit.MILLISECONDS);
+
+    ResourceSet parent = new ResourceSetImpl();
+    SourceLevelURIsAdapter.setSourceLevelUris(parent, Collections.emptySet());
+    LoadOperation operation = loader.create(parent, null);
+    try {
+      operation.load(List.of(SLOW_URI));
+
+      LoadOperationException timeout = assertThrows(LoadOperationException.class, operation::next);
+      assertInstanceOf(TimeoutException.class, timeout.getCause());
+      assertTrue(operation.hasNext(), "a timed-out poll must not consume the pending result");
+
+      loadReleased.countDown();
+      assertSame(slowResource, operation.next().getResource());
+    } finally {
+      loadReleased.countDown();
+      operation.cancel();
+    }
+  }
+
+  private static IResourceSetProvider resourceSetProvider() {
+    IResourceSetProvider provider = mock(IResourceSetProvider.class);
+    when(provider.get(any())).thenAnswer(invocation -> new ResourceSetImpl());
+    return provider;
+  }
+
+}

com.avaloq.tools.ddk.xtext.test/src/com/avaloq/tools/ddk/xtext/formatting/ExtendedFormattingConfigBasedStreamSortLocatorsTest.java

@@ -0,0 +1,96 @@
+/*******************************************************************************
+ * Copyright (c) 2026 Avaloq Group AG and others.
+ * All rights reserved. This program and the accompanying materials
+ * are made available under the terms of the Eclipse Public License v1.0
+ * which accompanies this distribution, and is available at
+ * http://www.eclipse.org/legal/epl-v10.html
+ *
+ * Contributors:
+ *     Avaloq Group AG - initial API and implementation
+ *******************************************************************************/
+package com.avaloq.tools.ddk.xtext.formatting;
+
+import static org.junit.jupiter.api.Assertions.assertEquals;
+
+import java.lang.reflect.InvocationTargetException;
+import java.lang.reflect.Method;
+import java.util.ArrayList;
+import java.util.List;
+
+import org.eclipse.xtext.XtextFactory;
+import org.eclipse.xtext.formatting.impl.AbstractFormattingConfig.ElementLocator;
+import org.eclipse.xtext.formatting.impl.FormattingConfig;
+import org.junit.jupiter.api.Disabled;
+import org.junit.jupiter.api.Test;
+
+import com.avaloq.tools.ddk.xtext.formatting.locators.FixedLocator;
+import com.avaloq.tools.ddk.xtext.formatting.locators.NoFormatLocator;
+
+
+/**
+ * Tests the private {@code sortLocators} of {@link ExtendedFormattingConfigBasedStream}, which must order column locators (opening before closing, then by
+ * column) regardless of other locators interleaved in the list.
+ */
+@SuppressWarnings({"PMD.JUnitAssertionsShouldIncludeMessage", "nls"})
+public class ExtendedFormattingConfigBasedStreamSortLocatorsTest {
+
+  private static final String OPEN_1 = "open@1";
+  private static final String OPEN_5 = "open@5";
+
+  private final FormattingConfig config = new FormattingConfig(null, null, null);
+
+  private final ExtendedFormattingConfigBasedStream stream = new ExtendedFormattingConfigBasedStream(null, null, config, null, null, false, null);
+
+  @Test
+  public void testFixedLocatorsAreSortedByColumn() throws ReflectiveOperationException {
+    List<ElementLocator> locators = new ArrayList<>(List.of(opening(5), opening(1)));
+    sortLocators(locators);
+    assertEquals(List.of(OPEN_1, OPEN_5), describeFixedLocators(locators));
+  }
+
+  @Disabled("Documents RO-1, see formal/BUGS.md; enable with the fix")
+  @Test
+  public void testFixedLocatorsAreSortedByColumnAcrossOtherLocator() throws ReflectiveOperationException {
+    List<ElementLocator> locators = new ArrayList<>(List.of(opening(5), new NoFormatLocator(config), opening(1)));
+    sortLocators(locators);
+    assertEquals(List.of(OPEN_1, OPEN_5), describeFixedLocators(locators));
+  }
+
+  @Disabled("Documents RO-1, see formal/BUGS.md; enable with the fix")
+  @Test
+  public void testOpeningFixedLocatorPrecedesClosingAcrossOtherLocator() throws ReflectiveOperationException {
+    List<ElementLocator> locators = new ArrayList<>(List.of(closing(5), new NoFormatLocator(config), opening(5)));
+    sortLocators(locators);
+    assertEquals(List.of(OPEN_5, "close@5"), describeFixedLocators(locators));
+  }
+
+  private FixedLocator opening(final int column) {
+    return new FixedLocator(config, column, false, false, false);
+  }
+
+  private FixedLocator closing(final int column) {
+    FixedLocator locator = new FixedLocator(config, column, false, false, false);
+    locator.after(XtextFactory.eINSTANCE.createKeyword());
+    return locator;
+  }
+
+  private void sortLocators(final List<ElementLocator> locators) throws ReflectiveOperationException {
+    Method method = ExtendedFormattingConfigBasedStream.class.getDeclaredMethod("sortLocators", List.class);
+    method.setAccessible(true); // NOPMD AvoidAccessibilityAlteration - sortLocators is private
+    try {
+      method.invoke(stream, locators);
+    } catch (InvocationTargetException e) {
+      throw new IllegalStateException(e.getCause());
+    }
+  }
+
+  private static List<String> describeFixedLocators(final List<ElementLocator> locators) {
+    List<String> result = new ArrayList<>();
+    for (ElementLocator locator : locators) {
+      if (locator instanceof FixedLocator fixed) {
+        result.add((fixed.getLeft() == null ? "open@" : "close@") + fixed.getColumn());
+      }
+    }
+    return result;
+  }
+}