From 5f7419b08f7aa01c52a62238399fa25a0c7ba347 Mon Sep 17 00:00:00 2001
From: Armin Zavada <zavadaarmin@edu.bme.hu>
Date: Thu, 7 Nov 2024 13:09:07 +0100
Subject: [PATCH] #18 Added CexReader

---
 .../hu/bme/mit/semantifyr/cex/lang/Cex.xtext  | 10 ++-
 subprojects/semantifyr/build.gradle.kts       |  1 +
 .../src/main/kotlin/theta/CexReader.kt        | 77 +++++++++++++++++++
 3 files changed, 86 insertions(+), 2 deletions(-)
 create mode 100644 subprojects/semantifyr/src/main/kotlin/theta/CexReader.kt

diff --git a/subprojects/cex.lang/src/main/java/hu/bme/mit/semantifyr/cex/lang/Cex.xtext b/subprojects/cex.lang/src/main/java/hu/bme/mit/semantifyr/cex/lang/Cex.xtext
index 6002a15..62fe15c 100644
--- a/subprojects/cex.lang/src/main/java/hu/bme/mit/semantifyr/cex/lang/Cex.xtext
+++ b/subprojects/cex.lang/src/main/java/hu/bme/mit/semantifyr/cex/lang/Cex.xtext
@@ -11,13 +11,19 @@ generate cex "http://www.bme.hu/mit/2024/cex"
 import "http://www.eclipse.org/emf/2002/Ecore" as Ecore
 
 Cex:
-	"(" "XstsStateSequence"
+	"(" ("XstsStateSequence" | "XstsCliTracegen")
 	    (states += XstsState)*
+
+	    (edges += StateEdge)*
 	")"
 ;
 
+StateEdge:
+    from=[XstsState] "->" to=[XstsState]
+;
+
 XstsState:
-    "(" "XstsState" (preInit?="pre_init")? (lastEnv?="last_env")? (lastInternal?="last_internal")?
+    "(" (name=ID ":")? "XstsState" (preInit?="pre_init")? (lastEnv?="last_env")? (lastInternal?="last_internal")?
         state = State
     ")"
 ;
diff --git a/subprojects/semantifyr/build.gradle.kts b/subprojects/semantifyr/build.gradle.kts
index 077ccec..ebfa5b6 100644
--- a/subprojects/semantifyr/build.gradle.kts
+++ b/subprojects/semantifyr/build.gradle.kts
@@ -35,6 +35,7 @@ artifacts {
 
 dependencies {
     implementation(project(":oxsts.lang"))
+    implementation(project(":cex.lang"))
 
     implementation(libs.guice)
     implementation(libs.slf4j.api)
diff --git a/subprojects/semantifyr/src/main/kotlin/theta/CexReader.kt b/subprojects/semantifyr/src/main/kotlin/theta/CexReader.kt
new file mode 100644
index 0000000..1663384
--- /dev/null
+++ b/subprojects/semantifyr/src/main/kotlin/theta/CexReader.kt
@@ -0,0 +1,77 @@
+package hu.bme.mit.semantifyr.oxsts.semantifyr.theta
+
+import hu.bme.mit.semantifyr.cex.lang.CexStandaloneSetup
+import hu.bme.mit.semantifyr.cex.lang.cex.Cex
+import hu.bme.mit.semantifyr.oxsts.semantifyr.utils.error
+import hu.bme.mit.semantifyr.oxsts.semantifyr.utils.info
+import hu.bme.mit.semantifyr.oxsts.semantifyr.utils.loggerFactory
+import hu.bme.mit.semantifyr.oxsts.semantifyr.utils.warn
+import org.eclipse.emf.common.util.URI
+import org.eclipse.emf.ecore.resource.Resource
+import org.eclipse.emf.ecore.resource.impl.ResourceSetImpl
+import org.eclipse.xtext.diagnostics.Severity
+import org.eclipse.xtext.resource.XtextResource
+import org.eclipse.xtext.util.CancelIndicator
+import org.eclipse.xtext.validation.CheckMode
+import java.io.File
+
+fun prepareCex() {
+    CexStandaloneSetup.doSetup()
+}
+
+class CexReader {
+    val logger by loggerFactory()
+
+    val resourceSet = ResourceSetImpl()
+
+    init {
+        resourceSet.loadOptions[XtextResource.OPTION_ENCODING] = "UTF-8"
+    }
+
+    fun validateResource(resource: Resource) {
+        if (resource.errors.any()) {
+            logger.error { "Errors found in file (${resource.uri.toFileString()})" }
+
+            for (error in resource.errors) {
+                logger.error(error.message)
+            }
+
+            error("Errors found in file (${resource.uri.toFileString()})}")
+        }
+        if (resource.warnings.any()) {
+            logger.warn { "Warnings found in file (${resource.uri.toFileString()})" }
+
+            for (warning in resource.warnings) {
+                logger.warn(warning.message)
+            }
+        }
+        val validator = (resource as XtextResource).resourceServiceProvider.resourceValidator
+        val issues = validator.validate(resource, CheckMode.ALL, CancelIndicator.NullImpl)
+        if (issues.any()) {
+            logger.info { "Issues found in file (${resource.uri.toFileString()})" }
+
+            for (issue in issues) {
+                when (issue.severity) {
+                    Severity.INFO -> {
+                        logger.info { "${issue.uriToProblem.toFileString()}[${issue.lineNumber}:${issue.column}] ${issue.message}" }
+                    }
+                    Severity.WARNING -> {
+                        logger.warn { "${issue.uriToProblem.toFileString()}[${issue.lineNumber}:${issue.column}] ${issue.message}" }
+                    }
+                    Severity.ERROR -> {
+                        logger.error { "${issue.uriToProblem.toFileString()}[${issue.lineNumber}:${issue.column}] ${issue.message}" }
+                    }
+                    else -> { }
+                }
+            }
+        }
+    }
+
+    fun readCexFile(file: File): Cex {
+        val resource = resourceSet.getResource(URI.createFileURI(file.path), true)
+        resource.load(emptyMap<Any, Any>())
+        validateResource(resource)
+
+        return resource.contents.single() as Cex
+    }
+}