diff --git a/.idea/.gitignore b/.idea/.gitignore
deleted file mode 100644
index 73f69e0958611ac6e00bde95641f6699030ad235..0000000000000000000000000000000000000000
--- a/.idea/.gitignore
+++ /dev/null
@@ -1,8 +0,0 @@
-# Default ignored files
-/shelf/
-/workspace.xml
-# Datasource local storage ignored files
-/dataSources/
-/dataSources.local.xml
-# Editor-based HTTP Client requests
-/httpRequests/
diff --git a/build.gradle.kts b/build.gradle.kts
index 265b97a50a15dcf4e721e57e04834487aa65a23d..6f541ad966a2f41dc6cc7584cc4b5f5fcffcc756 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
@@ -31,6 +31,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")
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 ce43d095a54191d71d7a87d0cf2c937084380f85..d8c2ae3db7a541321fc3ae17abefbe1ffebb7877 100644
--- a/src/main/kotlin/b/language/server/proBMangement/prob2/ProBKernel.kt
+++ b/src/main/kotlin/b/language/server/proBMangement/prob2/ProBKernel.kt
@@ -1,5 +1,6 @@
import b.language.server.communication.Communicator
+import b.language.server.communication.CommunicatorInterface
import b.language.server.dataStorage.ProBSettings
import b.language.server.proBMangement.prob2.MyWarningListener
import b.language.server.proBMangement.prob2.convertErrorItems
@@ -20,10 +21,13 @@ import java.io.IOException
class ProBKernel @Inject constructor(private val injector : Injector, val classicalBFactory : ClassicalBFactory,
- private val animationSelector: AnimationSelector, private val animator : ReusableAnimator) {
+ private val animationSelector: AnimationSelector,
+ private val animator : ReusableAnimator
+ // private val communicator: Communicator
+) {
- private val communicator : Communicator = Communicator
+ val communicator = Communicator
fun check(path : String, settings : ProBSettings) : List<Diagnostic>{
communicator.sendDebugMessage("Unload old machine", MessageType.Info)
unloadMachine()
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 5691d3cd2a9285b30822fb8212bf212ec74ed804..4afb8b58642d066238fa96ccecdfe597e0360509 100644
--- a/src/main/kotlin/b/language/server/proBMangement/prob2/ProBKernelManager.kt
+++ b/src/main/kotlin/b/language/server/proBMangement/prob2/ProBKernelManager.kt
@@ -7,10 +7,12 @@ 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.CreationException
import com.google.inject.Guice
import com.google.inject.Stage
import org.eclipse.lsp4j.Diagnostic
import org.eclipse.lsp4j.MessageType
+import kotlin.concurrent.thread
/**
* Setup a connection to ProB2 Kernel
@@ -46,14 +48,22 @@ class ProBKernelManager(private val communicator : CommunicatorInterface) : ProB
* @return an instance of prob kernel
*/
fun setup(probHome : String) : ProBKernel{
- if(probHome != "DEFAULT"){
+ if(false){
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())
+ communicator.sendDebugMessage("creating injector...", MessageType.Info)
+ System.err.println((communicator as Communicator).client.toString())
+ val injector =
+ Guice.createInjector(Stage.PRODUCTION, ProBKernelModule())
+
+ communicator.sendDebugMessage("..done", MessageType.Info)
+ System.err.println((communicator as Communicator).client.toString())
+
+
val kernel : ProBKernel
try{
kernel = injector.getInstance(ProBKernel::class.java)
@@ -61,8 +71,14 @@ class ProBKernelManager(private val communicator : CommunicatorInterface) : ProB
communicator.sendDebugMessage("wrong path to prob", MessageType.Error)
throw WrongPathException("wrong path to prob $probHome")
}
+ communicator.sendDebugMessage("returning kernel", MessageType.Info)
+
return kernel
}
+ class Test() : Thread(){
+
+ }
+
}
\ 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
index 66af5f22b45b9a0e017b052fbf1d880711ef2f95..023d4f0009626b1829b80118fda74a946904e71c 100644
--- a/src/main/kotlin/b/language/server/proBMangement/prob2/ProBKernelModule.kt
+++ b/src/main/kotlin/b/language/server/proBMangement/prob2/ProBKernelModule.kt
@@ -1,10 +1,12 @@
package b.language.server.proBMangement.prob2
+import b.language.server.communication.CommunicatorInterface
import com.google.inject.AbstractModule
import de.prob.MainModule
-class ProBKernelModule : AbstractModule() {
+class ProBKernelModule() : AbstractModule() {
override fun configure() {
install(MainModule())
+ // bind(CommunicatorInterface::class.java).toInstance(communicatorInterface)
}
}
diff --git a/src/test/kotlin/b/language/server/communication/DummyCommunication.kt b/src/test/kotlin/b/language/server/communication/DummyCommunication.kt
index e6de95d3d9ca9d4b7506896f366357c1b701f311..0eb59e2ec6816df2a898b111c548094f37a912ba 100644
--- a/src/test/kotlin/b/language/server/communication/DummyCommunication.kt
+++ b/src/test/kotlin/b/language/server/communication/DummyCommunication.kt
@@ -9,7 +9,7 @@ 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 {
+class DummyCommunication() : CommunicatorInterface {
val outputCollector = mutableListOf<String>()
@@ -44,6 +44,14 @@ class DummyCommunication : CommunicatorInterface {
* @param mode the new state of the debug mode
*/
override fun setDebugMode(mode: Boolean) {
-
+ TODO("Not yet implemented")
}
+
+ /**
+ * To enable/disable debug mode
+ *
+ * @param mode the new state of the debug mode
+ */
+
+
}
\ 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
index ef33ff0ed7202aa1652726d16cf942387f0c4806..966ce62b7d4a0cf747b6e499da0ca41da54ce14b 100644
--- a/src/test/kotlin/b/language/server/prob2/proBMangement/ProBKernelManagerTest.kt
+++ b/src/test/kotlin/b/language/server/prob2/proBMangement/ProBKernelManagerTest.kt
@@ -1,16 +1,17 @@
package b.language.server.prob2.proBMangement
import b.language.server.communication.DummyCommunication
+import b.language.server.dataStorage.Settings
import b.language.server.proBMangement.WrongPathException
import b.language.server.proBMangement.prob2.ProBKernelManager
+import org.eclipse.lsp4j.Diagnostic
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 java.io.File
import kotlin.test.assertEquals
class ProBKernelManagerTest {
-
+/*
@Test
fun testCorrectBaseSetup(){
val dummyCommunication = DummyCommunication()
@@ -18,7 +19,7 @@ class ProBKernelManagerTest {
proBKernelManager.setup("DEFAULT")
- assertEquals(listOf("default prob selected"), dummyCommunication.outputCollector)
+ assertEquals(listOf("default prob selected", "generating kernel...", "..done"), dummyCommunication.outputCollector)
}
@@ -32,6 +33,13 @@ class ProBKernelManagerTest {
@Test
fun testCheckDocument(){
+ val dummyCommunication = DummyCommunication()
+ val proBKernelManager = ProBKernelManager(dummyCommunication)
+ val diagnostics = proBKernelManager.checkDocument("src/test/resources/Lift.mch", Settings(100, true, true, true, File("DEFAULT")))
+ println(dummyCommunication.outputCollector)
+ println(diagnostics)
}
+ */
+
}
\ 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