diff --git a/de.prob.core/src/de/prob/core/command/GetPluginResultCommand.java b/de.prob.core/src/de/prob/core/command/GetPluginResultCommand.java
index eb99459f5a1e7b6264873bd541f0e8d7f81a06c0..7e28630bcfeb68b3da763a24c6bae25b8e93fd85 100644
--- a/de.prob.core/src/de/prob/core/command/GetPluginResultCommand.java
+++ b/de.prob.core/src/de/prob/core/command/GetPluginResultCommand.java
@@ -10,27 +10,29 @@ import de.prob.parser.BindingGenerator;
import de.prob.parser.ISimplifiedROMap;
import de.prob.parser.ResultParserException;
import de.prob.prolog.output.IPrologTermOutput;
-import de.prob.prolog.term.ListPrologTerm;
+import de.prob.prolog.term.CompoundPrologTerm;
import de.prob.prolog.term.PrologTerm;
public final class GetPluginResultCommand implements IComposableCommand {
private final String resultID;
- private ListPrologTerm result;
+ private CompoundPrologTerm result;
public GetPluginResultCommand(final String resultID) {
this.resultID = resultID;
}
- public ListPrologTerm getResult() {
+ public CompoundPrologTerm getResult() {
return result;
}
+ @Override
public void processResult(
final ISimplifiedROMap<String, PrologTerm> bindings)
throws CommandException {
try {
- result = BindingGenerator.getList(bindings, "Bindings");
+ result = BindingGenerator.getCompoundTerm(bindings.get("Bindings"),
+ 1);
} catch (ResultParserException e) {
CommandException commandException = new CommandException(
e.getLocalizedMessage(), e);
@@ -39,6 +41,7 @@ public final class GetPluginResultCommand implements IComposableCommand {
}
}
+ @Override
public void writeCommand(final IPrologTermOutput pto) {
pto.openTerm("get_plugin_output").printAtomOrNumber(resultID)
.printVariable("Bindings").closeTerm();
diff --git a/de.prob.units/src/de/prob/units/ui/StartUnitAnalysisHandler.java b/de.prob.units/src/de/prob/units/ui/StartUnitAnalysisHandler.java
index dd897bd7f9b239681da47f0badc101ce6b58df2e..20dffe8cd30d8211ec3f0143965d4e1555f17ea6 100644
--- a/de.prob.units/src/de/prob/units/ui/StartUnitAnalysisHandler.java
+++ b/de.prob.units/src/de/prob/units/ui/StartUnitAnalysisHandler.java
@@ -58,6 +58,7 @@ import de.prob.prolog.term.CompoundPrologTerm;
import de.prob.prolog.term.ListPrologTerm;
import de.prob.prolog.term.PrologTerm;
import de.prob.units.pragmas.InferredUnitPragmaAttribute;
+import de.prob.units.pragmas.UnitPragmaAttribute;
import de.prob.units.problems.MultipleUnitsInferredMarker;
public class StartUnitAnalysisHandler extends AbstractHandler implements
@@ -75,6 +76,7 @@ public class StartUnitAnalysisHandler extends AbstractHandler implements
}
}
+ @Override
public void resourceChanged(final IResourceChangeEvent event) {
if (path != null) {
final IResourceDelta delta = event.getDelta();
@@ -89,6 +91,7 @@ public class StartUnitAnalysisHandler extends AbstractHandler implements
private ISelection fSelection;
private ModificationListener listener;
+ @Override
public Object execute(final ExecutionEvent event) throws ExecutionException {
fSelection = HandlerUtil.getCurrentSelection(event);
@@ -134,16 +137,14 @@ public class StartUnitAnalysisHandler extends AbstractHandler implements
final StartAnimationCommand start = new StartAnimationCommand();
final ActivateUnitPluginCommand activatePlugin = new ActivateUnitPluginCommand();
- final ComposedCommand composed = new ComposedCommand(clear,
- setPrefs, load, start, activatePlugin);
-
- animator.execute(composed);
-
GetPluginResultCommand pluginResultCommand = new GetPluginResultCommand(
"Grounded Result State");
- animator.execute(pluginResultCommand);
+ final ComposedCommand composed = new ComposedCommand(clear,
+ setPrefs, load, start, activatePlugin,
+ pluginResultCommand);
+ animator.execute(composed);
processResults(pluginResultCommand.getResult());
} catch (ProBException e) {
e.notifyUserOnce();
@@ -194,23 +195,41 @@ public class StartUnitAnalysisHandler extends AbstractHandler implements
return result;
}
- private void processResults(ListPrologTerm result) throws RodinDBException,
- ExecutionException {
+ private void processResults(CompoundPrologTerm result)
+ throws RodinDBException, ExecutionException {
// preprocess the list into a map
Map<String, String> variables = new HashMap<String, String>();
- for (PrologTerm term : result) {
- CompoundPrologTerm compoundTerm;
- try {
- compoundTerm = BindingGenerator
- .getCompoundTerm(term, "bind", 2);
-
- variables.put(
- PrologTerm.atomicString(compoundTerm.getArgument(1)),
- PrologTerm.atomicString(compoundTerm.getArgument(2)));
- } catch (ResultParserException e) {
- CommandException commandException = new CommandException(
- e.getLocalizedMessage(), e);
- commandException.notifyUserOnce();
+ List<String> offendingDefinitions = new ArrayList<String>();
+
+ ListPrologTerm liste = BindingGenerator.getList(result.getArgument(1));
+
+ for (PrologTerm term : liste) {
+ if (term.isAtom()) {
+ // this is an error message. do something about it.
+ String offendingUnitDefinition = PrologTerm.atomicString(term)
+ .replace("Incorrect unit definition: ['", "");
+ offendingUnitDefinition = offendingUnitDefinition.replace("']",
+ "");
+
+ // add error to the list of incorrect definitions. error markers
+ // will be attached later
+ offendingDefinitions.add(offendingUnitDefinition);
+
+ } else {
+ // process inferred units and add to map
+ CompoundPrologTerm compoundTerm;
+ try {
+ compoundTerm = BindingGenerator.getCompoundTerm(term,
+ "bind", 2);
+
+ variables.put(PrologTerm.atomicString(compoundTerm
+ .getArgument(1)), PrologTerm
+ .atomicString(compoundTerm.getArgument(2)));
+ } catch (ResultParserException e) {
+ CommandException commandException = new CommandException(
+ e.getLocalizedMessage(), e);
+ commandException.notifyUserOnce();
+ }
}
}
@@ -247,6 +266,20 @@ public class StartUnitAnalysisHandler extends AbstractHandler implements
+ variableName));
}
}
+
+ // check if the attached unit pragma (given by user) was marked
+ // as offending
+ if (var.hasAttribute(UnitPragmaAttribute.ATTRIBUTE)) {
+ if (offendingDefinitions.contains(var
+ .getAttributeValue(UnitPragmaAttribute.ATTRIBUTE))) {
+ var.createProblemMarker(
+ InferredUnitPragmaAttribute.ATTRIBUTE,
+ new MultipleUnitsInferredMarker(
+ IMarker.SEVERITY_ERROR,
+ "Incorrect Unit Definition on Variable "
+ + variableName));
+ }
+ }
}
} else if (rootElement instanceof IContextRoot) {
@@ -254,16 +287,16 @@ public class StartUnitAnalysisHandler extends AbstractHandler implements
IConstant[] allConstants = rootElement.getContextRoot()
.getConstants();
- for (IConstant var : allConstants) {
- String constantName = var.getIdentifierString();
+ for (IConstant cst : allConstants) {
+ String constantName = cst.getIdentifierString();
if (variables.containsKey(constantName)) {
- var.setAttributeValue(
+ cst.setAttributeValue(
InferredUnitPragmaAttribute.ATTRIBUTE,
variables.get(constantName),
new NullProgressMonitor());
if (variables.get(constantName).equals("error")) {
- var.createProblemMarker(
+ cst.createProblemMarker(
InferredUnitPragmaAttribute.ATTRIBUTE,
new MultipleUnitsInferredMarker(
IMarker.SEVERITY_ERROR,
@@ -271,7 +304,7 @@ public class StartUnitAnalysisHandler extends AbstractHandler implements
+ constantName));
}
if (variables.get(constantName).equals("unknown")) {
- var.createProblemMarker(
+ cst.createProblemMarker(
InferredUnitPragmaAttribute.ATTRIBUTE,
new MultipleUnitsInferredMarker(
IMarker.SEVERITY_WARNING,
@@ -279,6 +312,20 @@ public class StartUnitAnalysisHandler extends AbstractHandler implements
+ constantName));
}
}
+
+ // check if the attached unit pragma (given by user) was marked
+ // as offending
+ if (cst.hasAttribute(UnitPragmaAttribute.ATTRIBUTE)) {
+ if (offendingDefinitions.contains(cst
+ .getAttributeValue(UnitPragmaAttribute.ATTRIBUTE))) {
+ cst.createProblemMarker(
+ InferredUnitPragmaAttribute.ATTRIBUTE,
+ new MultipleUnitsInferredMarker(
+ IMarker.SEVERITY_ERROR,
+ "Incorrect Unit Definition on Constant "
+ + constantName));
+ }
+ }
}
} else {
throw new ExecutionException(