Commit db2ef794 authored by Jens Bendisposto's avatar Jens Bendisposto
Browse files

merged

parents d6b1a47c 9c18d3c5
/**
* (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();
}
};
}
}
......@@ -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">
......
<?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