Hi,

I am a Grad Student at Vanderbilt University,TN,USA and am working on formal verification of software systems. I was using spot library and your site and wanted to know : if a TGBA ( Transition based generalized Buchi automaton) has all transitions as accepting transitions by definition then what is this {ACC[r]} condition that explicitly appears ion automaton when I write LTL formula : F r. And why don’t I get any such thing when I use LTL formula : X r.

I will appreciate your reply.

Thanks in advance,

Akshay Agrawal