From 879599fb0c647190d221e2884ea2dca8ce6831f5 Mon Sep 17 00:00:00 2001
From: dgelessus <dgelessus@users.noreply.github.com>
Date: Tue, 16 May 2023 10:27:48 +0200
Subject: [PATCH] Resurrect the tests

---
 de.prob.core.tests/META-INF/MANIFEST.MF                   | 8 ++++++--
 .../prob/core/translator/tests/AbstractEventBTests.java   | 2 +-
 .../de/prob/core/translator/tests/ContextChainTest.java   | 7 ++++++-
 .../core/translator/tests/ContextWithConstantsTest.java   | 5 +++++
 .../prob/core/translator/tests/EmptyTranslationsTest.java | 5 +++++
 settings.gradle                                           | 2 +-
 6 files changed, 24 insertions(+), 5 deletions(-)

diff --git a/de.prob.core.tests/META-INF/MANIFEST.MF b/de.prob.core.tests/META-INF/MANIFEST.MF
index 813b16b3..4b85c932 100644
--- a/de.prob.core.tests/META-INF/MANIFEST.MF
+++ b/de.prob.core.tests/META-INF/MANIFEST.MF
@@ -5,8 +5,12 @@ Bundle-SymbolicName: de.prob.core.tests
 Bundle-Version: 1.0.0.qualifier
 Bundle-Activator: de.prob.core.tests.Activator
 Require-Bundle: org.eclipse.ui,
+ org.eclipse.core.resources,
  org.eclipse.core.runtime,
- org.eventb.core;bundle-version="[2.1.0,2.6.0)",
- de.prob.core;bundle-version="9.3.0"
+ org.eventb.core;bundle-version="[3.3.0,4.0.0)",
+ org.eventb.core.ast;bundle-version="[3.3.0,4.0.0)",
+ org.junit;bundle-version="[4.0.0,5.0.0)",
+ org.rodinp.core;bundle-version="[1.7.0,2.0.0)",
+ de.prob.core;bundle-version="[9.4.0,9.5.0)"
 Bundle-ActivationPolicy: lazy
 Bundle-RequiredExecutionEnvironment: JavaSE-1.8
diff --git a/de.prob.core.tests/src/de/prob/core/translator/tests/AbstractEventBTests.java b/de.prob.core.tests/src/de/prob/core/translator/tests/AbstractEventBTests.java
index ec7daa22..c103bc2d 100644
--- a/de.prob.core.tests/src/de/prob/core/translator/tests/AbstractEventBTests.java
+++ b/de.prob.core.tests/src/de/prob/core/translator/tests/AbstractEventBTests.java
@@ -980,7 +980,7 @@ public abstract class AbstractEventBTests extends AbstractTests {
 					expected,
 					evt.getLabel() + ":" + evt.getConvergence() + ":"
 							+ evt.isExtended());
