Added GitHub actions CI

.github/workflows/gradle.yml

@@ -0,0 +1,52 @@
+name: Continous Integration
+on:
+  push:
+    branches: [ "main" ]
+  pull_request:
+    branches: [ "main" ]
+jobs:
+  build:
+    runs-on: ubuntu-latest
+    permissions:
+      contents: read
+    steps:
+    - uses: actions/checkout@v4
+
+    - name: Set up JDK 17
+      uses: actions/setup-java@v4
+      with:
+        java-version: '17'
+        distribution: 'temurin'
+
+    - name: Setup Gradle
+      uses: gradle/actions/setup-gradle@417ae3ccd767c252f5661f1ace9f835f9654f2b5 # v3.1.0
+
+    - name: Prepare script
+      run: chmod +x ./gradlew
+
+    - name: Build with Gradle Wrapper
+      run: ./gradlew build
+
+    - name: Store reports
+      uses: actions/upload-artifact@v3
+      with:
+        name: reports
+        path: |
+          **/build/reports/
+          **/build/test-results/
+
+  dependency-submission:
+    runs-on: ubuntu-latest
+    permissions:
+      contents: write
+    steps:
+    - uses: actions/checkout@v4
+
+    - name: Set up JDK 17
+      uses: actions/setup-java@v4
+      with:
+        java-version: '17'
+        distribution: 'temurin'
+
+    - name: Generate and submit dependency graph
+      uses: gradle/actions/dependency-submission@417ae3ccd767c252f5661f1ace9f835f9654f2b5 # v3.1.0

buildSrc/src/main/kotlin/hu/bme/mit/semantifyr/gradle/conventions/jvm.gradle.kts

@@ -44,6 +44,7 @@ tasks {
 
         minHeapSize = "512m"
         maxHeapSize = "4G"
+        testLogging.showStandardStreams = true
 
         finalizedBy(tasks.jacocoTestReport)
     }
@@ -53,6 +54,7 @@ tasks {
 
         minHeapSize = "512m"
         maxHeapSize = "4G"
+        testLogging.showStandardStreams = true
 
         finalizedBy(tasks.jacocoTestReport)
     }

engine/build.gradle.kts

@@ -28,10 +28,21 @@ val downloadTheta = tasks.create<Exec>("downloadTheta") {
     }
 }
 
+fun Test.addToVariable(key: String, value: String) {
+    val pathSeparator = File.pathSeparator
+    val old = environment[key]?.toString() ?: ""
+    val newValue = if (old.isBlank()) value else "$old$pathSeparator$value"
+    environment(key, newValue)
+}
+
 tasks.withType(Test::class.java) {
     inputs.dir("Test Models")
 
-    environment("PATH", layout.projectDirectory.dir("theta"))
+
+    val thetaDir = layout.projectDirectory.dir("theta").toString()
+
+    addToVariable("LD_LIBRARY_PATH", thetaDir)
+    addToVariable("PATH", thetaDir)
 
     dependsOn(downloadTheta)
 }

engine/src/main/kotlin/reader/OxstsReader.kt

@@ -73,9 +73,9 @@ class OxstsReader(
             }
             val validator = (resource as XtextResource).resourceServiceProvider.resourceValidator
             val issues = validator.validate(resource, CheckMode.ALL, CancelIndicator.NullImpl)
-            for (issue in issues) {
+            if (issues.any()) {
                 println("Issues found in file (${resource.uri.toFileString()}):")
-                println("${issue.severity} - ${issue.message}")
+                error("Issues found in file (${resource.uri.toFileString()}):\n${issues.joinToString("\n")}")
             }
         }
 

engine/src/testFixtures/kotlin/VerificationTest.kt

