public final class AntichainInvariantChecking extends Object implements InvariantCheckingAlgorithm
InvariantCheckingAlgorithm.Implementations
Algorithm.OrderingType, Algorithm.SearchType
Constructor and Description |
---|
AntichainInvariantChecking(Algorithm.SearchType type)
Creates a new instance of the antichain-based invariant checking algorithm.
|
AntichainInvariantChecking(Algorithm.SearchType type,
boolean computeCounterExample)
Creates a new instance of the antichain-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 AntichainInvariantChecking(Algorithm.SearchType type, boolean computeCounterExample)
type
- the search type of this instancecomputeCounterExample
- if true
a counterexample will be computed
if the invariant check failsAlgorithm.SearchType
public AntichainInvariantChecking(Algorithm.SearchType type)
type
- the search type of this instanceAlgorithm.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