| Modifier and Type | Method and Description |
|---|---|
Formula |
LTL2Automaton.parseFormula(java.lang.String ltl,
boolean negate) |
| Modifier and Type | Method and Description |
|---|---|
Automaton |
LTL2Automaton.translate(Formula formula) |
void |
LTL2Automaton.translate(Formula formula,
AutomatonFactory factory,
boolean singleProperty) |
Conjunction |
LTL2Automaton.translate(Formula formula,
boolean factorize) |
Automaton |
LTL2Automaton.translate(Formula ltl,
boolean singleProperty,
boolean useAutomatonProperties,
boolean minimizeSubAutomata,
boolean deep,
boolean deterministic,
java.util.Map<java.lang.String,DeterministicAutomaton> cache) |
DeterministicAutomaton |
LTL2Automaton.translateDeterministicAutomatonOperation(Formula formula,
boolean minimizeSubAutomata,
boolean deep,
java.util.Map<java.lang.String,DeterministicAutomaton> cache) |
Automaton |
LTL2Automaton.translateNondeterministicAutomatonOperation(Formula formula,
boolean minimizeSubAutomata) |
Automaton |
LTL2Automaton.translateSimple(Formula formula,
boolean singleProperty) |
| Modifier and Type | Method and Description |
|---|---|
Automaton |
LTL2Automaton.translate(java.util.Collection<Formula> formulas) |
Conjunction |
LTL2Automaton.translate(java.util.Collection<Formula> formulas,
boolean factorize) |
| Constructor and Description |
|---|
SinglePropertyGraph(Formula frm,
AutomatonFactory factory) |
| Modifier and Type | Method and Description |
|---|---|
static Formula |
CupParser.parse(java.lang.String ltl) |
| Modifier and Type | Method and Description |
|---|---|
Formula |
DefaultFormulaFactory.Always(Formula f) |
Formula |
DefaultFormulaFactory.And(Formula sx,
Formula dx) |
Formula |
Formula.clone() |
Formula |
DefaultFormulaFactory.create(char c,
Formula sx,
Formula dx,
java.lang.String n) |
Formula |
DefaultFormulaFactory.Equal(Formula lf,
Formula rf) |
Formula |
DefaultFormulaFactory.Eventually(Formula f) |
Formula |
DefaultFormulaFactory.False() |
Formula |
Formula.getLeft() |
Formula |
Formula.getNext() |
Formula |
Formula.getRight() |
Formula |
Formula.getSub1() |
Formula |
Formula.getSub2() |
Formula |
DefaultFormulaFactory.Implies(Formula sx,
Formula dx) |
Formula |
Formula.negate() |
Formula |
DefaultFormulaFactory.Next(Formula f) |
Formula |
DefaultFormulaFactory.Not(Formula f) |
Formula |
DefaultFormulaFactory.Or(Formula sx,
Formula dx) |
Formula |
DefaultFormulaFactory.Proposition(java.lang.String name) |
Formula |
DefaultFormulaFactory.Release(Formula sx,
Formula dx) |
Formula |
DefaultFormulaFactory.True() |
Formula |
DefaultFormulaFactory.Until(Formula sx,
Formula dx) |
Formula |
DefaultFormulaFactory.WNext(Formula f) |
Formula |
DefaultFormulaFactory.WRelease(Formula sx,
Formula dx) |
Formula |
DefaultFormulaFactory.WUntil(Formula sx,
Formula dx) |
| Modifier and Type | Method and Description |
|---|---|
Formula |
DefaultFormulaFactory.Always(Formula f) |
Formula |
DefaultFormulaFactory.And(Formula sx,
Formula dx) |
Formula |
DefaultFormulaFactory.create(char c,
Formula sx,
Formula dx,
java.lang.String n) |
Formula |
DefaultFormulaFactory.Equal(Formula lf,
Formula rf) |
Formula |
DefaultFormulaFactory.Eventually(Formula f) |
Formula |
DefaultFormulaFactory.Implies(Formula sx,
Formula dx) |
Formula |
DefaultFormulaFactory.Next(Formula f) |
Formula |
DefaultFormulaFactory.Not(Formula f) |
Formula |
DefaultFormulaFactory.Or(Formula sx,
Formula dx) |
Formula |
DefaultFormulaFactory.Release(Formula sx,
Formula dx) |
Formula |
DefaultFormulaFactory.Until(Formula sx,
Formula dx) |
Formula |
DefaultFormulaFactory.WNext(Formula f) |
Formula |
DefaultFormulaFactory.WRelease(Formula sx,
Formula dx) |
Formula |
DefaultFormulaFactory.WUntil(Formula sx,
Formula dx) |
| Modifier and Type | Method and Description |
|---|---|
boolean |
Formula.isSpecialRelease(java.util.Collection<Formula> formulas) |
boolean |
Formula.isSyntacticallyImplied(java.util.Collection<Formula> old,
java.util.Collection<Formula> next) |
boolean |
Formula.isSyntacticallyImplied(java.util.Collection<Formula> old,
java.util.Collection<Formula> next) |
| Constructor and Description |
|---|
Formula(char c,
Formula sx,
Formula dx,
java.lang.String n) |
| Modifier and Type | Field and Description |
|---|---|
protected java.util.Map<Formula,ConjunctionTreeLeaf> |
UnsortedTreeConjunction.formulaMap |
| Modifier and Type | Method and Description |
|---|---|
Formula |
ConjunctionTreeLeaf.getFormula() |
| Modifier and Type | Method and Description |
|---|---|
java.util.Collection<java.util.Set<Formula>> |
PartitionedConjunction.getPartitions() |
java.util.Iterator<Formula> |
ConjunctionTreeLeaf.iterator() |
java.util.Iterator<Formula> |
ConjunctionTreeNode.iterator() |
java.util.Iterator<Formula> |
QuickAddConjunction.iterator() |
java.util.Iterator<Formula> |
UnsortedTreeConjunction.iterator() |
| Modifier and Type | Method and Description |
|---|---|
static boolean |
FormulaTools.acceptsAllInit(java.util.Map<ConjunctionTreeNode,Automaton> cache,
Formula formula) |
void |
Conjunction.add(Formula term) |
void |
PartitionedConjunction.add(Formula term) |
void |
QuickAddConjunction.add(Formula term) |
void |
UnsortedTreeConjunction.add(Formula term) |
static boolean |
FormulaTools.containsNext(Formula f) |
ConjunctionTreeLeaf |
DefaultTreeFactory.createLeaf(Formula f,
char name) |
L |
TreeFactory.createLeaf(Formula f,
char name) |
static java.util.Collection<java.lang.String> |
FormulaTools.getAtomicPropositions(Formula f) |
T |
ConjunctionFactory.instance(Formula terms) |
void |
Conjunction.remove(Formula term) |
void |
GroupedTreeConjunction.remove(Formula term) |
void |
PartitionedConjunction.remove(Formula term) |
void |
QuickAddConjunction.remove(Formula term) |
void |
SizeSortedTreeConjunction.remove(Formula term) |
void |
UnsortedTreeConjunction.remove(Formula term) |
void |
Conjunction.setAll(Formula terms) |
void |
QuickAddConjunction.setAll(Formula terms) |
void |
UnsortedTreeConjunction.setAll(Formula f) |
void |
ConjunctionTreeLeaf.setFormula(Formula f) |
| Modifier and Type | Method and Description |
|---|---|
T |
ConjunctionFactory.instance(java.util.Collection<Formula> terms) |
void |
Conjunction.setAll(java.util.Collection<Formula> terms) |
void |
GroupedTreeConjunction.setAll(java.util.Collection<Formula> formulas) |
void |
PartitionedConjunction.setAll(java.util.Collection<Formula> formulas) |
void |
QuickAddConjunction.setAll(java.util.Collection<Formula> terms) |
void |
SizeSortedTreeConjunction.setAll(java.util.Collection<Formula> formulas) |
void |
UnsortedTreeConjunction.setAll(java.util.Collection<Formula> formulas) |
| Constructor and Description |
|---|
ConjunctionTreeLeaf(Formula f,
char name) |
GroupedTreeConjunction(TreeFactory<ConjunctionTreeNode,ConjunctionTreeLeaf> treefactory,
Formula f) |
PartitionedConjunction(TreeFactory<ConjunctionTreeNode,ConjunctionTreeLeaf> treefactory,
ConjunctionFactory<? extends UnsortedTreeConjunction> factory,
Formula f) |
QuickAddConjunction(UnsortedTreeConjunction base,
Formula f) |
SizeSortedTreeConjunction(TreeFactory<ConjunctionTreeNode,ConjunctionTreeLeaf> treefactory,
Formula f) |
UnsortedTreeConjunction(TreeFactory<ConjunctionTreeNode,ConjunctionTreeLeaf> treefactory,
Formula f) |
| Constructor and Description |
|---|
GroupedTreeConjunction(TreeFactory<ConjunctionTreeNode,ConjunctionTreeLeaf> treefactory,
java.util.Collection<Formula> formulas) |
PartitionedConjunction(TreeFactory<ConjunctionTreeNode,ConjunctionTreeLeaf> treefactory,
ConjunctionFactory<? extends UnsortedTreeConjunction> factory,
java.util.Collection<Formula> terms) |
QuickAddConjunction(UnsortedTreeConjunction base,
java.util.Collection<Formula> formulas) |
SizeSortedTreeConjunction(TreeFactory<ConjunctionTreeNode,ConjunctionTreeLeaf> treefactory,
java.util.Collection<Formula> formulas) |
UnsortedTreeConjunction(TreeFactory<ConjunctionTreeNode,ConjunctionTreeLeaf> treefactory,
java.util.Collection<Formula> formulas) |