diff --git a/de.prob.core/prob/macos/lib/cspm b/de.prob.core/prob/macos/lib/cspm
new file mode 100755
index 0000000000000000000000000000000000000000..e03e7ffe265fcc9ee586e86f84967e68780f1062
Binary files /dev/null and b/de.prob.core/prob/macos/lib/cspm differ
diff --git a/de.prob.core/src/de/prob/core/command/LoadCspModelCommand.java b/de.prob.core/src/de/prob/core/command/LoadCspModelCommand.java
new file mode 100644
index 0000000000000000000000000000000000000000..c28bf6cefe80c5111cda2bef18b4bf23c3f677c9
--- /dev/null
+++ b/de.prob.core/src/de/prob/core/command/LoadCspModelCommand.java
@@ -0,0 +1,132 @@
+/**
+ * (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 java.io.File;
+import java.io.IOException;
+import java.util.Collection;
+import java.util.HashSet;
+import java.util.Iterator;
+import java.util.Set;
+
+import org.eventb.core.IEventBRoot;
+import org.osgi.service.prefs.BackingStoreException;
+import org.osgi.service.prefs.Preferences;
+
+import de.be4.classicalb.core.parser.BParser;
+import de.be4.classicalb.core.parser.analysis.prolog.RecursiveMachineLoader;
+import de.be4.classicalb.core.parser.exceptions.BException;
+import de.be4.classicalb.core.parser.node.Start;
+import de.prob.core.Animator;
+import de.prob.core.domainobjects.Operation;
+import de.prob.core.domainobjects.ProBPreference;
+import de.prob.core.domainobjects.State;
+import de.prob.exceptions.ProBException;
+import de.prob.logging.Logger;
+import de.prob.parser.ISimplifiedROMap;
+import de.prob.prolog.output.IPrologTermOutput;
+import de.prob.prolog.output.StructuredPrologOutput;
+import de.prob.prolog.term.CompoundPrologTerm;
+import de.prob.prolog.term.ListPrologTerm;
+import de.prob.prolog.term.PrologTerm;
+
+/**
+ * Command to load a new Event B Model for animation.
+ */
+public final class LoadCspModelCommand {
+
+ private static boolean preferencesAlreadyCleanedUp = false;
+
+ private LoadCspModelCommand() {
+ throw new UnsupportedOperationException("Do not instantiate this class");
+ }
+
+ private LoadCspModelCommand(final IEventBRoot model) {
+ }
+
+
+ private static void removeObsoletePreferences(final Animator animator)
+ throws ProBException {
+ if (!preferencesAlreadyCleanedUp) {
+ // get all preference names from ProB
+ Collection<ProBPreference> prefs = GetPreferencesCommand
+ .getPreferences(animator);
+ Set<String> probPrefNames = new HashSet<String>();
+ for (ProBPreference probpref : prefs) {
+ probPrefNames.add(probpref.name);
+ }
+ // now check all stored (in Eclipse's store) preferences
+ // if they still exist
+ Preferences preferences = SetPreferencesCommand.getPreferences();
+ try {
+ boolean foundObsoletePreference = false;
+ for (String prefname : preferences.keys()) {
+ if (!probPrefNames.contains(prefname)) {
+ // preference does not exists anymore
+ preferences.remove(prefname);
+ foundObsoletePreference = true;
+ String message = "removed obsolete preference from preferences store: "
+ + prefname;
+ Logger.info(message);
+ }
+ }
+ if (foundObsoletePreference) {
+ preferences.flush();
+ }
+ } catch (BackingStoreException e) {
+ Logger.notifyUser("Error while accessing ProB Preferences", e);
+ }
+ preferencesAlreadyCleanedUp = true;
+ }
+ }
+
+ public static void load(final Animator animator, final File model, String name)
+ throws ProBException {
+ animator.resetDirty();
+ removeObsoletePreferences(animator);
+
+ final ClearMachineCommand clear = new ClearMachineCommand();
+ final SetPreferencesCommand setPrefs = SetPreferencesCommand
+ .createSetPreferencesCommand(animator);
+ final IComposableCommand load = getLoadCommand(model, name);
+ final StartAnimationCommand start = new StartAnimationCommand();
+ final ExploreStateCommand explore = new ExploreStateCommand("root");
+
+ final ComposedCommand composed = new ComposedCommand(clear, setPrefs,
+ load, start, explore);
+
+ animator.execute(composed);
+
+ final State commandResult = explore.getState();
+ animator.announceCurrentStateChanged(commandResult,
+ Operation.NULL_OPERATION);
+ }
+
+ private static IComposableCommand getLoadCommand(final File model, final String name)
+ throws ProBException {
+ return new IComposableCommand() {
+
+ @Override
+ public void writeCommand(final IPrologTermOutput pto) throws CommandException {
+ pto.openTerm("load_cspm_spec_from_cspm_file");
+ pto.printAtom(model.getAbsolutePath());
+ pto.closeTerm();
+ pto.printAtom("start_animation");
+ }
+
+ @Override
+ public void processResult(
+ final ISimplifiedROMap<String, PrologTerm> bindings) {
+ Animator.getAnimator().announceReset();
+ }
+ };
+
+
+ }
+
+
+}
diff --git a/de.prob.standalone/icons/csp.png b/de.prob.standalone/icons/csp.png
new file mode 100644
index 0000000000000000000000000000000000000000..26d3aeab2cbee46432ebb180e112bb32e69589d4
Binary files /dev/null and b/de.prob.standalone/icons/csp.png differ
diff --git a/de.prob.standalone/plugin.xml b/de.prob.standalone/plugin.xml
index 26b13886c94db6f78137c68f8be0ff5aee0b74e8..92814b534ed33b9e2dfd8b01d9ecc5716efe61f7 100644
--- a/de.prob.standalone/plugin.xml
+++ b/de.prob.standalone/plugin.xml
@@ -336,9 +336,65 @@
name="ProB Navigation Content Provider"
priority="normal">
<triggerPoints>
- <instanceof
- value="org.eclipse.core.resources.IResource">
- </instanceof>
+ <or>
+ <and>
+ <instanceof
+ value="org.eclipse.core.resources.IResource">
+ </instanceof>
+ <test
+ forcePluginActivation="true"
+ property="org.eclipse.core.resources.extension"
+ value="bum">
+ </test>
+ </and>
+ <and>
+ <instanceof
+ value="org.eclipse.core.resources.IResource">
+ </instanceof>
+ <test
+ forcePluginActivation="true"
+ property="org.eclipse.core.resources.extension"
+ value="buc">
+ </test>
+ </and>
+ <and>
+ <instanceof
+ value="org.eclipse.core.resources.IResource">
+ </instanceof>
+ <or>
+ <test
+ forcePluginActivation="true"
+ property="org.eclipse.core.resources.extension"
+ value="mch">
+ </test>
+ <test
+ forcePluginActivation="true"
+ property="org.eclipse.core.resources.extension"
+ value="ref">
+ </test>
+ <test
+ forcePluginActivation="true"
+ property="org.eclipse.core.resources.extension"
+ value="imp">
+ </test>
+ <test
+ forcePluginActivation="true"
+ property="org.eclipse.core.resources.extension"
+ value="csp">
+ </test>
+ </or>
+ </and>
+ <and>
+ <instanceof
+ value="org.eclipse.core.resources.IResource">
+ </instanceof>
+ <test
+ forcePluginActivation="true"
+ property="org.eclipse.core.resources.extension"
+ value="bmso">
+ </test>
+ </and>
+ </or>
</triggerPoints>
</navigatorContent>
<commonFilter
@@ -351,33 +407,90 @@
<instanceof
value="org.eclipse.core.resources.IResource">
</instanceof>
- <or>
- <test
- forcePluginActivation="true"
- property="org.eclipse.core.resources.extension"
- value="bcc">
- </test>
- <test
- forcePluginActivation="true"
- property="org.eclipse.core.resources.extension"
- value="bpo">
- </test>
- <test
- forcePluginActivation="true"
- property="org.eclipse.core.resources.extension"
- value="bpr">
- </test>
- <test
- forcePluginActivation="true"
- property="org.eclipse.core.resources.extension"
- value="bps">
- </test>
- <test
- forcePluginActivation="true"
- property="org.eclipse.core.resources.extension"
- value="bcm">
- </test>
- </or>
+ <not>
+ <and>
+ <instanceof
+ value="org.eclipse.core.resources.IFile">
+ </instanceof>
+ <test
+ forcePluginActivation="true"
+ property="org.eclipse.core.resources.extension"
+ value="buc">
+ </test>
+ </and>
+ </not>
+ <not>
+ <and>
+ <instanceof
+ value="org.eclipse.core.resources.IFile">
+ </instanceof>
+ <test
+ forcePluginActivation="true"
+ property="org.eclipse.core.resources.extension"
+ value="bum">
+ </test>
+ </and>
+ </not>
+ <not>
+ <and>
+ <instanceof
+ value="org.eclipse.core.resources.IFile">
+ </instanceof>
+ <test
+ forcePluginActivation="true"
+ property="org.eclipse.core.resources.extension"
+ value="bmso">
+ </test>
+ </and>
+ </not>
+ <not>
+ <and>
+ <instanceof
+ value="org.eclipse.core.resources.IFile">
+ </instanceof>
+ <test
+ forcePluginActivation="true"
+ property="org.eclipse.core.resources.extension"
+ value="ref">
+ </test>
+ </and>
+ </not>
+ <not>
+ <and>
+ <instanceof
+ value="org.eclipse.core.resources.IFile">
+ </instanceof>
+ <test
+ forcePluginActivation="true"
+ property="org.eclipse.core.resources.extension"
+ value="imp">
+ </test>
+ </and>
+ </not>
+ <not>
+ <and>
+ <instanceof
+ value="org.eclipse.core.resources.IFile">
+ </instanceof>
+ <test
+ forcePluginActivation="true"
+ property="org.eclipse.core.resources.extension"
+ value="csp">
+ </test>
+ </and>
+ </not>
+ <not>
+ <and>
+ <instanceof
+ value="org.eclipse.core.resources.IFile">
+ </instanceof>
+ <test
+ forcePluginActivation="true"
+ property="org.eclipse.core.resources.extension"
+ value="mch">
+ </test>
+ </and>
+ </not>
</and>
</or>
</filterExpression>
@@ -389,6 +502,10 @@
id="de.prob.command.startClassicalBAnimation"
name="Classical-B Animate / Model Check">
</command>
+ <command
+ id="de.prob.command.startCspAnimation"
+ name="CSP Animate / Model Check">
+ </command>
</extension>
<extension
point="org.eclipse.ui.handlers">
@@ -416,6 +533,30 @@
</with>
</enabledWhen>
</handler>
+ <handler
+ commandId="de.prob.command.startCspAnimation">
+ <class
+ class="de.prob.standalone.handler.StartCspAnimationHandler">
+ </class>
+ <enabledWhen>
+ <with
+ variable="selection">
+ <iterate
+ operator="or">
+ <and>
+ <instanceof
+ value="org.eclipse.core.resources.IResource">
+ </instanceof>
+ <test
+ forcePluginActivation="true"
+ property="org.eclipse.core.resources.extension"
+ value="csp">
+ </test>
+ </and>
+ </iterate>
+ </with>
+ </enabledWhen>
+ </handler>
</extension>
<extension
point="de.bmotionstudio.gef.editor.language">
diff --git a/de.prob.standalone/plugin.xml.orig b/de.prob.standalone/plugin.xml.orig
new file mode 100644
index 0000000000000000000000000000000000000000..0130fefbf2bc5c9c2e87cb6374ac8db7b41fe395
--- /dev/null
+++ b/de.prob.standalone/plugin.xml.orig
@@ -0,0 +1,660 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<?eclipse version="3.4"?>
+<plugin>
+
+
+ <extension
+ point="org.eclipse.ui.menus">
+ <menuContribution
+ locationURI="menu:org.eclipse.ui.main.menu?before=help">
+ <menu
+ id="contact"
+ label="Contact"
+ mnemonic="C">
+ </menu>
+ </menuContribution>
+ <menuContribution
+ locationURI="toolbar:org.eclipse.ui.main.toolbar">
+ <toolbar
+ id="probtoolbar">
+ </toolbar>
+ </menuContribution>
+ <menuContribution
+ locationURI="popup:de.prob.standalone.navigatorview">
+ <separator
+ name="de.prob.ui.separator2"
+ visible="true">
+ </separator>
+ <command
+ commandId="de.prob.ui.starteventbanimation"
+ icon="icons/icon16.png"
+ label="Start Animation / Model Checking"
+ style="push">
+ <visibleWhen>
+ <with
+ variable="selection">
+ <iterate
+ operator="or">
+ <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>
+ </iterate>
+ </with>
+ </visibleWhen>
+ </command>
+ <command
+ commandId="de.prob.command.startCspAnimation"
+ icon="icons/icon16.png"
+ label="Start Animation / Model Checking"
+ style="push">
+ <visibleWhen>
+ <with
+ variable="selection">
+ <iterate
+ operator="or">
+ <and>
+ <instanceof
+ value="org.eclipse.core.resources.IResource">
+ </instanceof>
+ <test
+ forcePluginActivation="true"
+ property="org.eclipse.core.resources.extension"
+ value="csp">
+ </test>
+ </and>
+ </iterate>
+ </with>
+ </visibleWhen>
+ </command>
+ <command
+ commandId="de.prob.command.startClassicalBAnimation"
+ icon="icons/icon16.png"
+ label="Start Animation / Model Checking"
+ style="push">
+ <visibleWhen>
+ <with
+ variable="selection">
+ <iterate
+ operator="or">
+ <and>
+ <instanceof
+ value="org.eclipse.core.resources.IResource">
+ </instanceof>
+ <or>
+ <test
+ forcePluginActivation="true"
+ property="org.eclipse.core.resources.extension"
+ value="mch">
+ </test>
+ <test
+ forcePluginActivation="true"
+ property="org.eclipse.core.resources.extension"
+ value="ref">
+ </test>
+ </or>
+ </and>
+ </iterate>
+ </with>
+ </visibleWhen>
+ </command>
+ <command
+ commandId="de.bmotionstudio.command.startVisualizationFromFile"
+ icon="icons/bms/bmsrun16.png"
+ label="Start Visualization"
+ style="push">
+ <visibleWhen>
+ <with
+ variable="selection">
+ <iterate
+ operator="or">
+ <and>
+ <instanceof
+ value="org.eclipse.core.resources.IResource">
+ </instanceof>
+ <test
+ forcePluginActivation="true"
+ property="org.eclipse.core.resources.extension"
+ value="bmso">
+ </test>
+ </and>
+ </iterate>
+ </with>
+ </visibleWhen>
+ </command>
+ <separator
+ name="de.prob.ui.separator1"
+ visible="true">
+ </separator>
+ </menuContribution>
+ <menuContribution
+ locationURI="menu:file">
+ <command
+ commandId="org.eclipse.ui.newWizard"
+ label="New"
+ style="push">
+ </command>
+ <separator
+ name="de.prob.standalone.separator1"
+ visible="true">
+ </separator>
+ <command
+ commandId="org.eclipse.ui.file.save"
+ label="Save"
+ style="push">
+ </command>
+ <command
+ commandId="org.eclipse.ui.file.saveAll"
+ label="Save All"
+ style="push">
+ </command>
+ <separator
+ name="de.prob.standalone.separator2"
+ visible="true">
+ </separator>
+ <command
+ commandId="org.eclipse.ui.file.close"
+ label="Close"
+ style="push">
+ </command>
+ <command
+ commandId="org.eclipse.ui.file.closeAll"
+ label="Close All"
+ style="push">
+ </command>
+ <separator
+ name="de.prob.standalone.separator3"
+ visible="true">
+ </separator>
+ <command
+ commandId="org.eclipse.ui.file.refresh"
+ label="Refresh"
+ style="push">
+ </command>
+ </menuContribution>
+ </extension>
+
+
+
+
+ <extension
+ id="application"
+ point="org.eclipse.core.runtime.applications">
+ <application>
+ <run
+ class="de.prob.standalone.Application">
+ </run>
+ </application>
+ </extension>
+ <extension
+ point="org.eclipse.ui.perspectives">
+ <perspective
+ class="de.prob.standalone.internal.AnimationPerspective"
+ icon="icons/icon16.png"
+ id="de.prob.ui.perspective"
+ name="Animation">
+ </perspective>
+ <perspective
+ class="de.prob.standalone.internal.VisualizationEditPerspective"
+ icon="icons/bms/bms16.png"
+ id="de.bmotionstudio.perspective.edit"
+ name="Visualization">
+ </perspective>
+ <perspective
+ class="de.prob.standalone.internal.VisualizationRunPerspective"
+ icon="icons/bms/bmsrun16.png"
+ id="de.bmotionstudio.perspective.run"
+ name="Visualization">
+ </perspective>
+ </extension>
+ <!-- <extension
+ point="org.eclipse.ui.actionSets">
+ <actionSet
+ label="ProB Demo Action Set"
+ visible="true"
+ id="demoActionSet">
+ <menu
+ label="File"
+ id="sampleMenu">
+ <separator
+ name="fileGroup">
+ </separator>
+ </menu>
+ <action
+ label="Open File"
+ class="de.prob.standalone.actions.OpenFileAction"
+ tooltip="Open a file"
+ menubarPath="sampleMenu/fileGroup"
+ id="openFileAction">
+ </action>
+ <action
+ label="Open Event-B Model"
+ class="de.prob.standalone.actions.OpenEventBFileAction"
+ tooltip="Open an Event-B Model"
+ menubarPath="sampleMenu/fileGroup"
+ id="openFileAction">
+ </action>
+ </actionSet>
+ </extension>
+
+ -->
+ <extension
+ id="prob"
+ point="org.eclipse.core.runtime.products">
+ <product
+ application="de.prob.standalone.application"
+ name="ProB">
+ <property
+ name="appName"
+ value="ProB">
+ </property>
+ <property
+ name="preferenceCustomization"
+ value="plugin_customization.ini">
+ </property>
+ <property
+ name="aboutImage"
+ value="icons/icon16.png">
+ </property>
+ <property
+ name="aboutText"
+ value="ProB: An Animator and Model Checker for B
-----------------------------------------

