de.uka.ilkd.key.symbolic_execution

Class TruthValueTracingUtil.BranchResult

java.lang.Object

de.uka.ilkd.key.symbolic_execution.TruthValueTracingUtil.BranchResult

Enclosing class:

TruthValueTracingUtil

public static class TruthValueTracingUtil.BranchResult
extends java.lang.Object

Represents the unmodifiable predicate results of a leaf Node (Goal).

Author:

Martin Hentschel

Field Summary

Fields

Modifier and Type	Field and Description
private Term	condition The condition under which the leaf Node is reached from the analyzed Node.
private java.lang.String	conditionString The human readable condition under which the leaf Node is reached from the analyzed Node.
private Node	leafNode The leaf Node.
private java.util.Map<java.lang.String,TruthValueTracingUtil.MultiEvaluationResult>	results All found results.
private Name	termLabelName The Name of the TermLabel to consider.

Constructor Summary

Constructors

Constructor and Description
BranchResult(Node leafNode, java.util.Map<java.lang.String,TruthValueTracingUtil.MultiEvaluationResult> results, Term condition, java.lang.String conditionString, Name termLabelName) Constructor.

Method Summary

Modifier and Type	Method and Description
TruthValueTracingUtil.TruthValue	evaluate(FormulaTermLabel termLabel) Evaluates the given FormulaTermLabel.
Term	getCondition() Returns the condition under which the leaf Node is reached from the analyzed Node.
java.lang.String	getConditionString() Returns the human readable condition under which the leaf Node is reached from the analyzed Node.
Node	getLeafNode() Returns the leaf Node.
FormulaTermLabel	getPredicateLabel(Term term) Returns the first FormulaTermLabel with Name getTermLabelName().
TruthValueTracingUtil.MultiEvaluationResult	getResult(FormulaTermLabel termLabel) Returns the TruthValueTracingUtil.MultiEvaluationResult for the given FormulaTermLabel.
java.util.Map<java.lang.String,TruthValueTracingUtil.MultiEvaluationResult>	getResults() Returns all found results.
Name	getTermLabelName() Returns the Name of the TermLabel to consider.
boolean	hasPredicateLabel(Term term) Checks if the Term has a TermLabel with Name getTermLabelName().
java.lang.String	toPrettyString() Creates a pretty printed String.
java.lang.String	toString()
void	updateResult(FormulaTermLabel termLabel, TruthValueTracingUtil.MultiEvaluationResult result) Updates a result.

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait

Field Detail

results

private final java.util.Map<java.lang.String,TruthValueTracingUtil.MultiEvaluationResult> results

All found results.

leafNode

private final Node leafNode

The leaf Node.

condition

private final Term condition

The condition under which the leaf Node is reached from the analyzed Node.

conditionString

private final java.lang.String conditionString

The human readable condition under which the leaf Node is reached from the analyzed Node.

termLabelName

private final Name termLabelName

The Name of the TermLabel to consider.

Constructor Detail

BranchResult

public BranchResult(Node leafNode,
                    java.util.Map<java.lang.String,TruthValueTracingUtil.MultiEvaluationResult> results,
                    Term condition,
                    java.lang.String conditionString,
                    Name termLabelName)

Constructor.

Parameters:

leafNode - The leaf Node.

results - All found results.

condition - The condition under which the leaf Node is reached from the analyzed Node.

conditionString - The human readable condition under which the leaf Node is reached from the analyzed Node.

termLabelName - The Name of the TermLabel to consider.

Method Detail

getResults

public java.util.Map<java.lang.String,TruthValueTracingUtil.MultiEvaluationResult> getResults()

Returns all found results.

Returns:

All found results.

getResult

public TruthValueTracingUtil.MultiEvaluationResult getResult(FormulaTermLabel termLabel)

Returns the TruthValueTracingUtil.MultiEvaluationResult for the given FormulaTermLabel.

Parameters:

termLabel - The FormulaTermLabel.

Returns:

The found TruthValueTracingUtil.MultiEvaluationResult or null if not available.

updateResult

public void updateResult(FormulaTermLabel termLabel,
                         TruthValueTracingUtil.MultiEvaluationResult result)

Updates a result.

Warning: TruthValueTracingUtil.BranchResults are considered to be unmodifiable. This means that an update of the result needs to be done before results are shown to the user by the UI.

Parameters:

termLabel - The FormulaTermLabel to update.

result - The new result of the given FormulaTermLabel.

getCondition

public Term getCondition()

Returns the condition under which the leaf Node is reached from the analyzed Node.

Returns:

The condition under which the leaf Node is reached from the analyzed Node.

getConditionString

public java.lang.String getConditionString()

Returns the human readable condition under which the leaf Node is reached from the analyzed Node.

Returns:

The human readable condition under which the leaf Node is reached from the analyzed Node.

getTermLabelName

public Name getTermLabelName()

Returns the Name of the TermLabel to consider.

Returns:

The Name of the TermLabel to consider.

hasPredicateLabel

public boolean hasPredicateLabel(Term term)

Checks if the Term has a TermLabel with Name getTermLabelName().

Parameters:

term - The Term to check.

Returns:

true has TermLabel, false do not has TermLabel.

getPredicateLabel

public FormulaTermLabel getPredicateLabel(Term term)

Returns the first FormulaTermLabel with Name getTermLabelName().

Parameters:

term - The Term.

Returns:

The found FormulaTermLabel or null otherwise.

getLeafNode

public Node getLeafNode()

Returns the leaf Node.

Returns:

The leaf Node.

toString

public java.lang.String toString()

Overrides:

toString in class java.lang.Object

toPrettyString

public java.lang.String toPrettyString()

Creates a pretty printed String.

Returns:

The pretty printed String.

evaluate

public TruthValueTracingUtil.TruthValue evaluate(FormulaTermLabel termLabel)

Evaluates the given FormulaTermLabel.

Parameters:

termLabel - The FormulaTermLabel to evaluate.

Returns:

The evaluation result.