public class LTL2Automaton
extends java.lang.Object
| Modifier | Constructor and Description |
|---|---|
protected |
LTL2Automaton() |
| Modifier and Type | Method and Description |
|---|---|
static LTL2Automaton |
getInstance() |
Formula |
parseFormula(java.lang.String ltl,
boolean negate) |
Automaton |
translate(java.util.Collection<Formula> formulas) |
Conjunction |
translate(java.util.Collection<Formula> formulas,
boolean factorize) |
Automaton |
translate(Formula formula) |
void |
translate(Formula formula,
AutomatonFactory factory,
boolean singleProperty) |
Conjunction |
translate(Formula formula,
boolean factorize) |
Automaton |
translate(Formula ltl,
boolean singleProperty,
boolean useAutomatonProperties,
boolean minimizeSubAutomata,
boolean deep,
boolean deterministic,
java.util.Map<java.lang.String,DeterministicAutomaton> cache) |
Automaton |
translate(java.lang.String ltl) |
Conjunction |
translate(java.lang.String ltl,
boolean factorize) |
DeterministicAutomaton |
translateDeterministicAutomatonOperation(Formula formula,
boolean minimizeSubAutomata,
boolean deep,
java.util.Map<java.lang.String,DeterministicAutomaton> cache) |
Automaton |
translateNondeterministicAutomatonOperation(Formula formula,
boolean minimizeSubAutomata) |
Automaton |
translateSimple(Formula formula,
boolean singleProperty) |
public static LTL2Automaton getInstance()
public Formula parseFormula(java.lang.String ltl, boolean negate) throws java.lang.Exception
java.lang.Exceptionpublic Automaton translate(java.util.Collection<Formula> formulas) throws java.lang.Exception
java.lang.Exceptionpublic Automaton translate(Formula formula) throws java.lang.Exception
java.lang.Exceptionpublic Conjunction translate(Formula formula, boolean factorize) throws java.lang.Exception
java.lang.Exceptionpublic Conjunction translate(java.util.Collection<Formula> formulas, boolean factorize) throws java.lang.Exception
java.lang.Exceptionpublic void translate(Formula formula, AutomatonFactory factory, boolean singleProperty) throws java.lang.Exception
java.lang.Exceptionpublic Automaton translate(Formula ltl, boolean singleProperty, boolean useAutomatonProperties, boolean minimizeSubAutomata, boolean deep, boolean deterministic, java.util.Map<java.lang.String,DeterministicAutomaton> cache) throws java.lang.Exception
java.lang.Exceptionpublic Conjunction translate(java.lang.String ltl, boolean factorize) throws java.lang.Exception
java.lang.Exceptionpublic Automaton translate(java.lang.String ltl) throws java.lang.Exception
java.lang.Exceptionpublic DeterministicAutomaton translateDeterministicAutomatonOperation(Formula formula, boolean minimizeSubAutomata, boolean deep, java.util.Map<java.lang.String,DeterministicAutomaton> cache) throws java.lang.Exception
java.lang.Exceptionpublic Automaton translateNondeterministicAutomatonOperation(Formula formula, boolean minimizeSubAutomata) throws java.lang.Exception
java.lang.Exception