SW5 (#32)

.gitmodules

@@ -1,4 +1,4 @@
 [submodule "src/main/Ecdar-ProtoBuf"]
-	path = src/main/Ecdar-ProtoBuf
-	url = [email protected]:Ecdar/Ecdar-ProtoBuf.git
-    branch = futureproof1
+    path = src/main/Ecdar-ProtoBuf
+    url = [email protected]:Ecdar/Ecdar-ProtoBuf.git
+    branch = SW5

README.md

@@ -1,47 +1,31 @@
 # Ecdar-test
 The test framework for automatic test case generation for Ecdar engines.
 
-Requires a configuration file `configuration.json` with information for each engine executable: 
+Clone with `git clone --recurse-submodules https://github.com/Ecdar/Ecdar-Test.git` or if you have already cloned use `git submodule update --init --recursive`
+Runs on JDK 11 Temurin
+
+Requires a configuration file `configuration.json` with information for each engine executable: (Also see [full config](#full-configuration-file))
 ```json
 [
-    {
-        "name": "Reveaal",
-        "version": "Main",
-        "executablePath": "path/to/Reveaal.exe",
-        "parameterExpression" : "-p={ip}:{port}",
-        "ip": "127.0.0.1",
-        "port" : 7000,
-        "processes" : 8,
-        "enabled" : true,
-        "verbose": true,
-        "testTimeout": 30,
-        "testCount" : 4000,        
-        "testSorting": "Random",
-        "queryComplexity": [0, 1000],
-        "testsSavePath": "/path/to/file",
-        "gRPCSettings": {
-          "disable-clock-reduction": true
-        }
-    },
-    {
-        "name": "J-Ecdar",
-        "version": "UCDD",
-        "executablePath": "path/to/j-Ecdar.bat",
-        "parameterExpression" : "-p={ip}:{port}",
-        "ip": "127.0.0.1",
-        "port" : 8000,
-        "processes" : 8,
-        "enabled" : false
-    },
-    {
-        "name": "External",
-        "version": "v1.0",
-        "ip": "127.0.0.1",
-        "port" : 9000,
-        "processes" : 1,
-        "enabled" : false
+  {
+    "name": "Reveaal",
+    "version": "Main",
+    "executablePath": "path/to/Reveaal/target/release/reveaal",
+    "parameters" : ["serve","{ip}:{port}"],
+    "ip": "127.0.0.1",
+    "port" : 7000,
+    "processes" : 8,
+    "enabled" : true,
+    "verbose": true,
+    "testTimeout": 500,
+    "testCount" : 4000,
+    "testSorting": "Random",
+    "queryComplexity": [0, 1000],
+    "gRPCSettings": {
+      "disable-clock-reduction": true
     }
- ]
+  }
+]
 ```
 If an `executablePath` or `parameterExpression` is omitted, the engine is expected to be hosted externally. An example of this is the `External` engine in the above configuration. Engines can optionally be marked `verbose` to print failed queries while the tests are run from [Run Tests for Engine](#run-tests-for-engine)
 
@@ -62,7 +46,7 @@ If the array is empty, no bound is set.
 `testsSavePath` determines if and where in the filesystem to save the text-file with the queries being generated. If not set, the queries will not be saved on disk.
 `gRPCSettings` is the settings that are sent to the engine through gRPC. The settings can be found in the [protobuf](https://github.com/Ecdar/Ecdar-ProtoBuf).
 ## Run Tests for Engine
-Run all tests on enabled engines from `main()` in [Main.kt](src/main/kotlin/Main.kt). Test results are stored in `results/ENGINE_NAME/ENGINE_VERSION/RUN_NUMBER`. Run numbering is used so new results on same engine and version do not override previous results.
+Run all tests on enabled engines from `main()` in [Main.kt](src/main/kotlin/Main.kt) *(Click me in your IDE)*. Test results are stored in `results/ENGINE_NAME/ENGINE_VERSION/RUN_NUMBER`. Run numbering is used so new results on same engine and version do not override previous results.
 ```
 Found 5730 tests
 
@@ -94,3 +78,46 @@ Plots can optionally have log scale axes, as the ones seen below.
 ![Line Plot](https://i.imgur.com/dsKycFL.png "Line Plot")
 ### Density Plots
 ![Density Plot](https://i.imgur.com/PAl3BdX.png "Density Plot")
+
+### Full configuration file
+```json
+[
+    {
+        "name": "Reveaal",
+        "version": "Main",
+        "executablePath": "path/to/Reveaal.exe",
+        "parameters" : ["serve","{ip}:{port}"],
+        "ip": "127.0.0.1",
+        "port" : 7000,
+        "processes" : 8,
+        "enabled" : true,
+        "verbose": true,
+        "testTimeout": 30,
+        "testCount" : 4000,        
+        "testSorting": "Random",
+        "queryComplexity": [0, 1000],
+        "testsSavePath": "/path/to/file",
+        "gRPCSettings": {
+          "disable-clock-reduction": true
+        }
+    },
+    {
+        "name": "J-Ecdar",
+        "version": "UCDD",
+        "executablePath": "path/to/j-Ecdar.bat",
+        "parameters" : ["-p={ip}:{port}"],
+        "ip": "127.0.0.1",
+        "port" : 8000,
+        "processes" : 8,
+        "enabled" : false
+    },
+    {
+        "name": "External",
+        "version": "v1.0",
+        "ip": "127.0.0.1",
+        "port" : 9000,
+        "processes" : 1,
+        "enabled" : false
+    }
+ ]
+```

build.gradle

@@ -1,13 +1,12 @@
 buildscript {
-    ext.kotlin_version = '1.6.10'
+    ext.kotlin_version = '+'
 
     repositories {
         mavenCentral()
         maven {
             name 'JFrog OSS snapshot repo'
             url 'https://oss.jfrog.org/oss-snapshot-local/'
         }
-        jcenter()
     }
 
     dependencies {
@@ -28,36 +27,35 @@ apply plugin: 'antlr'
 repositories {
     mavenLocal()
     mavenCentral()
-    jcenter()
 }
 
 def grpcVersion = '1.52.1' // CURRENT_GRPC_VERSION
-def protobufVersion = '3.17.2'
+def protobufVersion = '3.17.3'
 def protocVersion = protobufVersion
 
 dependencies {
-    implementation 'org.junit.jupiter:junit-jupiter:5.7.0'
+    api 'org.junit.jupiter:junit-jupiter:5.7.0'
     antlr "org.antlr:antlr4:4.9.1"
-    implementation "org.antlr:antlr4-runtime:4.9.1"
-    implementation 'com.google.protobuf:protobuf-java:3.19.6'
-    implementation "org.jetbrains.kotlin:kotlin-stdlib:$kotlin_version"
-    implementation "org.jetbrains.kotlin:kotlin-reflect:$kotlin_version"
+    api "org.antlr:antlr4-runtime:4.9.1"
+    api 'com.google.protobuf:protobuf-java:3.19.6'
+    api "org.jetbrains.kotlin:kotlin-stdlib:$kotlin_version"
+    api "org.jetbrains.kotlin:kotlin-reflect:$kotlin_version"
     testImplementation "org.jetbrains.kotlin:kotlin-test:$kotlin_version"
     testImplementation 'junit:junit:4.13.1'
-    implementation 'com.beust:klaxon:5.5'
-    implementation "org.jetbrains.kotlinx:kotlinx-coroutines-core:1.5.2"
+    api 'com.beust:klaxon:5.5'
+    api "org.jetbrains.kotlinx:kotlinx-coroutines-core:1.5.2"
     //GRPC:
-    implementation "io.grpc:grpc-protobuf:$grpcVersion"
-    implementation "io.grpc:grpc-stub:$grpcVersion"
+    api "io.grpc:grpc-protobuf:$grpcVersion"
+    api "io.grpc:grpc-stub:$grpcVersion"
     compileOnly "org.apache.tomcat:annotations-api:6.0.53"
 
     // Plotting
-    implementation "org.jetbrains.lets-plot:lets-plot-kotlin-jvm:3.2.0"
-    implementation "org.slf4j:slf4j-simple:1.7.36"  // Enable logging to console
+    api "org.jetbrains.lets-plot:lets-plot-kotlin-jvm:3.2.0"
+    api "org.slf4j:slf4j-simple:1.7.36"  // Enable logging to console
 
 
     // examples/advanced need this for JsonFormat
-    implementation "com.google.protobuf:protobuf-java-util:$protobufVersion"
+    api "com.google.protobuf:protobuf-java-util:$protobufVersion"
 
     runtimeOnly "io.grpc:grpc-netty-shaded:$grpcVersion"
 

src/main/kotlin/Executor.kt

@@ -4,8 +4,10 @@ import EcdarProtoBuf.QueryProtos
 import EcdarProtoBuf.QueryProtos.QueryResponse.ResultCase
 import io.grpc.ManagedChannelBuilder
 import io.grpc.StatusRuntimeException
+import java.io.BufferedReader
 import java.io.File
 import java.io.IOException
+import java.io.InputStreamReader
 import java.net.ServerSocket
 import java.util.concurrent.ConcurrentLinkedQueue
 import java.util.concurrent.TimeUnit
@@ -27,7 +29,7 @@ class Executor(engine: EngineConfiguration, address: String, private var port: I
     private val settings: QueryProtos.QueryRequest.Settings = engine.settings
     private val verbose = engine.verbose ?: true
     private val path = engine.path!!
-    private var expr = engine.parameterExpression!!
+    private var params = engine.parameters!!
     private val ip = engine.ip
 
     init {
@@ -138,14 +140,36 @@ class Executor(engine: EngineConfiguration, address: String, private var port: I
         var p = port
         while (!isLocalPortFree(p)) p++
 
+        // Supports any way of defining ips and ports anywhere in the params. Now {ip}:{port} is
+        // just as valid as
+        // -p={ip}:{port} and they can be written in any order with other params such as a new
+        // -t(threads) flag in Reveaal
+        // or -i(input folder flag) in J-Ecdar
+        val currentParams =
+            Array(params.size) { params[it].replace("{ip}", ip).replace("{port}", p.toString()) }
+
         proc =
-            ProcessBuilder(path, expr.replace("{port}", p.toString()).replace("{ip}", ip))
+            ProcessBuilder(path, *currentParams)
                 // .redirectOutput(ProcessBuilder.Redirect.appendTo(File("Engine-$name-log.txt")))
-                .redirectOutput(ProcessBuilder.Redirect.DISCARD)
-                .redirectError(ProcessBuilder.Redirect.DISCARD)
+                .redirectErrorStream(
+                    true) // wanted to just get outputstream, however outputstream is empty until
+                // the
+                // process closes. So this would work fine on  "echo hello", but won't work on
+                // starting servers in JDK 11.
+                // Somehow redirecting the error output fixes the input stream
                 .directory(File(path).parentFile)
                 .start()
         port = p
+
+        val inputAndErrorStream =
+            proc?.inputStream ?: throw Exception("Process exited unexpectedly")
+        val reader = BufferedReader(InputStreamReader(inputAndErrorStream))
+        var output: String? = null
+
+        while (output == null) {
+            output = reader.readLine()
+        }
+        println(output) // example: "Started grpc server on '127.0.0.1:70XX'
     }
 
     private fun resetStub() {

src/main/kotlin/Main.kt

@@ -216,7 +216,7 @@ private fun saveResults(results: ResultContext) {
     path += "/$fileNumber.json"
     println("Saving results for engine '${results.engine}' in $path")
 
-    writeJsonToFile(path, results.results.map { it.result })
+    writeJsonToFile(path, results.results.toList())
 }
 
 private fun writeJsonToFile(filePath: String, results: Any) {

src/main/kotlin/TestResult.kt

@@ -40,7 +40,9 @@ enum class ResultType {
                 PARSING_ERROR,
                 MODEL,
                 ERROR,
+                COMPONENTSNOTINCACHE,
                 RESULT_NOT_SET -> UNSATISFIED
+                SYNTAX -> TODO()
             }
         }
     }

src/main/kotlin/parsing/EngineConfiguration.kt

@@ -15,7 +15,7 @@ data class EngineConfiguration(
     val name: String,
     val version: String,
     @Json(name = "executablePath", serializeNull = false) val path: String?,
-    @Json(serializeNull = false) val parameterExpression: String?,
+    @Json(serializeNull = false) val parameters: Array<String>?,
     val ip: String,
     val port: Int,
     @Json(serializeNull = false) val verbose: Boolean?,

src/main/kotlin/tests/SingleTestJsonAdapter.kt

@@ -0,0 +1,13 @@
+package tests
+
+import com.beust.klaxon.TypeAdapter
+import kotlin.reflect.KClass
+
+class SingleTestJsonAdapter : TypeAdapter<SingleTest> {
+    override fun classFor(type: Any): KClass<out SingleTest> =
+        when (type as String) {
+            "NotSatisfiedTest" -> NotSatisfiedTest::class
+            "SatisfiedTest" -> SatisfiedTest::class
+            else -> throw IllegalArgumentException("Unknown type: $type")
+        }
+}

src/main/kotlin/tests/Test.kt

@@ -2,6 +2,7 @@ package tests
 
 import EcdarProtoBuf.QueryProtos.QueryResponse.ResultCase
 import TestResult
+import com.beust.klaxon.TypeFor
 
 abstract class Test(val testSuite: String, val projectPath: String) {
     val type = this.javaClass.simpleName
@@ -20,6 +21,7 @@ abstract class Test(val testSuite: String, val projectPath: String) {
     }
 }
 
+@TypeFor(field = "type", adapter = SingleTestJsonAdapter::class)
 abstract class SingleTest(testSuite: String, projectPath: String, val query: String) :
     Test(testSuite, projectPath) {
     abstract fun getResult(success: Boolean): TestResult