@@ -70,7 +70,16 @@ open class VerificationTest {
         val propertyPath = "$targetDirectory/$targetName.prop"
         val tracePath = "$targetDirectory/$targetName.cex"
 
-        executeTheta(modelPath, propertyPath, tracePath)
+        println("Executing theta on $modelPath")
+
+        try {
+            executeTheta(modelPath, propertyPath, tracePath)
+        } catch (e: Exception) {
+            e.printStackTrace()
+            throw e
+        }
+
+        println("Checking results of Theta")
 
         if (targetName.contains("Unsafe")) {
             Assertions.assertTrue(File(tracePath).exists(), "$targetName failed!")

oxsts.lang/build.gradle.kts

@@ -30,6 +30,10 @@ val syncModel by tasks.registering(Sync::class) {
 val generateXtextLanguage by tasks.registering(JavaExec::class) {
     dependsOn(syncModel)
 
+    doFirst {
+        mkdir(parent!!.layout.projectDirectory.dir("oxsts.lang.ide"))
+    }
+
     mainClass.set("org.eclipse.emf.mwe2.launch.runtime.Mwe2Launcher")
     classpath(configurations.mwe2)
 

oxsts.lang/src/main/java/hu/bme/mit/semantifyr/oxsts/lang/validation/OxstsValidator.java

@@ -24,8 +24,29 @@ public class OxstsValidator extends AbstractOxstsValidator {
     public void checkFeatureSubsetting(Feature feature) {
         if (feature.getSubsets().isEmpty()) return;
 
-        var featureType = getType(feature.getTyping());
-        var subsettingType = getType(feature.getSubsets().stream().findFirst().get().getTyping());
+        var featureTyping = feature.getTyping();
+        var subsettingTyping = feature.getSubsets().stream().findFirst().get().getTyping();
+
+        if (featureTyping instanceof IntegerType) {
+            if (!(subsettingTyping instanceof IntegerType)) {
+                error("Feature must have type that is compatible with subsetted feature",
+                        OxstsPackage.Literals.FEATURE__SUBSETS,
+                        INVALID_TYPE);
+            } else {
+                return;
+            }
+        } else if (featureTyping instanceof BooleanType) {
+            if (!(subsettingTyping instanceof BooleanType)) {
+                error("Feature must have type that is compatible with subsetted feature",
+                        OxstsPackage.Literals.FEATURE__SUBSETS,
+                        INVALID_TYPE);
+            } else {
+                return;
+            }
+        }
+
+        var featureType = getType(featureTyping);
+        var subsettingType = getType(subsettingTyping);
 
         if (!isSupertypeOf(subsettingType, featureType)) {
             error("Feature must have type that is compatible with subsetted feature",
@@ -38,12 +59,33 @@ public void checkFeatureSubsetting(Feature feature) {
     public void checkFeatureRedefinition(Feature feature) {
         if (feature.getRedefines() == null) return;
 
-        var featureType = getType(feature.getTyping());
-        var redefinedType = getType(feature.getRedefines().getTyping());
+        var featureTyping = feature.getTyping();
+        var redefinedTyping = feature.getRedefines().getTyping();
+
+        if (featureTyping instanceof IntegerType) {
+            if (!(redefinedTyping instanceof IntegerType)) {
+                error("Feature must have type that is compatible with redefined feature",
+                        OxstsPackage.Literals.FEATURE__SUBSETS,
+                        INVALID_TYPE);
+            } else {
+                return;
+            }
+        } else if (featureTyping instanceof BooleanType) {
+            if (!(redefinedTyping instanceof BooleanType)) {
+                error("Feature must have type that is compatible with redefined feature",
+                        OxstsPackage.Literals.FEATURE__SUBSETS,
+                        INVALID_TYPE);
+            } else {
+                return;
+            }
+        }
+
+        var featureType = getType(featureTyping);
+        var redefinedType = getType(redefinedTyping);
 
         if (!isSupertypeOf(redefinedType, featureType)) {
             error("Feature must have type that is compatible with redefined feature",
-					OxstsPackage.Literals.FEATURE__SUBSETS,
+                    OxstsPackage.Literals.FEATURE__SUBSETS,
                     INVALID_TYPE);
         }
     }