Commit 9c18d3c5 authored by Jens Bendisposto's avatar Jens Bendisposto
Browse files

csp loader

parent d9568531
/**
* (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();
}
};
}
}
......@@ -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">
......
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;
}
}
......@@ -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();
}
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment