diff --git a/README.md b/README.md
index 9e9e2b76fae8e52b816354ed174c04cdc6fc1683..265d685ddda22909eb312da9b427b2b1fd3c9912 100644
--- a/README.md
+++ b/README.md
@@ -1,2 +1,29 @@
# 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
diff --git a/build.gradle.kts b/build.gradle.kts
index afd2a57b632cba5a5dc2c49ed222135a1bcee920..64696b8038502ae674ee0739e9297584712d9534 100644
--- a/build.gradle.kts
+++ b/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()
}
diff --git a/package.json b/package.json
index 69e2f5dfd8bca802113c5031604ac995f488546b..e2584051a9b8b91f3fa0063e746af11d5a0f7cae 100644
--- a/package.json
+++ b/package.json
@@ -1,6 +1,6 @@
{
"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": {
diff --git a/settings.gradle.kts b/settings.gradle.kts
index 260c6a0f7a1f9c9158a3c4e6d8446e7bbe56b020..feec1793567b5d0ec0cdcbe26602d82a00dd890a 100644
--- a/settings.gradle.kts
+++ b/settings.gradle.kts
@@ -8,3 +8,4 @@
*/
rootProject.name = "b-language-server"
+//includeBuild("../prob2_kernel/de.prob2.kernel")
\ No newline at end of file
diff --git a/src/main/kotlin/b/language/server/App.kt b/src/main/kotlin/b/language/server/App.kt
index 014cb395c7398e42d9f1ac5f07ef89818d3175ef..b22a97c6bd72322f572bb97d28c32b6bd41e01dc 100644
--- a/src/main/kotlin/b/language/server/App.kt
+++ b/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()
diff --git a/src/main/kotlin/b/language/server/BDocumentService.kt b/src/main/kotlin/b/language/server/BDocumentService.kt
index 065066c6a2cf862beb9be97aa8192c4090c7f360..3e09911c7f120f84a59a4fa8d86a18e8c2c729b1 100644
--- a/src/main/kotlin/b/language/server/BDocumentService.kt
+++ b/src/main/kotlin/b/language/server/BDocumentService.kt
@@ -1,17 +1,15 @@
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)
}
diff --git a/src/main/kotlin/b/language/server/BWorkspaceService.kt b/src/main/kotlin/b/language/server/BWorkspaceService.kt
index 603b6dad7bc4a52768419d0f987e8fa4c7f47a6c..6ed6d36fb5b84f20ff3321132083b81a23e119d6 100644
--- a/src/main/kotlin/b/language/server/BWorkspaceService.kt
+++ b/src/main/kotlin/b/language/server/BWorkspaceService.kt
@@ -1,22 +1,20 @@
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{
diff --git a/src/main/kotlin/b/language/server/Server.kt b/src/main/kotlin/b/language/server/Server.kt
index 274196fc846eae6d7fac39a1d18c45c9aae2ab81..4820acbcce74adcae54c6ec2ac99e422d03ebb8e 100644
--- a/src/main/kotlin/b/language/server/Server.kt
+++ b/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
diff --git a/src/main/kotlin/b/language/server/Util.kt b/src/main/kotlin/b/language/server/Util.kt
index d6798327e62bf97e58832cca9878201aec41e2c3..3a19addfe6be97581eae0ffdf58d9b2172a5b29d 100644
--- a/src/main/kotlin/b/language/server/Util.kt
+++ b/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))
}
+
+
diff --git a/src/main/kotlin/b/language/server/communication/Communicator.kt b/src/main/kotlin/b/language/server/communication/Communicator.kt
index 1d7e97c3983082a30d949e5377f1113056818d06..4e8e8c3eab8cdf618a65a7b72961547ed60876c8 100644
--- a/src/main/kotlin/b/language/server/communication/Communicator.kt
+++ b/src/main/kotlin/b/language/server/communication/Communicator.kt
@@ -1,6 +1,5 @@
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
diff --git a/src/main/kotlin/b/language/server/dataStorage/Position.kt b/src/main/kotlin/b/language/server/dataStorage/Position.kt
deleted file mode 100644
index 14e00846910be7754a8e37eaef51b9d21f26d946..0000000000000000000000000000000000000000
--- a/src/main/kotlin/b/language/server/dataStorage/Position.kt
+++ /dev/null
@@ -1,4 +0,0 @@
-package b.language.server.dataStorage
-
-
-class Position(var line : Int, var col : Int)
\ No newline at end of file
diff --git a/src/main/kotlin/b/language/server/dataStorage/ProBSettings.kt b/src/main/kotlin/b/language/server/dataStorage/ProBSettings.kt
new file mode 100644
index 0000000000000000000000000000000000000000..21828a5f228cf7b3c29d753b47717e8872cc16c1
--- /dev/null
+++ b/src/main/kotlin/b/language/server/dataStorage/ProBSettings.kt
@@ -0,0 +1,3 @@
+package b.language.server.dataStorage
+
+data class ProBSettings(val wdChecks : Boolean, val strictChecks : Boolean, val performanceHints : Boolean)
\ No newline at end of file
diff --git a/src/main/kotlin/b/language/server/dataStorage/Problem.kt b/src/main/kotlin/b/language/server/dataStorage/Problem.kt
deleted file mode 100644
index 75648c672771ab97bb1f3ca6423b704172cc2f89..0000000000000000000000000000000000000000
--- a/src/main/kotlin/b/language/server/dataStorage/Problem.kt
+++ /dev/null
@@ -1,18 +0,0 @@
-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)
-
diff --git a/src/main/kotlin/b/language/server/dataStorage/Settings.kt b/src/main/kotlin/b/language/server/dataStorage/Settings.kt
index 16e6730db74edd2ce3a6dbc40e27675f580e80b5..40708a60950e5603a7d112f26b9dfd53afd867f0 100644
--- a/src/main/kotlin/b/language/server/dataStorage/Settings.kt
+++ b/src/main/kotlin/b/language/server/dataStorage/Settings.kt
@@ -1,7 +1,6 @@
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)
diff --git a/src/main/kotlin/b/language/server/proBMangement/ProBInterface.kt b/src/main/kotlin/b/language/server/proBMangement/ProBInterface.kt
index 8c16106da28290fc85b37587012407f21af2db07..75060beb895e631bf9e62dfd79068537a2c350c1 100644
--- a/src/main/kotlin/b/language/server/proBMangement/ProBInterface.kt
+++ b/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
diff --git a/src/main/kotlin/b/language/server/proBMangement/prob/CouldNotFindProBHomeException.kt b/src/main/kotlin/b/language/server/proBMangement/prob/CouldNotFindProBHomeException.kt
new file mode 100644
index 0000000000000000000000000000000000000000..e4adfa316c5d0fae6fab84e783f691ca17013495
--- /dev/null
+++ b/src/main/kotlin/b/language/server/proBMangement/prob/CouldNotFindProBHomeException.kt
@@ -0,0 +1,3 @@
+package b.language.server.proBMangement.prob
+
+class CouldNotFindProBHomeException(message : String) : Exception(message)
\ No newline at end of file
diff --git a/src/main/kotlin/b/language/server/proBMangement/prob/ProBKernel.kt b/src/main/kotlin/b/language/server/proBMangement/prob/ProBKernel.kt
new file mode 100644
index 0000000000000000000000000000000000000000..4f351af266b9272f2f30e8a070f5b7228ad8a190
--- /dev/null
+++ b/src/main/kotlin/b/language/server/proBMangement/prob/ProBKernel.kt
@@ -0,0 +1,158 @@
+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
diff --git a/src/main/kotlin/b/language/server/proBMangement/prob/ProBKernelManager.kt b/src/main/kotlin/b/language/server/proBMangement/prob/ProBKernelManager.kt
new file mode 100644
index 0000000000000000000000000000000000000000..cc610a9cd61620dce0a562eab1b76d55ac1967ff
--- /dev/null
+++ b/src/main/kotlin/b/language/server/proBMangement/prob/ProBKernelManager.kt
@@ -0,0 +1,97 @@
+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
diff --git a/src/main/kotlin/b/language/server/proBMangement/prob/ProBKernelModule.kt b/src/main/kotlin/b/language/server/proBMangement/prob/ProBKernelModule.kt
new file mode 100644
index 0000000000000000000000000000000000000000..25465911a116652a3a391224b3e8aac7e766e4b5
--- /dev/null
+++ b/src/main/kotlin/b/language/server/proBMangement/prob/ProBKernelModule.kt
@@ -0,0 +1,12 @@
+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
diff --git a/src/main/kotlin/b/language/server/proBMangement/prob/Util.kt b/src/main/kotlin/b/language/server/proBMangement/prob/Util.kt
new file mode 100644
index 0000000000000000000000000000000000000000..335d7e180c2631e73e8adcbe9daf5c491fa8096a
--- /dev/null
+++ b/src/main/kotlin/b/language/server/proBMangement/prob/Util.kt
@@ -0,0 +1,48 @@
+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
diff --git a/src/main/kotlin/b/language/server/proBMangement/prob/WarningListener.kt b/src/main/kotlin/b/language/server/proBMangement/prob/WarningListener.kt
new file mode 100644
index 0000000000000000000000000000000000000000..7df1aac275b4086287523067fdcbc56357b6f4a5
--- /dev/null
+++ b/src/main/kotlin/b/language/server/proBMangement/prob/WarningListener.kt
@@ -0,0 +1,21 @@
+package b.language.server.proBMangement.prob
+
+import de.prob.animator.IWarningListener
+import de.prob.animator.domainobjects.ErrorItem
+import org.eclipse.lsp4j.Diagnostic
+
+/**
+ * Custom collector to collect warnings from prob kernel
+ */
+class InformationListener(val fallbackPath : String) : IWarningListener {
+ private val warningList : ArrayList<ErrorItem> = arrayListOf()
+
+
+ override fun warningsOccurred(warnings: MutableList<ErrorItem>?) {
+ warningList.addAll(warnings!!.toList())
+ }
+
+ fun getInformation() : List<Diagnostic>{
+ return convertErrorItems(warningList, fallbackPath)
+ }
+}
\ No newline at end of file
diff --git a/src/main/kotlin/b/language/server/proBMangement/probCli/CommandCouldNotBeExecutedException.kt b/src/main/kotlin/b/language/server/proBMangement/probCli/CommandCouldNotBeExecutedException.kt
deleted file mode 100644
index d4ed1f9dbf3d8592d9d23f7c7c48b11484c9b005..0000000000000000000000000000000000000000
--- a/src/main/kotlin/b/language/server/proBMangement/probCli/CommandCouldNotBeExecutedException.kt
+++ /dev/null
@@ -1,3 +0,0 @@
-package b.language.server.proBMangement.probCli
-
-class CommandCouldNotBeExecutedException(message: String?) : Exception(message)
\ No newline at end of file
diff --git a/src/main/kotlin/b/language/server/proBMangement/probCli/PathCouldNotBeCreatedException.kt b/src/main/kotlin/b/language/server/proBMangement/probCli/PathCouldNotBeCreatedException.kt
deleted file mode 100644
index e359ab5367b11626dbbcdf93ad2ceb9df50265bd..0000000000000000000000000000000000000000
--- a/src/main/kotlin/b/language/server/proBMangement/probCli/PathCouldNotBeCreatedException.kt
+++ /dev/null
@@ -1,3 +0,0 @@
-package b.language.server.proBMangement.probCli
-
-class PathCouldNotBeCreatedException(message: String?) : Exception(message)
\ No newline at end of file
diff --git a/src/main/kotlin/b/language/server/proBMangement/probCli/ProBCommandLineAccess.kt b/src/main/kotlin/b/language/server/proBMangement/probCli/ProBCommandLineAccess.kt
deleted file mode 100644
index 3f18caef3e27d7d90c0c172086729431926c4e88..0000000000000000000000000000000000000000
--- a/src/main/kotlin/b/language/server/proBMangement/probCli/ProBCommandLineAccess.kt
+++ /dev/null
@@ -1,252 +0,0 @@
-package b.language.server.proBMangement.probCli
-
-import b.language.server.communication.CommunicatorInterface
-import b.language.server.dataStorage.Problem
-import b.language.server.dataStorage.Settings
-import b.language.server.proBMangement.ProBInterface
-import com.google.gson.Gson
-import org.eclipse.lsp4j.*
-import java.io.*
-import java.net.URI
-
-
-/**
- * Access ProB via command line
- */
-class ProBCommandLineAccess(val communicator : CommunicatorInterface) : ProBInterface {
- /**
- * Checks the given document with the help of ProB; Will setup all needed steps to ensure a clean process
- * @param uri the source to check
- * @return a list of all problems found
- */
- override fun checkDocument(uri : String, settings: Settings): List<Diagnostic> {
- communicator.sendDebugMessage("checking document ($uri) with proB", MessageType.Info )
- val realUri = URI(uri)
- val path = File(realUri.path)
- val errorPath = File(path.parent + "/tmp/_error.json")
- val errorDict = File(path.parent + "/tmp")
-
- val result = createFolder(errorDict, errorPath)
- if(!result){
- throw PathCouldNotBeCreatedException("The Path leading to $errorPath has not been created due some issue.")
- }
- communicator.sendDebugMessage("creation successful", MessageType.Info)
- val command = buildCommand(settings, path, errorPath)
- communicator.sendDebugMessage("sending command <$command> to proB", MessageType.Info)
-
- performActionOnDocument(command)
-
- val problems = readProblems(errorPath.path)
- communicator.sendDebugMessage("deleting tmp", MessageType.Info )
- errorDict.delete()
- communicator.sendDebugMessage("found the following problems: $problems", MessageType.Info)
-
- return transformProblems(problems)
- }
-
-
- /**
- * Constructs the commandline call to proB depending on the given settings
- * Produces something like
- * [/home/sebastian/prob_prolog/probcli, -p, MAX_INITIALISATIONS, 0, -version , -p, NDJSON_ERROR_LOG_FILE ,...]
- * @param settings the settings for the document
- * @param fileToCheck the current documents address
- * @param errorPath the path to dump the ndjson message
- * @return the execution ready command
- */
- fun buildCommand(settings : Settings, fileToCheck : File, errorPath : File) : ProcessBuilder{
- val additionalArgument = "-p"
- val version = "-version"
- val configuration = "MAX_INITIALISATIONS"
- val maxInitAmount = "0"
- val ndjson = "NDJSON_ERROR_LOG_FILE"
- val releaseJavaParser = "-release_java_parser"
- val wdCheck = "-wd-check"
- val strictClashChecking = "STRICT_CLASH_CHECKING"
- val typeCheckDefinitions = "TYPE_CHECK_DEFINITIONS"
- val lint = "-lint"
- val tRUE = "TRUE"
- val performanceHints = "" +
- "PERFORMANCE_INFO"
-
-
- //voiding stdout and stderr
- val outputSink = if(System.getProperty("os.name").toLowerCase().contains("win")){
- File("NUL")
- }else{
- File("/dev/null")
- }
-
- communicator.sendDebugMessage("voiding err and output to: ${outputSink.absolutePath}", MessageType.Info)
-
- val command = mutableListOf<String>()
-
-
- command.add(settings.probHome.absolutePath)
- command.add(additionalArgument)
- command.add(configuration)
- command.add(maxInitAmount)
- command.add(version)
- command.add(additionalArgument)
- command.add(ndjson)
- command.add(errorPath.absolutePath)
-
- if (settings.wdChecks){
- command.add(wdCheck)
- command.add(releaseJavaParser)
- }
-
- if(settings.strictChecks){
- command.add(additionalArgument)
- command.add(strictClashChecking)
- command.add(tRUE)
- command.add(additionalArgument)
- command.add(typeCheckDefinitions)
- command.add(tRUE)
- command.add(lint)
- }
-
-
- if(settings.performanceHints) {
- command.add(additionalArgument)
- command.add(performanceHints)
- command.add(tRUE)
- }
-
- command.add(fileToCheck.absolutePath)
-
-
-
- communicator.sendDebugMessage("creating cli call $command", MessageType.Info)
-
- try {
- return ProcessBuilder()
- .command(command)
- .redirectOutput(outputSink)
- .redirectError(outputSink)
-
- }catch (e : IllegalArgumentException){
- communicator.sendDebugMessage("illegal argument exception ${e.cause}", MessageType.Info)
- }
- return ProcessBuilder()
- }
-
-
- /**
- * Creates the tmp folder and an empty ndjson file; will recreate an empty ndjson file to ensure clean messages
- * @param errorDict the path of the tmp dict
- * @param errorPath the path to the error file
- * @return success of the action
- */
- fun createFolder(errorDict : File, errorPath: File) : Boolean{
- communicator.sendDebugMessage("creating errorDict $errorDict and errorFile $errorPath", MessageType.Info)
- errorDict.mkdirs()
- FileWriter(errorPath, false).close()
- errorPath.deleteOnExit()
- errorDict.deleteOnExit()
- return errorDict.exists() && errorPath.exists()
- }
-
- /**
- * Executes the given command
- * @param command to execute
- * @throws IOException failed to reach probcli
- */
- private fun performActionOnDocument(command : ProcessBuilder) {
- communicator.sendDebugMessage("execution of ${command.command()}", MessageType.Info)
-
- val process: Process = command.start()
-
- communicator.sendDebugMessage("waiting for process to return", MessageType.Info)
-
- // process.waitFor() //we must wait here to ensure correct behavior when reading an error
- val exitStatus = process.waitFor()
- communicator.sendDebugMessage("exit status of execution: $exitStatus", MessageType.Info)
- }
-
-
-
- /**
- * Reads the errors and transforms them to java objects
- * @param path the path to the error document
- * @return the list of read errors
- */
- fun readProblems(path : String): List<Problem> {
- val jsonStrings : ArrayList<String> = ArrayList()
- BufferedReader(FileReader(path)).use { br ->
- var line: String?
- while (br.readLine().also { line = it } != null) {
- jsonStrings.add(line!!)
- }
- }
-
- val strings = jsonStrings.toList().map { string -> Gson().fromJson(string, Problem::class.java) }
- return strings
-
- }
-
- /**
- * Transforms errors to error messages
- * @param problems the list of errors to transform
- * @return the transformed errors
- */
- fun transformProblems(problems : List<Problem>): List<Diagnostic> {
- return problems.
- /**
- * Some errors from prob_cli have negative values when there is no exact error location - we set them
- * to the first line
- */
- map{ problem ->
- if (problem.start.line == -1 && problem.start.col == -1 &&
- problem.end.line == -1 && problem.end.col == -1)
- {
- print(Integer.MAX_VALUE)
- Problem(problem.type,
- problem.message,
- problem.reason,
- problem.file,
- b.language.server.dataStorage.Position(1,0),
- b.language.server.dataStorage.Position(1, Integer.MAX_VALUE),
- problem.version)
- }
- else{
- /**
- * Lines are off by one when they get out of vscode
- */
- problem.start.line = problem.start.line - 1
- problem.end.line = problem.end.line - 1
-
- problem
- }
- }
- .map { problem ->
- val range = Range(
- Position(problem.start.line, problem.start.col),
- Position(problem.end.line, problem.end.col))
- val diagnostic = Diagnostic(
- range,
- problem.message,
- when (problem.type) {
- "error" -> {
- DiagnosticSeverity.Error
- }
- "warning" -> {
- DiagnosticSeverity.Warning
- }
- "information" -> {
- DiagnosticSeverity.Information
- }
- else -> {
- DiagnosticSeverity.Hint
- }
- },
- problem.file
- )
- diagnostic.relatedInformation =
- listOf(DiagnosticRelatedInformation(Location(problem.file, range), "probcli v.${problem.version}"))
- diagnostic
-
- }
- }
-
-}
\ No newline at end of file
diff --git a/src/test/kotlin/b/language/server/ProBCommandLineTest.kt b/src/test/kotlin/b/language/server/ProBCommandLineTest.kt
deleted file mode 100644
index 6ea73886635bfd4d941aee314186b307ae0fe397..0000000000000000000000000000000000000000
--- a/src/test/kotlin/b/language/server/ProBCommandLineTest.kt
+++ /dev/null
@@ -1,197 +0,0 @@
-package b.language.server
-
-import b.language.server.communication.Communicator
-import b.language.server.dataStorage.Position
-import b.language.server.dataStorage.Problem
-import b.language.server.dataStorage.Settings
-import b.language.server.proBMangement.probCli.ProBCommandLineAccess
-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
- fun test_readProblems(@TempDir tempPath : File = File("tmp"))
- {
- val file = File(tempPath.path+"/tmp.txt")
- val problemToWrite = Problem(message = "Test", file = "test.mch", reason = "test reason", version = "test",
- start = Position(1,1), end = Position(1,1), type = "test")
- file.writeText(Gson().toJson(problemToWrite))
-
- val problems = ProBCommandLineAccess(Communicator).readProblems(file.path)
-
- val problem = problems.first()
-
- assertEquals(problemToWrite.version, problem.version)
- assertEquals(problemToWrite.end.col, problem.end.col)
- assertEquals(problemToWrite.end.line, problemToWrite.end.line)
- assertEquals(problemToWrite.start.col, problem.start.col)
- assertEquals(problemToWrite.start.line, problemToWrite.start.line)
- assertEquals(problemToWrite.file, problem.file)
- assertEquals(problemToWrite.message, problem.message)
- assertEquals(problemToWrite.reason, problem.reason)
-
- }
-
- @Test
- fun test_buildCommand_everything_activated(@TempDir tempPath : File = File("tmp")){
- val testSettings = Settings()
- val tempFile = File(tempPath.path+"/m.mch")
- val command = ProBCommandLineAccess().buildCommand(testSettings, tempFile, tempPath)
- assertEquals("~/prob_prolog/probcli.sh -p MAX_INITIALISATIONS 0 " +
- "-version " +
- "-p PERFORMANCE_INFO TRUE " +
- "-p STRICT_CLASH_CHECKING TRUE " +
- "-p TYPE_CHECK_DEFINITIONS TRUE -lint " +
- "-wd-check -release_java_parser ${tempFile.path} " +
- "-p NDJSON_ERROR_LOG_FILE $tempPath", command)
- }
-
- @Test
- fun test_buildCommand_everything_not_strict(@TempDir tempPath : File = File("tmp")){
- val testSettings = Settings(strictChecks = false)
- val tempFile = File(tempPath.path+"/m.mch")
- val command = ProBCommandLineAccess().buildCommand(testSettings, tempFile, tempPath)
- assertEquals("~/prob_prolog/probcli.sh -p MAX_INITIALISATIONS 0 " +
- "-version " +
- "-p PERFORMANCE_INFO TRUE " +
- "-wd-check -release_java_parser ${tempFile.path} " +
- "-p NDJSON_ERROR_LOG_FILE $tempPath", command)
- }
-
-
- @Test
- fun test_buildCommand_everything_not_wd(@TempDir tempPath : File = File("tmp")){
- val testSettings = Settings(wdChecks = false)
- val tempFile = File(tempPath.path+"/m.mch")
- val command = ProBCommandLineAccess().buildCommand(testSettings, tempFile, tempPath)
- assertEquals("~/prob_prolog/probcli.sh -p MAX_INITIALISATIONS 0 " +
- "-version " +
- "-p PERFORMANCE_INFO TRUE " +
- "-p STRICT_CLASH_CHECKING TRUE " +
- "-p TYPE_CHECK_DEFINITIONS TRUE -lint " +
- "${tempFile.path} " +
- "-p NDJSON_ERROR_LOG_FILE $tempPath", command)
- }
-
-
- @Test
- fun test_buildCommand_everything_not_performanceHints(@TempDir tempPath : File = File("tmp")){
- val testSettings = Settings(performanceHints = false)
- val tempFile = File(tempPath.path+"/m.mch")
- val command = ProBCommandLineAccess().buildCommand(testSettings, tempFile, tempPath)
- assertEquals("~/prob_prolog/probcli.sh -p MAX_INITIALISATIONS 0 " +
- "-version " +
- "-p STRICT_CLASH_CHECKING TRUE " +
- "-p TYPE_CHECK_DEFINITIONS TRUE -lint " +
- "-wd-check -release_java_parser ${tempFile.path} " +
- "-p NDJSON_ERROR_LOG_FILE $tempPath", command)
- }
-
-
- @Test
- fun test_transformProblems_negative_range(){
- val problemFile = "test.mch"
- val message = "Test"
- val version = "test"
- val testProblem = Problem(message = message, file = problemFile, reason = "test reason", version = version,
- start = Position(-1,-1), end = Position(-1,-1), type = "error")
-
- val transformedProblem = ProBCommandLineAccess().transformProblems(listOf(testProblem)).first()
-
- val diagnostic = Diagnostic(Range(
- org.eclipse.lsp4j.Position(1,0),
- org.eclipse.lsp4j.Position(1, Integer.MAX_VALUE)), message, DiagnosticSeverity.Error, problemFile, " probcli v.$version" )
- assertEquals(diagnostic, transformedProblem)
-
- }
-
-
- @Test
- fun test_transformProblems_error(){
- val problemFile = "test.mch"
- val message = "Test"
- val version = "test"
- val testProblem = Problem(message = message, file = problemFile, reason = "test reason", version = version,
- start = Position(32,54), end = Position(54,65), type = "error")
-
- val transformedProblem = ProBCommandLineAccess().transformProblems(listOf(testProblem)).first()
-
- val diagnostic = Diagnostic(Range(
- org.eclipse.lsp4j.Position(31,54),
- org.eclipse.lsp4j.Position(53, 65)), message, DiagnosticSeverity.Error, problemFile, " probcli v.$version" )
- assertEquals(diagnostic, transformedProblem)
-
- }
-
-
- @Test
- fun test_transformProblems_warning(){
- val problemFile = "test.mch"
- val message = "Test"
- val version = "test"
- val testProblem = Problem(message = message, file = problemFile, reason = "test reason", version = version,
- start = Position(32,54), end = Position(54,65), type = "warning")
-
- val transformedProblem = ProBCommandLineAccess().transformProblems(listOf(testProblem)).first()
-
- val diagnostic = Diagnostic(Range(
- org.eclipse.lsp4j.Position(31,54),
- org.eclipse.lsp4j.Position(53, 65)), message, DiagnosticSeverity.Warning, problemFile, " probcli v.$version" )
- assertEquals(diagnostic, transformedProblem)
-
- }
-
- @Test
- fun test_transformProblems_information(){
- val problemFile = "test.mch"
- val message = "Test"
- val version = "test"
- val testProblem = Problem(message = message, file = problemFile, reason = "test reason", version = version,
- start = Position(32,54), end = Position(54,65), type = "information")
-
- val transformedProblem = ProBCommandLineAccess().transformProblems(listOf(testProblem)).first()
-
- val diagnostic = Diagnostic(Range(
- org.eclipse.lsp4j.Position(31,54),
- org.eclipse.lsp4j.Position(53, 65)), message, DiagnosticSeverity.Information, problemFile, " probcli v.$version" )
- assertEquals(diagnostic, transformedProblem)
-
- }
-
-
- @Test
- fun test_transformProblems_hint(){
- val problemFile = "test.mch"
- val message = "Test"
- val version = "test"
- val testProblem = Problem(message = message, file = problemFile, reason = "test reason", version = version,
- start = Position(32,54), end = Position(54,65), type = "something else")
-
- val transformedProblem = ProBCommandLineAccess().transformProblems(listOf(testProblem)).first()
-
- val diagnostic = Diagnostic(Range(
- org.eclipse.lsp4j.Position(31,54),
- org.eclipse.lsp4j.Position(5, 65)), message, DiagnosticSeverity.Hint, problemFile, " probcli v.$version" )
- assertEquals(diagnostic, transformedProblem)
-
- }
-
-
- @Test
- fun test_createFolders_success(@TempDir tempPath : File = File("tmp")){
- val errorDict = File(tempPath.path+"/tmp")
- val errorPath = File(tempPath.path+"/tmp/hallo.njson")
- val result = ProBCommandLineAccess().createFolder(errorDict, errorPath)
- assertTrue(result)
- }
-*/
-
-}
\ No newline at end of file
diff --git a/src/test/kotlin/b/language/server/prob2/proBMangement/UtilTest.kt b/src/test/kotlin/b/language/server/prob2/proBMangement/UtilTest.kt
new file mode 100644
index 0000000000000000000000000000000000000000..0eea8cf11c1a91a295309e6f67f06cda0e611535
--- /dev/null
+++ b/src/test/kotlin/b/language/server/prob2/proBMangement/UtilTest.kt
@@ -0,0 +1,68 @@
+package b.language.server.prob2.proBMangement
+
+import b.language.server.proBMangement.prob.convertErrorItems
+import b.language.server.proBMangement.prob.getErrorItemType
+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
+import org.junit.jupiter.api.Test
+import kotlin.test.assertEquals
+
+class UtilTest {
+
+ /**
+ * as we using functional programming we don´t test the logic but the functionality
+ */
+ @Test
+ fun generateErrorItem()
+ {
+ val startLine = 100
+ val statCol = 100
+ val endLine = 101
+ val endCol = 101
+ val message = "hello"
+ val file = "/test"
+
+ val errorItem = ErrorItem(message, ErrorItem.Type.INTERNAL_ERROR,
+ listOf(ErrorItem.Location(file, startLine,statCol,endLine,endCol)))
+
+ val diagnostic = Diagnostic(
+ Range(
+ Position(startLine-1, statCol),
+ Position(endLine-1, endCol)),
+ message, DiagnosticSeverity.Error, file)
+
+ val errorItemAfter = convertErrorItems(listOf(errorItem)).first()
+
+ assertEquals(diagnostic, errorItemAfter)
+
+ }
+
+ @Test
+ fun errorCodeTranslation_Error1()
+ {
+ val result = getErrorItemType(ErrorItem.Type.INTERNAL_ERROR)
+
+ assertEquals(DiagnosticSeverity.Error, result)
+ }
+
+ @Test
+ fun errorCodeTranslation_Error2()
+ {
+ val result = getErrorItemType(ErrorItem.Type.ERROR)
+
+ assertEquals(DiagnosticSeverity.Error, result)
+ }
+
+ @Test
+ fun errorCodeTranslation_Warning()
+ {
+ val result = getErrorItemType(ErrorItem.Type.WARNING)
+
+ assertEquals(DiagnosticSeverity.Warning, result)
+ }
+
+
+}
\ No newline at end of file
diff --git a/src/test/resources/Lift.mch b/src/test/resources/Lift.mch
new file mode 100644
index 0000000000000000000000000000000000000000..2aa64ac79146448a2b7f351d4dbf080844e7484d
--- /dev/null
+++ b/src/test/resources/Lift.mch
@@ -0,0 +1,19 @@
+MACHINE Lift
+
+VARIABLES floor
+
+INVARIANT floor : 0..100 /* NAT */
+
+INITIALISATION floor :=
+
+
+
+
+OPER1ATIONS
+
+ inc = PRE floor<100 THEN floor := floor + 1 END ;
+ dec = PRE floor>0 THEN floor := floor - 1 END;
+ open_door = skip;
+ close_door = skip
+
+END