public abstract class AbstractExecutionElement extends java.lang.Object implements IExecutionElement
IExecutionElement
.Modifier and Type | Field and Description |
---|---|
private java.lang.String |
name
The human readable name of this node.
|
private Node |
proofNode
The
Node of KeY's proof tree which is represented by this IExecutionNode . |
private ITreeSettings |
settings
The used
TreeSettings . |
Constructor and Description |
---|
AbstractExecutionElement(ITreeSettings settings,
Node proofNode)
Constructor.
|
Modifier and Type | Method and Description |
---|---|
protected java.lang.String |
formatTerm(Term term,
Services services)
|
RuleApp |
getAppliedRuleApp()
Returns the applied
RuleApp . |
InitConfig |
getInitConfig()
Returns the
InitConfig used by IExecutionElement.getProof() . |
java.lang.String |
getName()
Returns a human readable name which describes this element.
|
Proof |
getProof()
Returns the
Proof from which the symbolic execution tree was extracted. |
Node |
getProofNode()
Returns the
Node in KeY's proof tree which is represented by this execution tree node. |
NodeInfo |
getProofNodeInfo()
Returns the
NodeInfo of IExecutionElement.getProofNode() . |
Services |
getServices()
Returns the
Services used by IExecutionElement.getProof() . |
ITreeSettings |
getSettings()
Returns the
ITreeSettings to use. |
boolean |
isDisposed()
Checks if the proof is disposed.
|
protected boolean |
isNameComputed()
Checks if the value of
getName() is already computed. |
protected abstract java.lang.String |
lazyComputeName()
Computes the name of this node lazily when
getName()
is called the first time. |
protected void |
setName(java.lang.String name)
Sets the name.
|
java.lang.String |
toString() |
clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait
getElementType, getModalityPIO
private final ITreeSettings settings
TreeSettings
.private final Node proofNode
Node
of KeY's proof tree which is represented by this IExecutionNode
.private java.lang.String name
public AbstractExecutionElement(ITreeSettings settings, Node proofNode)
settings
- The ITreeSettings
to use.proofNode
- The Node
of KeY's proof tree which is represented by this IExecutionNode
.public Services getServices()
Services
used by IExecutionElement.getProof()
.getServices
in interface IExecutionElement
Services
used by IExecutionElement.getProof()
.public RuleApp getAppliedRuleApp()
RuleApp
.getAppliedRuleApp
in interface IExecutionElement
RuleApp
.public InitConfig getInitConfig()
InitConfig
used by IExecutionElement.getProof()
.getInitConfig
in interface IExecutionElement
InitConfig
used by IExecutionElement.getProof()
.public Proof getProof()
Proof
from which the symbolic execution tree was extracted.getProof
in interface IExecutionElement
Proof
from which the symbolic execution tree was extracted.public Node getProofNode()
Node
in KeY's proof tree which is represented by this execution tree node.getProofNode
in interface IExecutionElement
Node
in KeY's proof tree which is represented by this execution tree node.public NodeInfo getProofNodeInfo()
NodeInfo
of IExecutionElement.getProofNode()
.getProofNodeInfo
in interface IExecutionElement
NodeInfo
of IExecutionElement.getProofNode()
.public java.lang.String getName() throws ProofInputException
getName
in interface IExecutionElement
ProofInputException
- Occurred Exception.protected void setName(java.lang.String name)
name
- The new name to set.protected boolean isNameComputed()
getName()
is already computed.ture
name is computed, false
name is not computed yet.protected abstract java.lang.String lazyComputeName() throws ProofInputException
getName()
is called the first time.IExecutionNode
.ProofInputException
public java.lang.String toString()
toString
in class java.lang.Object
public boolean isDisposed()
isDisposed
in interface IExecutionElement
true
proof is disposed, false
proof is not disposed and still valid.public ITreeSettings getSettings()
ITreeSettings
to use.getSettings
in interface IExecutionElement
ITreeSettings
to use.