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 5011fc7bd78081d08fc601b0dfbd99c1858390ae..5e50c4d1458751ca574cb5de2474709ff30522b2 100644
--- a/de.prob.standalone/plugin.xml
+++ b/de.prob.standalone/plugin.xml
@@ -56,6 +56,30 @@
</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"
@@ -354,11 +378,28 @@
<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
@@ -422,6 +463,42 @@
</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
@@ -445,6 +522,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">
@@ -472,6 +553,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/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/FormalModelLabelProvider.java b/de.prob.standalone/src/de/prob/standalone/internal/FormalModelLabelProvider.java
index f28f7dd05660d6c5238265595957f7e5009f5a64..9a9da9e8d573febf303a9de20a996c66da49f807 100644
--- a/de.prob.standalone/src/de/prob/standalone/internal/FormalModelLabelProvider.java
+++ b/de.prob.standalone/src/de/prob/standalone/internal/FormalModelLabelProvider.java
@@ -24,7 +24,10 @@ public class FormalModelLabelProvider implements ILabelProvider {
} else if (file.getFileExtension().equals("buc")) {
return Activator.getImageDescriptor("icons/eventb/ctx_obj.png")
.createImage();
- } else if (file.getFileExtension().equals("mch")) {
+ } else if (file.getFileExtension().equals("csp")) {
+ return Activator.getImageDescriptor("icons/csp.png")
+ .createImage();
+ } else {
return Activator.getImageDescriptor("icons/icon16.png")
.createImage();
}