From 594cd2f6b27491fe8a2c015cf87f5b93b5c95cbd Mon Sep 17 00:00:00 2001
From: SeeBasTStick <sebastian.stock@hhu.de>
Date: Mon, 17 Aug 2020 11:49:49 +0200
Subject: [PATCH] added prob2 kernel access and some tests
---
.../b/language/server/BDocumentService.kt | 18 ++----
src/main/kotlin/b/language/server/Server.kt | 2 -
.../server/proBMangement/ProBFactory.kt | 16 ++++++
.../server/proBMangement/ProBInterface.kt | 3 +-
.../proBMangement/WrongPathException.kt | 3 +
.../proBMangement/prob2/MyWarningListener.kt | 2 +-
.../server/proBMangement/prob2/ProBKernel.kt | 57 ++++++++++---------
.../proBMangement/prob2/ProBKernelManager.kt | 48 ++++++++++++----
.../b/language/server/ProBCommandLineTest.kt | 5 +-
.../communication/DummyCommunication.kt | 49 ++++++++++++++++
.../proBMangement/ProBKernelManagerTest.kt | 37 ++++++++++++
11 files changed, 185 insertions(+), 55 deletions(-)
create mode 100644 src/main/kotlin/b/language/server/proBMangement/ProBFactory.kt
create mode 100644 src/main/kotlin/b/language/server/proBMangement/WrongPathException.kt
create mode 100644 src/test/kotlin/b/language/server/communication/DummyCommunication.kt
create mode 100644 src/test/kotlin/b/language/server/prob2/proBMangement/ProBKernelManagerTest.kt
diff --git a/src/main/kotlin/b/language/server/BDocumentService.kt b/src/main/kotlin/b/language/server/BDocumentService.kt
index f13ee1a..057d5af 100644
--- a/src/main/kotlin/b/language/server/BDocumentService.kt
+++ b/src/main/kotlin/b/language/server/BDocumentService.kt
@@ -1,16 +1,16 @@
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.probCli.ProBCommandLineAccess
+import b.language.server.proBMangement.ProBFactory
import b.language.server.proBMangement.ProBInterface
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, private val communicator: CommunicatorInterface) : TextDocumentService {
+class BDocumentService(private val server: Server,
+ private val communicator: CommunicatorInterface,
+ private val proBFactory: ProBFactory = ProBFactory()) : TextDocumentService {
private val documents = ConcurrentHashMap<String, String>()
private val issueTracker : ConcurrentHashMap<String, Set<String>> = ConcurrentHashMap()
@@ -43,7 +43,7 @@ class BDocumentService(private val server: Server, private val communicator: Com
/**
* checks a document via prob an the set options
- * @param the uri to perform actions on
+ * @param currentUri uri to perform actions on
*/
fun checkDocument(currentUri : String){
@@ -52,7 +52,7 @@ class BDocumentService(private val server: Server, private val communicator: Com
clientSettings.thenAccept{ settings ->
communicator.setDebugMode(settings.debugMode)
- val prob : ProBInterface = ProBCommandLineAccess(communicator)
+ val prob : ProBInterface = proBFactory.getProBAccess(communicator)
communicator.sendDebugMessage("settings are $settings", MessageType.Info)
try{
@@ -64,12 +64,6 @@ class BDocumentService(private val server: Server, private val communicator: Com
invalidFiles.forEach{uri -> communicator.publishDiagnostics(PublishDiagnosticsParams(uri, listOf()))}
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)
diff --git a/src/main/kotlin/b/language/server/Server.kt b/src/main/kotlin/b/language/server/Server.kt
index c0bfd91..0f4a0f7 100644
--- a/src/main/kotlin/b/language/server/Server.kt
+++ b/src/main/kotlin/b/language/server/Server.kt
@@ -5,12 +5,10 @@ import b.language.server.dataStorage.Settings
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{
diff --git a/src/main/kotlin/b/language/server/proBMangement/ProBFactory.kt b/src/main/kotlin/b/language/server/proBMangement/ProBFactory.kt
new file mode 100644
index 0000000..63efff8
--- /dev/null
+++ b/src/main/kotlin/b/language/server/proBMangement/ProBFactory.kt
@@ -0,0 +1,16 @@
+package b.language.server.proBMangement
+
+import b.language.server.communication.CommunicatorInterface
+import b.language.server.proBMangement.prob2.ProBKernelManager
+
+
+/**
+ * Generate new Instances of ProBKernelManger
+ */
+class ProBFactory {
+
+ fun getProBAccess(commuicator : CommunicatorInterface) : ProBInterface{
+ return ProBKernelManager(commuicator)
+ }
+
+}
\ No newline at end of file
diff --git a/src/main/kotlin/b/language/server/proBMangement/ProBInterface.kt b/src/main/kotlin/b/language/server/proBMangement/ProBInterface.kt
index 8c16106..75060be 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/WrongPathException.kt b/src/main/kotlin/b/language/server/proBMangement/WrongPathException.kt
new file mode 100644
index 0000000..0fa842a
--- /dev/null
+++ b/src/main/kotlin/b/language/server/proBMangement/WrongPathException.kt
@@ -0,0 +1,3 @@
+package b.language.server.proBMangement
+
+class WrongPathException (message: String?) : Exception(message)
\ No newline at end of file
diff --git a/src/main/kotlin/b/language/server/proBMangement/prob2/MyWarningListener.kt b/src/main/kotlin/b/language/server/proBMangement/prob2/MyWarningListener.kt
index 2418807..8fb2f1a 100644
--- a/src/main/kotlin/b/language/server/proBMangement/prob2/MyWarningListener.kt
+++ b/src/main/kotlin/b/language/server/proBMangement/prob2/MyWarningListener.kt
@@ -13,6 +13,6 @@ class MyWarningListener : IWarningListener {
}
fun getWarnings() : List<Diagnostic>{
- return convertErrorItems(warningList, DiagnosticSeverity.Warning)
+ return convertErrorItems(warningList)
}
}
\ No newline at end of file
diff --git a/src/main/kotlin/b/language/server/proBMangement/prob2/ProBKernel.kt b/src/main/kotlin/b/language/server/proBMangement/prob2/ProBKernel.kt
index 7b87aba..ce43d09 100644
--- a/src/main/kotlin/b/language/server/proBMangement/prob2/ProBKernel.kt
+++ b/src/main/kotlin/b/language/server/proBMangement/prob2/ProBKernel.kt
@@ -1,4 +1,5 @@
+import b.language.server.communication.Communicator
import b.language.server.dataStorage.ProBSettings
import b.language.server.proBMangement.prob2.MyWarningListener
import b.language.server.proBMangement.prob2.convertErrorItems
@@ -14,14 +15,40 @@ import de.prob.statespace.AnimationSelector
import de.prob.statespace.StateSpace
import de.prob.statespace.Trace
import org.eclipse.lsp4j.Diagnostic
-import org.eclipse.lsp4j.DiagnosticSeverity
+import org.eclipse.lsp4j.MessageType
import java.io.IOException
-import java.nio.file.Paths
class ProBKernel @Inject constructor(private val injector : Injector, val classicalBFactory : ClassicalBFactory,
private val animationSelector: AnimationSelector, private val animator : ReusableAnimator) {
+ private val communicator : Communicator = Communicator
+
+ fun check(path : String, settings : ProBSettings) : List<Diagnostic>{
+ communicator.sendDebugMessage("Unload old machine", MessageType.Info)
+ unloadMachine()
+ val factory = injector.getInstance(FactoryProvider.factoryClassFromExtension(path.substringAfterLast(".")))
+ val warningListener = MyWarningListener()
+ animator.addWarningListener(warningListener)
+ val parseErrors = mutableListOf<Diagnostic>()
+ communicator.sendDebugMessage("Load new machine", MessageType.Info)
+ loadMachine(
+ java.util.function.Function { stateSpace : StateSpace ->
+ try {
+ val extractedModel = factory.extract(path)
+ val stateSpaceWithSettings = extractedModel.load(prepareAdditionalSettings(settings))
+ extractedModel.loadIntoStateSpace(stateSpaceWithSettings)
+ } catch (e: IOException) {
+ throw RuntimeException(e)
+ } catch (e: ModelTranslationError) {
+ throw RuntimeException(e)
+ }catch (e : ProBError){
+ parseErrors.addAll(convertErrorItems(e.errors))
+ }
+ Trace(stateSpace)
+ }, settings)
+ return listOf(warningListener.getWarnings(), parseErrors).flatten()
+ }
private fun loadMachine(newTraceCreator :java.util.function.Function<StateSpace, Trace>, settings: ProBSettings){
val newStateSpace = animator.createStateSpace()
@@ -35,7 +62,7 @@ class ProBKernel @Inject constructor(private val injector : Injector, val classi
}
private fun executeAdditionalOptions(settings : ProBSettings){
- val newStateSpace = animator.createStateSpace()
+ animator.createStateSpace()
if(settings.wdChecks){
animator.execute(CheckWellDefinednessCommand())
}
@@ -51,30 +78,8 @@ class ProBKernel @Inject constructor(private val injector : Injector, val classi
}
}
- fun check(path : String, settings : ProBSettings) : List<Diagnostic>{
- unloadMachine()
- val factory = injector.getInstance(FactoryProvider.factoryClassFromExtension(path.substringAfterLast(".")))
- val warningListener = MyWarningListener()
- animator.addWarningListener(warningListener)
- val parseErrors = mutableListOf<Diagnostic>()
- loadMachine(
- java.util.function.Function { stateSpace : StateSpace ->
- try {
- factory.extract(path).load(prepareAdditionalSettings(settings))
- loadIntoStateSpace(stateSpace)
- } catch (e: IOException) {
- throw RuntimeException(e)
- } catch (e: ModelTranslationError) {
- throw RuntimeException(e)
- }catch (e : ProBError){
- parseErrors.addAll(convertErrorItems(e.errors))
- }
- Trace(stateSpace)
- }, settings)
- return listOf(warningListener.getWarnings(), parseErrors).flatten()
- }
- fun prepareAdditionalSettings(proBSettings: ProBSettings): MutableMap<String, String> {
+ private fun prepareAdditionalSettings(proBSettings: ProBSettings): MutableMap<String, String> {
val settings = mutableMapOf<String, String>()
if(proBSettings.performanceHints) {
settings["STRICT_CLASH_CHECKING"] = "TRUE"
diff --git a/src/main/kotlin/b/language/server/proBMangement/prob2/ProBKernelManager.kt b/src/main/kotlin/b/language/server/proBMangement/prob2/ProBKernelManager.kt
index 4da6661..5691d3c 100644
--- a/src/main/kotlin/b/language/server/proBMangement/prob2/ProBKernelManager.kt
+++ b/src/main/kotlin/b/language/server/proBMangement/prob2/ProBKernelManager.kt
@@ -1,39 +1,67 @@
package b.language.server.proBMangement.prob2
import ProBKernel
+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 b.language.server.proBMangement.ProBInterface
+import b.language.server.proBMangement.WrongPathException
import com.google.inject.Guice
import com.google.inject.Stage
import org.eclipse.lsp4j.Diagnostic
+import org.eclipse.lsp4j.MessageType
/**
* Setup a connection to ProB2 Kernel
*/
-class ProBKernelManager : ProBInterface{
+class ProBKernelManager(private val communicator : CommunicatorInterface) : ProBInterface{
private lateinit var kernel : ProBKernel
+ private var lastProBHome : String = "DEFAULT"
- /**
+ /**
* 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> {
val proBSettings = ProBSettings(settings.wdChecks, settings.strictChecks, settings.performanceHints)
val probHome = settings.probHome.absolutePath
- if(probHome != "DEFAULT" && !this::kernel.isInitialized)
- {
- if(probHome != "DEFAULT"){
- System.setProperty("prob.home", probHome)
- }
- val injector = Guice.createInjector(Stage.PRODUCTION, ProBKernelModule())
- kernel = injector.getInstance(ProBKernel::class.java)
+ communicator.sendDebugMessage("checking document", MessageType.Info)
+
+ return if(probHome == lastProBHome && this::kernel.isInitialized){
+ kernel.check(uri, proBSettings)
+ }else{
+ lastProBHome = probHome
+ setup(probHome).check(uri, proBSettings)
}
- return kernel.check(uri, proBSettings)
+ }
+
+ /**
+ * @param probHome the home of prob; DEFAULT for the prob version delivered with the library
+ * @return an instance of prob kernel
+ */
+ fun setup(probHome : String) : ProBKernel{
+ if(probHome != "DEFAULT"){
+ System.setProperty("prob.home", probHome)
+ communicator.sendDebugMessage("$probHome selected", MessageType.Info)
+ }else{
+ communicator.sendDebugMessage("default prob selected", MessageType.Info)
+ }
+
+ val injector = Guice.createInjector(Stage.PRODUCTION, ProBKernelModule())
+ 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 WrongPathException("wrong path to prob $probHome")
+ }
+ return kernel
}
diff --git a/src/test/kotlin/b/language/server/ProBCommandLineTest.kt b/src/test/kotlin/b/language/server/ProBCommandLineTest.kt
index 2f9a74f..06bec3e 100644
--- a/src/test/kotlin/b/language/server/ProBCommandLineTest.kt
+++ b/src/test/kotlin/b/language/server/ProBCommandLineTest.kt
@@ -3,7 +3,6 @@ package b.language.server
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
@@ -15,7 +14,7 @@ import kotlin.test.assertEquals
import kotlin.test.assertTrue
class ProBCommandLineTest{
-
+ /*
@Test
fun test_readProblems(@TempDir tempPath : File = File("tmp"))
{
@@ -191,6 +190,6 @@ class ProBCommandLineTest{
val result = ProBCommandLineAccess().createFolder(errorDict, errorPath)
assertTrue(result)
}
-
+*/
}
\ No newline at end of file
diff --git a/src/test/kotlin/b/language/server/communication/DummyCommunication.kt b/src/test/kotlin/b/language/server/communication/DummyCommunication.kt
new file mode 100644
index 0000000..e6de95d
--- /dev/null
+++ b/src/test/kotlin/b/language/server/communication/DummyCommunication.kt
@@ -0,0 +1,49 @@
+package b.language.server.communication
+
+import b.language.server.communication.CommunicatorInterface
+import org.eclipse.lsp4j.MessageType
+import org.eclipse.lsp4j.PublishDiagnosticsParams
+
+
+/**
+ * The Communicator is a side effect class, we don´t want side effects in out tests; especially such that are for
+ * debug purpose only
+ */
+class DummyCommunication : CommunicatorInterface {
+
+ val outputCollector = mutableListOf<String>()
+
+ /**
+ * Sends the diagnostics
+ *
+ * @param diagnostics object containing the Diagnostics
+ */
+ override fun publishDiagnostics(diagnostics: PublishDiagnosticsParams) {}
+
+ /**
+ * Sends a debug message resulting in a output channel message
+ *
+ * @param message the message to send
+ * @param severity the Severity of the message (Error/Info/Warning)
+ */
+ override fun sendDebugMessage(message: String, severity: MessageType) {
+ outputCollector.add(message)
+ }
+
+ /**
+ * Sends a popup message resulting in a popup message
+ *
+ * @param message the message to send
+ * @param severity the Severity of the message (Error/Info/Warning)
+ */
+ override fun showMessage(message: String, severity: MessageType) {}
+
+ /**
+ * To enable/disable debug mode
+ *
+ * @param mode the new state of the debug mode
+ */
+ override fun setDebugMode(mode: Boolean) {
+
+ }
+}
\ No newline at end of file
diff --git a/src/test/kotlin/b/language/server/prob2/proBMangement/ProBKernelManagerTest.kt b/src/test/kotlin/b/language/server/prob2/proBMangement/ProBKernelManagerTest.kt
new file mode 100644
index 0000000..ef33ff0
--- /dev/null
+++ b/src/test/kotlin/b/language/server/prob2/proBMangement/ProBKernelManagerTest.kt
@@ -0,0 +1,37 @@
+package b.language.server.prob2.proBMangement
+
+import b.language.server.communication.DummyCommunication
+import b.language.server.proBMangement.WrongPathException
+import b.language.server.proBMangement.prob2.ProBKernelManager
+import org.junit.jupiter.api.Assertions
+import org.junit.jupiter.api.Test
+import org.junit.jupiter.api.assertThrows
+import org.junit.jupiter.api.function.Executable
+import kotlin.test.assertEquals
+
+class ProBKernelManagerTest {
+
+ @Test
+ fun testCorrectBaseSetup(){
+ val dummyCommunication = DummyCommunication()
+ val proBKernelManager = ProBKernelManager(dummyCommunication)
+
+ proBKernelManager.setup("DEFAULT")
+
+ assertEquals(listOf("default prob selected"), dummyCommunication.outputCollector)
+ }
+
+
+ @Test
+ fun testCorrectBaseSetupWrongPath(){
+ val dummyCommunication = DummyCommunication()
+ val proBKernelManager = ProBKernelManager(dummyCommunication)
+
+ Assertions.assertThrows(WrongPathException::class.java) { proBKernelManager.setup("NOTDEFAULT") }
+ }
+
+ @Test
+ fun testCheckDocument(){
+
+ }
+}
\ No newline at end of file
--
GitLab