From aeeb0b2ac50021c5c5ab37dbec9bcb5c4b98ce34 Mon Sep 17 00:00:00 2001
From: Daniel Szekeres <szekeresdani@gmail.com>
Date: Wed, 4 Dec 2024 22:29:28 +0100
Subject: [PATCH] re-added tracegen as a separate test method

---
 .../mit/theta/xcfa/cli/ThyssenXcfaDslTest.kt  | 46 ++++++++++++++++++-
 1 file changed, 45 insertions(+), 1 deletion(-)

diff --git a/subprojects/xcfa/xcfa-cli/src/test/java/hu/bme/mit/theta/xcfa/cli/ThyssenXcfaDslTest.kt b/subprojects/xcfa/xcfa-cli/src/test/java/hu/bme/mit/theta/xcfa/cli/ThyssenXcfaDslTest.kt
index df27e83128..adb420ba29 100644
--- a/subprojects/xcfa/xcfa-cli/src/test/java/hu/bme/mit/theta/xcfa/cli/ThyssenXcfaDslTest.kt
+++ b/subprojects/xcfa/xcfa-cli/src/test/java/hu/bme/mit/theta/xcfa/cli/ThyssenXcfaDslTest.kt
@@ -254,7 +254,7 @@ class ThyssenXcfaDslTest {
     }
 
     @Test
-    fun defineXcfa() {
+    fun checkXcfa() {
         LbePass.level = LbePass.LbeLevel.LBE_LOCAL
         val origXcfa = getXcfa()
         println(origXcfa.toDot())
@@ -318,4 +318,48 @@ class ThyssenXcfaDslTest {
         )
     }
 
+    @Test
+    fun tracegen() {
+        LbePass.level = LbePass.LbeLevel.LBE_LOCAL
+        val origXcfa = getXcfa()
+        val inputConfig =
+            InputConfig(
+                xcfaWCtx = Triple(origXcfa, listOf(), ParseContext()),
+                property = ErrorDetection.NO_ERROR,
+            )
+        val frontendConfig =
+            FrontendConfig(
+                lbeLevel = LbePass.level,
+                loopUnroll = LoopUnrollPass.UNROLL_LIMIT,
+                inputType = InputType.C,
+                specConfig = CFrontendConfig(arithmetic = efficient),
+            )
+        val backendConfig =
+            BackendConfig(
+                backend = Backend.TRACEGEN,
+                timeoutMs = 0,
+                specConfig =
+                TracegenConfig(
+                    abstractorConfig =
+                    CegarAbstractorConfig(
+                        abstractionSolver = "Z3",
+                        validateAbstractionSolver = false,
+                        domain = EXPL,
+                        maxEnum = 1,
+                        search = DFS,
+                    )
+                ),
+            )
+        val outputConfig =
+            OutputConfig(
+                enableOutput = true,
+                resultFolder = File("F:\\egyetem\\thesta\\theta\\subprojects\\xcfa\\xcfa\\src\\test\\temp"),
+            )
+        runConfig(
+            XcfaConfig(inputConfig, frontendConfig, backendConfig, outputConfig, DebugConfig()),
+            ConsoleLogger(Logger.Level.SUBSTEP),
+            ConsoleLogger(Logger.Level.SUBSTEP),
+            true,
+        )
+    }
 }
\ No newline at end of file