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