de.uka.ilkd.key.symbolic_execution

Class TruthValueTracingUtil.MultiEvaluationResult

java.lang.Object

de.uka.ilkd.key.symbolic_execution.TruthValueTracingUtil.MultiEvaluationResult

Enclosing class:

TruthValueTracingUtil

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

Instances of this unmodifyable class are used to store the found evaluation results.

Author:

Martin Hentschel

Field Summary

Fields

Modifier and Type	Field and Description
private boolean	evaluatesToFalse true label evaluates at least once to false, false label never evaluates to false.
private boolean	evaluatesToTrue true label evaluates at least once to true, false label never evaluates to true.
private Term	instructionTerm The instruction Term.

Constructor Summary

Constructors

Constructor and Description
MultiEvaluationResult(boolean evaluationResult) Constructor.
MultiEvaluationResult(boolean evaluatesToTrue, boolean evaluatesToFalse, Term instructionTerm) Constructor.
MultiEvaluationResult(Term instructionTerm) Constructor.

Method Summary

Modifier and Type	Method and Description
TruthValueTracingUtil.TruthValue	evaluate(Name termLabelName, java.util.Map<java.lang.String,TruthValueTracingUtil.MultiEvaluationResult> results) Computes the final truth value.
private static TruthValueTracingUtil.TruthValue	evaluateTerm(Term term, Name termLabelName, java.util.Map<java.lang.String,TruthValueTracingUtil.MultiEvaluationResult> results) Computes the TruthValueTracingUtil.TruthValue of the given instruction Term.
Term	getInstructionTerm() Returns the instruction Term.
boolean	isEvaluatesToFalse() Checks if it is at least once evaluated to false.
boolean	isEvaluatesToTrue() Checks if it is at least once evaluated to true.
TruthValueTracingUtil.MultiEvaluationResult	newEvaluatesToFalse(boolean newEvaluatesToFalse) Creates a new TruthValueTracingUtil.MultiEvaluationResult based on the current once but with an update evaluates to false state.
TruthValueTracingUtil.MultiEvaluationResult	newEvaluatesToTrue(boolean newEvaluatesToTrue) Creates a new TruthValueTracingUtil.MultiEvaluationResult based on the current once but with an update evaluates to true state.
TruthValueTracingUtil.MultiEvaluationResult	newEvaluationResult(boolean evaluationResult) Creates a new TruthValueTracingUtil.MultiEvaluationResult based on the current once but with an updated evaluation result.
TruthValueTracingUtil.MultiEvaluationResult	newInstructionTerm(Term newInstructionTerm) Creates a new TruthValueTracingUtil.MultiEvaluationResult based on the current once but with an update instruction term.
java.lang.String	toPrettyString(Services services) Creates a pretty printed String.
java.lang.String	toString()

Methods inherited from class java.lang.Object

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

Field Detail

evaluatesToTrue

private final boolean evaluatesToTrue

true label evaluates at least once to true, false label never evaluates to true.

evaluatesToFalse

private final boolean evaluatesToFalse

true label evaluates at least once to false, false label never evaluates to false.

instructionTerm

private final Term instructionTerm

The instruction Term.

Constructor Detail

MultiEvaluationResult

public MultiEvaluationResult(boolean evaluationResult)

Constructor.

Parameters:

evaluationResult - true label evaluates at least once to true, false label evaluates at least once to false.

MultiEvaluationResult

public MultiEvaluationResult(Term instructionTerm)

Constructor.

Parameters:

instructionTerm - The instruction Term.

MultiEvaluationResult

public MultiEvaluationResult(boolean evaluatesToTrue,
                             boolean evaluatesToFalse,
                             Term instructionTerm)

Constructor.

Parameters:

evaluatesToTrue - true label evaluates at least once to true, false label never evaluates to true.

evaluatesToFalse - true label evaluates at least once to false, false label never evaluates to false.

instructionTerm - The instruction Term.

Method Detail

isEvaluatesToTrue

public boolean isEvaluatesToTrue()

Checks if it is at least once evaluated to true.

Returns:

true label evaluates at least once to true, false label never evaluates to true.

isEvaluatesToFalse

public boolean isEvaluatesToFalse()

Checks if it is at least once evaluated to false.

Returns:

true label evaluates at least once to false, false label never evaluates to false.

getInstructionTerm

public Term getInstructionTerm()

Returns the instruction Term.

Returns:

The instruction Term or null if undefined.

newEvaluationResult

public TruthValueTracingUtil.MultiEvaluationResult newEvaluationResult(boolean evaluationResult)

Creates a new TruthValueTracingUtil.MultiEvaluationResult based on the current once but with an updated evaluation result.

Parameters:

evaluationResult - true label evaluates at least once to true, false label evaluates at least once to false.

Returns:

The new created TruthValueTracingUtil.MultiEvaluationResult.

newEvaluatesToTrue

public TruthValueTracingUtil.MultiEvaluationResult newEvaluatesToTrue(boolean newEvaluatesToTrue)

Creates a new TruthValueTracingUtil.MultiEvaluationResult based on the current once but with an update evaluates to true state.

Parameters:

newEvaluatesToTrue - true label evaluates at least once to true, false label never evaluates to true.

Returns:

The new created TruthValueTracingUtil.MultiEvaluationResult.

newEvaluatesToFalse

public TruthValueTracingUtil.MultiEvaluationResult newEvaluatesToFalse(boolean newEvaluatesToFalse)

Creates a new TruthValueTracingUtil.MultiEvaluationResult based on the current once but with an update evaluates to false state.

Parameters:

newEvaluatesToFalse - true label evaluates at least once to false, false label never evaluates to false.

Returns:

The new created TruthValueTracingUtil.MultiEvaluationResult.

newInstructionTerm

public TruthValueTracingUtil.MultiEvaluationResult newInstructionTerm(Term newInstructionTerm)

Creates a new TruthValueTracingUtil.MultiEvaluationResult based on the current once but with an update instruction term.

Parameters:

newInstructionTerm - The new instruction Term.

Returns:

The new created TruthValueTracingUtil.MultiEvaluationResult.

toString

public java.lang.String toString()

Overrides:

toString in class java.lang.Object

toPrettyString

public java.lang.String toPrettyString(Services services)

Creates a pretty printed String.

Parameters:

services - The Services to use.

Returns:

The pretty printed String.

evaluate

public TruthValueTracingUtil.TruthValue evaluate(Name termLabelName,
                                                 java.util.Map<java.lang.String,TruthValueTracingUtil.MultiEvaluationResult> results)

Computes the final truth value.

Parameters:

termLabelName - The Name of the TermLabel to consider.

results - All available TruthValueTracingUtil.MultiEvaluationResults.

Returns:

The computed TruthValueTracingUtil.TruthValue.

evaluateTerm

private static TruthValueTracingUtil.TruthValue evaluateTerm(Term term,
                                                             Name termLabelName,
                                                             java.util.Map<java.lang.String,TruthValueTracingUtil.MultiEvaluationResult> results)

Computes the TruthValueTracingUtil.TruthValue of the given instruction Term.

Parameters:

term - The instruction Term to evaluate.

termLabelName - The Name of the TermLabel to consider.

results - All available TruthValueTracingUtil.MultiEvaluationResults.

Returns:

The computed TruthValueTracingUtil.TruthValue.