diff --git a/de.prob.core/META-INF/MANIFEST.MF b/de.prob.core/META-INF/MANIFEST.MF
index 2be2f97ea6d9fd8f5d6a85da0a431b035b665c33..bc48a47fa1f59a2e1243b5c7bb20200381853d2a 100644
--- a/de.prob.core/META-INF/MANIFEST.MF
+++ b/de.prob.core/META-INF/MANIFEST.MF
@@ -5,9 +5,7 @@ Bundle-SymbolicName: de.prob.core;singleton:=true
Bundle-Version: 9.2.2.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)",
- org.eventb.emf.core;bundle-version="2.2.4",
- org.eventb.emf.persistence;bundle-version="2.4.0"
+ org.eventb.core;bundle-version="[2.1.0,2.6.0)"
Bundle-ActivationPolicy: lazy
Eclipse-BundleShape: dir
Bundle-Vendor: HHU Düsseldorf STUPS Group
@@ -61,6 +59,7 @@ Export-Package: com.thoughtworks.xstream,
de.be4.ltl.core.parser.node,
de.be4.ltl.core.parser.parser,
de.hhu.stups.sablecc.patch,
+ de.prob.animator.domainobjects,
de.prob.cli,
de.prob.cli.clipatterns,
de.prob.cliparser,
@@ -83,9 +82,10 @@ Export-Package: com.thoughtworks.xstream,
de.prob.eventb.translator,
de.prob.eventb.translator.flow,
de.prob.eventb.translator.internal,
- de.prob.eventb.translator2,
de.prob.exceptions,
de.prob.logging,
+ de.prob.model.eventb,
+ de.prob.model.representation,
de.prob.parser,
de.prob.parserbase,
de.prob.prolog.match,
diff --git a/de.prob.core/src/de/prob/core/Animator.java b/de.prob.core/src/de/prob/core/Animator.java
index dbb83136d6f877ef40e3b41e5d2d530b6466fde5..ad8901b17fd22ca504219767355f4c832dd40b9e 100644
--- a/de.prob.core/src/de/prob/core/Animator.java
+++ b/de.prob.core/src/de/prob/core/Animator.java
@@ -13,7 +13,6 @@ import java.io.IOException;
import java.util.HashMap;
import java.util.Map;
-import org.eclipse.emf.common.command.Command;
import org.osgi.service.prefs.Preferences;
import com.thoughtworks.xstream.XStream;
@@ -347,16 +346,5 @@ public final class Animator {
if (implementation != null) implementation.sendUserInterruptSignal();
}
- public static void serializeModel(Model model) {
- XStream xstream = new XStream(new JettisonMappedXmlDriver());
- String xml = xstream.toXML(model);
- try {
- FileWriter fw = new FileWriter("model.xml");
- final BufferedWriter bw = new BufferedWriter(fw);
- bw.write(xml);
- bw.close();
- } catch (IOException e1) {
- System.out.println("could not create file");
- }
- }
+
}
diff --git a/de.prob.core/src/de/prob/eventb/translator2/EMFEventBTranslator.java b/de.prob.core/src/de/prob/eventb/translator2/EMFEventBTranslator.java
deleted file mode 100644
index 828469e7652b0f8453cf1c43a1404e66ee8cd8c1..0000000000000000000000000000000000000000
--- a/de.prob.core/src/de/prob/eventb/translator2/EMFEventBTranslator.java
+++ /dev/null
@@ -1,63 +0,0 @@
-package de.prob.eventb.translator2;
-
-import java.io.IOException;
-import java.util.ArrayList;
-import java.util.Arrays;
-import java.util.List;
-
-import org.eclipse.emf.common.util.EList;
-import org.eventb.core.IEventBRoot;
-import org.eventb.emf.core.EventBNamedCommentedComponentElement;
-import org.eventb.emf.core.Project;
-import org.eventb.emf.core.context.CarrierSet;
-import org.eventb.emf.core.context.Context;
-import org.eventb.emf.core.machine.Machine;
-import org.eventb.emf.persistence.ProjectResource;
-import org.rodinp.core.IRodinProject;
-
-import de.be4.classicalb.core.parser.node.ADeferredSetSet;
-import de.be4.classicalb.core.parser.node.PSet;
-import de.be4.classicalb.core.parser.node.TIdentifierLiteral;
-import de.prob.prolog.output.IPrologTermOutput;
-
-public class EMFEventBTranslator {
- private final Project project;
-
- public EMFEventBTranslator(IEventBRoot main) {
- IRodinProject rodinProject = main.getRodinProject();
- ProjectResource resource = new ProjectResource(rodinProject);
- try {
- resource.load(null);
- } catch (IOException e) {
- e.printStackTrace();
- }
- project = (Project) resource.getContents().get(0);
- }
-
- public void print(IPrologTermOutput pto) {
- for (EventBNamedCommentedComponentElement e : project.getComponents()) {
- if (e instanceof Context) {
- printContext(pto, (Context) e);
- } else {
- printMachine(pto, (Machine) e);
- }
- }
- }
-
- public void printContext(IPrologTermOutput pto, Context c) {
- EList<CarrierSet> sets = c.getSets();
- final List<PSet> setList = new ArrayList<PSet>(sets.size());
- for (CarrierSet s : sets) {
- final ADeferredSetSet deferredSet = new ADeferredSetSet(
- Arrays.asList(new TIdentifierLiteral[] { new TIdentifierLiteral(
- s.getName()) }));
- setList.add(deferredSet);
- }
-
- }
-
- public void printMachine(IPrologTermOutput pto, Machine m) {
-
- }
-
-}
diff --git a/de.prob.core/src/de/prob/model/eventb/Action.java b/de.prob.core/src/de/prob/model/eventb/Action.java
new file mode 100644
index 0000000000000000000000000000000000000000..6eb7c43c99c049fc6328e4e4645e712c2b5efcbe
--- /dev/null
+++ b/de.prob.core/src/de/prob/model/eventb/Action.java
@@ -0,0 +1,36 @@
+package de.prob.model.eventb;
+
+import java.util.Collections;
+import java.util.List;
+
+import de.prob.model.representation.IEntity;
+
+public class Action implements IEntity {
+
+ private final String code;
+ private final String name;
+
+ public Action(String code, String name) {
+ this.code = code;
+ this.name = name;
+ }
+
+ @Override
+ public List<IEntity> getChildren() {
+ return Collections.emptyList();
+ }
+
+ @Override
+ public boolean hasChildren() {
+ return false;
+ }
+
+ public String getCode() {
+ return code;
+ }
+
+ public String getName() {
+ return name;
+ }
+
+}
diff --git a/de.prob.core/src/de/prob/model/eventb/EBContext.java b/de.prob.core/src/de/prob/model/eventb/EBContext.java
index 0d6a1ae9605f451412f5f20049db58e3c1d20461..9cb041b0e403f340bfd0840b877eb3dc2092a71a 100644
--- a/de.prob.core/src/de/prob/model/eventb/EBContext.java
+++ b/de.prob.core/src/de/prob/model/eventb/EBContext.java
@@ -26,8 +26,8 @@ public class EBContext extends Label {
constants.addChild(new EventB(constant));
}
- public void addAxiom(final String axiom) {
- axioms.addChild(new EventB(axiom));
+ public void addAxiom(final String axiom, String aname) {
+ axioms.addChild(new EventB(axiom,aname));
}
}
diff --git a/de.prob.core/src/de/prob/model/eventb/EBEvent.java b/de.prob.core/src/de/prob/model/eventb/EBEvent.java
index 37899622d61911371d719f2019505cece1ad4252..12139186dd80a9ee2e47659b24156232fe98effb 100644
--- a/de.prob.core/src/de/prob/model/eventb/EBEvent.java
+++ b/de.prob.core/src/de/prob/model/eventb/EBEvent.java
@@ -16,7 +16,7 @@ public class EBEvent extends Label {
public EBEvent(final String name) {
super(name);
children.addAll(Arrays.asList(new IEntity[] { refines, parameters,
- guards, witnesses, actions }));
+ guards }));
}
@Override
@@ -32,15 +32,15 @@ public class EBEvent extends Label {
parameters.addChild(new EventB(parameter));
}
- public void addGuard(final String guard) {
- guards.addChild(new EventB(guard));
+ public void addGuard(final String guard, String gname) {
+ guards.addChild(new EventB(guard,gname));
}
- public void addWitness(final String witness) {
- witnesses.addChild(new EventB(witness));
+ public void addWitness(final String witness,String wname) {
+ witnesses.addChild(new EventB(witness,wname));
}
- public void addAction(final String action) {
- actions.addChild(new Label(action));
+ public void addAction(final String action, String aname) {
+ actions.addChild(new Action(action, aname));
}
}
diff --git a/de.prob.core/src/de/prob/model/eventb/EBMachine.java b/de.prob.core/src/de/prob/model/eventb/EBMachine.java
index 03c24021c3b95123a9b800c79f6a99c4de4200bb..08bbcfd6dee64c10e0d8cf52a8538755b74eb9b8 100644
--- a/de.prob.core/src/de/prob/model/eventb/EBMachine.java
+++ b/de.prob.core/src/de/prob/model/eventb/EBMachine.java
@@ -22,8 +22,8 @@ public class EBMachine extends Label {
variables.addChild(new EventB(variable));
}
- public void addInvariant(final String invariant) {
- invariants.addChild(new EventB(invariant));
+ public void addInvariant(final String invariant, String iname) {
+ invariants.addChild(new EventB(invariant, iname));
}
public void addVariant(final String variant) {
diff --git a/de.prob.core/src/de/prob/model/eventb/EventB.java b/de.prob.core/src/de/prob/model/eventb/EventB.java
index 5c6c3b9d1353e1fa19d67e9c81373579c988dbd8..c3f7ae108bcbbab9ba1e927b5be15d23c333b7e1 100644
--- a/de.prob.core/src/de/prob/model/eventb/EventB.java
+++ b/de.prob.core/src/de/prob/model/eventb/EventB.java
@@ -32,8 +32,15 @@ public class EventB implements IEvalElement, IEntity {
private String kind;
private Node ast = null;
- public EventB(final String code) {
+ private final String name;
+
+ public EventB(final String code, String name) {
this.code = code;
+ this.name = name;
+ }
+
+ public EventB(String code) {
+ this(code, "");
}
private void ensureParsed() {
@@ -81,7 +88,7 @@ public class EventB implements IEvalElement, IEntity {
}
StringBuilder sb = new StringBuilder();
for (String string : msgs) {
- sb.append(string+"\n");
+ sb.append(string + "\n");
}
final String error = sb.toString();
throw new RuntimeException("Cannot parse " + code + ":\n " + error); // FIXME
@@ -118,4 +125,8 @@ public class EventB implements IEvalElement, IEntity {
return false;
}
+ public String getName() {
+ return name;
+ }
+
}
diff --git a/de.prob.core/src/de/prob/model/eventb/Model.java b/de.prob.core/src/de/prob/model/eventb/Model.java
index 3d31386cdb10cfa5fef9076a0d55db4f4b94d4be..f835034bddb9f8f27e5ba758f2a4f20e58f45013 100644
--- a/de.prob.core/src/de/prob/model/eventb/Model.java
+++ b/de.prob.core/src/de/prob/model/eventb/Model.java
@@ -4,12 +4,19 @@ import java.util.ArrayList;
import java.util.List;
import de.prob.model.representation.Label;
+import de.prob.model.representation.RefType.ERefType;
public class Model {
- public List<Relationship> relationships = new ArrayList<Relationship>();
+ public final String serialization_version = "1";
+ public final String name;
+ public final List<Relationship> relationships = new ArrayList<Relationship>();
- public void addRelationship(final Label from, final Label to) {
- relationships.add(new Relationship(from, to));
+ public Model(String name) {
+ this.name = name;
+ }
+
+ public void addRelationship(final Label from, final Label to, ERefType type) {
+ relationships.add(new Relationship(from, to,type));
}
}
diff --git a/de.prob.core/src/de/prob/model/eventb/Relationship.java b/de.prob.core/src/de/prob/model/eventb/Relationship.java
index d6b3f130aee5248d1ae72afb65c2d3250c9fef15..09b5a098ce8b29279fd1077257ae02726c28e566 100644
--- a/de.prob.core/src/de/prob/model/eventb/Relationship.java
+++ b/de.prob.core/src/de/prob/model/eventb/Relationship.java
@@ -1,13 +1,17 @@
package de.prob.model.eventb;
import de.prob.model.representation.Label;
+import de.prob.model.representation.RefType.ERefType;
public class Relationship {
+
public final Label from;
public final Label to;
-
- public Relationship(Label from,Label to) {
+ public final ERefType type;
+
+ public Relationship(Label from, Label to, ERefType type) {
this.from = from;
this.to = to;
+ this.type = type;
}
}
diff --git a/de.prob.core/src/de/prob/model/representation/RefType.java b/de.prob.core/src/de/prob/model/representation/RefType.java
new file mode 100644
index 0000000000000000000000000000000000000000..192a8a4aafe21eb232ada4f0045f5b0c4e6e2b1d
--- /dev/null
+++ b/de.prob.core/src/de/prob/model/representation/RefType.java
@@ -0,0 +1,28 @@
+package de.prob.model.representation;
+
+public class RefType {
+ private final ERefType relationship;
+
+ /*
+ * RefType is used for both ClassicalBModels and EventBModels
+ *
+ * ClassicalB: SEES, USES, REFINES, INCLUDES, IMPORTS EventB: SEES, REFINES,
+ * EXTENDS
+ */
+ public enum ERefType {
+ SEES, USES, REFINES, INCLUDES, IMPORTS, EXTENDS
+ }
+
+ public RefType(final ERefType relationship) {
+ this.relationship = relationship;
+ }
+
+ @Override
+ public String toString() {
+ return relationship.toString();
+ }
+
+ public ERefType getRelationship() {
+ return relationship;
+ }
+}
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 79af767fe8c25b3e2ebca407f41d4d0d67f11c77..cbb940a1eae628b8e71031a4aee296f03610be73 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,12 @@
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.StringWriter;
import java.io.Writer;
-import java.util.Collections;
-import java.util.HashMap;
-import java.util.Map;
+import java.util.zip.GZIPOutputStream;
import org.apache.commons.codec.binary.Base64;
import org.eclipse.core.commands.AbstractHandler;
@@ -17,8 +15,6 @@ import org.eclipse.core.commands.ExecutionException;
import org.eclipse.core.commands.IHandler;
import org.eclipse.core.runtime.Platform;
import org.eclipse.core.runtime.preferences.InstanceScope;
-import org.eclipse.emf.ecore.xmi.XMLResource;
-import org.eclipse.emf.ecore.xmi.impl.XMLResourceImpl;
import org.eclipse.jface.dialogs.MessageDialog;
import org.eclipse.jface.viewers.ISelection;
import org.eclipse.jface.viewers.IStructuredSelection;
@@ -34,9 +30,12 @@ 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 {
@@ -117,8 +116,8 @@ public class ExportNewCoreHandler extends AbstractHandler implements IHandler {
TranslatorFactory.translate(root, new PrintWriter(fw));
fw.append('\n');
- fw.append("emf_model('" + root.getComponentName() + "',\""
- + serialize(project) + "\").");
+ fw.append("eclipse_model('" + root.getComponentName() + "',\""
+ + serialize(project, root.getComponentName()) + "\").");
} catch (TranslationFailedException e) {
e.notifyUserOnce();
@@ -135,22 +134,24 @@ public class ExportNewCoreHandler extends AbstractHandler implements IHandler {
}
}
- private static String serialize(Project project) {
-
- StringWriter sw = new StringWriter();
- Map<Object, Object> options = new HashMap<Object, Object>();
- options.put(XMLResource.OPTION_ROOT_OBJECTS,
- Collections.singletonList(project));
- options.put(XMLResource.OPTION_FORMATTED, false);
- XMLResourceImpl ri = new XMLResourceImpl();
+ 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 {
- ri.save(sw, options);
- } catch (IOException e1) {
- e1.printStackTrace();
+ gzip = new GZIPOutputStream(out);
+ gzip.write(xml.getBytes());
+ gzip.close();
+ bytes = out.toByteArray();
+ } catch (IOException e) {
+ bytes = xml.getBytes();
}
-
- String xml = Base64.encodeBase64String(sw.toString().getBytes());
- return xml;
+ return Base64.encodeBase64String(bytes);
}
private static boolean isSafeToWrite(final String filename) {
diff --git a/de.prob.ui/src/de/prob/ui/eventb/NewCoreModelTranslation.java b/de.prob.ui/src/de/prob/ui/eventb/NewCoreModelTranslation.java
new file mode 100644
index 0000000000000000000000000000000000000000..a95105e2548f3bbf6a54001a7a4bc17eb6768939
--- /dev/null
+++ b/de.prob.ui/src/de/prob/ui/eventb/NewCoreModelTranslation.java
@@ -0,0 +1,154 @@
+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;
+ }
+
+}