public class FinishSymbolicExecutionUntilMergePointMacro extends StrategyProofMacro
MergeRule
can
be applied) or there is no more modality on the sequent.
This is done by implementing a delegation Strategy
which assigns to
any rule application infinite costs if there is no modality on the sequent.
FinishSymbolicExecutionMacro
Modifier and Type | Class and Description |
---|---|
private class |
FinishSymbolicExecutionUntilMergePointMacro.FilterSymbexStrategy
The Class FilterSymbexStrategy is a special strategy assigning to any
rule infinite costs if the goal has no modality or if a merge point is
reached.
|
ProofMacro.ProgressBarListener
Modifier and Type | Field and Description |
---|---|
private java.util.HashSet<JavaBlock> |
alreadySeen |
private java.util.HashSet<ProgramElement> |
blockElems |
private static ProverTaskListener |
DUMMY_PROVER_TASK_LISTENER
Dummy ProverTaskListener.
|
private UserInterfaceControl |
uic |
Constructor and Description |
---|
FinishSymbolicExecutionUntilMergePointMacro() |
FinishSymbolicExecutionUntilMergePointMacro(java.util.HashSet<ProgramElement> blockElems) |
Modifier and Type | Method and Description |
---|---|
ProofMacroFinishedInfo |
applyTo(UserInterfaceControl uic,
Proof proof,
ImmutableList<Goal> goals,
PosInOccurrence posInOcc,
ProverTaskListener listener)
Apply this macro on the given goals.
|
protected Strategy |
createStrategy(Proof proof,
PosInOccurrence posInOcc) |
protected void |
doPostProcessing(Proof proof)
Subclasses can use this method to do some postprocessing on the
proof-object after the strategy has finished.
|
java.lang.String |
getCategory()
Gets the category of this macro.
|
java.lang.String |
getDescription()
Gets the description of this macro.
|
java.lang.String |
getName()
Gets the name of this macro.
|
private boolean |
hasBreakPoint(Semisequent succedent) |
private static boolean |
hasModality(Node node)
Returns true iff there is a modality in the sequent of the given node.
|
private static boolean |
hasModality(Term term)
Recursive check for existence of modality.
|
canApplyTo
applyTo, canApplyTo, getMaxSteps, getScriptCommandName, hasParameter, resetParams, setParameter
private java.util.HashSet<ProgramElement> blockElems
private java.util.HashSet<JavaBlock> alreadySeen
private UserInterfaceControl uic
private static final ProverTaskListener DUMMY_PROVER_TASK_LISTENER
public FinishSymbolicExecutionUntilMergePointMacro()
public FinishSymbolicExecutionUntilMergePointMacro(java.util.HashSet<ProgramElement> blockElems)
public java.lang.String getName()
ProofMacro
null
constant stringpublic java.lang.String getCategory()
ProofMacro
null
if no submenu is to be created.null
public java.lang.String getDescription()
ProofMacro
null
constant stringprivate static boolean hasModality(Node node)
node
- Node to check.private static boolean hasModality(Term term)
term
- The term to check.public ProofMacroFinishedInfo applyTo(UserInterfaceControl uic, Proof proof, ImmutableList<Goal> goals, PosInOccurrence posInOcc, ProverTaskListener listener) throws java.lang.InterruptedException
ProofMacro
InterruptedException
.
A ProverTaskListener
can be provided to which the progress will
be reported. If no reports are desired, null
cna be used for
this parameter. If more than one listener is needed, consider combining
them using a single listener object using the composite pattern.applyTo
in interface ProofMacro
applyTo
in class StrategyProofMacro
uic
- the UserInterfaceControl
to useproof
- the current Proof
(not null
)goals
- the goals (not null
)posInOcc
- the position in occurrence (may be null
)listener
- the listener to use for progress reports (may be
null
)java.lang.InterruptedException
- if the application of the macro has been interrupted.protected Strategy createStrategy(Proof proof, PosInOccurrence posInOcc)
createStrategy
in class StrategyProofMacro
protected void doPostProcessing(Proof proof)
StrategyProofMacro
doPostProcessing
in class StrategyProofMacro
proof
- The proof object.private boolean hasBreakPoint(Semisequent succedent)
succedent
- Succedent of a sequent.