🧪Ordered test cases execution

generate_report.py

@@ -32,28 +32,33 @@ def pretty_message(message):
     error_message = '⚠️ ' + error_type.split('.')[-1]
   return error_message
 
+def extract_task_number(filename):
+  match = re.search(r'T(\d+)', filename)
+  return int(match.group(1)) if match else float('inf')
 
 f = open('report.md', 'w', encoding='utf-8')
 f.write('\n# Report\n\n')
 headers = ["Test", "Status", "Reason"]
 
-for filename in os.listdir(TEST_DIR):
-  if filename.endswith('.xml'):
-    data = []
-    title = filename.split('.')[-2]
-    f.write('## ' + pretty_test_name(title) + '\n\n')
-    root = ET.parse(os.path.join(TEST_DIR, filename))
-    for e in root.findall('.//testcase'):
-      failure = e.find('failure')
-      if failure is not None:
-        test_name = pretty_test_name(e.get('name'))
-        message = pretty_message(failure.get('message'))
-        data.append([test_name, '❌ Failed', message])
-      else:
-        test_name = pretty_test_name(e.get('name'))
-        message = 'Passed'
-        data.append([test_name, '✅ Passed', '-'])
-
-    generate_report_table(headers, data)
-
-f.close()
+filenames = [filename for filename in os.listdir(TEST_DIR) if filename.endswith('.xml')]
+filenames.sort(key=extract_task_number)
+
+for filename in filenames:
+  data = []
+  title = filename.split('.')[-2]
+  f.write('## ' + pretty_test_name(title) + '\n\n')
+  root = ET.parse(os.path.join(TEST_DIR, filename))
+  for e in root.findall('.//testcase'):
+    failure = e.find('failure')
+    if failure is not None:
+      test_name = pretty_test_name(e.get('name'))
+      message = pretty_message(failure.get('message'))
+      data.append([test_name, '❌ Failed', message])
+    else:
+      test_name = pretty_test_name(e.get('name'))
+      message = 'Passed'
+      data.append([test_name, '✅ Passed', '-'])
+
+  generate_report_table(headers, data)
+
+f.close()

src/test/java/de/buw/fm4se/smtsolving/tests/T1WhoKilledAgathaTest.java

@@ -2,23 +2,29 @@
 
 import static org.junit.jupiter.api.Assertions.*;
 
+import org.junit.jupiter.api.MethodOrderer;
+import org.junit.jupiter.api.Order;
 import org.junit.jupiter.api.Test;
+import org.junit.jupiter.api.TestMethodOrder;
 
 import de.buw.fm4se.smtsolving.Tasks;
 import de.buw.fm4se.smtsolving.utils.FmPlay;
 import de.buw.fm4se.smtsolving.utils.Z3Utils;
 
