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 |
Classes to create, represent, manipulate data.
|
de.uni_due.inf.ti.raven.data.automata |
Classes to create, represent, manipulate 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 |
---|---|
CospanDecomposition |
CospanDecomposeAction.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 . |
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 . |
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(DecompositionPrinter printer,
CospanDecomposition decomposition)
Creates an action which prints a graph decomposition to a given printer.
|
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(CospanDecomposition decomposition,
String filename)
Creates a new save action which saves the decomposition
decomp to the file
named by filename . |
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 . |
Modifier and Type | Method and Description |
---|---|
CospanDecomposition |
DefaultCospanDecompositionAlgorithm.decompose(Cospan cospan) |
CospanDecomposition |
CospanDecompositionAlgorithm.decompose(Cospan cospan)
Returns a cospan decomposition of the cospan
cospan . |
Modifier and Type | Method and Description |
---|---|
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) |
Modifier and Type | Method and Description |
---|---|
CospanDecomposition |
CospanCounterExample.getCospan()
Returns the cospan decomposition of the counter-example graph.
|
static CospanDecomposition |
CospanDecomposition.getCospanDecomposition(GraphDecomposition decomposition)
Returns a cospan decomposition created from the graph decomposition
decomposition |
static CospanDecomposition |
CospanDecomposition.getCospanDecomposition(PathDecomposition pathDecomposition)
Returns a cospan decomposition created from the path decomposition
decomposition |
static CospanDecomposition |
CospanDecomposition.getCospanDecomposition(TreeDecomposition decomposition)
Returns a cospan decomposition created from the tree decomposition
decomposition |
CospanDecomposition |
RuleCounterExample.getSource()
Returns the cospan decomposition of the left hand-side used as a counter-example
|
CospanDecomposition |
RuleCounterExample.getTarget()
Returns the cospan decomposition of the right hand-side used as a counter-example
|
Modifier and Type | Method and Description |
---|---|
void |
CospanDecomposition.add(CospanDecomposition decomposition)
Adds the cospan decomposition
decomposition (seen as a list of operations) to this graph. |
Constructor and Description |
---|
Cospan(CospanDecomposition decomposition)
Creates a new cospan by copying the cospan decomposition
decomposition information. |
CospanCounterExample(CospanDecomposition cd)
Creates a new cospan counter-example
|
CospanDecomposition(CospanDecomposition decomposition)
Creates a new cospan decomposition by copying the cospan decomposition
decomposition . |
RuleCounterExample(CospanDecomposition leftHandSide,
CospanDecomposition rightHandSide,
CospanDecomposition context)
Creates a new rule counter-example
|
Modifier and Type | Method and Description |
---|---|
RavenBDD |
Automaton.getReachableStates(CospanDecomposition decomposition)
Returns the set of reachable states for a given graph decomposition
starting with the initial states.
|
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 |
---|---|
static InformationPanel<CospanDecomposition> |
CospanDecompositionInformationPanelBuilder.createPanel()
Creates an information panel displaying properties of a given cospan decomposition.
|
Modifier and Type | Method and Description |
---|---|
void |
CounterExampleWindow.showCounterExampleChooser(CospanDecomposition element,
String title)
Shows the chosen element
decomposition in this window. |
void |
GraphWindow.showDecomposition(CospanDecomposition decomposition,
String title)
Shows the Decomposition
decomposition in this window. |
void |
CounterExampleWindow.showRuleCounterExampleChooser(CospanDecomposition left,
CospanDecomposition right,
String title)
Shows the chosen element
decomposition in this window. |
void |
GraphWindow.showRun(Automaton automaton,
CospanDecomposition decomposition)
Shows the run of the automaton
automaton on the cospan decomposition decomposition . |
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 . |
void |
DecompositionView.print(CospanDecomposition decomposition) |
Modifier and Type | Method and Description |
---|---|
static CospanDecomposition |
OperationFileReader.readOperations(File file)
Reads an operation file
file and returns the cospan decomposition obtained from
the operation list. |
static CospanDecomposition |
OperationFileReader.readOperations(String filename)
Reads an operation file specified by the filename
filename and returns
the cospan decomposition obtained from the operation list. |
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.print(CospanDecomposition decomposition) |
void |
DotPrinter.print(CospanDecomposition decomposition) |
void |
DecompositionPrinter.print(CospanDecomposition decomposition)
Prints a cospan decomposition to this printer.
|
void |
ConsolePrinter.print(CospanDecomposition decomposition) |
static void |
CospanDecompositionFileWriter.writeOperations(String filename,
CospanDecomposition decomposition)
Writes a cospan decomposition to a file.
|