From 949b59c83e006f387836395dd923fc30bc914b37 Mon Sep 17 00:00:00 2001
From: SeeBasTStick <sebastian.stock@hhu.de>
Date: Thu, 13 Aug 2020 16:31:40 +0200
Subject: [PATCH] added prob2 java kernel dependencies
---
build.gradle.kts | 7 ++
.../b/language/server/BDocumentService.kt | 8 +-
src/main/kotlin/b/language/server/Util.kt | 1 +
.../server/dataStorage/ProBSettings.kt | 3 +
.../b/language/server/dataStorage/Settings.kt | 2 +-
.../proBMangement/prob2/MyWarningListener.kt | 18 ++++
.../server/proBMangement/prob2/ProBKernel.kt | 90 +++++++++++++++++++
.../proBMangement/prob2/ProBKernelManager.kt | 40 +++++++++
.../proBMangement/prob2/ProBKernelModule.kt | 10 +++
.../server/proBMangement/prob2/Util.kt | 36 ++++++++
.../b/language/server/ProBCommandLineTest.kt | 2 +-
11 files changed, 211 insertions(+), 6 deletions(-)
create mode 100644 src/main/kotlin/b/language/server/dataStorage/ProBSettings.kt
create mode 100644 src/main/kotlin/b/language/server/proBMangement/prob2/MyWarningListener.kt
create mode 100644 src/main/kotlin/b/language/server/proBMangement/prob2/ProBKernel.kt
create mode 100644 src/main/kotlin/b/language/server/proBMangement/prob2/ProBKernelManager.kt
create mode 100644 src/main/kotlin/b/language/server/proBMangement/prob2/ProBKernelModule.kt
create mode 100644 src/main/kotlin/b/language/server/proBMangement/prob2/Util.kt
diff --git a/build.gradle.kts b/build.gradle.kts
index 4f7097f..265b97a 100644
--- a/build.gradle.kts
+++ b/build.gradle.kts
@@ -19,6 +19,9 @@ plugins {
repositories {
// Use jcenter for resolving dependencies.
jcenter()
+
+ maven("https://oss.sonatype.org/content/repositories/snapshots")
+
}
dependencies {
@@ -41,6 +44,10 @@ 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")
+
}
diff --git a/src/main/kotlin/b/language/server/BDocumentService.kt b/src/main/kotlin/b/language/server/BDocumentService.kt
index 490e7e1..f13ee1a 100644
--- a/src/main/kotlin/b/language/server/BDocumentService.kt
+++ b/src/main/kotlin/b/language/server/BDocumentService.kt
@@ -1,9 +1,9 @@
package b.language.server
import b.language.server.communication.CommunicatorInterface
-import b.language.server.proBMangement.CommandCouldNotBeExecutedException
-import b.language.server.proBMangement.PathCouldNotBeCreatedException
-import b.language.server.proBMangement.ProBCommandLineAccess
+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.ProBInterface
import org.eclipse.lsp4j.*
import org.eclipse.lsp4j.services.TextDocumentService
@@ -64,7 +64,7 @@ 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 ){
+ }catch (e : PathCouldNotBeCreatedException){
communicator.sendDebugMessage("error path could not be created", MessageType.Info)
communicator.showMessage(e.message!!, MessageType.Error)
}catch (e : CommandCouldNotBeExecutedException){
diff --git a/src/main/kotlin/b/language/server/Util.kt b/src/main/kotlin/b/language/server/Util.kt
index d1d0d31..9ba3755 100644
--- a/src/main/kotlin/b/language/server/Util.kt
+++ b/src/main/kotlin/b/language/server/Util.kt
@@ -19,4 +19,5 @@ fun castJsonToSetting(json : JsonObject) : Settings {
Gson().fromJson(json.get("performanceHints"), Boolean::class.java),
File(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/dataStorage/ProBSettings.kt b/src/main/kotlin/b/language/server/dataStorage/ProBSettings.kt
new file mode 100644
index 0000000..21828a5
--- /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/Settings.kt b/src/main/kotlin/b/language/server/dataStorage/Settings.kt
index 0cc9534..895add0 100644
--- a/src/main/kotlin/b/language/server/dataStorage/Settings.kt
+++ b/src/main/kotlin/b/language/server/dataStorage/Settings.kt
@@ -3,5 +3,5 @@ package b.language.server.dataStorage
import java.io.File
data class Settings(val maxNumberOfProblem : Int = 1000, val strictChecks : Boolean = true, val wdChecks : Boolean = true,
- val performanceHints : Boolean = true , val probHome : File = File("~/prob_prolog/probcli.sh"),
+ val performanceHints : Boolean = true , val probHome : File = File("DEFAULT"),
val debugMode : Boolean = true)
diff --git a/src/main/kotlin/b/language/server/proBMangement/prob2/MyWarningListener.kt b/src/main/kotlin/b/language/server/proBMangement/prob2/MyWarningListener.kt
new file mode 100644
index 0000000..2418807
--- /dev/null
+++ b/src/main/kotlin/b/language/server/proBMangement/prob2/MyWarningListener.kt
@@ -0,0 +1,18 @@
+package b.language.server.proBMangement.prob2
+
+import de.prob.animator.IWarningListener
+import de.prob.animator.domainobjects.ErrorItem
+import org.eclipse.lsp4j.Diagnostic
+import org.eclipse.lsp4j.DiagnosticSeverity
+
+
+class MyWarningListener : IWarningListener {
+ private val warningList : ArrayList<ErrorItem> = arrayListOf()
+ override fun warningsOccurred(warnings: MutableList<ErrorItem>?) {
+ warningList.addAll(warnings!!.toList())
+ }
+
+ fun getWarnings() : List<Diagnostic>{
+ return convertErrorItems(warningList, DiagnosticSeverity.Warning)
+ }
+}
\ 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
new file mode 100644
index 0000000..7b87aba
--- /dev/null
+++ b/src/main/kotlin/b/language/server/proBMangement/prob2/ProBKernel.kt
@@ -0,0 +1,90 @@
+
+import b.language.server.dataStorage.ProBSettings
+import b.language.server.proBMangement.prob2.MyWarningListener
+import b.language.server.proBMangement.prob2.convertErrorItems
+import com.google.inject.Inject
+import com.google.inject.Injector
+import de.prob.animator.ReusableAnimator
+import de.prob.animator.command.CheckWellDefinednessCommand
+import de.prob.exception.ProBError
+import de.prob.scripting.ClassicalBFactory
+import de.prob.scripting.FactoryProvider
+import de.prob.scripting.ModelTranslationError
+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 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 fun loadMachine(newTraceCreator :java.util.function.Function<StateSpace, Trace>, settings: ProBSettings){
+ val newStateSpace = animator.createStateSpace()
+ try {
+ animationSelector.changeCurrentAnimation(newTraceCreator.apply(newStateSpace))
+ executeAdditionalOptions(settings)
+ } catch (e: RuntimeException) {
+ newStateSpace.kill()
+ throw e
+ }
+ }
+
+ private fun executeAdditionalOptions(settings : ProBSettings){
+ val newStateSpace = animator.createStateSpace()
+ if(settings.wdChecks){
+ animator.execute(CheckWellDefinednessCommand())
+ }
+
+ }
+
+ private fun unloadMachine() {
+ val oldTrace = animationSelector.currentTrace
+ if (oldTrace != null) {
+ assert(oldTrace.stateSpace === animator.currentStateSpace)
+ animationSelector.changeCurrentAnimation(null)
+ oldTrace.stateSpace.kill()
+ }
+ }
+
+ 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> {
+ val settings = mutableMapOf<String, String>()
+ if(proBSettings.performanceHints) {
+ settings["STRICT_CLASH_CHECKING"] = "TRUE"
+ settings["TYPE_CHECK_DEFINITIONS"] = "TRUE"
+ }
+ if (proBSettings.strictChecks) {
+ settings["PERFORMANCE_INFO"] = "TRUE"
+ }
+ return settings
+ }
+
+
+}
\ No newline at end of file
diff --git a/src/main/kotlin/b/language/server/proBMangement/prob2/ProBKernelManager.kt b/src/main/kotlin/b/language/server/proBMangement/prob2/ProBKernelManager.kt
new file mode 100644
index 0000000..4da6661
--- /dev/null
+++ b/src/main/kotlin/b/language/server/proBMangement/prob2/ProBKernelManager.kt
@@ -0,0 +1,40 @@
+package b.language.server.proBMangement.prob2
+
+import ProBKernel
+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
+
+/**
+ * Setup a connection to ProB2 Kernel
+ */
+class ProBKernelManager : ProBInterface{
+
+ private lateinit var kernel : ProBKernel
+
+ /**
+ * Checks the given document with the help of ProB
+ * @param uri the source to check
+ * @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)
+ }
+
+ return kernel.check(uri, proBSettings)
+ }
+
+
+}
\ No newline at end of file
diff --git a/src/main/kotlin/b/language/server/proBMangement/prob2/ProBKernelModule.kt b/src/main/kotlin/b/language/server/proBMangement/prob2/ProBKernelModule.kt
new file mode 100644
index 0000000..66af5f2
--- /dev/null
+++ b/src/main/kotlin/b/language/server/proBMangement/prob2/ProBKernelModule.kt
@@ -0,0 +1,10 @@
+package b.language.server.proBMangement.prob2
+
+import com.google.inject.AbstractModule
+import de.prob.MainModule
+
+class ProBKernelModule : AbstractModule() {
+ override fun configure() {
+ install(MainModule())
+ }
+}
diff --git a/src/main/kotlin/b/language/server/proBMangement/prob2/Util.kt b/src/main/kotlin/b/language/server/proBMangement/prob2/Util.kt
new file mode 100644
index 0000000..96d7e8b
--- /dev/null
+++ b/src/main/kotlin/b/language/server/proBMangement/prob2/Util.kt
@@ -0,0 +1,36 @@
+package b.language.server.proBMangement.prob2
+
+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>) : List<Diagnostic>{
+ return errorItems.toList().map { errorItem ->
+ errorItem.locations.map { location ->
+ Diagnostic(Range(Position(location.startLine, location.startColumn), Position(location.endLine, location.endColumn)),
+ errorItem.message,
+ getErrorItemType(errorItem),
+ location.filename)
+ }
+ }.flatten()
+}
+
+fun getErrorItemType(errorItem : ErrorItem) : DiagnosticSeverity{
+ return when(errorItem.type){
+ ErrorItem.Type.ERROR -> {
+ DiagnosticSeverity.Error
+ }
+ ErrorItem.Type.WARNING -> {
+ DiagnosticSeverity.Warning
+ }
+ ErrorItem.Type.INTERNAL_ERROR -> {
+ DiagnosticSeverity.Error
+ }
+ else -> {
+ DiagnosticSeverity.Error
+ }
+ }
+
+}
\ 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
index 79e90d6..2f9a74f 100644
--- a/src/test/kotlin/b/language/server/ProBCommandLineTest.kt
+++ b/src/test/kotlin/b/language/server/ProBCommandLineTest.kt
@@ -3,7 +3,7 @@ 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.ProBCommandLineAccess
+import b.language.server.proBMangement.probCli.ProBCommandLineAccess
import com.google.gson.Gson
import org.eclipse.lsp4j.Diagnostic
import org.eclipse.lsp4j.DiagnosticSeverity
--
GitLab