Merge branch 'prob2_connection'

# Conflicts:
#	src/main/kotlin/b/language/server/BDocumentService.kt
#	src/main/kotlin/b/language/server/BWorkspaceService.kt
#	src/main/kotlin/b/language/server/Server.kt
#	src/main/kotlin/b/language/server/communication/Communicator.kt
#	src/main/kotlin/b/language/server/dataStorage/Settings.kt
#	src/main/kotlin/b/language/server/proBMangement/probCli/CommandCouldNotBeExecutedException.kt
#	src/main/kotlin/b/language/server/proBMangement/probCli/PathCouldNotBeCreatedException.kt
#	src/main/kotlin/b/language/server/proBMangement/probCli/ProBCommandLineAccess.kt
#	src/test/kotlin/b/language/server/ProBCommandLineTest.kt

README.md

 # b-language-server
-A language server implementation for B, using ProB as backend, based on Java/Kotlin
+A language server implementation for B, using ProB as backend, based on Java/Kotlin. This language server comes with his
+own version of probcli.
+
+## Usage
+After starting the server; either from an IDE via main or by building and executing a shadowjar, a language client can 
+connect to it via port 55555.
+
+## Capabilities
+
+- Calling ProB Java Kernel with additional options
+- Options need to be specified by the client; They are requested by the server
+- Options are: 
+    *   val strictChecks : Boolean = true  
+    *   val wdChecks : Boolean = true
+    *   val performanceHints : Boolean = true 
+    *   val probHome : String = "DEFAULT"
+    *   val debugMode : Boolean = true
+    
+- Setting probHome to a different target then DEFAULT can cause all sorts of bad stuff. Ensure that the path points to the
+correct directory. Note that any probcli other version then the version used by prob java kernel can cause uncaught errors.
+If you want to use another version probcli point to the directory, not to probcli.sh e.g.:
+```
+/home/sebastian/prob_prolog
+```
+    
+## Clients
+
+- VSCode: https://marketplace.visualstudio.com/items?itemName=SeeBasTStick.b-language-extension
\ No newline at end of file

build.gradle.kts