-		} catch (RodinDBException e) {
+		} catch (CoreException e) {
 			e.printStackTrace();
 			fail("There should be no exception");
 			return;
diff --git a/de.prob.core.tests/src/de/prob/core/translator/tests/ContextChainTest.java b/de.prob.core.tests/src/de/prob/core/translator/tests/ContextChainTest.java
index 237722c6..b871dd93 100644
--- a/de.prob.core.tests/src/de/prob/core/translator/tests/ContextChainTest.java
+++ b/de.prob.core.tests/src/de/prob/core/translator/tests/ContextChainTest.java
@@ -7,10 +7,15 @@ import org.eclipse.core.resources.IncrementalProjectBuilder;
 import org.eclipse.core.runtime.CoreException;
 import org.eventb.core.IContextRoot;
 import org.eventb.core.IEventBProject;
+import org.junit.Before;
+import org.junit.Ignore;
+import org.junit.Test;
 
 import de.prob.core.translator.TranslationFailedException;
 import de.prob.eventb.translator.TranslatorFactory;
 
+import static org.junit.Assert.assertEquals;
+
 public class ContextChainTest extends AbstractEventBTests {
 	private StringWriter stringWriter;
 	private PrintWriter writer;
@@ -40,7 +45,7 @@ public class ContextChainTest extends AbstractEventBTests {
 		TranslatorFactory.translate(context2, writer);
 
 		assertEquals(
-				"package(load_event_b_project([],[event_b_context(none,'TestContext2',[extends(none,['TestContext1']),constants(none,[]),abstract_constants(none,[]),axioms(none,[]),theorems(none,[]),sets(none,[])]),event_b_context(none,'TestContext1',[extends(none,[]),constants(none,[]),axioms(none,[]),theorems(none,[]),sets(none,[])])],[exporter_version(3)],_Error)).\n",
+				"package(load_event_b_project([],[event_b_context(none,'TestContext2',[extends(none,['TestContext1']),constants(none,[]),abstract_constants(none,[]),axioms(none,[]),theorems(none,[]),sets(none,[])]),event_b_context(none,'TestContext1',[extends(none,[]),constants(none,[]),abstract_constants(none,[]),axioms(none,[]),theorems(none,[]),sets(none,[])])],[exporter_version(3)],_Error)).\n",
 				stringWriter.getBuffer().toString());
 	}
 }
diff --git a/de.prob.core.tests/src/de/prob/core/translator/tests/ContextWithConstantsTest.java b/de.prob.core.tests/src/de/prob/core/translator/tests/ContextWithConstantsTest.java
index fc60ba04..2919be6f 100644
--- a/de.prob.core.tests/src/de/prob/core/translator/tests/ContextWithConstantsTest.java
+++ b/de.prob.core.tests/src/de/prob/core/translator/tests/ContextWithConstantsTest.java
@@ -7,10 +7,15 @@ import org.eclipse.core.resources.IncrementalProjectBuilder;
 import org.eclipse.core.runtime.CoreException;
 import org.eventb.core.IContextRoot;
 import org.eventb.core.IEventBProject;
+import org.junit.Before;
+import org.junit.Ignore;
+import org.junit.Test;
 
 import de.prob.core.translator.TranslationFailedException;
 import de.prob.eventb.translator.TranslatorFactory;
 
+import static org.junit.Assert.assertEquals;
+
 public class ContextWithConstantsTest extends AbstractEventBTests {
 	private StringWriter stringWriter;
 	private PrintWriter writer;
diff --git a/de.prob.core.tests/src/de/prob/core/translator/tests/EmptyTranslationsTest.java b/de.prob.core.tests/src/de/prob/core/translator/tests/EmptyTranslationsTest.java
index fddef397..5a64393c 100644
--- a/de.prob.core.tests/src/de/prob/core/translator/tests/EmptyTranslationsTest.java
+++ b/de.prob.core.tests/src/de/prob/core/translator/tests/EmptyTranslationsTest.java
@@ -8,10 +8,15 @@ import org.eclipse.core.runtime.CoreException;
 import org.eventb.core.IContextRoot;
 import org.eventb.core.IEventBProject;
 import org.eventb.core.IMachineRoot;
+import org.junit.Before;
+import org.junit.Ignore;
+import org.junit.Test;
 
 import de.prob.core.translator.TranslationFailedException;
 import de.prob.eventb.translator.TranslatorFactory;
 
+import static org.junit.Assert.assertEquals;
+
 public class EmptyTranslationsTest extends AbstractEventBTests {
 	private StringWriter stringWriter;
 	private PrintWriter writer;
diff --git a/settings.gradle b/settings.gradle
index 6b848199..80933621 100644
--- a/settings.gradle
+++ b/settings.gradle
@@ -1 +1 @@
-include 'de.prob.core', 'de.bmotionstudio.gef.editor' ,'de.bmotionstudio.rodin' , 'de.prob.plugin', 'de.prob.ui', 'de.prob2.feature', 'de.prob.symbolic', 'de.prob2.symbolic.feature', 'de.prob.eventb.disprover.core', 'de.prob.eventb.disprover.ui', 'de.prob2.disprover.feature'
+include 'de.prob.core', 'de.prob.core.tests', 'de.bmotionstudio.gef.editor' ,'de.bmotionstudio.rodin' , 'de.prob.plugin', 'de.prob.ui', 'de.prob2.feature', 'de.prob.symbolic', 'de.prob2.symbolic.feature', 'de.prob.eventb.disprover.core', 'de.prob.eventb.disprover.ui', 'de.prob2.disprover.feature'
-- 
GitLab