- Spot - LRE

Question about the use of ltlcross
by 肖圣平 15 Dec '19

15 Dec '19

Dear Spot Fans, It is frustrating that I encountered some problems when using ltlcross. I have  implemented a tool to get BA from LTL formula. Then I want to use ltlcross to compare spot with my tools. When I ran the ltlcross, I got the following result：//failed to create lcr-o0-fdbDS4 Besides, I tried the following and still failed：//failed to create lcr-o0-kSl51L I sincerely hope you can help to see my question I would appreciate it if I could get some guidance on the use of ltlcross from you. Looking forward to your reply! Best Regards! Shengping Shaw, ECNU

1 0

Keep all APs when translating LTL?
by Dominick Pastore 21 Nov '19

21 Nov '19

Hello, We are using the Python bindings in Spot to translate LTL to monitors, as described at https://spot.lrde.epita.fr/tut11.html. We have a question: Is it possible to set an option that will preserve all the atomic propositions, even when they cannot affect the automaton? For example, with the formula "Ga & Fb", the resulting monitor would not include "b". Is there a way to do this? Thanks, Dominick

2 2

ltl2tgba: diagnostics for stutter-sensitive properties
by Victor Khomenko 21 Nov '19

21 Nov '19

Hi Alexandre, Suppose one calls ltl2tgba with the option --check=stutter-invariant. Would it be possible to print a warning with diagnostics, like the online tool does? Something like: Warning: The property is stutter-sensitive - the following words are a proof, as they differ only by some stuttering: Accepted word: a & b; a & b; cycle{!a & !b} Rejected word: a & b; cycle{!a & !b} Motivation: * by passing the option --check=stutter-invariant the user tells the tool that stutter-invariance is important for them, hence a warning/diagnostics is desirable if the check fails (this warning does not have to be printed if this option is not passed) * it's not easy to get these traces from the final automaton - my understanding is that some potentially costly operations are required, which are performed during the check anyway * the current way of getting this diagnostics (python + libraries; maybe there is a better way I don't know about?) creates many dependencies, thus making it difficult to integrate this functionality into toolchains - ideally one would want just a single executable ltl2tgba * my (perhaps naive) understanding is that this is not difficult to implement and does not incur much extra run-time as the check has to be performed anyway Best regards, Victor.

2 1

Re: [Spot] command-line option to negate input formula
by Victor Khomenko 24 Sep '19

24 Sep '19

> > Could you add a command-line option for ltl2tgba to invert the input > formula before computing the automaton? > > Done. > https://gitlab.lrde.epita.fr/spot/spot/commit/7f21d3ff29ad3a513f261025c5 > 75e4676a14cc50 Great - many thanks! > Any opinion on what passing --negate twice should do? A really good and nerdy one - twice the smiley face! :-) :-) Cheers, Victor.

1 0

command-line option to negate input formula
by Victor Khomenko 24 Sep '19

24 Sep '19

Hi, Could you add a command-line option for ltl2tgba to invert the input formula before computing the automaton? Yes, it's trivial to do externally, but there are good reasons to have this option: * this would remove an extra step from model checking toolchains (where the automaton is built for the negation of a formula) * if the formula goes through a toolchain, it's better to keep equivalence all the way through to the automata, so that the user can easily see that the property has not been broken by transformations, and also comprehend any formula-related diagnostics logged by the tools. Thanks, Victor.

2 1

LTLf formulas
by Yong Li (李勇) 10 Sep '19

10 Sep '19

Dear Spot developers, I am Yong Li from Chinese Academy of Sciences and I am writing to you to ask a question about parsing LTLf (LTL over finite traces) formulas. Spot supports LTL with finite semantics (LTLf) but I found out that Spot eagerly simplifies the input formulas with LTL semantics. For instance, if I use command line ltlfilt --from-ltlf -f "a U !(X True)", Spot immediately gives me 0. This is not correct since the input formula should be satisfiable in LTLf semantics. I wonder whether there is a way to get around it? Is there a an option I can use to make Spot parse the formula without simplying it? Regards, Yong

2 1

Issue with SPOT and LTLf
by Andrew Wells 28 Aug '19

28 Aug '19

I'm trying to use SPOT to build an automaton for an LTLf formula, but I think there is a bug. I'm using this code (based on https://spot.lrde.epita.fr/tut12.html) #include <iostream> #include <spot/tl/ltlf.hh> #include <spot/tl/parse.hh> #include <spot/twaalgos/hoa.hh> #include <spot/twaalgos/remprop.hh> #include <spot/twaalgos/translate.hh> int main() { spot::parsed_formula pf = spot::parse_infix_psl("((a && b) U (! (X 1)))"); if (pf.format_errors(std::cerr)) return 1; spot::translator trans; trans.set_type(spot::postprocessor::BA); trans.set_pref(spot::postprocessor::Small); spot::twa_graph_ptr aut = trans.run(spot::from_ltlf(pf.f)); spot::remove_ap rem; rem.add_ap("alive"); aut = rem.strip(aut); spot::postprocessor post; post.set_type(spot::postprocessor::BA); post.set_pref(spot::postprocessor::Small); // or ::Deterministic aut = post.run(aut); print_hoa(std::cout, aut) << '\n'; return 0; } In LTL, this would be a contradiction, but in LTLf it is not as the next operator cannot be true at the last timestep. There seems to be an issue with SPOT where it simplifies the automaton as though the formula is in LTL, yielding an incorrect automaton. Am I using this correctly? I'd be willing to write a patch if this is indeed a bug. Thanks, Andrew Wells

2 1

Change log from version 2.0 to 2.8
by M. H. Zibaeenejad 24 Aug '19

24 Aug '19

Hi, I have used the version 2.0 of your online tool for LTL to Buchi automata translation. At the time the tool did not return a deterministic Buchi automaton, but the new version does the transformation with ease. I was wondering if something fundamental has changed in your code that made this possible. Do you have the Changelog from 2.0 to 2.8? Here is the formula i used : G(!e) & G((c&!d&Fd)->(p Ud)) & G(a&!c->(!c W(b&!c))) & GF(a)&GF(b)&GF(c)&GF(d) RegardsHadi Zibaeenejad,PhDUniversity of Waterloo

2 1

Compiling Spot on windows
by Maxime Bouton 04 Jul '19

04 Jul '19

Dear Spot maintainers, I was wondering if there had been some work on compiling Spot with the python bindings on windows? I have been able to create windows binaries for libspot.so using a cross-compilation environment and mingw with the option `--disable-python`, and I saw that there was a similar example in the continuous integration configuration on gitlab. However I would be interested in having the python bindings as well. * Do you think it is possible for one to get the python bindings for windows? * Do you have any hints on how one could proceed? In the cross-compilation environment I had an error in the `./configure` step, related to not being able to find `python.h` on the target (windows 64bits) and was not able to make much progress in that direction. Thanks for your help, Maxime

2 2

Theorem question
by Scott M. Staley 30 Jun '19

30 Jun '19

Hi all, A quick (?) question. When I put the following LTL formula into SPOT online: G (G (p => Gp ) => Gp) => (FG p => Gp) SPOT says it is equivalent to 1. Therefore I assume it’s a theorem of LTL. My question: Is there anyway to see the series of rewrites of the formula to show how it gets form the original formula to “true”? Thanks, Scott

2 1