Skip to content
Snippets Groups Projects
Commit 0ce436b5 authored by SeeBasTStick's avatar SeeBasTStick
Browse files

implementation of prob2 kernel connection

parent 501dda02
Branches
Tags
No related merge requests found
Showing
with 131 additions and 261 deletions
......@@ -22,11 +22,6 @@ fun main() {
fun startServer(inputStream: InputStream, outputStream: OutputStream){
println("starting kernel")
val kernel = ProBKernelManager()
kernel.start()
println("done")
val server = Server()
val launcher : Launcher<LanguageClient> = LSPLauncher.createServerLauncher(server, inputStream, outputStream)
val startListing : Future<*> = launcher.startListening()
......
......@@ -2,9 +2,9 @@ package b.language.server
import b.language.server.communication.CommunicatorInterface
import b.language.server.proBMangement.ProBInterface
import b.language.server.proBMangement.prob.CouldNotFindProBHomeException
import org.eclipse.lsp4j.*
import org.eclipse.lsp4j.services.TextDocumentService
import java.io.IOException
import java.util.concurrent.ConcurrentHashMap
class BDocumentService(private val server: Server,
......@@ -62,9 +62,10 @@ class BDocumentService(private val server: Server,
invalidFiles.forEach{uri -> communicator.publishDiagnostics(PublishDiagnosticsParams(uri, listOf()))}
communicator.sendDebugMessage("invalidating old files $invalidFiles", MessageType.Info)
issueTracker[currentUri] = filesWithProblems.toSet()
}catch (e : IOException){
communicator.sendDebugMessage("command could not be executed", MessageType.Info)
communicator.showMessage(e.message!!, MessageType.Error)
}catch (e : CouldNotFindProBHomeException){
communicator.sendDebugMessage(e.message!!, MessageType.Info)
communicator.showMessage(e.message, MessageType.Error)
}
}
......
......@@ -2,7 +2,6 @@ package b.language.server
import b.language.server.communication.Communicator
import b.language.server.dataStorage.Settings
import b.language.server.proBMangement.prob.ProBKernelConnector
import b.language.server.proBMangement.prob.ProBKernelManager
import com.google.gson.JsonObject
import org.eclipse.lsp4j.*
......@@ -12,11 +11,11 @@ import java.util.concurrent.CompletableFuture
import kotlin.collections.HashMap
import kotlin.system.exitProcess
class Server() : LanguageServer{
class Server : LanguageServer{
private val textDocumentService : TextDocumentService = BDocumentService(this, Communicator, ProBKernelConnector(Communicator))
private val textDocumentService : TextDocumentService = BDocumentService(this, Communicator, ProBKernelManager(Communicator))
private val bWorkspaceService : WorkspaceService = BWorkspaceService(this)
lateinit var languageClient : LanguageClient
private lateinit var languageClient : LanguageClient
var globalSettings : Settings = Settings()
val documentSettings : HashMap<String, CompletableFuture<Settings>> = HashMap()
var configurationAbility : Boolean = true
......@@ -30,9 +29,6 @@ class Server() : LanguageServer{
res.capabilities.workspace = WorkspaceServerCapabilities(WorkspaceFoldersOptions())
res.capabilities.workspace.workspaceFolders.supported = true
// languageClient.registerCapability(
// RegistrationParams(listOf(Registration("all_config_changes", "didChangeConfiguration" , bWorkspaceService))))
return CompletableFuture.supplyAsync { res }
}
......@@ -75,9 +71,6 @@ class Server() : LanguageServer{
}
/**
* Get the settings for the current document - will fallback to global settings eventually; If setting not cached
* method will try to get setting from the client
......
......@@ -13,11 +13,11 @@ import java.io.File
* @return the settings object
*/
fun castJsonToSetting(json : JsonObject) : Settings {
return Settings(Gson().fromJson(json.get("maxNumberOfProblems"), Int::class.java),
return Settings(
Gson().fromJson(json.get("wdChecks"), Boolean::class.java),
Gson().fromJson(json.get("strictChecks"), Boolean::class.java),
Gson().fromJson(json.get("performanceHints"), Boolean::class.java),
File(Gson().fromJson(json.get("probHome"), String::class.java)),
Gson().fromJson(json.get("probHome"), String::class.java),
Gson().fromJson(json.get("debugMode"), Boolean::class.java))
}
package b.language.server.dataStorage
class Position(var line : Int, var col : Int)
\ No newline at end of file
package b.language.server.dataStorage
/**
* kotlin representation of prob ndjson problems
*/
/**
* @param type type of the problem (error/warning/information(
* @param message problem message
* @param reason reason for the problem to occur
* @param file the file where the problem occurred
* @param start start position of the problem
* @param end end position of the problem
* @version version of porbcli
*/
data class Problem(val type : String , val message: String, val reason : String, val file : String, val start : Position,
val end : Position, val version : String)
......@@ -2,6 +2,6 @@ package b.language.server.dataStorage
import java.io.File
data class Settings(val maxNumberOfProblem : Int = 1000, val strictChecks : Boolean = true, val wdChecks : Boolean = true,
val performanceHints : Boolean = true , val probHome : File = File("DEFAULT"),
data class Settings(val strictChecks : Boolean = true, val wdChecks : Boolean = true,
val performanceHints : Boolean = true , val probHome : String = "DEFAULT",
val debugMode : Boolean = true)
package b.language.server.proBMangement.prob
enum class MessageTypes {
CHECK, KILL
}
\ No newline at end of file
class CouldNotFindProBHomeException(message : String) : Exception(message)
\ No newline at end of file
package b.language.server.proBMangement.prob
import b.language.server.communication.CommunicationCollector
import b.language.server.communication.Communicator
import b.language.server.communication.CommunicatorInterface
import b.language.server.dataStorage.ProBSettings
import b.language.server.proBMangement.prob.MyWarningListener
import b.language.server.proBMangement.prob.convertErrorItems
import com.google.inject.Inject
import com.google.inject.Injector
import de.prob.animator.ReusableAnimator
......@@ -20,63 +19,90 @@ import org.eclipse.lsp4j.Diagnostic
import org.eclipse.lsp4j.MessageType
import java.io.IOException
class ProBKernel @Inject constructor(private val injector : Injector, val classicalBFactory : ClassicalBFactory,
/**
* Represents the interface to communicate with prob kernel
* Is called via injector
* @see ProBKernelManager
*/
class ProBKernel @Inject constructor(private val injector : Injector,
val classicalBFactory : ClassicalBFactory,
private val animationSelector: AnimationSelector,
private val animator : ReusableAnimator) {
private val animator : ReusableAnimator,
private val communicator : CommunicatorInterface) {
val communicator = CommunicationCollector()
fun check(path : String, settings : ProBSettings) : Pair<List<Diagnostic>, List<Pair<String, MessageType>>>{
communicator.log.clear()
/**
* Checks the given machine file; prepares all necessary object
* @param path the file to check
* @param settings the settings under which the check takes place
* @return a list with the problems found
*/
fun check(path : String, settings : ProBSettings) : List<Diagnostic>{
Communicator.sendDebugMessage("Unload old machine", MessageType.Info)
unloadMachine()
//TODO Rules factory
val factory = injector.getInstance(FactoryProvider.factoryClassFromExtension(path.substringAfterLast(".")))
val warningListener = MyWarningListener()
val warningListener = WarningListener()
animator.addWarningListener(warningListener)
val parseErrors = mutableListOf<Diagnostic>()
Communicator.sendDebugMessage("Load new machine", MessageType.Info)
loadMachine(
val strictProblems = loadMachine(
{ stateSpace : StateSpace ->
try {
val extractedModel = factory.extract(path)
val stateSpaceWithSettings = extractedModel.load(prepareAdditionalSettings(settings))
extractedModel.loadIntoStateSpace(stateSpaceWithSettings)
factory.extract(path).loadIntoStateSpace(stateSpace)
} catch (e: IOException) {
// throw RuntimeException(e)
communicator.sendDebugMessage("IOException ${e.message}", MessageType.Info)
} catch (e: ModelTranslationError) {
communicator.sendDebugMessage("ModelTranslationError ${e.message}", MessageType.Info)
// throw RuntimeException(e)
}catch (e : ProBError){
parseErrors.addAll(convertErrorItems(e.errors))
}
Trace(stateSpace)
}, settings)
return Pair(listOf(warningListener.getWarnings(), parseErrors).flatten(), communicator.log)
communicator.sendDebugMessage("returning from kernel", MessageType.Info)
return listOf(warningListener.getWarnings(), parseErrors).flatten()
}
/**
* Does the main work
* @param newTraceCreator a anonymous function dealing with the state space
* @param settings the settings to be applied
*/
private fun loadMachine(newTraceCreator :java.util.function.Function<StateSpace, Trace>, settings: ProBSettings){
val newStateSpace = animator.createStateSpace()
newStateSpace.changePreferences(prepareAdditionalSettings(settings))
try {
communicator.sendDebugMessage("changing animation", MessageType.Info)
animationSelector.changeCurrentAnimation(newTraceCreator.apply(newStateSpace))
communicator.sendDebugMessage("executing optional steps", MessageType.Info)
executeAdditionalOptions(settings)
newStateSpace.performExtendedStaticChecks() //TODO move to additional options
communicator.sendDebugMessage("returning...", MessageType.Info)
} catch (e: RuntimeException) {
newStateSpace.kill()
throw e
}
}
/**
* executes additional commands, which are defined as separate command, all others are executed at
* @see prepareAdditionalSettings
* @param settings the settings to be executed as command
*/
private fun executeAdditionalOptions(settings : ProBSettings){
// animator.createStateSpace()
if(settings.wdChecks){
communicator.sendDebugMessage("Doing WD checks", MessageType.Info)
animator.execute(CheckWellDefinednessCommand())
}
}
/**
* to clean up a machine
*/
private fun unloadMachine() {
val oldTrace = animationSelector.currentTrace
if (oldTrace != null) {
......@@ -87,6 +113,11 @@ class ProBKernel @Inject constructor(private val injector : Injector, val classi
}
/**
* prepares a map with additional settings
* @param proBSettings the settings to put in the map
* @return the settings map
*/
private fun prepareAdditionalSettings(proBSettings: ProBSettings): MutableMap<String, String> {
val settings = mutableMapOf<String, String>()
if(proBSettings.performanceHints) {
......
package b.language.server.proBMangement.prob
import b.language.server.communication.CommunicatorInterface
import b.language.server.dataStorage.Settings
import b.language.server.proBMangement.ProBInterface
import com.google.gson.Gson
import com.google.gson.JsonSyntaxException
import org.eclipse.lsp4j.Diagnostic
import org.eclipse.lsp4j.MessageType
import org.zeromq.SocketType
import org.zeromq.ZContext
import org.zeromq.ZMQ
class ProBKernelConnector(val communicator : CommunicatorInterface) : ProBInterface, ServerConnection{
private val context = ZContext()
private val socket: ZMQ.Socket = context.createSocket(SocketType.REQ)
init {
socket.connect("tcp://localhost:5557")
}
/**
* Checks the given document with the help of ProB
* @param uri the source to check
* @param settings the settings for this document
* @return a list of all problems found
*/
override fun checkDocument(uri: String, settings: Settings): List<Diagnostic> {
communicator.sendDebugMessage("start checking, submitting to prob server " , MessageType.Info)
val reply = send(Request(MessageTypes.CHECK, uri, settings))
communicator.sendDebugMessage("got reply " , MessageType.Info)
System.err.println("getting reply $reply")
deliverDebugMessages(reply.messages)
System.err.println("deliverd messages")
return reply.diagnostics
}
/**
* sends a request to the b kernel thread
* @param payLoad the request to be send
* @return a reply
*/
fun send(payLoad : Request) : Reply{
communicator.sendDebugMessage("sending... " , MessageType.Info)
socket.send(Gson().toJson(payLoad))
communicator.sendDebugMessage("rec... " , MessageType.Info)
val recv = socket.recvStr()
communicator.sendDebugMessage("rec: $recv " , MessageType.Info)
System.err.println("deserialize message")
val answer = try{
Gson().fromJson(recv, Reply::class.java)
}catch (e : JsonSyntaxException){
System.err.println("Failed..")
throw Exception(e)
}
System.err.println("deserialize message done")
communicator.sendDebugMessage("answer $answer" , MessageType.Info)
return answer
}
/**
* Delivers Messages we got from the b kernel thread
* @param messages list with the messages
*/
fun deliverDebugMessages(messages : List<Pair<String, MessageType>>){
messages.forEach{ message -> communicator.sendDebugMessage(message.first, message.second) }
}
/**
* Orders the server to shutdown the process it keeps, clean up and shutdown itself
*/
override fun kill(): Reply {
socket.send(Gson().toJson(Request(MessageTypes.KILL)))
return Gson().fromJson(socket.recvStr(), Reply::class.java)
}
}
\ No newline at end of file
package b.language.server.proBMangement.prob
import ProBKernel
import b.language.server.communication.CommunicationCollector
import b.language.server.communication.Communicator
import b.language.server.communication.CommunicatorInterface
import b.language.server.dataStorage.ProBSettings
import b.language.server.dataStorage.Settings
import com.google.gson.Gson
import b.language.server.proBMangement.ProBInterface
import com.google.inject.Guice
import com.google.inject.Stage
import org.eclipse.lsp4j.Diagnostic
import org.eclipse.lsp4j.MessageType
import org.zeromq.SocketType
import org.zeromq.ZContext
import org.zeromq.ZMQ
import java.io.File
import java.net.URI
/**
* Creates the prob kernel access and maintaince a stady connection
* Creates the prob kernel access and maintenance
*/
class ProBKernelManager : Thread() {
private var active = true
private lateinit var kernel : ProBKernel
private var probHome = ""
private val communicator = CommunicationCollector()
class ProBKernelManager(private val communicator : CommunicatorInterface) : ProBInterface {
private var kernel : ProBKernel
private var probHome = "DEFAULT"
override fun run() {
ZContext().use { context ->
val socket: ZMQ.Socket = context.createSocket(SocketType.REP)
socket.bind("tcp://*:5557")
init{
kernel = setup()
while (active) {
val message = socket.recvStr()
val request = Gson().fromJson(message, Request::class.java)
Communicator.sendDebugMessage("manageer got request... " , MessageType.Info)
val reply = if (request.type==MessageTypes.CHECK){
check(request.uri, request.settings)
}else{
kill()
}
System.err.println("sending result back")
socket.send(Gson().toJson(reply))
}
}
}
fun check(uri : String, settings : Settings) : Reply{
val path = URI(uri).path
System.err.println("start prob")
System.err.println("checking file $path")
Communicator.sendDebugMessage("checking document", MessageType.Info)
val result = kernel.check(path, ProBSettings(settings.wdChecks, settings.strictChecks, settings.performanceHints))
System.err.println("returning result")
return Reply(result.first, result.second)
}
fun kill() : Reply{
active = false
return Reply(listOf(), listOf())
}
/**
* @param probHome the home of prob; DEFAULT for the prob version delivered with the library
* @return an instance of prob kernel
*/
fun setup() : ProBKernel {
// Communicator.sendDebugMessage("creating injector...", MessageType.Info)
System.err.println("Creating injector in thread " + this.id)
val injector = Guice.createInjector(Stage.PRODUCTION, ProBKernelModule())
System.err.println("Done " + this.id)
// Communicator.sendDebugMessage("..done", MessageType.Info)
private fun setup() : ProBKernel {
val injector = Guice.createInjector(Stage.PRODUCTION, ProBKernelModule(communicator))
val kernel : ProBKernel
try{
kernel = injector.getInstance(ProBKernel::class.java)
}catch (e : de.prob.exception.CliError){
// Communicator.sendDebugMessage("wrong path to prob", MessageType.Error)
throw Exception("wrong path to prob $probHome")
}
// Communicator.sendDebugMessage("returning kernel", MessageType.Info)
return kernel
}
/**
* Checks if the given prob home matches - if not a knew prob kernel will be initialized
* @param probNewHome the potential new proB home
* @return changes was successful/no change at all
*/
private fun checkProBVersionSetting(probNewHome : String) : Boolean{
return if(probNewHome != probHome)
{
if(File(probNewHome).exists()) {
System.setProperty("prob.home", "/home/sebastian/prob_prolog")
kernel = setup()
probHome = probNewHome
true
} else{
false
}
}else{
true
}
}
/**
* Checks the given document with the help of ProB
* @param uri the source to check
* @param settings the settings for this document
* @return a list of all problems found
*
* @throws CouldNotFindProBHomeException the given path ist not "DEFAULT" and wrong
*/
override fun checkDocument(uri: String, settings: Settings): List<Diagnostic> {
val path = URI(uri).path
communicator.sendDebugMessage("try to use ${settings.probHome} as prob version", MessageType.Info)
val result = checkProBVersionSetting(settings.probHome)
if(!result){
throw CouldNotFindProBHomeException("searched at ${settings.probHome} for prob but found nothing")
}
communicator.sendDebugMessage("success...", MessageType.Info)
communicator.sendDebugMessage("checking document", MessageType.Info)
return kernel.check(path, ProBSettings(wdChecks = settings.wdChecks, strictChecks = settings.strictChecks, performanceHints = settings.performanceHints))
}
}
\ No newline at end of file
package b.language.server.proBMangement.prob
import b.language.server.communication.Communicator
import b.language.server.communication.CommunicatorInterface
import com.google.inject.AbstractModule
import de.prob.MainModule
class ProBKernelModule() : AbstractModule() {
class ProBKernelModule(val communicator : CommunicatorInterface) : AbstractModule() {
override fun configure() {
install(MainModule())
bind(CommunicatorInterface::class.java).toInstance(communicator)
}
}
\ No newline at end of file
package b.language.server.proBMangement.prob
import org.eclipse.lsp4j.Diagnostic
import org.eclipse.lsp4j.MessageType
data class Reply(val diagnostics : List<Diagnostic>, val messages : List<Pair<String, MessageType>>)
\ No newline at end of file
package b.language.server.proBMangement.prob
import b.language.server.dataStorage.Settings
data class Request(val type : MessageTypes, val uri : String = String(), val settings : Settings = Settings())
\ No newline at end of file
package b.language.server.proBMangement.prob
interface ServerConnection {
/**
* Orders the server to shutdown the process it keeps, clean up and shutdown itself
*/
fun kill() : Reply
}
\ No newline at end of file
......@@ -9,7 +9,7 @@ import org.eclipse.lsp4j.Range
fun convertErrorItems(errorItems : List<ErrorItem>) : List<Diagnostic>{
return errorItems.toList().map { errorItem ->
errorItem.locations.map { location ->
Diagnostic(Range(Position(location.startLine, location.startColumn), Position(location.endLine, location.endColumn)),
Diagnostic(Range(Position(location.startLine-1, location.startColumn), Position(location.endLine-1, location.endColumn)),
errorItem.message,
getErrorItemType(errorItem),
location.filename)
......
......@@ -5,8 +5,10 @@ import de.prob.animator.domainobjects.ErrorItem
import org.eclipse.lsp4j.Diagnostic
import org.eclipse.lsp4j.DiagnosticSeverity
class MyWarningListener : IWarningListener {
/**
* Custom collector to collect warnings from prob kernel
*/
class WarningListener : IWarningListener {
private val warningList : ArrayList<ErrorItem> = arrayListOf()
override fun warningsOccurred(warnings: MutableList<ErrorItem>?) {
warningList.addAll(warnings!!.toList())
......
package b.language.server
import b.language.server.dataStorage.Position
import b.language.server.dataStorage.Problem
import b.language.server.dataStorage.Settings
import com.google.gson.Gson
import org.eclipse.lsp4j.Diagnostic
import org.eclipse.lsp4j.DiagnosticSeverity
import org.eclipse.lsp4j.Range
import kotlin.test.Test
import org.junit.jupiter.api.io.TempDir
import java.io.File
import kotlin.test.assertEquals
import kotlin.test.assertTrue
class ProBCommandLineTest{
/*
@Test
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment