June 2012 - Spot

Re: [Spot] TGBA Doubt
by Alexandre Duret-Lutz 20 Jun '12

20 Jun '12

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

1 0

how to add new features to spot
by 李建文 19 Jun '12

19 Jun '12

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

2 4

TGBA Doubt
by Agrawal, Akshay 19 Jun '12

19 Jun '12

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

2 1

spot using help
by Jianwen Li 11 Jun '12

11 Jun '12

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

2 1