public class TestGenMacro extends StrategyProofMacro
Modifier and Type | Class and Description |
---|---|
private static class |
TestGenMacro.TestGenStrategy
The Class FilterAppManager is a special strategy assigning to any rule
infinite costs if the goal has no modality
|
ProofMacro.ProgressBarListener
Constructor and Description |
---|
TestGenMacro() |
Modifier and Type | Method and Description |
---|---|
protected Strategy |
createStrategy(Proof proof,
PosInOccurrence posInOcc) |
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 static boolean |
hasModality(Node node) |
private static boolean |
hasModality(Term term) |
applyTo, canApplyTo, doPostProcessing
applyTo, canApplyTo, getMaxSteps, getScriptCommandName, hasParameter, resetParams, setParameter
private static boolean hasModality(Node node)
private static boolean hasModality(Term term)
protected Strategy createStrategy(Proof proof, PosInOccurrence posInOcc)
createStrategy
in class StrategyProofMacro
public java.lang.String getDescription()
ProofMacro
null
constant stringpublic java.lang.String getName()
ProofMacro
null
constant stringpublic java.lang.String getCategory()
ProofMacro
null
if no submenu is to be created.null