From 8f2062162dc628d4c73849db23b95c9695736ccb Mon Sep 17 00:00:00 2001 From: Thomas Lohse <49527735+t-lohse@users.noreply.github.com> Date: Mon, 12 Feb 2024 09:58:22 +0100 Subject: [PATCH 1/4] SW5 (#32) * Update .gitmodules * change config to take an array of args, replace 2nd arg with ip and port. Also improved README.md * renamed parameterExpression -> parameters Fixed so that {ip} and {port} can be used anywhere in parameters * Protobuf submodule pointer update (#1) * Updated protobuf submodule pointer * Fixed dependency and result type error * Fixed Results.kt and Plotting.kt --------- Co-authored-by: Aavild <46568674+Aavild@users.noreply.github.com> Co-authored-by: aavild Co-authored-by: William Woldum <41169797+williamwoldum@users.noreply.github.com> --- .gitmodules | 3 +- README.md | 105 +++++++++++------- build.gradle | 2 +- src/main/Ecdar-ProtoBuf | 2 +- src/main/kotlin/Executor.kt | 37 ++++-- src/main/kotlin/Main.kt | 2 +- src/main/kotlin/TestResult.kt | 1 + .../kotlin/parsing/EngineConfiguration.kt | 2 +- .../kotlin/tests/SingleTestJsonAdapter.kt | 12 ++ src/main/kotlin/tests/Test.kt | 2 + 10 files changed, 115 insertions(+), 53 deletions(-) create mode 100644 src/main/kotlin/tests/SingleTestJsonAdapter.kt diff --git a/.gitmodules b/.gitmodules index a42b21e..d6d642d 100644 --- a/.gitmodules +++ b/.gitmodules @@ -1,4 +1,3 @@ [submodule "src/main/Ecdar-ProtoBuf"] path = src/main/Ecdar-ProtoBuf - url = git@github.com:Ecdar/Ecdar-ProtoBuf.git - branch = futureproof1 + url = https://github.com/ECDAR-AAU-SW-P5/Ecdar-ProtoBuf.git diff --git a/README.md b/README.md index 339d5ec..a46cb69 100644 --- a/README.md +++ b/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 + } + ] +``` \ No newline at end of file diff --git a/build.gradle b/build.gradle index 856612c..10773c3 100644 --- a/build.gradle +++ b/build.gradle @@ -32,7 +32,7 @@ repositories { } def grpcVersion = '1.52.1' // CURRENT_GRPC_VERSION -def protobufVersion = '3.17.2' +def protobufVersion = '3.17.3' def protocVersion = protobufVersion dependencies { diff --git a/src/main/Ecdar-ProtoBuf b/src/main/Ecdar-ProtoBuf index ae8364e..0997267 160000 --- a/src/main/Ecdar-ProtoBuf +++ b/src/main/Ecdar-ProtoBuf @@ -1 +1 @@ -Subproject commit ae8364e6c8942a5cfde24adec779ca87d4431e4a +Subproject commit 0997267c1efefe96b384ee7f619c3d84a6cd4b38 diff --git a/src/main/kotlin/Executor.kt b/src/main/kotlin/Executor.kt index 180f8c1..72b913a 100644 --- a/src/main/kotlin/Executor.kt +++ b/src/main/kotlin/Executor.kt @@ -4,16 +4,19 @@ import EcdarProtoBuf.QueryProtos import EcdarProtoBuf.QueryProtos.QueryResponse.ResultCase import io.grpc.ManagedChannelBuilder import io.grpc.StatusRuntimeException +import parsing.EngineConfiguration +import tests.MultiTest +import tests.SingleTest +import tests.Test +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 import java.util.concurrent.atomic.AtomicInteger -import parsing.EngineConfiguration -import tests.MultiTest -import tests.SingleTest -import tests.Test + class Executor(engine: EngineConfiguration, address: String, private var port: Int) { val name = engine.name @@ -27,7 +30,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 +141,32 @@ 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() { diff --git a/src/main/kotlin/Main.kt b/src/main/kotlin/Main.kt index c2161bc..ffa55f5 100644 --- a/src/main/kotlin/Main.kt +++ b/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) { diff --git a/src/main/kotlin/TestResult.kt b/src/main/kotlin/TestResult.kt index 1ccef7f..b86d3e6 100644 --- a/src/main/kotlin/TestResult.kt +++ b/src/main/kotlin/TestResult.kt @@ -40,6 +40,7 @@ enum class ResultType { PARSING_ERROR, MODEL, ERROR, + COMPONENTSNOTINCACHE, RESULT_NOT_SET -> UNSATISFIED } } diff --git a/src/main/kotlin/parsing/EngineConfiguration.kt b/src/main/kotlin/parsing/EngineConfiguration.kt index 695f672..249834b 100644 --- a/src/main/kotlin/parsing/EngineConfiguration.kt +++ b/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?, val ip: String, val port: Int, @Json(serializeNull = false) val verbose: Boolean?, diff --git a/src/main/kotlin/tests/SingleTestJsonAdapter.kt b/src/main/kotlin/tests/SingleTestJsonAdapter.kt new file mode 100644 index 0000000..52317e5 --- /dev/null +++ b/src/main/kotlin/tests/SingleTestJsonAdapter.kt @@ -0,0 +1,12 @@ +package tests + +import com.beust.klaxon.TypeAdapter +import kotlin.reflect.KClass + +class SingleTestJsonAdapter: TypeAdapter { + override fun classFor(type: Any): KClass = when(type as String) { + "NotSatisfiedTest" -> NotSatisfiedTest::class + "SatisfiedTest" -> SatisfiedTest::class + else -> throw IllegalArgumentException("Unknown type: $type") + } +} \ No newline at end of file diff --git a/src/main/kotlin/tests/Test.kt b/src/main/kotlin/tests/Test.kt index 541209f..aa5ca98 100644 --- a/src/main/kotlin/tests/Test.kt +++ b/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 From f8111a661efe66c9d9d63f0dd688e55ef5c69bf1 Mon Sep 17 00:00:00 2001 From: Thomas Lohse Date: Mon, 12 Feb 2024 15:42:37 +0100 Subject: [PATCH 2/4] upd submodule --- .gitmodules | 3 ++- src/main/Ecdar-ProtoBuf | 2 +- 2 files changed, 3 insertions(+), 2 deletions(-) diff --git a/.gitmodules b/.gitmodules index d6d642d..c1fbb05 100644 --- a/.gitmodules +++ b/.gitmodules @@ -1,3 +1,4 @@ [submodule "src/main/Ecdar-ProtoBuf"] path = src/main/Ecdar-ProtoBuf - url = https://github.com/ECDAR-AAU-SW-P5/Ecdar-ProtoBuf.git + url = git@github.com:Ecdar/Ecdar-ProtoBuf.git + branch = SW5 diff --git a/src/main/Ecdar-ProtoBuf b/src/main/Ecdar-ProtoBuf index 0997267..f5ae959 160000 --- a/src/main/Ecdar-ProtoBuf +++ b/src/main/Ecdar-ProtoBuf @@ -1 +1 @@ -Subproject commit 0997267c1efefe96b384ee7f619c3d84a6cd4b38 +Subproject commit f5ae9598ebd6de74e17a7a03ae1b0896ae322ef7 From d3b1fee5fd6a3db870fffd20e7ce88da9b68925c Mon Sep 17 00:00:00 2001 From: Thomas Lohse Date: Mon, 12 Feb 2024 15:43:12 +0100 Subject: [PATCH 3/4] upd submodule --- .gitmodules | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/.gitmodules b/.gitmodules index c1fbb05..c29fe1f 100644 --- a/.gitmodules +++ b/.gitmodules @@ -1,4 +1,4 @@ [submodule "src/main/Ecdar-ProtoBuf"] - path = src/main/Ecdar-ProtoBuf - url = git@github.com:Ecdar/Ecdar-ProtoBuf.git + path = src/main/Ecdar-ProtoBuf + url = git@github.com:Ecdar/Ecdar-ProtoBuf.git branch = SW5 From c66766edcfc4dc510c45f27a1581addd8383a0fb Mon Sep 17 00:00:00 2001 From: Thomas Lohse Date: Mon, 12 Feb 2024 16:03:55 +0100 Subject: [PATCH 4/4] fmt fix --- build.gradle | 28 ++++++++-------- src/main/kotlin/Executor.kt | 33 ++++++++++--------- src/main/kotlin/TestResult.kt | 1 + .../kotlin/tests/SingleTestJsonAdapter.kt | 15 +++++---- 4 files changed, 40 insertions(+), 37 deletions(-) diff --git a/build.gradle b/build.gradle index 10773c3..a4ec6ab 100644 --- a/build.gradle +++ b/build.gradle @@ -1,5 +1,5 @@ buildscript { - ext.kotlin_version = '1.6.10' + ext.kotlin_version = '+' repositories { mavenCentral() @@ -7,7 +7,6 @@ buildscript { name 'JFrog OSS snapshot repo' url 'https://oss.jfrog.org/oss-snapshot-local/' } - jcenter() } dependencies { @@ -28,7 +27,6 @@ apply plugin: 'antlr' repositories { mavenLocal() mavenCentral() - jcenter() } def grpcVersion = '1.52.1' // CURRENT_GRPC_VERSION @@ -36,28 +34,28 @@ 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" diff --git a/src/main/kotlin/Executor.kt b/src/main/kotlin/Executor.kt index 72b913a..5163fdc 100644 --- a/src/main/kotlin/Executor.kt +++ b/src/main/kotlin/Executor.kt @@ -4,10 +4,6 @@ import EcdarProtoBuf.QueryProtos import EcdarProtoBuf.QueryProtos.QueryResponse.ResultCase import io.grpc.ManagedChannelBuilder import io.grpc.StatusRuntimeException -import parsing.EngineConfiguration -import tests.MultiTest -import tests.SingleTest -import tests.Test import java.io.BufferedReader import java.io.File import java.io.IOException @@ -16,7 +12,10 @@ import java.net.ServerSocket import java.util.concurrent.ConcurrentLinkedQueue import java.util.concurrent.TimeUnit import java.util.concurrent.atomic.AtomicInteger - +import parsing.EngineConfiguration +import tests.MultiTest +import tests.SingleTest +import tests.Test class Executor(engine: EngineConfiguration, address: String, private var port: Int) { val name = engine.name @@ -141,25 +140,29 @@ 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 + // 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()) - } + val currentParams = + Array(params.size) { params[it].replace("{ip}", ip).replace("{port}", p.toString()) } proc = - ProcessBuilder(path, - *currentParams) + ProcessBuilder(path, *currentParams) // .redirectOutput(ProcessBuilder.Redirect.appendTo(File("Engine-$name-log.txt"))) - .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. + .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 inputAndErrorStream = + proc?.inputStream ?: throw Exception("Process exited unexpectedly") val reader = BufferedReader(InputStreamReader(inputAndErrorStream)) var output: String? = null diff --git a/src/main/kotlin/TestResult.kt b/src/main/kotlin/TestResult.kt index b86d3e6..e4b350f 100644 --- a/src/main/kotlin/TestResult.kt +++ b/src/main/kotlin/TestResult.kt @@ -42,6 +42,7 @@ enum class ResultType { ERROR, COMPONENTSNOTINCACHE, RESULT_NOT_SET -> UNSATISFIED + SYNTAX -> TODO() } } } diff --git a/src/main/kotlin/tests/SingleTestJsonAdapter.kt b/src/main/kotlin/tests/SingleTestJsonAdapter.kt index 52317e5..23f9783 100644 --- a/src/main/kotlin/tests/SingleTestJsonAdapter.kt +++ b/src/main/kotlin/tests/SingleTestJsonAdapter.kt @@ -3,10 +3,11 @@ package tests import com.beust.klaxon.TypeAdapter import kotlin.reflect.KClass -class SingleTestJsonAdapter: TypeAdapter { - override fun classFor(type: Any): KClass = when(type as String) { - "NotSatisfiedTest" -> NotSatisfiedTest::class - "SatisfiedTest" -> SatisfiedTest::class - else -> throw IllegalArgumentException("Unknown type: $type") - } -} \ No newline at end of file +class SingleTestJsonAdapter : TypeAdapter { + override fun classFor(type: Any): KClass = + when (type as String) { + "NotSatisfiedTest" -> NotSatisfiedTest::class + "SatisfiedTest" -> SatisfiedTest::class + else -> throw IllegalArgumentException("Unknown type: $type") + } +}