Package | Description |
---|---|
de.uni_due.inf.ti.raven.actions |
General Action Classes.
|
de.uni_due.inf.ti.raven.algorithms |
Classes to run different algorithms.
|
de.uni_due.inf.ti.raven.data.automata |
Classes to create, represent, manipulate automata.
|
de.uni_due.inf.ti.raven.encodings |
Classes to encode the state space and the transitions of the various graph automata.
|
de.uni_due.inf.ti.raven.gui |
GUI Classes.
|
de.uni_due.inf.ti.raven.gui.automaton |
Classes which provide (visual) forms either used to collect information required to create the
several graph automata or used to present information about existing graph automata.
|
de.uni_due.inf.ti.raven.gui.graphs |
GUI Classes to visualize graphs.
|
de.uni_due.inf.ti.raven.io |
Classes to load, save and print data.
|
Modifier and Type | Method and Description |
---|---|
Automaton |
ShiftAutomatonAction.getResult() |
Constructor and Description |
---|
AntichainInvariantCheckingAction(Algorithm.SearchType type,
boolean computeCounterExample,
Automaton automaton,
CospanDecomposition leftHandSide,
CospanDecomposition rightHandSide)
Creates a new
Action to execute the antichain-based invariant
check for the automaton automaton and the left- resp. right-hand
side leftHandSide and rightHandSide . |
AntichainLanguageInclusionAction(Algorithm.SearchType type,
boolean computeCounterExample,
Automaton firstAutomaton,
Automaton secondAutomaton)
Creates a new
Action to execute the antichain-based language inclusion check for the
two automata firstAutomaton and secondAutomaton . |
AntichainUniversalityAction(Algorithm.SearchType type,
boolean computeCounterExample,
Automaton automaton)
Creates a new
Action to execute the antichain-based universality check for the
automaton automaton . |
BisimulationUpToCongruenceInvariantCheckingAction(Algorithm.SearchType type,
boolean computeCounterExample,
Automaton automaton,
CospanDecomposition leftHandSide,
CospanDecomposition rightHandSide)
Creates a new
Action to execute the bisimulation-up-to-congruence invariant check
for the automaton automaton and the left- resp. right-hand side leftHandSide
and rightHandSide . |
BisimulationUpToCongruenceLanguageInclusionAction(Algorithm.SearchType type,
Automaton firstAutomaton,
Automaton secondAutomaton)
Creates a new
Action to execute the bisimulation-up-to-congruence
language inclusion check for the two automata firstAutomaton and
secondAutomaton . |
BisimulationUpToCongruenceLanguageInclusionAction(Algorithm.SearchType type,
boolean computeCounterExample,
Automaton firstAutomaton,
Automaton secondAutomaton)
Creates a new
Action to execute the bisimulation-up-to-congruence
language inclusion check for the two automata firstAutomaton and
secondAutomaton . |
EmptinessCheckAction(Algorithm.SearchType type,
Automaton automaton)
Creates a new
Action to execute the emptiness check for the automaton automaton . |
MembershipAction(Automaton automaton,
CospanDecomposition decomposition)
Creates a new
Action to execute the membership check for the automaton
automaton and the cospan decomposition decomposition , i.e. it will be
checked whether the cospan decomposition (of an input graph) is accepted by the automaton. |
PrintAction(AutomatonPrinter printer,
Automaton automaton)
Creates an action which prints an automaton to a given printer.
|
ProductAutomatonAction(Automaton first,
Automaton second)
Creates an action which constructs the product automaton for two given automata.
|
ReachabilityAction(Automaton automaton,
CospanDecomposition decomposition)
Creates an action which computes all states for the automaton
automaton which are
reachable by processing the cospan decomposition decomposition . |
SaveAction(SaveAction.AutomatonPersistenceType type,
Automaton automaton,
String filename)
Creates a new save action which saves the automaton
automaton to the file named by
filename . |
ShiftAutomatonAction(Automaton automaton,
Cospan cospan)
Creates an action which constructs the product automaton for two given automata.
|
ShiftAutomatonAction(Automaton automaton,
CospanDecomposition decomposition)
Creates an action which constructs the product automaton for two given automata.
|
SimulationAntichainInvariantCheckingAction(Algorithm.SearchType type,
boolean computeCounterExample,
Automaton automaton,
CospanDecomposition leftHandSide,
CospanDecomposition rightHandSide)
Creates a new
Action to execute the simulation-based invariant check for the
automaton automaton and the left- resp. right-hand side leftHandSide and
rightHandSide . |
SimulationAntichainLanguageInclusionAction(Algorithm.SearchType type,
boolean computeCounterExample,
Automaton firstAutomaton,
Automaton secondAutomaton)
Creates a new
Action to execute the antichain-based language inclusion check for the
two automata firstAutomaton and secondAutomaton . |
SimulationAntichainUniversalityAction(Algorithm.SearchType type,
boolean computeCounterExample,
Automaton automaton)
Creates a new
Action to execute the antichain-based universality check for the
automaton automaton . |
SimulationComputationAction(Algorithm.SearchType type,
Automaton automaton)
Creates a new
Action to compute the simulation relation for the automaton
automaton |
SimulationComputationAction(Algorithm.SearchType type,
Automaton firstAutomaton,
Automaton secondAutomaton)
Creates a new
Action to compute the simulation relation for the automata
firstAutomaton and secondAutomaton |
SimulationComputationAction(Automaton automaton)
Creates a new
Action to compute the simulation relation for the automaton
automaton |
SimulationComputationAction(Automaton firstAutomaton,
Automaton secondAutomaton)
Creates a new
Action to compute the simulation relation for the automata
firstAutomaton and secondAutomaton |
UnionAutomatonAction(Automaton first,
Automaton second)
Creates an action which constructs the union automaton for two given automata.
|
Modifier and Type | Method and Description |
---|---|
boolean |
BackwardEmptinessCheck.acceptsEmptyLanguage(Automaton automaton) |
boolean |
ForwardEmptinessCheck.acceptsEmptyLanguage(Automaton automaton) |
boolean |
EmptinessCheckAlgorithm.acceptsEmptyLanguage(Automaton automaton)
Returns
true if and only if the language of the automaton automaton is the |
RavenBDD |
IdentityRelationAlgorithm.getIdentityRelation(Automaton automaton)
Returns the identity relation on the states of the automaton
automaton . |
RavenBDD |
ForwardSimulationAlgorithm.getSimulation(Automaton automaton) |
RavenBDD |
SimulationAlgorithm.getSimulation(Automaton automaton)
Returns the simulation relation on the states of the automaton
automaton . |
RavenBDD |
BackwardSimulationAlgorithm.getSimulation(Automaton automaton) |
RavenBDD |
ForwardSimulationAlgorithm.getSimulation(Automaton firstAutomaton,
Automaton secondAutomaton) |
RavenBDD |
SimulationAlgorithm.getSimulation(Automaton firstAutomaton,
Automaton secondAutomaton)
Returns the simulation relation on the states of the automata
firstAutomaton
and secondAutomaton . |
RavenBDD |
BackwardSimulationAlgorithm.getSimulation(Automaton firstAutomaton,
Automaton secondAutomaton) |
boolean |
LanguageEquivalenceAlgorithm.isEquivalent(Automaton first,
Automaton second)
Checks whether the language of the first automaton
first is equivalent to
the language of the second automaton second . |
boolean |
BisimulationUpToCongruenceLanguageEquivalence.isEquivalent(Automaton first,
Automaton second) |
boolean |
LanguageInclusionAlgorithm.isIncluded(Automaton first,
Automaton second)
Checks whether the language of the first automaton
first is included in
the language of the second automaton second . |
boolean |
SimulationAntichainLanguageInclusion.isIncluded(Automaton first,
Automaton second) |
boolean |
BisimulationUpToCongruenceLanguageInclusion.isIncluded(Automaton first,
Automaton second) |
boolean |
AntichainLanguageInclusion.isIncluded(Automaton first,
Automaton second) |
boolean |
AntichainInvariantChecking.isInvariant(Automaton automaton,
CospanDecomposition leftHandSide,
CospanDecomposition rightHandSide) |
boolean |
SimulationAntichainInvariantChecking.isInvariant(Automaton automaton,
CospanDecomposition leftHandSide,
CospanDecomposition rightHandSide) |
boolean |
InvariantCheckingAlgorithm.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 . |
boolean |
BisimulationUpToCongruenceInvariantChecking.isInvariant(Automaton automaton,
CospanDecomposition leftHandSide,
CospanDecomposition rightHandSide) |
boolean |
MembershipAlgorithm.isMemberOf(Automaton automaton,
CospanDecomposition decomposition)
Returns
true if and only if the automaton automaton accepts the cospan
decomposition decomposition . |
boolean |
DefaultMembershipAlgorithm.isMemberOf(Automaton automaton,
CospanDecomposition decomposition) |
boolean |
ForwardSimulationAlgorithm.isSimulatedBy(Automaton firstAutomaton,
Automaton secondAutomaton,
RavenBDD firstStateSet,
RavenBDD secondStateSet) |
boolean |
SimulationAlgorithm.isSimulatedBy(Automaton firstAutomaton,
Automaton secondAutomaton,
RavenBDD firstStateSet,
RavenBDD secondStateSet)
Returns
true if and only if the state set firstStateSet of the first
automaton firstAutomaton is simulated by the state set secondStateSet
of the second automaton secondAutomaton . |
boolean |
BackwardSimulationAlgorithm.isSimulatedBy(Automaton firstAutomaton,
Automaton secondAutomaton,
RavenBDD firstStateSet,
RavenBDD secondStateSet) |
boolean |
ForwardSimulationAlgorithm.isSimulatedBy(Automaton firstAutomaton,
RavenBDD firstStateSet,
RavenBDD secondStateSet) |
boolean |
SimulationAlgorithm.isSimulatedBy(Automaton automaton,
RavenBDD firstStateSet,
RavenBDD secondStateSet)
Returns
true if and only if the state set firstStateSet of the automaton
automaton is simulated by the second state set secondStateSet of the
automaton automaton . |
boolean |
BackwardSimulationAlgorithm.isSimulatedBy(Automaton firstAutomaton,
RavenBDD firstStateSet,
RavenBDD secondStateSet) |
boolean |
SimulationAntichainUniversality.isUniversal(Automaton automaton) |
boolean |
UniversalityAlgorithm.isUniversal(Automaton automaton)
Returns
true if and only if the automaton automaton is universal. |
boolean |
AntichainUniversality.isUniversal(Automaton automaton) |
Modifier and Type | Class and Description |
---|---|
class |
ColorabilityAutomaton
This class implements a graph automaton accepting the language of all graphs which are
k-colorable.
|
class |
DominatingSetAutomaton
This class implements a graph automaton accepting the language of all graphs which have a
dominating set of size at most k, i.e. a set D of nodes with size at most k
such that each node of the graph is either in D or adjacent to a node in D.
|
class |
EdgeCountingAutomaton
This class implements a graph automaton accepting the language of all graphs whose number of
edges of a specific kind is equal to remainder modulo divisor.
|
class |
LinkAutomaton
This class implements a graph automaton accepting all graphs that have an
edge between a node from the inner to a node from the outer interface.
|
class |
MaximumEdgeAutomaton
This class implements a graph automaton accepting the language of all graphs
whose number of edges is at most maximum.
|
class |
MaximumVertexAutomaton
This class implements a graph automaton accepting the language of all graphs
whose number of nodes is at most maximum.
|
class |
MinimumEdgeAutomaton
This class implements a graph automaton accepting the language of all graphs
whose number of edges is at least minimum.
|
class |
MinimumVertexAutomaton
This class implements a graph automaton accepting the language of all graphs
whose number of nodes is at least minimum.
|
class |
NoIsolatedNodesAutomaton
This class implements a graph automaton accepting the language of all graphs which do not
contain any isolated node.
|
class |
PathAutomaton
This class implements a graph automaton accepting the language of all graphs
where certain nodes are connected by a path.
|
class |
ProductAutomaton
This class implements a graph automaton accepting the language which is obtained by the
intersection of the languages of the two underlying graph automata.
|
class |
SubgraphAutomaton
This class implements a graph automaton accepting the language of all graphs which contain a
specific graph as subgraph.
|
class |
UnionAutomaton
This class implements a graph automaton accepting the language which is obtained by the
union of the languages of the two underlying graph automata.
|
class |
VertexCountingAutomaton
This class implements a graph automaton accepting the language of all graphs whose number of
nodes is equal to remainder modulo divisor.
|
class |
VertexCoverAutomaton
This class implements a graph automaton accepting the language of all graphs which have a
vertex cover of size at most k, i.e. a set C of nodes with size at most k
such that each edge of the graph is incident to at least one node of C.
|
Modifier and Type | Method and Description |
---|---|
Automaton |
MaximumEdgeAutomaton.clone() |
Automaton |
LinkAutomaton.clone() |
Automaton |
EdgeCountingAutomaton.clone() |
Automaton |
VertexCountingAutomaton.clone() |
Automaton |
SubgraphAutomaton.clone() |
Automaton |
MinimumVertexAutomaton.clone() |
Automaton |
NoIsolatedNodesAutomaton.clone() |
abstract Automaton |
Automaton.clone() |
Automaton |
ProductAutomaton.clone() |
Automaton |
MinimumEdgeAutomaton.clone() |
Automaton |
UnionAutomaton.clone() |
Automaton |
MaximumVertexAutomaton.clone() |
Automaton |
VertexCoverAutomaton.clone() |
Automaton |
PathAutomaton.clone() |
Automaton |
ColorabilityAutomaton.clone() |
Automaton |
DominatingSetAutomaton.clone() |
static Automaton |
AutomatonFactory.shiftAutomaton(Automaton automaton,
CospanDecomposition decomposition)
Creates a new automaton which is shifted over the cospan decomposition
decomposition
i.e. the initial states of the new automaton are states reachable by the original automaton
after processing the cospan decomposition decomposition . |
Modifier and Type | Method and Description |
---|---|
ProductAutomaton |
AutomatonFactory.createProductAutomaton(Automaton first,
Automaton second)
Creates a new product automaton out of the automata
first and second . |
UnionAutomaton |
AutomatonFactory.createUnionAutomaton(Automaton first,
Automaton second)
Creates a new union automaton out of the automata
first and second . |
static RavenBDDPairing |
Automaton.getInterfacePairing(Automaton first,
Automaton second)
Returns a BDD pairing which pairs the the interface bits of the two
automata
first and second . |
static Automaton |
AutomatonFactory.shiftAutomaton(Automaton automaton,
CospanDecomposition decomposition)
Creates a new automaton which is shifted over the cospan decomposition
decomposition
i.e. the initial states of the new automaton are states reachable by the original automaton
after processing the cospan decomposition decomposition . |
Modifier and Type | Method and Description |
---|---|
Automaton |
ProductEncoding.getFirstAutomaton()
Returns the first automaton.
|
Automaton |
UnionEncoding.getFirstAutomaton()
Returns the first automaton.
|
Automaton |
ProductEncoding.getSecondAutomaton()
Returns the second automaton.
|
Automaton |
UnionEncoding.getSecondAutomaton()
Returns the second automaton.
|
Modifier and Type | Method and Description |
---|---|
RavenBDD |
ProductEncoding.convertFinalStates(Automaton automaton)
Converts the final state set of the given automaton to the
UnionEncoding . |
RavenBDD |
UnionEncoding.convertFinalStates(Automaton automaton)
Converts the final state set of the given automaton to the
UnionEncoding . |
RavenBDD |
ProductEncoding.convertInitialStates(Automaton automaton)
Converts the initial state set of the given automaton to the
UnionEncoding . |
RavenBDD |
UnionEncoding.convertInitialStates(Automaton automaton)
Converts the initial state set of the given automaton to the
UnionEncoding . |
RavenBDD |
ProductEncoding.convertNonFinalStates(Automaton automaton)
Converts the non-final state set of the given automaton to the
UnionEncoding . |
RavenBDD |
UnionEncoding.convertNonFinalStates(Automaton automaton)
Converts the non-final state set of the given automaton to the
UnionEncoding . |
RavenBDD |
ProductEncoding.convertStates(Automaton automaton)
Converts the state set of the given automaton to the
UnionEncoding . |
RavenBDD |
UnionEncoding.convertStates(Automaton automaton)
Converts the state set of the given automaton to the
UnionEncoding . |
RavenBDD |
ProductEncoding.convertTransitions(Automaton automaton,
Operation letter)
Converts the transitions of the given automaton and the given letter to the
UnionEncoding . |
RavenBDD |
UnionEncoding.convertTransitions(Automaton automaton,
Operation letter)
Converts the transitions of the given automaton and the given letter to the
UnionEncoding . |
static ProductEncoding |
ProductEncoding.getEncoding(Automaton first,
Automaton second)
Returns the default BDD encoding for a product of two BDD encodings.
|
static UnionEncoding |
UnionEncoding.getEncoding(Automaton first,
Automaton second)
Returns the default BDD encoding for a union of two automata.
|
Modifier and Type | Method and Description |
---|---|
static void |
BDDDialog.showDialog(Window owner,
Automaton automaton,
Operation letter)
Shows the dialog for displaying BDDs which encode transitions of the automaton
automaton for the letter letter . |
void |
GraphWindow.showRun(Automaton automaton,
CospanDecomposition decomposition)
Shows the run of the automaton
automaton on the cospan decomposition decomposition . |
Modifier and Type | Class and Description |
---|---|
class |
AutomatonInformationPanel<T extends Automaton>
This class provides graphical components to display the properties of graph automata objects.
|
Modifier and Type | Method and Description |
---|---|
void |
AutomatonRunView.print(Automaton automaton,
CospanDecomposition decomposition)
Prints the run of the automaton
automaton on the cospan decomposition decomposition . |
Modifier and Type | Method and Description |
---|---|
static VisualGraph |
VisualGraph.getVisualGraph(Automaton automaton,
CospanDecomposition decomposition)
Creates a graph visualization of the run of the automaton
automaton on
the decomposition decomposition . |
Modifier and Type | Method and Description |
---|---|
Automaton |
AutomatonReader.readAutomaton(String filename)
Reads an automaton from the given zip archive, puts it into the
repository and returns it.
|
Automaton |
AutomatonFileReader.readAutomaton(String filename) |
Modifier and Type | Method and Description |
---|---|
void |
RunPrinter.print(Automaton automaton,
CospanDecomposition decomposition)
Prints the run of an automaton on a decomposition to this printer.
|
void |
ExecutionPrinter.print(Automaton automaton,
CospanDecomposition decomposition)
Prints a run of the automaton
automaton on the cospan decomposition decomposition . |
void |
DotPrinter.print(Automaton automaton,
CospanDecomposition decomposition) |
void |
TextAreaPrinter.printAutomaton(Automaton automaton) |
void |
ConsolePrinter.printAutomaton(Automaton automaton) |
void |
AutomatonPrinter.printAutomaton(Automaton automaton)
Prints an automaton to this printer.
|
void |
PlainTextWriter.write(Automaton automaton,
String filename) |
void |
AutomatonWriter.write(Automaton automaton,
String filename)
Writes an automaton to the file specified by
filename . |
void |
AutomatonFileWriter.write(Automaton automaton,
String zipname)
Writes an automaton to the zip archive specified by
zipname . |