diff --git a/de.prob.core/src/de/prob/core/command/EvaluationExpandCommand.java b/de.prob.core/src/de/prob/core/command/EvaluationExpandCommand.java deleted file mode 100644 index bd3c6a830479c976b8055c477b9d25996caeb897..0000000000000000000000000000000000000000 --- a/de.prob.core/src/de/prob/core/command/EvaluationExpandCommand.java +++ /dev/null @@ -1,55 +0,0 @@ -package de.prob.core.command; - -import java.util.List; - -import de.prob.parser.ISimplifiedROMap; -import de.prob.prolog.output.IPrologTermOutput; -import de.prob.prolog.term.CompoundPrologTerm; -import de.prob.prolog.term.ListPrologTerm; -import de.prob.prolog.term.PrologTerm; - -/** - * This command sends the ID of an expression to the ProB core and receives the - * corresponding label (usually the pretty-printed expression) and the IDs of - * the expression's child nodes. - * - * @see EvaluationGetTopLevelCommand - * @see EvaluationGetValuesCommand - * @author plagge - */ -public class EvaluationExpandCommand implements IComposableCommand { - private static final String LABEL_VARNAME = "Lbl"; - private static final String CHILDREN_VARNAME = "Chs"; - - private final PrologTerm evaluationElement; - - private String label; - private List<PrologTerm> children; - - public EvaluationExpandCommand(final PrologTerm evaluationElement) { - this.evaluationElement = evaluationElement; - } - - public void processResult( - final ISimplifiedROMap<String, PrologTerm> bindings) - throws CommandException { - label = ((CompoundPrologTerm) bindings.get(LABEL_VARNAME)).getFunctor(); - children = (ListPrologTerm) bindings.get(CHILDREN_VARNAME); - } - - public void writeCommand(final IPrologTermOutput pto) { - pto.openTerm("evaluation_expand_formula"); - evaluationElement.toTermOutput(pto); - pto.printVariable(LABEL_VARNAME); - pto.printVariable(CHILDREN_VARNAME); - pto.closeTerm(); - } - - public String getLabel() { - return label; - } - - public List<PrologTerm> getChildrenIds() { - return children; - } -} diff --git a/de.prob.core/src/de/prob/core/command/EvaluationGetTopLevelCommand.java b/de.prob.core/src/de/prob/core/command/EvaluationGetTopLevelCommand.java deleted file mode 100644 index 091564a467ee4abdb12681ef770bcaa063897a3d..0000000000000000000000000000000000000000 --- a/de.prob.core/src/de/prob/core/command/EvaluationGetTopLevelCommand.java +++ /dev/null @@ -1,83 +0,0 @@ -/** - * - */ -package de.prob.core.command; - -import java.util.List; - -import de.prob.core.Animator; -import de.prob.core.domainobjects.EvaluationElement; -import de.prob.exceptions.ProBException; -import de.prob.parser.ISimplifiedROMap; -import de.prob.prolog.output.IPrologTermOutput; -import de.prob.prolog.term.CompoundPrologTerm; -import de.prob.prolog.term.ListPrologTerm; -import de.prob.prolog.term.PrologTerm; - -/** - * This command retrieves the IDs of the top-level expressions and their labels - * and the IDs of their children. - * - * @see EvaluationExpandCommand - * @see EvaluationGetValuesCommand - * @author plagge - */ -public class EvaluationGetTopLevelCommand implements IComposableCommand { - private static final String FIRST_EXPANSION_VARNAME = "FE"; - - public static EvaluationElement[] retrieveTopLevelElements() - throws ProBException { - final Animator animator = Animator.getAnimator(); - final EvaluationGetTopLevelCommand cmd = new EvaluationGetTopLevelCommand( - animator); - animator.execute(cmd); - return cmd.getTopLevelElements(); - } - - private final Animator animator; - private EvaluationElement[] tops; - - public EvaluationGetTopLevelCommand(final Animator animator) { - this.animator = animator; - } - - public void processResult( - final ISimplifiedROMap<String, PrologTerm> bindings) - throws CommandException { - ListPrologTerm resultList = (ListPrologTerm) bindings - .get(FIRST_EXPANSION_VARNAME); - tops = new EvaluationElement[resultList.size()]; - int i = 0; - for (final PrologTerm elemTerm : resultList) { - tops[i] = createElement(elemTerm); - i++; - } - } - - private EvaluationElement createElement(final PrologTerm elemTerm) - throws CommandException { - final EvaluationElement top; - if (elemTerm.hasFunctor("top", 3)) { - final CompoundPrologTerm elem = (CompoundPrologTerm) elemTerm; - final PrologTerm id = elem.getArgument(1); - final String label = ((CompoundPrologTerm) elem.getArgument(2)) - .getFunctor(); - final List<PrologTerm> childrenIds = ((ListPrologTerm) elem - .getArgument(3)); - top = new EvaluationElement(animator, id, label, childrenIds); - } else - throw new CommandException("ProB core sent unexpected term " - + elemTerm); - return top; - } - - public void writeCommand(final IPrologTermOutput pto) { - pto.openTerm("evaluation_get_top_level"); - pto.printVariable(FIRST_EXPANSION_VARNAME); - pto.closeTerm(); - } - - public EvaluationElement[] getTopLevelElements() { - return tops; - } -} diff --git a/de.prob.core/src/de/prob/core/command/EvaluationGetValuesCommand.java b/de.prob.core/src/de/prob/core/command/EvaluationGetValuesCommand.java deleted file mode 100644 index 2208813ae501d7873b26b0ef34c5085cfde1462a..0000000000000000000000000000000000000000 --- a/de.prob.core/src/de/prob/core/command/EvaluationGetValuesCommand.java +++ /dev/null @@ -1,280 +0,0 @@ -/** - * - */ -package de.prob.core.command; - -import java.util.ArrayList; -import java.util.Collection; -import java.util.Collections; -import java.util.HashMap; -import java.util.HashSet; -import java.util.Iterator; -import java.util.Map; - -import de.prob.core.Animator; -import de.prob.core.domainobjects.EvaluationElement; -import de.prob.core.domainobjects.EvaluationStateElement; -import de.prob.core.domainobjects.History; -import de.prob.core.domainobjects.HistoryBasedCache; -import de.prob.core.domainobjects.State; -import de.prob.eventb.translator.FormulaTranslator; -import de.prob.exceptions.ProBException; -import de.prob.parser.ISimplifiedROMap; -import de.prob.prolog.output.IPrologTermOutput; -import de.prob.prolog.term.CompoundPrologTerm; -import de.prob.prolog.term.ListPrologTerm; -import de.prob.prolog.term.PrologTerm; - -/** - * This command sends a list of expression IDs and a state ID to ProB and - * retrieves a list of values of their corresponding values in that state. - * - * @see EvaluationExpandCommand - * @see EvaluationGetTopLevelCommand - * @author plagge - */ -public class EvaluationGetValuesCommand implements IComposableCommand { - private static final String COMMAND_NAME = "evaluation_get_values"; - private static final String VALUE_VARNAME = "Values"; - private static final String TRUE = FormulaTranslator.translate("true"); - private static final String FALSE = FormulaTranslator.translate("false"); - private static final String CACHE_KEY = EvaluationGetValuesCommand.class - .getName() + ".valuecache"; - - /** - * Ask ProB for the values of the given elements in the given state. - * - * @param state - * @param elements - * @return - * @throws ProBException - */ - public static Collection<EvaluationStateElement> getValuesForExpressionsUncached( - final State state, final Collection<EvaluationElement> elements) - throws ProBException { - final Collection<EvaluationStateElement> result; - if (state == null || elements.isEmpty()) { - result = Collections.emptyList(); - } else { - final EvaluationGetValuesCommand cmd = new EvaluationGetValuesCommand( - state.getId(), elements); - Animator.getAnimator().execute(cmd); - Map<EvaluationElement, EvaluationResult> values = cmd.getResult(); - result = new ArrayList<EvaluationStateElement>(values.size()); - for (final Map.Entry<EvaluationElement, EvaluationResult> entry : values - .entrySet()) { - result.add(new EvaluationStateElement(entry.getKey(), state, - entry.getValue())); - } - } - return result; - } - - public static Collection<EvaluationStateElement> getValuesForExpressionsCached( - final State state, final Collection<EvaluationElement> elements) - throws ProBException { - final Collection<EvaluationStateElement> result; - if (state == null || elements.isEmpty()) { - result = Collections.emptyList(); - } else { - final Map<EvaluationElement, EvaluationStateElement> cache = getCache(state); - synchronized (cache) { - Collection<EvaluationElement> toCompute = new HashSet<EvaluationElement>( - elements); - Collection<EvaluationElement> cached = cache.keySet(); - toCompute.removeAll(cached); - Collection<EvaluationStateElement> computed = getValuesForExpressionsUncached( - state, toCompute); - for (final EvaluationStateElement dElement : computed) { - cache.put(dElement.getElement(), dElement); - } - - result = new ArrayList<EvaluationStateElement>(elements.size()); - for (final EvaluationElement sElement : elements) { - result.add(cache.get(sElement)); - } - result.addAll(computed); - } - } - return result; - } - - public static EvaluationStateElement getSingleValueCached( - final State state, final EvaluationElement element) - throws ProBException { - EvaluationStateElement result; - if (state == null) { - result = null; - } else { - final Map<EvaluationElement, EvaluationStateElement> cache = getCache(state); - synchronized (cache) { - result = cache.get(element); - if (result == null) { - Collection<EvaluationStateElement> values = getValuesForExpressionsUncached( - state, Collections.singleton(element)); - result = values.iterator().next(); - cache.put(element, result); - } - } - } - return result; - } - - @SuppressWarnings("unchecked") - private static Map<EvaluationElement, EvaluationStateElement> getCache( - final State state) { - Map<EvaluationElement, EvaluationStateElement> cache; - final Animator animator = Animator.getAnimator(); - synchronized (animator) { - HistoryBasedCache<Map<EvaluationElement, EvaluationStateElement>> hcache = (HistoryBasedCache<Map<EvaluationElement, EvaluationStateElement>>) animator - .getData(CACHE_KEY); - if (hcache == null) { - History history = animator.getHistory(); - hcache = new HistoryBasedCache<Map<EvaluationElement, EvaluationStateElement>>( - history); - history.addListener(hcache); - animator.setData(CACHE_KEY, hcache); - } - cache = hcache.get(state); - if (cache == null) { - cache = new HashMap<EvaluationElement, EvaluationStateElement>(); - hcache.put(state, cache); - } - } - return cache; - } - - private final String stateId; - private final Collection<EvaluationElement> elements; - - private Map<EvaluationElement, EvaluationResult> result; - - public EvaluationGetValuesCommand(final String stateId, - final Collection<EvaluationElement> elements) { - this.stateId = stateId; - this.elements = new ArrayList<EvaluationElement>(elements); - } - - public void processResult( - final ISimplifiedROMap<String, PrologTerm> bindings) - throws CommandException { - final ListPrologTerm valueTerms = (ListPrologTerm) bindings - .get(VALUE_VARNAME); - result = retrieveValues(elements, valueTerms); - } - - public Map<EvaluationElement, EvaluationResult> getResult() { - return result; - } - - private static Map<EvaluationElement, EvaluationResult> retrieveValues( - final Collection<EvaluationElement> elements, - final Collection<PrologTerm> valueTerms) { - if (valueTerms.size() != elements.size()) - throw new IllegalStateException(COMMAND_NAME - + " returned the wrong number of results"); - Map<EvaluationElement, EvaluationResult> results = new HashMap<EvaluationElement, EvaluationResult>(); - Iterator<PrologTerm> it = valueTerms.iterator(); - for (final EvaluationElement element : elements) { - final PrologTerm valueTerm = it.next(); - final EvaluationResult value; - if (valueTerm.hasFunctor("p", 1)) { - final CompoundPrologTerm vc = (CompoundPrologTerm) valueTerm; - final String valString = ((CompoundPrologTerm) vc - .getArgument(1)).getFunctor(); - final boolean predTrue = "true".equals(valString); - final String asString = predTrue ? TRUE : FALSE; - value = new EvaluationResult(asString, true, true, predTrue, - false); - } else if (valueTerm.hasFunctor("v", 1)) { - final CompoundPrologTerm vc = (CompoundPrologTerm) valueTerm; - final String valString = ((CompoundPrologTerm) vc - .getArgument(1)).getFunctor(); - final String translated = valString.length() == 0 ? "" - : FormulaTranslator.translate(valString); - value = new EvaluationResult(translated, true, false, false, - false); - } else if (valueTerm.hasFunctor("e", 1)) { - final CompoundPrologTerm vc = (CompoundPrologTerm) valueTerm; - final String error = ((CompoundPrologTerm) vc.getArgument(1)) - .getFunctor(); - value = new EvaluationResult(error, true, false, false, true); - } else if (valueTerm.hasFunctor("i", 0)) { - value = new EvaluationResult(null, false, false, false, false); - } else - throw new IllegalArgumentException(COMMAND_NAME - + " returned unexpected term " + valueTerm.toString()); - results.put(element, value); - } - return results; - } - - public void writeCommand(final IPrologTermOutput pto) { - pto.openTerm(COMMAND_NAME); - pto.openList(); - for (final EvaluationElement element : elements) { - element.getId().toTermOutput(pto); - } - pto.closeList(); - pto.printAtomOrNumber(stateId); - pto.printVariable(VALUE_VARNAME); - pto.closeTerm(); - } - - public static class EvaluationResult { - private final String text; - private final boolean isActive; - private final boolean isPredicate; - private final boolean isPredicateTrue; - private final boolean hasError; - - public EvaluationResult(final String text, final boolean isActive, - final boolean isPredicate, final boolean isPredicateTrue, - final boolean hasError) { - this.text = text; - this.isActive = isActive; - this.isPredicate = isPredicate; - this.isPredicateTrue = isPredicateTrue; - this.hasError = hasError; - } - - public String getText() { - return text; - } - - public boolean isActive() { - return isActive; - } - - public boolean isPredicate() { - return isPredicate; - } - - /** - * note: returns arbitrary value if called on something else than a - * predicate. - * - * @return - */ - public boolean isPredicateTrue() { - return isPredicateTrue; - } - - public boolean hasError() { - return hasError; - } - }; - - @Override - public String toString() { - StringBuilder sb = new StringBuilder( - "EvaluationGetValuesCommand[elements="); - for (EvaluationElement element : elements) { - sb.append(element.getId()); - sb.append(','); - } - sb.append(" stateId=").append(stateId).append(']'); - return sb.toString(); - } - -} diff --git a/de.prob.core/src/de/prob/core/command/EvaluationInsertFormulaCommand.java b/de.prob.core/src/de/prob/core/command/EvaluationInsertFormulaCommand.java deleted file mode 100644 index e9f12dd56a36272914e6af6c96c62e01061e339b..0000000000000000000000000000000000000000 --- a/de.prob.core/src/de/prob/core/command/EvaluationInsertFormulaCommand.java +++ /dev/null @@ -1,110 +0,0 @@ -/** - * - */ -package de.prob.core.command; - -import de.prob.core.Animator; -import de.prob.core.LanguageDependendAnimationPart; -import de.prob.core.domainobjects.EvaluationElement; -import de.prob.exceptions.ProBException; -import de.prob.parser.ISimplifiedROMap; -import de.prob.parserbase.ProBParseException; -import de.prob.parserbase.ProBParserBaseAdapter; -import de.prob.prolog.output.IPrologTermOutput; -import de.prob.prolog.term.PrologTerm; - -/** - * This commands registers a formula (given as an already parsed - * {@link PrologTerm}) in the Prolog core and returns an - * {@link EvaluationElement} that can be used to evaluate the formula and - * retrieve its subformulas. - * - * @author plagge - */ -public class EvaluationInsertFormulaCommand implements IComposableCommand { - - public static enum FormulaType { - PREDICATE, EXPRESSION - }; - - private static final String VARNAME_ID = "ID"; - private final PrologTerm rawExpression; - private PrologTerm id; - - public static EvaluationElement insertFormula(final PrologTerm formula) - throws ProBException { - final EvaluationInsertFormulaCommand cmd = new EvaluationInsertFormulaCommand( - formula); - final Animator animator = Animator.getAnimator(); - animator.execute(cmd); - return new EvaluationElement(animator, cmd.getId(), null); - } - - public static EvaluationElement insertPredicate(final String formula) - throws ProBException, UnsupportedOperationException, - ProBParseException { - return insertFormula(getParser().parsePredicate(formula, false)); - } - - public static EvaluationElement insertExpression(final String formula) - throws ProBException, UnsupportedOperationException, - ProBParseException { - return insertFormula(getParser().parseExpression(formula, false)); - } - - public static EvaluationElement insertFormula(final Animator animator, - final FormulaType type, final String formula) throws ProBException, - UnsupportedOperationException, ProBParseException { - final ProBParserBaseAdapter parser = getParser(animator); - final PrologTerm parsed; - switch (type) { - case EXPRESSION: - parsed = parser.parseExpression(formula, false); - break; - case PREDICATE: - parsed = parser.parsePredicate(formula, false); - break; - default: - throw new IllegalArgumentException("Unsupported formula type: " - + type); - } - return insertFormula(parsed); - } - - private static ProBParserBaseAdapter getParser() { - return getParser(Animator.getAnimator()); - } - - private static ProBParserBaseAdapter getParser(final Animator animator) { - final LanguageDependendAnimationPart ldp = animator - .getLanguageDependendPart(); - if (ldp == null) { - throw new UnsupportedOperationException( - "The current formalism does not allow parsing of formulas"); - } else { - return new ProBParserBaseAdapter(ldp); - } - } - - public EvaluationInsertFormulaCommand(final PrologTerm rawExpression) { - this.rawExpression = rawExpression; - } - - public void processResult( - final ISimplifiedROMap<String, PrologTerm> bindings) - throws CommandException { - id = bindings.get(VARNAME_ID); - } - - public void writeCommand(final IPrologTermOutput pto) { - pto.openTerm("evaluation_insert_formula"); - rawExpression.toTermOutput(pto); - pto.printAtom("user"); - pto.printVariable(VARNAME_ID); - pto.closeTerm(); - } - - public PrologTerm getId() { - return id; - } -} diff --git a/de.prob.core/src/de/prob/core/domainobjects/EvaluationElement.java b/de.prob.core/src/de/prob/core/domainobjects/EvaluationElement.java deleted file mode 100644 index 82afa345cd2847d36b08b304aa6c230367ac3445..0000000000000000000000000000000000000000 --- a/de.prob.core/src/de/prob/core/domainobjects/EvaluationElement.java +++ /dev/null @@ -1,116 +0,0 @@ -package de.prob.core.domainobjects; - -import java.util.Collection; -import java.util.List; - -import de.prob.core.Animator; -import de.prob.core.command.EvaluationExpandCommand; -import de.prob.core.command.EvaluationGetValuesCommand; -import de.prob.eventb.translator.FormulaTranslator; -import de.prob.exceptions.ProBException; -import de.prob.prolog.term.PrologTerm; - -public class EvaluationElement { - private final PrologTerm id; - private final Animator animator; - private final EvaluationElement parent; - - private EvLazyInformation lazy; - - public EvaluationElement(final Animator animator, final PrologTerm id, - final EvaluationElement parent) { - this.id = id; - this.animator = animator; - this.parent = parent; - } - - public EvaluationElement(final Animator animator, final PrologTerm id, - final String label, final List<PrologTerm> childrenIds) { - this(animator, id, null); - EvaluationElement[] children = new EvaluationElement[childrenIds.size()]; - int i = 0; - for (final PrologTerm childId : childrenIds) { - children[i] = new EvaluationElement(animator, childId, this); - i++; - } - this.lazy = new EvLazyInformation(label, children); - } - - public PrologTerm getId() { - return id; - } - - public EvaluationElement getParent() { - return parent; - } - - public EvaluationElement[] getChildren() throws ProBException { - checkForLazyInformation(); - return lazy.children; - } - - public String getLabel() throws ProBException { - checkForLazyInformation(); - return lazy.label; - } - - public EvaluationStateElement evaluateForState(final State state) - throws ProBException { - return EvaluationGetValuesCommand.getSingleValueCached(state, this); - } - - private void checkForLazyInformation() throws ProBException { - if (lazy == null) { - final EvaluationExpandCommand cmd = new EvaluationExpandCommand(id); - animator.execute(cmd); - final Collection<PrologTerm> childIds = cmd.getChildrenIds(); - final EvaluationElement[] children = new EvaluationElement[childIds - .size()]; - int i = 0; - for (final PrologTerm childId : childIds) { - children[i] = new EvaluationElement(animator, childId, this); - i++; - } - final String label = cmd.getLabel(); - lazy = new EvLazyInformation(label, children); - } - } - - private static final class EvLazyInformation { - private final String label; - private final EvaluationElement[] children; - - public EvLazyInformation(final String label, - final EvaluationElement[] children) { - this.label = FormulaTranslator.translate(label); - this.children = children; - } - } - - @Override - public int hashCode() { - return 31 + id.hashCode(); - } - - @Override - public boolean equals(final Object obj) { - if (this == obj) - return true; - if (obj == null || getClass() != obj.getClass()) - return false; - return id.equals(((EvaluationElement) obj).id); - } - - @Override - public String toString() { - StringBuilder sb = new StringBuilder(); - sb.append("EvaluationElement[id=").append(id); - if (lazy == null) { - sb.append(",label not yet loaded]"); - } else { - sb.append(",label='").append(lazy.label).append("']"); - } - return sb.toString(); - } - -} diff --git a/de.prob.core/src/de/prob/core/domainobjects/EvaluationStateElement.java b/de.prob.core/src/de/prob/core/domainobjects/EvaluationStateElement.java deleted file mode 100644 index 81582797111264d9cb1f98ac2ffeff94c0177aaf..0000000000000000000000000000000000000000 --- a/de.prob.core/src/de/prob/core/domainobjects/EvaluationStateElement.java +++ /dev/null @@ -1,92 +0,0 @@ -/** - * - */ -package de.prob.core.domainobjects; - -import java.util.ArrayList; -import java.util.Arrays; -import java.util.Collections; -import java.util.List; -import java.util.Map; - -import de.prob.core.Animator; -import de.prob.core.command.EvaluationGetValuesCommand; -import de.prob.core.command.EvaluationGetValuesCommand.EvaluationResult; -import de.prob.exceptions.ProBException; - -/** - * @author plagge - * - */ -public class EvaluationStateElement { - public final static EvaluationStateElement[] EMPTY_EVALUATION_STATE_ELEMENT_ARRAY = new EvaluationStateElement[0]; - - private final EvaluationElement element; - private final State state; - private final EvaluationResult result; - - private List<EvaluationStateElement> children; - - public EvaluationStateElement(final EvaluationElement element, - final State state, final EvaluationResult result) { - this.element = element; - this.state = state; - this.result = result; - } - - public EvaluationElement getElement() { - return element; - } - - public State getState() { - return state; - } - - public List<EvaluationStateElement> getChildren() throws ProBException { - checkChildren(); - return children; - } - - public EvaluationResult getResult() { - return result; - } - - private void checkChildren() throws ProBException { - if (children == null) { - EvaluationElement[] staticChildren = element.getChildren(); - EvaluationGetValuesCommand cmd = new EvaluationGetValuesCommand( - state.getId(), Arrays.asList(staticChildren)); - Animator.getAnimator().execute(cmd); - Map<EvaluationElement, EvaluationResult> values = cmd.getResult(); - children = new ArrayList<EvaluationStateElement>( - staticChildren.length); - for (final EvaluationElement staticChild : staticChildren) { - final EvaluationResult value = values.get(staticChild); - children.add(new EvaluationStateElement(staticChild, state, - value)); - } - children = Collections.unmodifiableList(children); - } - - } - - @Override - public int hashCode() { - return 19 * (13 + element.hashCode()) + state.hashCode(); - } - - @Override - public boolean equals(final Object obj) { - if (this == obj) - return true; - if (obj == null || getClass() != obj.getClass()) - return false; - EvaluationStateElement other = (EvaluationStateElement) obj; - return element.equals(other.element) && state.equals(other.state); - } - - public String getText() { - return result == null ? null : result.getText(); - } - -} diff --git a/de.prob.ui/src/de/prob/ui/stateview/AddFormulaHandler.java b/de.prob.ui/src/de/prob/ui/stateview/AddFormulaHandler.java index 134bf771662499fe3a69f7dcefda9621c4302409..61bc81203b8ca4466060ed15841cbb5fe0de7866 100644 --- a/de.prob.ui/src/de/prob/ui/stateview/AddFormulaHandler.java +++ b/de.prob.ui/src/de/prob/ui/stateview/AddFormulaHandler.java @@ -15,8 +15,7 @@ import org.eclipse.ui.handlers.HandlerUtil; import de.prob.core.Animator; import de.prob.core.LanguageDependendAnimationPart; -import de.prob.core.command.EvaluationInsertFormulaCommand; -import de.prob.core.domainobjects.EvaluationElement; +//import de.prob.core.command.EvaluationInsertFormulaCommand; import de.prob.exceptions.ProBException; import de.prob.parserbase.ProBParseException; import de.prob.parserbase.ProBParserBaseAdapter; @@ -40,38 +39,39 @@ public class AddFormulaHandler extends AbstractHandler implements IHandler { validator); int button = dialog.open(); if (button == InputDialog.OK) { - final String entered = dialog.getValue(); - PrologTerm parsed = null; - try { - parsed = parser.parsePredicate(entered, false); - } catch (ProBParseException pe) { - try { - parsed = parser.parseExpression(entered, false); - } catch (ProBParseException ee) { - MessageDialog.openError(shell, title, - StateViewStrings.dialogSyntaxError); - } - } - if (parsed != null) { - try { - final EvaluationElement staticElement = EvaluationInsertFormulaCommand - .insertFormula(parsed); - - final IWorkbenchPage activePage = PlatformUI - .getWorkbench().getActiveWorkbenchWindow() - .getActivePage(); - final StateViewPart view = (StateViewPart) activePage - .findView(StateViewPart.STATE_VIEW_ID); - if (view != null) { - view.addUserDefinedExpression(staticElement); - } else { - MessageDialog.openError(shell, "Error", - "Unable to access state view"); - } - } catch (ProBException e) { - e.notifyUserOnce(); - } - } + //TODO: Refactor to replace EvaluationInsertFormulaCommand with new core +// final String entered = dialog.getValue(); +// PrologTerm parsed = null; +// try { +// parsed = parser.parsePredicate(entered, false); +// } catch (ProBParseException pe) { +// try { +// parsed = parser.parseExpression(entered, false); +// } catch (ProBParseException ee) { +// MessageDialog.openError(shell, title, +// StateViewStrings.dialogSyntaxError); +// } +// } +// if (parsed != null) { +// try { +// final EvaluationElement staticElement = EvaluationInsertFormulaCommand +// .insertFormula(parsed); +// +// final IWorkbenchPage activePage = PlatformUI +// .getWorkbench().getActiveWorkbenchWindow() +// .getActivePage(); +// final StateViewPart view = (StateViewPart) activePage +// .findView(StateViewPart.STATE_VIEW_ID); +// if (view != null) { +// view.addUserDefinedExpression(staticElement); +// } else { +// MessageDialog.openError(shell, "Error", +// "Unable to access state view"); +// } +// } catch (ProBException e) { +// e.notifyUserOnce(); +// } +// } } } }; diff --git a/de.prob.ui/src/de/prob/ui/stateview/StateViewPart.java b/de.prob.ui/src/de/prob/ui/stateview/StateViewPart.java index 7680e3500695125cc43a8b5dd6e9b7e927765d6f..ab267fe81c677644c0c917f9f351fec62d007012 100644 --- a/de.prob.ui/src/de/prob/ui/stateview/StateViewPart.java +++ b/de.prob.ui/src/de/prob/ui/stateview/StateViewPart.java @@ -48,9 +48,6 @@ import org.eclipse.ui.PlatformUI; import de.prob.core.Animator; import de.prob.core.LanguageDependendAnimationPart; import de.prob.core.LimitedLogger; -import de.prob.core.command.EvaluationGetTopLevelCommand; -import de.prob.core.command.EvaluationGetValuesCommand; -import de.prob.core.domainobjects.EvaluationElement; import de.prob.core.domainobjects.MachineDescription; import de.prob.core.domainobjects.Operation; import de.prob.core.domainobjects.State; @@ -87,7 +84,8 @@ public class StateViewPart extends StateBasedViewPart { private LabelViewer modelchangeViewer; - private Collection<EvaluationElement> topEvaluationElements; + //TODO: Refactor to replace EvaluationElement + //private Collection<EvaluationElement> topEvaluationElements; private StateTreeExpressionSection expressionSection; private final VarLabelProvider varLabelProvider = new VarLabelProvider(); @@ -205,27 +203,28 @@ public class StateViewPart extends StateBasedViewPart { private void loadEvaluationElements(final ShownState shownState, final State current, final State last) { - Set<EvaluationElement> visibleElements = new HashSet<EvaluationElement>(); - boolean errorShown = false; - visibleElements.addAll(topEvaluationElements); - try { - for (final Object obj : treeViewer.getVisibleExpandedElements()) { - if (obj instanceof StateTreeExpression) { - StateTreeExpression ste = (StateTreeExpression) obj; - EvaluationElement elem = ste.getStaticElement(); - visibleElements.add(elem); - visibleElements.addAll(Arrays.asList(elem.getChildren())); - } - } - EvaluationGetValuesCommand.getValuesForExpressionsCached(current, - visibleElements); - EvaluationGetValuesCommand.getValuesForExpressionsCached(last, - visibleElements); - } catch (ProBException e) { - if (!errorShown) { - e.notifyUserOnce(); - } - } + //TODO: Refactor to replace EvaluationGetValuesCommand with new core +// Set<EvaluationElement> visibleElements = new HashSet<EvaluationElement>(); +// boolean errorShown = false; +// visibleElements.addAll(topEvaluationElements); +// try { +// for (final Object obj : treeViewer.getVisibleExpandedElements()) { +// if (obj instanceof StateTreeExpression) { +// StateTreeExpression ste = (StateTreeExpression) obj; +// EvaluationElement elem = ste.getStaticElement(); +// visibleElements.add(elem); +// visibleElements.addAll(Arrays.asList(elem.getChildren())); +// } +// } +// EvaluationGetValuesCommand.getValuesForExpressionsCached(current, +// visibleElements); +// EvaluationGetValuesCommand.getValuesForExpressionsCached(last, +// visibleElements); +// } catch (ProBException e) { +// if (!errorShown) { +// e.notifyUserOnce(); +// } +// } } @Override @@ -236,31 +235,32 @@ public class StateViewPart extends StateBasedViewPart { private void initShownState() { if (shownState == null) { - try { - EvaluationElement[] tops = EvaluationGetTopLevelCommand - .retrieveTopLevelElements(); - topEvaluationElements = new ArrayList<EvaluationElement>( - Arrays.asList(tops)); - } catch (ProBException e) { - e.notifyUserOnce(); - topEvaluationElements = Collections.emptyList(); - } - shownState = new ShownState(); - final MachineDescription md = Animator.getAnimator() - .getMachineDescription(); - shownState.setMachineDescription(md); - final StateTreeElement[] topLevelElements = new StateTreeElement[shownState - .getSections().size() + 1]; - int i = 0; - for (final String section : shownState.getSections()) { - topLevelElements[i] = new StateTreeSection(section, md); - i++; - } - expressionSection = new StateTreeExpressionSection( - StateViewStrings.formulasSectionLabel, - topEvaluationElements); - topLevelElements[i] = expressionSection; - treeViewer.setInput(topLevelElements); + //TODO: Refactor to replace EvaluationElement +// try { +// EvaluationElement[] tops = EvaluationGetTopLevelCommand +// .retrieveTopLevelElements(); +// topEvaluationElements = new ArrayList<EvaluationElement>( +// Arrays.asList(tops)); +// } catch (ProBException e) { +// e.notifyUserOnce(); +// topEvaluationElements = Collections.emptyList(); +// } +// shownState = new ShownState(); +// final MachineDescription md = Animator.getAnimator() +// .getMachineDescription(); +// shownState.setMachineDescription(md); +// final StateTreeElement[] topLevelElements = new StateTreeElement[shownState +// .getSections().size() + 1]; +// int i = 0; +// for (final String section : shownState.getSections()) { +// topLevelElements[i] = new StateTreeSection(section, md); +// i++; +// } +// expressionSection = new StateTreeExpressionSection( +// StateViewStrings.formulasSectionLabel, +// topEvaluationElements); +// topLevelElements[i] = expressionSection; +// treeViewer.setInput(topLevelElements); } } @@ -485,10 +485,11 @@ public class StateViewPart extends StateBasedViewPart { } } - public void addUserDefinedExpression( - final EvaluationElement userDefinedElement) { - this.expressionSection.addChild(userDefinedElement); - this.topEvaluationElements.add(userDefinedElement); - refreshTreeView(); - } + //TODO: Refactor to replace EvaluationElement +// public void addUserDefinedExpression( +// final EvaluationElement userDefinedElement) { +// this.expressionSection.addChild(userDefinedElement); +// this.topEvaluationElements.add(userDefinedElement); +// refreshTreeView(); +// } } diff --git a/de.prob.ui/src/de/prob/ui/stateview/statetree/StateTreeExpression.java b/de.prob.ui/src/de/prob/ui/stateview/statetree/StateTreeExpression.java index b5e5d24d74eaf0d774c4b014b0d4f1a48ff654bd..87d54f321d4df81d0069849746e318abea1cc725 100644 --- a/de.prob.ui/src/de/prob/ui/stateview/statetree/StateTreeExpression.java +++ b/de.prob.ui/src/de/prob/ui/stateview/statetree/StateTreeExpression.java @@ -9,10 +9,6 @@ import java.util.List; import org.apache.commons.lang.ObjectUtils; -import de.prob.core.command.EvaluationGetValuesCommand; -import de.prob.core.command.EvaluationGetValuesCommand.EvaluationResult; -import de.prob.core.domainobjects.EvaluationElement; -import de.prob.core.domainobjects.EvaluationStateElement; import de.prob.core.domainobjects.State; import de.prob.exceptions.ProBException; @@ -21,105 +17,145 @@ import de.prob.exceptions.ProBException; * */ public class StateTreeExpression extends AbstractStateTreeElement { - private final EvaluationElement staticElement; - private List<StateTreeElement> children = null; - public StateTreeExpression(final StaticStateElement parent, - final EvaluationElement staticElement) { + public StateTreeExpression(StaticStateElement parent) { super(parent); - this.staticElement = staticElement; - - } - - public StaticStateElement[] getChildren() { - checkForChildren(); - return children.toArray(StateTreeElement.EMPTY_ARRAY); - } - - private void checkForChildren() { - if (children == null) { - try { - EvaluationElement[] staticChildren = staticElement - .getChildren(); - children = new ArrayList<StateTreeElement>( - staticChildren.length); - for (EvaluationElement sChild : staticChildren) { - final StateTreeExpression dChild = new StateTreeExpression( - this, sChild); - children.add(dChild); - } - } catch (ProBException e) { - e.notifyUserOnce(); - children = Collections.emptyList(); - } - } - } - - public String getLabel() { - try { - return staticElement.getLabel(); - } catch (ProBException e) { - e.notifyUserOnce(); - return null; - } + // TODO Auto-generated constructor stub } + //TODO: Refactor to replace EvaluationElement +// private final EvaluationElement staticElement; +// private List<StateTreeElement> children = null; +// +// public StateTreeExpression(final StaticStateElement parent, +// final EvaluationElement staticElement) { +// super(parent); +// this.staticElement = staticElement; +// +// } +// +// public StaticStateElement[] getChildren() { +// checkForChildren(); +// return children.toArray(StateTreeElement.EMPTY_ARRAY); +// } +// +// private void checkForChildren() { +// if (children == null) { +// try { +// EvaluationElement[] staticChildren = staticElement +// .getChildren(); +// children = new ArrayList<StateTreeElement>( +// staticChildren.length); +// for (EvaluationElement sChild : staticChildren) { +// final StateTreeExpression dChild = new StateTreeExpression( +// this, sChild); +// children.add(dChild); +// } +// } catch (ProBException e) { +// e.notifyUserOnce(); +// children = Collections.emptyList(); +// } +// } +// } +// +// public String getLabel() { +// try { +// return staticElement.getLabel(); +// } catch (ProBException e) { +// e.notifyUserOnce(); +// return null; +// } +// } +// +// public boolean hasChildren() { +// checkForChildren(); +// return !children.isEmpty(); +// } +// +// public boolean hasChanged(final State current, final State last) { +// final String curval, lastval; +// try { +// curval = getResultString(current); +// lastval = getResultString(last); +// } catch (ProBException e) { +// e.notifyUserOnce(); +// return false; +// } +// return !ObjectUtils.equals(curval, lastval); +// } +// +// private String getResultString(final State state) throws ProBException { +// //TODO: Refactor to replace EvaluationGetValuesCommand with new core +//// final EvaluationStateElement dyn = EvaluationGetValuesCommand +//// .getSingleValueCached(state, staticElement); +//// final EvaluationResult res = dyn == null ? null : dyn.getResult(); +//// return res == null ? null : res.getText(); +// return null; +// } +// +// public EvaluationElement getStaticElement() { +// return staticElement; +// } +// +// public StateDependendElement getValue(final State state) { +// //TODO: Refactor to replace EvaluationGetValuesCommand with new core +//// StateDependendElement sd; +//// try { +//// EvaluationStateElement dynamicElement = EvaluationGetValuesCommand +//// .getSingleValueCached(state, staticElement); +//// EStateTreeElementProperty property = EStateTreeElementProperty.INACTIVE; +//// String value = "?"; +//// if (dynamicElement != null) { +//// final EvaluationResult result = dynamicElement.getResult(); +//// if (result.isActive()) { +//// if (result.hasError()) { +//// property = EStateTreeElementProperty.ERROR; +//// } else if (result.isPredicate()) { +//// property = result.isPredicateTrue() ? EStateTreeElementProperty.TRUE +//// : EStateTreeElementProperty.FALSE; +//// } else { +//// property = EStateTreeElementProperty.NONBOOLEAN; +//// } +//// } +//// value = result.getText(); +//// } +//// sd = new StateDependendElement(state, value, property); +//// } catch (ProBException e) { +//// e.notifyUserOnce(); +//// sd = new StateDependendElement(state, "(internal error)", +//// EStateTreeElementProperty.ERROR); +//// } +//// return sd; +// return null; +// } + @Override public boolean hasChildren() { - checkForChildren(); - return !children.isEmpty(); + // TODO Auto-generated method stub + return false; } - public boolean hasChanged(final State current, final State last) { - final String curval, lastval; - try { - curval = getResultString(current); - lastval = getResultString(last); - } catch (ProBException e) { - e.notifyUserOnce(); - return false; - } - return !ObjectUtils.equals(curval, lastval); + @Override + public StaticStateElement[] getChildren() { + // TODO Auto-generated method stub + return null; } - private String getResultString(final State state) throws ProBException { - final EvaluationStateElement dyn = EvaluationGetValuesCommand - .getSingleValueCached(state, staticElement); - final EvaluationResult res = dyn == null ? null : dyn.getResult(); - return res == null ? null : res.getText(); + @Override + public String getLabel() { + // TODO Auto-generated method stub + return null; } - public EvaluationElement getStaticElement() { - return staticElement; + @Override + public StateDependendElement getValue(State state) { + // TODO Auto-generated method stub + return null; } - public StateDependendElement getValue(final State state) { - StateDependendElement sd; - try { - EvaluationStateElement dynamicElement = EvaluationGetValuesCommand - .getSingleValueCached(state, staticElement); - EStateTreeElementProperty property = EStateTreeElementProperty.INACTIVE; - String value = "?"; - if (dynamicElement != null) { - final EvaluationResult result = dynamicElement.getResult(); - if (result.isActive()) { - if (result.hasError()) { - property = EStateTreeElementProperty.ERROR; - } else if (result.isPredicate()) { - property = result.isPredicateTrue() ? EStateTreeElementProperty.TRUE - : EStateTreeElementProperty.FALSE; - } else { - property = EStateTreeElementProperty.NONBOOLEAN; - } - } - value = result.getText(); - } - sd = new StateDependendElement(state, value, property); - } catch (ProBException e) { - e.notifyUserOnce(); - sd = new StateDependendElement(state, "(internal error)", - EStateTreeElementProperty.ERROR); - } - return sd; + @Override + public boolean hasChanged(State current, State last) { + // TODO Auto-generated method stub + return false; } } diff --git a/de.prob.ui/src/de/prob/ui/stateview/statetree/StateTreeExpressionSection.java b/de.prob.ui/src/de/prob/ui/stateview/statetree/StateTreeExpressionSection.java index 10286c0b789987eda00cfb3bb72a60f57257bb79..f7fd9d00e75aae98ac715632613dbb490698e9d8 100644 --- a/de.prob.ui/src/de/prob/ui/stateview/statetree/StateTreeExpressionSection.java +++ b/de.prob.ui/src/de/prob/ui/stateview/statetree/StateTreeExpressionSection.java @@ -7,7 +7,6 @@ import java.util.ArrayList; import java.util.Collection; import java.util.List; -import de.prob.core.domainobjects.EvaluationElement; import de.prob.core.domainobjects.State; /** @@ -15,50 +14,86 @@ import de.prob.core.domainobjects.State; * */ public class StateTreeExpressionSection extends AbstractStateTreeElement { - private final String label; - private final List<StateTreeElement> children; - public StateTreeExpressionSection(final String label, - final Collection<EvaluationElement> children) { - this(null, label, children); + public StateTreeExpressionSection(StaticStateElement parent) { + super(parent); + // TODO Auto-generated constructor stub } + //TODO: Refactor to replace EvaluationElement +// private final String label; +// private final List<StateTreeElement> children; +// +// public StateTreeExpressionSection(final String label, +// final Collection<EvaluationElement> children) { +// this(null, label, children); +// } +// +// public StateTreeExpressionSection(final StaticStateElement parent, +// final String label, final Collection<EvaluationElement> children) { +// super(parent); +// this.label = label; +// this.children = new ArrayList<StateTreeElement>(children.size()); +// for (final EvaluationElement elem : children) { +// StateTreeElement child = new StateTreeExpression(this, elem); +// this.children.add(child); +// } +// } +// +// public StaticStateElement[] getChildren() { +// return children.toArray(StateTreeElement.EMPTY_ARRAY); +// } +// +// public String getLabel() { +// return label; +// } +// +// public boolean hasChildren() { +// return !children.isEmpty(); +// } +// +// public boolean hasChanged(State current, State last) { +// return false; +// } +// +// public void addChild(final EvaluationElement staticElement) { +// final StateTreeExpression child = new StateTreeExpression(this, +// staticElement); +// this.children.add(child); +// } +// +// public StateDependendElement getValue(final State state) { +// return new StateDependendElement(state, null, +// EStateTreeElementProperty.NONBOOLEAN); +// } - public StateTreeExpressionSection(final StaticStateElement parent, - final String label, final Collection<EvaluationElement> children) { - super(parent); - this.label = label; - this.children = new ArrayList<StateTreeElement>(children.size()); - for (final EvaluationElement elem : children) { - StateTreeElement child = new StateTreeExpression(this, elem); - this.children.add(child); - } + @Override + public boolean hasChildren() { + // TODO Auto-generated method stub + return false; } + @Override public StaticStateElement[] getChildren() { - return children.toArray(StateTreeElement.EMPTY_ARRAY); + // TODO Auto-generated method stub + return null; } + @Override public String getLabel() { - return label; + // TODO Auto-generated method stub + return null; } - public boolean hasChildren() { - return !children.isEmpty(); + @Override + public StateDependendElement getValue(State state) { + // TODO Auto-generated method stub + return null; } + @Override public boolean hasChanged(State current, State last) { + // TODO Auto-generated method stub return false; } - public void addChild(final EvaluationElement staticElement) { - final StateTreeExpression child = new StateTreeExpression(this, - staticElement); - this.children.add(child); - } - - public StateDependendElement getValue(final State state) { - return new StateDependendElement(state, null, - EStateTreeElementProperty.NONBOOLEAN); - } - }