diff --git a/build.gradle b/build.gradle
index 205642b5ddc596bef7f8ca1338034bc4c8114a79..33b77a6710bc05ca7ef1d25d8b8e5fa151413695 100644
--- a/build.gradle
+++ b/build.gradle
@@ -1,5 +1,5 @@
// to trigger a full tycho build please use 'gradle deleteFromClassPath completeInstall'
-
+import org.apache.tools.ant.taskdefs.condition.Os
project.ext{
@@ -101,6 +101,53 @@ task downloadCli << {
}
+
+task downloadCli2 ( type: Exec ) {
+
+ def dir = workspacePath+'de.prob.core/prob/'
+ delete file(dir)
+ new File(dir).mkdirs()
+
+ ['leopard64':'macos','linux':'linux','linux64':'linux64','win32':'windows'].each {
+ def n = it.getKey()
+
+ def targetdir = dir+it.getValue()
+ def targetzip = dir+"probcli_${n}.zip"
+ def url = "http://nightly.cobra.cs.uni-duesseldorf.de/cli/probcli_${n}.zip"
+ download(url,targetzip)
+ FileTree zip = zipTree(targetzip)
+ copy {
+ from zip
+ into targetdir
+ }
+ delete file(targetzip)
+ }
+
+ def targetdir = dir+"windows/"
+ def targetzip = targetdir+"windowslib.zip"
+ download("http://nightly.cobra.cs.uni-duesseldorf.de/cli/windowslib.zip",targetzip)
+ FileTree zip = zipTree(targetzip)
+ copy {
+ from zip
+ into targetdir
+ }
+ delete file(targetzip)
+
+ ['leopard64':'macos','linux32':'linux','linux64':'linux64'].each {
+
+ def n = it.getKey()
+ targetdir = dir+it.getValue()
+
+ download( "http://nightly.cobra.cs.uni-duesseldorf.de/cspm/cspm-"+n, targetdir+"/cspm" )
+ }
+ commandLine 'chmod', 'a+x', dir+'linux'+'/cspm', dir+'linux64'+'/cspm', dir+'macos'+'/cspm'
+ //commandLine 'chmod', 'a+x', dir+'*'+'/cspm'
+
+ download( "http://nightly.cobra.cs.uni-duesseldorf.de/cspm/cspm-windows", dir+"windows"+"/cspm.exe" )
+}
+
+
+
completeInstall.dependsOn downloadCli
completeInstall.dependsOn subprojects.setClassPath
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 9ea99009688c58a066ad0add611d91b1e6a429a6..ad5b33afb304accdbaa9f275db0e8a47d91b6707 100644
--- a/de.prob.core/src/de/prob/eventb/translator/ContextTranslator.java
+++ b/de.prob.core/src/de/prob/eventb/translator/ContextTranslator.java
@@ -13,11 +13,10 @@ import java.util.LinkedList;
import java.util.List;
import java.util.Map;
-import org.apache.commons.lang.StringUtils;
import org.eclipse.core.runtime.Assert;
-import org.eventb.core.IAxiom;
import org.eventb.core.IContextRoot;
import org.eventb.core.IExtendsContext;
+import org.eventb.core.ILabeledElement;
import org.eventb.core.IPOSequent;
import org.eventb.core.IPOSource;
import org.eventb.core.IPSRoot;
@@ -54,8 +53,9 @@ import de.be4.classicalb.core.parser.node.PSet;
import de.be4.classicalb.core.parser.node.TIdentifierLiteral;
import de.hhu.stups.sablecc.patch.SourcePosition;
import de.prob.core.translator.TranslationFailedException;
-import de.prob.eventb.translator.internal.DischargedProof;
-import de.prob.logging.Logger;
+import de.prob.eventb.translator.internal.EProofStatus;
+import de.prob.eventb.translator.internal.ProofObligation;
+import de.prob.eventb.translator.internal.SequentSource;
public final class ContextTranslator extends AbstractComponentTranslator {
@@ -63,16 +63,13 @@ public final class ContextTranslator extends AbstractComponentTranslator {
private final ISCContext context;
private final AEventBContextParseUnit model = new AEventBContextParseUnit();
private final Map<String, ISCContext> depContext = new HashMap<String, ISCContext>();
- private final List<DischargedProof> proofs = new ArrayList<DischargedProof>();
+ 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 {
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: ";
@@ -95,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;
@@ -136,10 +124,10 @@ public final class ContextTranslator extends AbstractComponentTranslator {
}
- private void collectProofInfo(ISCContextRoot context_root)
+ private void collectProofInfo(ISCContextRoot origin)
throws RodinDBException {
- IPSRoot proofStatus = context_root.getPSRoot();
+ IPSRoot proofStatus = origin.getPSRoot();
IPSStatus[] statuses = proofStatus.getStatuses();
List<String> bugs = new LinkedList<String>();
@@ -147,34 +135,37 @@ public final class ContextTranslator extends AbstractComponentTranslator {
for (IPSStatus status : statuses) {
final int confidence = status.getConfidence();
boolean broken = status.isBroken();
- if (!broken && confidence == IConfidence.DISCHARGED_MAX) {
- IPOSequent sequent = status.getPOSequent();
- IPOSource[] sources = sequent.getSources();
-
- for (IPOSource source : sources) {
-
- IRodinElement srcElement = source.getSource();
- if (!srcElement.exists()) {
- bugs.add(status.getElementName());
- break;
- }
-
- if (srcElement instanceof IAxiom) {
- IAxiom tmp = (IAxiom) srcElement;
- if (((IContextRoot) tmp.getParent())
- .equals(context_root.getContextRoot())) {
- proofs.add(new DischargedProof(context_root, tmp,
- null));
- }
- }
+
+ EProofStatus pstatus = EProofStatus.UNPROVEN;
+
+ if (!broken && confidence == IConfidence.REVIEWED_MAX)
+ pstatus = EProofStatus.REVIEWED;
+ if (!broken && confidence == IConfidence.DISCHARGED_MAX)
+ pstatus = EProofStatus.PROVEN;
+
+ IPOSequent sequent = status.getPOSequent();
+ IPOSource[] sources = sequent.getSources();
+
+ String name = sequent.getDescription();
+
+ ArrayList<SequentSource> s = new ArrayList<SequentSource>(
+ sources.length);
+ for (IPOSource source : sources) {
+
+ IRodinElement srcElement = source.getSource();
+ if (!srcElement.exists()
+ || !(srcElement instanceof ILabeledElement)) {
+ bugs.add(status.getElementName());
+ break;
}
- }
- }
- if (!bugs.isEmpty()) {
- String message = "Translation incomplete due to a Bug in Rodin. This does not affect correctness of the Animation/Model Checking but can decrease its performance. Skipped discharged information about: "
- + StringUtils.join(bugs, ",");
- Logger.notifyUser(message);
+ ILabeledElement le = (ILabeledElement) srcElement;
+
+ s.add(new SequentSource(srcElement.getElementType(), le
+ .getLabel()));
+
+ }
+ proofs.add(new ProofObligation(origin, s, name, pstatus));
}
}
@@ -319,6 +310,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);
@@ -330,7 +323,7 @@ public final class ContextTranslator extends AbstractComponentTranslator {
return list;
}
- public List<DischargedProof> getProofs() {
+ public List<ProofObligation> getProofs() {
return proofs;
}
diff --git a/de.prob.core/src/de/prob/eventb/translator/internal/EProofStatus.java b/de.prob.core/src/de/prob/eventb/translator/internal/EProofStatus.java
new file mode 100644
index 0000000000000000000000000000000000000000..160bf968ce3bd637dea4af99e8b5eea6ee72fd8f
--- /dev/null
+++ b/de.prob.core/src/de/prob/eventb/translator/internal/EProofStatus.java
@@ -0,0 +1,15 @@
+package de.prob.eventb.translator.internal;
+
+public enum EProofStatus {
+ UNPROVEN("false"), PROVEN("true"), REVIEWED("reviewed");
+ private final String text;
+
+ private EProofStatus(String text) {
+ this.text = text;
+ }
+
+ @Override
+ public String toString() {
+ return text;
+ }
+}
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 43ea5792f26eee7de07938f106ef26696642a2c8..ed82d8a8e8ee13b70b2e191805fa67b5168c306b 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
@@ -11,13 +11,11 @@ import java.util.Collection;
import java.util.Map;
import org.eclipse.core.runtime.Assert;
-import org.eventb.core.IEvent;
import org.eventb.core.IEventBProject;
import org.eventb.core.IEventBRoot;
import org.eventb.core.ISCInternalContext;
import org.eventb.core.ISCMachineRoot;
import org.rodinp.core.IInternalElement;
-import org.rodinp.core.RodinDBException;
import de.be4.classicalb.core.parser.analysis.prolog.ASTProlog;
import de.be4.classicalb.core.parser.node.AEventBContextParseUnit;
@@ -27,16 +25,13 @@ 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 {
protected final IEventBProject project;
- private final String name;
protected EventBTranslator(final IEventBRoot root) {
this.project = root.getEventBProject();
- this.name = root.getComponentName();
}
// another constructor to cater for ISCInternalContext (which is not a root
@@ -44,7 +39,6 @@ public abstract class EventBTranslator implements ITranslator {
protected EventBTranslator(final ISCInternalContext ctx) {
Assert.isTrue(ctx.getRoot() instanceof ISCMachineRoot);
this.project = ((ISCMachineRoot) ctx.getRoot()).getEventBProject();
- this.name = ctx.getComponentName();
}
private LabelPositionPrinter createPrinter(
@@ -89,7 +83,7 @@ public abstract class EventBTranslator implements ITranslator {
Collection<ContextTranslator> contextTranslators,
final IPrologTermOutput pout) throws TranslationFailedException {
- ArrayList<DischargedProof> list = new ArrayList<DischargedProof>();
+ ArrayList<ProofObligation> list = new ArrayList<ProofObligation>();
for (ContextTranslator contextTranslator : contextTranslators) {
list.addAll(contextTranslator.getProofs());
@@ -98,20 +92,19 @@ public abstract class EventBTranslator implements ITranslator {
list.addAll(modelTranslator.getProofs());
}
- for (DischargedProof proof : list) {
- pout.openTerm("discharged");
- pout.printAtom(proof.machine.getRodinFile().getBareName());
- try {
- IEvent event = proof.event;
- final String elementName = proof.predicate;
- if (event != null)
- pout.printAtom(event.getLabel());
- pout.printAtom(elementName);
- } catch (RodinDBException e) {
- final String details = "Translation error while getting information about discharged proof obligations";
- throw new TranslationFailedException(name, details);
+ for (ProofObligation proof : list) {
+ pout.openTerm("po");
+ pout.printAtom(proof.origin.getRodinFile().getBareName());
+ pout.printAtom(proof.kind);
+ pout.openList();
+ for (SequentSource source : proof.sources) {
+ pout.openTerm(source.type);
+ pout.printAtom(source.label);
+ pout.closeTerm();
}
+ pout.closeList();
+ pout.printAtom(proof.discharged.toString());
pout.closeTerm();
}
@@ -142,6 +135,9 @@ public abstract class EventBTranslator implements ITranslator {
printModels(refinementChainTranslators, pout, prolog);
printContexts(contextTranslators, pout, prolog);
pout.openList();
+ pout.openTerm("exporter_version");
+ pout.printNumber(2);
+ pout.closeTerm();
printProofInformation(refinementChainTranslators, contextTranslators,
pout);
// FIXME THEORY-PLUGIN re-enable when the theory plugin was released
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 d9fdf6fbb66e8880d7577915fe8fc80d36a17c87..ead67da6ba447b4f830418088f54eb34069a3bf7 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
@@ -15,8 +15,7 @@ import java.util.List;
import org.apache.commons.lang.StringUtils;
import org.eventb.core.IConvergenceElement.Convergence;
-import org.eventb.core.IEvent;
-import org.eventb.core.IInvariant;
+import org.eventb.core.ILabeledElement;
import org.eventb.core.IMachineRoot;
import org.eventb.core.IPOSequent;
import org.eventb.core.IPOSource;
@@ -40,6 +39,7 @@ import org.eventb.core.ast.FormulaFactory;
import org.eventb.core.ast.ITypeEnvironment;
import org.eventb.core.ast.Predicate;
import org.eventb.core.seqprover.IConfidence;
+import org.rodinp.core.IElementType;
import org.rodinp.core.IRodinElement;
import org.rodinp.core.IRodinFile;
import org.rodinp.core.RodinDBException;
@@ -80,7 +80,7 @@ public class ModelTranslator extends AbstractComponentTranslator {
private final FormulaFactory ff;
private final ITypeEnvironment te;
private final IMachineRoot origin;
- private final List<DischargedProof> proofs = new ArrayList<DischargedProof>();
+ private final List<ProofObligation> proofs = new ArrayList<ProofObligation>();
// private final List<String> depContext = new ArrayList<String>();
// Confined in the thread calling the factory method
@@ -113,7 +113,7 @@ public class ModelTranslator extends AbstractComponentTranslator {
return modelTranslator;
}
- public List<DischargedProof> getProofs() {
+ public List<ProofObligation> getProofs() {
return Collections.unmodifiableList(proofs);
}
@@ -176,41 +176,37 @@ public class ModelTranslator extends AbstractComponentTranslator {
for (IPSStatus status : statuses) {
final int confidence = status.getConfidence();
boolean broken = status.isBroken();
- if (!broken && confidence == IConfidence.DISCHARGED_MAX) {
- IPOSequent sequent = status.getPOSequent();
- IPOSource[] sources = sequent.getSources();
-
- IEvent evt = null;
- IInvariant inv = null;
-
- for (IPOSource source : sources) {
-
- IRodinElement srcElement = source.getSource();
- if (!srcElement.exists()) {
- bugs.add(status.getElementName());
- break;
- }
-
- if (srcElement instanceof IEvent) {
- IEvent tmp = (IEvent) srcElement;
- if (((IMachineRoot) tmp.getParent()).equals(origin)) {
- evt = tmp;
- }
- }
- if (srcElement instanceof IInvariant) {
- IInvariant tmp = (IInvariant) srcElement;
- if (((IMachineRoot) tmp.getParent()).equals(origin)) {
- inv = tmp;
- }
- }
- }
- if (evt != null && inv != null) {
- proofs.add(new DischargedProof(origin, inv, evt));
- }
- if (evt == null && inv != null && inv.isTheorem()) {
- proofs.add(new DischargedProof(origin, inv, evt));
+
+ EProofStatus pstatus = EProofStatus.UNPROVEN;
+
+ if (!broken && (confidence > IConfidence.PENDING && confidence <= IConfidence.REVIEWED_MAX))
+ pstatus = EProofStatus.REVIEWED;
+ if (!broken && confidence == IConfidence.DISCHARGED_MAX)
+ pstatus = EProofStatus.PROVEN;
+
+ IPOSequent sequent = status.getPOSequent();
+ IPOSource[] sources = sequent.getSources();
+
+ String name = sequent.getDescription();
+
+ ArrayList<SequentSource> s = new ArrayList<SequentSource>(
+ sources.length);
+ for (IPOSource source : sources) {
+
+ IRodinElement srcElement = source.getSource();
+ if (!srcElement.exists()
+ || !(srcElement instanceof ILabeledElement)) {
+ bugs.add(status.getElementName());
+ break;
}
+
+ ILabeledElement le = (ILabeledElement) srcElement;
+ IElementType<? extends IRodinElement> type = srcElement
+ .getElementType();
+ s.add(new SequentSource(type, le.getLabel()));
+
}
+ proofs.add(new ProofObligation(origin, s, name, pstatus));
}
if (!bugs.isEmpty()) {
diff --git a/de.prob.core/src/de/prob/eventb/translator/internal/ProofObligation.java b/de.prob.core/src/de/prob/eventb/translator/internal/ProofObligation.java
new file mode 100644
index 0000000000000000000000000000000000000000..39b10069a3de8357e334a8f218384ae907ea96ae
--- /dev/null
+++ b/de.prob.core/src/de/prob/eventb/translator/internal/ProofObligation.java
@@ -0,0 +1,22 @@
+package de.prob.eventb.translator.internal;
+
+import java.util.ArrayList;
+
+import org.eventb.core.IEventBRoot;
+
+public class ProofObligation {
+
+ public final IEventBRoot origin;
+ public final ArrayList<SequentSource> sources;
+ public final String kind;
+ public final EProofStatus discharged;
+
+ public ProofObligation(IEventBRoot origin, ArrayList<SequentSource> s,
+ String name, EProofStatus pstatus) {
+ this.origin = origin;
+ this.sources = s;
+ this.kind = name;
+ this.discharged = pstatus;
+ }
+
+}
diff --git a/de.prob.core/src/de/prob/eventb/translator/internal/SequentSource.java b/de.prob.core/src/de/prob/eventb/translator/internal/SequentSource.java
new file mode 100644
index 0000000000000000000000000000000000000000..5575130fc9509990ab94e0aabc665cbceccc5740
--- /dev/null
+++ b/de.prob.core/src/de/prob/eventb/translator/internal/SequentSource.java
@@ -0,0 +1,17 @@
+package de.prob.eventb.translator.internal;
+
+import org.rodinp.core.IElementType;
+import org.rodinp.core.IRodinElement;
+
+public class SequentSource {
+
+ public final String type;
+ public final String label;
+
+ public SequentSource(IElementType<? extends IRodinElement> type,
+ String label) {
+ this.type = type.toString().replaceAll("org.eventb.core.", "");
+ this.label = label;
+ }
+
+}