diff --git a/.gitmodules b/.gitmodules index a42b21e..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 - branch = futureproof1 + path = src/main/Ecdar-ProtoBuf + url = git@github.com:Ecdar/Ecdar-ProtoBuf.git + branch = SW5 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..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,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" diff --git a/src/main/Ecdar-ProtoBuf b/src/main/Ecdar-ProtoBuf index ae8364e..f5ae959 160000 --- a/src/main/Ecdar-ProtoBuf +++ b/src/main/Ecdar-ProtoBuf @@ -1 +1 @@ -Subproject commit ae8364e6c8942a5cfde24adec779ca87d4431e4a +Subproject commit f5ae9598ebd6de74e17a7a03ae1b0896ae322ef7 diff --git a/src/main/kotlin/Executor.kt b/src/main/kotlin/Executor.kt index 180f8c1..5163fdc 100644 --- a/src/main/kotlin/Executor.kt +++ b/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() { 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..e4b350f 100644 --- a/src/main/kotlin/TestResult.kt +++ b/src/main/kotlin/TestResult.kt @@ -40,7 +40,9 @@ enum class ResultType { PARSING_ERROR, MODEL, ERROR, + COMPONENTSNOTINCACHE, RESULT_NOT_SET -> UNSATISFIED + SYNTAX -> TODO() } } } 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..23f9783 --- /dev/null +++ b/src/main/kotlin/tests/SingleTestJsonAdapter.kt @@ -0,0 +1,13 @@ +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") + } +} 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