org.processmining.ltl2automaton.plugins

Class LTL2Automaton

java.lang.Object

org.processmining.ltl2automaton.plugins.LTL2Automaton

public class LTL2Automaton
extends java.lang.Object

Constructor Summary

Constructors

Modifier	Constructor and Description
protected	LTL2Automaton()

Method Summary

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)

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Constructor Detail

LTL2Automaton

protected LTL2Automaton()

Method Detail

getInstance

public static LTL2Automaton getInstance()

parseFormula

public Formula parseFormula(java.lang.String ltl,
                            boolean negate)
                     throws java.lang.Exception

Throws:

java.lang.Exception

translate

public Automaton translate(java.util.Collection<Formula> formulas)
                    throws java.lang.Exception

Throws:

java.lang.Exception

translate

public Automaton translate(Formula formula)
                    throws java.lang.Exception

Throws:

java.lang.Exception

translate

public Conjunction translate(Formula formula,
                             boolean factorize)
                      throws java.lang.Exception

Throws:

java.lang.Exception

translate

public Conjunction translate(java.util.Collection<Formula> formulas,
                             boolean factorize)
                      throws java.lang.Exception

Throws:

java.lang.Exception

translate

public void translate(Formula formula,
                      AutomatonFactory factory,
                      boolean singleProperty)
               throws java.lang.Exception

Throws:

java.lang.Exception

translate

public 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

Throws:

java.lang.Exception

translate

public Conjunction translate(java.lang.String ltl,
                             boolean factorize)
                      throws java.lang.Exception

Throws:

java.lang.Exception

translate

public Automaton translate(java.lang.String ltl)
                    throws java.lang.Exception

Throws:

java.lang.Exception

translateDeterministicAutomatonOperation

public DeterministicAutomaton translateDeterministicAutomatonOperation(Formula formula,
                                                                       boolean minimizeSubAutomata,
                                                                       boolean deep,
                                                                       java.util.Map<java.lang.String,DeterministicAutomaton> cache)
                                                                throws java.lang.Exception

Throws:

java.lang.Exception

translateNondeterministicAutomatonOperation

public Automaton translateNondeterministicAutomatonOperation(Formula formula,
                                                             boolean minimizeSubAutomata)
                                                      throws java.lang.Exception

Throws:

java.lang.Exception

translateSimple

public Automaton translateSimple(Formula formula,
                                 boolean singleProperty)
                          throws java.lang.Exception

Throws:

java.lang.Exception