m3c: further debugging of flaky tests

LearnLib · Mar 7, 2025 · 9b8524a · 9b8524a
1 parent 731a5b1
commit 9b8524a
Showing 1 changed file with 15 additions and 0 deletions.
diff --git a/...cking/m3c/src/test/java/net/automatalib/modelchecker/m3c/solver/SolverHistoryADDTest.java b/...cking/m3c/src/test/java/net/automatalib/modelchecker/m3c/solver/SolverHistoryADDTest.java
@@ -88,6 +88,7 @@ public void testMustTransformers(SolverHistory<ADDTransformer<String, String>, S
 
         for (int i = 0; i < Math.pow(2, numSubformulas); i++) {
             String errMsg = "Failure in system: " + i;
+            checkATransformer(aPT, errMsg);
             String binaryString = String.format("%05d", Integer.parseInt(Integer.toBinaryString(i)));
             boolean[] input = new boolean[numSubformulas];
             input[0] = binaryString.charAt(0) == '1';
@@ -119,4 +120,18 @@ public void testMustTransformers(SolverHistory<ADDTransformer<String, String>, S
         }
     }
 
+    private static void checkATransformer(ADDTransformer<String, String> aPT, String errMsg) {
+        XDD<BooleanVector> dd = aPT.getAdd();
+        Assert.assertNotNull(dd, errMsg);
+        Assert.assertEquals(dd.readIndex(), 0, errMsg);
+        XDD<BooleanVector> ddT = dd.t();
+        XDD<BooleanVector> ddE = dd.e();
+        Assert.assertTrue(ddT.isConstant(), errMsg);
+        Assert.assertTrue(ddE.isConstant(), errMsg);
+        boolean[] expectedTrueBranch = {false, false, false, false, true};
+        boolean[] expectedFalseBranch = {false, false, false, false, false};
+        Assert.assertEquals(ddT.v().data(), expectedTrueBranch, errMsg);
+        Assert.assertEquals(ddE.v().data(), expectedFalseBranch, errMsg);
+    }
+
 }