diff --git a/de.prob.core/.classpath b/de.prob.core/.classpath
index bb1ae0592818db067d6599e1a8f034a51349b613..b5efa8550ac9c4daefb09ca828889085b018d941 100644
--- a/de.prob.core/.classpath
+++ b/de.prob.core/.classpath
@@ -4,20 +4,20 @@
<classpathentry exported="true" kind="lib" path="lib/dependencies/xmlpull-1.1.3.1.jar"/>
<classpathentry exported="true" kind="lib" path="lib/dependencies/xpp3_min-1.1.4c.jar"/>
<classpathentry exported="true" kind="lib" path="lib/dependencies/xstream-1.4.3.jar"/>
- <classpathentry exported="true" kind="lib" path="lib/dependencies/answerparser-2.4.8-SNAPSHOT.jar"/>
- <classpathentry exported="true" kind="lib" path="lib/dependencies/bparser-2.4.8-SNAPSHOT.jar"/>
- <classpathentry exported="true" kind="lib" path="lib/dependencies/cliparser-2.4.8-SNAPSHOT.jar"/>
<classpathentry exported="true" kind="lib" path="lib/dependencies/commons-lang-2.6.jar"/>
<classpathentry exported="true" kind="lib" path="lib/dependencies/jgrapht-0.8.3.jar"/>
<classpathentry exported="true" kind="lib" path="lib/dependencies/jsr305-1.3.9.jar"/>
- <classpathentry exported="true" kind="lib" path="lib/dependencies/ltlparser-2.4.8-SNAPSHOT.jar"/>
- <classpathentry exported="true" kind="lib" path="lib/dependencies/parserbase-2.4.8-SNAPSHOT.jar"/>
- <classpathentry exported="true" kind="lib" path="lib/dependencies/prologlib-2.4.8-SNAPSHOT.jar"/>
- <classpathentry exported="true" kind="lib" path="lib/dependencies/unicode-2.4.8-SNAPSHOT.jar"/>
<classpathentry kind="con" path="org.eclipse.jdt.launching.JRE_CONTAINER/org.eclipse.jdt.internal.debug.ui.launcher.StandardVMType/JavaSE-1.6"/>
<classpathentry kind="con" path="org.eclipse.pde.core.requiredPlugins"/>
<classpathentry kind="src" path="src"/>
<classpathentry kind="src" path="test"/>
<classpathentry kind="con" path="org.eclipse.jdt.junit.JUNIT_CONTAINER/4"/>
+ <classpathentry exported="true" kind="lib" path="lib/dependencies/parserbase-2.4.12-SNAPSHOT.jar"/>
+ <classpathentry exported="true" kind="lib" path="lib/dependencies/answerparser-2.4.12-SNAPSHOT.jar"/>
+ <classpathentry exported="true" kind="lib" path="lib/dependencies/cliparser-2.4.12-SNAPSHOT.jar"/>
+ <classpathentry exported="true" kind="lib" path="lib/dependencies/prologlib-2.4.12-SNAPSHOT.jar"/>
+ <classpathentry exported="true" kind="lib" path="lib/dependencies/bparser-2.4.12-SNAPSHOT.jar"/>
+ <classpathentry exported="true" kind="lib" path="lib/dependencies/unicode-2.4.12-SNAPSHOT.jar"/>
+ <classpathentry exported="true" kind="lib" path="lib/dependencies/ltlparser-2.4.12-SNAPSHOT.jar"/>
<classpathentry kind="output" path="bin"/>
</classpath>
diff --git a/de.prob.core/META-INF/MANIFEST.MF b/de.prob.core/META-INF/MANIFEST.MF
index b68f1d0afc2a00b39086b6c5c55bff7f6296a9c2..f294dd34c178468f36b26bcd9d7c232658361103 100644
--- a/de.prob.core/META-INF/MANIFEST.MF
+++ b/de.prob.core/META-INF/MANIFEST.MF
@@ -70,7 +70,6 @@ Export-Package: com.thoughtworks.xstream,
de.prob.core.domainobjects,
de.prob.core.domainobjects.eval,
de.prob.core.domainobjects.ltl,
- de.prob.core.domainobjects.ltl.unittests,
de.prob.core.internal,
de.prob.core.langdep,
de.prob.core.prolog,
@@ -119,11 +118,11 @@ Bundle-ClassPath: .,
lib/dependencies/bparser-2.4.12-SNAPSHOT.jar,
lib/dependencies/cliparser-2.4.12-SNAPSHOT.jar,
lib/dependencies/commons-codec-1.6.jar,
+ lib/dependencies/parserbase-2.4.12-SNAPSHOT.jar,
lib/dependencies/commons-lang-2.6.jar,
lib/dependencies/jgrapht-0.8.3.jar,
lib/dependencies/jsr305-1.3.9.jar,
lib/dependencies/ltlparser-2.4.12-SNAPSHOT.jar,
- lib/dependencies/parserbase-2.4.12-SNAPSHOT.jar,
lib/dependencies/prologlib-2.4.12-SNAPSHOT.jar,
lib/dependencies/unicode-2.4.12-SNAPSHOT.jar,
lib/dependencies/xmlpull-1.1.3.1.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 7e52913c1a13ed56d2a45e4ff132a287b4428fcf..27c3e2e805fe6155ea2338f7778ee5af35976d21 100644
--- a/de.prob.core/src/de/prob/eventb/translator/ContextTranslator.java
+++ b/de.prob.core/src/de/prob/eventb/translator/ContextTranslator.java
@@ -64,8 +64,6 @@ public final class ContextTranslator extends AbstractComponentTranslator {
private final Map<String, ISCContext> depContext = new HashMap<String, ISCContext>();
private final List<ProofObligation> proofs = new ArrayList<ProofObligation>();
private final List<ClassifiedPragma> proofspragmas = new ArrayList<ClassifiedPragma>();
- private final FormulaFactory ff;
- private ITypeEnvironment te;
public static ContextTranslator create(final ISCContext context)
throws TranslationFailedException {
@@ -94,21 +92,12 @@ public final class ContextTranslator extends AbstractComponentTranslator {
private ContextTranslator(final ISCContext context)
throws TranslationFailedException {
this.context = context;
- 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 {
if (context instanceof ISCContextRoot) {
ISCContextRoot context_root = (ISCContextRoot) context;
Assert.isTrue(context_root.getRodinFile().isConsistent());
- te = context_root.getTypeEnvironment(ff);
} else if (context instanceof ISCInternalContext) {
ISCInternalContext context_internal = (ISCInternalContext) context;
@@ -155,7 +144,8 @@ public final class ContextTranslator extends AbstractComponentTranslator {
String name = sequent.getDescription();
- ArrayList<SequentSource> s = new ArrayList<SequentSource>(sources.length);
+ ArrayList<SequentSource> s = new ArrayList<SequentSource>(
+ sources.length);
for (IPOSource source : sources) {
IRodinElement srcElement = source.getSource();
@@ -167,7 +157,8 @@ public final class ContextTranslator extends AbstractComponentTranslator {
ILabeledElement le = (ILabeledElement) srcElement;
- s.add(new SequentSource(srcElement.getElementType(), le.getLabel()));
+ s.add(new SequentSource(srcElement.getElementType(), le
+ .getLabel()));
}
proofs.add(new ProofObligation(origin, s, name, discharged));
@@ -315,6 +306,8 @@ public final class ContextTranslator extends AbstractComponentTranslator {
}
final PredicateVisitor visitor = new PredicateVisitor(
new LinkedList<String>());
+ final FormulaFactory ff = FormulaFactory.getDefault();
+ final ITypeEnvironment te = ff.makeTypeEnvironment();
element.getPredicate(ff, te).accept(visitor);
final PPredicate predicate = visitor.getPredicate();
list.add(predicate);