@@ -7,7 +7,7 @@
 
 plugins {
     // Apply the Kotlin JVM plugin to add support for Kotlin.
-    id("org.jetbrains.kotlin.jvm") version "1.3.72"
+    kotlin("jvm") version "1.4.0"
     idea
     // Apply the application plugin to add support for building a CLI application.
     application
@@ -19,8 +19,13 @@ plugins {
 repositories {
     // Use jcenter for resolving dependencies.
     jcenter()
+
+    maven("https://oss.sonatype.org/content/repositories/snapshots")
+
 }
 
+
+
 dependencies {
     // Align versions of all Kotlin components
     implementation(platform("org.jetbrains.kotlin:kotlin-bom"))
@@ -28,6 +33,10 @@ dependencies {
     // Use the Kotlin JDK 8 standard library.
     implementation("org.jetbrains.kotlin:kotlin-stdlib-jdk8")
 
+
+    implementation("org.jetbrains.kotlinx:kotlinx-coroutines-core:1.3.9")
+
+
     // eclipse lsp implementation
     implementation("org.eclipse.lsp4j", "org.eclipse.lsp4j",  "0.9.0")
 
@@ -41,15 +50,32 @@ dependencies {
     // https://mvnrepository.com/artifact/org.junit.jupiter/junit-jupiter-api
     testImplementation("org.junit.jupiter","junit-jupiter-engine" ,  "5.7.0-M1")
 
+    implementation("de.hhu.stups:de.prob2.kernel:4.0.0-SNAPSHOT")
+
+    implementation( "com.google.guava", "guava", "28.2-jre")
+
+
+    // https://mvnrepository.com/artifact/org.zeromq/jeromq
+    implementation ("org.zeromq",   "jeromq", "0.5.2")
+
 
 }
 
 
+
+
+
 tasks.test {
     useJUnitPlatform()
 }
 
 val gitVersion: groovy.lang.Closure<*> by extra
+
+tasks.withType<org.jetbrains.kotlin.gradle.tasks.KotlinCompile>(){
+    kotlinOptions.jvmTarget = "1.8"
+}
+
+
 tasks.shadowJar{
   //  this.version = gitVersion().toString()
 }

package.json

 {
   "name": "b-language-server",
-  "version": "1.0.0",
+  "version": "2.0.0",
   "description": "a java based language server implementing the lsp",
   "main": "index.js",
   "scripts": {

settings.gradle.kts

@@ -8,3 +8,4 @@
  */
 
 rootProject.name = "b-language-server"
+//includeBuild("../prob2_kernel/de.prob2.kernel")
\ No newline at end of file

src/main/kotlin/b/language/server/App.kt

@@ -3,16 +3,22 @@ package b.language.server
 import org.eclipse.lsp4j.jsonrpc.Launcher
 import org.eclipse.lsp4j.launch.LSPLauncher
 import org.eclipse.lsp4j.services.LanguageClient
-import java.io.InputStream
-import java.io.OutputStream
+import java.io.*
+import java.net.ServerSocket
 import java.util.concurrent.Future
 
 
 fun main() {
-    startServer(System.`in`, System.out)
+    val socket = ServerSocket(0)
+
+    println("<${socket.localPort}> is the port; opening connection and listening")
+    val channel = socket.accept()
+    //println("accepted connection from ${channel.inetAddress}")
+    startServer(channel.getInputStream(), channel.getOutputStream())
 }
 
 fun startServer(inputStream: InputStream, outputStream: OutputStream){
+
     val server = Server()
     val launcher : Launcher<LanguageClient> = LSPLauncher.createServerLauncher(server, inputStream, outputStream)
     val startListing : Future<*> = launcher.startListening()

src/main/kotlin/b/language/server/BDocumentService.kt

 package b.language.server
 
 import b.language.server.communication.CommunicatorInterface
-import b.language.server.proBMangement.probCli.CommandCouldNotBeExecutedException
-import b.language.server.proBMangement.probCli.PathCouldNotBeCreatedException
 import b.language.server.proBMangement.ProBInterface
-import b.language.server.proBMangement.probCli.ProBCommandLineAccess
+import b.language.server.proBMangement.prob.CouldNotFindProBHomeException
 import org.eclipse.lsp4j.*
 import org.eclipse.lsp4j.services.TextDocumentService
-import java.io.IOException
-import java.net.URI
 import java.util.concurrent.ConcurrentHashMap
 
-class BDocumentService(private val server: Server, private val communicator: CommunicatorInterface) : TextDocumentService {
+class BDocumentService(private val server: Server,
+                       private val communicator: CommunicatorInterface,
+                       private val proBInterface: ProBInterface) : TextDocumentService {
 
     private val documents = ConcurrentHashMap<String, String>()
     private val issueTracker : ConcurrentHashMap<String, Set<String>> = ConcurrentHashMap()
@@ -36,7 +34,7 @@ class BDocumentService(private val server: Server, private val communicator: Com
      */
     override fun didSave(params: DidSaveTextDocumentParams?) {
 
-        communicator.bufferDebugMessage("document ${params!!.textDocument.uri} was saved", MessageType.Info)
+        communicator.sendDebugMessage("document ${params!!.textDocument.uri} was saved", MessageType.Info)
         val currentUri = params.textDocument.uri
         checkDocument(currentUri)
 
@@ -49,7 +47,7 @@ class BDocumentService(private val server: Server, private val communicator: Com
     fun checkDocument(currentUri : String){
 
         val clientSettings = server.getDocumentSettings(currentUri)
-        communicator.bufferDebugMessage("waiting for document settings", MessageType.Info)
+        communicator.sendDebugMessage("waiting for document settings", MessageType.Info)
 
         clientSettings.thenAccept{ settings ->
             communicator.setDebugMode(settings.debugMode)
@@ -69,15 +67,9 @@ class BDocumentService(private val server: Server, private val communicator: Com
                 communicator.sendDebugMessage("invalidating old files $invalidFiles", MessageType.Info)
                 issueTracker[currentUri] = filesWithProblems.toSet()
 
-            }catch (e : PathCouldNotBeCreatedException){
-                communicator.sendDebugMessage("error path could not be created", MessageType.Info)
-                communicator.showMessage(e.message!!, MessageType.Error)
-            }catch (e : CommandCouldNotBeExecutedException){
-                communicator.sendDebugMessage("command could not be executed", MessageType.Info)
-                communicator.showMessage(e.message!!, MessageType.Error)
-            }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)
             }
         }
 
@@ -113,7 +105,7 @@ class BDocumentService(private val server: Server, private val communicator: Com
      * Registration Options: TextDocumentChangeRegistrationOptions
      */
     override fun didChange(params: DidChangeTextDocumentParams?) {
-        communicator.bufferDebugMessage("document ${params!!.textDocument.uri} was changed", MessageType.Info)
+        communicator.sendDebugMessage("document ${params!!.textDocument.uri} was changed", MessageType.Info)
         val currentUri = params.textDocument.uri
         checkDocument(currentUri)
     }

src/main/kotlin/b/language/server/BWorkspaceService.kt

 package b.language.server
 
 import b.language.server.communication.Communicator
-import b.language.server.dataStorage.Settings
-import com.google.gson.Gson
 import com.google.gson.JsonObject
 import org.eclipse.lsp4j.DidChangeConfigurationParams
 import org.eclipse.lsp4j.DidChangeWatchedFilesParams
 import org.eclipse.lsp4j.MessageType
 import org.eclipse.lsp4j.services.WorkspaceService
-import java.io.File
 
-class BWorkspaceService(private val server : Server) : WorkspaceService {
+
+class BWorkspaceService(private val server: Server, val communicator: Communicator) : WorkspaceService {
     /**
      * The watched files notification is sent from the client to the server when
      * the client detects changes to file watched by the language client.
      */
     override fun didChangeWatchedFiles(params: DidChangeWatchedFilesParams?) {
-        Communicator.bufferDebugMessage("changed watched files", MessageType.Info)
+         communicator.sendDebugMessage("----------changed watched files", MessageType.Info)
 
         // Not needed
     }
@@ -26,7 +24,7 @@ class BWorkspaceService(private val server : Server) : WorkspaceService {
      * configuration settings.
      */
     override fun didChangeConfiguration(params: DidChangeConfigurationParams?) {
-        Communicator.bufferDebugMessage("received change in configuration settings", MessageType.Info)
+        communicator.sendDebugMessage("received change in configuration settings", MessageType.Info)
         if(server.configurationAbility) {
             server.documentSettings.clear()
         }else{

src/main/kotlin/b/language/server/Server.kt

@@ -2,35 +2,33 @@ package b.language.server
 
 import b.language.server.communication.Communicator
 import b.language.server.dataStorage.Settings
+import b.language.server.proBMangement.prob.ProBKernelManager
 import com.google.gson.JsonObject
 import org.eclipse.lsp4j.*
 import org.eclipse.lsp4j.jsonrpc.messages.Either
-import org.eclipse.lsp4j.jsonrpc.services.JsonNotification
 import org.eclipse.lsp4j.services.*
 import java.util.concurrent.CompletableFuture
 import kotlin.collections.HashMap
 import kotlin.system.exitProcess
-import org.eclipse.lsp4j.jsonrpc.services.GenericEndpoint
 
 class Server : LanguageServer{
 
-    private val textDocumentService : TextDocumentService = BDocumentService(this, Communicator)
-    private val bWorkspaceService : WorkspaceService = BWorkspaceService(this)
-     lateinit var languageClient : LanguageClient
+    private val textDocumentService : TextDocumentService = BDocumentService(this, Communicator, ProBKernelManager(Communicator))
+    private val bWorkspaceService : WorkspaceService = BWorkspaceService(this, Communicator)
+    private lateinit var languageClient : LanguageClient
     var globalSettings : Settings = Settings()
     val documentSettings : HashMap<String, CompletableFuture<Settings>> = HashMap()
     var configurationAbility : Boolean = true
 
 
+
+
     override fun initialize(params: InitializeParams?): CompletableFuture<InitializeResult> {
         val res = InitializeResult(ServerCapabilities())
         res.capabilities.textDocumentSync = Either.forLeft(TextDocumentSyncKind.Full)
         res.capabilities.workspace = WorkspaceServerCapabilities(WorkspaceFoldersOptions())
         res.capabilities.workspace.workspaceFolders.supported = true
-
-      //  languageClient.registerCapability(
-        //        RegistrationParams(listOf(Registration("all_config_changes", "didChangeConfiguration" , bWorkspaceService))))
-
+       // res.capabilities.completionProvider = CompletionOptions()
         return CompletableFuture.supplyAsync { res }
     }
 
@@ -73,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
@@ -83,7 +78,7 @@ class Server : LanguageServer{
      * @return settings of the document requested
      */
     fun getDocumentSettings(uri : String) : CompletableFuture<Settings> {
-        Communicator.bufferDebugMessage("received configuration data of the document $uri", MessageType.Info)
+        Communicator.sendDebugMessage("requesting configuration for document: $uri", MessageType.Info)
         return if(!configurationAbility){
             val returnValue = CompletableFuture<Settings>()
             returnValue.complete(globalSettings)
@@ -93,6 +88,7 @@ class Server : LanguageServer{
             val configurationItem = ConfigurationItem()
             configurationItem.scopeUri = uri
             configurationItem.section = "languageServer"
+
             val requestedConfig = languageClient.configuration(ConfigurationParams(listOf(configurationItem)))
             documentSettings[uri] = CompletableFuture.allOf(requestedConfig).thenApply{ castJsonToSetting(requestedConfig.get().first() as JsonObject) }
             documentSettings[uri]!!
@@ -100,4 +96,7 @@ class Server : LanguageServer{
     }
 
 
+
+
+
 }
\ No newline at end of file

src/main/kotlin/b/language/server/Util.kt

@@ -4,8 +4,6 @@ import b.language.server.dataStorage.Settings
 import com.google.gson.Gson
 import com.google.gson.JsonObject
 
-import java.io.File
-
 
 /**
  * Takes a json and tries to cast it into a settings objects
@@ -17,6 +15,8 @@ fun castJsonToSetting(json : JsonObject) : 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))
 }
+
+

src/main/kotlin/b/language/server/communication/Communicator.kt

 package b.language.server.communication
 
-import org.eclipse.lsp4j.Diagnostic
 import org.eclipse.lsp4j.MessageParams
 import org.eclipse.lsp4j.MessageType
 import org.eclipse.lsp4j.PublishDiagnosticsParams
@@ -16,15 +15,14 @@ object Communicator : CommunicatorInterface {
     lateinit var client : LanguageClient
 
     private var debugMode : Boolean = true
-    private val storedMessages = mutableListOf<Pair<String, MessageType>>()
 
     /**
      * Sends the diagnostics
      *
      * @param diagnostics object containing the Diagnostics
      */
-    override fun publishDiagnostics(target :String, diagnostics : List<Diagnostic>) {
-        client.publishDiagnostics(PublishDiagnosticsParams(target, diagnostics))
+    override fun publishDiagnostics(diagnostics: PublishDiagnosticsParams) {
+        client.publishDiagnostics(diagnostics)
     }
 
     /**
@@ -34,13 +32,8 @@ object Communicator : CommunicatorInterface {
      * @param severity the Severity of the message (Error/Info/Warning)
      */
     override fun sendDebugMessage(message: String, severity: MessageType) {
-
-
         if(debugMode) {
-            if(storedMessages.isNotEmpty()) {
-                storedMessages.toList().forEach { element -> client.logMessage(MessageParams(element.second, element.first)) }
-                storedMessages.clear()
-            }
+            println("Debug messages: $message")
             client.logMessage(MessageParams(severity, message))
         }
 
@@ -65,17 +58,4 @@ object Communicator : CommunicatorInterface {
     override fun setDebugMode(mode : Boolean){
         debugMode = mode
     }
-
-    /**
-     * Can be used to store a messages until a "sendDebugMessage" command is sent. The messages will be sent as FIFO
-     * @param message the message to send
-     * @param severity tne message severity
-     */
-    override fun bufferDebugMessage(message: String, severity: MessageType) {
-        if(debugMode) {
-            storedMessages.add(Pair(message, severity))
-        }
-    }
-
-
 }
\ No newline at end of file

src/main/kotlin/b/language/server/dataStorage/Position.kt

-package b.language.server.dataStorage
-
-
-class Position(var line : Int, var col : Int)
\ No newline at end of file

src/main/kotlin/b/language/server/dataStorage/ProBSettings.kt

+package b.language.server.dataStorage
+
+data class ProBSettings(val wdChecks : Boolean, val strictChecks : Boolean, val performanceHints : Boolean)
\ No newline at end of file

src/main/kotlin/b/language/server/dataStorage/Problem.kt

-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)
-

src/main/kotlin/b/language/server/dataStorage/Settings.kt

 package b.language.server.dataStorage
 
-import java.io.File
 
 data class Settings(val strictChecks : Boolean = true,  val wdChecks : Boolean = true,
-                    val performanceHints : Boolean = true , val probHome : File = File("~/prob_prolog/probcli.sh"),
+                    val performanceHints : Boolean = true , val probHome : String = "DEFAULT",
                     val debugMode : Boolean = true)

src/main/kotlin/b/language/server/proBMangement/ProBInterface.kt

@@ -8,8 +8,9 @@ interface ProBInterface {
     /**
      * 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
      */
-    abstract fun checkDocument(uri : String, settings: Settings) : List<Diagnostic>
+    fun checkDocument(uri : String, settings: Settings) : List<Diagnostic>
 
 }
\ No newline at end of file

src/main/kotlin/b/language/server/proBMangement/prob/CouldNotFindProBHomeException.kt

+package b.language.server.proBMangement.prob
+
+class CouldNotFindProBHomeException(message : String) : Exception(message)
\ No newline at end of file

src/main/kotlin/b/language/server/proBMangement/prob/ProBKernel.kt

+package b.language.server.proBMangement.prob
+
+
+import b.language.server.communication.Communicator
+import b.language.server.communication.CommunicatorInterface
+import b.language.server.dataStorage.ProBSettings
+import com.google.inject.Inject
+import com.google.inject.Injector
+import de.prob.animator.ReusableAnimator
+import de.prob.animator.command.CheckWellDefinednessCommand
+import de.prob.animator.command.GetMachineOperationInfos
+import de.prob.animator.domainobjects.ErrorItem
+import de.prob.exception.ProBError
+import de.prob.scripting.ClassicalBFactory
+import de.prob.scripting.FactoryProvider
+import de.prob.scripting.ModelFactory
+import de.prob.scripting.ModelTranslationError
+import de.prob.statespace.AnimationSelector
+import de.prob.statespace.StateSpace
+import de.prob.statespace.Trace
+import kotlinx.coroutines.flow.flowViaChannel
+import org.eclipse.lsp4j.Diagnostic
+import org.eclipse.lsp4j.MessageType
+import java.io.IOException
+
+/**
+ * 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 communicator : CommunicatorInterface) {
+
+
+    /**
+     * 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("unloading old machine", MessageType.Info)
+        unloadMachine()
+
+        val factory = injector.getInstance(FactoryProvider.factoryClassFromExtension(path.substringAfterLast(".")))
+
+        val informationListener = InformationListener(path)
+        animator.addWarningListener(informationListener)
+
+        Communicator.sendDebugMessage("loading new machine", MessageType.Info)
+
+        val problems = loadMachine(settings, path, factory)
+
+        communicator.sendDebugMessage("returning from kernel problems are ${problems.toString()}", MessageType.Info)
+
+        return listOf(informationListener.getInformation(), problems).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(settings: ProBSettings, path : String, factory : ModelFactory<*>): List<Diagnostic> {
+        communicator.sendDebugMessage("creating new state space", MessageType.Info)
+
+        val newStateSpace = animator.createStateSpace()
+        communicator.sendDebugMessage("setting preferences", MessageType.Info)
+        newStateSpace.changePreferences(prepareAdditionalSettings(settings))
+
+        val errors = mutableListOf<ErrorItem>()
+
+        try {
+            factory.extract(path).loadIntoStateSpace(newStateSpace)
+        } catch (e: IOException) {
+            communicator.sendDebugMessage("IOException ${e.message}", MessageType.Info)
+        } catch (e: ModelTranslationError) {
+            communicator.sendDebugMessage("ModelTranslationError ${e.message}", MessageType.Info)
+        } catch (e : ProBError){
+            errors.addAll(e.errors)
+        }
+
+        if(errors.none { errorItem -> errorItem.type == ErrorItem.Type.ERROR }) {
+            communicator.sendDebugMessage("No fatal errors found, continuing with option steps...", MessageType.Info)
+
+            if (settings.strictChecks) {
+                errors.addAll(newStateSpace.performExtendedStaticChecks())
+            }
+
+            try {
+                communicator.sendDebugMessage("executing optional steps", MessageType.Info)
+                executeAdditionalOptions(settings)
+            } catch (e: RuntimeException) {
+                communicator.sendDebugMessage("something bad happened, statespace was killed", MessageType.Warning)
+                newStateSpace.kill()
+            }
+
+        }
+
+        communicator.sendDebugMessage("processing errors", MessageType.Info)
+        newStateSpace.kill()
+        return convertErrorItems(errors, path)
+    }
+
+
+    /**
+     * 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){
+        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) {
+            assert(oldTrace.stateSpace === animator.currentStateSpace)
+            animationSelector.changeCurrentAnimation(null)
+            oldTrace.stateSpace.kill()
+        }
+    }
+
+
+    /**
+     * prepares a map with additional settings
+     * note that the -lint option is an extra call to the state space and must be performed elsewhere
+     * @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) {
+            settings["STRICT_CLASH_CHECKING"] = "TRUE"
+            settings["TYPE_CHECK_DEFINITIONS"] = "TRUE"
+        }else{
+            settings["STRICT_CLASH_CHECKING"] = "TRUE"
+            settings["TYPE_CHECK_DEFINITIONS"] = "TRUE"
+        }
+        if (proBSettings.strictChecks) {
+            settings["PERFORMANCE_INFO"] = "TRUE"
+        }else{
+            settings["PERFORMANCE_INFO"] = "TRUE"
+        }
+        return settings
+    }
+
+
+}
\ No newline at end of file

src/main/kotlin/b/language/server/proBMangement/prob/ProBKernelManager.kt

+package b.language.server.proBMangement.prob
+
+import b.language.server.communication.CommunicatorInterface
+import b.language.server.dataStorage.ProBSettings
+import b.language.server.dataStorage.Settings
+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 java.io.File
+import java.net.URI
+
+/**
+ * Creates the prob kernel access and maintenance
+ */
+class ProBKernelManager(private val communicator : CommunicatorInterface) : ProBInterface {
+
+    private var kernel : ProBKernel
+    private var probHome = "DEFAULT"
+
+    init{
+        kernel = setup()
+    }
+
+
+    /**
+     * @return an instance of prob kernel
+     */
+    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){
+            throw Exception("wrong path to prob $probHome")
+        }
+        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(probNewHome == "DEFAULT"){ //Use default prob
+                System.setProperty("prob.home", "null")
+                kernel = setup()
+                true
+            }
+            else {
+
+                val dict = File(probNewHome)
+                if (dict.exists() && dict.isDirectory) { // Use custom prob
+                    System.setProperty("prob.home", probNewHome)
+                    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
+       //Files.exists(Path.of(URI(uri)))
+
+        communicator.sendDebugMessage("try to use ${settings.probHome} as prob version instead of " + System.getProperty("prob.home"), MessageType.Info)
+        val result = checkProBVersionSetting(settings.probHome)
+        if(!result){
+          throw CouldNotFindProBHomeException("searched at ${settings.probHome} for prob but found nothing - make sure " +
+                  "you point to the prob directory not to probcli.sh/probcli")
+        }
+
+        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

src/main/kotlin/b/language/server/proBMangement/prob/ProBKernelModule.kt

+package b.language.server.proBMangement.prob
+
+import b.language.server.communication.CommunicatorInterface
+import com.google.inject.AbstractModule
+import de.prob.MainModule
+
+class ProBKernelModule(private val communicator : CommunicatorInterface) : AbstractModule() {
+    override fun configure() {
+        install(MainModule())
+        bind(CommunicatorInterface::class.java).toInstance(communicator)
+    }
+}
\ No newline at end of file

src/main/kotlin/b/language/server/proBMangement/prob/Util.kt

+package b.language.server.proBMangement.prob
+
+import de.prob.animator.domainobjects.ErrorItem
+import org.eclipse.lsp4j.Diagnostic
+import org.eclipse.lsp4j.DiagnosticSeverity
+import org.eclipse.lsp4j.Position
+import org.eclipse.lsp4j.Range
+
+fun convertErrorItems(errorItems: List<ErrorItem>, currentLoadedFile : String) : List<Diagnostic>{
+    return  errorItems.map { errorItem ->
+        errorItem.locations.map { location ->
+            Diagnostic(Range(
+                    Position(location.startLine - 1, location.startColumn),
+                    Position(location.endLine - 1, location.endColumn)),
+                    errorItem.message,
+                    getErrorItemType(errorItem.type),
+                    location.filename)
+        }.ifEmpty { //Fallback when errors from prob do not have position infos
+            listOf(Diagnostic(Range(
+                    Position(0,0),
+                    Position(0,0)),
+                    errorItem.message,
+                    getErrorItemType(errorItem.type),
+                    currentLoadedFile))
+        }
+    }.flatten()
+}
+
+fun getErrorItemType(errorItem: ErrorItem.Type) : DiagnosticSeverity{
+    return when(errorItem){
+        ErrorItem.Type.ERROR -> {
+            DiagnosticSeverity.Error
+        }
+        ErrorItem.Type.WARNING -> {
+            DiagnosticSeverity.Warning
+        }
+        ErrorItem.Type.INTERNAL_ERROR -> {
+            DiagnosticSeverity.Error
+        }
+        ErrorItem.Type.MESSAGE -> {
+            DiagnosticSeverity.Information
+        }
+        else -> {
+            DiagnosticSeverity.Error
+        }
+    }
+
+}
\ No newline at end of file