diff --git a/de.prob.core/plugin.xml b/de.prob.core/plugin.xml index c19d91206519aa9e612525bce6960363bbbb0891..b84a1eaef2043d86514040b1a698b95d501b759d 100644 --- a/de.prob.core/plugin.xml +++ b/de.prob.core/plugin.xml @@ -23,17 +23,4 @@ class="de.prob.core.StaticListenerRegistry"> </listener> </extension> - <extension - point="org.rodinp.core.attributeTypes"> - <attributeType - id="unitPragmaAttribute" - kind="string" - name="Content of a unit Pragma to send to ProB"> - </attributeType> - <attributeType - id="inferredUnitPragmaAttribute" - kind="string" - name="Content of a unit Pragma received from ProB"> - </attributeType> - </extension> </plugin> diff --git a/de.prob.core/src/de/prob/eventb/translator/ContextTranslator.java b/de.prob.core/src/de/prob/eventb/translator/ContextTranslator.java index 8087d36ade5702052ab18cbe8c46fbf5ada74e36..e65b7464246d76d8685d5b6bb32ff9e891d19f24 100644 --- a/de.prob.core/src/de/prob/eventb/translator/ContextTranslator.java +++ b/de.prob.core/src/de/prob/eventb/translator/ContextTranslator.java @@ -54,7 +54,6 @@ import de.be4.classicalb.core.parser.node.PPredicate; import de.be4.classicalb.core.parser.node.PSet; import de.be4.classicalb.core.parser.node.TIdentifierLiteral; import de.hhu.stups.sablecc.patch.SourcePosition; -import de.prob.core.internal.Activator; import de.prob.core.translator.TranslationFailedException; import de.prob.core.translator.pragmas.IPragma; import de.prob.core.translator.pragmas.UnitPragma; @@ -133,7 +132,7 @@ public final class ContextTranslator extends AbstractComponentTranslator { private void collectPragmas() throws RodinDBException { // unit pragma, attached to constants final IAttributeType.String UNITATTRIBUTE = RodinCore - .getStringAttrType(Activator.PLUGIN_ID + ".unitPragmaAttribute"); + .getStringAttrType("de.prob.units.unitPragmaAttribute"); final ISCConstant[] constants = context.getSCConstants(); diff --git a/de.prob.core/src/de/prob/eventb/translator/internal/ModelTranslator.java b/de.prob.core/src/de/prob/eventb/translator/internal/ModelTranslator.java index 67c9e62dad4399ce2256076dd7efc7fd2667eda6..b121f405c522a52f7b8f866fd93487234a8900e0 100644 --- a/de.prob.core/src/de/prob/eventb/translator/internal/ModelTranslator.java +++ b/de.prob.core/src/de/prob/eventb/translator/internal/ModelTranslator.java @@ -69,7 +69,6 @@ import de.be4.classicalb.core.parser.node.PPredicate; import de.be4.classicalb.core.parser.node.PSubstitution; import de.be4.classicalb.core.parser.node.PWitness; import de.be4.classicalb.core.parser.node.TIdentifierLiteral; -import de.prob.core.internal.Activator; import de.prob.core.translator.TranslationFailedException; import de.prob.core.translator.pragmas.IPragma; import de.prob.core.translator.pragmas.UnitPragma; @@ -184,7 +183,7 @@ public class ModelTranslator extends AbstractComponentTranslator { private void collectPragmas() throws RodinDBException { // unit pragma, attached to constants final IAttributeType.String UNITATTRIBUTE = RodinCore - .getStringAttrType(Activator.PLUGIN_ID + ".unitPragmaAttribute"); + .getStringAttrType("de.prob.units.unitPragmaAttribute"); final IVariable[] variables = origin.getVariables(); diff --git a/de.prob.ui/META-INF/MANIFEST.MF b/de.prob.ui/META-INF/MANIFEST.MF index 0789fd1e77bbe418961404c52e1aedbe96120a5e..0292f6b17151194d687a1bdffa1d3ffd3a2a4e35 100644 --- a/de.prob.ui/META-INF/MANIFEST.MF +++ b/de.prob.ui/META-INF/MANIFEST.MF @@ -10,8 +10,7 @@ Require-Bundle: org.eclipse.ui;bundle-version="[3.5.0,4.0.0)", de.prob.core;bundle-version="[9.3.0,9.4.0)", org.eventb.core;bundle-version="[2.1.0,2.6.0)", org.eclipse.core.expressions;bundle-version="[3.4.101,4.0.0)", - org.eclipse.gef;bundle-version="[3.5.0,4.0.0)", - org.eventb.ui;bundle-version="[2.1.0,2.6.0)" + org.eclipse.gef;bundle-version="[3.5.0,4.0.0)" Bundle-ActivationPolicy: lazy Bundle-Vendor: HHU Düsseldorf STUPS Group Bundle-Activator: de.prob.ui.ProbUiPlugin diff --git a/de.prob.ui/plugin.xml b/de.prob.ui/plugin.xml index 817c0fd5f246b495868644673648867d97274432..a64882ef7a42135a4a34f5d12d6b38230c1960c2 100644 --- a/de.prob.ui/plugin.xml +++ b/de.prob.ui/plugin.xml @@ -355,10 +355,6 @@ id="de.prob.command.startCspAnimation" name="Start CSP Animation"> </command> - <command - id="de.prob.ui.startunitanalysis" - name="Analyse Physical Units"> - </command> </extension> <extension point="org.eclipse.ui.handlers"> @@ -749,42 +745,6 @@ </with> </enabledWhen> </handler> - <handler - commandId="de.prob.ui.startunitanalysis"> - <class - class="de.prob.ui.eventb.StartUnitAnalysisHandler"> - </class> - <enabledWhen> - <with - variable="selection"> - <iterate - operator="or"> - <or> - <instanceof - value="org.eventb.core.IEventBRoot"> - </instanceof> - <and> - <instanceof - value="org.eclipse.core.resources.IResource"> - </instanceof> - <or> - <test - forcePluginActivation="true" - property="org.eclipse.core.resources.extension" - value="bum"> - </test> - <test - forcePluginActivation="true" - property="org.eclipse.core.resources.extension" - value="buc"> - </test> - </or> - </and> - </or> - </iterate> - </with> - </enabledWhen> - </handler> <!-- <handler commandId="de.prob.ui.startdmc"> <class @@ -1016,23 +976,6 @@ </with> </visibleWhen> </command> - <command - commandId="de.prob.ui.startunitanalysis" - icon="icons/prob.png" - label="Analyse Physical Units" - style="push"> - <visibleWhen> - <with - variable="selection"> - <iterate - operator="or"> - <instanceof - value="org.eventb.core.IEventBRoot"> - </instanceof> - </iterate> - </with> - </visibleWhen> - </command> <!-- <command commandId="de.prob.ui.startdmc" icon="icons/prob.png" @@ -1252,43 +1195,4 @@ </variable> </sourceProvider> </extension> - <extension - point="org.eventb.ui.editorItems"> - <textAttribute - class="de.prob.ui.pragmas.UnitPragmaAttribute" - expandsHorizontally="true" - id="de.prob.ui.unitPragmaAttribute" - isMath="true" - prefix="Physical Unit:" - style="de.prob.ui.unitPragmaAttribute" - typeId="de.prob.core.unitPragmaAttribute"> - </textAttribute> - <attributeRelation - elementTypeId="org.eventb.core.variable"> - <attributeReference - descriptionId="de.prob.ui.unitPragmaAttribute"> - </attributeReference> - <attributeReference - descriptionId="de.prob.ui.inferredUnitPragmaAttribute"> - </attributeReference> - </attributeRelation> - <attributeRelation - elementTypeId="org.eventb.core.constant"> - <attributeReference - descriptionId="de.prob.ui.unitPragmaAttribute"> - </attributeReference> - <attributeReference - descriptionId="de.prob.ui.inferredUnitPragmaAttribute"> - </attributeReference> - </attributeRelation> - <textAttribute - class="de.prob.ui.pragmas.InferredUnitPragmaAttribute" - expandsHorizontally="true" - id="de.prob.ui.inferredUnitPragmaAttribute" - isMath="true" - prefix="Inferred Physical Unit:" - style="de.prob.ui.inferredUnitPragmaAttribute" - typeId="de.prob.core.inferredUnitPragmaAttribute"> - </textAttribute> - </extension> </plugin> diff --git a/de.prob.units/.classpath b/de.prob.units/.classpath new file mode 100644 index 0000000000000000000000000000000000000000..ad32c83a7885b8953a938b41df3b4fd4fe1aae01 --- /dev/null +++ b/de.prob.units/.classpath @@ -0,0 +1,7 @@ +<?xml version="1.0" encoding="UTF-8"?> +<classpath> + <classpathentry kind="con" path="org.eclipse.jdt.launching.JRE_CONTAINER/org.eclipse.jdt.internal.debug.ui.launcher.StandardVMType/JavaSE-1.6"/> + <classpathentry kind="con" path="org.eclipse.pde.core.requiredPlugins"/> + <classpathentry kind="src" path="src"/> + <classpathentry kind="output" path="bin"/> +</classpath> diff --git a/de.prob.units/.project b/de.prob.units/.project new file mode 100644 index 0000000000000000000000000000000000000000..22333fa9cb227f96d35310a6635507f782547a31 --- /dev/null +++ b/de.prob.units/.project @@ -0,0 +1,28 @@ +<?xml version="1.0" encoding="UTF-8"?> +<projectDescription> + <name>de.prob.units</name> + <comment></comment> + <projects> + </projects> + <buildSpec> + <buildCommand> + <name>org.eclipse.jdt.core.javabuilder</name> + <arguments> + </arguments> + </buildCommand> + <buildCommand> + <name>org.eclipse.pde.ManifestBuilder</name> + <arguments> + </arguments> + </buildCommand> + <buildCommand> + <name>org.eclipse.pde.SchemaBuilder</name> + <arguments> + </arguments> + </buildCommand> + </buildSpec> + <natures> + <nature>org.eclipse.pde.PluginNature</nature> + <nature>org.eclipse.jdt.core.javanature</nature> + </natures> +</projectDescription> diff --git a/de.prob.units/.settings/org.eclipse.jdt.core.prefs b/de.prob.units/.settings/org.eclipse.jdt.core.prefs new file mode 100644 index 0000000000000000000000000000000000000000..c537b63063ce6052bdc49c5fd0745b078f162c90 --- /dev/null +++ b/de.prob.units/.settings/org.eclipse.jdt.core.prefs @@ -0,0 +1,7 @@ +eclipse.preferences.version=1 +org.eclipse.jdt.core.compiler.codegen.inlineJsrBytecode=enabled +org.eclipse.jdt.core.compiler.codegen.targetPlatform=1.6 +org.eclipse.jdt.core.compiler.compliance=1.6 +org.eclipse.jdt.core.compiler.problem.assertIdentifier=error +org.eclipse.jdt.core.compiler.problem.enumIdentifier=error +org.eclipse.jdt.core.compiler.source=1.6 diff --git a/de.prob.units/META-INF/MANIFEST.MF b/de.prob.units/META-INF/MANIFEST.MF new file mode 100644 index 0000000000000000000000000000000000000000..8fcd833628d6e9afe494d6563f2984f1a32fc9e1 --- /dev/null +++ b/de.prob.units/META-INF/MANIFEST.MF @@ -0,0 +1,13 @@ +Manifest-Version: 1.0 +Bundle-ManifestVersion: 2 +Bundle-Name: Units +Bundle-SymbolicName: de.prob.units;singleton:=true +Bundle-Version: 1.0.0.qualifier +Bundle-Activator: de.prob.units.Activator +Require-Bundle: org.eclipse.ui, + org.eclipse.core.runtime, + de.prob.core;bundle-version="9.3.0", + org.eventb.ui;bundle-version="2.5.0", + de.prob.ui;bundle-version="7.3.0" +Bundle-ActivationPolicy: lazy +Bundle-RequiredExecutionEnvironment: JavaSE-1.6 diff --git a/de.prob.units/build.properties b/de.prob.units/build.properties new file mode 100644 index 0000000000000000000000000000000000000000..e9863e281eaccc5123e82ed75713bab3e8b87bbe --- /dev/null +++ b/de.prob.units/build.properties @@ -0,0 +1,5 @@ +source.. = src/ +output.. = bin/ +bin.includes = META-INF/,\ + .,\ + plugin.xml diff --git a/de.prob.units/icons/unit_analysis.png b/de.prob.units/icons/unit_analysis.png new file mode 100644 index 0000000000000000000000000000000000000000..36d5d6278be2e2226de7b9d4d0fc9da720e47f1b Binary files /dev/null and b/de.prob.units/icons/unit_analysis.png differ diff --git a/de.prob.units/plugin.xml b/de.prob.units/plugin.xml new file mode 100644 index 0000000000000000000000000000000000000000..2b12b8589fe445b7dcf500ebc7232371a6c77b14 --- /dev/null +++ b/de.prob.units/plugin.xml @@ -0,0 +1,99 @@ +<?xml version="1.0" encoding="UTF-8"?> +<?eclipse version="3.4"?> +<plugin> + <extension + point="org.eventb.ui.editorItems"> + <textAttribute + class="de.prob.units.pragmas.UnitPragmaAttribute" + expandsHorizontally="true" + id="de.prob.units.unitPragmaAttribute" + isMath="true" + prefix="Physical Unit:" + style="de.prob.units.unitPragmaAttribute" + typeId="de.prob.units.unitPragmaAttribute"> + </textAttribute> + <attributeRelation + elementTypeId="org.eventb.core.variable"> + <attributeReference + descriptionId="de.prob.units.unitPragmaAttribute"> + </attributeReference> + <attributeReference + descriptionId="de.prob.units.inferredUnitPragmaAttribute"> + </attributeReference> + </attributeRelation> + <attributeRelation + elementTypeId="org.eventb.core.constant"> + <attributeReference + descriptionId="de.prob.units.unitPragmaAttribute"> + </attributeReference> + <attributeReference + descriptionId="de.prob.units.inferredUnitPragmaAttribute"> + </attributeReference> + </attributeRelation> + <textAttribute + class="de.prob.units.pragmas.InferredUnitPragmaAttribute" + expandsHorizontally="true" + id="de.prob.units.inferredUnitPragmaAttribute" + isMath="true" + prefix="Inferred Physical Unit:" + style="de.prob.units.inferredUnitPragmaAttribute" + typeId="de.prob.units.inferredUnitPragmaAttribute"> + </textAttribute> + </extension> + <extension + point="org.eclipse.ui.handlers"> + <handler + class="de.prob.units.ui.StartUnitAnalysisHandler" + commandId="de.prob.units.startunitanalysis"> + </handler> + </extension> + <extension + point="org.eclipse.ui.menus"> + <menuContribution + locationURI="popup:fr.systerel.explorer.navigator.view"> + <separator + name="de.prob.units.separator2"> + </separator> + <command + commandId="de.prob.units.startunitanalysis" + icon="icons/unit_analysis.png" + label="Analyse Physical Units" + style="push"> + <visibleWhen> + <with + variable="selection"> + <iterate + operator="or"> + <instanceof + value="org.eventb.core.IEventBRoot"> + </instanceof> + </iterate> + </with> + </visibleWhen> + </command> + <separator + name="de.prob.units.separator1"> + </separator> + </menuContribution> + </extension> + <extension + point="org.eclipse.ui.commands"> + <command + id="de.prob.units.startunitanalysis" + name="Analyse Physical Units"> + </command> + </extension> + <extension + point="org.rodinp.core.attributeTypes"> + <attributeType + id="unitPragmaAttribute" + kind="string" + name="Content of a unit Pragma to send to ProB"> + </attributeType> + <attributeType + id="inferredUnitPragmaAttribute" + kind="string" + name="Content of a unit Pragma received from ProB"> + </attributeType> + </extension> +</plugin> diff --git a/de.prob.units/src/de/prob/units/Activator.java b/de.prob.units/src/de/prob/units/Activator.java new file mode 100644 index 0000000000000000000000000000000000000000..cb9482f57446625e611905dd23c999190b96cf5c --- /dev/null +++ b/de.prob.units/src/de/prob/units/Activator.java @@ -0,0 +1,50 @@ +package de.prob.units; + +import org.eclipse.ui.plugin.AbstractUIPlugin; +import org.osgi.framework.BundleContext; + +/** + * The activator class controls the plug-in life cycle + */ +public class Activator extends AbstractUIPlugin { + + // The plug-in ID + public static final String PLUGIN_ID = "de.prob.units"; //$NON-NLS-1$ + + // The shared instance + private static Activator plugin; + + /** + * The constructor + */ + public Activator() { + } + + /* + * (non-Javadoc) + * @see org.eclipse.ui.plugin.AbstractUIPlugin#start(org.osgi.framework.BundleContext) + */ + public void start(BundleContext context) throws Exception { + super.start(context); + plugin = this; + } + + /* + * (non-Javadoc) + * @see org.eclipse.ui.plugin.AbstractUIPlugin#stop(org.osgi.framework.BundleContext) + */ + public void stop(BundleContext context) throws Exception { + plugin = null; + super.stop(context); + } + + /** + * Returns the shared instance + * + * @return the shared instance + */ + public static Activator getDefault() { + return plugin; + } + +} diff --git a/de.prob.ui/src/de/prob/ui/pragmas/InferredUnitPragmaAttribute.java b/de.prob.units/src/de/prob/units/pragmas/InferredUnitPragmaAttribute.java similarity index 97% rename from de.prob.ui/src/de/prob/ui/pragmas/InferredUnitPragmaAttribute.java rename to de.prob.units/src/de/prob/units/pragmas/InferredUnitPragmaAttribute.java index 6a7810049cac80b3c6807e5a979a4436d1205c9c..a2d7ec278f082fb569e9827a184f7b6785a823c1 100644 --- a/de.prob.ui/src/de/prob/ui/pragmas/InferredUnitPragmaAttribute.java +++ b/de.prob.units/src/de/prob/units/pragmas/InferredUnitPragmaAttribute.java @@ -4,7 +4,7 @@ * (http://www.eclipse.org/org/documents/epl-v10.html) * */ -package de.prob.ui.pragmas; +package de.prob.units.pragmas; import org.eclipse.core.runtime.IProgressMonitor; import org.eventb.core.IVariable; @@ -16,7 +16,7 @@ import org.rodinp.core.IRodinElement; import org.rodinp.core.RodinCore; import org.rodinp.core.RodinDBException; -import de.prob.core.internal.Activator; +import de.prob.units.Activator; public class InferredUnitPragmaAttribute implements IAttributeManipulation { public static IAttributeType.String ATTRIBUTE = RodinCore diff --git a/de.prob.ui/src/de/prob/ui/pragmas/UnitPragmaAttribute.java b/de.prob.units/src/de/prob/units/pragmas/UnitPragmaAttribute.java similarity index 96% rename from de.prob.ui/src/de/prob/ui/pragmas/UnitPragmaAttribute.java rename to de.prob.units/src/de/prob/units/pragmas/UnitPragmaAttribute.java index 74aa0f9a6a548f5cb754129a760d3561b9fc3d37..8c0075f18b1545de6594c0234b6480b690db660f 100644 --- a/de.prob.ui/src/de/prob/ui/pragmas/UnitPragmaAttribute.java +++ b/de.prob.units/src/de/prob/units/pragmas/UnitPragmaAttribute.java @@ -4,7 +4,7 @@ * (http://www.eclipse.org/org/documents/epl-v10.html) * */ -package de.prob.ui.pragmas; +package de.prob.units.pragmas; import org.eclipse.core.runtime.IProgressMonitor; import org.eventb.core.IVariable; @@ -16,7 +16,7 @@ import org.rodinp.core.IRodinElement; import org.rodinp.core.RodinCore; import org.rodinp.core.RodinDBException; -import de.prob.core.internal.Activator; +import de.prob.units.Activator; public class UnitPragmaAttribute implements IAttributeManipulation { public static IAttributeType.String ATTRIBUTE = RodinCore diff --git a/de.prob.ui/src/de/prob/ui/eventb/StartUnitAnalysisHandler.java b/de.prob.units/src/de/prob/units/ui/StartUnitAnalysisHandler.java similarity index 99% rename from de.prob.ui/src/de/prob/ui/eventb/StartUnitAnalysisHandler.java rename to de.prob.units/src/de/prob/units/ui/StartUnitAnalysisHandler.java index ad8b1ebf708e0743ffbed10981eb994b7669cbcc..13585c407fc04e9c63257ab7e220d1e8159d62e1 100644 --- a/de.prob.ui/src/de/prob/ui/eventb/StartUnitAnalysisHandler.java +++ b/de.prob.units/src/de/prob/units/ui/StartUnitAnalysisHandler.java @@ -4,7 +4,7 @@ * (http://www.eclipse.org/org/documents/epl-v10.html) * */ -package de.prob.ui.eventb; +package de.prob.units.ui; import java.util.ArrayList; import java.util.HashMap; @@ -56,7 +56,7 @@ 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.ui.pragmas.InferredUnitPragmaAttribute; +import de.prob.units.pragmas.InferredUnitPragmaAttribute; public class StartUnitAnalysisHandler extends AbstractHandler implements IHandler { diff --git a/de.prob2.units.feature/.project b/de.prob2.units.feature/.project new file mode 100644 index 0000000000000000000000000000000000000000..96b7c78653fba0643a8efc26c06b6a3f61c66bd7 --- /dev/null +++ b/de.prob2.units.feature/.project @@ -0,0 +1,17 @@ +<?xml version="1.0" encoding="UTF-8"?> +<projectDescription> + <name>de.prob2.units.feature</name> + <comment></comment> + <projects> + </projects> + <buildSpec> + <buildCommand> + <name>org.eclipse.pde.FeatureBuilder</name> + <arguments> + </arguments> + </buildCommand> + </buildSpec> + <natures> + <nature>org.eclipse.pde.FeatureNature</nature> + </natures> +</projectDescription> diff --git a/de.prob2.units.feature/.settings/org.eclipse.core.resources.prefs b/de.prob2.units.feature/.settings/org.eclipse.core.resources.prefs new file mode 100644 index 0000000000000000000000000000000000000000..ae8dfb5865c1107f8366e1e8c2af6ad2d1a7a9f1 --- /dev/null +++ b/de.prob2.units.feature/.settings/org.eclipse.core.resources.prefs @@ -0,0 +1,3 @@ +#Tue Nov 29 16:17:25 CET 2011 +eclipse.preferences.version=1 +encoding/<project>=UTF-8 diff --git a/de.prob2.units.feature/.settings/org.eclipse.core.runtime.prefs b/de.prob2.units.feature/.settings/org.eclipse.core.runtime.prefs new file mode 100644 index 0000000000000000000000000000000000000000..57a8ae0b2a629cab658cebb8c79bd02f33f25fb0 --- /dev/null +++ b/de.prob2.units.feature/.settings/org.eclipse.core.runtime.prefs @@ -0,0 +1,3 @@ +#Tue Nov 29 16:17:25 CET 2011 +eclipse.preferences.version=1 +line.separator=\n diff --git a/de.prob2.units.feature/build.properties b/de.prob2.units.feature/build.properties new file mode 100644 index 0000000000000000000000000000000000000000..64f93a9f0b7328eb563aa5ad6cec7f828020e124 --- /dev/null +++ b/de.prob2.units.feature/build.properties @@ -0,0 +1 @@ +bin.includes = feature.xml diff --git a/de.prob2.units.feature/feature.xml b/de.prob2.units.feature/feature.xml new file mode 100644 index 0000000000000000000000000000000000000000..e6432b794d0c846138eb1b6eaf1315ba8303f26b --- /dev/null +++ b/de.prob2.units.feature/feature.xml @@ -0,0 +1,281 @@ +<?xml version="1.0" encoding="UTF-8"?> +<feature + id="de.prob2.units.feature" + label="ProB for Rodin2 - Physical Units Support" + version="2.3.5.qualifier" + provider-name="HHU Düsseldorf STUPS Group"> + + <description url="http://www.stups.uni-duesseldorf.de/ProB"> + ProB is an animator and model checker for the B-Method. It allows fully automatic animation of many B specifications, and can be used to systematically check a specification for errors. +Part of the research and development was conducted within the EPSRC funded projects ABCD and iMoc, and within the EU funded project Rodin. +Development is continued under the EU funded project Deploy and the DFG project Gepavas. +ProB has been successfully used on various industrial specifications and is now being used within Siemens. + </description> + + <copyright> + (C) 2000-2011 Michael Leuschel (and many others) All rights reserved. + </copyright> + + <license url="http://www.eclipse.org/org/documents/epl-v10.html"> + ProB can be used freely for commercial, non-commercial and academic +use under the Eclipse Public Licence v. 1.0. (below) +For availability of commercial support, please contact the author +(http://www.stups.uni-duesseldorf.de/~leuschel). +Use of ProB's nauty library for symmetry reduction implies further +restrictions (no applications with nontrivial military significance, +see http://cs.anu.edu.au/~bdm/nauty/). +--- +Eclipse Public License - v. 1.0 +THE ACCOMPANYING PROGRAM IS PROVIDED UNDER THE TERMS OF THIS +ECLIPSE PUBLIC LICENSE ("AGREEMENT"). ANY USE, REPRODUCTION OR +DISTRIBUTION OF THE PROGRAM CONSTITUTES RECIPIENT'S ACCEPTANCE +OF THIS AGREEMENT. +1. DEFINITIONS +"Contribution" means: +a) in the case of the initial Contributor, the initial code and +documentation distributed under this Agreement, and +b) in the case of each subsequent Contributor: +i) changes to the Program, and +ii) additions to the Program; +where such changes and/or additions to the Program originate +from and are distributed by that particular Contributor. A Contribution +'originates' from a Contributor if it was added to the Program +by such Contributor itself or anyone acting on such Contributor's +behalf. Contributions do not include additions to the Program +which: (i) are separate modules of software distributed in conjunction +with the Program under their own license agreement, and (ii) +are not derivative works of the Program. +"Contributor" means any person or entity that distributes the +Program. +"Licensed Patents" mean patent claims licensable by a Contributor +which are necessarily infringed by the use or sale of its Contribution +alone or when combined with the Program. +"Program" means the Contributions distributed in accordance with +this Agreement. +"Recipient" means anyone who receives the Program under this +Agreement, including all Contributors. +2. GRANT OF RIGHTS +a) Subject to the terms of this Agreement, each Contributor hereby +grants Recipient a non-exclusive, worldwide, royalty-free copyright +license to reproduce, prepare derivative works of, publicly display, +publicly perform, distribute and sublicense the Contribution +of such Contributor, if any, and such derivative works, in source +code and object code form. +b) Subject to the terms of this Agreement, each Contributor hereby +grants Recipient a non-exclusive, worldwide, royalty-free patent +license under Licensed Patents to make, use, sell, offer to sell, +import and otherwise transfer the Contribution of such Contributor, +if any, in source code and object code form. This patent license +shall apply to the combination of the Contribution and the Program +if, at the time the Contribution is added by the Contributor, +such addition of the Contribution causes such combination to +be covered by the Licensed Patents. The patent license shall +not apply to any other combinations which include the Contribution. +No hardware per se is licensed hereunder. +c) Recipient understands that although each Contributor grants +the licenses to its Contributions set forth herein, no assurances +are provided by any Contributor that the Program does not infringe +the patent or other intellectual property rights of any other +entity. Each Contributor disclaims any liability to Recipient +for claims brought by any other entity based on infringement +of intellectual property rights or otherwise. As a condition +to exercising the rights and licenses granted hereunder, each +Recipient hereby assumes sole responsibility to secure any other +intellectual property rights needed, if any. For example, if +a third party patent license is required to allow Recipient to +distribute the Program, it is Recipient's responsibility to acquire +that license before distributing the Program. +d) Each Contributor represents that to its knowledge it has sufficient +copyright rights in its Contribution, if any, to grant the copyright +license set forth in this Agreement. +3. REQUIREMENTS +A Contributor may choose to distribute the Program in object +code form under its own license agreement, provided that: +a) it complies with the terms and conditions of this Agreement; +and +b) its license agreement: +i) effectively disclaims on behalf of all Contributors all warranties +and conditions, express and implied, including warranties or +conditions of title and non-infringement, and implied warranties +or conditions of merchantability and fitness for a particular +purpose; +ii) effectively excludes on behalf of all Contributors all liability +for damages, including direct, indirect, special, incidental +and consequential damages, such as lost profits; +iii) states that any provisions which differ from this Agreement +are offered by that Contributor alone and not by any other party; +and +iv) states that source code for the Program is available from +such Contributor, and informs licensees how to obtain it in a +reasonable manner on or through a medium customarily used for +software exchange. +When the Program is made available in source code form: +a) it must be made available under this Agreement; and +b) a copy of this Agreement must be included with each copy of +the Program. +Contributors may not remove or alter any copyright notices contained +within the Program. +Each Contributor must identify itself as the originator of its +Contribution, if any, in a manner that reasonably allows subsequent +Recipients to identify the originator of the Contribution. +4. COMMERCIAL DISTRIBUTION +Commercial distributors of software may accept certain responsibilities +with respect to end users, business partners and the like. While +this license is intended to facilitate the commercial use of +the Program, the Contributor who includes the Program in a commercial +product offering should do so in a manner which does not create +potential liability for other Contributors. Therefore, if a Contributor +includes the Program in a commercial product offering, such Contributor +("Commercial Contributor") hereby agrees to defend and indemnify +every other Contributor ("Indemnified Contributor") against any +losses, damages and costs (collectively "Losses") arising from +claims, lawsuits and other legal actions brought by a third party +against the Indemnified Contributor to the extent caused by the +acts or omissions of such Commercial Contributor in connection +with its distribution of the Program in a commercial product +offering. The obligations in this section do not apply to any +claims or Losses relating to any actual or alleged intellectual +property infringement. In order to qualify, an Indemnified Contributor +must: a) promptly notify the Commercial Contributor in writing +of such claim, and b) allow the Commercial Contributor to control, +and cooperate with the Commercial Contributor in, the defense +and any related settlement negotiations. The Indemnified Contributor +may participate in any such claim at its own expense. +For example, a Contributor might include the Program in a commercial +product offering, Product X. That Contributor is then a Commercial +Contributor. If that Commercial Contributor then makes performance +claims, or offers warranties related to Product X, those performance +claims and warranties are such Commercial Contributor's responsibility +alone. Under this section, the Commercial Contributor would have +to defend claims against the other Contributors related to those +performance claims and warranties, and if a court requires any +other Contributor to pay any damages as a result, the Commercial +Contributor must pay those damages. +5. NO WARRANTY +EXCEPT AS EXPRESSLY SET FORTH IN THIS AGREEMENT, THE PROGRAM +IS PROVIDED ON AN "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS +OF ANY KIND, EITHER EXPRESS OR IMPLIED INCLUDING, WITHOUT LIMITATION, +ANY WARRANTIES OR CONDITIONS OF TITLE, NON-INFRINGEMENT, MERCHANTABILITY +OR FITNESS FOR A PARTICULAR PURPOSE. Each Recipient is solely +responsible for determining the appropriateness of using and +distributing the Program and assumes all risks associated with +its exercise of rights under this Agreement , including but not +limited to the risks and costs of program errors, compliance +with applicable laws, damage to or loss of data, programs or +equipment, and unavailability or interruption of operations. +6. DISCLAIMER OF LIABILITY +EXCEPT AS EXPRESSLY SET FORTH IN THIS AGREEMENT, NEITHER RECIPIENT +NOR ANY CONTRIBUTORS SHALL HAVE ANY LIABILITY FOR ANY DIRECT, +INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES +(INCLUDING WITHOUT LIMITATION LOST PROFITS), HOWEVER CAUSED AND +ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, +OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY +OUT OF THE USE OR DISTRIBUTION OF THE PROGRAM OR THE EXERCISE +OF ANY RIGHTS GRANTED HEREUNDER, EVEN IF ADVISED OF THE POSSIBILITY +OF SUCH DAMAGES. +7. GENERAL +If any provision of this Agreement is invalid or unenforceable +under applicable law, it shall not affect the validity or enforceability +of the remainder of the terms of this Agreement, and without +further action by the parties hereto, such provision shall be +reformed to the minimum extent necessary to make such provision +valid and enforceable. +If Recipient institutes patent litigation against any entity +(including a cross-claim or counterclaim in a lawsuit) alleging +that the Program itself (excluding combinations of the Program +with other software or hardware) infringes such Recipient's patent(s), +then such Recipient's rights granted under Section 2(b) shall +terminate as of the date such litigation is filed. +All Recipient's rights under this Agreement shall terminate if +it fails to comply with any of the material terms or conditions +of this Agreement and does not cure such failure in a reasonable +period of time after becoming aware of such noncompliance. If +all Recipient's rights under this Agreement terminate, Recipient +agrees to cease use and distribution of the Program as soon as +reasonably practicable. However, Recipient's obligations under +this Agreement and any licenses granted by Recipient relating +to the Program shall continue and survive. +Everyone is permitted to copy and distribute copies of this Agreement, +but in order to avoid inconsistency the Agreement is copyrighted +and may only be modified in the following manner. The Agreement +Steward reserves the right to publish new versions (including +revisions) of this Agreement from time to time. No one other +than the Agreement Steward has the right to modify this Agreement. +The Eclipse Foundation is the initial Agreement Steward. The +Eclipse Foundation may assign the responsibility to serve as +the Agreement Steward to a suitable separate entity. Each new +version of the Agreement will be given a distinguishing version +number. The Program (including Contributions) may always be distributed +subject to the version of the Agreement under which it was received. +In addition, after a new version of the Agreement is published, +Contributor may elect to distribute the Program (including its +Contributions) under the new version. Except as expressly stated +in Sections 2(a) and 2(b) above, Recipient receives no rights +or licenses to the intellectual property of any Contributor under +this Agreement, whether expressly, by implication, estoppel or +otherwise. All rights in the Program not expressly granted under +this Agreement are reserved. +This Agreement is governed by the laws of the State of New York +and the intellectual property laws of the United States of America. +No party to this Agreement will bring a legal action under this +Agreement more than one year after the cause of action arose. +Each party waives its rights to a jury trial in any resulting +litigation. + </license> + + <requires> + <import plugin="org.eclipse.ui" version="3.5.0" match="compatible"/> + <import plugin="org.eclipse.ui.ide" version="3.5.0" match="compatible"/> + <import plugin="org.eclipse.ui.views" version="3.5.0" match="compatible"/> + <import plugin="org.eclipse.core.runtime" version="3.5.0" match="compatible"/> + <import plugin="org.eclipse.core.databinding" version="1.2.0" match="compatible"/> + <import plugin="org.eclipse.jface.databinding" version="1.2.1" match="compatible"/> + <import plugin="org.eclipse.core.databinding.beans" version="1.1.1" match="compatible"/> + <import plugin="org.eclipse.gef" version="3.7.0" match="compatible"/> + <import plugin="de.prob.core" version="9.3.0" match="equivalent"/> + <import plugin="org.eventb.core" version="2.1.0"/> + <import plugin="org.rodinp.core" version="1.3.1"/> + <import plugin="de.prob.ui" version="7.3.0" match="equivalent"/> + <import plugin="org.eclipse.core.resources" version="3.5.0" match="compatible"/> + <import plugin="org.eclipse.core.expressions" version="3.4.101" match="compatible"/> + <import plugin="org.eclipse.gef" version="3.5.0" match="compatible"/> + <import plugin="org.eclipse.ui.navigator" version="3.5.0" match="greaterOrEqual"/> + </requires> + + <plugin + id="de.bmotionstudio.gef.editor" + download-size="0" + install-size="0" + version="0.0.0" + unpack="false"/> + + <plugin + id="de.prob.core" + download-size="0" + install-size="0" + version="0.0.0"/> + + <plugin + id="de.prob.plugin" + download-size="0" + install-size="0" + version="0.0.0" + fragment="true" + unpack="false"/> + + <plugin + id="de.prob.ui" + download-size="0" + install-size="0" + version="0.0.0" + unpack="false"/> + + <plugin + id="de.bmotionstudio.rodin" + download-size="0" + install-size="0" + version="0.0.0" + fragment="true" + unpack="false"/> + +</feature> diff --git a/settings.gradle b/settings.gradle index bb2187c38344f1fac923b7dee971552ee4cdd523..b488c61bc8301f8a4a686f9ad23d2b6109f7d62a 100644 --- a/settings.gradle +++ b/settings.gradle @@ -1,2 +1,2 @@ -include 'de.prob.core', 'de.bmotionstudio.gef.editor' ,'de.bmotionstudio.rodin', 'de.bmotionstudio.help' , 'de.prob.plugin', 'de.prob.ui', 'de.prob2.feature' +include 'de.prob.core', 'de.bmotionstudio.gef.editor' ,'de.bmotionstudio.rodin', 'de.bmotionstudio.help' , 'de.prob.plugin', 'de.prob.ui', 'de.prob2.feature', 'de.prob.units', 'de.prob2.units.feature'