Hi Jianwen, On Fri, Jun 8, 2012 at 5:44 PM, Jianwen Li <lijwen2748(a)gmail.com> wrote: The tgba class defines a read-only interface that only allows you to explore the automaton, but not to modify it. Some subclasses of tgba use a graph to store the automaton explicitly. You may want to look for tgba_explicit_numbered, tgba_explicit_string, tgba_explicit_formula depending on whether your states are labelled by integers, strings, or LTL formulas. All these types are actually specialization of the explicit_graph class, which implements the tgba interface as well as a few other methods to modify the automaton. Other subclasses such as tgba_bdd_concrete represent the automaton symbolically using BDDs. You may also chose not to represent the automaton at all, but compute it on the fly. In that case your algorithm should be a class that inherits from tgba, and implement its interface (for instance the product of two automata is implemented this way). -- Alexandre Duret-Lutz