(C) 2000-2010 Michael Leuschel (and many others; see below)
All rights reserved.
ProB can now be used freely for commercial, non-commercial
and academic use.
For availability of commercial support, please contact the author
(http://www.stups.uni-duesseldorf.de/~leuschel).
No re-distribution allowed. 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/).

ProB comes with ABSOLUTELY NO WARRANTY OF ANY KIND !
This software is distributed in the hope that it will be useful
but WITHOUT ANY WARRANTY. The author(s) do not accept responsibility
to anyone for the consequences of using it or for whether it serves
any particular purpose or works at all. No warranty is made about
the software or its performance.

For updates and news check:
 http://www.stups.uni-duesseldorf.de/ProB/

ProB uses state-of-the-art Prolog technology (co-routining, finite
domain constraint solvers,...) to achieve symbolic debugging,
constraint-based and temporal-logic based model checking.
The tool was partly being developed within the EPSRC grants iMoc and ABCD
and the EU grant ASAP. Further development within RODIN has been carried out.
Future developments within DEPLOY and GEPAVAS are being undertaken.

Development, Copyright and Intellectual Property Rights:
B-Kernel & Model Checker:
 Michael Leuschel, Daniel Plagge, Jens Bendisposto
Java Interface:
 Jens Bendisposto, Daniel Plagge, Michael Leuschel
