Skip to content
Snippets Groups Projects
Commit 42dd4ec3 authored by Sebastian Krings's avatar Sebastian Krings
Browse files

refactoring, new command structure for unit analysis handler

parent 8eea83fc
No related branches found
No related tags found
No related merge requests found
...@@ -19,17 +19,15 @@ import org.rodinp.core.RodinDBException; ...@@ -19,17 +19,15 @@ import org.rodinp.core.RodinDBException;
import de.prob.core.Animator; import de.prob.core.Animator;
import de.prob.core.LanguageDependendAnimationPart; import de.prob.core.LanguageDependendAnimationPart;
import de.prob.core.command.internal.InternalLoadCommand;
import de.prob.core.domainobjects.MachineDescription; import de.prob.core.domainobjects.MachineDescription;
import de.prob.core.domainobjects.Operation; import de.prob.core.domainobjects.Operation;
import de.prob.core.domainobjects.ProBPreference; import de.prob.core.domainobjects.ProBPreference;
import de.prob.core.domainobjects.State; import de.prob.core.domainobjects.State;
import de.prob.core.langdep.EventBAnimatorPart; 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.exceptions.ProBException;
import de.prob.logging.Logger; import de.prob.logging.Logger;
import de.prob.parser.ISimplifiedROMap; import de.prob.parser.ISimplifiedROMap;
import de.prob.prolog.output.IPrologTermOutput;
import de.prob.prolog.output.StructuredPrologOutput; import de.prob.prolog.output.StructuredPrologOutput;
import de.prob.prolog.term.PrologTerm; import de.prob.prolog.term.PrologTerm;
...@@ -162,32 +160,4 @@ public final class LoadEventBModelCommand { ...@@ -162,32 +160,4 @@ public final class LoadEventBModelCommand {
animator.announceReset(); 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
}
}
} }
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
...@@ -8,6 +8,7 @@ package de.prob.ui.eventb; ...@@ -8,6 +8,7 @@ package de.prob.ui.eventb;
import java.util.ArrayList; import java.util.ArrayList;
import java.util.List; import java.util.List;
import java.util.Map;
import org.eclipse.core.commands.AbstractHandler; import org.eclipse.core.commands.AbstractHandler;
import org.eclipse.core.commands.ExecutionEvent; import org.eclipse.core.commands.ExecutionEvent;
...@@ -36,10 +37,15 @@ import org.rodinp.core.RodinCore; ...@@ -36,10 +37,15 @@ import org.rodinp.core.RodinCore;
import de.prob.core.Animator; import de.prob.core.Animator;
import de.prob.core.LimitedLogger; import de.prob.core.LimitedLogger;
import de.prob.core.command.ActivateUnitPluginCommand; 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.exceptions.ProBException;
import de.prob.logging.Logger; import de.prob.logging.Logger;
import de.prob.ui.PerspectiveFactory;
public class StartUnitAnalysisHandler extends AbstractHandler implements public class StartUnitAnalysisHandler extends AbstractHandler implements
IHandler { IHandler {
...@@ -101,14 +107,39 @@ public class StartUnitAnalysisHandler extends AbstractHandler implements ...@@ -101,14 +107,39 @@ public class StartUnitAnalysisHandler extends AbstractHandler implements
LimitedLogger.getLogger().log("user started animation", LimitedLogger.getLogger().log("user started animation",
rootElement.getElementName(), null); rootElement.getElementName(), null);
registerModificationListener(resource); 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(); final Animator animator = Animator.getAnimator();
try { try {
// load machine and activate plugin // load machine and activate plugin
LoadEventBModelCommand.load(animator, rootElement); final ClearMachineCommand clear = new ClearMachineCommand();
ActivateUnitPluginCommand.activateUnitPlugin(animator); 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 // 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) { } catch (ProBException e) {
e.notifyUserOnce(); e.notifyUserOnce();
throw new ExecutionException("Loading the machine failed", e); throw new ExecutionException("Loading the machine failed", e);
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment