diff --git a/de.prob.core/.classpath b/de.prob.core/.classpath
index b5efa8550ac9c4daefb09ca828889085b018d941..f469a1446bc01801b9d7033478bd396dfa04b812 100644
--- a/de.prob.core/.classpath
+++ b/de.prob.core/.classpath
@@ -1,23 +1,23 @@
<?xml version="1.0" encoding="UTF-8"?>
<classpath>
- <classpathentry exported="true" kind="lib" path="lib/dependencies/commons-codec-1.6.jar"/>
- <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/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 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 kind="output" path="bin"/>
<classpathentry exported="true" kind="lib" path="lib/dependencies/answerparser-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/cliparser-2.4.12-SNAPSHOT.jar"/>
+ <classpathentry exported="true" kind="lib" path="lib/dependencies/commons-codec-1.6.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.12-SNAPSHOT.jar"/>
+ <classpathentry exported="true" kind="lib" path="lib/dependencies/parserbase-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"/>
+ <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"/>
</classpath>
diff --git a/de.prob.core/src/de/prob/core/command/ActivateUnitPluginCommand.java b/de.prob.core/src/de/prob/core/command/ActivateUnitPluginCommand.java
new file mode 100644
index 0000000000000000000000000000000000000000..5071e60e1f179908b6a1d438c12b818c408407ac
--- /dev/null
+++ b/de.prob.core/src/de/prob/core/command/ActivateUnitPluginCommand.java
@@ -0,0 +1,57 @@
+/**
+ * (c) 2009 Lehrstuhl fuer Softwaretechnik und Programmiersprachen, Heinrich
+ * Heine Universitaet Duesseldorf This software is licenced under EPL 1.0
+ * (http://www.eclipse.org/org/documents/epl-v10.html)
+ * */
+
+package de.prob.core.command;
+
+import de.prob.core.Animator;
+import de.prob.exceptions.ProBException;
+import de.prob.parser.ISimplifiedROMap;
+import de.prob.prolog.output.IPrologTermOutput;
+import de.prob.prolog.term.PrologTerm;
+
+public class ActivateUnitPluginCommand implements IComposableCommand {
+
+ private static final ActivateCmd ACTIVATE_CMD = new ActivateCmd();
+ private final GetPrologRandomSeed getRandomSeed;
+ private final ComposedCommand cmd;
+
+ public ActivateUnitPluginCommand() {
+ this.getRandomSeed = new GetPrologRandomSeed();
+ this.cmd = new ComposedCommand(getRandomSeed, ACTIVATE_CMD);
+ }
+
+ public static void activateUnitPlugin(final Animator animator)
+ throws ProBException {
+ animator.execute(new ActivateUnitPluginCommand());
+ }
+
+ public void processResult(
+ final ISimplifiedROMap<String, PrologTerm> bindings)
+ throws CommandException {
+ cmd.processResult(bindings);
+ final Animator animator = Animator.getAnimator();
+ animator.setRandomSeed(getRandomSeed.getSeed());
+ }
+
+ public void writeCommand(final IPrologTermOutput pto)
+ throws CommandException {
+ cmd.writeCommand(pto);
+ }
+
+ private final static class ActivateCmd implements IComposableCommand {
+ public void processResult(
+ final ISimplifiedROMap<String, PrologTerm> bindings)
+ throws CommandException {
+ }
+
+ public void writeCommand(final IPrologTermOutput pto) {
+ pto.openTerm("activate_plugin");
+ pto.printAtom("units");
+ pto.closeTerm();
+ }
+ }
+
+}
diff --git a/de.prob.core/src/de/prob/core/command/GetPluginResultCommand.java b/de.prob.core/src/de/prob/core/command/GetPluginResultCommand.java
new file mode 100644
index 0000000000000000000000000000000000000000..eb99459f5a1e7b6264873bd541f0e8d7f81a06c0
--- /dev/null
+++ b/de.prob.core/src/de/prob/core/command/GetPluginResultCommand.java
@@ -0,0 +1,47 @@
+/**
+ * (c) 2009 Lehrstuhl fuer Softwaretechnik und Programmiersprachen, Heinrich
+ * Heine Universitaet Duesseldorf This software is licenced under EPL 1.0
+ * (http://www.eclipse.org/org/documents/epl-v10.html)
+ * */
+
+package de.prob.core.command;
+
+import de.prob.parser.BindingGenerator;
+import de.prob.parser.ISimplifiedROMap;
+import de.prob.parser.ResultParserException;
+import de.prob.prolog.output.IPrologTermOutput;
+import de.prob.prolog.term.ListPrologTerm;
+import de.prob.prolog.term.PrologTerm;
+
+public final class GetPluginResultCommand implements IComposableCommand {
+
+ private final String resultID;
+ private ListPrologTerm result;
+
+ public GetPluginResultCommand(final String resultID) {
+ this.resultID = resultID;
+ }
+
+ public ListPrologTerm getResult() {
+ return result;
+ }
+
+ public void processResult(
+ final ISimplifiedROMap<String, PrologTerm> bindings)
+ throws CommandException {
+ try {
+ result = BindingGenerator.getList(bindings, "Bindings");
+ } catch (ResultParserException e) {
+ CommandException commandException = new CommandException(
+ e.getLocalizedMessage(), e);
+ commandException.notifyUserOnce();
+ throw commandException;
+ }
+ }
+
+ public void writeCommand(final IPrologTermOutput pto) {
+ pto.openTerm("get_plugin_output").printAtomOrNumber(resultID)
+ .printVariable("Bindings").closeTerm();
+ }
+
+}
diff --git a/de.prob.core/src/de/prob/core/command/LoadEventBModelCommand.java b/de.prob.core/src/de/prob/core/command/LoadEventBModelCommand.java
index 316d436cfb029a75fd3232548ee3415f178854a1..78335f27dbe8219e1129b5286e771ac514283b15 100644
--- a/de.prob.core/src/de/prob/core/command/LoadEventBModelCommand.java
+++ b/de.prob.core/src/de/prob/core/command/LoadEventBModelCommand.java
@@ -19,17 +19,15 @@ import org.rodinp.core.RodinDBException;
import de.prob.core.Animator;
import de.prob.core.LanguageDependendAnimationPart;
+import de.prob.core.command.internal.InternalLoadCommand;
import de.prob.core.domainobjects.MachineDescription;
import de.prob.core.domainobjects.Operation;
import de.prob.core.domainobjects.ProBPreference;
import de.prob.core.domainobjects.State;
import de.prob.core.langdep.EventBAnimatorPart;
-import de.prob.core.translator.TranslationFailedException;
-import de.prob.eventb.translator.TranslatorFactory;
import de.prob.exceptions.ProBException;
import de.prob.logging.Logger;
import de.prob.parser.ISimplifiedROMap;
-import de.prob.prolog.output.IPrologTermOutput;
import de.prob.prolog.output.StructuredPrologOutput;
import de.prob.prolog.term.PrologTerm;
@@ -162,32 +160,4 @@ public final class LoadEventBModelCommand {
animator.announceReset();
}
}
-
- private static class InternalLoadCommand implements IComposableCommand {
- private final IEventBRoot model;
-
- public InternalLoadCommand(final IEventBRoot model) {
- this.model = model;
- }
-
- @Override
- public void writeCommand(final IPrologTermOutput pto)
- throws CommandException {
- try {
- TranslatorFactory.translate(model, pto);
- } catch (TranslationFailedException e) {
- throw new CommandException(
- "Translation from Event-B to ProB's internal representation failed",
- e);
- }
- }
-
- @Override
- public void processResult(
- final ISimplifiedROMap<String, PrologTerm> bindings)
- throws CommandException {
- // there are no results to process
- }
-
- }
}
diff --git a/de.prob.core/src/de/prob/core/command/internal/InternalLoadCommand.java b/de.prob.core/src/de/prob/core/command/internal/InternalLoadCommand.java
new file mode 100644
index 0000000000000000000000000000000000000000..2a3eaf98d4fd0b82a4a4718c0878d2366bf08e67
--- /dev/null
+++ b/de.prob.core/src/de/prob/core/command/internal/InternalLoadCommand.java
@@ -0,0 +1,39 @@
+package de.prob.core.command.internal;
+
+import org.eventb.core.IEventBRoot;
+
+import de.prob.core.command.CommandException;
+import de.prob.core.command.IComposableCommand;
+import de.prob.core.translator.TranslationFailedException;
+import de.prob.eventb.translator.TranslatorFactory;
+import de.prob.parser.ISimplifiedROMap;
+import de.prob.prolog.output.IPrologTermOutput;
+import de.prob.prolog.term.PrologTerm;
+
+public final class InternalLoadCommand implements IComposableCommand {
+ private final IEventBRoot model;
+
+ public InternalLoadCommand(final IEventBRoot model) {
+ this.model = model;
+ }
+
+ @Override
+ public void writeCommand(final IPrologTermOutput pto)
+ throws CommandException {
+ try {
+ TranslatorFactory.translate(model, pto);
+ } catch (TranslationFailedException e) {
+ throw new CommandException(
+ "Translation from Event-B to ProB's internal representation failed",
+ e);
+ }
+ }
+
+ @Override
+ public void processResult(
+ final ISimplifiedROMap<String, PrologTerm> bindings)
+ throws CommandException {
+ // there are no results to process
+ }
+
+}
\ No newline at end of file
diff --git a/de.prob.core/src/de/prob/core/translator/pragmas/IPragma.java b/de.prob.core/src/de/prob/core/translator/pragmas/IPragma.java
new file mode 100644
index 0000000000000000000000000000000000000000..aa8994a965629cc4da6ca5c395c7a05cfcb83512
--- /dev/null
+++ b/de.prob.core/src/de/prob/core/translator/pragmas/IPragma.java
@@ -0,0 +1,15 @@
+/**
+ * (c) 2009 Lehrstuhl fuer Softwaretechnik und Programmiersprachen, Heinrich
+ * Heine Universitaet Duesseldorf This software is licenced under EPL 1.0
+ * (http://www.eclipse.org/org/documents/epl-v10.html)
+ * */
+
+package de.prob.core.translator.pragmas;
+
+import de.prob.prolog.output.IPrologTermOutput;
+
+public interface IPragma {
+
+ void output(IPrologTermOutput pout);
+
+}
diff --git a/de.prob.core/src/de/prob/core/translator/pragmas/UnitPragma.java b/de.prob.core/src/de/prob/core/translator/pragmas/UnitPragma.java
new file mode 100644
index 0000000000000000000000000000000000000000..a1b5fd09d13a81b4e05149e7ca95aae0a2c76acd
--- /dev/null
+++ b/de.prob.core/src/de/prob/core/translator/pragmas/UnitPragma.java
@@ -0,0 +1,34 @@
+/**
+ * (c) 2009 Lehrstuhl fuer Softwaretechnik und Programmiersprachen, Heinrich
+ * Heine Universitaet Duesseldorf This software is licenced under EPL 1.0
+ * (http://www.eclipse.org/org/documents/epl-v10.html)
+ * */
+
+package de.prob.core.translator.pragmas;
+
+import de.prob.prolog.output.IPrologTermOutput;
+
+public class UnitPragma implements IPragma {
+ private String definedIn;
+ private String attachedTo;
+ private String content;
+
+ public UnitPragma(String definedIn, String attachedTo, String content) {
+ this.definedIn = definedIn;
+ this.attachedTo = attachedTo;
+ this.content = content;
+ }
+
+ @Override
+ public void output(IPrologTermOutput pout) {
+ pout.openTerm("pragma");
+ pout.printAtom("unit");
+ pout.printAtom(definedIn);
+ pout.printAtom(attachedTo);
+ pout.openList();
+ pout.printAtom(content);
+ pout.closeList();
+ pout.closeTerm();
+ }
+
+}
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 ad5b33afb304accdbaa9f275db0e8a47d91b6707..e65b7464246d76d8685d5b6bb32ff9e891d19f24 100644
--- a/de.prob.core/src/de/prob/eventb/translator/ContextTranslator.java
+++ b/de.prob.core/src/de/prob/eventb/translator/ContextTranslator.java
@@ -32,9 +32,11 @@ import org.eventb.core.ISCMachineRoot;
import org.eventb.core.ast.FormulaFactory;
import org.eventb.core.ast.ITypeEnvironment;
import org.eventb.core.seqprover.IConfidence;
+import org.rodinp.core.IAttributeType;
import org.rodinp.core.IRodinElement;
import org.rodinp.core.IRodinFile;
import org.rodinp.core.IRodinProject;
+import org.rodinp.core.RodinCore;
import org.rodinp.core.RodinDBException;
import de.be4.classicalb.core.parser.analysis.pragma.internal.ClassifiedPragma;
@@ -53,6 +55,8 @@ 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.core.translator.pragmas.IPragma;
+import de.prob.core.translator.pragmas.UnitPragma;
import de.prob.eventb.translator.internal.EProofStatus;
import de.prob.eventb.translator.internal.ProofObligation;
import de.prob.eventb.translator.internal.SequentSource;
@@ -65,6 +69,7 @@ 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 List<IPragma> pragmas = new ArrayList<IPragma>();
public static ContextTranslator create(final ISCContext context)
throws TranslationFailedException {
@@ -121,7 +126,26 @@ public final class ContextTranslator extends AbstractComponentTranslator {
Assert.isTrue(machine_root.getRodinFile().isConsistent());
}
translateContext();
+ collectPragmas();
+ }
+
+ private void collectPragmas() throws RodinDBException {
+ // unit pragma, attached to constants
+ final IAttributeType.String UNITATTRIBUTE = RodinCore
+ .getStringAttrType("de.prob.units.unitPragmaAttribute");
+
+ final ISCConstant[] constants = context.getSCConstants();
+
+ for (final ISCConstant constant : constants) {
+ if (constant.hasAttribute(UNITATTRIBUTE)) {
+ String content = constant.getAttributeValue(UNITATTRIBUTE);
+ if (!content.isEmpty()) {
+ pragmas.add(new UnitPragma(getResource(), constant
+ .getIdentifierString(), content));
+ }
+ }
+ }
}
private void collectProofInfo(ISCContextRoot origin)
@@ -327,6 +351,11 @@ public final class ContextTranslator extends AbstractComponentTranslator {
return proofs;
}
+ public List<IPragma> getPragmas() {
+ // TODO Auto-generated method stub
+ return pragmas;
+ }
+
public List<ClassifiedPragma> getProofspragmas() {
return proofspragmas;
}
diff --git a/de.prob.core/src/de/prob/eventb/translator/internal/EventBContextTranslator.java b/de.prob.core/src/de/prob/eventb/translator/internal/EventBContextTranslator.java
index ae640ff98a9c1d84b2014b850b42db0f3c2058f3..075270d4ae253ae3aef71dafd9d877e1ee61a433 100644
--- a/de.prob.core/src/de/prob/eventb/translator/internal/EventBContextTranslator.java
+++ b/de.prob.core/src/de/prob/eventb/translator/internal/EventBContextTranslator.java
@@ -51,13 +51,15 @@ public final class EventBContextTranslator extends EventBTranslator {
private void constructTranslation(final IPrologTermOutput pto)
throws TranslationFailedException {
- List<ContextTranslator> translators = new ArrayList<ContextTranslator>();
-// translators.add(ContextTranslator.create(context));
+ List<ContextTranslator> contextTranslators = new ArrayList<ContextTranslator>();
+
+ // translators.add(ContextTranslator.create(context));
if (context instanceof ISCContextRoot) {
ISCContextRoot root = (ISCContextRoot) context;
- collectContexts(translators, new ArrayList<String>(), root);
+ collectContexts(contextTranslators, new ArrayList<String>(), root);
}
- printProlog(new ArrayList<ModelTranslator>(), translators, pto);
+
+ printProlog(new ArrayList<ModelTranslator>(), contextTranslators, pto);
}
private void collectContexts(final List<ContextTranslator> translatorMap,
diff --git a/de.prob.core/src/de/prob/eventb/translator/internal/EventBMachineTranslator.java b/de.prob.core/src/de/prob/eventb/translator/internal/EventBMachineTranslator.java
index b6ee12f4e13e3fbabecdd6b9ea25020a3f8b907f..1b9e5fb6179714c13da881ffcedb401ac70ef529 100644
--- a/de.prob.core/src/de/prob/eventb/translator/internal/EventBMachineTranslator.java
+++ b/de.prob.core/src/de/prob/eventb/translator/internal/EventBMachineTranslator.java
@@ -102,6 +102,7 @@ public final class EventBMachineTranslator extends EventBTranslator {
throws TranslationFailedException {
final List<ContextTranslator> translators = new ArrayList<ContextTranslator>();
final List<String> processed = new ArrayList<String>();
+
for (ISCMachineRoot m : models) {
ISCInternalContext[] seenContexts;
try {
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 ed82d8a8e8ee13b70b2e191805fa67b5168c306b..4cf7538db93dfea3df0b9355063386031bca3f3a 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
@@ -23,6 +23,7 @@ import de.be4.classicalb.core.parser.node.AEventBModelParseUnit;
import de.be4.classicalb.core.parser.node.Node;
import de.prob.core.translator.ITranslator;
import de.prob.core.translator.TranslationFailedException;
+import de.prob.core.translator.pragmas.IPragma;
import de.prob.eventb.translator.AbstractComponentTranslator;
import de.prob.eventb.translator.ContextTranslator;
import de.prob.prolog.output.IPrologTermOutput;
@@ -112,6 +113,24 @@ public abstract class EventBTranslator implements ITranslator {
printFlowInformation(pout);
}
+ private void printPragmaContents(
+ Collection<ModelTranslator> refinementChainTranslators,
+ Collection<ContextTranslator> contextTranslators,
+ IPrologTermOutput pout) {
+ ArrayList<IPragma> pragmas = new ArrayList<IPragma>();
+
+ for (ContextTranslator contextTranslator : contextTranslators) {
+ pragmas.addAll(contextTranslator.getPragmas());
+ }
+ for (ModelTranslator modelTranslator : refinementChainTranslators) {
+ pragmas.addAll(modelTranslator.getPragmas());
+ }
+
+ for (IPragma pragma : pragmas) {
+ pragma.output(pout);
+ }
+ }
+
protected abstract void printFlowInformation(final IPrologTermOutput pout);
private ASTProlog createAstVisitor(
@@ -147,6 +166,8 @@ public abstract class EventBTranslator implements ITranslator {
// } catch (RodinDBException e) {
// e.printStackTrace();
// }
+ printPragmaContents(refinementChainTranslators, contextTranslators,
+ pout);
pout.closeList();
pout.printVariable("_Error");
pout.closeTerm();
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 ead67da6ba447b4f830418088f54eb34069a3bf7..b121f405c522a52f7b8f866fd93487234a8900e0 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
@@ -35,13 +35,16 @@ import org.eventb.core.ISCVariable;
import org.eventb.core.ISCVariant;
import org.eventb.core.ISCWitness;
import org.eventb.core.ITraceableElement;
+import org.eventb.core.IVariable;
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.IAttributeType;
import org.rodinp.core.IElementType;
import org.rodinp.core.IRodinElement;
import org.rodinp.core.IRodinFile;
+import org.rodinp.core.RodinCore;
import org.rodinp.core.RodinDBException;
import de.be4.classicalb.core.parser.node.AAnticipatedEventstatus;
@@ -67,6 +70,8 @@ import de.be4.classicalb.core.parser.node.PSubstitution;
import de.be4.classicalb.core.parser.node.PWitness;
import de.be4.classicalb.core.parser.node.TIdentifierLiteral;
import de.prob.core.translator.TranslationFailedException;
+import de.prob.core.translator.pragmas.IPragma;
+import de.prob.core.translator.pragmas.UnitPragma;
import de.prob.eventb.translator.AbstractComponentTranslator;
import de.prob.eventb.translator.AssignmentVisitor;
import de.prob.eventb.translator.ExpressionVisitor;
@@ -81,6 +86,8 @@ public class ModelTranslator extends AbstractComponentTranslator {
private final ITypeEnvironment te;
private final IMachineRoot origin;
private final List<ProofObligation> proofs = new ArrayList<ProofObligation>();
+ private final List<IPragma> pragmas = new ArrayList<IPragma>();
+
// private final List<String> depContext = new ArrayList<String>();
// Confined in the thread calling the factory method
@@ -117,6 +124,10 @@ public class ModelTranslator extends AbstractComponentTranslator {
return Collections.unmodifiableList(proofs);
}
+ public List<IPragma> getPragmas() {
+ return Collections.unmodifiableList(pragmas);
+ }
+
public AEventBModelParseUnit getModelAST() {
if (broken) {
final String message = "The machine contains Rodin Problems. Please fix it before animating";
@@ -164,6 +175,28 @@ public class ModelTranslator extends AbstractComponentTranslator {
// Check for fully discharged Invariants and Events
collectProofInfo();
+
+ // Collect Pragmas, Units, etc.
+ collectPragmas();
+ }
+
+ private void collectPragmas() throws RodinDBException {
+ // unit pragma, attached to constants
+ final IAttributeType.String UNITATTRIBUTE = RodinCore
+ .getStringAttrType("de.prob.units.unitPragmaAttribute");
+
+ final IVariable[] variables = origin.getVariables();
+
+ for (final IVariable variable : variables) {
+ if (variable.hasAttribute(UNITATTRIBUTE)) {
+ String content = variable.getAttributeValue(UNITATTRIBUTE);
+
+ if (!content.isEmpty()) {
+ pragmas.add(new UnitPragma(getResource(), variable
+ .getIdentifierString(), content));
+ }
+ }
+ }
}
private void collectProofInfo() throws RodinDBException {
@@ -179,7 +212,8 @@ public class ModelTranslator extends AbstractComponentTranslator {
EProofStatus pstatus = EProofStatus.UNPROVEN;
- if (!broken && (confidence > IConfidence.PENDING && confidence <= IConfidence.REVIEWED_MAX))
+ if (!broken
+ && (confidence > IConfidence.PENDING && confidence <= IConfidence.REVIEWED_MAX))
pstatus = EProofStatus.REVIEWED;
if (!broken && confidence == IConfidence.DISCHARGED_MAX)
pstatus = EProofStatus.PROVEN;
diff --git a/de.prob.ui/.classpath b/de.prob.ui/.classpath
index f67843181ee95a7771d0edd1009be1faaed415b0..100092b255b1ad1a077f31d3e5931b134f6f5f45 100644
--- a/de.prob.ui/.classpath
+++ b/de.prob.ui/.classpath
@@ -1,10 +1,10 @@
<?xml version="1.0" encoding="UTF-8"?>
<classpath>
- <classpathentry exported="true" kind="lib" path="lib/dependencies/commons-codec-1.6.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 exported="true" kind="lib" path="lib/apache_xmlrpc.jar"/>
<classpathentry exported="true" kind="lib" path="lib/ws_commons.jar"/>
<classpathentry kind="output" path="bin"/>
+ <classpathentry exported="true" kind="lib" path="lib/dependencies/commons-codec-1.6.jar"/>
</classpath>
diff --git a/de.prob.units/.classpath b/de.prob.units/.classpath
new file mode 100644
index 0000000000000000000000000000000000000000..ad32c83a7885b8953a938b41df3b4fd4fe1aae01
--- /dev/null
+++ b/de.prob.units/.classpath
@@ -0,0 +1,7 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<classpath>
+ <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="output" path="bin"/>
+</classpath>
diff --git a/de.prob.units/.project b/de.prob.units/.project
new file mode 100644
index 0000000000000000000000000000000000000000..22333fa9cb227f96d35310a6635507f782547a31
--- /dev/null
+++ b/de.prob.units/.project
@@ -0,0 +1,28 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<projectDescription>
+ <name>de.prob.units</name>
+ <comment></comment>
+ <projects>
+ </projects>
+ <buildSpec>
+ <buildCommand>
+ <name>org.eclipse.jdt.core.javabuilder</name>
+ <arguments>
+ </arguments>
+ </buildCommand>
+ <buildCommand>
+ <name>org.eclipse.pde.ManifestBuilder</name>
+ <arguments>
+ </arguments>
+ </buildCommand>
+ <buildCommand>
+ <name>org.eclipse.pde.SchemaBuilder</name>
+ <arguments>
+ </arguments>
+ </buildCommand>
+ </buildSpec>
+ <natures>
+ <nature>org.eclipse.pde.PluginNature</nature>
+ <nature>org.eclipse.jdt.core.javanature</nature>
+ </natures>
+</projectDescription>
diff --git a/de.prob.units/.settings/org.eclipse.jdt.core.prefs b/de.prob.units/.settings/org.eclipse.jdt.core.prefs
new file mode 100644
index 0000000000000000000000000000000000000000..c537b63063ce6052bdc49c5fd0745b078f162c90
--- /dev/null
+++ b/de.prob.units/.settings/org.eclipse.jdt.core.prefs
@@ -0,0 +1,7 @@
+eclipse.preferences.version=1
+org.eclipse.jdt.core.compiler.codegen.inlineJsrBytecode=enabled
+org.eclipse.jdt.core.compiler.codegen.targetPlatform=1.6
+org.eclipse.jdt.core.compiler.compliance=1.6
+org.eclipse.jdt.core.compiler.problem.assertIdentifier=error
+org.eclipse.jdt.core.compiler.problem.enumIdentifier=error
+org.eclipse.jdt.core.compiler.source=1.6
diff --git a/de.prob.units/META-INF/MANIFEST.MF b/de.prob.units/META-INF/MANIFEST.MF
new file mode 100644
index 0000000000000000000000000000000000000000..2fd89c80dfacabe94b60f1cb276335c25705d1f1
--- /dev/null
+++ b/de.prob.units/META-INF/MANIFEST.MF
@@ -0,0 +1,14 @@
+Manifest-Version: 1.0
+Bundle-ManifestVersion: 2
+Bundle-Name: ProB Physical Units Support
+Bundle-SymbolicName: de.prob.units;singleton:=true
+Bundle-Version: 1.0.0.qualifier
+Bundle-Activator: de.prob.units.Activator
+Require-Bundle: org.eclipse.ui,
+ org.eclipse.core.runtime,
+ de.prob.core;bundle-version="9.3.0",
+ org.eventb.ui;bundle-version="[2.1.0,2.6.0)",
+ de.prob.ui;bundle-version="7.3.0"
+Bundle-ActivationPolicy: lazy
+Bundle-RequiredExecutionEnvironment: JavaSE-1.6
+Bundle-Vendor: HHU Düsseldorf STUPS Group
diff --git a/de.prob.units/build.properties b/de.prob.units/build.properties
new file mode 100644
index 0000000000000000000000000000000000000000..e9863e281eaccc5123e82ed75713bab3e8b87bbe
--- /dev/null
+++ b/de.prob.units/build.properties
@@ -0,0 +1,5 @@
+source.. = src/
+output.. = bin/
+bin.includes = META-INF/,\
+ .,\
+ plugin.xml
diff --git a/de.prob.units/icons/unit_analysis.png b/de.prob.units/icons/unit_analysis.png
new file mode 100644
index 0000000000000000000000000000000000000000..36d5d6278be2e2226de7b9d4d0fc9da720e47f1b
Binary files /dev/null and b/de.prob.units/icons/unit_analysis.png differ
diff --git a/de.prob.units/plugin.xml b/de.prob.units/plugin.xml
new file mode 100644
index 0000000000000000000000000000000000000000..9c40c5db7d2f4deb3e68226c679a129edede9373
--- /dev/null
+++ b/de.prob.units/plugin.xml
@@ -0,0 +1,101 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<?eclipse version="3.4"?>
+<plugin>
+ <extension
+ point="org.eventb.ui.editorItems">
+ <textAttribute
+ class="de.prob.units.pragmas.UnitPragmaAttribute"
+ expandsHorizontally="true"
+ id="de.prob.units.unitPragmaAttribute"
+ isMath="true"
+ prefix="Physical Unit:"
+ style="de.prob.units.unitPragmaAttribute"
+ typeId="de.prob.units.unitPragmaAttribute">
+ </textAttribute>
+ <attributeRelation
+ elementTypeId="org.eventb.core.variable">
+ <attributeReference
+ descriptionId="de.prob.units.unitPragmaAttribute">
+ </attributeReference>
+ <attributeReference
+ descriptionId="de.prob.units.inferredUnitPragmaAttribute">
+ </attributeReference>
+ </attributeRelation>
+ <attributeRelation
+ elementTypeId="org.eventb.core.constant">
+ <attributeReference
+ descriptionId="de.prob.units.unitPragmaAttribute">
+ </attributeReference>
+ <attributeReference
+ descriptionId="de.prob.units.inferredUnitPragmaAttribute">
+ </attributeReference>
+ </attributeRelation>
+ <textAttribute
+ class="de.prob.units.pragmas.InferredUnitPragmaAttribute"
+ expandsHorizontally="true"
+ id="de.prob.units.inferredUnitPragmaAttribute"
+ isMath="true"
+ prefix="Inferred Physical Unit:"
+ style="de.prob.units.inferredUnitPragmaAttribute"
+ typeId="de.prob.units.inferredUnitPragmaAttribute">
+ </textAttribute>
+ </extension>
+ <extension
+ point="org.eclipse.ui.handlers">
+ <handler
+ class="de.prob.units.ui.StartUnitAnalysisHandler"
+ commandId="de.prob.units.startunitanalysis">
+ </handler>
+ </extension>
+ <extension
+ point="org.eclipse.ui.menus">
+ <menuContribution
+ locationURI="popup:fr.systerel.explorer.navigator.view">
+ <separator
+ name="de.prob.units.separator2"
+ visible="true">
+ </separator>
+ <command
+ commandId="de.prob.units.startunitanalysis"
+ icon="icons/unit_analysis.png"
+ label="Analyse Physical Units"
+ style="push">
+ <visibleWhen>
+ <with
+ variable="selection">
+ <iterate
+ operator="or">
+ <instanceof
+ value="org.eventb.core.IEventBRoot">
+ </instanceof>
+ </iterate>
+ </with>
+ </visibleWhen>
+ </command>
+ <separator
+ name="de.prob.units.separator1"
+ visible="true">
+ </separator>
+ </menuContribution>
+ </extension>
+ <extension
+ point="org.eclipse.ui.commands">
+ <command
+ id="de.prob.units.startunitanalysis"
+ name="Analyse Physical Units">
+ </command>
+ </extension>
+ <extension
+ point="org.rodinp.core.attributeTypes">
+ <attributeType
+ id="unitPragmaAttribute"
+ kind="string"
+ name="Content of a unit Pragma to send to ProB">
+ </attributeType>
+ <attributeType
+ id="inferredUnitPragmaAttribute"
+ kind="string"
+ name="Content of a unit Pragma received from ProB">
+ </attributeType>
+ </extension>
+</plugin>
diff --git a/de.prob.units/src/de/prob/units/Activator.java b/de.prob.units/src/de/prob/units/Activator.java
new file mode 100644
index 0000000000000000000000000000000000000000..cb9482f57446625e611905dd23c999190b96cf5c
--- /dev/null
+++ b/de.prob.units/src/de/prob/units/Activator.java
@@ -0,0 +1,50 @@
+package de.prob.units;
+
+import org.eclipse.ui.plugin.AbstractUIPlugin;
+import org.osgi.framework.BundleContext;
+
+/**
+ * The activator class controls the plug-in life cycle
+ */
+public class Activator extends AbstractUIPlugin {
+
+ // The plug-in ID
+ public static final String PLUGIN_ID = "de.prob.units"; //$NON-NLS-1$
+
+ // The shared instance
+ private static Activator plugin;
+
+ /**
+ * The constructor
+ */
+ public Activator() {
+ }
+
+ /*
+ * (non-Javadoc)
+ * @see org.eclipse.ui.plugin.AbstractUIPlugin#start(org.osgi.framework.BundleContext)
+ */
+ public void start(BundleContext context) throws Exception {
+ super.start(context);
+ plugin = this;
+ }
+
+ /*
+ * (non-Javadoc)
+ * @see org.eclipse.ui.plugin.AbstractUIPlugin#stop(org.osgi.framework.BundleContext)
+ */
+ public void stop(BundleContext context) throws Exception {
+ plugin = null;
+ super.stop(context);
+ }
+
+ /**
+ * Returns the shared instance
+ *
+ * @return the shared instance
+ */
+ public static Activator getDefault() {
+ return plugin;
+ }
+
+}
diff --git a/de.prob.units/src/de/prob/units/pragmas/InferredUnitPragmaAttribute.java b/de.prob.units/src/de/prob/units/pragmas/InferredUnitPragmaAttribute.java
new file mode 100644
index 0000000000000000000000000000000000000000..a2d7ec278f082fb569e9827a184f7b6785a823c1
--- /dev/null
+++ b/de.prob.units/src/de/prob/units/pragmas/InferredUnitPragmaAttribute.java
@@ -0,0 +1,75 @@
+/**
+ * (c) 2009 Lehrstuhl fuer Softwaretechnik und Programmiersprachen, Heinrich
+ * Heine Universitaet Duesseldorf This software is licenced under EPL 1.0
+ * (http://www.eclipse.org/org/documents/epl-v10.html)
+ * */
+
+package de.prob.units.pragmas;
+
+import org.eclipse.core.runtime.IProgressMonitor;
+import org.eventb.core.IVariable;
+import org.eventb.core.basis.Constant;
+import org.eventb.internal.ui.eventbeditor.manipulation.IAttributeManipulation;
+import org.rodinp.core.IAttributeType;
+import org.rodinp.core.IInternalElement;
+import org.rodinp.core.IRodinElement;
+import org.rodinp.core.RodinCore;
+import org.rodinp.core.RodinDBException;
+
+import de.prob.units.Activator;
+
+public class InferredUnitPragmaAttribute implements IAttributeManipulation {
+ public static IAttributeType.String ATTRIBUTE = RodinCore
+ .getStringAttrType(Activator.PLUGIN_ID
+ + ".inferredUnitPragmaAttribute");
+
+ public InferredUnitPragmaAttribute() {
+ // empty constructor
+ }
+
+ private IInternalElement asInternalElement(IRodinElement element) {
+ if (element instanceof IVariable) {
+ return (IVariable) element;
+ } else if (element instanceof Constant) {
+ return (Constant) element;
+ }
+ return null;
+ }
+
+ @Override
+ public String[] getPossibleValues(IRodinElement element,
+ IProgressMonitor monitor) {
+ return null;
+ }
+
+ @Override
+ public String getValue(IRodinElement element, IProgressMonitor monitor)
+ throws RodinDBException {
+ return asInternalElement(element).getAttributeValue(ATTRIBUTE);
+ }
+
+ @Override
+ public boolean hasValue(IRodinElement element, IProgressMonitor monitor)
+ throws RodinDBException {
+ return asInternalElement(element).hasAttribute(ATTRIBUTE);
+ }
+
+ @Override
+ public void removeAttribute(IRodinElement element, IProgressMonitor monitor)
+ throws RodinDBException {
+ asInternalElement(element).removeAttribute(ATTRIBUTE, monitor);
+
+ }
+
+ @Override
+ public void setDefaultValue(IRodinElement element, IProgressMonitor monitor)
+ throws RodinDBException {
+ asInternalElement(element).setAttributeValue(ATTRIBUTE, "", monitor);
+ }
+
+ @Override
+ public void setValue(IRodinElement element, String value,
+ IProgressMonitor monitor) throws RodinDBException {
+ asInternalElement(element).setAttributeValue(ATTRIBUTE, value, monitor);
+ }
+}
diff --git a/de.prob.units/src/de/prob/units/pragmas/UnitPragmaAttribute.java b/de.prob.units/src/de/prob/units/pragmas/UnitPragmaAttribute.java
new file mode 100644
index 0000000000000000000000000000000000000000..8c0075f18b1545de6594c0234b6480b690db660f
--- /dev/null
+++ b/de.prob.units/src/de/prob/units/pragmas/UnitPragmaAttribute.java
@@ -0,0 +1,74 @@
+/**
+ * (c) 2009 Lehrstuhl fuer Softwaretechnik und Programmiersprachen, Heinrich
+ * Heine Universitaet Duesseldorf This software is licenced under EPL 1.0
+ * (http://www.eclipse.org/org/documents/epl-v10.html)
+ * */
+
+package de.prob.units.pragmas;
+
+import org.eclipse.core.runtime.IProgressMonitor;
+import org.eventb.core.IVariable;
+import org.eventb.core.basis.Constant;
+import org.eventb.internal.ui.eventbeditor.manipulation.IAttributeManipulation;
+import org.rodinp.core.IAttributeType;
+import org.rodinp.core.IInternalElement;
+import org.rodinp.core.IRodinElement;
+import org.rodinp.core.RodinCore;
+import org.rodinp.core.RodinDBException;
+
+import de.prob.units.Activator;
+
+public class UnitPragmaAttribute implements IAttributeManipulation {
+ public static IAttributeType.String ATTRIBUTE = RodinCore
+ .getStringAttrType(Activator.PLUGIN_ID + ".unitPragmaAttribute");
+
+ public UnitPragmaAttribute() {
+ // empty constructor
+ }
+
+ private IInternalElement asInternalElement(IRodinElement element) {
+ if (element instanceof IVariable) {
+ return (IVariable) element;
+ } else if (element instanceof Constant) {
+ return (Constant) element;
+ }
+ return null;
+ }
+
+ @Override
+ public String[] getPossibleValues(IRodinElement element,
+ IProgressMonitor monitor) {
+ return null;
+ }
+
+ @Override
+ public String getValue(IRodinElement element, IProgressMonitor monitor)
+ throws RodinDBException {
+ return asInternalElement(element).getAttributeValue(ATTRIBUTE);
+ }
+
+ @Override
+ public boolean hasValue(IRodinElement element, IProgressMonitor monitor)
+ throws RodinDBException {
+ return asInternalElement(element).hasAttribute(ATTRIBUTE);
+ }
+
+ @Override
+ public void removeAttribute(IRodinElement element, IProgressMonitor monitor)
+ throws RodinDBException {
+ asInternalElement(element).removeAttribute(ATTRIBUTE, monitor);
+
+ }
+
+ @Override
+ public void setDefaultValue(IRodinElement element, IProgressMonitor monitor)
+ throws RodinDBException {
+ asInternalElement(element).setAttributeValue(ATTRIBUTE, "", monitor);
+ }
+
+ @Override
+ public void setValue(IRodinElement element, String value,
+ IProgressMonitor monitor) throws RodinDBException {
+ asInternalElement(element).setAttributeValue(ATTRIBUTE, value, monitor);
+ }
+}
diff --git a/de.prob.units/src/de/prob/units/ui/StartUnitAnalysisHandler.java b/de.prob.units/src/de/prob/units/ui/StartUnitAnalysisHandler.java
new file mode 100644
index 0000000000000000000000000000000000000000..13585c407fc04e9c63257ab7e220d1e8159d62e1
--- /dev/null
+++ b/de.prob.units/src/de/prob/units/ui/StartUnitAnalysisHandler.java
@@ -0,0 +1,283 @@
+/**
+ * (c) 2009 Lehrstuhl fuer Softwaretechnik und Programmiersprachen, Heinrich
+ * Heine Universitaet Duesseldorf This software is licenced under EPL 1.0
+ * (http://www.eclipse.org/org/documents/epl-v10.html)
+ * */
+
+package de.prob.units.ui;
+
+import java.util.ArrayList;
+import java.util.HashMap;
+import java.util.List;
+import java.util.Map;
+
+import org.eclipse.core.commands.AbstractHandler;
+import org.eclipse.core.commands.ExecutionEvent;
+import org.eclipse.core.commands.ExecutionException;
+import org.eclipse.core.commands.IHandler;
+import org.eclipse.core.resources.IFile;
+import org.eclipse.core.resources.IMarker;
+import org.eclipse.core.resources.IProject;
+import org.eclipse.core.resources.IResource;
+import org.eclipse.core.resources.IResourceChangeEvent;
+import org.eclipse.core.resources.IResourceChangeListener;
+import org.eclipse.core.resources.IResourceDelta;
+import org.eclipse.core.resources.ResourcesPlugin;
+import org.eclipse.core.runtime.CoreException;
+import org.eclipse.core.runtime.IPath;
+import org.eclipse.core.runtime.NullProgressMonitor;
+import org.eclipse.jface.action.IAction;
+import org.eclipse.jface.viewers.ISelection;
+import org.eclipse.jface.viewers.IStructuredSelection;
+import org.eclipse.ui.handlers.HandlerUtil;
+import org.eventb.core.IConstant;
+import org.eventb.core.IContextRoot;
+import org.eventb.core.IEventBRoot;
+import org.eventb.core.IMachineRoot;
+import org.eventb.core.IVariable;
+import org.rodinp.core.IRodinFile;
+import org.rodinp.core.RodinCore;
+import org.rodinp.core.RodinDBException;
+
+import de.prob.core.Animator;
+import de.prob.core.LimitedLogger;
+import de.prob.core.command.ActivateUnitPluginCommand;
+import de.prob.core.command.ClearMachineCommand;
+import de.prob.core.command.CommandException;
+import de.prob.core.command.ComposedCommand;
+import de.prob.core.command.GetPluginResultCommand;
+import de.prob.core.command.SetPreferencesCommand;
+import de.prob.core.command.StartAnimationCommand;
+import de.prob.core.command.internal.InternalLoadCommand;
+import de.prob.exceptions.ProBException;
+import de.prob.logging.Logger;
+import de.prob.parser.BindingGenerator;
+import de.prob.parser.ResultParserException;
+import de.prob.prolog.term.CompoundPrologTerm;
+import de.prob.prolog.term.ListPrologTerm;
+import de.prob.prolog.term.PrologTerm;
+import de.prob.units.pragmas.InferredUnitPragmaAttribute;
+
+public class StartUnitAnalysisHandler extends AbstractHandler implements
+ IHandler {
+
+ public static class ModificationListener implements IResourceChangeListener {
+
+ private final IPath path;
+
+ public ModificationListener(final IFile resource) {
+ if (resource == null) {
+ path = null;
+ } else {
+ this.path = resource.getProject().getFullPath();
+ }
+ }
+
+ public void resourceChanged(final IResourceChangeEvent event) {
+ if (path != null) {
+ final IResourceDelta delta = event.getDelta();
+ IResourceDelta member = delta.findMember(path);
+ if (member != null) {
+ Animator.getAnimator().setDirty();
+ }
+ }
+ }
+ }
+
+ private ISelection fSelection;
+ private ModificationListener listener;
+
+ public Object execute(final ExecutionEvent event) throws ExecutionException {
+
+ fSelection = HandlerUtil.getCurrentSelection(event);
+
+ // Get the Selection
+ final IEventBRoot rootElement = getRootElement();
+ final IFile resource = extractResource(rootElement);
+
+ ArrayList<String> errors = new ArrayList<String>();
+ boolean realError = checkErrorMarkers(resource, errors);
+ if (!errors.isEmpty()) {
+ String message = "Some components in your project contain "
+ + (realError ? "errors" : "warnings")
+ + ". This can lead to unexpected behavior (e.g. missing variables) when animating.\n\nDetails:\n";
+ StringBuffer stringBuffer = new StringBuffer(message);
+ for (String string : errors) {
+ stringBuffer.append(string);
+ stringBuffer.append('\n');
+ }
+ if (realError)
+ Logger.notifyUserWithoutBugreport(stringBuffer.toString());
+ else
+ Logger.notifyUserAboutWarningWithoutBugreport(stringBuffer
+ .toString());
+ }
+ ;
+
+ if (resource != null) {
+ LimitedLogger.getLogger().log("user started unit analysis",
+ rootElement.getElementName(), null);
+ registerModificationListener(resource);
+
+ final Animator animator = Animator.getAnimator();
+ try {
+ // load machine and activate plugin
+ final ClearMachineCommand clear = new ClearMachineCommand();
+ final SetPreferencesCommand setPrefs = SetPreferencesCommand
+ .createSetPreferencesCommand(animator);
+ final InternalLoadCommand load = new InternalLoadCommand(
+ rootElement);
+ final StartAnimationCommand start = new StartAnimationCommand();
+ final ActivateUnitPluginCommand activatePlugin = new ActivateUnitPluginCommand();
+
+ final ComposedCommand composed = new ComposedCommand(clear,
+ setPrefs, load, start, activatePlugin);
+
+ animator.execute(composed);
+
+ GetPluginResultCommand pluginResultCommand = new GetPluginResultCommand(
+ "Grounded Result State");
+
+ animator.execute(pluginResultCommand);
+
+ processResults(pluginResultCommand.getResult());
+ } catch (ProBException e) {
+ e.notifyUserOnce();
+ throw new ExecutionException("Unit Analysis Failed", e);
+ } catch (RodinDBException e) {
+ throw new ExecutionException(
+ "Unit Analysis Failed with a RodinDBException", e);
+ }
+ }
+ return null;
+ }
+
+ private boolean checkErrorMarkers(final IFile resource, List<String> errors) {
+ boolean result = false;
+ IProject project = resource.getProject();
+ try {
+ IMarker[] markers = project.findMarkers(
+ "org.eclipse.core.resources.problemmarker", true,
+ IResource.DEPTH_INFINITE);
+ for (IMarker iMarker : markers) {
+ errors.add(iMarker.getResource().getName()
+ + ": "
+ + iMarker
+ .getAttribute(IMarker.MESSAGE, "unknown Error"));
+ result = result
+ || (Integer) iMarker.getAttribute(IMarker.SEVERITY) == IMarker.SEVERITY_ERROR;
+ }
+
+ } catch (CoreException e1) {
+ }
+ return result;
+ }
+
+ private void processResults(ListPrologTerm result) throws RodinDBException,
+ ExecutionException {
+ // preprocess the list into a map
+ Map<String, String> variables = new HashMap<String, String>();
+ for (PrologTerm term : result) {
+ CompoundPrologTerm compoundTerm;
+ try {
+ compoundTerm = BindingGenerator
+ .getCompoundTerm(term, "bind", 2);
+
+ variables.put(
+ PrologTerm.atomicString(compoundTerm.getArgument(1)),
+ PrologTerm.atomicString(compoundTerm.getArgument(2)));
+ } catch (ResultParserException e) {
+ CommandException commandException = new CommandException(
+ e.getLocalizedMessage(), e);
+ commandException.notifyUserOnce();
+ }
+ }
+
+ IEventBRoot rootElement = getRootElement();
+ // look up the variables / constants of the selected machine in
+ // the state
+ // and set the inferredUnitPragma attribute
+ if (rootElement instanceof IMachineRoot) {
+ // find and update variables
+ IVariable[] allVariables = rootElement.getMachineRoot()
+ .getVariables();
+
+ for (IVariable var : allVariables) {
+ String variableName = var.getIdentifierString();
+ if (variables.containsKey(variableName)) {
+ var.setAttributeValue(
+ InferredUnitPragmaAttribute.ATTRIBUTE,
+ variables.get(variableName),
+ new NullProgressMonitor());
+ }
+ }
+
+ } else if (rootElement instanceof IContextRoot) {
+ // find and update constants
+ IConstant[] allConstants = rootElement.getContextRoot()
+ .getConstants();
+
+ for (IConstant var : allConstants) {
+ String constantName = var.getIdentifierString();
+ if (variables.containsKey(constantName)) {
+ var.setAttributeValue(
+ InferredUnitPragmaAttribute.ATTRIBUTE,
+ variables.get(constantName),
+ new NullProgressMonitor());
+ }
+ }
+ } else {
+ throw new ExecutionException(
+ "Cannot execute unit analysis on this element type. Type of "
+ + rootElement.getComponentName() + " was: "
+ + rootElement.getClass());
+ }
+ }
+
+ private IEventBRoot getRootElement() {
+ IEventBRoot root = null;
+ if (fSelection instanceof IStructuredSelection) {
+ final IStructuredSelection ssel = (IStructuredSelection) fSelection;
+ if (ssel.size() == 1) {
+ final Object element = ssel.getFirstElement();
+ if (element instanceof IEventBRoot) {
+ root = (IEventBRoot) element;
+ } else if (element instanceof IFile) {
+ IRodinFile rodinFile = RodinCore.valueOf((IFile) element);
+ if (rodinFile != null)
+ root = (IEventBRoot) rodinFile.getRoot();
+ }
+ }
+ }
+ return root;
+ }
+
+ private IFile extractResource(final IEventBRoot rootElement) {
+ IFile resource = null;
+ if (rootElement == null) {
+ resource = null;
+ } else if (rootElement instanceof IMachineRoot) {
+ resource = ((IMachineRoot) rootElement).getSCMachineRoot()
+ .getResource();
+ } else if (rootElement instanceof IContextRoot) {
+ resource = ((IContextRoot) rootElement).getSCContextRoot()
+ .getResource();
+ }
+ return resource;
+ }
+
+ private void registerModificationListener(final IFile resource) {
+ if (listener != null) {
+ ResourcesPlugin.getWorkspace().removeResourceChangeListener(
+ listener);
+ }
+ listener = new ModificationListener(resource);
+ ResourcesPlugin.getWorkspace().addResourceChangeListener(listener);
+ }
+
+ public void selectionChanged(final IAction action,
+ final ISelection selection) {
+ fSelection = selection;
+ }
+
+}
diff --git a/de.prob2.units.feature/.project b/de.prob2.units.feature/.project
new file mode 100644
index 0000000000000000000000000000000000000000..96b7c78653fba0643a8efc26c06b6a3f61c66bd7
--- /dev/null
+++ b/de.prob2.units.feature/.project
@@ -0,0 +1,17 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<projectDescription>
+ <name>de.prob2.units.feature</name>
+ <comment></comment>
+ <projects>
+ </projects>
+ <buildSpec>
+ <buildCommand>
+ <name>org.eclipse.pde.FeatureBuilder</name>
+ <arguments>
+ </arguments>
+ </buildCommand>
+ </buildSpec>
+ <natures>
+ <nature>org.eclipse.pde.FeatureNature</nature>
+ </natures>
+</projectDescription>
diff --git a/de.prob2.units.feature/.settings/org.eclipse.core.resources.prefs b/de.prob2.units.feature/.settings/org.eclipse.core.resources.prefs
new file mode 100644
index 0000000000000000000000000000000000000000..ae8dfb5865c1107f8366e1e8c2af6ad2d1a7a9f1
--- /dev/null
+++ b/de.prob2.units.feature/.settings/org.eclipse.core.resources.prefs
@@ -0,0 +1,3 @@
+#Tue Nov 29 16:17:25 CET 2011
+eclipse.preferences.version=1
+encoding/<project>=UTF-8
diff --git a/de.prob2.units.feature/.settings/org.eclipse.core.runtime.prefs b/de.prob2.units.feature/.settings/org.eclipse.core.runtime.prefs
new file mode 100644
index 0000000000000000000000000000000000000000..57a8ae0b2a629cab658cebb8c79bd02f33f25fb0
--- /dev/null
+++ b/de.prob2.units.feature/.settings/org.eclipse.core.runtime.prefs
@@ -0,0 +1,3 @@
+#Tue Nov 29 16:17:25 CET 2011
+eclipse.preferences.version=1
+line.separator=\n
diff --git a/de.prob2.units.feature/build.properties b/de.prob2.units.feature/build.properties
new file mode 100644
index 0000000000000000000000000000000000000000..64f93a9f0b7328eb563aa5ad6cec7f828020e124
--- /dev/null
+++ b/de.prob2.units.feature/build.properties
@@ -0,0 +1 @@
+bin.includes = feature.xml
diff --git a/de.prob2.units.feature/feature.xml b/de.prob2.units.feature/feature.xml
new file mode 100644
index 0000000000000000000000000000000000000000..e6432b794d0c846138eb1b6eaf1315ba8303f26b
--- /dev/null
+++ b/de.prob2.units.feature/feature.xml
@@ -0,0 +1,281 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<feature
+ id="de.prob2.units.feature"
+ label="ProB for Rodin2 - Physical Units Support"
+ version="2.3.5.qualifier"
+ provider-name="HHU Düsseldorf STUPS Group">
+
+ <description url="http://www.stups.uni-duesseldorf.de/ProB">
+ ProB is an animator and model checker for the B-Method. It allows fully automatic animation of many B specifications, and can be used to systematically check a specification for errors.
+Part of the research and development was conducted within the EPSRC funded projects ABCD and iMoc, and within the EU funded project Rodin.
+Development is continued under the EU funded project Deploy and the DFG project Gepavas.
+ProB has been successfully used on various industrial specifications and is now being used within Siemens.
+ </description>
+
+ <copyright>
+ (C) 2000-2011 Michael Leuschel (and many others) All rights reserved.
+ </copyright>
+
+ <license url="http://www.eclipse.org/org/documents/epl-v10.html">
+ ProB can be used freely for commercial, non-commercial and academic
+use under the Eclipse Public Licence v. 1.0. (below)
+For availability of commercial support, please contact the author
+(http://www.stups.uni-duesseldorf.de/~leuschel).
+Use of ProB's nauty library for symmetry reduction implies further
+restrictions (no applications with nontrivial military significance,
+see http://cs.anu.edu.au/~bdm/nauty/).
+---
+Eclipse Public License - v. 1.0
+THE ACCOMPANYING PROGRAM IS PROVIDED UNDER THE TERMS OF THIS
+ECLIPSE PUBLIC LICENSE ("AGREEMENT"). ANY USE, REPRODUCTION OR
+DISTRIBUTION OF THE PROGRAM CONSTITUTES RECIPIENT'S ACCEPTANCE
+OF THIS AGREEMENT.
+1. DEFINITIONS
+"Contribution" means:
+a) in the case of the initial Contributor, the initial code and
+documentation distributed under this Agreement, and
+b) in the case of each subsequent Contributor:
+i) changes to the Program, and
+ii) additions to the Program;
+where such changes and/or additions to the Program originate
+from and are distributed by that particular Contributor. A Contribution
+'originates' from a Contributor if it was added to the Program
+by such Contributor itself or anyone acting on such Contributor's
+behalf. Contributions do not include additions to the Program
+which: (i) are separate modules of software distributed in conjunction
+with the Program under their own license agreement, and (ii)
+are not derivative works of the Program.
+"Contributor" means any person or entity that distributes the
+Program.
+"Licensed Patents" mean patent claims licensable by a Contributor
+which are necessarily infringed by the use or sale of its Contribution
+alone or when combined with the Program.
+"Program" means the Contributions distributed in accordance with
+this Agreement.
+"Recipient" means anyone who receives the Program under this
+Agreement, including all Contributors.
+2. GRANT OF RIGHTS
+a) Subject to the terms of this Agreement, each Contributor hereby
+grants Recipient a non-exclusive, worldwide, royalty-free copyright
+license to reproduce, prepare derivative works of, publicly display,
+publicly perform, distribute and sublicense the Contribution
+of such Contributor, if any, and such derivative works, in source
+code and object code form.
+b) Subject to the terms of this Agreement, each Contributor hereby
+grants Recipient a non-exclusive, worldwide, royalty-free patent
+license under Licensed Patents to make, use, sell, offer to sell,
+import and otherwise transfer the Contribution of such Contributor,
+if any, in source code and object code form. This patent license
+shall apply to the combination of the Contribution and the Program
+if, at the time the Contribution is added by the Contributor,
+such addition of the Contribution causes such combination to
+be covered by the Licensed Patents. The patent license shall
+not apply to any other combinations which include the Contribution.
+No hardware per se is licensed hereunder.
+c) Recipient understands that although each Contributor grants
+the licenses to its Contributions set forth herein, no assurances
+are provided by any Contributor that the Program does not infringe
+the patent or other intellectual property rights of any other
+entity. Each Contributor disclaims any liability to Recipient
+for claims brought by any other entity based on infringement
+of intellectual property rights or otherwise. As a condition
+to exercising the rights and licenses granted hereunder, each
+Recipient hereby assumes sole responsibility to secure any other
+intellectual property rights needed, if any. For example, if
+a third party patent license is required to allow Recipient to
+distribute the Program, it is Recipient's responsibility to acquire
+that license before distributing the Program.
+d) Each Contributor represents that to its knowledge it has sufficient
+copyright rights in its Contribution, if any, to grant the copyright
+license set forth in this Agreement.
+3. REQUIREMENTS
+A Contributor may choose to distribute the Program in object
+code form under its own license agreement, provided that:
+a) it complies with the terms and conditions of this Agreement;
+and
+b) its license agreement:
+i) effectively disclaims on behalf of all Contributors all warranties
+and conditions, express and implied, including warranties or
+conditions of title and non-infringement, and implied warranties
+or conditions of merchantability and fitness for a particular
+purpose;
+ii) effectively excludes on behalf of all Contributors all liability
+for damages, including direct, indirect, special, incidental
+and consequential damages, such as lost profits;
+iii) states that any provisions which differ from this Agreement
+are offered by that Contributor alone and not by any other party;
+and
+iv) states that source code for the Program is available from
+such Contributor, and informs licensees how to obtain it in a
+reasonable manner on or through a medium customarily used for
+software exchange.
+When the Program is made available in source code form:
+a) it must be made available under this Agreement; and
+b) a copy of this Agreement must be included with each copy of
+the Program.
+Contributors may not remove or alter any copyright notices contained
+within the Program.
+Each Contributor must identify itself as the originator of its
+Contribution, if any, in a manner that reasonably allows subsequent
+Recipients to identify the originator of the Contribution.
+4. COMMERCIAL DISTRIBUTION
+Commercial distributors of software may accept certain responsibilities
+with respect to end users, business partners and the like. While
+this license is intended to facilitate the commercial use of
+the Program, the Contributor who includes the Program in a commercial
+product offering should do so in a manner which does not create
+potential liability for other Contributors. Therefore, if a Contributor
+includes the Program in a commercial product offering, such Contributor
+("Commercial Contributor") hereby agrees to defend and indemnify
+every other Contributor ("Indemnified Contributor") against any
+losses, damages and costs (collectively "Losses") arising from
+claims, lawsuits and other legal actions brought by a third party
+against the Indemnified Contributor to the extent caused by the
+acts or omissions of such Commercial Contributor in connection
+with its distribution of the Program in a commercial product
+offering. The obligations in this section do not apply to any
+claims or Losses relating to any actual or alleged intellectual
+property infringement. In order to qualify, an Indemnified Contributor
+must: a) promptly notify the Commercial Contributor in writing
+of such claim, and b) allow the Commercial Contributor to control,
+and cooperate with the Commercial Contributor in, the defense
+and any related settlement negotiations. The Indemnified Contributor
+may participate in any such claim at its own expense.
+For example, a Contributor might include the Program in a commercial
+product offering, Product X. That Contributor is then a Commercial
+Contributor. If that Commercial Contributor then makes performance
+claims, or offers warranties related to Product X, those performance
+claims and warranties are such Commercial Contributor's responsibility
+alone. Under this section, the Commercial Contributor would have
+to defend claims against the other Contributors related to those
+performance claims and warranties, and if a court requires any
+other Contributor to pay any damages as a result, the Commercial
+Contributor must pay those damages.
+5. NO WARRANTY
+EXCEPT AS EXPRESSLY SET FORTH IN THIS AGREEMENT, THE PROGRAM
+IS PROVIDED ON AN "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS
+OF ANY KIND, EITHER EXPRESS OR IMPLIED INCLUDING, WITHOUT LIMITATION,
+ANY WARRANTIES OR CONDITIONS OF TITLE, NON-INFRINGEMENT, MERCHANTABILITY
+OR FITNESS FOR A PARTICULAR PURPOSE. Each Recipient is solely
+responsible for determining the appropriateness of using and
+distributing the Program and assumes all risks associated with
+its exercise of rights under this Agreement , including but not
+limited to the risks and costs of program errors, compliance
+with applicable laws, damage to or loss of data, programs or
+equipment, and unavailability or interruption of operations.
+6. DISCLAIMER OF LIABILITY
+EXCEPT AS EXPRESSLY SET FORTH IN THIS AGREEMENT, NEITHER RECIPIENT
+NOR ANY CONTRIBUTORS SHALL HAVE ANY LIABILITY FOR ANY DIRECT,
+INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES
+(INCLUDING WITHOUT LIMITATION LOST PROFITS), HOWEVER CAUSED AND
+ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,
+OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY
+OUT OF THE USE OR DISTRIBUTION OF THE PROGRAM OR THE EXERCISE
+OF ANY RIGHTS GRANTED HEREUNDER, EVEN IF ADVISED OF THE POSSIBILITY
+OF SUCH DAMAGES.
+7. GENERAL
+If any provision of this Agreement is invalid or unenforceable
+under applicable law, it shall not affect the validity or enforceability
+of the remainder of the terms of this Agreement, and without
+further action by the parties hereto, such provision shall be
+reformed to the minimum extent necessary to make such provision
+valid and enforceable.
+If Recipient institutes patent litigation against any entity
+(including a cross-claim or counterclaim in a lawsuit) alleging
+that the Program itself (excluding combinations of the Program
+with other software or hardware) infringes such Recipient's patent(s),
+then such Recipient's rights granted under Section 2(b) shall
+terminate as of the date such litigation is filed.
+All Recipient's rights under this Agreement shall terminate if
+it fails to comply with any of the material terms or conditions
+of this Agreement and does not cure such failure in a reasonable
+period of time after becoming aware of such noncompliance. If
+all Recipient's rights under this Agreement terminate, Recipient
+agrees to cease use and distribution of the Program as soon as
+reasonably practicable. However, Recipient's obligations under
+this Agreement and any licenses granted by Recipient relating
+to the Program shall continue and survive.
+Everyone is permitted to copy and distribute copies of this Agreement,
+but in order to avoid inconsistency the Agreement is copyrighted
+and may only be modified in the following manner. The Agreement
+Steward reserves the right to publish new versions (including
+revisions) of this Agreement from time to time. No one other
+than the Agreement Steward has the right to modify this Agreement.
+The Eclipse Foundation is the initial Agreement Steward. The
+Eclipse Foundation may assign the responsibility to serve as
+the Agreement Steward to a suitable separate entity. Each new
+version of the Agreement will be given a distinguishing version
+number. The Program (including Contributions) may always be distributed
+subject to the version of the Agreement under which it was received.
+In addition, after a new version of the Agreement is published,
+Contributor may elect to distribute the Program (including its
+Contributions) under the new version. Except as expressly stated
+in Sections 2(a) and 2(b) above, Recipient receives no rights
+or licenses to the intellectual property of any Contributor under
+this Agreement, whether expressly, by implication, estoppel or
+otherwise. All rights in the Program not expressly granted under
+this Agreement are reserved.
+This Agreement is governed by the laws of the State of New York
+and the intellectual property laws of the United States of America.
+No party to this Agreement will bring a legal action under this
+Agreement more than one year after the cause of action arose.
+Each party waives its rights to a jury trial in any resulting
+litigation.
+ </license>
+
+ <requires>
+ <import plugin="org.eclipse.ui" version="3.5.0" match="compatible"/>
+ <import plugin="org.eclipse.ui.ide" version="3.5.0" match="compatible"/>
+ <import plugin="org.eclipse.ui.views" version="3.5.0" match="compatible"/>
+ <import plugin="org.eclipse.core.runtime" version="3.5.0" match="compatible"/>
+ <import plugin="org.eclipse.core.databinding" version="1.2.0" match="compatible"/>
+ <import plugin="org.eclipse.jface.databinding" version="1.2.1" match="compatible"/>
+ <import plugin="org.eclipse.core.databinding.beans" version="1.1.1" match="compatible"/>
+ <import plugin="org.eclipse.gef" version="3.7.0" match="compatible"/>
+ <import plugin="de.prob.core" version="9.3.0" match="equivalent"/>
+ <import plugin="org.eventb.core" version="2.1.0"/>
+ <import plugin="org.rodinp.core" version="1.3.1"/>
+ <import plugin="de.prob.ui" version="7.3.0" match="equivalent"/>
+ <import plugin="org.eclipse.core.resources" version="3.5.0" match="compatible"/>
+ <import plugin="org.eclipse.core.expressions" version="3.4.101" match="compatible"/>
+ <import plugin="org.eclipse.gef" version="3.5.0" match="compatible"/>
+ <import plugin="org.eclipse.ui.navigator" version="3.5.0" match="greaterOrEqual"/>
+ </requires>
+
+ <plugin
+ id="de.bmotionstudio.gef.editor"
+ download-size="0"
+ install-size="0"
+ version="0.0.0"
+ unpack="false"/>
+
+ <plugin
+ id="de.prob.core"
+ download-size="0"
+ install-size="0"
+ version="0.0.0"/>
+
+ <plugin
+ id="de.prob.plugin"
+ download-size="0"
+ install-size="0"
+ version="0.0.0"
+ fragment="true"
+ unpack="false"/>
+
+ <plugin
+ id="de.prob.ui"
+ download-size="0"
+ install-size="0"
+ version="0.0.0"
+ unpack="false"/>
+
+ <plugin
+ id="de.bmotionstudio.rodin"
+ download-size="0"
+ install-size="0"
+ version="0.0.0"
+ fragment="true"
+ unpack="false"/>
+
+</feature>
diff --git a/settings.gradle b/settings.gradle
index bb2187c38344f1fac923b7dee971552ee4cdd523..b488c61bc8301f8a4a686f9ad23d2b6109f7d62a 100644
--- a/settings.gradle
+++ b/settings.gradle
@@ -1,2 +1,2 @@
-include 'de.prob.core', 'de.bmotionstudio.gef.editor' ,'de.bmotionstudio.rodin', 'de.bmotionstudio.help' , 'de.prob.plugin', 'de.prob.ui', 'de.prob2.feature'
+include 'de.prob.core', 'de.bmotionstudio.gef.editor' ,'de.bmotionstudio.rodin', 'de.bmotionstudio.help' , 'de.prob.plugin', 'de.prob.ui', 'de.prob2.feature', 'de.prob.units', 'de.prob2.units.feature'