B Parser:
 Fabian Fritz
B Typechecker:
 Daniel Plagge
Event-B Translator:
 Jens Bendipsoto, Daniel Plagge
ProZ, LTL model checker:
 Daniel Plagge, Michael Leuschel
ProCSP:
 Michael Leuschel, Marc Fontaine
Parser for CSP-M:
 Marc Fontaine
Nauty interface for ProB:
 Corinna Spermann, Michael Leuschel
Symmetry Hash Markers
 Michael Leuschel, Thierry Massart
ProMLA
 Dennis Winter, Michael Leuschel

Other Developers:
 Michael Butler, Carla Ferreira,
 Stephane Lo-Presti, Li Luo, Leonid Mikhailov,
 Ed Turner, Phil Turner
 

Fuzz Parser and Type Checker for Z:
 Mike Spivey
 (see http://spivey.oriel.ox.ac.uk/mike/fuzz)
Nauty library for symmetry reduction:
 Copyright (1984-2007) Brendan McKay
 http://cs.anu.edu.au/~bdm/nauty/

Known limitations:
==================
 - Unsupported features: 
 the closure operator (but closure1 is supported), tuple notation
 without parentheses a,b,c (use (a,b,c) instead), relational
 composition needs to be put inside parantheses, the VALUES clause, ...
 (see ProB Summary in About menu for which features are supported)
 - Atelier B's tree operations are not supported
 - Preconditions of operations are not automatically propagated down
 to operations in refinements and implementations
 - Refinement checker treats PRE as SELECT
 - ... possibly more ...

Notes:
======
 - To visualize state space graphs: dot from AT&T's GraphViz package has to be installed

See the FAQ.txt file for troubleshooting and frequently asked questions.">
+ </property>
+ <property
+ name="windowImages"
+ value="icons/icon16.png,icons/icon32.png,icons/icon48png,icons/icon64.png,icons/icon128.png">
+ </property>
+ <property
+ name="startupForegroundColor"
+ value="FFFFFF">
+ </property>
+ <property
+ name="startupMessageRect"
+ value="20,350,670,20">
+ </property>
+ <property
+ name="startupProgressRect"
+ value="15,370,670,20">
+ </property>
+ </product>
+ </extension>
+ <extension
+ point="org.eclipse.ui.presentationFactories">
+ <factory
+ class="de.prob.standalone.presentation.PresentationFactory"
+ id="de.prob.standalone.presentation"
+ name="ProB Presentation">
+ </factory>
+ </extension>
+
+
+ <extension
+ point="org.eclipse.ui.activities">
+ <activity id="hiddenActivity" name="Hide Eclipse UI "/>
+ <activityPatternBinding
+ activityId="hiddenActivity"
+ isEqualityPattern="false"
+ pattern="org\.eclipse\.ui\.project\..*">
+ </activityPatternBinding>
+</extension>
+ <extension
+ point="org.eclipse.ui.views">
+ <view
+ allowMultiple="false"
+ class="org.eclipse.ui.navigator.CommonNavigator"
+ id="de.prob.standalone.navigatorview"
+ name="Navigation"
+ restorable="true">
+ </view>
+ </extension>
+ <extension
+ point="org.eclipse.ui.navigator.viewer">
+ <viewer
+ viewerId="de.prob.standalone.navigatorview">
+ </viewer>
+ <viewerContentBinding
+ viewerId="de.prob.standalone.navigatorview">
+ <includes>
+ <contentExtension
+ pattern="org.eclipse.ui.navigator.resourceContent">
+ </contentExtension>
+ <contentExtension
+ pattern="org.eclipse.ui.navigator.resources.filters.*">
+ </contentExtension>
+ <contentExtension
+ pattern="de.prob.standalone.commonFilter.*">
+ </contentExtension>
+ <contentExtension
+ pattern="de.prob.standalone.navigatorContent.*">
+ </contentExtension>
+ </includes>
+ </viewerContentBinding>
+ <viewerActionBinding
+ viewerId="de.prob.standalone.navigatorview">
+ <includes>
+ <actionExtension
+ pattern="org.eclipse.ui.navigator.resources.*">
+ </actionExtension></includes>
+ </viewerActionBinding>
+ </extension>
+ <extension
+ point="org.eclipse.ui.navigator.navigatorContent">
+ <navigatorContent
+ activeByDefault="true"
+ contentProvider="de.prob.standalone.internal.ProBNavigatorContentProvider"
+ id="de.prob.standalone.navigatorContent.probContent"
+ labelProvider="de.prob.standalone.internal.ProBNavigatorLabelProvider"
+ name="ProB Navigation Content Provider"
+ priority="normal">
+ <triggerPoints>
+<<<<<<< HEAD
+ <instanceof
+ value="org.eclipse.core.resources.IResource">
+ </instanceof>
+=======
+ <or>
+ <and>
+ <instanceof
+ value="org.eclipse.core.resources.IResource">
+ </instanceof>
+ <test
+ forcePluginActivation="true"
+ property="org.eclipse.core.resources.extension"
+ value="bum">
+ </test>
+ </and>
+ <and>
+ <instanceof
+ value="org.eclipse.core.resources.IResource">
+ </instanceof>
+ <test
+ forcePluginActivation="true"
+ property="org.eclipse.core.resources.extension"
+ value="buc">
+ </test>
+ </and>
+ <and>
+ <instanceof
+ value="org.eclipse.core.resources.IResource">
+ </instanceof>
+ <or>
+ <test
+ forcePluginActivation="true"
+ property="org.eclipse.core.resources.extension"
+ value="mch">
+ </test>
+ <test
+ forcePluginActivation="true"
+ property="org.eclipse.core.resources.extension"
+ value="ref">
+ </test>
+ <test
+ forcePluginActivation="true"
+ property="org.eclipse.core.resources.extension"
+ value="imp">
+ </test>
+ <test
+ forcePluginActivation="true"
+ property="org.eclipse.core.resources.extension"
+ value="csp">
+ </test>
+ </or>
+ </and>
+ <and>
+ <instanceof
+ value="org.eclipse.core.resources.IResource">
+ </instanceof>
+ <test
+ forcePluginActivation="true"
+ property="org.eclipse.core.resources.extension"
+ value="bmso">
+ </test>
+ </and>
+ </or>
+>>>>>>> 9c18d3c58cce99fd4c0ffb41f046dcfa8f18801e
+ </triggerPoints>
+ </navigatorContent>
+ <commonFilter
+ activeByDefault="true"
+ id="de.prob.standalone.commonFilter.probFileFilter"
+ name="ProB Navigation Filter">
+ <filterExpression>
+ <or>
+ <and>
+ <instanceof
+ value="org.eclipse.core.resources.IResource">
+ </instanceof>
+<<<<<<< HEAD
+ <or>
+ <test
+ forcePluginActivation="true"
+ property="org.eclipse.core.resources.extension"
+ value="bcc">
+ </test>
+ <test
+ forcePluginActivation="true"
+ property="org.eclipse.core.resources.extension"
+ value="bpo">
+ </test>
+ <test
+ forcePluginActivation="true"
+ property="org.eclipse.core.resources.extension"
+ value="bpr">
+ </test>
+ <test
+ forcePluginActivation="true"
+ property="org.eclipse.core.resources.extension"
+ value="bps">
+ </test>
+ <test
+ forcePluginActivation="true"
+ property="org.eclipse.core.resources.extension"
+ value="bcm">
+ </test>
+ </or>
+=======
+ <not>
+ <and>
+ <instanceof
+ value="org.eclipse.core.resources.IFile">
+ </instanceof>
+ <test
+ forcePluginActivation="true"
+ property="org.eclipse.core.resources.extension"
+ value="buc">
+ </test>
+ </and>
+ </not>
+ <not>
+ <and>
+ <instanceof
+ value="org.eclipse.core.resources.IFile">
+ </instanceof>
+ <test
+ forcePluginActivation="true"
+ property="org.eclipse.core.resources.extension"
+ value="bum">
+ </test>
+ </and>
+ </not>
+ <not>
+ <and>
+ <instanceof
+ value="org.eclipse.core.resources.IFile">
+ </instanceof>
+ <test
+ forcePluginActivation="true"
+ property="org.eclipse.core.resources.extension"
+ value="bmso">
+ </test>
+ </and>
+ </not>
+ <not>
+ <and>
+ <instanceof
+ value="org.eclipse.core.resources.IFile">
+ </instanceof>
+ <test
+ forcePluginActivation="true"
+ property="org.eclipse.core.resources.extension"
+ value="ref">
+ </test>
+ </and>
+ </not>
+ <not>
+ <and>
+ <instanceof
+ value="org.eclipse.core.resources.IFile">
+ </instanceof>
+ <test
+ forcePluginActivation="true"
+ property="org.eclipse.core.resources.extension"
+ value="imp">
+ </test>
+ </and>
+ </not>
+ <not>
+ <and>
+ <instanceof
+ value="org.eclipse.core.resources.IFile">
+ </instanceof>
+ <test
+ forcePluginActivation="true"
+ property="org.eclipse.core.resources.extension"
+ value="csp">
+ </test>
+ </and>
+ </not>
+ <not>
+ <and>
+ <instanceof
+ value="org.eclipse.core.resources.IFile">
+ </instanceof>
+ <test
+ forcePluginActivation="true"
+ property="org.eclipse.core.resources.extension"
+ value="mch">
+ </test>
+ </and>
+ </not>
+>>>>>>> 9c18d3c58cce99fd4c0ffb41f046dcfa8f18801e
+ </and>
+ </or>
+ </filterExpression>
+ </commonFilter>
+ </extension>
+ <extension
+ point="org.eclipse.ui.commands">
+ <command
+ id="de.prob.command.startClassicalBAnimation"
+ name="Classical-B Animate / Model Check">
+ </command>
+ <command
+ id="de.prob.command.startCspAnimation"
+ name="CSP Animate / Model Check">
+ </command>
+ </extension>
+ <extension
+ point="org.eclipse.ui.handlers">
+ <handler
+ commandId="de.prob.command.startClassicalBAnimation">
+ <class
+ class="de.prob.standalone.handler.StartClassicalBAnimationHandler">
+ </class>
+ <enabledWhen>
+ <with
+ variable="selection">
+ <iterate
+ operator="or">
+ <and>
+ <instanceof
+ value="org.eclipse.core.resources.IResource">
+ </instanceof>
+ <test
+ forcePluginActivation="true"
+ property="org.eclipse.core.resources.extension"
+ value="mch">
+ </test>
+ </and>
+ </iterate>
+ </with>
+ </enabledWhen>
+ </handler>
+ <handler
+ commandId="de.prob.command.startCspAnimation">
+ <class
+ class="de.prob.standalone.handler.StartCspAnimationHandler">
+ </class>
+ <enabledWhen>
+ <with
+ variable="selection">
+ <iterate
+ operator="or">
+ <and>
+ <instanceof
+ value="org.eclipse.core.resources.IResource">
+ </instanceof>
+ <test
+ forcePluginActivation="true"
+ property="org.eclipse.core.resources.extension"
+ value="csp">
+ </test>
+ </and>
+ </iterate>
+ </with>
+ </enabledWhen>
+ </handler>
+ </extension>
+ <extension
+ point="de.bmotionstudio.gef.editor.language">
+ <language
+ id="ClassicalB"
+ service="de.prob.standalone.internal.ClassicalBLanguageService">
+ </language>
+ </extension>
+ <extension
+ point="org.eclipse.ui.editors">
+ <editor
+ class="org.eclipse.ui.editors.text.TextEditor"
+ contributorClass="org.eclipse.ui.editors.text.TextEditorActionContributor"
+ default="true"
+ extensions="bum"
+ icon="icons/eventb/mch_obj.png"
+ id="de.prob.standalone.editor.eventb.machine"
+ name="Event-B Machine Editor">
+ </editor>
+ <editor
+ class="org.eclipse.ui.editors.text.TextEditor"
+ contributorClass="org.eclipse.ui.editors.text.TextEditorActionContributor"
+ default="true"
+ extensions="buc"
+ icon="icons/eventb/ctx_obj.png"
+ id="de.prob.standalone.editor.eventb.context"
+ name="Event-B Context Editor">
+ </editor>
+ <editor
+ class="org.eclipse.ui.editors.text.TextEditor"
+ contributorClass="org.eclipse.ui.editors.text.TextEditorActionContributor"
+ default="true"
+ extensions="mch"
+ icon="icons/icon16.png"
+ id="de.prob.standalone.editor.classicalb.machine"
+ name="Classical-B Machine Editor">
+ </editor>
+ </extension>
+
+
+</plugin>
diff --git a/de.prob.standalone/src/de/prob/standalone/handler/StartCspAnimationHandler.java b/de.prob.standalone/src/de/prob/standalone/handler/StartCspAnimationHandler.java
new file mode 100644
index 0000000000000000000000000000000000000000..0fa5a2e4aff958befe54c65336f5049f148375e0
--- /dev/null
+++ b/de.prob.standalone/src/de/prob/standalone/handler/StartCspAnimationHandler.java
@@ -0,0 +1,49 @@
+package de.prob.standalone.handler;
+
+import java.io.File;
+
+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.commands.IHandlerListener;
+import org.eclipse.core.resources.IFile;
+import org.eclipse.jface.viewers.ISelection;
+import org.eclipse.jface.viewers.IStructuredSelection;
+import org.eclipse.ui.handlers.HandlerUtil;
+
+import de.prob.core.Animator;
+import de.prob.core.command.LoadClassicalBModelCommand;
+import de.prob.core.command.LoadCspModelCommand;
+import de.prob.exceptions.ProBException;
+
+public class StartCspAnimationHandler extends AbstractHandler implements IHandler {
+
+ @Override
+ public Object execute(ExecutionEvent event) throws ExecutionException {
+ ISelection fSelection = HandlerUtil.getCurrentSelection(event);
+
+ if (fSelection instanceof IStructuredSelection) {
+ final IStructuredSelection ssel = (IStructuredSelection) fSelection;
+ if (ssel.size() == 1) {
+ final Object element = ssel.getFirstElement();
+ if (element instanceof IFile) {
+ IFile f = (IFile) element;
+ String n = f.getName();
+ String name = n.substring(0,n.length()-4);
+ File file = new File(f.getLocationURI());
+ try {
+ LoadCspModelCommand.load(Animator.getAnimator(), file, name);
+ } catch (ProBException e) {
+ throw new ExecutionException(e.getLocalizedMessage(),e);
+ }
+ }
+ }
+ }
+ return null;
+ }
+
+
+
+
+}
diff --git a/de.prob.standalone/src/de/prob/standalone/internal/ProBNavigatorLabelProvider.java b/de.prob.standalone/src/de/prob/standalone/internal/ProBNavigatorLabelProvider.java
index 0b55b1214ef3e5b1f546de8fa89228fc1e593d75..b3aeab2f84c0bcec58190eb019325c04ef78f64d 100644
--- a/de.prob.standalone/src/de/prob/standalone/internal/ProBNavigatorLabelProvider.java
+++ b/de.prob.standalone/src/de/prob/standalone/internal/ProBNavigatorLabelProvider.java
@@ -1,44 +1,44 @@
-package de.prob.standalone.internal;
-
-/**
- * (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)
- * */
-
-import org.eclipse.core.resources.IFile;
-import org.eclipse.jface.viewers.ILabelProvider;
-import org.eclipse.jface.viewers.ILabelProviderListener;
-import org.eclipse.swt.graphics.Image;
-
-public class ProBNavigatorLabelProvider implements ILabelProvider {
-
- public Image getImage(final Object element) {
- return null;
- }
-
- public String getText(final Object element) {
- if (element instanceof IFile) {
- IFile file = (IFile) element;
- return file.getName().replace("." + file.getFileExtension(), "");
- }
- return null;
- }
-
- public void addListener(final ILabelProviderListener listener) {
- // do nothing
- }
-
- public void dispose() {
- // do nothing
- }
-
- public boolean isLabelProperty(final Object element, final String property) {
- return false;
- }
-
- public void removeListener(final ILabelProviderListener listener) {
- // do nothing
- }
-
-}
+package de.prob.standalone.internal;
+
+/**
+ * (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)
+ * */
+
+import org.eclipse.core.resources.IFile;
+import org.eclipse.jface.viewers.ILabelProvider;
+import org.eclipse.jface.viewers.ILabelProviderListener;
+import org.eclipse.swt.graphics.Image;
+
+public class ProBNavigatorLabelProvider implements ILabelProvider {
+
+ public Image getImage(final Object element) {
+ return null;
+ }
+
+ public String getText(final Object element) {
+ if (element instanceof IFile) {
+ IFile file = (IFile) element;
+ return file.getName().replace("." + file.getFileExtension(), "");
+ }
+ return null;
+ }
+
+ public void addListener(final ILabelProviderListener listener) {
+ // do nothing
+ }
+
+ public void dispose() {
+ // do nothing
+ }
+
+ public boolean isLabelProperty(final Object element, final String property) {
+ return false;
+ }
+
+ public void removeListener(final ILabelProviderListener listener) {
+ // do nothing
+ }
+
+}
diff --git a/de.prob.standalone/src/de/prob/standalone/internal/ProBNavigatorLabelProvider.java.orig b/de.prob.standalone/src/de/prob/standalone/internal/ProBNavigatorLabelProvider.java.orig
new file mode 100644
index 0000000000000000000000000000000000000000..c7599a6d1a0a72004d9ee859ba84454068b15912
--- /dev/null
+++ b/de.prob.standalone/src/de/prob/standalone/internal/ProBNavigatorLabelProvider.java.orig
@@ -0,0 +1,109 @@
+<<<<<<< HEAD
+package de.prob.standalone.internal;
+
+/**
+ * (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)
+ * */
+
+import org.eclipse.core.resources.IFile;
+import org.eclipse.jface.viewers.ILabelProvider;
+import org.eclipse.jface.viewers.ILabelProviderListener;
+import org.eclipse.swt.graphics.Image;
+
+public class ProBNavigatorLabelProvider implements ILabelProvider {
+
+ public Image getImage(final Object element) {
+ return null;
+ }
+
+ public String getText(final Object element) {
+ if (element instanceof IFile) {
+ IFile file = (IFile) element;
+ return file.getName().replace("." + file.getFileExtension(), "");
+ }
+ return null;
+ }
+
+ public void addListener(final ILabelProviderListener listener) {
+ // do nothing
+ }
+
+ public void dispose() {
+ // do nothing
+ }
+
+ public boolean isLabelProperty(final Object element, final String property) {
+ return false;
+ }
+
+ public void removeListener(final ILabelProviderListener listener) {
+ // do nothing
+ }
+
+}
+=======
+package de.prob.standalone.internal;
+
+/**
+ * (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)
+ * */
+
+import org.eclipse.core.resources.IFile;
+import org.eclipse.jface.viewers.ILabelProvider;
+import org.eclipse.jface.viewers.ILabelProviderListener;
+import org.eclipse.swt.graphics.Image;
+
+import de.prob.standalone.Activator;
+
+public class FormalModelLabelProvider implements ILabelProvider {
+
+ public Image getImage(final Object element) {
+ if (element instanceof IFile) {
+ IFile file = (IFile) element;
+ if (file.getFileExtension().equals("bum")) {
+ return Activator.getImageDescriptor("icons/eventb/mch_obj.png")
+ .createImage();
+ } else if (file.getFileExtension().equals("buc")) {
+ return Activator.getImageDescriptor("icons/eventb/ctx_obj.png")
+ .createImage();
+ } else if (file.getFileExtension().equals("csp")) {
+ return Activator.getImageDescriptor("icons/csp.png")
+ .createImage();
+ } else {
+ return Activator.getImageDescriptor("icons/icon16.png")
+ .createImage();
+ }
+ }
+ return null;
+ }
+
+ public String getText(final Object element) {
+ if (element instanceof IFile) {
+ IFile file = (IFile) element;
+ return file.getName().replace("." + file.getFileExtension(), "");
+ }
+ return null;
+ }
+
+ public void addListener(final ILabelProviderListener listener) {
+ // do nothing
+ }
+
+ public void dispose() {
+ // do nothing
+ }
+
+ public boolean isLabelProperty(final Object element, final String property) {
+ return false;
+ }
+
+ public void removeListener(final ILabelProviderListener listener) {
+ // do nothing
+ }
+
+}
+>>>>>>> 9c18d3c58cce99fd4c0ffb41f046dcfa8f18801e