added prob2 java kernel dependencies

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")
+
 
 }
 

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

 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

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

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

src/main/kotlin/b/language/server/proBMangement/prob2/MyWarningListener.kt

+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

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

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

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

+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

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

+package b.language.server.proBMangement.prob2
+
+import com.google.inject.AbstractModule
+import de.prob.MainModule
+
+class ProBKernelModule : AbstractModule() {
+    override fun configure() {
+        install(MainModule())
+    }
+}

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

+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

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