feat(connector): change VDMJ to use interpreter

This commit is contained in:
Anthony Berg 2024-04-18 17:16:48 +01:00
parent b784ab9799
commit e781c12d22
3 changed files with 88 additions and 47 deletions

View File

@ -1,12 +1,14 @@
package io.anthonyberg.connector.routes
import io.anthonyberg.connector.shared.vdmj.vdmjExecute
import io.anthonyberg.connector.shared.vdmj.VDMJ
import io.ktor.http.*
import io.ktor.server.application.*
import io.ktor.server.response.*
import io.ktor.server.routing.*
fun Route.vdmjRouting() {
val vdmj = VDMJ()
route("/vdmj") {
get("{exp?}") {
val exp = call.parameters["exp"] ?: return@get call.respondText(
@ -15,7 +17,7 @@ fun Route.vdmjRouting() {
)
// TODO output is empty string after first request
val result = vdmjExecute(exp)
val result = vdmj.run(exp)
call.respond(result)
}

View File

@ -1,7 +1,6 @@
package io.anthonyberg.connector.shared.entity
import com.fujitsu.vdmj.ExitStatus
import kotlinx.serialization.Serializable
@Serializable
data class VDMJExpression(val output: String, val exitStatus: ExitStatus)
data class VDMJExpression(val output: String)

View File

@ -1,5 +1,6 @@
package io.anthonyberg.connector.shared.vdmj
import com.fujitsu.vdmj.ExitStatus
import com.fujitsu.vdmj.Settings
import com.fujitsu.vdmj.config.Properties
import com.fujitsu.vdmj.messages.Console
@ -8,62 +9,101 @@ import com.fujitsu.vdmj.plugins.EventHub
import com.fujitsu.vdmj.plugins.Lifecycle
import com.fujitsu.vdmj.plugins.VDMJ
import io.anthonyberg.connector.shared.entity.VDMJExpression
import java.io.ByteArrayOutputStream
import kotlinx.coroutines.*
import java.io.*
import java.nio.file.Paths
import kotlin.io.path.pathString
/**
* Handler for the VDM Model
*/
fun vdmjExecute(expression: String): VDMJExpression {
Settings.mainClass = VDMJ::class.java
Properties.init()
val lifecycle: Lifecycle = createLifecycle(expression)
@OptIn(DelicateCoroutinesApi::class)
class VDMJ {
// Create a ByteArrayOutputStream to capture the output
val byteArrayOutputStream = ByteArrayOutputStream()
val printStream = ConsolePrintWriter(byteArrayOutputStream)
private val byteArrayOutputStream = ByteArrayOutputStream()
private val printStream = ConsolePrintWriter(byteArrayOutputStream)
private val inputStream = PipedInputStream()
private val inputOutput = PipedOutputStream(inputStream)
private val bufferedReader = BufferedReader(InputStreamReader(inputStream))
private val writer = BufferedWriter(OutputStreamWriter(inputOutput))
// Save the old PrintStreams
val oldOut = Console.out
val oldErr = Console.err
private val oldOut = Console.out
private val oldErr = Console.err
private val oldIn = Console.`in`
private lateinit var exitStatus: ExitStatus
/**
* Starts VDMJ interpreter
*/
init {
Settings.mainClass = VDMJ::class.java
Properties.init()
// Redirect Console's PrintStreams to the new PrintStream
Console.out = printStream
Console.err = printStream
Console.`in` = bufferedReader
// TODO check if there is actually a memory leak or if it is just Java
val exitStatus = lifecycle.run()
val lifecycle: Lifecycle = createLifecycle()
// Start a coroutine for VDMJ to run in
GlobalScope.launch {
exitStatus = lifecycle.run()
}
}
/**
* Creates VDMJ Lifecycle with interpreter mode
*/
private fun createLifecycle(): Lifecycle {
val vdmPath = Paths.get("src/main/resources/checklist.vdmsl")
// Creates the arguments for VDMJ - i.e. where the file is located
val vdmArgs = arrayOf(vdmPath.pathString, "-vdmsl", "-i", "-q")
return Lifecycle(vdmArgs)
}
fun cleanup() {
// Reset Console's PrintStreams to the old PrintStreams
Console.out = oldOut
Console.err = oldErr
// Convert the captured output to a string
val console = byteArrayOutputStream.toString()
Console.`in` = oldIn
// Reset the ByteArrayOutputStream
byteArrayOutputStream.reset()
// Resets VDMJ's EventHub after closing lifecycle
EventHub.reset()
}
val output = VDMJExpression(output = console, exitStatus = exitStatus)
return output
// exitProcess(if (lifecycle.run() == ExitStatus.EXIT_OK) 0 else 1)
}
/**
* Creates arguments for VDMJ
/**
* Runs VDM command
*/
private fun createLifecycle(command: String): Lifecycle {
val vdmPath = Paths.get( "src/main/resources/checklist.vdmsl")
suspend fun run(command: String): VDMJExpression {
// Clean previous console outputs
byteArrayOutputStream.reset()
// Creates the arguments for VDMJ - i.e. where the file is located
val vdmArgs = arrayOf(vdmPath.pathString, "-vdmsl", "-e", command, "-q", "-w")
// Run commands
withContext(Dispatchers.IO) {
writer.write(command)
writer.write(System.lineSeparator())
writer.flush()
}
return Lifecycle(vdmArgs)
var output = byteArrayOutputStream.toString()
while(!this::exitStatus.isInitialized and output.isEmpty()) {
delay(10)
// Convert the captured output to a string
output = byteArrayOutputStream.toString()
}
// Clear console output again, just to be kind
byteArrayOutputStream.reset()
return VDMJExpression(output = output)
}
}