[I2 logo] [RWTH logo] MOVES: Software Modeling and Verification
(Informatik 2)
Computer Science / RWTH / I2 / Research / RV / Ltl2ba4j / Docs / Api / Rwth / I2 / Ltl2ba4j / LTL2BA4J
Printer-friendly
LTL2BA4J (LTL2BA4J)

rwth.i2.ltl2ba4j
Class LTL2BA4J

java.lang.Object
  extended by rwth.i2.ltl2ba4j.LTL2BA4J

public class LTL2BA4J
extends Object

Author:
Eric Bodden LTL2BA4J - Facade giving access to ltl2ba.

Constructor Summary
LTL2BA4J()
           
 
Method Summary
static Collection<ITransition> formulaToBA(IFormula formula)
          Converts the given formula into a finite state machine.
static Collection<ITransition> formulaToBA(String formulaAsString)
          Converts the given formula into a finite state machine.
static IGraphFactory getGraphFactory()
           
static void main(String[] args)
           
static void setGraphFactory(IGraphFactory customGraphFactory)
          Sets a factory used to generate the resulting graph.
 
Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
 

Constructor Detail

LTL2BA4J

public LTL2BA4J()
Method Detail

formulaToBA

public static Collection<ITransition> formulaToBA(IFormula formula)
Converts the given formula into a finite state machine.

Parameters:
formula - a valid ltl2ba formula the formula must not be longer than 4095 characters
Returns:
the resulting automaton as a list of transitions; if the list is empty, that means that the automaton never matches
Throws:
IllegalArgumentException - if formula has invalid syntax

formulaToBA

public static Collection<ITransition> formulaToBA(String formulaAsString)
Converts the given formula into a finite state machine.

Parameters:
formulaAsString - a valid ltl2ba formula; the formula must not be longer than 4095 characters
Returns:
the resulting automaton as a list of transitions; if the list is empty, that means that the automaton never matches
Throws:
IllegalArgumentException - if formula has invalid syntax

setGraphFactory

public static void setGraphFactory(IGraphFactory customGraphFactory)
Sets a factory used to generate the resulting graph. Default is GraphFactory.

Parameters:
customGraphFactory -
See Also:
GraphFactory

getGraphFactory

public static IGraphFactory getGraphFactory()

main

public static void main(String[] args)
Parameters:
args - the formula


Eric Bodden, RWTH Aachen University, 2005.
Valid HTML 4.01 Strict! Valid CSS!