public final class SimulationAntichainInvariantChecking extends Object implements InvariantCheckingAlgorithm
InvariantCheckingAlgorithm.Implementations
Algorithm.OrderingType, Algorithm.SearchType
Constructor and Description |
---|
SimulationAntichainInvariantChecking(Algorithm.SearchType searchType,
boolean computeCounterExample)
Creates a new instance of the simulation-based invariant checking algorithm.
|
Modifier and Type | Method and Description |
---|---|
void |
addComputationListener(ComputationListener l)
Adds the Computation Listener
l to this algorithm. |
void |
cancelComputation()
Cancels the computation of this algorithm.
|
RuleCounterExample |
getInvariantCounterExample()
Returns the counter example, if the language of the automaton is not
an invariant for the graph transformation rule, and
null otherwise |
boolean |
isInvariant(Automaton automaton,
CospanDecomposition leftHandSide,
CospanDecomposition rightHandSide)
Returns
true if and only if the language of the automaton automaton is an
invariant according to the graph transformation rule with the left-hand side leftHandSide and the right-hand side rightHandSide . |
void |
removeComputationListener(ComputationListener l)
Removes the Computation Listener
l from this algorithm. |
public SimulationAntichainInvariantChecking(Algorithm.SearchType searchType, boolean computeCounterExample)
searchType
- the search type used by the algorithm, either forward
or
backward
computeCounterExample
- if true
, the algorithm will compute a counter-exampleAlgorithm.SearchType
public void addComputationListener(ComputationListener l)
Algorithm
l
to this algorithm.addComputationListener
in interface Algorithm
l
- the listener to receive computation eventspublic void removeComputationListener(ComputationListener l)
Algorithm
l
from this algorithm.removeComputationListener
in interface Algorithm
l
- the listener to be removedpublic boolean isInvariant(Automaton automaton, CospanDecomposition leftHandSide, CospanDecomposition rightHandSide)
InvariantCheckingAlgorithm
true
if and only if the language of the automaton automaton
is an
invariant according to the graph transformation rule with the left-hand side leftHandSide
and the right-hand side rightHandSide
.isInvariant
in interface InvariantCheckingAlgorithm
automaton
- the automaton representing the languageleftHandSide
- the left-hand side of the transformation rulerightHandSide
- the right-hand side of the transformation ruletrue
if the language is an invariant, false
otherwisepublic RuleCounterExample getInvariantCounterExample()
InvariantCheckingAlgorithm
null
otherwisegetInvariantCounterExample
in interface InvariantCheckingAlgorithm
null
otherwisepublic void cancelComputation()
Algorithm
cancelComputation
in interface Algorithm