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..6db887e7a802b2c0f78666e65959b729bc320aa9 --- /dev/null +++ b/de.prob.core/src/de/prob/core/command/LoadCspModelCommand.java @@ -0,0 +1,122 @@ +/** + * (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.util.Collection; +import java.util.HashSet; +import java.util.Set; + +import org.eventb.core.IEventBRoot; +import org.osgi.service.prefs.BackingStoreException; +import org.osgi.service.prefs.Preferences; + +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.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(); + } + }; + + } + + +} \ No newline at end of file diff --git a/de.prob.ui/src/de/prob/ui/csp/StartCSPAnimationHandler.java b/de.prob.ui/src/de/prob/ui/csp/StartCSPAnimationHandler.java new file mode 100644 index 0000000000000000000000000000000000000000..00113770cb69e5336c07a5adb98f66c41163843b --- /dev/null +++ b/de.prob.ui/src/de/prob/ui/csp/StartCSPAnimationHandler.java @@ -0,0 +1,53 @@ +/** + * (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.ui.csp; + +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.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.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; + } + + +}