public class FinishSymbolicExecutionWithSpecJoinsMacro extends AbstractProofMacro
FinishSymbolicExecutionMacro
Modifier and Type | Class and Description |
---|---|
private class |
FinishSymbolicExecutionWithSpecJoinsMacro.FilterSymbexStrategy
The Class FilterSymbexStrategy is a special strategy assigning to any
rule infinite costs if the goal has no modality or if a join point is
reached.
|
private static interface |
FinishSymbolicExecutionWithSpecJoinsMacro.Predicate<T> |
ProofMacro.ProgressBarListener
Constructor and Description |
---|
FinishSymbolicExecutionWithSpecJoinsMacro() |
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.
|
boolean |
canApplyTo(Proof proof,
ImmutableList<Goal> goals,
PosInOccurrence posInOcc)
Can this macro be applied on the given goals?
This method should not make any changes but check if the macro can be
applied or not on the given goals.
|
String |
getCategory()
Gets the category of this macro.
|
String |
getDescription()
Gets the description of this macro.
|
String |
getName()
Gets the name of this macro.
|
private Statement |
getNthStatementOfMethodFrameBlock(StatementBlock block,
int n,
Services services) |
private Statement |
getSecondStatementOfMethodFrameBlock(StatementBlock block,
Services services) |
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.
|
private static <T> ImmutableList<T> |
setDifference(ImmutableList<T> list1,
ImmutableList<T> list2)
Computes the set difference of the two given lists.
|
private StatementBlock |
stripMethodFrame(StatementBlock sb,
Services services)
Removes the
try { method-frame { ... |
applyTo, canApplyTo, getMaxSteps, getScriptCommandName
public FinishSymbolicExecutionWithSpecJoinsMacro()
public String getName()
ProofMacro
null
constant stringpublic String getCategory()
ProofMacro
null
if no submenu is to be created.null
public String getDescription()
ProofMacro
null
constant stringpublic boolean canApplyTo(Proof proof, ImmutableList<Goal> goals, PosInOccurrence posInOcc)
ProofMacro
proof
- the current Proof
(not null
)goals
- the goals (not null
)posInOcc
- the position in occurrence (may be null
)true
, if the macro is allowed to be appliedpublic ProofMacroFinishedInfo applyTo(UserInterfaceControl uic, Proof proof, ImmutableList<Goal> goals, PosInOccurrence posInOcc, ProverTaskListener listener) throws 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.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
)InterruptedException
- if the application of the macro has been interrupted.private static <T> ImmutableList<T> setDifference(ImmutableList<T> list1, ImmutableList<T> list2)
list1
- First list.list2
- Second list.private static boolean hasModality(Node node)
node
- Node to check.private static boolean hasModality(Term term)
term
- The term to check.private Statement getSecondStatementOfMethodFrameBlock(StatementBlock block, Services services)
block
- The statement block which is assumed to wrap another block by
a method frame.private Statement getNthStatementOfMethodFrameBlock(StatementBlock block, int n, Services services)
block
- The statement block which is assumed to wrap another block by
a method frame.n
- Specification of the element to obtain.private StatementBlock stripMethodFrame(StatementBlock sb, Services services)
try { method-frame { ... }}
parts from the given
statement block, i.e. returns the inner code. If there is nothing to
remove, the original block is returned.sb
- The statement block to remove the try/method-frame parts from.