Skip to content
Snippets Groups Projects
Commit a0c13101 authored by dgelessus's avatar dgelessus
Browse files

Switch to nightly version of ProB and update parsers accordingly

parent e0b77d1e
No related branches found
No related tags found
No related merge requests found
Pipeline #145684 passed
......@@ -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 {
......
......@@ -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>
......@@ -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
......@@ -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 {
......
......@@ -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 {
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment