diff --git a/de.prob.ui/META-INF/MANIFEST.MF b/de.prob.ui/META-INF/MANIFEST.MF index 0ab9a6cf07669d654268e69b8f68c9b0964f3c49..7d8cf9a52560dee05217e31077bc6a1ae6be47a4 100644 --- a/de.prob.ui/META-INF/MANIFEST.MF +++ b/de.prob.ui/META-INF/MANIFEST.MF @@ -10,9 +10,7 @@ Require-Bundle: org.eclipse.ui;bundle-version="[3.5.0,4.0.0)", de.prob.core;bundle-version="[9.2.0,9.3.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/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; - } - -}