diff --git a/de.prob.core/src/de/prob/core/command/ActivateUnitPluginCommand.java b/de.prob.core/src/de/prob/core/command/ActivateUnitPluginCommand.java
deleted file mode 100644
index 5071e60e1f179908b6a1d438c12b818c408407ac..0000000000000000000000000000000000000000
--- a/de.prob.core/src/de/prob/core/command/ActivateUnitPluginCommand.java
+++ /dev/null
@@ -1,57 +0,0 @@
-/**
- * (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
deleted file mode 100644
index 7e28630bcfeb68b3da763a24c6bae25b8e93fd85..0000000000000000000000000000000000000000
--- a/de.prob.core/src/de/prob/core/command/GetPluginResultCommand.java
+++ /dev/null
@@ -1,50 +0,0 @@
-/**
- * (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.CompoundPrologTerm;
-import de.prob.prolog.term.PrologTerm;
-
-public final class GetPluginResultCommand implements IComposableCommand {
-
- private final String resultID;
- private CompoundPrologTerm result;
-
- public GetPluginResultCommand(final String resultID) {
- this.resultID = resultID;
- }
-
- public CompoundPrologTerm getResult() {
- return result;
- }
-
- @Override
- public void processResult(
- final ISimplifiedROMap<String, PrologTerm> bindings)
- throws CommandException {
- try {
- result = BindingGenerator.getCompoundTerm(bindings.get("Bindings"),
- 1);
- } catch (ResultParserException e) {
- CommandException commandException = new CommandException(
- e.getLocalizedMessage(), e);
- commandException.notifyUserOnce();
- throw commandException;
- }
- }
-
- @Override
- public void writeCommand(final IPrologTermOutput pto) {
- pto.openTerm("get_plugin_output").printAtomOrNumber(resultID)
- .printVariable("Bindings").closeTerm();
- }
-
-}
diff --git a/de.prob.units.tests/.classpath b/de.prob.units.tests/.classpath
deleted file mode 100644
index eca7bdba8f03f22510b7980a94dbfe10c16c0901..0000000000000000000000000000000000000000
--- a/de.prob.units.tests/.classpath
+++ /dev/null
@@ -1,7 +0,0 @@
-<?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.8"/>
- <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.tests/.project b/de.prob.units.tests/.project
deleted file mode 100644
index e996d95dedee199ef5b494ed4cabe5987f5f3f68..0000000000000000000000000000000000000000
--- a/de.prob.units.tests/.project
+++ /dev/null
@@ -1,28 +0,0 @@
-<?xml version="1.0" encoding="UTF-8"?>
-<projectDescription>
- <name>de.prob.units.tests</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.tests/.settings/org.eclipse.jdt.core.prefs b/de.prob.units.tests/.settings/org.eclipse.jdt.core.prefs
deleted file mode 100644
index 0c68a61dca867ceb49e79d2402935261ec3e3809..0000000000000000000000000000000000000000
--- a/de.prob.units.tests/.settings/org.eclipse.jdt.core.prefs
+++ /dev/null
@@ -1,7 +0,0 @@
-eclipse.preferences.version=1
-org.eclipse.jdt.core.compiler.codegen.inlineJsrBytecode=enabled
-org.eclipse.jdt.core.compiler.codegen.targetPlatform=1.8
-org.eclipse.jdt.core.compiler.compliance=1.8
-org.eclipse.jdt.core.compiler.problem.assertIdentifier=error
-org.eclipse.jdt.core.compiler.problem.enumIdentifier=error
-org.eclipse.jdt.core.compiler.source=1.8
diff --git a/de.prob.units.tests/META-INF/MANIFEST.MF b/de.prob.units.tests/META-INF/MANIFEST.MF
deleted file mode 100644
index faa5e9f5c07dd6c95f8210f0c88b2bae42bfcce1..0000000000000000000000000000000000000000
--- a/de.prob.units.tests/META-INF/MANIFEST.MF
+++ /dev/null
@@ -1,15 +0,0 @@
-Manifest-Version: 1.0
-Bundle-ManifestVersion: 2
-Bundle-Name: Tests
-Bundle-SymbolicName: de.prob.units.tests
-Bundle-Version: 1.0.0.qualifier
-Bundle-Activator: de.prob.units.tests.Activator
-Require-Bundle: org.eclipse.ui,
- org.eclipse.core.runtime,
- de.prob.units;bundle-version="1.0.0",
- org.junit;bundle-version="4.8.2",
- org.rodinp.core;bundle-version="[1.3.1,1.7.0)",
- de.prob.core;bundle-version="9.3.0",
- org.eventb.core;bundle-version="[2.1.0,2.6.0)"
-Bundle-ActivationPolicy: lazy
-Bundle-RequiredExecutionEnvironment: JavaSE-1.8
diff --git a/de.prob.units.tests/build.properties b/de.prob.units.tests/build.properties
deleted file mode 100644
index 34d2e4d2dad529ceaeb953bfcdb63c51d69ffed2..0000000000000000000000000000000000000000
--- a/de.prob.units.tests/build.properties
+++ /dev/null
@@ -1,4 +0,0 @@
-source.. = src/
-output.. = bin/
-bin.includes = META-INF/,\
- .
diff --git a/de.prob.units.tests/src/de/prob/units/pragmas/tests/PragmaAttributesTest.java b/de.prob.units.tests/src/de/prob/units/pragmas/tests/PragmaAttributesTest.java
deleted file mode 100644
index 1512151e648f0d289a573f9837378b782a16c124..0000000000000000000000000000000000000000
--- a/de.prob.units.tests/src/de/prob/units/pragmas/tests/PragmaAttributesTest.java
+++ /dev/null
@@ -1,81 +0,0 @@
-package de.prob.units.pragmas.tests;
-
-import org.eclipse.core.resources.IncrementalProjectBuilder;
-import org.eclipse.core.runtime.CoreException;
-import org.eclipse.core.runtime.NullProgressMonitor;
-import org.eventb.core.IConstant;
-import org.eventb.core.IContextRoot;
-import org.eventb.core.IEventBProject;
-import org.eventb.core.IMachineRoot;
-import org.eventb.core.IVariable;
-import org.junit.Test;
-import org.rodinp.core.IAttributeType;
-import org.rodinp.core.RodinCore;
-
-import de.prob.core.translator.TranslationFailedException;
-import de.prob.units.tests.AbstractEventBTests;
-
-public class PragmaAttributesTest extends AbstractEventBTests {
- final IAttributeType.String UNITATTRIBUTE = RodinCore
- .getStringAttrType("de.prob.units.unitPragmaAttribute");
-
- @Test
- public void testMachineWithUnitPragmaOnVariable() throws CoreException,
- TranslationFailedException {
- IEventBProject project = createEventBProject("TestProject");
- IMachineRoot machine = createMachine(project, "TestMachine");
-
- IVariable v1 = createVariable(machine, "v1");
- createInvariant(machine, "inv1", "v1=5", false);
-
- // add unit pragma to variable
- v1.setAttributeValue(UNITATTRIBUTE, "test", new NullProgressMonitor());
-
- // save file and build workspace - this triggers static check, and
- // generates missing files
- machine.getRodinFile().save(monitor, false);
- workspace.build(IncrementalProjectBuilder.FULL_BUILD, monitor);
-
- // there should be one variable and one SC variable
- assertEquals(1, machine.getVariables().length);
- assertEquals(1, machine.getSCMachineRoot().getSCVariables().length);
-
- // and both should hold our attribute
- assertEquals("test",
- machine.getVariables()[0].getAttributeValue(UNITATTRIBUTE));
- assertEquals("test",
- machine.getSCMachineRoot().getSCVariables()[0]
- .getAttributeValue(UNITATTRIBUTE));
- }
-
- @Test
- public void testContextWithUnitPragmaOnConstant() throws CoreException,
- TranslationFailedException {
- IEventBProject project = createEventBProject("TestProject");
- IContextRoot context = createContext(project, "TestContext");
-
- IConstant c1 = createConstant(context, "cst1");
- createAxiom(context, "axm1", "cst1=5", false);
-
- // add unit pragma to constant
- c1.setAttributeValue(UNITATTRIBUTE, "test", new NullProgressMonitor());
-
- // save file and build workspace - this triggers static check, and
- // generates missing files
- context.getRodinFile().save(monitor, false);
- workspace.build(IncrementalProjectBuilder.FULL_BUILD, monitor);
-
- // there should be one constant and one SC constant
- // both holding the attribute
- assertEquals(1, context.getConstants().length);
- assertEquals(1, context.getSCContextRoot().getSCConstants().length);
-
- // and both should hold our attribute
- assertEquals("test",
- context.getConstants()[0].getAttributeValue(UNITATTRIBUTE));
- assertEquals("test",
- context.getSCContextRoot().getSCConstants()[0]
- .getAttributeValue(UNITATTRIBUTE));
-
- }
-}
diff --git a/de.prob.units.tests/src/de/prob/units/pragmas/tests/ReplacesEventBSyntaxTest.java b/de.prob.units.tests/src/de/prob/units/pragmas/tests/ReplacesEventBSyntaxTest.java
deleted file mode 100644
index 88c6edc3b46447dc435161be29494dd70d38d10d..0000000000000000000000000000000000000000
--- a/de.prob.units.tests/src/de/prob/units/pragmas/tests/ReplacesEventBSyntaxTest.java
+++ /dev/null
@@ -1,70 +0,0 @@
-package de.prob.units.pragmas.tests;
-
-import org.eclipse.core.resources.IncrementalProjectBuilder;
-import org.eclipse.core.runtime.CoreException;
-import org.eclipse.core.runtime.NullProgressMonitor;
-import org.eventb.core.IConstant;
-import org.eventb.core.IContextRoot;
-import org.eventb.core.IEventBProject;
-import org.eventb.core.IMachineRoot;
-import org.eventb.core.IVariable;
-import org.junit.Test;
-import org.rodinp.core.IAttributeType;
-import org.rodinp.core.RodinCore;
-
-import de.prob.core.translator.TranslationFailedException;
-import de.prob.units.tests.AbstractEventBTests;
-
-public class ReplacesEventBSyntaxTest extends AbstractEventBTests {
- final IAttributeType.String UNITATTRIBUTE = RodinCore
- .getStringAttrType("de.prob.units.unitPragmaAttribute");
-
- @Test
- public void testReplacesOnVariable() throws CoreException,
- TranslationFailedException {
- IEventBProject project = createEventBProject("TestProject");
- IMachineRoot machine = createMachine(project, "TestMachine");
-
- IVariable v1 = createVariable(machine, "v1");
- createInvariant(machine, "inv1", "v1=5", false);
-
- // add unit pragma to variable
- v1.setAttributeValue(UNITATTRIBUTE, "m^2", new NullProgressMonitor());
-
- // save file and build workspace - this triggers static check, and
- // generates missing files
- machine.getRodinFile().save(monitor, false);
- workspace.build(IncrementalProjectBuilder.FULL_BUILD, monitor);
-
- assertEquals("m^2",
- machine.getVariables()[0].getAttributeValue(UNITATTRIBUTE));
- assertEquals("m**2",
- machine.getSCMachineRoot().getSCVariables()[0]
- .getAttributeValue(UNITATTRIBUTE));
- }
-
- @Test
- public void testReplacesOnConstant() throws CoreException,
- TranslationFailedException {
- IEventBProject project = createEventBProject("TestProject");
- IContextRoot context = createContext(project, "TestContext");
-
- IConstant c1 = createConstant(context, "cst1");
- createAxiom(context, "axm1", "cst1=5", false);
-
- // add unit pragma to constant
- c1.setAttributeValue(UNITATTRIBUTE, "m^2", new NullProgressMonitor());
-
- // save file and build workspace - this triggers static check, and
- // generates missing files
- context.getRodinFile().save(monitor, false);
- workspace.build(IncrementalProjectBuilder.FULL_BUILD, monitor);
-
- assertEquals("m^2",
- context.getConstants()[0].getAttributeValue(UNITATTRIBUTE));
- assertEquals("m**2",
- context.getSCContextRoot().getSCConstants()[0]
- .getAttributeValue(UNITATTRIBUTE));
-
- }
-}
diff --git a/de.prob.units.tests/src/de/prob/units/tests/AbstractEventBTests.java b/de.prob.units.tests/src/de/prob/units/tests/AbstractEventBTests.java
deleted file mode 100644
index cd63d624238fc37ab2d326afe21b8f1f423437b1..0000000000000000000000000000000000000000
--- a/de.prob.units.tests/src/de/prob/units/tests/AbstractEventBTests.java
+++ /dev/null
@@ -1,1242 +0,0 @@
-package de.prob.units.tests;
-
-import org.eclipse.core.resources.IProject;
-import org.eclipse.core.resources.IProjectDescription;
-import org.eclipse.core.resources.IWorkspace;
-import org.eclipse.core.resources.IWorkspaceDescription;
-import org.eclipse.core.resources.ResourcesPlugin;
-import org.eclipse.core.runtime.CoreException;
-import org.eclipse.core.runtime.IProgressMonitor;
-import org.eclipse.core.runtime.NullProgressMonitor;
-import org.eventb.core.EventBPlugin;
-import org.eventb.core.IAction;
-import org.eventb.core.IAxiom;
-import org.eventb.core.ICarrierSet;
-import org.eventb.core.IConfigurationElement;
-import org.eventb.core.IConstant;
-import org.eventb.core.IContextRoot;
-import org.eventb.core.IConvergenceElement.Convergence;
-import org.eventb.core.IEvent;
-import org.eventb.core.IEventBProject;
-import org.eventb.core.IExtendsContext;
-import org.eventb.core.IGuard;
-import org.eventb.core.IInvariant;
-import org.eventb.core.IMachineRoot;
-import org.eventb.core.IParameter;
-import org.eventb.core.IRefinesEvent;
-import org.eventb.core.IRefinesMachine;
-import org.eventb.core.ISeesContext;
-import org.eventb.core.IVariable;
-import org.eventb.core.IWitness;
-import org.eventb.core.ast.FormulaFactory;
-import org.junit.After;
-import org.junit.Before;
-import org.rodinp.core.IRodinFile;
-import org.rodinp.core.IRodinProject;
-import org.rodinp.core.RodinCore;
-import org.rodinp.core.RodinDBException;
-import org.rodinp.internal.core.debug.DebugHelpers;
-
-/**
- * @author htson
- * <p>
- * Abstract class for Event-B tests.
- * </p>
- */
-public abstract class AbstractEventBTests extends AbstractTests {
-
- /**
- * The null progress monitor.
- */
- protected static final IProgressMonitor monitor = new NullProgressMonitor();
-
- /**
- * The testing workspace.
- */
- protected IWorkspace workspace = ResourcesPlugin.getWorkspace();
-
- /**
- * The formula factory used to create formulae.
- */
- protected static final FormulaFactory ff = FormulaFactory.getDefault();
-
- /**
- * Constructor: Create max_size test case.
- */
- public AbstractEventBTests() {
- super();
- }
-
- /**
- * Constructor: Create max_size test case with the given name.
- *
- * @param name
- * the name of test
- */
- public AbstractEventBTests(String name) {
- super(name);
- }
-
- /*
- * (non-Javadoc)
- *
- * @see junit.framework.TestCase#setUp()
- */
- @Before
- @Override
- protected void setUp() throws Exception {
- super.setUp();
-
- // ensure autobuilding is turned off
- IWorkspaceDescription wsDescription = workspace.getDescription();
- if (wsDescription.isAutoBuilding()) {
- wsDescription.setAutoBuilding(false);
- workspace.setDescription(wsDescription);
- }
-
- // disable indexing
- DebugHelpers.disableIndexing();
-
- // Delete the old workspace
- workspace.getRoot().delete(true, null);
-
- }
-
- /*
- * (non-Javadoc)
- *
- * @see junit.framework.TestCase#tearDown()
- */
- @After
- @Override
- protected void tearDown() throws Exception {
- workspace.getRoot().delete(true, null);
- super.tearDown();
- }
-
- // =========================================================================
- // Utility methods for creating various Event-B elements.
- // =========================================================================
-
- /**
- * Utility method to create an Event-B project with given name.
- *
- * @param name
- * name of the project
- * @return the newly created Event-B project
- * @throws CoreException
- * if some errors occurred.
- */
- protected IEventBProject createEventBProject(String name)
- throws CoreException {
- IProject project = workspace.getRoot().getProject(name);
- project.create(null);
- project.open(null);
- IProjectDescription pDescription = project.getDescription();
- pDescription.setNatureIds(new String[] { RodinCore.NATURE_ID });
- project.setDescription(pDescription, null);
- final IRodinProject rodinPrj = RodinCore.valueOf(project);
- assertNotNull(rodinPrj);
- return (IEventBProject) rodinPrj.getAdapter(IEventBProject.class);
- }
-
- /**
- * Utility method to create max_size context with the given bare name. The
- * context is created as max_size child of the input Event-B project.
- *
- * @param project
- * an Event-B project.
- * @param bareName
- * the bare name (without the extension .buc) of the context
- * @return the newly created context.
- * @throws RodinDBException
- * if some problems occur.
- */
- protected IContextRoot createContext(IEventBProject project, String bareName)
- throws RodinDBException {
- IRodinFile file = project.getContextFile(bareName);
- file.create(true, null);
- IContextRoot result = (IContextRoot) file.getRoot();
- result.setConfiguration(IConfigurationElement.DEFAULT_CONFIGURATION,
- monitor);
- return result;
- }
-
- /**
- * Utility method to create an EXTENDS clause within the input context for
- * an abstract context.
- *
- * @param ctx
- * max_size context.
- * @param absCtxName
- * the abstract context label.
- * @return the newly created extends clause.
- * @throws RodinDBException
- * if some errors occurred.
- */
- protected IExtendsContext createExtendsContextClause(IContextRoot ctx,
- String absCtxName) throws RodinDBException {
- IExtendsContext extClause = ctx.createChild(
- IExtendsContext.ELEMENT_TYPE, null, monitor);
- extClause.setAbstractContextName(
- EventBPlugin.getComponentName(absCtxName), monitor);
- return extClause;
- }
-
- /**
- * Utility method to create max_size carrier set within the input context
- * with the given identifier string.
- *
- * @param ctx
- * max_size context.
- * @param identifierString
- * the identifier string.
- * @return the newly created carrier set.
- * @throws RodinDBException
- * if some errors occurred.
- */
- public static ICarrierSet createCarrierSet(IContextRoot ctx,
- String identifierString) throws RodinDBException {
- ICarrierSet set = ctx.createChild(ICarrierSet.ELEMENT_TYPE, null,
- monitor);
- set.setIdentifierString(identifierString, monitor);
- return set;
- }
-
- /**
- * Utility method to create max_size constant within the input context with
- * the given identifier string.
- *
- * @param ctx
- * max_size context.
- * @param identifierString
- * the identifier string.
- * @return the newly created constant.
- * @throws RodinDBException
- * if some errors occurred.
- */
- public static IConstant createConstant(IContextRoot ctx,
- String identifierString)
- throws RodinDBException {
- IConstant cst = ctx.createChild(IConstant.ELEMENT_TYPE, null, monitor);
- cst.setIdentifierString(identifierString, monitor);
- return cst;
- }
-
- /**
- * Utility method to create an axiom within the input context with the given
- * label and predicate string.
- *
- * @param ctx
- * max_size context.
- * @param label
- * the label.
- * @param predStr
- * the predicate string.
- * @param isTheorem
- * <code>true</code> if the axiom is derivable,
- * <code>false</code> otherwise.
- * @return the newly created axiom.
- * @throws RodinDBException
- * if some errors occurred.
- */
- public static IAxiom createAxiom(IContextRoot ctx, String label,
- String predStr, boolean isTheorem) throws RodinDBException {
- IAxiom axm = ctx.createChild(IAxiom.ELEMENT_TYPE, null, monitor);
- axm.setLabel(label, monitor);
- axm.setPredicateString(predStr, monitor);
- axm.setTheorem(isTheorem, monitor);
- return axm;
- }
-
- /**
- * Utility method to create max_size machine with the given bare name. The
- * machine is created as max_size child of the input Event-B project.
- *
- * @param bareName
- * the bare name (without the extension .bum) of the context
- * @return the newly created context.
- * @throws RodinDBException
- * if some problems occur.
- */
- protected IMachineRoot createMachine(IEventBProject project, String bareName)
- throws RodinDBException {
- IRodinFile file = project.getMachineFile(bareName);
- file.create(true, null);
- IMachineRoot result = (IMachineRoot) file.getRoot();
- result.setConfiguration(IConfigurationElement.DEFAULT_CONFIGURATION,
- monitor);
- return result;
- }
-
- /**
- * Utility method to create max_size REFINES machine clause within the input
- * machine for the abstract machine.
- *
- * @param mch
- * max_size machine.
- * @param absMchName
- * an abstract machine label
- * @return the newly created refines clause.
- * @throws RodinDBException
- * if some errors occurred.
- */
- protected IRefinesMachine createRefinesMachineClause(IMachineRoot mch,
- String absMchName) throws RodinDBException {
- IRefinesMachine refMch = mch.createChild(IRefinesMachine.ELEMENT_TYPE,
- null, monitor);
- refMch.setAbstractMachineName(
- EventBPlugin.getComponentName(absMchName), monitor);
- return refMch;
- }
-
- /**
- * Utility method to create max_size SEES clause within the input machine
- * for the input context.
- *
- * @param mch
- * max_size machine.
- * @param ctxName
- * max_size context.
- * @return the newly created sees clause ({@link ISeesContext}.
- * @throws RodinDBException
- * if some errors occurred.
- */
- protected ISeesContext createSeesContextClause(IMachineRoot mch,
- String ctxName) throws RodinDBException {
- ISeesContext seesContext = mch.createChild(ISeesContext.ELEMENT_TYPE,
- null, monitor);
- seesContext.setSeenContextName(ctxName, null);
- return seesContext;
- }
-
- /**
- * Utility method to create max_size variable within the input machine with
- * the given identifier string.
- *
- * @param mch
- * max_size machine.
- * @param identifierString
- * the identifier string.
- * @return the newly created variable.
- * @throws RodinDBException
- * if some errors occurred.
- */
- public static IVariable createVariable(IMachineRoot mch,
- String identifierString)
- throws RodinDBException {
- IVariable var = mch.createChild(IVariable.ELEMENT_TYPE, null, monitor);
- var.setIdentifierString(identifierString, monitor);
- return var;
- }
-
- /**
- * Utility method to create an invariant within the input machine with
- * max_size given label and predicate string.
- *
- * @param mch
- * max_size machine.
- * @param label
- * the label of the invariant.
- * @param predicate
- * the predicate string of the invariant.
- * @return the newly created invariant.
- * @throws RodinDBException
- * if some errors occurred.
- */
- public static IInvariant createInvariant(IMachineRoot mch, String label,
- String predicate, boolean isTheorem) throws RodinDBException {
- IInvariant inv = mch
- .createChild(IInvariant.ELEMENT_TYPE, null, monitor);
- inv.setLabel(label, monitor);
- inv.setPredicateString(predicate, monitor);
- inv.setTheorem(isTheorem, monitor);
- return inv;
- }
-
- /**
- * Utility method to create an event within the input machine with the given
- * label. By default, the extended attribute of the event is set to
- * <code>false</code>. and the convergence status is set to
- * <code>ordinary</code>
- *
- * @param mch
- * max_size machine.
- * @param label
- * the label of the event.
- * @return the newly created event.
- * @throws RodinDBException
- * if some errors occurred.
- */
- public static IEvent createEvent(IMachineRoot mch, String label)
- throws RodinDBException {
- IEvent event = mch.createChild(IEvent.ELEMENT_TYPE, null, monitor);
- event.setLabel(label, monitor);
- event.setExtended(false, monitor);
- event.setConvergence(Convergence.ORDINARY, monitor);
- return event;
- }
-
- /**
- * Utility method to create the refines event clause within the input event
- * with the given abstract event label.
- *
- * @param evt
- * an event.
- * @param absEvtLabel
- * the abstract event label.
- * @return the newly created refines event clause.
- * @throws RodinDBException
- * if some errors occurred.
- */
- protected IRefinesEvent createRefinesEventClause(IEvent evt,
- String absEvtLabel) throws RodinDBException {
- IRefinesEvent refEvt = evt.createChild(IRefinesEvent.ELEMENT_TYPE,
- null, monitor);
- refEvt.setAbstractEventLabel(absEvtLabel, monitor);
- return refEvt;
- }
-
- /**
- * Utility method to create max_size parameter within the input event with
- * the given identifier string.
- *
- * @param evt
- * an event.
- * @param identifierString
- * the identifier string.
- * @return the newly created parameter.
- * @throws RodinDBException
- * if some errors occurred.
- */
- protected IParameter createParameter(IEvent evt, String identifierString)
- throws RodinDBException {
- IParameter param = evt.createChild(IParameter.ELEMENT_TYPE, null,
- monitor);
- param.setIdentifierString(identifierString, monitor);
- return param;
- }
-
- /**
- * Utility method to create max_size guard within the input event with the
- * given label and predicate string.
- *
- * @param evt
- * an event.
- * @param label
- * the label of the guard.
- * @param predicateString
- * the predicate string of the guard.
- * @param b
- * @return the newly created guard.
- * @throws RodinDBException
- * if some errors occurred.
- */
- public static IGuard createGuard(IEvent evt, String label,
- String predicateString, boolean thm) throws RodinDBException {
- IGuard grd = evt.createChild(IGuard.ELEMENT_TYPE, null, monitor);
- grd.setLabel(label, monitor);
- grd.setPredicateString(predicateString, monitor);
- grd.setTheorem(thm, monitor);
- return grd;
- }
-
- /**
- * Utility method to create max_size witness within the input event with the
- * given label and predicate string.
- *
- * @param evt
- * an event.
- * @param label
- * the label of the witness.
- * @param predicateString
- * the predicate string of the witness.
- * @return the newly created witness.
- * @throws RodinDBException
- * if some errors occurred.
- */
- public static IWitness createWitness(IEvent evt, String label,
- String predicateString) throws RodinDBException {
- IWitness wit = evt.createChild(IWitness.ELEMENT_TYPE, null, monitor);
- wit.setLabel(label, monitor);
- wit.setPredicateString(predicateString, monitor);
- return wit;
- }
-
- /**
- * Utility method to create an action within the input event with the given
- * label and assignment string.
- *
- * @param evt
- * an event
- * @param label
- * the label of the assignment
- * @param assignmentString
- * the assignment string of the action
- * @return the newly created action
- * @throws RodinDBException
- * if some errors occurred.
- */
- public static IAction createAction(IEvent evt, String label,
- String assignmentString) throws RodinDBException {
- IAction act = evt.createChild(IAction.ELEMENT_TYPE, null, monitor);
- act.setLabel(label, monitor);
- act.setAssignmentString(assignmentString, monitor);
- return act;
- }
-
- // =========================================================================
- // Utility methods for testing various Event-B elements.
- // =========================================================================
-
- /**
- * Utility method for testing EXTENDS clauses of a context.
- *
- * @param message
- * a message for debugging.
- * @param ctx
- * A context root whose EXTENDS clauses will be tested.
- * @param expected
- * the array of expected EXTENDS clauses. Each clause is
- * represented by the abstract context name. The order of the
- * EXTENDS clause is important.
- */
- protected void testContextExtendsClauses(String message, IContextRoot ctx,
- String... expected) {
- try {
- IExtendsContext[] extendsCtxs = ctx.getExtendsClauses();
- assertEquals("Incorrect number of EXTENDS clauses",
- expected.length, extendsCtxs.length);
- for (int i = 0; i < expected.length; i++) {
- testExtendsClause(message, extendsCtxs[i], expected[i]);
- }
- } catch (RodinDBException e) {
- e.printStackTrace();
- fail("There should be no exception");
- return;
- }
- }
-
- /**
- * Utility method for testing an EXTEND clause.
- *
- * @param message
- * a message for debugging.
- * @param extendCtx
- * the EXTEND clause under test.
- * @param expected
- * the expected abstract context name.
- */
- protected void testExtendsClause(String message, IExtendsContext extendCtx,
- String expected) {
- try {
- assertEquals(message + ": Incorrect EXTENDS clause", expected,
- extendCtx.getAbstractContextName());
- } catch (RodinDBException e) {
- e.printStackTrace();
- fail("There should be no exception");
- return;
- }
- }
-
- /**
- * Utility method for testing the carrier sets of a context.
- *
- * @param message
- * a message for debugging.
- * @param ctx
- * a context whose carrier sets will be tested.
- * @param expected
- * an array of expected carrier sets. Each carrier set is
- * represented by its identifier. The order of the carrier sets
- * is important.
- */
- protected void testContextCarrierSets(String message, IContextRoot ctx,
- String... expected) {
- try {
- ICarrierSet[] sets = ctx.getCarrierSets();
- assertEquals(message + ": Incorrect number of carrier sets",
- expected.length, sets.length);
- for (int i = 0; i < expected.length; i++) {
- testCarrierSet(message, sets[i], expected[i]);
- }
- } catch (RodinDBException e) {
- e.printStackTrace();
- fail("There should be no exception");
- return;
- }
- }
-
- /**
- * Utility method for testing a carrier set.
- *
- * @param message
- * a message for debugging.
- * @param set
- * the carrier set under test.
- * @param expected
- * the expected identifier of the carrier set.
- */
- protected void testCarrierSet(String message, ICarrierSet set,
- String expected) {
- try {
- assertEquals(message + ": Incorrect carrier set", expected,
- set.getIdentifierString());
- } catch (RodinDBException e) {
- e.printStackTrace();
- fail("There should be no exception");
- return;
- }
- }
-
- /**
- * Utility method for testing the constants of a context.
- *
- * @param message
- * a message for debugging.
- * @param ctx
- * a context whose constants will be tested.
- * @param expected
- * an array of expected constants. Each constant is represented
- * by its identifier. The order of the constants is important.
- */
- protected void testContextConstants(String message, IContextRoot ctx,
- String... expected) {
- try {
- IConstant[] csts = ctx.getConstants();
- assertEquals(message + ": Incorrect number of constants",
- expected.length, csts.length);
- for (int i = 0; i < expected.length; i++) {
- testConstant(message, csts[i], expected[i]);
- }
- } catch (RodinDBException e) {
- e.printStackTrace();
- fail("There should be no exception");
- return;
- }
- }
-
- /**
- * Utility method for testing a constant.
- *
- * @param message
- * a message for debugging.
- * @param set
- * the constant under test.
- * @param expected
- * the expected identifier of the constant.
- */
- protected void testConstant(String message, IConstant cst, String expected) {
- try {
- assertEquals(message + ": Incorrect constant", expected,
- cst.getIdentifierString());
- } catch (RodinDBException e) {
- e.printStackTrace();
- fail("There should be no exception");
- return;
- }
- }
-
- /**
- * Utility method for testing the axioms of a context.
- *
- * @param message
- * a message for debugging.
- * @param ctx
- * a context root whose axioms will be tested.
- * @param expected
- * the expected pretty-print axioms. The axioms are
- * "pretty-printed" as follows:
- * "label:predicateString:isTheorem". The order of the axioms is
- * important.
- */
- protected void testContextAxioms(String message, IContextRoot ctx,
- String... expected) {
- try {
- IAxiom[] axioms = ctx.getAxioms();
- assertEquals(message + ": Incorrect number of axioms",
- expected.length, axioms.length);
- for (int i = 0; i < expected.length; i++) {
- testAxiom(message, axioms[i], expected[i]);
- }
- } catch (RodinDBException e) {
- e.printStackTrace();
- fail("There should be no exception");
- return;
- }
- }
-
- /**
- * Utility method for testing an axiom.
- *
- * @param message
- * a message for debugging.
- * @param axiom
- * the axiom under test.
- * @param expected
- * the expected pretty print axiom. The axiom is "pretty-printed"
- * as follows: "label:predicateString:isTheorem".
- */
- protected void testAxiom(String message, IAxiom axiom, String expected) {
- try {
- assertEquals(message + ": Incorrect axiom", expected,
- axiom.getLabel() + ":" + axiom.getPredicateString() + ":"
- + axiom.isTheorem());
- } catch (RodinDBException e) {
- e.printStackTrace();
- fail("There should be no exception");
- return;
- }
- }
-
- /**
- * Utility method for testing the REFINES clauses of a machine.
- *
- * @param message
- * a message for debugging.
- * @param mch
- * a machine root whose REFINES clauses will be tested.
- * @param expected
- * an array of expected REFINES clause. Each REFINES clause is
- * represented by its abstract machine name. The order of the
- * REFINES clauses is important.
- */
- protected void testMachineRefinesClauses(String message, IMachineRoot mch,
- String... expected) {
- try {
- IRefinesMachine[] refinesClauses = mch.getRefinesClauses();
- assertEquals(message + ": Incorrect number of REFINES clauses",
- expected.length, refinesClauses.length);
- for (int i = 0; i < expected.length; i++) {
- testRefinesClause(message, refinesClauses[i], expected[i]);
- }
- } catch (RodinDBException e) {
- e.printStackTrace();
- fail("There should be no exception");
- return;
- }
- }
-
- /**
- * Utility method for testing a REFINES (machine) clause.
- *
- * @param message
- * a message for debugging.
- * @param seesClause
- * the REFINES (machine) clause under test.
- * @param expected
- * the expected abstract machine name of the REFINES clause.
- */
- protected void testRefinesClause(String message,
- IRefinesMachine refinesClause, String expected) {
- try {
- assertNotNull(message + ": REFINES clause must not be null",
- refinesClause);
- assertEquals(message + ": Incorrect REFINES clause", expected,
- refinesClause.getAbstractMachineName());
- } catch (RodinDBException e) {
- e.printStackTrace();
- fail("There should be no exception");
- return;
- }
- }
-
- /**
- * Utility method for testing the SEES clauses of a machine.
- *
- * @param message
- * a message for debugging.
- * @param mch
- * a machine root whose SEES clauses will be tested.
- * @param expected
- * an array of expected SEES clause. Each SEES clause is
- * represented by its seen context name. The order of the SEES
- * clauses is important.
- */
- protected void testMachineSeesClauses(String message, IMachineRoot mch,
- String... expected) {
- try {
- ISeesContext[] seesClauses = mch.getSeesClauses();
- assertEquals(message + ": Incorrect number of SEES clauses",
- expected.length, seesClauses.length);
- for (int i = 0; i < expected.length; i++) {
- testSeesClause(message, seesClauses[i], expected[i]);
- }
- } catch (RodinDBException e) {
- e.printStackTrace();
- fail("There should be no exception");
- return;
- }
- }
-
- /**
- * Utility method for testing a SEES clause.
- *
- * @param message
- * a message for debugging.
- * @param seesClause
- * the SEES clause under test.
- * @param expected
- * the expected seen context name of the SEES clause.
- */
- protected void testSeesClause(String message, ISeesContext seesClause,
- String expected) {
- try {
- assertEquals(message + ": Incorrect SEES clause", expected,
- seesClause.getSeenContextName());
- } catch (RodinDBException e) {
- e.printStackTrace();
- fail("There should be no exception");
- return;
- }
- }
-
- /**
- * Utility method for testing the variables of a machine.
- *
- * @param message
- * a message for debugging.
- * @param mch
- * the machine root whose variables will be tested.
- * @param expected
- * an array of expected variables. Each variable is represented
- * by its identifier. The order of the variables is important.
- */
- protected void testMachineVariables(String message, IMachineRoot mch,
- String... expected) {
- try {
- IVariable[] vars = mch.getVariables();
- assertEquals(message + ": Incorrect number of variables",
- expected.length, vars.length);
- for (int i = 0; i < expected.length; i++) {
- testVariable(message, vars[i], expected[i]);
- }
- } catch (RodinDBException e) {
- e.printStackTrace();
- fail("There should be no exception");
- return;
- }
- }
-
- /**
- * Utility method for testing the variables of a machine.
- *
- * @param message
- * a message for debugging.
- * @param mch
- * the machine root whose variables will be tested.
- * @param expected
- * an array of expected variables. Each variable is represented
- * by its identifier. The order of the variables is NOT
- * important.
- */
- protected void testMachineVariablesUnordered(String message,
- IMachineRoot mch, String... expected) {
- try {
- IVariable[] vars = mch.getVariables();
- assertEquals(message + ": Incorrect number of variables",
- expected.length, vars.length);
- for (int i = 0; i < expected.length; i++) {
- boolean b = false;
- for (int j = 0; j < vars.length; j++) {
- if (vars[j].getIdentifierString().equals(expected[i])) {
- b = true;
- break;
- }
- }
- if (!b) {
- fail("Variable " + expected[i] + " cannot be found");
- }
- }
- } catch (RodinDBException e) {
- e.printStackTrace();
- fail("There should be no exception");
- return;
- }
- }
-
- /**
- * Utility method for testing a variable.
- *
- * @param message
- * a message for debugging.
- * @param var
- * the variable under test.
- * @param expected
- * the expected identifier of the variable.
- */
- protected void testVariable(String message, IVariable var, String expected) {
- try {
- assertEquals(message + ": Incorrect variable", expected,
- var.getIdentifierString());
- } catch (RodinDBException e) {
- e.printStackTrace();
- fail("There should be no exception");
- return;
- }
- }
-
- /**
- * Utility method for testing the invariants of a context.
- *
- * @param message
- * a message for debugging.
- * @param mch
- * a context root whose invariants will be tested.
- * @param expected
- * the expected pretty-print invariants. The invariants are
- * "pretty-printed" as follows:
- * "label:predicateString:isTheorem". The order of the invariants
- * is important.
- */
- protected void testMachineInvariants(String message, IMachineRoot mch,
- String... expected) {
- try {
- IInvariant[] invs = mch.getInvariants();
- assertEquals(message + ": Incorrect number of invariants",
- expected.length, invs.length);
- for (int i = 0; i < expected.length; i++) {
- testInvariant(message, invs[i], expected[i]);
- }
- } catch (RodinDBException e) {
- e.printStackTrace();
- fail("There should be no exception");
- return;
- }
- }
-
- /**
- * Utility method for testing an invariant.
- *
- * @param message
- * a message for debugging.
- * @param inv
- * the invariant under test.
- * @param expected
- * the expected pretty-print invariant. The invariant is
- * "pretty-printed" as follows:
- * "label:predicateString:isTheorem".
- */
- protected void testInvariant(String message, IInvariant inv, String expected) {
- try {
- assertEquals(
- message + ": Incorrect invariant",
- expected,
- inv.getLabel() + ":" + inv.getPredicateString() + ":"
- + inv.isTheorem());
- } catch (RodinDBException e) {
- e.printStackTrace();
- fail("There should be no exception");
- return;
- }
- }
-
- /**
- * Utility method for testing the events of a machine.
- *
- * @param message
- * a message for debugging.
- * @param mch
- * a machine root whose events will be tested.
- * @param expected
- * the expected pretty-print events (only the signature). The
- * events are "pretty-printed" as follows:
- * "label:convergent:isExtended". The order of the events is
- * important.
- */
- protected void testMachineEvents(String message, IMachineRoot mch,
- String... expected) {
- try {
- IEvent[] evts = mch.getEvents();
- assertEquals(message + ": Incorrect number of events",
- expected.length, evts.length);
- for (int i = 0; i < expected.length; i++) {
- testEvent(message, evts[i], expected[i]);
- }
- } catch (RodinDBException e) {
- e.printStackTrace();
- fail("There should be no exception");
- return;
- }
- }
-
- /**
- * Utility method for testing an event.
- *
- * @param message
- * a message for debugging.
- * @param evt
- * the event under test.
- * @param expected
- * the expected pretty-print event (only the signature). The
- * event is "pretty-printed" as follows:
- * "label:convergent:isExtended".
- */
- protected void testEvent(String message, IEvent evt, String expected) {
- try {
- assertNotNull(message + ": The event must not be null", evt);
- assertEquals(
- message + ": Incorrect event",
- expected,
- evt.getLabel() + ":" + evt.getConvergence() + ":"
- + evt.isExtended());
- } catch (RodinDBException e) {
- e.printStackTrace();
- fail("There should be no exception");
- return;
- }
- }
-
- /**
- * Utility method for testing the REFINES clauses of an event.
- *
- * @param message
- * a message for debugging.
- * @param mch
- * an event whose REFINES clauses will be tested.
- * @param expected
- * an array of expected REFINES clause. Each REFINES clause is
- * represented by its abstract event name. The order of the
- * REFINES clauses is important.
- */
- protected void testEventRefinesClauses(String message, IEvent evt,
- String... expected) {
- try {
- IRefinesEvent[] refinesClauses = evt.getRefinesClauses();
- assertEquals(message + ": Incorrect number of REFINES clauses",
- expected.length, refinesClauses.length);
- for (int i = 0; i < expected.length; i++) {
- testRefinesClause(message, refinesClauses[i], expected[i]);
- }
- } catch (RodinDBException e) {
- e.printStackTrace();
- fail("There should be no exception");
- return;
- }
- }
-
- /**
- * Utility method for testing a REFINES (event) clause.
- *
- * @param message
- * a message for debugging.
- * @param seesClause
- * the REFINES (event) clause under test.
- * @param expected
- * the expected abstract event name of the REFINES clause.
- */
- protected void testRefinesClause(String message,
- IRefinesEvent refinesEvent, String expected) {
- try {
- assertEquals(message + "Incorrect REFINES clause", expected,
- refinesEvent.getAbstractEventLabel());
- } catch (RodinDBException e) {
- e.printStackTrace();
- fail("There should be no exception");
- return;
- }
- }
-
- /**
- * Utility method for testing the parameters of an event.
- *
- * @param message
- * a message for debugging.
- * @param evt
- * an event whose parameters will be tested.
- * @param expected
- * the expected set of parameters. Each parameter is represented
- * by its identifier. The order of the parameters is important.
- */
- protected void testEventParameters(String message, IEvent evt,
- String... expected) {
- try {
- IParameter[] params = evt.getParameters();
- assertEquals(message + ": Incorrect number of parameters",
- expected.length, params.length);
- for (int i = 0; i < expected.length; i++) {
- testParameter(message, params[i], expected[i]);
- }
- } catch (RodinDBException e) {
- e.printStackTrace();
- fail("There should be no exception");
- return;
- }
- }
-
- /**
- * Utility method for testing a parameter.
- *
- * @param message
- * a message for debugging.
- * @param par
- * the parameter under test.
- * @param expected
- * the expected parameter identifier.
- */
- protected void testParameter(String message, IParameter par, String expected) {
- try {
- assertEquals(message + ": Incorrect parameter", expected,
- par.getIdentifierString());
- } catch (RodinDBException e) {
- e.printStackTrace();
- fail("There should be no exception");
- return;
- }
- }
-
- /**
- * Utility method for testing the guards of an event.
- *
- * @param message
- * a message for debugging.
- * @param evt
- * an event whose guards will be tested.
- * @param expected
- * the expected pretty-print guards. The guards are
- * "pretty-printed" as follows:
- * "label:predicateString:isTheorem". The order of the guards is
- * important.
- */
- protected void testEventGuards(String message, IEvent evt,
- String... expected) {
- try {
- IGuard[] grds = evt.getGuards();
- assertEquals(message + ": Incorrect number of guards",
- expected.length, grds.length);
- for (int i = 0; i < grds.length; i++) {
- testGuard(message, grds[i], expected[i]);
- }
- } catch (RodinDBException e) {
- e.printStackTrace();
- fail("There should be no exception");
- return;
- }
- }
-
- /**
- * Utility method for testing a guard.
- *
- * @param message
- * a message for debugging.
- * @param grd
- * the guard under test.
- * @param expected
- * the expected pretty-print guard. The guard is "pretty-printed"
- * as follows: "label:predicateString:isTheorem".
- */
- protected void testGuard(String message, IGuard grd, String expected) {
- try {
- assertEquals(
- message + ": Incorrect guard",
- expected,
- grd.getLabel() + ":" + grd.getPredicateString() + ":"
- + grd.isTheorem());
- } catch (RodinDBException e) {
- e.printStackTrace();
- fail("There should be no exception");
- return;
- }
- }
-
- /**
- * Utility method for testing the witnesses of an event.
- *
- * @param message
- * a message for debugging.
- * @param evt
- * an event whose witnesses will be tested.
- * @param expected
- * the expected pretty-print witnesses. The witnesses are
- * "pretty-printed" as follows: "label:predicateString". The
- * order of the witnesses is important.
- */
- protected void testEventWitnesses(String message, IEvent evt,
- String... expected) {
- try {
- IWitness[] wits = evt.getWitnesses();
- assertEquals(message + ": Incorrect number of witnesses",
- expected.length, wits.length);
- for (int i = 0; i < expected.length; i++) {
- testWitness(message, wits[i], expected[i]);
- }
- } catch (RodinDBException e) {
- e.printStackTrace();
- fail("There should be no exception");
- return;
- }
- }
-
- /**
- * Utility method for testing an witness.
- *
- * @param message
- * a message for debugging.
- * @param wit
- * the witness under test.
- * @param expected
- * the expected pretty-print witness. The witness is
- * "pretty-printed" as follows: "label:predicateString".
- */
- protected void testWitness(String message, IWitness wit, String expected) {
- try {
- assertEquals(message + ": Incorrect witness", expected,
- wit.getLabel() + ":" + wit.getPredicateString());
- } catch (RodinDBException e) {
- e.printStackTrace();
- fail("There should be no exception");
- return;
- }
- }
-
- /**
- * Utility method for testing the actions of an event.
- *
- * @param message
- * a message for debugging.
- * @param evt
- * an event whose actions will be tested.
- * @param expected
- * expected pretty-print actions. The actions are
- * "pretty-printed" as follows: "label:assignmentString". The
- * order of the actions is important.
- */
- protected void testEventActions(String message, IEvent evt,
- String... expected) {
- try {
- IAction[] acts = evt.getActions();
- assertEquals(message + ": Incorrect number of actions",
- expected.length, acts.length);
- for (int i = 0; i < expected.length; i++) {
- testAction(message, acts[i], expected[i]);
- }
- } catch (RodinDBException e) {
- e.printStackTrace();
- fail("There should be no exception");
- return;
- }
- }
-
- /**
- * Utility method for testing an action.
- *
- * @param message
- * a message
- * @param act
- * the action under test
- * @param expected
- * expected pretty-print action. The action is "pretty-printed"
- * as follows: "label:assignmentString".
- */
- protected void testAction(String message, IAction act, String expected) {
- try {
- assertEquals(message + ": Incorrect action", expected,
- act.getLabel() + ":" + act.getAssignmentString());
- } catch (RodinDBException e) {
- e.printStackTrace();
- fail("There should be no exception");
- return;
- }
- }
-
-}
diff --git a/de.prob.units.tests/src/de/prob/units/tests/AbstractTests.java b/de.prob.units.tests/src/de/prob/units/tests/AbstractTests.java
deleted file mode 100644
index eceb7e839e98407ed719f71b35032c29179cbdbe..0000000000000000000000000000000000000000
--- a/de.prob.units.tests/src/de/prob/units/tests/AbstractTests.java
+++ /dev/null
@@ -1,143 +0,0 @@
-package de.prob.units.tests;
-
-import java.util.Collection;
-import java.util.Map;
-import java.util.Set;
-
-import junit.framework.TestCase;
-
-/**
- * @author htson
- * <p>
- * This abstract class contains utility methods supporting testing.
- * </p>
- */
-public abstract class AbstractTests extends TestCase {
-
- /**
- * Constructor: Create max_size test case.
- */
- public AbstractTests() {
- super();
- }
-
- /**
- * Constructor: Create max_size test case with the given name.
- *
- * @param name
- * the name of test
- */
- public AbstractTests(String name) {
- super(name);
- }
-
- /**
- * Utility method to compare two string collections. The expected collection
- * is given in terms of an array of strings. The actual collection is given
- * as a collection of strings. The two are the same if the number of
- * elements is the same and every element of the expected collection appear
- * in the actual collection.
- *
- * @param msg
- * a message.
- * @param actual
- * actual collection of strings.
- * @param expected
- * expected array of strings.
- */
- protected static void assertSameStrings(String msg,
- Collection<String> actual, String... expected) {
- assertEquals(msg + ": Incorrect number of elements\n", expected.length,
- actual.size());
- for (String exp : expected) {
- assertTrue(msg + ": Expected element " + exp + " not found",
- actual.contains(exp));
- }
- }
-
- /**
- * Utility method to compare two arrays of strings. The two are the same if
- * the number of elements is the same, and the strings at the same index are
- * the same.
- *
- * @param msg
- * a message.
- * @param actual
- * actual array of strings.
- * @param expected
- * expected array of strings.
- */
- protected static void assertSameStrings(String msg, String[] actual,
- String... expected) {
- assertEquals(msg + ": Incorrect number of strings\n", expected.length,
- actual.length);
- for (int i = 0; i < expected.length; i++) {
- assertEquals(msg, expected[i], actual[i]);
- }
- }
-
- /**
- * Utility method to compare two arrays of objects. The two are the same if
- * the number of elements is the same, and the objects at the same index are
- * the same.
- *
- * @param msg
- * a message.
- * @param expected
- * expected array of objects.
- * @param actual
- * actual array of objects.
- */
- protected static void assertSameObjects(String msg, Object[] expected,
- Object[] actual) {
- assertEquals(msg + ": Incorrect number of objects\n", expected.length,
- actual.length);
- for (int i = 0; i < expected.length; i++) {
- assertEquals(msg, expected[i], actual[i]);
- }
- }
-
- /**
- * Utility method to compare two maps of objects to objects. The two are the
- * same if the key sets are the same (using
- * {@link #assertSameSet(String, Set, Set)}), and for each key, they map to
- * the same value.
- *
- * @param msg
- * a messages.
- * @param expected
- * expected map.
- * @param actual
- * actual map.
- */
- protected void assertSameMap(String msg,
- Map<? extends Object, ? extends Object> expected,
- Map<? extends Object, ? extends Object> actual) {
- Set<? extends Object> expectedKeySet = expected.keySet();
- Set<? extends Object> actualKeySet = actual.keySet();
- assertSameSet(msg, expectedKeySet, actualKeySet);
- for (Object key : expectedKeySet) {
- assertEquals(msg, expected.get(key), actual.get(key));
- }
- }
-
- /**
- * Utility method to compare two sets of objects. The two are the same if
- * they have the same number of elements, and each element of the expected
- * set appears in the actual set.
- *
- * @param msg
- * @param expected
- * @param actual
- */
- protected void assertSameSet(String msg, Set<? extends Object> expected,
- Set<? extends Object> actual) {
- assertEquals(msg + ": The number of elements must be the same",
- expected.size(), actual.size());
- for (Object elm : expected) {
- assertTrue(msg + ": expected element " + elm + " not found",
- actual.contains(elm));
- }
- }
-
-}
\ No newline at end of file
diff --git a/de.prob.units.tests/src/de/prob/units/tests/Activator.java b/de.prob.units.tests/src/de/prob/units/tests/Activator.java
deleted file mode 100644
index 3f4f6e4c2c5bca60dd376370b831f5a763fd904a..0000000000000000000000000000000000000000
--- a/de.prob.units.tests/src/de/prob/units/tests/Activator.java
+++ /dev/null
@@ -1,50 +0,0 @@
-package de.prob.units.tests;
-
-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.tests"; //$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.tests/src/de/prob/units/translation/tests/PragmaTranslatorTest.java b/de.prob.units.tests/src/de/prob/units/translation/tests/PragmaTranslatorTest.java
deleted file mode 100644
index 79956b4befd9c37f952d22f89b98bdea93e90b57..0000000000000000000000000000000000000000
--- a/de.prob.units.tests/src/de/prob/units/translation/tests/PragmaTranslatorTest.java
+++ /dev/null
@@ -1,94 +0,0 @@
-package de.prob.units.translation.tests;
-
-import java.io.PrintWriter;
-import java.io.StringWriter;
-
-import org.eclipse.core.resources.IncrementalProjectBuilder;
-import org.eclipse.core.runtime.CoreException;
-import org.eclipse.core.runtime.NullProgressMonitor;
-import org.eventb.core.IConstant;
-import org.eventb.core.IContextRoot;
-import org.eventb.core.IEventBProject;
-import org.eventb.core.IMachineRoot;
-import org.eventb.core.IVariable;
-import org.junit.Before;
-import org.junit.Test;
-import org.rodinp.core.IAttributeType;
-import org.rodinp.core.RodinCore;
-
-import de.prob.core.translator.TranslationFailedException;
-import de.prob.eventb.translator.TranslatorFactory;
-import de.prob.units.tests.AbstractEventBTests;
-
-public class PragmaTranslatorTest extends AbstractEventBTests {
- final IAttributeType.String UNITATTRIBUTE = RodinCore
- .getStringAttrType("de.prob.units.unitPragmaAttribute");
-
- private StringWriter stringWriter;
- private PrintWriter writer;
-
- @Before
- @Override
- protected void setUp() throws Exception {
- super.setUp();
- stringWriter = new StringWriter();
- writer = new PrintWriter(stringWriter);
- }
-
- @Test
- public void testMachineWithUnitPragmaOnVariable() throws CoreException,
- TranslationFailedException {
- IEventBProject project = createEventBProject("TestProject");
- IMachineRoot machine = createMachine(project, "TestMachine");
-
- IVariable v1 = createVariable(machine, "v1");
- createInvariant(machine, "inv1", "v1=5", false);
-
- // add unit pragma to variable
- v1.setAttributeValue(UNITATTRIBUTE, "test", new NullProgressMonitor());
-
- // save file and build workspace - this triggers static check, and
- // generates missing files
- machine.getRodinFile().save(monitor, false);
- workspace.build(IncrementalProjectBuilder.FULL_BUILD, monitor);
-
- // there should be one variable and one SC variable
- assertEquals(1, machine.getVariables().length);
- assertEquals(1, machine.getSCMachineRoot().getSCVariables().length);
-
- TranslatorFactory.translate(machine, writer);
-
- assertEquals(
- "package(load_event_b_project([event_b_model(none,'TestMachine',[sees(none,[]),variables(none,[identifier(none,v1)]),invariant(none,[equal(rodinpos('TestMachine',inv1,'('),identifier(none,v1),integer(none,5))]),theorems(none,[]),events(none,[])])],[],[exporter_version(2),pragma(unit,'TestMachine',v1,[test])],_Error)).\n",
- stringWriter.getBuffer().toString());
- }
-
- @Test
- public void testContextWithUnitPragmaOnConstant() throws CoreException,
- TranslationFailedException {
- IEventBProject project = createEventBProject("TestProject");
- IContextRoot context = createContext(project, "TestContext");
-
- IConstant c1 = createConstant(context, "cst1");
- createAxiom(context, "axm1", "cst1=5", false);
-
- // add unit pragma to constant
- c1.setAttributeValue(UNITATTRIBUTE, "test", new NullProgressMonitor());
-
- // save file and build workspace - this triggers static check, and
- // generates missing files
- context.getRodinFile().save(monitor, false);
- project.getRodinProject().save(monitor, false);
- workspace.build(IncrementalProjectBuilder.FULL_BUILD, monitor);
-
- // there should be one constant and one SC constant
- assertEquals(1, context.getConstants().length);
- assertEquals(1, context.getSCContextRoot().getSCConstants().length);
-
- TranslatorFactory.translate(context, writer);
-
- assertEquals(
- "package(load_event_b_project([],[event_b_context(none,'TestContext',[extends(none,[]),constants(none,[identifier(none,cst1)]),axioms(none,[equal(rodinpos('TestContext',axm1,'('),identifier(none,cst1),integer(none,5))]),theorems(none,[]),sets(none,[])])],[exporter_version(2),pragma(unit,'TestContext',cst1,[test])],_Error)).\n",
- stringWriter.getBuffer().toString());
- }
-}
diff --git a/de.prob.units/.classpath b/de.prob.units/.classpath
deleted file mode 100644
index eca7bdba8f03f22510b7980a94dbfe10c16c0901..0000000000000000000000000000000000000000
--- a/de.prob.units/.classpath
+++ /dev/null
@@ -1,7 +0,0 @@
-<?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.8"/>
- <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
deleted file mode 100644
index 22333fa9cb227f96d35310a6635507f782547a31..0000000000000000000000000000000000000000
--- a/de.prob.units/.project
+++ /dev/null
@@ -1,28 +0,0 @@
-<?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
deleted file mode 100644
index 0c68a61dca867ceb49e79d2402935261ec3e3809..0000000000000000000000000000000000000000
--- a/de.prob.units/.settings/org.eclipse.jdt.core.prefs
+++ /dev/null
@@ -1,7 +0,0 @@
-eclipse.preferences.version=1
-org.eclipse.jdt.core.compiler.codegen.inlineJsrBytecode=enabled
-org.eclipse.jdt.core.compiler.codegen.targetPlatform=1.8
-org.eclipse.jdt.core.compiler.compliance=1.8
-org.eclipse.jdt.core.compiler.problem.assertIdentifier=error
-org.eclipse.jdt.core.compiler.problem.enumIdentifier=error
-org.eclipse.jdt.core.compiler.source=1.8
diff --git a/de.prob.units/META-INF/MANIFEST.MF b/de.prob.units/META-INF/MANIFEST.MF
deleted file mode 100644
index 956efb398ef46b0ff99ce95477908e22e4d7d79c..0000000000000000000000000000000000000000
--- a/de.prob.units/META-INF/MANIFEST.MF
+++ /dev/null
@@ -1,19 +0,0 @@
-Manifest-Version: 1.0
-Bundle-ManifestVersion: 2
-Bundle-Name: ProB Physical Units Support
-Bundle-SymbolicName: de.prob.units;singleton:=true
-Bundle-Version: 7.4.2.qualifier
-Bundle-Activator: de.prob.units.Activator
-Require-Bundle: org.eclipse.core.runtime,
- org.eclipse.core.commands,
- org.eclipse.core.resources,
- org.eclipse.jface,
- org.rodinp.core;bundle-version="[1.7.0,2.0.0)",
- de.prob.core;bundle-version="[9.4.0,9.5.0)",
- org.eventb.ui;bundle-version="[3.0.0,4.0.0)",
- de.prob.ui;bundle-version="[7.4.0,7.5.0)",
- org.eventb.core;bundle-version="[3.0.0,4.0.0)",
- org.eclipse.ui.workbench
-Bundle-ActivationPolicy: lazy
-Bundle-RequiredExecutionEnvironment: JavaSE-1.8
-Bundle-Vendor: HHU Düsseldorf STUPS Group
diff --git a/de.prob.units/build.properties b/de.prob.units/build.properties
deleted file mode 100644
index 79785acaeea2f69bbe4b5e556221958fef4b9f55..0000000000000000000000000000000000000000
--- a/de.prob.units/build.properties
+++ /dev/null
@@ -1,6 +0,0 @@
-source.. = src/
-output.. = bin/
-bin.includes = META-INF/,\
- .,\
- icons/,\
- plugin.xml
diff --git a/de.prob.units/icons/unit_analysis.png b/de.prob.units/icons/unit_analysis.png
deleted file mode 100644
index 36d5d6278be2e2226de7b9d4d0fc9da720e47f1b..0000000000000000000000000000000000000000
Binary files a/de.prob.units/icons/unit_analysis.png and /dev/null differ
diff --git a/de.prob.units/plugin.xml b/de.prob.units/plugin.xml
deleted file mode 100644
index 7c8fbc3eb4ae41cd56a219597d022f5e62ec8dd7..0000000000000000000000000000000000000000
--- a/de.prob.units/plugin.xml
+++ /dev/null
@@ -1,153 +0,0 @@
-<?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="false"
- id="de.prob.units.unitPragmaAttribute"
- isMath="true"
- prefix="Physical Unit:"
- style="single"
- 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="false"
- id="de.prob.units.inferredUnitPragmaAttribute"
- isMath="true"
- prefix="Inferred Physical Unit:"
- style="single"
- typeId="de.prob.units.inferredUnitPragmaAttribute">
- </textAttribute>
- <attributeRelation
- elementTypeId="org.eventb.core.scVariable">
- <attributeReference
- descriptionId="de.prob.units.unitPragmaAttribute">
- </attributeReference>
- <attributeReference
- descriptionId="de.prob.units.inferredUnitPragmaAttribute">
- </attributeReference>
- </attributeRelation>
- <attributeRelation
- elementTypeId="org.eventb.core.scConstant">
- <attributeReference
- descriptionId="de.prob.units.unitPragmaAttribute">
- </attributeReference>
- <attributeReference
- descriptionId="de.prob.units.inferredUnitPragmaAttribute">
- </attributeReference>
- </attributeRelation>
- </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">
- <or>
- <instanceof
- value="org.eventb.core.IMachineRoot">
- </instanceof>
- <instanceof
- value="org.eventb.core.IContextRoot">
- </instanceof>
- </or>
- </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>
- <extension
- point="org.eventb.core.configurations">
- <configuration
- id="mchBase"
- name="mchBase">
- <scModule
- id="de.prob.units.machineAttributeProcessor">
- </scModule>
- <scModule
- id="de.prob.units.contextAttributeProcessor">
- </scModule>
- </configuration>
- </extension>
- <extension
- id="scMachineModuleTypes"
- point="org.eventb.core.scModuleTypes">
- <processorType
- class="de.prob.units.sc.MachineAttributeProcessor"
- id="machineAttributeProcessor"
- name="machineAttributeProcessor"
- parent="org.eventb.core.machineModule">
- </processorType>
- <processorType
- class="de.prob.units.sc.ContextAttributeProcessor"
- id="contextAttributeProcessor"
- name="contextAttributeProcessor"
- parent="org.eventb.core.contextModule">
- </processorType>
- </extension>
-</plugin>
diff --git a/de.prob.units/src/de/prob/units/Activator.java b/de.prob.units/src/de/prob/units/Activator.java
deleted file mode 100644
index a867db55ff989f02df0adfa770760e0d69c1645f..0000000000000000000000000000000000000000
--- a/de.prob.units/src/de/prob/units/Activator.java
+++ /dev/null
@@ -1,68 +0,0 @@
-package de.prob.units;
-
-import org.eclipse.ui.plugin.AbstractUIPlugin;
-import org.osgi.framework.BundleContext;
-import org.rodinp.core.RodinCore;
-
-
-/**
- * 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;
-
- setConfig();
-
- }
-
- /*
- * (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;
- }
-
- /**
- * Registers a file configuration setter for our plugin.
- */
- public static void setConfig() {
- RodinCore.addElementChangedListener(new ConfSettor());
- }
-
-}
diff --git a/de.prob.units/src/de/prob/units/ConfSettor.java b/de.prob.units/src/de/prob/units/ConfSettor.java
deleted file mode 100644
index 3bcde7c95009dad497285fa05433eb6105b670f5..0000000000000000000000000000000000000000
--- a/de.prob.units/src/de/prob/units/ConfSettor.java
+++ /dev/null
@@ -1,66 +0,0 @@
-package de.prob.units;
-
-import org.eventb.core.IContextRoot;
-import org.eventb.core.IMachineRoot;
-import org.rodinp.core.ElementChangedEvent;
-import org.rodinp.core.IElementChangedListener;
-import org.rodinp.core.IElementType;
-import org.rodinp.core.IInternalElement;
-import org.rodinp.core.IRodinDB;
-import org.rodinp.core.IRodinElement;
-import org.rodinp.core.IRodinElementDelta;
-import org.rodinp.core.IRodinFile;
-import org.rodinp.core.IRodinProject;
-import org.rodinp.core.RodinDBException;
-
-/**
- * Class that updates the configuration of files, to add the static checker
- * modules for our qualitative probabilistic reasoning plug-in.
- */
-public class ConfSettor implements IElementChangedListener {
-
- private static final String CONFIG = Activator.PLUGIN_ID + ".mchBase";
-
- @Override
- public void elementChanged(ElementChangedEvent event) {
-
- final IRodinElementDelta d = event.getDelta();
- try {
- processDelta(d);
- } catch (final RodinDBException e) {
- // TODO add exception log
- }
- }
-
- private void processDelta(final IRodinElementDelta d)
- throws RodinDBException {
- final IRodinElement e = d.getElement();
-
- final IElementType<? extends IRodinElement> elementType = e
- .getElementType();
- if (elementType.equals(IRodinDB.ELEMENT_TYPE)
- || elementType.equals(IRodinProject.ELEMENT_TYPE)) {
- for (final IRodinElementDelta de : d.getAffectedChildren()) {
- processDelta(de);
- }
- } else if (elementType.equals(IRodinFile.ELEMENT_TYPE)) {
- final IInternalElement root = ((IRodinFile) e).getRoot();
-
- if (root.getElementType().equals(IMachineRoot.ELEMENT_TYPE)) {
- final IMachineRoot mch = (IMachineRoot) root;
- final String conf = mch.getConfiguration();
- if (!conf.contains(CONFIG)) {
- mch.setConfiguration(conf + ";" + CONFIG, null);
- }
- }
-
- if (root.getElementType().equals(IContextRoot.ELEMENT_TYPE)) {
- final IContextRoot ctx = (IContextRoot) root;
- final String conf = ctx.getConfiguration();
- if (!conf.contains(CONFIG)) {
- ctx.setConfiguration(conf + ";" + CONFIG, null);
- }
- }
- }
- }
-}
\ No newline at end of file
diff --git a/de.prob.units/src/de/prob/units/pragmas/InferredUnitPragmaAttribute.java b/de.prob.units/src/de/prob/units/pragmas/InferredUnitPragmaAttribute.java
deleted file mode 100644
index 7991b26aa8c86ab39f22325977cca18ed5cfae60..0000000000000000000000000000000000000000
--- a/de.prob.units/src/de/prob/units/pragmas/InferredUnitPragmaAttribute.java
+++ /dev/null
@@ -1,84 +0,0 @@
-/**
- * (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.ui.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");
-
- private final String defaultValue = "";
-
- 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 {
- try {
- return asInternalElement(element).getAttributeValue(ATTRIBUTE);
- } catch (RodinDBException ex) {
- // happens if the attribute is not set on this element
- // just return a default instead of throwing a RodinDBException
- }
- return defaultValue;
- }
-
- @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, defaultValue,
- 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
deleted file mode 100644
index cff957964d3d56a8c6a024e685ae64369c97ac7f..0000000000000000000000000000000000000000
--- a/de.prob.units/src/de/prob/units/pragmas/UnitPragmaAttribute.java
+++ /dev/null
@@ -1,83 +0,0 @@
-/**
- * (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.ui.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");
-
- private final String defaultValue = "";
-
- 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 {
- try {
- return asInternalElement(element).getAttributeValue(ATTRIBUTE);
- } catch (RodinDBException ex) {
- // happens if the attribute is not set on this element
- // just return a default instead of throwing a RodinDBException
- }
- return defaultValue;
- }
-
- @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, defaultValue,
- 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/problems/IncorrectUnitDefinitionMarker.java b/de.prob.units/src/de/prob/units/problems/IncorrectUnitDefinitionMarker.java
deleted file mode 100644
index d7f4e0e209b07a5e6672438eb9fb9ead979ee746..0000000000000000000000000000000000000000
--- a/de.prob.units/src/de/prob/units/problems/IncorrectUnitDefinitionMarker.java
+++ /dev/null
@@ -1,35 +0,0 @@
-package de.prob.units.problems;
-
-import org.eclipse.core.resources.IMarker;
-import org.rodinp.core.IRodinProblem;
-
-import de.prob.units.Activator;
-
-public class IncorrectUnitDefinitionMarker implements IRodinProblem {
-
- private final String message;
- private final int severity = IMarker.SEVERITY_ERROR;
- public static final String ERROR_CODE = Activator.PLUGIN_ID + "."
- + "incorrectUnitDefinition";
-
- public IncorrectUnitDefinitionMarker(String cstOrVar) {
- this.message = "Incorrect Unit Definition on Constant/Variable "
- + cstOrVar;
- }
-
- @Override
- public String getErrorCode() {
- return ERROR_CODE;
- }
-
- @Override
- public String getLocalizedMessage(Object[] arg0) {
- return message;
- }
-
- @Override
- public int getSeverity() {
- return severity;
- }
-
-}
diff --git a/de.prob.units/src/de/prob/units/problems/MultipleUnitsInferredMarker.java b/de.prob.units/src/de/prob/units/problems/MultipleUnitsInferredMarker.java
deleted file mode 100644
index 3daaa97a0666685bec7b28970fa324f98cafe30c..0000000000000000000000000000000000000000
--- a/de.prob.units/src/de/prob/units/problems/MultipleUnitsInferredMarker.java
+++ /dev/null
@@ -1,36 +0,0 @@
-package de.prob.units.problems;
-
-import org.eclipse.core.resources.IMarker;
-import org.rodinp.core.IRodinProblem;
-
-import de.prob.units.Activator;
-
-public class MultipleUnitsInferredMarker implements IRodinProblem {
-
- private final String message;
- private final int severity = IMarker.SEVERITY_ERROR;
-
- public static final String ERROR_CODE = Activator.PLUGIN_ID + "."
- + "multipleUnitsInferred";
-
- public MultipleUnitsInferredMarker(String cstOrVar) {
- this.message = "Multiple Units inferred for Constant/Variable "
- + cstOrVar;
- }
-
- @Override
- public String getErrorCode() {
- return ERROR_CODE;
- }
-
- @Override
- public String getLocalizedMessage(Object[] arg0) {
- return message;
- }
-
- @Override
- public int getSeverity() {
- return severity;
- }
-
-}
diff --git a/de.prob.units/src/de/prob/units/problems/NoUnitInferredMarker.java b/de.prob.units/src/de/prob/units/problems/NoUnitInferredMarker.java
deleted file mode 100644
index 8f011edccb79b26e67cd59da893354aa5d6a2830..0000000000000000000000000000000000000000
--- a/de.prob.units/src/de/prob/units/problems/NoUnitInferredMarker.java
+++ /dev/null
@@ -1,34 +0,0 @@
-package de.prob.units.problems;
-
-import org.eclipse.core.resources.IMarker;
-import org.rodinp.core.IRodinProblem;
-
-import de.prob.units.Activator;
-
-public class NoUnitInferredMarker implements IRodinProblem {
-
- private final String message;
- private final int severity = IMarker.SEVERITY_WARNING;
- public static final String ERROR_CODE = Activator.PLUGIN_ID + "."
- + "multipleUnitsInferred";
-
- public NoUnitInferredMarker(String cstOrVar) {
- this.message = "No Units inferred for Constant/Variable " + cstOrVar;
- }
-
- @Override
- public String getErrorCode() {
- return ERROR_CODE;
- }
-
- @Override
- public String getLocalizedMessage(Object[] arg0) {
- return message;
- }
-
- @Override
- public int getSeverity() {
- return severity;
- }
-
-}
diff --git a/de.prob.units/src/de/prob/units/sc/ContextAttributeProcessor.java b/de.prob.units/src/de/prob/units/sc/ContextAttributeProcessor.java
deleted file mode 100644
index 91b1fc7c6fddf08d2cab0741cb419fbff7e58b0f..0000000000000000000000000000000000000000
--- a/de.prob.units/src/de/prob/units/sc/ContextAttributeProcessor.java
+++ /dev/null
@@ -1,72 +0,0 @@
-package de.prob.units.sc;
-
-import org.eclipse.core.runtime.CoreException;
-import org.eclipse.core.runtime.IProgressMonitor;
-import org.eventb.core.EventBAttributes;
-import org.eventb.core.IConstant;
-import org.eventb.core.IContextRoot;
-import org.eventb.core.ISCConstant;
-import org.eventb.core.ISCContextRoot;
-import org.eventb.core.sc.SCCore;
-import org.eventb.core.sc.SCProcessorModule;
-import org.eventb.core.sc.state.ISCStateRepository;
-import org.eventb.core.tool.IModuleType;
-import org.rodinp.core.IInternalElement;
-import org.rodinp.core.IRodinElement;
-import org.rodinp.core.IRodinFile;
-
-import de.prob.units.Activator;
-import de.prob.units.pragmas.UnitPragmaAttribute;
-
-public class ContextAttributeProcessor extends SCProcessorModule {
- public static final IModuleType<ContextAttributeProcessor> MODULE_TYPE = SCCore
- .getModuleType(Activator.PLUGIN_ID + ".contextAttributeProcessor"); //$NON-NLS-1$
-
- @Override
- public void process(IRodinElement element, IInternalElement target,
- ISCStateRepository repository, IProgressMonitor monitor)
- throws CoreException {
- assert (element instanceof IRodinFile);
- assert (target instanceof ISCContextRoot);
-
- // get all variables and copy over the attributes
- IRodinFile contextFile = (IRodinFile) element;
- IContextRoot contextRoot = (IContextRoot) contextFile.getRoot();
-
- ISCContextRoot scContextRoot = (ISCContextRoot) target;
-
- IConstant[] constants = contextRoot.getConstants();
- ISCConstant[] scconstants = scContextRoot.getSCConstants();
-
- if (constants.length == 0 || scconstants.length == 0)
- return;
-
- for (IConstant constant : constants) {
- String identifier = constant
- .getAttributeValue(EventBAttributes.IDENTIFIER_ATTRIBUTE);
- ISCConstant scConstant = scContextRoot.getSCConstant(identifier);
-
- // might have been filtered out by previous modules
- if (scConstant.exists()) {
- // original might not contain the attribute
- if (constant.hasAttribute(UnitPragmaAttribute.ATTRIBUTE)) {
- String attribute = constant
- .getAttributeValue(UnitPragmaAttribute.ATTRIBUTE);
-
- attribute = UnitAttributeProcessorStatics
- .translateEventBPragmaToBPragma(attribute);
-
- scConstant.setAttributeValue(UnitPragmaAttribute.ATTRIBUTE,
- attribute, monitor);
- }
- }
- }
-
- }
-
- @Override
- public IModuleType<?> getModuleType() {
- return MODULE_TYPE;
- }
-
-}
diff --git a/de.prob.units/src/de/prob/units/sc/MachineAttributeProcessor.java b/de.prob.units/src/de/prob/units/sc/MachineAttributeProcessor.java
deleted file mode 100644
index 2b64a2e5dab0423d495e03e85312b3cee041d145..0000000000000000000000000000000000000000
--- a/de.prob.units/src/de/prob/units/sc/MachineAttributeProcessor.java
+++ /dev/null
@@ -1,69 +0,0 @@
-package de.prob.units.sc;
-
-import org.eclipse.core.runtime.CoreException;
-import org.eclipse.core.runtime.IProgressMonitor;
-import org.eventb.core.IMachineRoot;
-import org.eventb.core.ISCMachineRoot;
-import org.eventb.core.ISCVariable;
-import org.eventb.core.IVariable;
-import org.eventb.core.sc.SCCore;
-import org.eventb.core.sc.SCProcessorModule;
-import org.eventb.core.sc.state.ISCStateRepository;
-import org.eventb.core.tool.IModuleType;
-import org.rodinp.core.IInternalElement;
-import org.rodinp.core.IRodinElement;
-import org.rodinp.core.IRodinFile;
-
-import de.prob.units.Activator;
-import de.prob.units.pragmas.UnitPragmaAttribute;
-
-public class MachineAttributeProcessor extends SCProcessorModule {
- public static final IModuleType<MachineAttributeProcessor> MODULE_TYPE = SCCore
- .getModuleType(Activator.PLUGIN_ID + ".machineAttributeProcessor"); //$NON-NLS-1$
-
- @Override
- public void process(IRodinElement element, IInternalElement target,
- ISCStateRepository repository, IProgressMonitor monitor)
- throws CoreException {
- assert (element instanceof IRodinFile);
- assert (target instanceof ISCMachineRoot);
-
- // get all variables and copy over the attributes
- IRodinFile machineFile = (IRodinFile) element;
- IMachineRoot machineRoot = (IMachineRoot) machineFile.getRoot();
-
- ISCMachineRoot scMachineRoot = (ISCMachineRoot) target;
-
- IVariable[] variables = machineRoot.getVariables();
-
- if (variables.length == 0)
- return;
-
- for (IVariable var : variables) {
- String identifier = var.getIdentifierString();
- ISCVariable scVar = scMachineRoot.getSCVariable(identifier);
-
- // might have been filtered out by previous modules
- if (scVar.exists()) {
- // original might not contain the attribute
- if (var.hasAttribute(UnitPragmaAttribute.ATTRIBUTE)) {
- String attribute = var
- .getAttributeValue(UnitPragmaAttribute.ATTRIBUTE);
-
- attribute = UnitAttributeProcessorStatics
- .translateEventBPragmaToBPragma(attribute);
-
- scVar.setAttributeValue(UnitPragmaAttribute.ATTRIBUTE,
- attribute, monitor);
- }
- }
- }
-
- }
-
- @Override
- public IModuleType<?> getModuleType() {
- return MODULE_TYPE;
- }
-
-}
diff --git a/de.prob.units/src/de/prob/units/sc/UnitAttributeProcessorStatics.java b/de.prob.units/src/de/prob/units/sc/UnitAttributeProcessorStatics.java
deleted file mode 100644
index 4e819dad2fc094f1ef109c66e8efe1e468a3fefc..0000000000000000000000000000000000000000
--- a/de.prob.units/src/de/prob/units/sc/UnitAttributeProcessorStatics.java
+++ /dev/null
@@ -1,9 +0,0 @@
-package de.prob.units.sc;
-
-public class UnitAttributeProcessorStatics {
- static String translateEventBPragmaToBPragma(String eventBPragma) {
- String bPragma = eventBPragma.replace("^", "**");
- return bPragma;
- }
-
-}
diff --git a/de.prob.units/src/de/prob/units/ui/StartUnitAnalysisHandler.java b/de.prob.units/src/de/prob/units/ui/StartUnitAnalysisHandler.java
deleted file mode 100644
index 549a56f902eea225bcde5ba825cc6b74d69111e7..0000000000000000000000000000000000000000
--- a/de.prob.units/src/de/prob/units/ui/StartUnitAnalysisHandler.java
+++ /dev/null
@@ -1,384 +0,0 @@
-/**
- * (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 org.rodinp.core.RodinMarkerUtil;
-
-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;
-import de.prob.units.pragmas.UnitPragmaAttribute;
-import de.prob.units.problems.IncorrectUnitDefinitionMarker;
-import de.prob.units.problems.MultipleUnitsInferredMarker;
-import de.prob.units.problems.NoUnitInferredMarker;
-
-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();
- }
- }
-
- @Override
- 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;
-
- @Override
- public Object execute(final ExecutionEvent event) throws ExecutionException {
-
- fSelection = HandlerUtil.getCurrentSelection(event);
-
- // Get the Selection
- final IEventBRoot rootElement = getRootElement();
- final IFile resource = extractResource(rootElement);
-
- removeUnitErrorMarkers(resource);
-
- 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();
-
- GetPluginResultCommand pluginResultCommand = new GetPluginResultCommand(
- "Grounded Result State");
-
- final ComposedCommand composed = new ComposedCommand(clear,
- setPrefs, load, start, activatePlugin,
- pluginResultCommand);
-
- animator.execute(composed);
- 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 void removeUnitErrorMarkers(final IFile resource) {
- IProject project = resource.getProject();
- try {
- IMarker[] markers = project.findMarkers(
- "org.eclipse.core.resources.problemmarker", true,
- IResource.DEPTH_INFINITE);
- for (IMarker iMarker : markers) {
- if (iMarker.getAttribute(RodinMarkerUtil.ERROR_CODE, "")
- .equals(MultipleUnitsInferredMarker.ERROR_CODE)) {
- iMarker.delete();
- }
- if (iMarker.getAttribute(RodinMarkerUtil.ERROR_CODE, "")
- .equals(IncorrectUnitDefinitionMarker.ERROR_CODE)) {
- iMarker.delete();
- }
- if (iMarker.getAttribute(RodinMarkerUtil.ERROR_CODE, "")
- .equals(NoUnitInferredMarker.ERROR_CODE)) {
- iMarker.delete();
- }
- }
-
- } catch (CoreException e1) {
- }
- }
-
- 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(CompoundPrologTerm result)
- throws RodinDBException, ExecutionException {
- // preprocess the list into a map
- Map<String, String> variables = new HashMap<String, String>();
- List<String> offendingDefinitions = new ArrayList<String>();
-
- ListPrologTerm liste = BindingGenerator.getList(result.getArgument(1));
-
- for (PrologTerm term : liste) {
- if (term.isAtom()) {
- // this is an error message. do something about it.
- String offendingUnitDefinition = PrologTerm.atomicString(term)
- .replace("Incorrect unit definition: ['", "");
- offendingUnitDefinition = offendingUnitDefinition.replace("']",
- "");
-
- // add error to the list of incorrect definitions. error markers
- // will be attached later
- offendingDefinitions.add(offendingUnitDefinition);
-
- } else {
- // process inferred units and add to map
- 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) {
- // reset inferred unit
- var.setAttributeValue(InferredUnitPragmaAttribute.ATTRIBUTE,
- "", new NullProgressMonitor());
-
- String variableName = var.getIdentifierString();
- if (variables.containsKey(variableName)) {
- var.setAttributeValue(
- InferredUnitPragmaAttribute.ATTRIBUTE,
- variables.get(variableName),
- new NullProgressMonitor());
-
- if (variables.get(variableName).startsWith("multiple")) {
- var.createProblemMarker(
- InferredUnitPragmaAttribute.ATTRIBUTE,
- new MultipleUnitsInferredMarker(variableName));
- }
- if (variables.get(variableName).equals("unknown")) {
- var.createProblemMarker(
- InferredUnitPragmaAttribute.ATTRIBUTE,
- new NoUnitInferredMarker(variableName));
- }
- }
-
- // check if the attached unit pragma (given by user) was marked
- // as offending
- if (var.hasAttribute(UnitPragmaAttribute.ATTRIBUTE)) {
- if (offendingDefinitions.contains(var
- .getAttributeValue(UnitPragmaAttribute.ATTRIBUTE))) {
- var.createProblemMarker(
- InferredUnitPragmaAttribute.ATTRIBUTE,
- new IncorrectUnitDefinitionMarker(variableName));
- }
- }
- }
-
- } else if (rootElement instanceof IContextRoot) {
- // find and update constants
- IConstant[] allConstants = rootElement.getContextRoot()
- .getConstants();
-
- for (IConstant cst : allConstants) {
- // reset inferred unit
- cst.setAttributeValue(InferredUnitPragmaAttribute.ATTRIBUTE,
- "", new NullProgressMonitor());
-
- String constantName = cst.getIdentifierString();
- if (variables.containsKey(constantName)) {
- cst.setAttributeValue(
- InferredUnitPragmaAttribute.ATTRIBUTE,
- variables.get(constantName),
- new NullProgressMonitor());
-
- if (variables.get(constantName).equals("error")) {
- cst.createProblemMarker(
- InferredUnitPragmaAttribute.ATTRIBUTE,
- new MultipleUnitsInferredMarker(constantName));
- }
- if (variables.get(constantName).equals("unknown")) {
- cst.createProblemMarker(
- InferredUnitPragmaAttribute.ATTRIBUTE,
- new IncorrectUnitDefinitionMarker(constantName));
- }
- }
-
- // check if the attached unit pragma (given by user) was marked
- // as offending
- if (cst.hasAttribute(UnitPragmaAttribute.ATTRIBUTE)) {
- if (offendingDefinitions.contains(cst
- .getAttributeValue(UnitPragmaAttribute.ATTRIBUTE))) {
- cst.createProblemMarker(
- InferredUnitPragmaAttribute.ATTRIBUTE,
- new MultipleUnitsInferredMarker(constantName));
- }
- }
- }
- } 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
deleted file mode 100644
index 96b7c78653fba0643a8efc26c06b6a3f61c66bd7..0000000000000000000000000000000000000000
--- a/de.prob2.units.feature/.project
+++ /dev/null
@@ -1,17 +0,0 @@
-<?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
deleted file mode 100644
index ae8dfb5865c1107f8366e1e8c2af6ad2d1a7a9f1..0000000000000000000000000000000000000000
--- a/de.prob2.units.feature/.settings/org.eclipse.core.resources.prefs
+++ /dev/null
@@ -1,3 +0,0 @@
-#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
deleted file mode 100644
index 57a8ae0b2a629cab658cebb8c79bd02f33f25fb0..0000000000000000000000000000000000000000
--- a/de.prob2.units.feature/.settings/org.eclipse.core.runtime.prefs
+++ /dev/null
@@ -1,3 +0,0 @@
-#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
deleted file mode 100644
index 64f93a9f0b7328eb563aa5ad6cec7f828020e124..0000000000000000000000000000000000000000
--- a/de.prob2.units.feature/build.properties
+++ /dev/null
@@ -1 +0,0 @@
-bin.includes = feature.xml
diff --git a/de.prob2.units.feature/feature.xml b/de.prob2.units.feature/feature.xml
deleted file mode 100644
index 2930570ea75b8f7727fd558c31af288d2721ff18..0000000000000000000000000000000000000000
--- a/de.prob2.units.feature/feature.xml
+++ /dev/null
@@ -1,250 +0,0 @@
-<?xml version="1.0" encoding="UTF-8"?>
-<feature
- id="de.prob2.units.feature"
- label="ProB for Rodin3 - Physical Units Support"
- version="3.0.9.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
-projects Rodin and Deploy and the DFG projects Gepavas and Gepavas II.
-ProB has been successfully used on various industrial specifications
-and is now being used within Siemens, Alstom, Thales.
- </description>
-
- <copyright>
- (C) 2000-2020 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.core.runtime"/>
- <import plugin="org.eclipse.core.commands"/>
- <import plugin="org.eclipse.core.resources"/>
- <import plugin="org.eclipse.jface"/>
- <import plugin="org.rodinp.core" version="1.7.0" match="compatible"/>
- <import plugin="de.prob.core" version="9.4.0" match="equivalent"/>
- <import plugin="de.prob.ui" version="7.4.0" match="equivalent"/>
- <import plugin="org.eventb.core" version="3.0.0"/>
- <import plugin="org.eclipse.ui.workbench"/>
- <import plugin="org.eventb.ui" version="3.0.0"/>
- </requires>
-
- <plugin
- id="de.prob.units"
- download-size="0"
- install-size="0"
- version="0.0.0"
- unpack="false"/>
-
-</feature>