From 28015f9b527610a4eed80025d04cce4e8d96643f Mon Sep 17 00:00:00 2001 From: Sebastian Krings <sebastian@krin.gs> Date: Wed, 19 Dec 2012 12:16:15 +0100 Subject: [PATCH] working on unit analysis command --- .../command/ActivateUnitPluginCommand.java | 55 ++++++ .../ui/eventb/StartUnitAnalysisHandler.java | 174 +++++++++++++++++- 2 files changed, 224 insertions(+), 5 deletions(-) create mode 100644 de.prob.core/src/de/prob/core/command/ActivateUnitPluginCommand.java diff --git a/de.prob.core/src/de/prob/core/command/ActivateUnitPluginCommand.java b/de.prob.core/src/de/prob/core/command/ActivateUnitPluginCommand.java new file mode 100644 index 00000000..c75c3a7b --- /dev/null +++ b/de.prob.core/src/de/prob/core/command/ActivateUnitPluginCommand.java @@ -0,0 +1,55 @@ +/** + * (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 de.prob.core.Animator; +import de.prob.exceptions.ProBException; +import de.prob.parser.ISimplifiedROMap; +import de.prob.prolog.output.IPrologTermOutput; +import de.prob.prolog.term.PrologTerm; + +public class ActivateUnitPluginCommand implements IComposableCommand { + + private static final ActivateCmd ACTIVATE_CMD = new ActivateCmd(); + private final GetPrologRandomSeed getRandomSeed; + private final ComposedCommand cmd; + + public ActivateUnitPluginCommand() { + this.getRandomSeed = new GetPrologRandomSeed(); + this.cmd = new ComposedCommand(getRandomSeed, ACTIVATE_CMD); + } + + public static void activateUnitPlugin(final Animator animator) + throws ProBException { + animator.execute(new ActivateUnitPluginCommand()); + } + + public void processResult( + final ISimplifiedROMap<String, PrologTerm> bindings) + throws CommandException { + cmd.processResult(bindings); + final Animator animator = Animator.getAnimator(); + animator.setRandomSeed(getRandomSeed.getSeed()); + } + + public void writeCommand(final IPrologTermOutput pto) + throws CommandException { + cmd.writeCommand(pto); + } + + private final static class ActivateCmd implements IComposableCommand { + public void processResult( + final ISimplifiedROMap<String, PrologTerm> bindings) + throws CommandException { + } + + public void writeCommand(final IPrologTermOutput pto) { + pto.openTerm("activate_plugin(units)").closeTerm(); + } + } + +} 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 e6e88da4..f6bd4fc4 100644 --- a/de.prob.ui/src/de/prob/ui/eventb/StartUnitAnalysisHandler.java +++ b/de.prob.ui/src/de/prob/ui/eventb/StartUnitAnalysisHandler.java @@ -1,17 +1,181 @@ package de.prob.ui.eventb; +import java.util.ArrayList; +import java.util.List; + 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.core.resources.IMarker; +import org.eclipse.core.resources.IProject; +import org.eclipse.core.resources.IResource; +import org.eclipse.core.resources.IResourceChangeEvent; +import org.eclipse.core.resources.IResourceChangeListener; +import org.eclipse.core.resources.IResourceDelta; +import org.eclipse.core.resources.ResourcesPlugin; +import org.eclipse.core.runtime.CoreException; +import org.eclipse.core.runtime.IPath; +import org.eclipse.jface.action.IAction; +import org.eclipse.jface.viewers.ISelection; +import org.eclipse.jface.viewers.IStructuredSelection; +import org.eclipse.ui.handlers.HandlerUtil; +import org.eventb.core.IContextRoot; +import org.eventb.core.IEventBRoot; +import org.eventb.core.IMachineRoot; +import org.rodinp.core.IRodinFile; +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.exceptions.ProBException; +import de.prob.logging.Logger; +import de.prob.ui.PerspectiveFactory; + +public class StartUnitAnalysisHandler extends AbstractHandler implements + IHandler { + + public static class ModificationListener implements IResourceChangeListener { + + private final IPath path; + + public ModificationListener(final IFile resource) { + if (resource == null) { + path = null; + } else { + this.path = resource.getProject().getFullPath(); + } + } + + public void resourceChanged(final IResourceChangeEvent event) { + if (path != null) { + final IResourceDelta delta = event.getDelta(); + IResourceDelta member = delta.findMember(path); + if (member != null) { + Animator.getAnimator().setDirty(); + } + } + } + } + + private ISelection fSelection; + private ModificationListener listener; + + public Object execute(final ExecutionEvent event) throws ExecutionException { + + fSelection = HandlerUtil.getCurrentSelection(event); + + // Get the Selection + final IEventBRoot rootElement = getRootElement(); + final IFile resource = extractResource(rootElement); -public class StartUnitAnalysisHandler extends AbstractHandler implements IHandler { + ArrayList<String> errors = new ArrayList<String>(); + boolean realError = checkErrorMarkers(resource, errors); + if (!errors.isEmpty()) { + String message = "Some components in your project contain " + + (realError ? "errors" : "warnings") + + ". This can lead to unexpected behavior (e.g. missing variables) when animating.\n\nDetails:\n"; + StringBuffer stringBuffer = new StringBuffer(message); + for (String string : errors) { + stringBuffer.append(string); + stringBuffer.append('\n'); + } + if (realError) + Logger.notifyUserWithoutBugreport(stringBuffer.toString()); + else + Logger.notifyUserAboutWarningWithoutBugreport(stringBuffer + .toString()); + } + ; - @Override - public Object execute(ExecutionEvent event) throws ExecutionException { - // TODO Auto-generated method stub - System.out.println("Unit Analysis"); + if (resource != null) { + LimitedLogger.getLogger().log("user started animation", + rootElement.getElementName(), null); + registerModificationListener(resource); + PerspectiveFactory.openPerspective(); + + final Animator animator = Animator.getAnimator(); + try { + // load machine and activate plugin + LoadEventBModelCommand.load(animator, rootElement); + ActivateUnitPluginCommand.activateUnitPlugin(animator); + // TODO: get resulting state and fill attributes + } catch (ProBException e) { + e.notifyUserOnce(); + throw new ExecutionException("Loading the machine failed", e); + } + } return null; } + private boolean checkErrorMarkers(final IFile resource, List<String> errors) { + boolean result = false; + IProject project = resource.getProject(); + try { + IMarker[] markers = project.findMarkers( + "org.eclipse.core.resources.problemmarker", true, + IResource.DEPTH_INFINITE); + for (IMarker iMarker : markers) { + errors.add(iMarker.getResource().getName() + + ": " + + iMarker + .getAttribute(IMarker.MESSAGE, "unknown Error")); + result = result + || (Integer) iMarker.getAttribute(IMarker.SEVERITY) == IMarker.SEVERITY_ERROR; + } + + } catch (CoreException e1) { + } + return result; + } + + private IEventBRoot getRootElement() { + IEventBRoot root = null; + if (fSelection instanceof IStructuredSelection) { + final IStructuredSelection ssel = (IStructuredSelection) fSelection; + if (ssel.size() == 1) { + final Object element = ssel.getFirstElement(); + if (element instanceof IEventBRoot) { + root = (IEventBRoot) element; + } else if (element instanceof IFile) { + IRodinFile rodinFile = RodinCore.valueOf((IFile) element); + if (rodinFile != null) + root = (IEventBRoot) rodinFile.getRoot(); + } + } + } + return root; + } + + private IFile extractResource(final IEventBRoot rootElement) { + IFile resource = null; + if (rootElement == null) { + resource = null; + } else if (rootElement instanceof IMachineRoot) { + resource = ((IMachineRoot) rootElement).getSCMachineRoot() + .getResource(); + } else if (rootElement instanceof IContextRoot) { + resource = ((IContextRoot) rootElement).getSCContextRoot() + .getResource(); + } + return resource; + } + + private void registerModificationListener(final IFile resource) { + if (listener != null) { + ResourcesPlugin.getWorkspace().removeResourceChangeListener( + listener); + } + listener = new ModificationListener(resource); + ResourcesPlugin.getWorkspace().addResourceChangeListener(listener); + } + + public void selectionChanged(final IAction action, + final ISelection selection) { + fSelection = selection; + } + } -- GitLab