+@TestMethodOrder(MethodOrderer.OrderAnnotation.class)
 public class T1WhoKilledAgathaTest {
 
   String code = FmPlay.getCodeFromPermalink(Tasks.task_1);
 
   @Test
+  @Order(1)
   void testCheckFormula1() {
     String constraints = "(assert (not (exists ((x Person)) (killed x Agatha))))";
     assertTrue(Z3Utils.isUnsatForConstraints(code, constraints), "Encoding of formula 1 is wrong");
   }
 
   @Test
+  @Order(2)
   void testCheckFormula2() {
     String c1 = "(assert (not (forall ((x Person) (y Person))(=> (killed x y) (hates x y)))))";
     String c2 = "(assert (not (forall ((x Person) (y Person))(=> (killed x y) (not (richer x y))))))";
@@ -27,12 +33,14 @@ void testCheckFormula2() {
   }
 
   @Test
+  @Order(3)
   void testCheckFormula3() {
     String c1 = "(assert (not (forall ((x Person))(=> (hates Agatha x) (not (hates Charles x))))))";
     assertTrue(Z3Utils.isUnsatForConstraints(code, c1), "Encoding of formula 3 is wrong");
   }
 
   @Test
+  @Order(4)
   void testCheckFormula4() {
     String c1 = "(assert (not (hates Agatha Agatha)))";
     String c2 = "(assert (not (hates Agatha Charles)))";
@@ -41,24 +49,28 @@ void testCheckFormula4() {
   }
 
   @Test
+  @Order(5)
   void testCheckFormula5() {
     String constraints = "(assert (not (forall ((x Person))(=> (not (richer x Agatha)) (hates Butler x)))))";
     assertTrue(Z3Utils.isUnsatForConstraints(code, constraints), "Encoding of formula 5 is wrong");
   }
 
   @Test
+  @Order(6)
   void testCheckFormula6() {
     String constraints = "(assert (not (forall ((x Person))(=> (hates Agatha x) (hates Butler x)))))";
     assertTrue(Z3Utils.isUnsatForConstraints(code, constraints), "Encoding of formula 6 is wrong");
   }
 
   @Test
+  @Order(7)
   void testCheckFormula7() {
     String constraints = "(assert (not (forall ((x Person)) (exists ((y Person)) (not (hates x y))))))";
     assertTrue(Z3Utils.isUnsatForConstraints(code, constraints), "Encoding of formula 7 is wrong");
   }
 
   @Test
+  @Order(8)
   void testCheckConclusion() {
     String constraints = "(assert (killed Agatha Agatha))";
     assertFalse(Z3Utils.isUnsatForConstraints(code, constraints), "Conclusion is wrong");

src/test/java/de/buw/fm4se/smtsolving/tests/T2MathPuzzleTest.java

@@ -4,7 +4,10 @@
 
 import java.util.List;
 
+import org.junit.jupiter.api.MethodOrderer;
+import org.junit.jupiter.api.Order;
 import org.junit.jupiter.api.Test;
+import org.junit.jupiter.api.TestMethodOrder;
 
 import com.microsoft.z3.Z3Exception;
 
@@ -13,6 +16,7 @@
 import de.buw.fm4se.smtsolving.utils.PuzzleTest;
 import de.buw.fm4se.smtsolving.utils.Z3Utils;
 
+@TestMethodOrder(MethodOrderer.OrderAnnotation.class)
 public class T2MathPuzzleTest {
 
   String code = FmPlay.getCodeFromPermalink(Tasks.task_2);
@@ -21,21 +25,25 @@ public class T2MathPuzzleTest {
   List<String> smt = PuzzleTest.generateSmtAssert(puzzle);
 
   @Test
+  @Order(1)
   void testCheckFormula1() {
     testCheckFormula(0);
   }
 
   @Test
+  @Order(2)
   void testCheckFormula2() {
     testCheckFormula(1);
   }
 
   @Test
+  @Order(3)
   void testCheckFormula3() {
     testCheckFormula(2);
   }
 
   @Test
+  @Order(4)
   void testCheckFormula4() {
     testCheckFormula(3);
   }
@@ -50,9 +58,10 @@ private void testCheckFormula(int i) {
   }
 
   @Test
+  @Order(5)
   void testCheckConclusion() {
     try {
-      assertFalse(Z3Utils.isUnsatForConstraints(code, ""), "The puzzle has no solution");      
+      assertFalse(Z3Utils.isUnsatForConstraints(code, ""), "The puzzle has no solution");
     } catch (Z3Exception e) {
       fail("The encoding of the puzzle likely contains a syntax error");
     }

src/test/java/de/buw/fm4se/smtsolving/tests/T3PcConfigurationTest.java

@@ -1,13 +1,18 @@
 package de.buw.fm4se.smtsolving.tests;
+
 import static org.junit.jupiter.api.Assertions.assertFalse;
 import static org.junit.jupiter.api.Assertions.assertTrue;
 
+import org.junit.jupiter.api.MethodOrderer;
+import org.junit.jupiter.api.Order;
 import org.junit.jupiter.api.Test;
+import org.junit.jupiter.api.TestMethodOrder;
 
 import de.buw.fm4se.smtsolving.Tasks;
 import de.buw.fm4se.smtsolving.utils.FmPlay;
 import de.buw.fm4se.smtsolving.utils.Z3Utils;
 
+@TestMethodOrder(MethodOrderer.OrderAnnotation.class)
 public class T3PcConfigurationTest {
   // Office: 283
   // Server: 307
@@ -17,61 +22,66 @@ public class T3PcConfigurationTest {
   String code = FmPlay.getCodeFromPermalink(Tasks.task_3);
 
   @Test
-  void testPurposeOffice1(){
-    assertFalse(Z3Utils.isUnsatForConstraints(code, 
-              "(assert (= purpose office))\n(assert (= budget 283))"),
-              "For office purpose, €283 is enough, Check `(get-value (budget))`");
+  @Order(1)
+  void testPurposeOffice1() {
+    assertFalse(Z3Utils.isUnsatForConstraints(code,
+        "(assert (= purpose office))\n(assert (= budget 283))"),
+        "For office purpose, €283 is enough, Check `(get-value (budget))`");
   }
 
   @Test
-  void testPurposeOffice2(){
-    assertTrue(Z3Utils.isUnsatForConstraints(code, 
-              "(assert (= purpose office))\n(assert (= budget 282))"),
-              "For office purpose, the budget should be at least €283, Check `(get-value (budget))`");
+  @Order(2)
+  void testPurposeOffice2() {
+    assertTrue(Z3Utils.isUnsatForConstraints(code,
+        "(assert (= purpose office))\n(assert (= budget 282))"),
+        "For office purpose, the budget should be at least €283, Check `(get-value (budget))`");
   }
 
   @Test
-  void testPurposeServer1(){
-    assertFalse(Z3Utils.isUnsatForConstraints(code, 
-              "(assert (= purpose server))\n(assert (= budget 307))"),
-              "For server purpose, €307 is enough, Check `(get-value (budget))`");
+  @Order(3)
+  void testPurposeServer1() {
+    assertFalse(Z3Utils.isUnsatForConstraints(code,
+        "(assert (= purpose server))\n(assert (= budget 307))"),
+        "For server purpose, €307 is enough, Check `(get-value (budget))`");
   }
 
   @Test
-  void testPurposeServer2(){
-    assertTrue(Z3Utils.isUnsatForConstraints(code, 
-              "(assert (= purpose server))\n(assert (= budget 306))"),
-              "For server purpose, the budget should be at least €307, Check `(get-value (budget))`");
+  @Order(4)
+  void testPurposeServer2() {
+    assertTrue(Z3Utils.isUnsatForConstraints(code,
+        "(assert (= purpose server))\n(assert (= budget 306))"),
+        "For server purpose, the budget should be at least €307, Check `(get-value (budget))`");
   }
 
   @Test
-  void testPurposeGaming1(){
-    assertFalse(Z3Utils.isUnsatForConstraints(code, 
-              "(assert (= purpose gaming))\n(assert (= budget 1006))"),
-              "For gaming purpose, €1006 is enough, Check `(get-value (budget))`");
+  @Order(5)
+  void testPurposeGaming1() {
+    assertFalse(Z3Utils.isUnsatForConstraints(code,
+        "(assert (= purpose gaming))\n(assert (= budget 1006))"),
+        "For gaming purpose, €1006 is enough, Check `(get-value (budget))`");
   }
 
   @Test
-  void testPurposeGaming2(){
-    assertTrue(Z3Utils.isUnsatForConstraints(code, 
-              "(assert (= purpose gaming))\n(assert (= budget 1005))"),
-              "For gaming purpose, the budget should be at least €1006, Check `(get-value (budget))`");
+  @Order(6)
+  void testPurposeGaming2() {
+    assertTrue(Z3Utils.isUnsatForConstraints(code,
+        "(assert (= purpose gaming))\n(assert (= budget 1005))"),
+        "For gaming purpose, the budget should be at least €1006, Check `(get-value (budget))`");
   }
 
   @Test
-  void testPurposeVideoEditing1(){
-    assertFalse(Z3Utils.isUnsatForConstraints(code, 
-              "(assert (= purpose video))\n(assert (= budget 318))"),
-              "For video editing purpose, €318 is enough, Check `(get-value (budget))`");
+  @Order(7)
+  void testPurposeVideoEditing1() {
+    assertFalse(Z3Utils.isUnsatForConstraints(code,
+        "(assert (= purpose video))\n(assert (= budget 318))"),
+        "For video editing purpose, €318 is enough, Check `(get-value (budget))`");
   }
 
   @Test
-  void testPurposeVideoEditing2(){
-    assertTrue(Z3Utils.isUnsatForConstraints(code, 
-              "(assert (= purpose video))\n(assert (= budget 317))"),
-              "For video editing purpose, the budget should be at least €318, Check `(get-value (budget))`");
+  @Order(8)
+  void testPurposeVideoEditing2() {
+    assertTrue(Z3Utils.isUnsatForConstraints(code,
+        "(assert (= purpose video))\n(assert (= budget 317))"),
+        "For video editing purpose, the budget should be at least €318, Check `(get-value (budget))`");
   }
-
-
-
 }