On Tue, Jun 19, 2012 at 11:48 AM, Agrawal, Akshay
<akshay.agrawal(a)vanderbilt.edu> wrote:
> Dear Alexandre,
> Thank you for a prompt reply. So I think my perception was wrong
> about TGBA. I did not learn about TGBA from SPOT's wiki. I learnt it
> from some papers and Wikipedia. But I think I formed a wrong
> impression.
> So after your explanation I believe that a TGBA for G(p->Xr) is a
> special case of TGBA with all transitions as accepting transitions??
Yes. Any safety formula can be translated into a TGBA without
acceptance set.
> Also, there was a need for me to convert these TGBA generated from
> SPOT to C code so I wanted to know how is Acc[r] logically read??
> Because sometimes in complex TGBA's there are various such accepting
> sets where we may have Acc[r] and Acc[r|q] or something. So the
> Boolean condition in the brackets of Acc[] , how is it read/what
> does it exactly mean?? I think this will help me to get C code out
> of these TGBAs.
You should regard these just as unique strings used to name the
acceptance conditions. They could be numbers, it would not change the
language. When evaluating an ω-word on such an automaton, you want to
see each of these strings infinitely often. The fact that they denote
subformulae is an implementation detail of Spot's translation.
During the translation of LTL into TGBA, the string actually denotes
subformulae that have been promised to hold eventually. (The
transitions that don't have Acc[φ] are the transitions that promise to
see φ later/) See
http://www.lrde.epita.fr/~adl/dl/adl/duret.11.vecos.pdf if you want
more details.
However you may not rely on this second meaning, because some
post-processing (like degeneralization, WDBA-minimization) might
introduce Acc[1]. This Acc[1] is also used during PSL translation.
Obviously it makes not sense to promise "true", since it's always true :-)
If you are confused, just forget about the previous two paragraphs.
Unless you want to change the translation algorithm, there is no need
to know what the argument of Acc[] means.
> Does SPOT give a C code or other type of executable monitor type
> code for generated TGBAs??
Spot does not generate C.
What we call monitor (in Spot at least) is a finite automaton that
accepts all finite prefixes of the executions that satisfy some
formula. Spot can generate a deterministic monitor for any LTL
formula, and will present it as a TGBA without acceptance condition.
See the "monitor" output on the online translator.
--
Alexandre Duret-Lutz
Dear sir:
I am trying to extend spot by adding a new ltl-to-ba translation
algorithm. The brief idea is that I extend the formula structure in spot
so that I can
use the parser for ltl formulas.
Now I have finished the code and want to compile my codes with those in
spot, but I am confused how I can achieve this. Does spot provides some
interfaces that can help someone to extend it?
Thanks very much for attention and I am expecting your reply.
Best
Jianwen
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
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
