From eaf30ff0b09714e8700b753b193a87afef7fc660 Mon Sep 17 00:00:00 2001
From: Sebastian Krings <sebastian@krin.gs>
Date: Wed, 2 Jan 2013 13:03:28 +0100
Subject: [PATCH] insert results of unit analysis in the inferredUnitPragma
text fields
---
.../ui/eventb/StartUnitAnalysisHandler.java | 80 +++++++++++++++++--
1 file changed, 74 insertions(+), 6 deletions(-)
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 554c05b9..3b2ce2fe 100644
--- a/de.prob.ui/src/de/prob/ui/eventb/StartUnitAnalysisHandler.java
+++ b/de.prob.ui/src/de/prob/ui/eventb/StartUnitAnalysisHandler.java
@@ -7,7 +7,9 @@
package de.prob.ui.eventb;
import java.util.ArrayList;
+import java.util.HashMap;
import java.util.List;
+import java.util.Map;
import org.eclipse.core.commands.AbstractHandler;
import org.eclipse.core.commands.ExecutionEvent;
@@ -23,20 +25,25 @@ 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.core.runtime.NullProgressMonitor;
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.IConstant;
import org.eventb.core.IContextRoot;
import org.eventb.core.IEventBRoot;
import org.eventb.core.IMachineRoot;
+import org.eventb.core.IVariable;
import org.rodinp.core.IRodinFile;
import org.rodinp.core.RodinCore;
+import org.rodinp.core.RodinDBException;
import de.prob.core.Animator;
import de.prob.core.LimitedLogger;
import de.prob.core.command.ActivateUnitPluginCommand;
import de.prob.core.command.ClearMachineCommand;
+import de.prob.core.command.CommandException;
import de.prob.core.command.ComposedCommand;
import de.prob.core.command.GetPluginResultCommand;
import de.prob.core.command.SetPreferencesCommand;
@@ -44,7 +51,12 @@ import de.prob.core.command.StartAnimationCommand;
import de.prob.core.command.internal.InternalLoadCommand;
import de.prob.exceptions.ProBException;
import de.prob.logging.Logger;
+import de.prob.parser.BindingGenerator;
+import de.prob.parser.ResultParserException;
+import de.prob.prolog.term.CompoundPrologTerm;
import de.prob.prolog.term.ListPrologTerm;
+import de.prob.prolog.term.PrologTerm;
+import de.prob.ui.pragmas.InferredUnitPragma;
public class StartUnitAnalysisHandler extends AbstractHandler implements
IHandler {
@@ -130,20 +142,76 @@ public class StartUnitAnalysisHandler extends AbstractHandler implements
animator.execute(composed);
// TODO: get resulting state and fill attributes
- GetPluginResultCommand stateValuesCommand = new GetPluginResultCommand(
+ GetPluginResultCommand pluginResultCommand = new GetPluginResultCommand(
"Grounded Result State");
- animator.execute(stateValuesCommand);
-
- ListPrologTerm output = stateValuesCommand.getResult();
+ animator.execute(pluginResultCommand);
+
+ ListPrologTerm output = pluginResultCommand.getResult();
+ System.out.println("Resulting state: " + output);
+
+ // preprocess the list into a map
+ Map<String, String> variables = new HashMap<String, String>();
+ for (PrologTerm term : output) {
+ CompoundPrologTerm compoundTerm;
+ try {
+ compoundTerm = BindingGenerator.getCompoundTerm(term,
+ "bind", 2);
+ } catch (ResultParserException e) {
+ CommandException commandException = new CommandException(
+ e.getLocalizedMessage(), e);
+ commandException.notifyUserOnce();
+ throw commandException;
+ }
+ variables.put(compoundTerm.getArgument(1).toString(),
+ compoundTerm.getArgument(2).toString());
+ }
- System.out.println(output);
+ // look up the variables / constants of the selected machine in
+ // the state
+ // and set the inferredUnitPragma attribute
+ if (rootElement instanceof IMachineRoot) {
+ // find and update variables
+ IVariable[] allVariables = rootElement.getMachineRoot()
+ .getVariables();
+
+ for (IVariable var : allVariables) {
+ String variableName = var.getIdentifierString();
+ if (variables.containsKey(variableName)) {
+ var.setAttributeValue(InferredUnitPragma.ATTRIBUTE,
+ variables.get(variableName),
+ new NullProgressMonitor());
+ }
+ }
+
+ } else if (rootElement instanceof IContextRoot) {
+ // find and update constants
+ IConstant[] allConstants = rootElement.getContextRoot()
+ .getConstants();
+
+ for (IConstant var : allConstants) {
+ String constantName = var.getIdentifierString();
+ if (variables.containsKey(constantName)) {
+ var.setAttributeValue(InferredUnitPragma.ATTRIBUTE,
+ variables.get(constantName),
+ new NullProgressMonitor());
+ }
+ }
+ } else {
+ throw new ExecutionException(
+ "Cannot translate anything else than IMachineRoot or IContextRoot. Type of "
+ + rootElement.getComponentName() + " was: "
+ + rootElement.getClass());
+ }
// shutdown animator
animator.shutdown();
} catch (ProBException e) {
e.notifyUserOnce();
- throw new ExecutionException("Loading the machine failed", e);
+ throw new ExecutionException("Unit Analysis Failed", e);
+ } catch (RodinDBException e) {
+ throw new ExecutionException(
+ "Unit Analysis Failed with a RodinDBException", e);
}
}
return null;
--
GitLab