Dear sir: I recently try to implement the algorithm translating LTL formulas to Buchi automata in the SPOT framework. When I read the source codes of SPOT I was confused about the structure of the automaton. How did you store the transitions and states in the automaton, such as tgba? I am sorry I can't catch you since I do not see any structure storing them when you define the tgba (tgba.hh, tgba.cc).
Thank you for your attention.
Best Jianwen
Hi Jianwen,
On Fri, Jun 8, 2012 at 5:44 PM, Jianwen Li lijwen2748@gmail.com wrote:
When I read the source codes of SPOT I was confused about the structure of the automaton. How did you store the transitions and states in the automaton, such as tgba?
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 -
Jianwen Li