diff --git a/build.gradle b/build.gradle
index f0dcc50d2773d7e38a5e789e275d6bdbc340ca68..6a1e2f847fefaca25ca49ff51edc16ff590a4a1b 100644
--- a/build.gradle
+++ b/build.gradle
@@ -33,7 +33,7 @@ project(':de.prob.core') {
}
}
- def parser_version = "2.13.3"
+ def parser_version = "2.13.5"
dependencies {
// Note: After changing/updating dependencies or their versions here,
@@ -87,7 +87,7 @@ task downloadCli {
def targetdir = dir + it.getValue()
def targetzip = dir + "probcli_${n}.zip"
- def url = "https://stups.hhu-hosting.de/downloads/prob/cli/releases/1.13.1-beta2/probcli_${n}.zip"
+ def url = "https://stups.hhu-hosting.de/downloads/prob/cli/nightly/probcli_${n}.zip"
download(url, targetzip)
FileTree zip = zipTree(targetzip)
copy {
diff --git a/de.prob.core/.classpath b/de.prob.core/.classpath
index 47744048c15785b9ac6a9f24d583de49bd30dc34..1aecefae8475ce40ca753bdada1b7e72ef32f200 100644
--- a/de.prob.core/.classpath
+++ b/de.prob.core/.classpath
@@ -4,12 +4,12 @@
<classpathentry kind="con" path="org.eclipse.pde.core.requiredPlugins"/>
<classpathentry kind="src" path="src"/>
<classpathentry kind="output" path="bin"/>
- <classpathentry exported="true" kind="lib" path="lib/dependencies/answerparser-2.13.3.jar"/>
- <classpathentry exported="true" kind="lib" path="lib/dependencies/bparser-2.13.3.jar"/>
- <classpathentry exported="true" kind="lib" path="lib/dependencies/ltlparser-2.13.3.jar"/>
- <classpathentry exported="true" kind="lib" path="lib/dependencies/parserbase-2.13.3.jar"/>
- <classpathentry exported="true" kind="lib" path="lib/dependencies/prologlib-2.13.3.jar"/>
- <classpathentry exported="true" kind="lib" path="lib/dependencies/sablecc-runtime-3.8.0.jar"/>
- <classpathentry exported="true" kind="lib" path="lib/dependencies/theorymapping-2.13.3.jar"/>
- <classpathentry exported="true" kind="lib" path="lib/dependencies/unicode-2.13.3.jar"/>
+ <classpathentry exported="true" kind="lib" path="lib/dependencies/answerparser-2.13.5.jar"/>
+ <classpathentry exported="true" kind="lib" path="lib/dependencies/bparser-2.13.5.jar"/>
+ <classpathentry exported="true" kind="lib" path="lib/dependencies/ltlparser-2.13.5.jar"/>
+ <classpathentry exported="true" kind="lib" path="lib/dependencies/parserbase-2.13.5.jar"/>
+ <classpathentry exported="true" kind="lib" path="lib/dependencies/prologlib-2.13.5.jar"/>
+ <classpathentry exported="true" kind="lib" path="lib/dependencies/sablecc-runtime-3.9.0.jar"/>
+ <classpathentry exported="true" kind="lib" path="lib/dependencies/theorymapping-2.13.5.jar"/>
+ <classpathentry exported="true" kind="lib" path="lib/dependencies/unicode-2.13.5.jar"/>
</classpath>
diff --git a/de.prob.core/META-INF/MANIFEST.MF b/de.prob.core/META-INF/MANIFEST.MF
index 6d71e24f5e5f07136640b2ba48967c671026497b..099074028d2c596c85c6976db792c8364d987086 100644
--- a/de.prob.core/META-INF/MANIFEST.MF
+++ b/de.prob.core/META-INF/MANIFEST.MF
@@ -75,11 +75,11 @@ Bundle-Activator: de.prob.core.internal.Activator
Eclipse-BuddyPolicy: registered
Bundle-RequiredExecutionEnvironment: JavaSE-11
Bundle-ClassPath: .,
- lib/dependencies/answerparser-2.13.3.jar,
- lib/dependencies/bparser-2.13.3.jar,
- lib/dependencies/ltlparser-2.13.3.jar,
- lib/dependencies/parserbase-2.13.3.jar,
- lib/dependencies/prologlib-2.13.3.jar,
- lib/dependencies/sablecc-runtime-3.8.0.jar,
- lib/dependencies/theorymapping-2.13.3.jar,
- lib/dependencies/unicode-2.13.3.jar
+ lib/dependencies/answerparser-2.13.5.jar,
+ lib/dependencies/bparser-2.13.5.jar,
+ lib/dependencies/ltlparser-2.13.5.jar,
+ lib/dependencies/parserbase-2.13.5.jar,
+ lib/dependencies/prologlib-2.13.5.jar,
+ lib/dependencies/sablecc-runtime-3.9.0.jar,
+ lib/dependencies/theorymapping-2.13.5.jar,
+ lib/dependencies/unicode-2.13.5.jar
diff --git a/de.prob.core/src/de/prob/eventb/translator/ContextTranslator.java b/de.prob.core/src/de/prob/eventb/translator/ContextTranslator.java
index fffe0da3d4e3a4cfd2375b77f9cbe0f3cb3f13ef..67849c1fea70f1bf0df176b934fd797988fefc20 100644
--- a/de.prob.core/src/de/prob/eventb/translator/ContextTranslator.java
+++ b/de.prob.core/src/de/prob/eventb/translator/ContextTranslator.java
@@ -8,6 +8,7 @@ package de.prob.eventb.translator;
import java.util.ArrayList;
import java.util.Arrays;
+import java.util.Collections;
import java.util.HashMap;
import java.util.LinkedList;
import java.util.List;
@@ -47,6 +48,7 @@ import de.be4.classicalb.core.parser.node.AAbstractConstantsContextClause;
import de.be4.classicalb.core.parser.node.AAxiomsContextClause;
import de.be4.classicalb.core.parser.node.AConstantsContextClause;
import de.be4.classicalb.core.parser.node.ADeferredSetSet;
+import de.be4.classicalb.core.parser.node.ADescriptionPragma;
import de.be4.classicalb.core.parser.node.ADescriptionPredicate;
import de.be4.classicalb.core.parser.node.AEventBContextParseUnit;
import de.be4.classicalb.core.parser.node.AExtendsContextClause;
@@ -382,7 +384,8 @@ public final class ContextTranslator extends AbstractComponentTranslator {
final String commentString = uca.getAttributeValue(EventBAttributes.COMMENT_ATTRIBUTE);
//System.out.println("Axiom/theorem " + element + " has description " + commentString);
final TPragmaFreeText desc = new TPragmaFreeText(commentString);
- final ADescriptionPredicate dpred = new ADescriptionPredicate(desc,predicate);
+ ADescriptionPragma descPragma = new ADescriptionPragma(Collections.singletonList(desc));
+ ADescriptionPredicate dpred = new ADescriptionPredicate(descPragma, predicate);
list.add(dpred);
labelMapping.put(dpred, element);
} else {
diff --git a/de.prob.core/src/de/prob/eventb/translator/internal/ModelTranslator.java b/de.prob.core/src/de/prob/eventb/translator/internal/ModelTranslator.java
index 0843445fe39450edd6f8a013355fba14ab111d0a..407412ff068f67e3128b174006ed67ec3c832435 100644
--- a/de.prob.core/src/de/prob/eventb/translator/internal/ModelTranslator.java
+++ b/de.prob.core/src/de/prob/eventb/translator/internal/ModelTranslator.java
@@ -8,12 +8,12 @@ package de.prob.eventb.translator.internal;
import java.util.ArrayList;
import java.util.Arrays;
+import java.util.Collections;
import java.util.LinkedList;
import java.util.List;
import org.eclipse.core.runtime.CoreException;
import org.eventb.core.EventBAttributes;
-import org.eventb.core.ICommentedElement;
import org.eventb.core.IConvergenceElement.Convergence;
import org.eventb.core.ILabeledElement;
import org.eventb.core.IMachineRoot;
@@ -21,7 +21,6 @@ import org.eventb.core.IPOSequent;
import org.eventb.core.IPOSource;
import org.eventb.core.IPSRoot;
import org.eventb.core.IPSStatus;
-import org.eventb.core.IPredicateElement;
import org.eventb.core.ISCAction;
import org.eventb.core.IEvent;
import org.eventb.core.IInvariant;
@@ -53,6 +52,7 @@ import org.rodinp.core.RodinDBException;
import de.be4.classicalb.core.parser.node.AAnticipatedEventstatus;
import de.be4.classicalb.core.parser.node.AConvergentEventstatus;
import de.be4.classicalb.core.parser.node.ADescriptionEvent;
+import de.be4.classicalb.core.parser.node.ADescriptionPragma;
import de.be4.classicalb.core.parser.node.ADescriptionPredicate;
import de.be4.classicalb.core.parser.node.AEvent;
import de.be4.classicalb.core.parser.node.AEventBModelParseUnit;
@@ -366,11 +366,9 @@ public class ModelTranslator extends AbstractComponentTranslator {
if (ucevent.hasAttribute(EventBAttributes.COMMENT_ATTRIBUTE)) {
final String commentString = ucevent.getAttributeValue(EventBAttributes.COMMENT_ATTRIBUTE);
System.out.println("Event " + revent.getLabel() + " has description " + commentString);
- final ADescriptionEvent devent = new ADescriptionEvent();
- devent.setEvent(event);
final TPragmaFreeText desc = new TPragmaFreeText(commentString);
- devent.setContent(desc);
- eventsList.add(devent); // we add the event with a description node around it; requires new probcli
+ ADescriptionPragma descPragma = new ADescriptionPragma(Collections.singletonList(desc));
+ eventsList.add(new ADescriptionEvent(descPragma, event));
} else {
eventsList.add(event);
}
@@ -542,7 +540,8 @@ public class ModelTranslator extends AbstractComponentTranslator {
final String commentString = ucp.getAttributeValue(EventBAttributes.COMMENT_ATTRIBUTE);
//System.out.println("Invariant/theorem " + predicate + " has description " + commentString);
final TPragmaFreeText desc = new TPragmaFreeText(commentString);
- final ADescriptionPredicate dpred = new ADescriptionPredicate(desc,predicate);
+ ADescriptionPragma descPragma = new ADescriptionPragma(Collections.singletonList(desc));
+ ADescriptionPredicate dpred = new ADescriptionPredicate(descPragma, predicate);
list.add(dpred);
labelMapping.put(dpred, evPredicate);
} else {