diff --git a/de.prob.core/src/de/prob/core/command/LoadEventBModelCommand.java b/de.prob.core/src/de/prob/core/command/LoadEventBModelCommand.java index 316d436cfb029a75fd3232548ee3415f178854a1..78335f27dbe8219e1129b5286e771ac514283b15 100644 --- a/de.prob.core/src/de/prob/core/command/LoadEventBModelCommand.java +++ b/de.prob.core/src/de/prob/core/command/LoadEventBModelCommand.java @@ -19,17 +19,15 @@ import org.rodinp.core.RodinDBException; import de.prob.core.Animator; import de.prob.core.LanguageDependendAnimationPart; +import de.prob.core.command.internal.InternalLoadCommand; import de.prob.core.domainobjects.MachineDescription; import de.prob.core.domainobjects.Operation; import de.prob.core.domainobjects.ProBPreference; import de.prob.core.domainobjects.State; import de.prob.core.langdep.EventBAnimatorPart; -import de.prob.core.translator.TranslationFailedException; -import de.prob.eventb.translator.TranslatorFactory; 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.PrologTerm; @@ -162,32 +160,4 @@ public final class LoadEventBModelCommand { animator.announceReset(); } } - - private static class InternalLoadCommand implements IComposableCommand { - private final IEventBRoot model; - - public InternalLoadCommand(final IEventBRoot model) { - this.model = model; - } - - @Override - public void writeCommand(final IPrologTermOutput pto) - throws CommandException { - try { - TranslatorFactory.translate(model, pto); - } catch (TranslationFailedException e) { - throw new CommandException( - "Translation from Event-B to ProB's internal representation failed", - e); - } - } - - @Override - public void processResult( - final ISimplifiedROMap<String, PrologTerm> bindings) - throws CommandException { - // there are no results to process - } - - } } diff --git a/de.prob.core/src/de/prob/core/command/internal/InternalLoadCommand.java b/de.prob.core/src/de/prob/core/command/internal/InternalLoadCommand.java new file mode 100644 index 0000000000000000000000000000000000000000..2a3eaf98d4fd0b82a4a4718c0878d2366bf08e67 --- /dev/null +++ b/de.prob.core/src/de/prob/core/command/internal/InternalLoadCommand.java @@ -0,0 +1,39 @@ +package de.prob.core.command.internal; + +import org.eventb.core.IEventBRoot; + +import de.prob.core.command.CommandException; +import de.prob.core.command.IComposableCommand; +import de.prob.core.translator.TranslationFailedException; +import de.prob.eventb.translator.TranslatorFactory; +import de.prob.parser.ISimplifiedROMap; +import de.prob.prolog.output.IPrologTermOutput; +import de.prob.prolog.term.PrologTerm; + +public final class InternalLoadCommand implements IComposableCommand { + private final IEventBRoot model; + + public InternalLoadCommand(final IEventBRoot model) { + this.model = model; + } + + @Override + public void writeCommand(final IPrologTermOutput pto) + throws CommandException { + try { + TranslatorFactory.translate(model, pto); + } catch (TranslationFailedException e) { + throw new CommandException( + "Translation from Event-B to ProB's internal representation failed", + e); + } + } + + @Override + public void processResult( + final ISimplifiedROMap<String, PrologTerm> bindings) + throws CommandException { + // there are no results to process + } + +} \ No newline at end of file diff --git a/de.prob.ui/src/de/prob/ui/eventb/StartUnitAnalysisHandler.java b/de.prob.ui/src/de/prob/ui/eventb/StartUnitAnalysisHandler.java index 1566f67477669356a926fe058f49d19c5c7333b9..954e243608cba7c1305f5242f912b7094183679f 100644 --- a/de.prob.ui/src/de/prob/ui/eventb/StartUnitAnalysisHandler.java +++ b/de.prob.ui/src/de/prob/ui/eventb/StartUnitAnalysisHandler.java @@ -8,6 +8,7 @@ package de.prob.ui.eventb; import java.util.ArrayList; import java.util.List; +import java.util.Map; import org.eclipse.core.commands.AbstractHandler; import org.eclipse.core.commands.ExecutionEvent; @@ -36,10 +37,15 @@ import org.rodinp.core.RodinCore; import de.prob.core.Animator; import de.prob.core.LimitedLogger; import de.prob.core.command.ActivateUnitPluginCommand; -import de.prob.core.command.LoadEventBModelCommand; +import de.prob.core.command.ClearMachineCommand; +import de.prob.core.command.ComposedCommand; +import de.prob.core.command.SetPreferencesCommand; +import de.prob.core.command.StartAnimationCommand; +import de.prob.core.command.internal.InternalLoadCommand; +import de.prob.core.domainobjects.State; +import de.prob.core.domainobjects.Variable; import de.prob.exceptions.ProBException; import de.prob.logging.Logger; -import de.prob.ui.PerspectiveFactory; public class StartUnitAnalysisHandler extends AbstractHandler implements IHandler { @@ -101,14 +107,39 @@ public class StartUnitAnalysisHandler extends AbstractHandler implements LimitedLogger.getLogger().log("user started animation", rootElement.getElementName(), null); registerModificationListener(resource); - PerspectiveFactory.openPerspective(); + + // do not change perspective - just start animator and shut it down + // after the analysis + // PerspectiveFactory.openPerspective(); final Animator animator = Animator.getAnimator(); try { // load machine and activate plugin - LoadEventBModelCommand.load(animator, rootElement); - ActivateUnitPluginCommand.activateUnitPlugin(animator); + final ClearMachineCommand clear = new ClearMachineCommand(); + final SetPreferencesCommand setPrefs = SetPreferencesCommand + .createSetPreferencesCommand(animator); + + final InternalLoadCommand load = new InternalLoadCommand( + rootElement); + final StartAnimationCommand start = new StartAnimationCommand(); + + final ActivateUnitPluginCommand activatePlugin = new ActivateUnitPluginCommand(); + + final ComposedCommand composed = new ComposedCommand(clear, + setPrefs, load, start, activatePlugin); + + animator.execute(composed); + // TODO: get resulting state and fill attributes + State state = animator.getCurrentState(); + Map<String, Variable> values = state.getValues(); + + for (String s : values.keySet()) { + System.out.println(s); + } + + // shutdown animator + animator.shutdown(); } catch (ProBException e) { e.notifyUserOnce(); throw new ExecutionException("Loading the machine failed", e);