From 4bcc7446272f5e78bfa5bd06adf71590c196961c Mon Sep 17 00:00:00 2001
From: SeeBasTStick <sebastian.stock@hhu.de>
Date: Wed, 19 Aug 2020 10:07:03 +0200
Subject: [PATCH] save commit

---
 .idea/.gitignore                              |  8 --------
 build.gradle.kts                              |  6 +++++-
 .../server/proBMangement/prob2/ProBKernel.kt  |  8 ++++++--
 .../proBMangement/prob2/ProBKernelManager.kt  | 20 +++++++++++++++++--
 .../proBMangement/prob2/ProBKernelModule.kt   |  4 +++-
 .../communication/DummyCommunication.kt       | 12 +++++++++--
 .../proBMangement/ProBKernelManagerTest.kt    | 16 +++++++++++----
 src/test/resources/Lift.mch                   | 19 ++++++++++++++++++
 8 files changed, 73 insertions(+), 20 deletions(-)
 delete mode 100644 .idea/.gitignore
 create mode 100644 src/test/resources/Lift.mch

diff --git a/.idea/.gitignore b/.idea/.gitignore
deleted file mode 100644
index 73f69e0..0000000
--- 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 265b97a..6f541ad 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 ce43d09..d8c2ae3 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 5691d3c..4afb8b5 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 66af5f2..023d4f0 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 e6de95d..0eb59e2 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 ef33ff0..966ce62 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 0000000..2aa64ac
--- /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
-- 
GitLab