- Spot - LRE

LTL operator precedence
by Molnár Vince 08 Jun '15

08 Jun '15

Dear SPOT Developers, I am writing to you to ask what the operator precedence is that you use for parsing LTL formulae. As I use SPOT to translate LTL formulae to automata, but I also need to handle expressions separately, it would be crucial to stay compatible with your implementation. I am working on .NET, so I cannot simply use your library as a parser and AST metamodel. Thank you for your time! Best regards, Vince Molnár

2 1

LTL input format in SPOT
by Jianwen Li 02 Mar '15

02 Mar '15

Dear Alexandre: I am trying to figure out whether SPOT can accept boolean assertions such as "x >1". For example, can SPOT recognize the LTL formula F (x > 1), which is accepted by Promela format? I tried it with SPOT by ./ltl2tgba -f "F (x>1)" and SPOT fails to parse it. But I really want to make sure whether I have used it correctly. Many thanks~ -- Best Regards Jianwen Li

2 1

Negation Propagation using Spot library
by Dennis Park 18 Oct '14

18 Oct '14

Hello, My name is Dennis Park and I'm a student at the University of British Columbia. I am using the Spot library in a research project I am currently working on and I wanted to ask whether the Spot library supports negation propagation. More specifically, I would like to take an ltl formula spot::ltl::formula* f and propagate all negations in f so that negations only occur before atomic propositions. Does the Spot library support such a functionality? If so, where in the documentation could I find information on it (I tried to look for something like it in the documentation but had trouble finding anything). Thank you, Dennis Park

2 1

Question sur la simplification de formules LTL
by Amélie DAVID 14 Oct '14

14 Oct '14

Bonjour, Je suis en doctorat d'informatique à l'université d'Evry et je travaille sur la logique ATL. Je viens de découvrir votre outil Spot et en particulier l'outil de simplification des formules. Je suis entrain de développer des méthodes de tableaux pour ATL, et je souhaiterais également pouvoir simplifier les formules fournies en entrée de l'outil. J'aurais donc voulu savoir s'il existait une référence dans la littérature ou une compilation de l'ensemble (ou en tout cas la majorité) de ces simplifications. J'ai beau chercher depuis un petit moment et je n'ai rien trouvé à l'exception de votre outil Spot. Merci d'avance pour l'aide que vous pourriez m'apporter concernant cette question. Bien cordialement, Amélie DAVID

2 1

I'd like to add you to my professional network on LinkedIn
by Jianwen Li 23 Sep '14

23 Sep '14

Hi, I'd like to add you to my professional network on LinkedIn. - Jianwen Accept: http://www.linkedin.com/blink?simpleRedirect=czgSdPsUcjsSdP4Zh4BKrSBQonhFtC… You received an invitation to connect. LinkedIn will use your email address to make suggestions to our members in features like People You May Know. Unsubscribe here: http://www.linkedin.com/blink?simpleRedirect=79Chj8BonhFs6l5cylBp79Ic3gBt6Z… Learn why we included this at the following link: http://www.linkedin.com/blink?simpleRedirect=e3wTd3RAimlIoSBQsC4Ct7dBtmtvpn… © 2014, LinkedIn Corporation. 2029 Stierlin Ct. Mountain View, CA 94043, USA

1 0

[LTL2TGBA] SPOT translation produces unexpected results
by Caroline Lemieux 13 Aug '14

13 Aug '14

Hello, I'm an undergraduate student at UBC working on a log analysis project under Ivan Beschastnikh <http://www.cs.ubc.ca/~bestchai/>. I'm using SPOT in the project to parse LTL strings into formulae, and now trying to use the translation to automata functionality. The situation I'm dealing with would involve passing a finite sequence of states into the automaton, and the description of the Monitor output appeared to be what I needed. However, the monitor DFA provided for the response formula G(a->Fb) was an all-accepting DFA: which didn't seem to align with the given definition of monitor. I've been searching the documentation, but can't find anything more describing why this DFA would be produced. I've also been looking for a description of acceptance condition syntax, especially for the state-based degeneralized Buchi automaton, where both edges and states are labeled as accepting. Could you direct me to any documentation on these subjects or give any insight on why the above monitor is being produced for the response pattern? (As defined by the specification pattern project here <http://patterns.projects.cis.ksu.edu/documentation/patterns/ltl.shtml>.) Merci, Caroline Lemieux

2 1

Invitation to connect on LinkedIn
by Jianwen Li 30 Oct '13

30 Oct '13

LinkedIn ------------ I'd like to add you to my professional network on LinkedIn. - Jianwen Jianwen Li Student at 华东师范大学 Shanghai City, China Confirm that you know Jianwen Li: https://www.linkedin.com/e/-nsg3vs-hndxc2hn-6m/isd/17671877642/tb7AAFae/?hs… -- You are receiving Invitation to Connect emails. Click to unsubscribe: http://www.linkedin.com/e/-nsg3vs-hndxc2hn-6m/u-a3zDAksnebW94Ku3oUMPGzZndMu… (c) 2012 LinkedIn Corporation. 2029 Stierlin Ct, Mountain View, CA 94043, USA.

1 0

monitor construction error
by Angelo Gargantini 06 Mar '13

06 Mar '13

Dear spot maintainers, we have been using SPOT by using its web site to build monitors from LTL formulas (http://spot.lip6.fr/ltl2tgba.html) Now with the new version, translation to monitors gives always an error like: ome maps are not empty Variable Map: 0 Free 1 Var[a] x1 { 0xa001d10 } Anonymous lists: [0] Free list: (0, 1) close failed in file object destructor: sys.excepthook is missing lost sys.stderr Could you please fix it? Thanks Angelo Gargantini University of Bergamo Italy

2 2

check for the emptyness of the automata
by Jianwen Li 08 Dec '12

08 Dec '12

Dear Sir: I want to ask whether SPOT integrate some algorithm that can check the generated autoamta's emptyness ? Recently I want to use SPOT to do the LTL satisfiability checking. If you do not, I have to combine SPOT with SPIN to achieve that. Thanks very much! -- Best Regards Jianwen

2 1

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