From 42dd4ec35d91dc1ea6d70dc2f5d3b77373ba2a33 Mon Sep 17 00:00:00 2001
From: Sebastian Krings <sebastian@krin.gs>
Date: Thu, 20 Dec 2012 12:09:05 +0100
Subject: [PATCH] refactoring, new command structure for unit analysis handler
---
.../core/command/LoadEventBModelCommand.java | 32 +--------------
.../command/internal/InternalLoadCommand.java | 39 ++++++++++++++++++
.../ui/eventb/StartUnitAnalysisHandler.java | 41 ++++++++++++++++---
3 files changed, 76 insertions(+), 36 deletions(-)
create mode 100644 de.prob.core/src/de/prob/core/command/internal/InternalLoadCommand.java
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 316d436c..78335f27 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 00000000..2a3eaf98
--- /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 1566f674..954e2436 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);
--
GitLab