
8 Jun
2012
8 Jun
'12
5:44 p.m.
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