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