bringing stvs into verifaps

VerifAPS · Mar 23, 2024 · e94ee82 · e94ee82
1 parent 85dd8d2
commit e94ee82
Show file tree

Hide file tree

Showing 31 changed files with 111 additions and 2,239 deletions.
diff --git a/build.gradle b/build.gradle
@@ -1,9 +1,8 @@
 import java.text.SimpleDateFormat
 
 plugins {
-    id "org.jetbrains.kotlin.jvm" version "2.0.0-Beta4" apply false
+    id "org.jetbrains.kotlin.jvm" version "1.9.23" apply false
     id("org.jetbrains.dokka") version "1.9.20"
-    id "org.sonarqube" version "4.4.1.3373"
     id "com.github.ben-manes.versions" version "0.51.0"
 }
 
@@ -28,16 +27,6 @@ allprojects {
         mavenCentral()
         jcenter()
     }
-
-    sonarqube {
-        properties {
-            property "sonar.coverage.jacoco.xmlReportPaths", "build/reports/jacoco/test/jacocoTestReport.xml"
-            property "sonar.exclusions", "*/build/generated-src/antlr/**"
-            property "sonar.c.file.suffixes", "-"
-            property "sonar.cpp.file.suffixes", "-"
-            property "sonar.objc.file.suffixes", "-"
-        }
-    }
 }
 
 subprojects {
@@ -49,7 +38,7 @@ subprojects {
     apply plugin: 'maven-publish'
     apply plugin: 'jacoco'
 
-    ext.kotlin_version = '2.0.0-Beta4'
+    ext.kotlin_version = '2.0.0-Beta5'
 
     sourceCompatibility = 21
     targetCompatibility = 21

diff --git a/geteta/src/main/kotlin/edu/kit/iti/formal/automation/testtables/GetetaFacade.kt b/geteta/src/main/kotlin/edu/kit/iti/formal/automation/testtables/GetetaFacade.kt
@@ -40,7 +40,7 @@ import java.io.StringWriter
 
 const val TABLE_SEP = "_"
 
-object GetetaFacade {
+public object GetetaFacade {
     fun createParser(input: CharStream): TestTableLanguageParser {
         val lexer = TestTableLanguageLexer(input)
         val parser = TestTableLanguageParser(CommonTokenStream(lexer))
@@ -151,6 +151,7 @@ object GetetaFacade {
         return ttlb.testTables
     }
 
+    @JvmStatic
     fun exprsToSMV(vc: ParseContext,
                    constraints: Map<ColumnVariable, TestTableLanguageParser.CellContext>)
             : Map<String, SMVExpr> = constraints.map { (t, u) ->
@@ -163,21 +164,25 @@ object GetetaFacade {
     }.toMap()
 
 
+    @JvmStatic
     fun getHistoryName(variable: SVariable, cycles: Int): String {
         return getHistoryName(variable) + "._$" + cycles
     }
 
+    @JvmStatic
     fun getHistoryName(variable: SVariable): String {
         return variable.name + "__history"
     }
 
+    @JvmStatic
     fun runNuXMV(nuXmvPath: String, folder: String,
                  modules: List<SMVModule>,
                  vt: VerificationTechnique): NuXMVOutput {
         val adapter = createNuXMVProcess(folder, modules, nuXmvPath, vt)
         return adapter.call()
     }
 
+    @JvmStatic
     fun createNuXMVProcess(folder: String, modules: List<SMVModule>,
                            nuXmvPath: String, vt: VerificationTechnique): NuXMVProcess {
         val outputFolder = File(folder)
@@ -196,6 +201,7 @@ object GetetaFacade {
         return adapter
     }
 
+    @JvmStatic
     fun createSuperEnum(scopes: List<Scope>): EnumType {
         val allowedValues =
                 scopes.flatMap { scope ->
@@ -207,6 +213,7 @@ object GetetaFacade {
         return EnumType(allowedValues)
     }
 
+    @JvmStatic
     fun generateInterface(name: String = "anonym",
                           scope: Scope = Scope.defaultScope(),
                           includeState: Boolean = true): String {
@@ -234,47 +241,56 @@ object GetetaFacade {
         return s.toString()
     }
 
+    @JvmStatic
     fun readTables(file: File, timeConstants: Map<String, Int> = hashMapOf()): List<GeneralizedTestTable> {
         return parseTableDSL(file, timeConstants)
     }
 
+    @JvmStatic
     fun constructTable(table: GeneralizedTestTable) =
             AutomatonBuilderPipeline(table).transform()
 
+    @JvmStatic
     fun constructSMV(table: GeneralizedTestTable, superEnum: EnumType) =
             constructSMV(constructTable(table), superEnum)
 
+    @JvmStatic
     fun constructSMV(automaton: AutomataTransformerState, superEnum: EnumType) =
             SmvConstructionPipeline(automaton, superEnum).transform()
 
+    @JvmStatic
     fun analyzeCounterExample(automaton: TestTableAutomaton, testTable: GeneralizedTestTable, counterExample: CounterExample): MutableList<Mapping> {
         val analyzer = CounterExampleAnalyzer(automaton, testTable, counterExample,
                 "_${testTable.name}")
         analyzer.run()
         return analyzer.rowMapping
     }
 
+    @JvmStatic
     fun print(gtt: GeneralizedTestTable): String {
         val stream = StringWriter()
         val p = DSLTablePrinter(CodeWriter(stream))
         p.print(gtt)
         return stream.toString()
     }
 
+    @JvmStatic
     fun functionToSmv(fd: FunctionDeclaration): SmvFunctionDefinition {
         val parameters = fd.scope.variables.filter { it.isInput }
                 .map { DefaultTypeTranslator.INSTANCE.translate(it) }
         val body = SymbExFacade.evaluateFunction(fd, parameters)
         return SmvFunctionDefinition(body, parameters)
     }
 
+    @JvmStatic
     fun exprToSmv(expr: TestTableLanguageParser.ExprContext, parseContext: ParseContext): SMVExpr {
         val dummy = SVariable("dummy", SMVTypes.BOOLEAN)
         val visitor = TblLanguageToSmv(dummy, 0, parseContext)
         return expr.accept(visitor)
     }
 
 
+    @JvmStatic
     fun meshTables(tables: List<SMVConstructionModel>): TestTableAutomaton {
         val automaton = TestTableAutomaton()
         automaton.stateError = tables.first().automaton.stateError
@@ -357,6 +373,7 @@ object GetetaFacade {
      *
      * Useful for meshed gtts where a common signature is needed during the SMV construction.
      */
+    @JvmStatic
     fun createMeshedDummy(gtts: List<GeneralizedTestTable>): GeneralizedTestTable {
         val gtt = GeneralizedTestTable("__meshed__")
         gtt.programRuns = gtts.first().programRuns

diff --git a/gradle/wrapper/gradle-wrapper.jar b/gradle/wrapper/gradle-wrapper.jar
diff --git a/gradle/wrapper/gradle-wrapper.properties b/gradle/wrapper/gradle-wrapper.properties
@@ -1,6 +1,6 @@
 distributionBase=GRADLE_USER_HOME
 distributionPath=wrapper/dists
-distributionUrl=https\://services.gradle.org/distributions/gradle-8.4-bin.zip
+distributionUrl=https\://services.gradle.org/distributions/gradle-8.6-bin.zip
 networkTimeout=10000
 validateDistributionUrl=true
 zipStoreBase=GRADLE_USER_HOME

diff --git a/gradlew.bat b/gradlew.bat
@@ -43,11 +43,11 @@ set JAVA_EXE=java.exe
 %JAVA_EXE% -version >NUL 2>&1
 if %ERRORLEVEL% equ 0 goto execute
 
-echo.
-echo ERROR: JAVA_HOME is not set and no 'java' command could be found in your PATH.
-echo.
-echo Please set the JAVA_HOME variable in your environment to match the
-echo location of your Java installation.
+echo. 1>&2
+echo ERROR: JAVA_HOME is not set and no 'java' command could be found in your PATH. 1>&2
+echo. 1>&2
+echo Please set the JAVA_HOME variable in your environment to match the 1>&2
+echo location of your Java installation. 1>&2
 
 goto fail
 
@@ -57,11 +57,11 @@ set JAVA_EXE=%JAVA_HOME%/bin/java.exe
 
 if exist "%JAVA_EXE%" goto execute
 
-echo.
-echo ERROR: JAVA_HOME is set to an invalid directory: %JAVA_HOME%
-echo.
-echo Please set the JAVA_HOME variable in your environment to match the
-echo location of your Java installation.
+echo. 1>&2
+echo ERROR: JAVA_HOME is set to an invalid directory: %JAVA_HOME% 1>&2
+echo. 1>&2
+echo Please set the JAVA_HOME variable in your environment to match the 1>&2
+echo location of your Java installation. 1>&2
 
 goto fail
 

diff --git a/settings.gradle b/settings.gradle
@@ -12,6 +12,7 @@ include ':exec'
 include ':geteta'
 include ':smt'
 include 'absintsfc'
+include 'stvs'
 
 //include ':web-backend'
 //include 'asdl'
diff --git a/stvs/build.gradle b/stvs/build.gradle
@@ -1,34 +1,19 @@
-/*
- * This build file was auto generated by running the Gradle 'init' task
- * by 'Philipp' at '08.11.16 16:32' with Gradle 3.1
- *
- * This generated file contains a sample Java project to get you started.
- * For more details take a look at the Java Quickstart chapter in the Gradle
- * user guide available at https://docs.gradle.org/3.1/userguide/tutorial_java_projects.html
- */
-
 plugins {
-    id 'com.github.jacobono.jaxb' version '1.3.5'
-    id 'com.github.kt3k.coveralls' version '2.8.2'
-    id 'net.saliman.cobertura' version '2.3.1'
-
+    //id 'com.github.jacobono.jaxb' version '1.3.5'
+    //id 'com.github.kt3k.coveralls' version '2.8.2'
+    //id 'net.saliman.cobertura' version '2.3.1'
+    id("application")
+    id("antlr")
+    id 'org.openjfx.javafxplugin' version '0.1.0'
 }
 
-apply plugin: 'application'
-apply plugin: 'antlr'
-
-group = "edu.kit.iti.formal"
 version = "1.4.0-beta"
 
-compileJava.options.encoding = 'UTF-8'
-compileJava.dependsOn(xjc)
-
 sourceSets {
     main {
         java {
             srcDirs = [
                     'src/main/java',
-                    'build/generated-src/jaxb',
                     'build/generated-src/antlr/main'
             ]
         }
@@ -40,49 +25,40 @@ javadoc {
     options.charSet = 'UTF-8'
 }
 
-// In this section you declare where to find the dependencies of your project
-repositories {
-    // Use 'jcenter' for resolving your dependencies.
-    // You can declare any Maven/Ivy/file repository here.
-    jcenter()
-    mavenCentral()
-    maven {
-        url "http://formal.iti.kit.edu/maven2/"
-    }
-    //mavenLocal()
+javafx {
+    version = "21"
+    modules = ["javafx.controls", "javafx.controls", "javafx.fxml", "javafx.graphics", "javafx.web"]
 }
+
 dependencies {
-    compile 'org.apache.commons:commons-collections4:4.0'
-    compile 'de.tu-dresden.inf.lat.jsexp:jsexp:0.2.2'
-    compile 'org.apache.commons:commons-lang3:3.1'
-    compile 'commons-io:commons-io:2.5'
-    compile 'com.google.code.gson:gson:2.8.0'
-    compile 'org.fxmisc.richtext:richtextfx:0.6.10'
-    compile 'org.antlr:antlr4-runtime:4.7'
-    compile 'edu.kit.iti.formal:iec61131lang:0.1.15-SNAPSHOT'
-    compile group: 'de.jensd', name: 'fontawesomefx', version: '8.9'
-    compile group: 'com.sun.xml.bind', name: 'jaxb-impl', version: '2.2.3-1'
-    compile 'org.slf4j:slf4j-jdk14:1.8.0-alpha2'
+    implementation project(':lang')
+    implementation project(':geteta')
+
+
+    implementation 'org.apache.commons:commons-collections4:4.4'
+    implementation 'de.tu-dresden.inf.lat.jsexp:jsexp:0.2.2'
+    implementation 'org.apache.commons:commons-lang3:3.1'
+    implementation 'commons-io:commons-io:2.9.0'
+    implementation 'com.google.code.gson:gson:2.9.1'
+    implementation 'org.fxmisc.richtext:richtextfx:0.6.10'
+    implementation 'org.antlr:antlr4-runtime:4.7'
+    implementation group: 'de.jensd', name: 'fontawesomefx', version: '8.9'
+    implementation 'org.slf4j:slf4j-jdk14:1.8.0-alpha2'
 
-    compile 'org.fxmisc.cssfx:cssfx:1.0.0'
+    implementation 'org.fxmisc.cssfx:cssfx:1.0.0'
 
-    compile 'org.controlsfx:controlsfx:8.40.13'
+    implementation 'org.controlsfx:controlsfx:8.40.13'
 
-    testCompile "junit:junit:4.12"
+    testImplementation 'junit:junit:4.13.2'
 
     antlr 'org.antlr:antlr4:4.7'
 
-    jaxb 'com.sun.xml.bind:jaxb-xjc:2.2.7-b41'
-    jaxb 'com.sun.xml.bind:jaxb-impl:2.2.7-b41'
-    jaxb 'javax.xml.bind:jaxb-api:2.2.7'
-
-    testCompile "junit:junit:4.12"
-    testCompile group: 'com.googlecode.junit-toolbox', name: 'junit-toolbox', version: '2.2'
-    testCompile "org.testfx:testfx-core:4.0.+"
-    testCompile "org.testfx:testfx-junit:4.0.+"
-    testCompile "org.mockito:mockito-core:2.4.0"
-    testCompile group: 'org.powermock', name: 'powermock-module-junit4', version: '1.7.0RC2'
-    testCompile group: 'org.powermock', name: 'powermock-api-mockito2', version: '1.7.0RC2'
+    testImplementation group: 'com.googlecode.junit-toolbox', name: 'junit-toolbox', version: '2.2'
+    testImplementation "org.testfx:testfx-core:4.0.+"
+    testImplementation "org.testfx:testfx-junit:4.0.+"
+    testImplementation "org.mockito:mockito-core:2.4.0"
+    testImplementation group: 'org.powermock', name: 'powermock-module-junit4', version: '1.7.0RC2'
+    testImplementation group: 'org.powermock', name: 'powermock-api-mockito2', version: '1.7.0RC2'
 }
 
 System.setProperty('javax.xml.accessExternalSchema', 'file')
@@ -96,13 +72,13 @@ def getVersionName = { ->
     return stdout.toString().trim()
 }
 
-jaxb {
+/*jaxb {
     xjc {
         xsdDir "src/main/resources/fileFormats/"
         destinationDir "build/generated-src/jaxb/"
         args = ["-encoding", "UTF-8"]
     }
-}
+}*/
 
 generateGrammarSource {
     maxHeapSize = "64m"
@@ -118,25 +94,6 @@ ext.sharedManifest = manifest {
             "Main-Class": mainClassName)
 }
 
-jar {
-    manifest = project.manifest {
-        from sharedManifest
-        attributes(
-                'Class-Path': configurations.compile.collect {
-                    it.getName()
-                }.join(' '))
-    }
-}
-
-task fatJar(type: Jar) {
-    manifest = project.manifest { from sharedManifest }
-    baseName = project.name + '-all'
-    from {
-        configurations.compile.collect { it.isDirectory() ? it : zipTree(it) }
-    }
-    with jar
-}
-
 test {
     filter {
         includeTestsMatching "edu.kit.iti.formal.stvs.model.*"
@@ -170,4 +127,4 @@ task guiTest(type: Test) {
 }
 
 // coverage
-cobertura.coverageFormats = ['html', 'xml'] // coveralls plugin depends on xml format report
+//cobertura.coverageFormats = ['html', 'xml'] // coveralls plugin depends on xml format report
diff --git a/stvs/gradle/wrapper/gradle-wrapper.jar b/stvs/gradle/wrapper/gradle-wrapper.jar
diff --git a/stvs/gradle/wrapper/gradle-wrapper.properties b/stvs/gradle/wrapper/gradle-wrapper.properties