diff --git a/de.bmotionstudio.gef.editor/META-INF/MANIFEST.MF b/de.bmotionstudio.gef.editor/META-INF/MANIFEST.MF
index b1c60870a72a551f618f26316aec6a54c4507366..d51f7c6fbfc3643ab3835dfea27032834f06a5f2 100644
--- a/de.bmotionstudio.gef.editor/META-INF/MANIFEST.MF
+++ b/de.bmotionstudio.gef.editor/META-INF/MANIFEST.MF
@@ -2,7 +2,7 @@ Manifest-Version: 1.0
Bundle-ManifestVersion: 2
Bundle-Name: BMotion Studio Editor Plug-in
Bundle-SymbolicName: de.bmotionstudio.gef.editor;singleton:=true
-Bundle-Version: 5.3.2.qualifier
+Bundle-Version: 5.4.0.qualifier
Bundle-Activator: de.bmotionstudio.gef.editor.BMotionEditorPlugin
Require-Bundle: org.eclipse.ui;bundle-version="[3.5.0,4.0.0)",
org.eclipse.ui.ide;bundle-version="[3.5.0,4.0.0)",
@@ -12,7 +12,7 @@ Require-Bundle: org.eclipse.ui;bundle-version="[3.5.0,4.0.0)",
org.eclipse.jface.databinding;bundle-version="[1.2.1,2.0.0)",
org.eclipse.core.databinding.beans;bundle-version="[1.1.1,2.0.0)",
org.eclipse.gef;bundle-version="[3.7.0,4.0.0)";visibility:=reexport,
- de.prob.core;bundle-version="[9.2.0,9.3.0)";visibility:=reexport,
+ de.prob.core;bundle-version="[9.3.0,9.4.0)";visibility:=reexport,
org.eventb.core;bundle-version="[2.1.0,2.6.0)"
Bundle-ActivationPolicy: lazy
Bundle-RequiredExecutionEnvironment: JavaSE-1.6
diff --git a/de.bmotionstudio.rodin/META-INF/MANIFEST.MF b/de.bmotionstudio.rodin/META-INF/MANIFEST.MF
index 3347d0705525e9327f7402141c5aed8d346f69db..360c3fa5618b3b8a8c13988958c0d325bcd4d256 100644
--- a/de.bmotionstudio.rodin/META-INF/MANIFEST.MF
+++ b/de.bmotionstudio.rodin/META-INF/MANIFEST.MF
@@ -2,8 +2,8 @@ Manifest-Version: 1.0
Bundle-ManifestVersion: 2
Bundle-Name: BMotion Studio Rodin Integration
Bundle-SymbolicName: de.bmotionstudio.rodin;singleton:=true
-Bundle-Version: 1.0.3.qualifier
-Fragment-Host: de.bmotionstudio.gef.editor;bundle-version="5.2.1"
+Bundle-Version: 1.1.0.qualifier
+Fragment-Host: de.bmotionstudio.gef.editor;bundle-version="[5.4.0,5.5.0)"
Bundle-RequiredExecutionEnvironment: JavaSE-1.6
Bundle-Vendor: HHU Düsseldorf STUPS Group
Require-Bundle: org.eclipse.ui.navigator;bundle-version="3.5.0"
diff --git a/de.prob.core/META-INF/MANIFEST.MF b/de.prob.core/META-INF/MANIFEST.MF
index bc48a47fa1f59a2e1243b5c7bb20200381853d2a..e1cf9ef6e6d4630ea3dbbbc24da03219d65c3db5 100644
--- a/de.prob.core/META-INF/MANIFEST.MF
+++ b/de.prob.core/META-INF/MANIFEST.MF
@@ -2,10 +2,11 @@ Manifest-Version: 1.0
Bundle-ManifestVersion: 2
Bundle-Name: ProB Animator Core
Bundle-SymbolicName: de.prob.core;singleton:=true
-Bundle-Version: 9.2.2.qualifier
+Bundle-Version: 9.3.0.qualifier
Require-Bundle: org.eclipse.core.runtime;bundle-version="[3.5.0,4.0.0)",
org.rodinp.core;bundle-version="[1.3.1,1.7.0)",
org.eventb.core;bundle-version="[2.1.0,2.6.0)"
+REENABLE-FOR-THEORY-PLUGIN: org.eventb.theory.core;bundle-version="2.0.0"
Bundle-ActivationPolicy: lazy
Eclipse-BundleShape: dir
Bundle-Vendor: HHU Düsseldorf STUPS Group
diff --git a/de.prob.core/build.gradle b/de.prob.core/build.gradle
index 82ad7bd0a0355e26c646e7ab8a31e8f5fb3d5234..b3649c6d3744cf303464ce77818144dc264b6a2c 100644
--- a/de.prob.core/build.gradle
+++ b/de.prob.core/build.gradle
@@ -1,7 +1,7 @@
apply plugin: 'java'
-def parser_version = '2.4.8-SNAPSHOT'
+def parser_version = '2.4.12-SNAPSHOT'
dependencies {
compile group: "de.prob", name: "answerparser", version: parser_version , changing: true
diff --git a/de.prob.core/plugin.xml b/de.prob.core/plugin.xml
index 2d7b472c3f23462dc53c415d78961b70f7940e2f..b84a1eaef2043d86514040b1a698b95d501b759d 100644
--- a/de.prob.core/plugin.xml
+++ b/de.prob.core/plugin.xml
@@ -4,6 +4,7 @@
<extension-point id="de.prob.core.lifecycle" name="Lifecycle Events" schema="schema/de.prob.core.lifecycle.exsd"/>
<extension-point id="de.prob.core.computation" name="Computation Events" schema="schema/de.prob.core.computation.exsd"/>
<extension-point id="de.prob.core.animation" name="Animation Events" schema="schema/de.prob.core.animation.exsd"/>
+ <extension-point id="de.prob.translator" name="Translator Extensions" schema="schema/de.prob.translator.exsd"/>
<extension
point="de.prob.core.animation">
<listener
diff --git a/de.prob.core/schema/de.prob.translator.exsd b/de.prob.core/schema/de.prob.translator.exsd
new file mode 100644
index 0000000000000000000000000000000000000000..90efcf3ea4b5913068fc906cd4a9206a2d2860b1
--- /dev/null
+++ b/de.prob.core/schema/de.prob.translator.exsd
@@ -0,0 +1,109 @@
+<?xml version='1.0' encoding='UTF-8'?>
+<!-- Schema file written by PDE -->
+<schema targetNamespace="de.prob.core" xmlns="http://www.w3.org/2001/XMLSchema">
+<annotation>
+ <appInfo>
+ <meta.schema plugin="de.prob.core" id="de.prob.translator" name="Translator Extensions"/>
+ </appInfo>
+ <documentation>
+ [Enter description of this extension point.]
+ </documentation>
+ </annotation>
+
+ <element name="extension">
+ <annotation>
+ <appInfo>
+ <meta.element />
+ </appInfo>
+ </annotation>
+ <complexType>
+ <sequence minOccurs="0" maxOccurs="unbounded">
+ <element ref="translator"/>
+ </sequence>
+ <attribute name="point" type="string" use="required">
+ <annotation>
+ <documentation>
+
+ </documentation>
+ </annotation>
+ </attribute>
+ <attribute name="id" type="string">
+ <annotation>
+ <documentation>
+
+ </documentation>
+ </annotation>
+ </attribute>
+ <attribute name="name" type="string">
+ <annotation>
+ <documentation>
+
+ </documentation>
+ <appInfo>
+ <meta.attribute translatable="true"/>
+ </appInfo>
+ </annotation>
+ </attribute>
+ </complexType>
+ </element>
+
+ <element name="translator">
+ <complexType>
+ <attribute name="name" type="string">
+ <annotation>
+ <documentation>
+
+ </documentation>
+ </annotation>
+ </attribute>
+ <attribute name="class" type="string" use="required">
+ <annotation>
+ <documentation>
+
+ </documentation>
+ <appInfo>
+ <meta.attribute kind="java" basedOn=":de.prob.core.translator.IExternalTranslator"/>
+ </appInfo>
+ </annotation>
+ </attribute>
+ </complexType>
+ </element>
+
+ <annotation>
+ <appInfo>
+ <meta.section type="since"/>
+ </appInfo>
+ <documentation>
+ [Enter the first release in which this extension point appears.]
+ </documentation>
+ </annotation>
+
+ <annotation>
+ <appInfo>
+ <meta.section type="examples"/>
+ </appInfo>
+ <documentation>
+ [Enter extension point usage example here.]
+ </documentation>
+ </annotation>
+
+ <annotation>
+ <appInfo>
+ <meta.section type="apiinfo"/>
+ </appInfo>
+ <documentation>
+ [Enter API information here.]
+ </documentation>
+ </annotation>
+
+ <annotation>
+ <appInfo>
+ <meta.section type="implementation"/>
+ </appInfo>
+ <documentation>
+ [Enter information about supplied implementation of this extension point.]
+ </documentation>
+ </annotation>
+
+
+</schema>
diff --git a/de.prob.core/src/de/prob/core/Animator.java b/de.prob.core/src/de/prob/core/Animator.java
index ad8901b17fd22ca504219767355f4c832dd40b9e..e78a5611b36a4821ca7e01fd01fdc0075bfba21c 100644
--- a/de.prob.core/src/de/prob/core/Animator.java
+++ b/de.prob.core/src/de/prob/core/Animator.java
@@ -6,18 +6,12 @@
package de.prob.core;
-import java.io.BufferedWriter;
import java.io.File;
-import java.io.FileWriter;
-import java.io.IOException;
import java.util.HashMap;
import java.util.Map;
import org.osgi.service.prefs.Preferences;
-import com.thoughtworks.xstream.XStream;
-import com.thoughtworks.xstream.io.json.JettisonMappedXmlDriver;
-
import de.prob.core.command.IComposableCommand;
import de.prob.core.domainobjects.History;
import de.prob.core.domainobjects.MachineDescription;
@@ -29,7 +23,6 @@ import de.prob.core.internal.AnimatorImpl;
import de.prob.core.internal.ServerTraceConnection;
import de.prob.core.internal.TraceConnectionProvider;
import de.prob.exceptions.ProBException;
-import de.prob.model.eventb.Model;
/**
diff --git a/de.prob.core/src/de/prob/core/translator/IExternalTranslator.java b/de.prob.core/src/de/prob/core/translator/IExternalTranslator.java
new file mode 100644
index 0000000000000000000000000000000000000000..d01511727a1c9d8cd430d91b88066da528ecce67
--- /dev/null
+++ b/de.prob.core/src/de/prob/core/translator/IExternalTranslator.java
@@ -0,0 +1,7 @@
+package de.prob.core.translator;
+
+import de.prob.prolog.output.PrologTermOutput;
+
+public interface IExternalTranslator {
+ public void writeProlog(PrologTermOutput pto);
+}
diff --git a/de.prob.core/src/de/prob/core/translator/TranslationFailedException.java b/de.prob.core/src/de/prob/core/translator/TranslationFailedException.java
index bb5a1fb6e8b3b20d2032f27880866b171dbffd1a..f1edb0bdac9c2b72b6e03aaaa3948f0a5c6d4f60 100644
--- a/de.prob.core/src/de/prob/core/translator/TranslationFailedException.java
+++ b/de.prob.core/src/de/prob/core/translator/TranslationFailedException.java
@@ -18,8 +18,12 @@ public class TranslationFailedException extends ProBException {
public TranslationFailedException(final String component,
final String details) {
- super("Translation of " + component + " failed\n" + details);
- notifyUserOnce();
+ this(component, details, null);
}
+ public TranslationFailedException(final String component,
+ final String details, Throwable e) {
+ super("Translation of " + component + " failed\n" + details, e, false);
+ notifyUserOnce();
+ }
}
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 340c94557f3d396764624d39a1ab2a831fc80e26..9ea99009688c58a066ad0add611d91b1e6a429a6 100644
--- a/de.prob.core/src/de/prob/eventb/translator/ContextTranslator.java
+++ b/de.prob.core/src/de/prob/eventb/translator/ContextTranslator.java
@@ -66,14 +66,13 @@ public final class ContextTranslator extends AbstractComponentTranslator {
private final List<DischargedProof> proofs = new ArrayList<DischargedProof>();
private final List<ClassifiedPragma> proofspragmas = new ArrayList<ClassifiedPragma>();
private final FormulaFactory ff;
-
- // Confined in the thread calling the factory method
private ITypeEnvironment te;
public static ContextTranslator create(final ISCContext context)
throws TranslationFailedException {
ContextTranslator contextTranslator = new ContextTranslator(context);
try {
+ (new TheoryTranslator()).translate();
contextTranslator.translate();
} catch (RodinDBException e) {
final String message = "A Rodin exception occured during translation process. Possible cause: building aborted or still in progress. Please wait until building has finished before starting ProB. If this does not help, perform a clean and start ProB after building has finished. Original Exception: ";
@@ -90,11 +89,20 @@ public final class ContextTranslator extends AbstractComponentTranslator {
* contains errors)
*
* @param context
+ * @throws TranslationFailedException
* @throws RodinDBException
*/
- private ContextTranslator(final ISCContext context) {
+ private ContextTranslator(final ISCContext context)
+ throws TranslationFailedException {
this.context = context;
- ff = FormulaFactory.getDefault();
+ ff = ((ISCContextRoot) context).getFormulaFactory();
+ try {
+ te = ((ISCContextRoot) context).getTypeEnvironment(ff);
+ } catch (RodinDBException e) {
+ final String message = "A Rodin exception occured during translation process. Original Exception: ";
+ throw new TranslationFailedException(context.getComponentName(),
+ message + e.getLocalizedMessage());
+ }
}
private void translate() throws RodinDBException {
@@ -102,7 +110,6 @@ public final class ContextTranslator extends AbstractComponentTranslator {
ISCContextRoot context_root = (ISCContextRoot) context;
Assert.isTrue(context_root.getRodinFile().isConsistent());
te = context_root.getTypeEnvironment(ff);
- collectProofInfo(context_root);
} else if (context instanceof ISCInternalContext) {
ISCInternalContext context_internal = (ISCInternalContext) context;
@@ -124,9 +131,9 @@ public final class ContextTranslator extends AbstractComponentTranslator {
ISCMachineRoot machine_root = (ISCMachineRoot) context_internal
.getRoot();
Assert.isTrue(machine_root.getRodinFile().isConsistent());
- te = machine_root.getTypeEnvironment(ff);
}
translateContext();
+
}
private void collectProofInfo(ISCContextRoot context_root)
@@ -313,7 +320,6 @@ public final class ContextTranslator extends AbstractComponentTranslator {
final PredicateVisitor visitor = new PredicateVisitor(
new LinkedList<String>());
element.getPredicate(ff, te).accept(visitor);
-
final PPredicate predicate = visitor.getPredicate();
list.add(predicate);
labelMapping.put(predicate, element);
diff --git a/de.prob.core/src/de/prob/eventb/translator/ExpressionVisitor.java b/de.prob.core/src/de/prob/eventb/translator/ExpressionVisitor.java
index 49af627156fefc608f681e454c9291c95f2d0803..96a04d1a9eb4ae1667be87ccca45209656782dbe 100644
--- a/de.prob.core/src/de/prob/eventb/translator/ExpressionVisitor.java
+++ b/de.prob.core/src/de/prob/eventb/translator/ExpressionVisitor.java
@@ -20,6 +20,7 @@ import org.eventb.core.ast.BoolExpression;
import org.eventb.core.ast.BoundIdentDecl;
import org.eventb.core.ast.BoundIdentifier;
import org.eventb.core.ast.Expression;
+import org.eventb.core.ast.ExtendedExpression;
import org.eventb.core.ast.Formula;
import org.eventb.core.ast.FreeIdentifier;
import org.eventb.core.ast.ISimpleVisitor;
@@ -28,6 +29,7 @@ import org.eventb.core.ast.Predicate;
import org.eventb.core.ast.QuantifiedExpression;
import org.eventb.core.ast.SetExtension;
import org.eventb.core.ast.UnaryExpression;
+import org.eventb.core.ast.extension.IExpressionExtension;
import de.be4.classicalb.core.parser.node.AAddExpression;
import de.be4.classicalb.core.parser.node.ABoolSetExpression;
@@ -50,6 +52,7 @@ import de.be4.classicalb.core.parser.node.AEventBFirstProjectionV2Expression;
import de.be4.classicalb.core.parser.node.AEventBIdentityExpression;
import de.be4.classicalb.core.parser.node.AEventBSecondProjectionExpression;
import de.be4.classicalb.core.parser.node.AEventBSecondProjectionV2Expression;
+import de.be4.classicalb.core.parser.node.AExtendedExprExpression;
import de.be4.classicalb.core.parser.node.AFunctionExpression;
import de.be4.classicalb.core.parser.node.AGeneralIntersectionExpression;
import de.be4.classicalb.core.parser.node.AGeneralUnionExpression;
@@ -112,7 +115,6 @@ public class ExpressionVisitor extends SimpleVisitorAdapter implements // NOPMD
// we need some abilities of the linked list, using List is not an option
private boolean expressionSet = false;
- @SuppressWarnings("unused")
private ExpressionVisitor() { // we want to prevent clients from calling
// the default constructor
super();
@@ -157,15 +159,14 @@ public class ExpressionVisitor extends SimpleVisitorAdapter implements // NOPMD
list.add(visitor.getExpression());
}
- // Process internal Expression and Predcate
+ // Process internal Expression and Predicate
final Predicate predicate = expression.getPredicate();
final PredicateVisitor predicateVisitor = new PredicateVisitor(bounds);
predicate.accept(predicateVisitor);
final PPredicate pr = predicateVisitor.getPredicate();
- final ExpressionVisitor expressionVisitor = new ExpressionVisitor(
- bounds);
+ final ExpressionVisitor expressionVisitor = new ExpressionVisitor();
expression.getExpression().accept(expressionVisitor);
final PExpression ex = expressionVisitor.getExpression();
@@ -619,6 +620,41 @@ public class ExpressionVisitor extends SimpleVisitorAdapter implements // NOPMD
setExpression(setExtensionExpression);
}
+ @Override
+ public void visitExtendedExpression(ExtendedExpression expression) {
+ AExtendedExprExpression p = new AExtendedExprExpression();
+
+ IExpressionExtension extension = expression.getExtension();
+ String symbol = extension.getSyntaxSymbol();
+ Object origin = extension.getOrigin();
+
+ // FIXME THEORY-PLUGIN re-enable when the theory plugin was released
+ // Theories.addOrigin(origin);
+
+ p.setIdentifier(new TIdentifierLiteral(symbol));
+ Expression[] expressions = expression.getChildExpressions();
+ List<PExpression> childExprs = new ArrayList<PExpression>();
+ for (Expression e : expressions) {
+ ExpressionVisitor v = new ExpressionVisitor(
+ new LinkedList<String>());
+ e.accept(v);
+ childExprs.add(v.getExpression());
+ }
+ p.setExpressions(childExprs);
+
+ Predicate[] childPredicates = expression.getChildPredicates();
+ List<PPredicate> childPreds = new ArrayList<PPredicate>();
+ for (Predicate pd : childPredicates) {
+ PredicateVisitor v = new PredicateVisitor(null);
+ pd.accept(v);
+ childPreds.add(v.getPredicate());
+ }
+ p.setPredicates(childPreds);
+
+ setExpression(p);
+
+ }
+
@SuppressWarnings("deprecation")
@Override
public void visitUnaryExpression(final UnaryExpression expression) { // NOPMD
diff --git a/de.prob.core/src/de/prob/eventb/translator/PredicateVisitor.java b/de.prob.core/src/de/prob/eventb/translator/PredicateVisitor.java
index 7094ecabecf5f2ed6abe1799ca4bca63ff594463..035811a2be35d24c8b52eb576e29a7dc5b5c37b0 100644
--- a/de.prob.core/src/de/prob/eventb/translator/PredicateVisitor.java
+++ b/de.prob.core/src/de/prob/eventb/translator/PredicateVisitor.java
@@ -15,6 +15,7 @@ import org.eventb.core.ast.AssociativePredicate;
import org.eventb.core.ast.BinaryPredicate;
import org.eventb.core.ast.BoundIdentDecl;
import org.eventb.core.ast.Expression;
+import org.eventb.core.ast.ExtendedPredicate;
import org.eventb.core.ast.Formula;
import org.eventb.core.ast.ISimpleVisitor;
import org.eventb.core.ast.LiteralPredicate;
@@ -24,12 +25,14 @@ import org.eventb.core.ast.QuantifiedPredicate;
import org.eventb.core.ast.RelationalPredicate;
import org.eventb.core.ast.SimplePredicate;
import org.eventb.core.ast.UnaryPredicate;
+import org.eventb.core.ast.extension.IPredicateExtension;
import de.be4.classicalb.core.parser.node.AConjunctPredicate;
import de.be4.classicalb.core.parser.node.ADisjunctPredicate;
import de.be4.classicalb.core.parser.node.AEqualPredicate;
import de.be4.classicalb.core.parser.node.AEquivalencePredicate;
import de.be4.classicalb.core.parser.node.AExistsPredicate;
+import de.be4.classicalb.core.parser.node.AExtendedPredPredicate;
import de.be4.classicalb.core.parser.node.AFalsityPredicate;
import de.be4.classicalb.core.parser.node.AFinitePredicate;
import de.be4.classicalb.core.parser.node.AForallPredicate;
@@ -50,6 +53,7 @@ import de.be4.classicalb.core.parser.node.ASubsetStrictPredicate;
import de.be4.classicalb.core.parser.node.ATruthPredicate;
import de.be4.classicalb.core.parser.node.PExpression;
import de.be4.classicalb.core.parser.node.PPredicate;
+import de.be4.classicalb.core.parser.node.TIdentifierLiteral;
import de.prob.eventb.translator.internal.SimpleVisitorAdapter;
public class PredicateVisitor extends SimpleVisitorAdapter implements // NOPMD
@@ -76,12 +80,19 @@ public class PredicateVisitor extends SimpleVisitorAdapter implements // NOPMD
predicateSet = true;
this.p = p;
}
- //public ClassifiedPragma(String name, Node attachedTo, List<String> arguments, List<String> warnings, SourcePosition start, SourcePosition end) {
-
- // new ClassifiedPragma("discharged", p, proof, Collections.emptyList(), new SourcePosition(-1, -1), new SourcePosition(-1, -1));
+ // public ClassifiedPragma(String name, Node attachedTo, List<String>
+ // arguments, List<String> warnings, SourcePosition start,
+ // SourcePosition end) {
+
+ // new ClassifiedPragma("discharged", p, proof, Collections.emptyList(),
+ // new SourcePosition(-1, -1), new SourcePosition(-1, -1));
+ }
+
+ public PredicateVisitor() {
+ this(null);
}
- public PredicateVisitor(final LinkedList<String> bounds) {
+ public PredicateVisitor(LinkedList<String> bounds) {
super();
if (bounds == null) {
this.bounds = new LinkedList<String>();
@@ -90,10 +101,6 @@ public class PredicateVisitor extends SimpleVisitorAdapter implements // NOPMD
}
}
- public PredicateVisitor() {
- this(null);
- }
-
@Override
public void visitQuantifiedPredicate(final QuantifiedPredicate predicate) {
final int tag = predicate.getTag();
@@ -406,4 +413,37 @@ public class PredicateVisitor extends SimpleVisitorAdapter implements // NOPMD
setPredicate(result);
}
+ @Override
+ public void visitExtendedPredicate(ExtendedPredicate predicate) {
+ AExtendedPredPredicate p = new AExtendedPredPredicate();
+ IPredicateExtension extension = predicate.getExtension();
+ String symbol = extension.getSyntaxSymbol();
+ Object origin = extension.getOrigin();
+
+ // FIXME THEORY-PLUGIN re-enable when the theory plugin was released
+
+ // Theories.addOrigin(origin);
+
+ p.setIdentifier(new TIdentifierLiteral(symbol));
+
+ Expression[] expressions = predicate.getChildExpressions();
+ List<PExpression> childExprs = new ArrayList<PExpression>();
+ for (Expression e : expressions) {
+ ExpressionVisitor v = new ExpressionVisitor(bounds);
+ e.accept(v);
+ childExprs.add(v.getExpression());
+ }
+ p.setExpressions(childExprs);
+
+ Predicate[] childPredicates = predicate.getChildPredicates();
+ List<PPredicate> childPreds = new ArrayList<PPredicate>();
+ for (Predicate pd : childPredicates) {
+ PredicateVisitor v = new PredicateVisitor(bounds);
+ pd.accept(v);
+ childPreds.add(v.getPredicate());
+ }
+ p.setPredicates(childPreds);
+ setPredicate(p);
+ }
+
}
diff --git a/de.prob.core/src/de/prob/eventb/translator/Theories.java b/de.prob.core/src/de/prob/eventb/translator/Theories.java
new file mode 100644
index 0000000000000000000000000000000000000000..a74d82914e8f220539a04cf6a36eff7a0025293a
--- /dev/null
+++ b/de.prob.core/src/de/prob/eventb/translator/Theories.java
@@ -0,0 +1,198 @@
+package de.prob.eventb.translator;
+
+
+// FIXME THEORY-PLUGIN re-enable when the theory plugin was released
+
+public class Theories {
+
+// private static Map<String, IDeployedTheoryRoot> theories = new TreeMap<String, IDeployedTheoryRoot>();
+//
+// public static final ITypeEnvironment global_te = FormulaFactory
+// .getDefault().makeTypeEnvironment();
+//
+// public static void addOrigin(Object origin) {
+// if (origin instanceof ISCNewOperatorDefinition) {
+// final IDeployedTheoryRoot theory = (IDeployedTheoryRoot) ((ISCNewOperatorDefinition) origin)
+// .getParent();
+// final String name = theory.getElementName();
+// theories.put(name, theory);
+// } else {
+// System.out.println("Did not register origin: "
+// + origin.getClass().getName());
+// }
+// }
+//
+// public static void translate(IPrologTermOutput pto) throws RodinDBException {
+// for (IDeployedTheoryRoot theory : theories.values()) {
+// printTranslation(theory, pto);
+// }
+// }
+//
+// private static void printTranslation(IDeployedTheoryRoot theory,
+// IPrologTermOutput pto) throws RodinDBException {
+// pto.openTerm("theory");
+// printTypeParameters(theory, pto);
+// printDataTypes(theory, pto);
+// printOperatorDefs(theory, pto);
+// pto.closeTerm();
+// }
+//
+// private static void printTypeParameters(IFormulaExtensionsSource theory,
+// IPrologTermOutput pto) throws RodinDBException {
+// pto.openList();
+// for (ISCTypeParameter parameter : theory.getSCTypeParameters()) {
+// pto.printAtom(parameter.getIdentifierString());
+// }
+// pto.closeList();
+// }
+//
+// private static void printDataTypes(IDeployedTheoryRoot theory,
+// IPrologTermOutput pto) throws RodinDBException {
+// final FormulaFactory ff = theory.getFormulaFactory();
+// pto.openList();
+// for (ISCDatatypeDefinition def : theory.getSCDatatypeDefinitions()) {
+// printDataType(def, ff, pto);
+// }
+// pto.closeList();
+// }
+//
+// private static void printDataType(ISCDatatypeDefinition def,
+// FormulaFactory ff, IPrologTermOutput pto) throws RodinDBException {
+// pto.openTerm("datatype");
+// pto.printAtom(def.getIdentifierString());
+// pto.openList();
+// for (ISCTypeArgument arg : def.getTypeArguments()) {
+// printType(arg.getSCGivenType(ff), ff, pto);
+// }
+// pto.closeList();
+// pto.openList();
+// for (ISCDatatypeConstructor cons : def.getConstructors()) {
+// printConstructor(cons, ff, pto);
+// }
+// pto.closeList();
+// pto.closeTerm();
+//
+// }
+//
+// private static void printConstructor(ISCDatatypeConstructor cons,
+// FormulaFactory ff, IPrologTermOutput pto) throws RodinDBException {
+// pto.openTerm("constructor");
+// pto.printAtom(cons.getIdentifierString());
+// pto.openList();
+// for (ISCConstructorArgument arg : cons.getConstructorArguments()) {
+// printTypedIdentifier("destructor", arg, ff, pto);
+// }
+// pto.closeList();
+// pto.closeTerm();
+//
+// }
+//
+// private static void printOperatorDefs(IDeployedTheoryRoot theory,
+// IPrologTermOutput pto) throws RodinDBException {
+// pto.openList();
+// for (ISCNewOperatorDefinition opdef : theory
+// .getSCNewOperatorDefinitions()) {
+// printOperator(opdef, theory, pto);
+// }
+// pto.closeList();
+// }
+//
+// private static void printOperator(ISCNewOperatorDefinition opDef,
+// IDeployedTheoryRoot theory, IPrologTermOutput prologOutput)
+// throws RodinDBException {
+//
+// prologOutput.openTerm("operator");
+// prologOutput.printAtom(opDef.getLabel());
+//
+// final FormulaFactory ff = theory.getFormulaFactory();
+// final ITypeEnvironment te = theory.getTypeEnvironment(ff);
+//
+// // Arguments
+// prologOutput.openList();
+// ISCOperatorArgument[] operatorArguments = opDef.getOperatorArguments();
+// for (ISCOperatorArgument argument : operatorArguments) {
+// printTypedIdentifier("argument", argument, ff, prologOutput);
+// }
+// prologOutput.closeList();
+//
+// // WD Condition
+// Predicate wdCondition = opDef.getWDCondition(ff, te);
+// printPredicate(prologOutput, wdCondition);
+//
+// // Direct Definitions
+// prologOutput.openList();
+// processDefinitions(ff, te, prologOutput,
+// opDef.getDirectOperatorDefinitions());
+// prologOutput.closeList();
+//
+// // Recursive Definitions
+// prologOutput.openList();
+// ISCRecursiveOperatorDefinition[] definitions = opDef
+// .getRecursiveOperatorDefinitions();
+// for (ISCRecursiveOperatorDefinition definition : definitions) {
+// ISCRecursiveDefinitionCase[] recursiveDefinitionCases = definition
+// .getRecursiveDefinitionCases();
+// for (ISCRecursiveDefinitionCase c : recursiveDefinitionCases) {
+// Expression ex = c.getExpression(ff, te);
+// printExpression(prologOutput, ex);
+// }
+// }
+// prologOutput.closeList();
+//
+// prologOutput.closeTerm();
+// }
+//
+// private static void processDefinitions(FormulaFactory ff,
+// ITypeEnvironment te, IPrologTermOutput prologOutput,
+// ISCDirectOperatorDefinition[] directOperatorDefinitions)
+// throws RodinDBException {
+// for (ISCDirectOperatorDefinition def : directOperatorDefinitions) {
+// Formula<?> scFormula = def.getSCFormula(ff, te);
+//
+// if (scFormula instanceof Predicate) {
+// Predicate pp = (Predicate) scFormula;
+// printPredicate(prologOutput, pp);
+// }
+// if (scFormula instanceof Expression) {
+// Expression pp = (Expression) scFormula;
+// printExpression(prologOutput, pp);
+// }
+//
+// }
+// }
+//
+// private static void printTypedIdentifier(final String functor,
+// final ISCIdentifierElement id, final FormulaFactory ff,
+// final IPrologTermOutput pto) throws RodinDBException {
+// pto.openTerm(functor);
+// pto.printAtom(id.getIdentifierString());
+// printType(id.getType(ff), ff, pto);
+// pto.closeTerm();
+// }
+//
+// private static void printType(final Type type, final FormulaFactory ff,
+// final IPrologTermOutput pto) {
+// printExpression(pto, type.toExpression(ff));
+// }
+//
+// private static void printExpression(IPrologTermOutput prologOutput,
+// Expression pp) {
+// ExpressionVisitor visitor = new ExpressionVisitor(
+// new LinkedList<String>());
+// pp.accept(visitor);
+// PExpression ex = visitor.getExpression();
+// ASTProlog pv = new ASTProlog(prologOutput, null);
+// ex.apply(pv);
+// }
+//
+// private static void printPredicate(IPrologTermOutput prologOutput,
+// Predicate pp) {
+// PredicateVisitor visitor = new PredicateVisitor(
+// new LinkedList<String>());
+// pp.accept(visitor);
+// PPredicate predicate = visitor.getPredicate();
+// ASTProlog pv = new ASTProlog(prologOutput, null);
+// predicate.apply(pv);
+// }
+
+}
diff --git a/de.prob.core/src/de/prob/eventb/translator/TheoryTranslator.java b/de.prob.core/src/de/prob/eventb/translator/TheoryTranslator.java
new file mode 100644
index 0000000000000000000000000000000000000000..d31ff06a2e8cfe0f759cd5a3e1390ad44bc49ea0
--- /dev/null
+++ b/de.prob.core/src/de/prob/eventb/translator/TheoryTranslator.java
@@ -0,0 +1,23 @@
+package de.prob.eventb.translator;
+
+import org.eclipse.core.runtime.IConfigurationElement;
+import org.eclipse.core.runtime.IExtension;
+import org.eclipse.core.runtime.IExtensionPoint;
+import org.eclipse.core.runtime.IExtensionRegistry;
+import org.eclipse.core.runtime.Platform;
+
+public class TheoryTranslator {
+
+ public void translate() {
+ final IExtensionRegistry extensionRegistry = Platform
+ .getExtensionRegistry();
+ final IExtensionPoint extensionPoint = extensionRegistry
+ .getExtensionPoint("org.eventb.theory.core.deployedElements");
+ for (final IExtension extension : extensionPoint.getExtensions()) {
+ for (final IConfigurationElement configurationElement : extension
+ .getConfigurationElements()) {
+ System.out.println(configurationElement.getAttribute("name"));
+ }
+ }
+ }
+}
diff --git a/de.prob.core/src/de/prob/eventb/translator/TranslatorFactory.java b/de.prob.core/src/de/prob/eventb/translator/TranslatorFactory.java
index 0e9a5d1af765473e700a8e24a4306f0caa3d2441..8f7d0c95826235ae17633361922c7237640c9396 100644
--- a/de.prob.core/src/de/prob/eventb/translator/TranslatorFactory.java
+++ b/de.prob.core/src/de/prob/eventb/translator/TranslatorFactory.java
@@ -33,6 +33,7 @@ public class TranslatorFactory {
*/
public static void translate(final IEventBRoot root,
final IPrologTermOutput pto) throws TranslationFailedException {
+
if (root instanceof IMachineRoot) {
final ISCMachineRoot scRoot = ((IMachineRoot) root)
.getSCMachineRoot();
diff --git a/de.prob.core/src/de/prob/eventb/translator/internal/EventBTranslator.java b/de.prob.core/src/de/prob/eventb/translator/internal/EventBTranslator.java
index 54eb566182fa3856b663293d6f4072e46f81e82b..43ea5792f26eee7de07938f106ef26696642a2c8 100644
--- a/de.prob.core/src/de/prob/eventb/translator/internal/EventBTranslator.java
+++ b/de.prob.core/src/de/prob/eventb/translator/internal/EventBTranslator.java
@@ -27,6 +27,7 @@ import de.prob.core.translator.ITranslator;
import de.prob.core.translator.TranslationFailedException;
import de.prob.eventb.translator.AbstractComponentTranslator;
import de.prob.eventb.translator.ContextTranslator;
+import de.prob.eventb.translator.Theories;
import de.prob.prolog.output.IPrologTermOutput;
public abstract class EventBTranslator implements ITranslator {
@@ -143,6 +144,13 @@ public abstract class EventBTranslator implements ITranslator {
pout.openList();
printProofInformation(refinementChainTranslators, contextTranslators,
pout);
+ // FIXME THEORY-PLUGIN re-enable when the theory plugin was released
+
+ // try {
+ // Theories.translate(pout);
+ // } catch (RodinDBException e) {
+ // e.printStackTrace();
+ // }
pout.closeList();
pout.printVariable("_Error");
pout.closeTerm();
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 ba6f53a2ec7b4238cc99f87f50a16c33226f7132..d9fdf6fbb66e8880d7577915fe8fc80d36a17c87 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
@@ -77,13 +77,13 @@ public class ModelTranslator extends AbstractComponentTranslator {
private final ISCMachineRoot machine;
private final AEventBModelParseUnit model = new AEventBModelParseUnit();
- private final FormulaFactory ff = FormulaFactory.getDefault();;
+ private final FormulaFactory ff;
+ private final ITypeEnvironment te;
private final IMachineRoot origin;
private final List<DischargedProof> proofs = new ArrayList<DischargedProof>();
// private final List<String> depContext = new ArrayList<String>();
// Confined in the thread calling the factory method
- private ITypeEnvironment te;
private String refines;
private boolean broken = false;
@@ -137,9 +137,18 @@ public class ModelTranslator extends AbstractComponentTranslator {
// ###############################################################################################################################################################
// Implementation
- private ModelTranslator(final ISCMachineRoot currentMachine) {
- this.machine = currentMachine;
+ private ModelTranslator(final ISCMachineRoot machine)
+ throws TranslationFailedException {
+ this.machine = machine;
origin = machine.getMachineRoot();
+ ff = ((ISCMachineRoot) machine).getFormulaFactory();
+ try {
+ te = ((ISCMachineRoot) machine).getTypeEnvironment(ff);
+ } catch (RodinDBException e) {
+ final String message = "A Rodin exception occured during translation process. Original Exception: ";
+ throw new TranslationFailedException(machine.getComponentName(),
+ message + e.getLocalizedMessage());
+ }
}
private void translate() throws RodinDBException,
@@ -151,8 +160,6 @@ public class ModelTranslator extends AbstractComponentTranslator {
broken = !machine.isAccurate(); // isAccurate() is not transitive, we
// need to collect the information also
// for the events
- te = machine.getTypeEnvironment(ff);
-
translateMachine();
// Check for fully discharged Invariants and Events
diff --git a/de.prob.plugin/META-INF/MANIFEST.MF b/de.prob.plugin/META-INF/MANIFEST.MF
index 24202af6eb41c3f85b4e1d5345dda77b95a4de61..35b77a2148d75ceb3a3c4b74cc62234c662a31f3 100644
--- a/de.prob.plugin/META-INF/MANIFEST.MF
+++ b/de.prob.plugin/META-INF/MANIFEST.MF
@@ -2,7 +2,7 @@ Manifest-Version: 1.0
Bundle-ManifestVersion: 2
Bundle-Name: ProB Rodin2 UI Bindings
Bundle-SymbolicName: de.prob.plugin;singleton:=true
-Bundle-Version: 2.1.3.qualifier
-Fragment-Host: de.prob.ui;bundle-version="[7.2.0,7.3.0)"
+Bundle-Version: 2.2.0.qualifier
+Fragment-Host: de.prob.ui;bundle-version="[7.3.0,7.4.0)"
Bundle-RequiredExecutionEnvironment: JavaSE-1.6
Bundle-Vendor: HHU Düsseldorf STUPS Group
diff --git a/de.prob.ui/META-INF/MANIFEST.MF b/de.prob.ui/META-INF/MANIFEST.MF
index 0ab9a6cf07669d654268e69b8f68c9b0964f3c49..0292f6b17151194d687a1bdffa1d3ffd3a2a4e35 100644
--- a/de.prob.ui/META-INF/MANIFEST.MF
+++ b/de.prob.ui/META-INF/MANIFEST.MF
@@ -2,17 +2,15 @@ Manifest-Version: 1.0
Bundle-ManifestVersion: 2
Bundle-Name: ProB Ui Plug-in
Bundle-SymbolicName: de.prob.ui;singleton:=true
-Bundle-Version: 7.2.2.qualifier
+Bundle-Version: 7.3.0.qualifier
Require-Bundle: org.eclipse.ui;bundle-version="[3.5.0,4.0.0)",
org.eclipse.core.runtime;bundle-version="[3.5.0,4.0.0)",
org.eclipse.core.resources;bundle-version="[3.5.0,4.0.0)",
org.eclipse.ui.ide;bundle-version="[3.5.0,4.0.0)",
- de.prob.core;bundle-version="[9.2.0,9.3.0)",
+ de.prob.core;bundle-version="[9.3.0,9.4.0)",
org.eventb.core;bundle-version="[2.1.0,2.6.0)",
org.eclipse.core.expressions;bundle-version="[3.4.101,4.0.0)",
- org.eclipse.gef;bundle-version="[3.5.0,4.0.0)",
- org.eventb.emf.core;bundle-version="2.2.4",
- org.eventb.emf.persistence;bundle-version="2.4.0"
+ org.eclipse.gef;bundle-version="[3.5.0,4.0.0)"
Bundle-ActivationPolicy: lazy
Bundle-Vendor: HHU Düsseldorf STUPS Group
Bundle-Activator: de.prob.ui.ProbUiPlugin
diff --git a/de.prob.ui/plugin.xml b/de.prob.ui/plugin.xml
index 31a3a0a82deaec1c94bd4eea20d9cfd4df7530db..a8edde201a3de97737dd4a38086703bde5240114 100644
--- a/de.prob.ui/plugin.xml
+++ b/de.prob.ui/plugin.xml
@@ -727,7 +727,7 @@
<handler
commandId="de.prob.ui.newcore.export">
<class
- class="de.prob.ui.eventb.ExportNewCoreHandler">
+ class="de.prob.ui.eventb.ExportClassicHandler">
</class>
<enabledWhen>
<with
diff --git a/de.prob.ui/src/de/prob/ui/eventb/ExportNewCoreHandler.java b/de.prob.ui/src/de/prob/ui/eventb/ExportNewCoreHandler.java
index cbb940a1eae628b8e71031a4aee296f03610be73..2b2f7f8492fa31ad6c2bc83f345f2bcfbc7767b7 100644
--- a/de.prob.ui/src/de/prob/ui/eventb/ExportNewCoreHandler.java
+++ b/de.prob.ui/src/de/prob/ui/eventb/ExportNewCoreHandler.java
@@ -1,14 +1,11 @@
package de.prob.ui.eventb;
-import java.io.ByteArrayOutputStream;
import java.io.File;
import java.io.FileWriter;
import java.io.IOException;
import java.io.PrintWriter;
import java.io.Writer;
-import java.util.zip.GZIPOutputStream;
-import org.apache.commons.codec.binary.Base64;
import org.eclipse.core.commands.AbstractHandler;
import org.eclipse.core.commands.ExecutionEvent;
import org.eclipse.core.commands.ExecutionException;
@@ -24,18 +21,12 @@ import org.eclipse.swt.widgets.Shell;
import org.eclipse.ui.handlers.HandlerUtil;
import org.eventb.core.IEventBRoot;
import org.eventb.core.IMachineRoot;
-import org.eventb.emf.core.Project;
-import org.eventb.emf.persistence.ProjectResource;
import org.osgi.service.prefs.BackingStoreException;
import org.osgi.service.prefs.Preferences;
-import org.rodinp.core.IRodinProject;
-
-import com.thoughtworks.xstream.XStream;
import de.prob.core.translator.TranslationFailedException;
import de.prob.eventb.translator.TranslatorFactory;
import de.prob.logging.Logger;
-import de.prob.model.eventb.Model;
public class ExportNewCoreHandler extends AbstractHandler implements IHandler {
@@ -100,15 +91,6 @@ public class ExportNewCoreHandler extends AbstractHandler implements IHandler {
final IEventBRoot root) {
final boolean isSafeToWrite = isSafeToWrite(filename);
- IRodinProject rodinProject = root.getRodinProject();
- ProjectResource resource = new ProjectResource(rodinProject);
- try {
- resource.load(null);
- } catch (IOException e) {
- e.printStackTrace();
- }
- Project project = (Project) resource.getContents().get(0);
-
if (isSafeToWrite) {
Writer fw = null;
try {
@@ -116,9 +98,6 @@ public class ExportNewCoreHandler extends AbstractHandler implements IHandler {
TranslatorFactory.translate(root, new PrintWriter(fw));
fw.append('\n');
- fw.append("eclipse_model('" + root.getComponentName() + "',\""
- + serialize(project, root.getComponentName()) + "\").");
-
} catch (TranslationFailedException e) {
e.notifyUserOnce();
} catch (IOException e) {
@@ -134,25 +113,25 @@ public class ExportNewCoreHandler extends AbstractHandler implements IHandler {
}
}
- private static String serialize(Project project, String maincomponent) {
- NewCoreModelTranslation translation = new NewCoreModelTranslation();
- Model model = translation.translate(project, maincomponent);
- // XStream xstream = new XStream(new JettisonMappedXmlDriver());
- XStream xstream = new XStream();
- String xml = xstream.toXML(model);
- ByteArrayOutputStream out = new ByteArrayOutputStream();
- GZIPOutputStream gzip;
- byte[] bytes;
- try {
- gzip = new GZIPOutputStream(out);
- gzip.write(xml.getBytes());
- gzip.close();
- bytes = out.toByteArray();
- } catch (IOException e) {
- bytes = xml.getBytes();
- }
- return Base64.encodeBase64String(bytes);
- }
+ // private static String serialize(Project project, String maincomponent) {
+ // NewCoreModelTranslation translation = new NewCoreModelTranslation();
+ // Model model = translation.translate(project, maincomponent);
+ // // XStream xstream = new XStream(new JettisonMappedXmlDriver());
+ // XStream xstream = new XStream();
+ // String xml = xstream.toXML(model);
+ // ByteArrayOutputStream out = new ByteArrayOutputStream();
+ // GZIPOutputStream gzip;
+ // byte[] bytes;
+ // try {
+ // gzip = new GZIPOutputStream(out);
+ // gzip.write(xml.getBytes());
+ // gzip.close();
+ // bytes = out.toByteArray();
+ // } catch (IOException e) {
+ // bytes = xml.getBytes();
+ // }
+ // return Base64.encodeBase64String(bytes);
+ // }
private static boolean isSafeToWrite(final String filename) {
if (new File(filename).exists()) {
diff --git a/de.prob.ui/src/de/prob/ui/eventb/NewCoreModelTranslation.java b/de.prob.ui/src/de/prob/ui/eventb/NewCoreModelTranslation.java
deleted file mode 100644
index a95105e2548f3bbf6a54001a7a4bc17eb6768939..0000000000000000000000000000000000000000
--- a/de.prob.ui/src/de/prob/ui/eventb/NewCoreModelTranslation.java
+++ /dev/null
@@ -1,154 +0,0 @@
-package de.prob.ui.eventb;
-
-import static de.prob.model.representation.RefType.ERefType.*;
-
-import java.util.HashMap;
-import java.util.Map;
-import java.util.Map.Entry;
-
-import org.eclipse.emf.common.util.EList;
-import org.eventb.emf.core.EventBNamedCommentedComponentElement;
-import org.eventb.emf.core.Project;
-import org.eventb.emf.core.context.Axiom;
-import org.eventb.emf.core.context.CarrierSet;
-import org.eventb.emf.core.context.Constant;
-import org.eventb.emf.core.context.Context;
-import org.eventb.emf.core.machine.Action;
-import org.eventb.emf.core.machine.Event;
-import org.eventb.emf.core.machine.Guard;
-import org.eventb.emf.core.machine.Invariant;
-import org.eventb.emf.core.machine.Machine;
-import org.eventb.emf.core.machine.Parameter;
-import org.eventb.emf.core.machine.Variable;
-import org.eventb.emf.core.machine.Variant;
-import org.eventb.emf.core.machine.Witness;
-
-import de.prob.model.eventb.EBContext;
-import de.prob.model.eventb.EBEvent;
-import de.prob.model.eventb.EBMachine;
-import de.prob.model.eventb.Model;
-import de.prob.model.representation.Label;
-
-public class NewCoreModelTranslation {
-
- private HashMap<String, Label> components;
-
- public Model translate(final Project p, final String mainComponent) {
- this.components = new HashMap<String, Label>();
-
- Model model = new Model(mainComponent);
-
- final Map<String, EventBNamedCommentedComponentElement> allComponents = new HashMap<String, EventBNamedCommentedComponentElement>();
-
- for (final EventBNamedCommentedComponentElement cmpt : p
- .getComponents()) {
- final String name = cmpt.doGetName();
- allComponents.put(name, cmpt);
- if (cmpt instanceof Context) {
- components.put(name, createContext((Context) cmpt));
-
- } else if (cmpt instanceof Machine) {
- components.put(name, createMachine((Machine) cmpt));
- }
- }
-
- for (Entry<String, EventBNamedCommentedComponentElement> entry : allComponents
- .entrySet()) {
-
- EventBNamedCommentedComponentElement element = entry.getValue();
-
- final String name = element.doGetName();
- final Label from = components.get(name);
- Label to = null;
-
- if (element instanceof Context) {
- for (final Context context : ((Context) element).getExtends()) {
- final String ctxName = context.doGetName();
- to = components.get(ctxName);
- model.addRelationship(from, to, EXTENDS);
- }
- }
-
- if (element instanceof Machine) {
- for (final Context context : ((Machine) element).getSees()) {
- final String ctxName = context.doGetName();
- to = components.get(ctxName);
- model.addRelationship(from, to, SEES);
- }
- for (final Machine machine : ((Machine) element).getRefines()) {
- final String mName = machine.doGetName();
- to = components.get(mName);
- model.addRelationship(from, to, REFINES);
- }
- }
- }
- return model;
- }
-
- private Label createMachine(Machine machine) {
- EBMachine m = new EBMachine(machine.getName());
- for (Event event : machine.getEvents()) {
- m.addEvent(createEvent(event));
- }
-
- for (Variable variable : machine.getVariables()) {
- m.addVariable(variable.getName());
- }
-
- Variant variant = machine.getVariant();
- if (variant != null)
- m.addVariant(variant.getExpression());
-
- for (Invariant invariant : machine.getInvariants()) {
- m.addInvariant(invariant.getPredicate(), invariant.getName());
- }
-
- return m;
- }
-
- private EBEvent createEvent(Event event) {
-
- EBEvent e = new EBEvent(event.getName());
-
- for (Witness witness : event.getWitnesses()) {
- e.addWitness(witness.getPredicate(), witness.getName());
- }
-
- for (Guard guard : event.getGuards()) {
- e.addGuard(guard.getPredicate(), guard.getName());
- }
- for (Parameter parameter : event.getParameters()) {
- e.addParameter(parameter.getName());
- }
-
- for (String string : event.getRefinesNames()) {
- e.addParameter(string);
- }
- EList<Action> actions = event.getActions();
- for (Action action : actions) {
- e.addAction(action.getAction(), action.getName());
- }
-
- return e;
- }
-
- private Label createContext(Context c) {
- String name = c.getName();
- EBContext context = new EBContext(name);
- EList<Axiom> axioms = c.getAxioms();
- for (Axiom axiom : axioms) {
- context.addAxiom(axiom.getPredicate(), axiom.doGetName());
- }
-
- for (Constant constant : c.getConstants()) {
- context.addConstant(constant.doGetName());
- }
-
- for (CarrierSet carrierSet : c.getSets()) {
- context.addSet(carrierSet.doGetName());
- }
-
- return context;
- }
-
-}
diff --git a/de.prob.ui/src/de/prob/ui/ltl/CounterExampleTab.java b/de.prob.ui/src/de/prob/ui/ltl/CounterExampleTab.java
index f3170291f8de5203287d1e9fc52cafee06d9bd99..038ed22b66e301b266b548f92473c374914099e8 100644
--- a/de.prob.ui/src/de/prob/ui/ltl/CounterExampleTab.java
+++ b/de.prob.ui/src/de/prob/ui/ltl/CounterExampleTab.java
@@ -275,19 +275,15 @@ public class CounterExampleTab {
public void zoomIn() {
final ZoomManager zoomManager = rootEditPart.getZoomManager();
- if (zoomManager != null) {
- if (zoomManager != null && zoomManager.canZoomIn()) {
- zoomManager.setZoom(zoomManager.getNextZoomLevel());
- }
+ if (zoomManager != null && zoomManager.canZoomIn()) {
+ zoomManager.setZoom(zoomManager.getNextZoomLevel());
}
}
public void zoomOut() {
final ZoomManager zoomManager = rootEditPart.getZoomManager();
- if (zoomManager != null) {
- if (zoomManager != null && zoomManager.canZoomOut()) {
- zoomManager.setZoom(zoomManager.getPreviousZoomLevel());
- }
+ if (zoomManager != null && zoomManager.canZoomOut()) {
+ zoomManager.setZoom(zoomManager.getPreviousZoomLevel());
}
}
diff --git a/de.prob.ui/src/de/prob/ui/ltl/LtlCheckingDialog.java b/de.prob.ui/src/de/prob/ui/ltl/LtlCheckingDialog.java
index d8abf60cbb848ab0759118ed6a1639b476b2675e..0860779f1f4078267f51ca61d5bd48cf6cd19233 100644
--- a/de.prob.ui/src/de/prob/ui/ltl/LtlCheckingDialog.java
+++ b/de.prob.ui/src/de/prob/ui/ltl/LtlCheckingDialog.java
@@ -413,7 +413,7 @@ public final class LtlCheckingDialog extends TrayDialog {
Logger.notifyUser("Command exception", e);
} finally {
try {
- reader.close();
+ if (reader != null) reader.close();
} catch (IOException e) {
Logger.notifyUser("Unexpected IO exception", e);
}
diff --git a/de.prob2.feature/feature.xml b/de.prob2.feature/feature.xml
index d316717eac4e0ba62c0180d4b1f92ec26b6d53ba..b2dc420bf9559760fa14aef52939e9f5a917989a 100644
--- a/de.prob2.feature/feature.xml
+++ b/de.prob2.feature/feature.xml
@@ -2,7 +2,7 @@
<feature
id="de.prob2.feature"
label="ProB for Rodin2"
- version="2.3.2.qualifier"
+ version="2.3.3.qualifier"
provider-name="HHU Düsseldorf STUPS Group">
<description url="http://www.stups.uni-duesseldorf.de/ProB">
@@ -228,20 +228,19 @@ litigation.
<import plugin="org.eclipse.ui.ide" version="3.5.0" match="compatible"/>
<import plugin="org.eclipse.ui.views" version="3.5.0" match="compatible"/>
<import plugin="org.eclipse.core.runtime" version="3.5.0" match="compatible"/>
- <import plugin="org.eclipse.jface" version="3.5.0" match="compatible"/>
<import plugin="org.eclipse.core.databinding" version="1.2.0" match="compatible"/>
<import plugin="org.eclipse.jface.databinding" version="1.2.1" match="compatible"/>
<import plugin="org.eclipse.core.databinding.beans" version="1.1.1" match="compatible"/>
<import plugin="org.eclipse.gef" version="3.7.0" match="compatible"/>
- <import plugin="de.prob.core" version="9.2.0" match="equivalent"/>
+ <import plugin="de.prob.core" version="9.3.0" match="equivalent"/>
<import plugin="org.eventb.core" version="2.1.0"/>
<import plugin="org.rodinp.core" version="1.3.1"/>
- <import plugin="de.prob.ui" version="7.2.0" match="equivalent"/>
+ <import plugin="de.prob.ui" version="7.3.0" match="equivalent"/>
<import plugin="org.eclipse.core.resources" version="3.5.0" match="compatible"/>
<import plugin="org.eclipse.core.expressions" version="3.4.101" match="compatible"/>
<import plugin="org.eclipse.gef" version="3.5.0" match="compatible"/>
<import plugin="org.eclipse.ui.navigator" version="3.5.0" match="greaterOrEqual"/>
- <import plugin="de.bmotionstudio.gef.editor" version="5.2.1" match="greaterOrEqual"/>
+ <import plugin="de.bmotionstudio.gef.editor" version="5.4.0" match="equivalent"/>
</requires>
<plugin