Merge branch 'develop' of github.com:bendisposto/prob into develop

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,

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");
-		}
-	}
+
 }

de.prob.core/src/de/prob/eventb/translator2/EMFEventBTranslator.java

-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) {
-
-	}
-
-}

de.prob.core/src/de/prob/model/eventb/Action.java

+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;
+	}
+
+}

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));
 	}
 
 }

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));
 	}
 }

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) {

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() {
@@ -118,4 +125,8 @@ public class EventB implements IEvalElement, IEntity {
 		return false;
 	}
 
+	public String getName() {
+		return name;
+	}
+
 }

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));
 	}
 }

de.prob.core/src/de/prob/model/eventb/Relationship.java

 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 final ERefType type;
 
-	public Relationship(Label from,Label to) {
+	public Relationship(Label from, Label to, ERefType type) {
 		this.from = from;
 		this.to = to;
+		this.type = type;
 	}
 }

de.prob.core/src/de/prob/model/representation/RefType.java

+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;
+	}
+}

de.prob.ui/src/de/prob/ui/eventb/ExportNewCoreHandler.java

 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) {

de.prob.ui/src/de/prob/ui/eventb/NewCoreModelTranslation.java

+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;
+	}
+
+}