- Spot - LRE

Spot 0.9 is released
by Alexandre Duret-Lutz 09 May '12

09 May '12

We are pleased to announce the release of Spot 0.9. Spot is a model-checking library developed collaboratively by LRDE and LIP6. It provides algorithms and data structures to implement the automata-theoretic approach to LTL model checking. You can find the new release here: http://spot.lip6.fr/dl/spot-0.9.tar.gz (11MB) The major news in this release are all related to the logic-to-Büchi-automaton translation engine: 1. The linear-time fragment of PSL is supported. This first implementation, enough to experiment with the logic, shall be improved in future versions. (Feedback most welcome.) 2. The LTL simplification code has been overhauled and augmented with new rules. 3. A new simulation-based post-processing can be used to simplify the TGBA constructed. For more details about the first two points (supported operators, and rewritings performed), please read the file doc/tl/tl.pdf included in spot-0.9.tar.gz. A consequence of the last two points is that Spot 0.9 is faster than Spot 0.8.3 and can produce even smaller automata. For some comparative benchmarks, please download http://spot.lip6.fr/dl/bench-0.9.pdf Please direct any feedback and questions to <spot(a)lrde.epita.fr>. (Subscribe at https://www.lrde.epita.fr/mailman/listinfo/spot if you wish.) A more detailed list of new features follows. New in spot 0.9 (2012-05-09): * New features: - Operators from the linear fragment of PSL are supported. This basically extends LTL with Sequential Extended Regulat Expressions (SERE), and a couple of operators to bridge SERE and LTL. See doc/tl/tl.pdf for the list of operators and their semantics. - Formula rewritings have been completely revamped, and augmented with rules for PSL operators (and some new LTL rules as well). See doc/tl/tl.pdf for the list of the rewritings implemented. - Some of these rewritings that may produce larger formulas (for instance to rewrite "{a;b;c}" into "a & X(b & Xc)") may be explicitely disabled with a new option. - The src/ltltest/randltl tool can now generate random SEREs and random PSL formulae. - Only one translator (ltl2tgba_fm) has been augmented to translate the new SERE and PSL operators. The internal translation from SERE to DFA is likely to be rewriten in a future version. - A new function, length_boolone(), computes the size of an LTL/PSL formula while considering that any Boolean term has length 1. - The LTL/PSL parser recognizes some UTF-8 characters (like ◇ or ∧) as operators, and some output routines now have an UTF-8 output mode. Tools like randltl and ltl2tgba have gained an -8 option to enable such output. See doc/tl/tl.pdf for the list of recognized codepoints. - A new direct simulation reduction has been implemented. It works directly on TGBAs. It is in src/tgbaalgos/simlation.hh, and it can be tested via ltl2tgba's -RDS option. - unabbreviate_wm() is a function that rewrites the W and M operators of LTL formulae using R and U. This is called whenever we output a formula in Spin syntax. By combining this with the aforementioned PSL rewriting rules, many PSL formulae that use simple SERE can be converted into LTL formulae that can be feed to tools that only understand U and R. The web interface will let you do this. - changes to the on-line translator: + SVG output is available + can display some properties of a formula + new options for direct simulation, larger rewritings, and utf-8 output - configure --without-included-lbtt will prevent LBTT from being configured and built. This helps on systems (such as MinGW) where LBTT cannot be built. The test-suite will skip any LBTT-based test if LBTT is missing. * Interface changes: - Operators ->, <->, U, W, R, and M are now parsed as right-associative to better match the PSL standard. - The constructors for temporal formulae will perform some trivial simplifications based on associativity, commutativity, idempotence, and neutral elements. See doc/tl/tl.pdf for the list of such simplifications. - Formula instances now have many methods to inspect their properties (membership to syntactic classes, absence of X operator, etc...) in constant time. - LTL/PSL formulae are now handled everywhere as 'const formula*' and not just 'formula*'. This reflects the true nature of these (immutable) formula objects, and cleanups a lot of code. Unfortunately, it is a backward incompatible change: you may have to add 'const' to a couple of lines in your code, and change 'ltl::const_vistitor' into 'ltl::visitor' if you have written a custom visitor. - The new entry point for LTL/PSL simplifications is the function ltl_simplifier::simplify() declared in src/ltlvisit/simplify.hh. The ltl_simplifier class implements a cache. Functions such as reduce() or reduce_tau03() are deprecated. - The old game-theory-based implementations for direct and delayed simulation reductions have been removed. The old direct simulation would only work on degeneralized automata, and yet produce results inferior to the new direct simulation introduced in this release. The implementation of delayed simulation was unreliable. The function reduc_tgba_sim() has been kept for compatibility (it calls the new direct simulation whatever the type of simulation requested) and marked as deprecated. ltl2tgba's options -Rd, -RD are gone. Options -R1t, -R1s, -R2s, and -R2t are deprecated and all made equivalent to -RDS. - The tgba_explicit hierarchy has been reorganized in order to make room for sba_explicit classes that share most of the code. The main consequence is that the tgba_explicit type no longuer exists. However the tgba_explicit_number, tgba_explicit_formula, and tgba_explicit_string still do.

1 0

some questions about spot
by Jianwen Li 18 Apr '12

18 Apr '12

Dear Sir (Madam): Recently I am following your spot tool and try to use it to practice some of my ideas on ltl-to-Buchi translation. After reading the manuals I appreciate if you can answer me these questions: 1. Can I use your ltl parser source codes directly to implement my ideas? 2. Does SPOT integrate some ltl generators? Or, Are there any test suits available for me? 3. Does SPOT provide any interface which can generate the Buchi automata from a list of formulas and output them with any format (e.g prolmea or xml ) back to a file? I appreciate this function very much since I do want to compare my results with those from SPOT. ^^ 4. If I have some new idea to implement a new translation, is it possible for me to integrate it to SPOT? (I ask this since I thought SPOT is open :) ) Thank you very much and hope your reply! Best Jianwen Li

2 1

some questions about spot
by Jianwen Li 17 Mar '12

17 Mar '12

Dear Sir(Madam): When I use the SPOT tool online recently I found the truth that the result Buchi automata for such formulas G(F a && F b) from your tool is not a traditional one. Can you explain why? Thank you very much! Best Jianwen Li

2 1

performance of tgba_safra_complementation
by Nikos Gorogiannis 17 Jan '12

17 Jan '12

Hi Alexandre, I have some code that uses the standard pattern for checking language inclusion between two automata, using tgba_safra_complementation. The automata have a small number of states (<100) and one acceptance condition. Running my code under valgrind for time profiling reveals a curious time distribution: 30% of the execution time is spent in malloc and free (20%/10% resp). The call hierarchy is as follows: malloc/free <- operator new/delete <- tgba_tba_proxy::succ_iter <- tgba_sba_proxy ctor <- safra_determinisation::create_safra_automaton <- tgba_safra_complement I have eliminated the contribution of my code to the run time of malloc and free (basically by avoiding creating and destroying the same states repeatedly through memoizing). Is there any workaround to this, i.e., could better/different memory management eliminate this 30% of overhead? Are other complementation algorithms better for this use-case? Best regards Nikos PS What is the preferred way of referencing Spot in a publication?

2 1

spot-beginner questions
by Nikos Gorogiannis 17 Nov '11

17 Nov '11

Hi, I'm trying to learn spot, and I want to run an emptiness check on a product of two automata which I will be creating by subclassing tgba. The two automata have overlapping, but different, signatures i.e. atomic propositions. If I understand correctly, I cannot achieve this by using two different bdd_dicts, as the two automata passed to the product object must share the same bdd_dict. How does one deal with this problem in spot? Thanks Nikos

2 13

self-modifying automaton
by Nikos Gorogiannis 07 Oct '11

07 Oct '11

Hi, I've been looking for a library that would allow me to provide a (lazy) interface for enumerating the states of an automaton and doing on-the-fly model checking. Spot looks like exactly what I need! (which is great; I couldn't find any other tool supporting custom model checking like this). What I will need on top of this, is when the emptiness check fails, I'd like to modify the automaton using the information provided by the check and re-run the check. Changes to the automaton will be localized, so destroying and rebuilding the objects relating to the emptiness check seems unnecessarily expensive. Is there any way around this? Best regards Nikos Gorogiannis

2 2

Nondeterministic behavior of ltl2tgba tool
by Tomáš Babiak 17 Aug '11

17 Aug '11

Dear SPOT developers, I am doing a research on translation of LTL to BA and I am using the tool "ltl2tgba" included in the SPOT 0.7.1 distribution as a reference. While comparing "ltl2tgba" to some other translations using the "lbtt" tool, I have noticed that it sometimes produces different results (regarding the size of produced automata) without changing any parameters. It appers that for some formulae it nondeterministicaly produces different automata. I attach an example when "ltl2tgba" was executed four times in the row always producing a different automaton. First three automata differs only by the names of states or the ordering of transitions, while the last automaton has one state less than the others. However, all automata seam to be correct and mutually equivalent. After a closer examination, it seams that this behavior is caused be the -r7 option enabling tau03 formula reductions. Similar behavior can be observed using -r5 or -r6 options as well. The question is whether such a nondeterminstic behavior is expected while using language containment formula reductions or it is caused by an implementation bug. Thank you for your help. Best regards, Tomas Babiak

2 1

make check failed
by Johan Oudinet 07 Dec '10

07 Dec '10

Hi, I've trouble to install Spot-0.6. make check produces an error when compiling evtgba/symbol.hh. g++ (4.4.3) complains about a dereferencing pointer call that breaks strict-aliasing rules. Can I still install the package safely? ============================= g++ -DPACKAGE_NAME=\"spot\" -DPACKAGE_TARNAME=\"spot\" -DPACKAGE_VERSION=\"0.6\" -DPACKAGE_STRING=\"spot\ 0.6\" -DPACKAGE_BUGREPORT=\"spot(a)lrde.epita.fr\" -DPACKAGE_URL=\"\" -DPACKAGE=\"spot\" -DVERSION=\"0.6\" -DSTDC_HEADERS=1 -DHAVE_SYS_TYPES_H=1 -DHAVE_SYS_STAT_H=1 -DHAVE_STDLIB_H=1 -DHAVE_STRING_H=1 -DHAVE_MEMORY_H=1 -DHAVE_STRINGS_H=1 -DHAVE_INTTYPES_H=1 -DHAVE_STDINT_H=1 -DHAVE_UNISTD_H=1 -DHAVE_SRAND48=1 -DHAVE_DRAND48=1 -DHAVE_DLFCN_H=1 -DLT_OBJDIR=\".libs/\" -I./.. -I../../buddy/src -DNDEBUG -W -Wall -Wcast-align -Wpointer-arith -Wwrite-strings -Wcast-qual -DXTSTRINGDEFINES -Werror -g -O3 -ffast-math -fstrict-aliasing -fomit-frame-pointer -MT explicit.o -MD -MP -MF .deps/explicit.Tpo -c -o explicit.o explicit.cc cc1plus: warnings being treated as errors ./../evtgba/symbol.hh: In function ‘int main()’: ./../evtgba/symbol.hh:114: error: dereferencing pointer ‘__x.170’ does break strict-aliasing rules /usr/include/c++/4.4/bits/stl_tree.h:525: note: initialized from here ./../evtgba/symbol.hh:114: error: dereferencing pointer ‘__x.170’ does break strict-aliasing rules /usr/include/c++/4.4/bits/stl_tree.h:525: note: initialized from here make[3]: *** [explicit.o] Erreur 1 make[3]: quittant le répertoire « /users/fortesse/oudinet/projects/spot-0.6/src/evtgbatest » make[2]: *** [check-am] Erreur 2 make[2]: quittant le répertoire « /users/fortesse/oudinet/projects/spot-0.6/src/evtgbatest » make[1]: *** [check-recursive] Erreur 1 make[1]: quittant le répertoire « /users/fortesse/oudinet/projects/spot-0.6/src » make: *** [check-recursive] Erreur 1 ============================ Regards, -- Johan () ascii ribbon campaign - against html e-mail /\ www.asciiribbon.org - against proprietary attachments

2 1

Problème de compilation de SPOT
by Silien Hong 07 Oct '10

07 Oct '10

Bonjour, Je suis HONG Silien, je travail avec Yann Thierry-Mieg pour intégrer SPOT dans notre serveur d'intégration continu. Yann m'a dit qu'il y avait une branche "stable" qui me permettait d'éviter les erreurs de compilation avec les Warnings. Malheuresement ca ne compile toujours pas, voici l'erreur : /bin/sh ../../libtool --tag=CXX --mode=compile g++-4.2 -DPACKAGE_NAME=\"spot\" -DPACKAGE_TARNAME=\"spot\" -DPACKAGE_VERSION=\"0.6\" -DPACKAGE_STRING=\"spot\ 0.6\" -DPACKAGE_BUGREPORT=\"spot(a)lrde.epita.fr\" -DPACKAGE_URL=\"\" -DPACKAGE=\"spot\" -DVERSION=\"0.6\" -DYYTEXT_POINTER=1 -DSTDC_HEADERS=1 -DHAVE_SYS_TYPES_H=1 -DHAVE_SYS_STAT_H=1 -DHAVE_STDLIB_H=1 -DHAVE_STRING_H=1 -DHAVE_MEMORY_H=1 -DHAVE_STRINGS_H=1 -DHAVE_INTTYPES_H=1 -DHAVE_STDINT_H=1 -DHAVE_UNISTD_H=1 -DHAVE_SRAND48=1 -DHAVE_DRAND48=1 -DHAVE_DLFCN_H=1 -DLT_OBJDIR=\".libs/\" -I./.. -I../../buddy/src -I/Users/hong/usr/include -DNDEBUG -W -Wall -Wcast-align -Wpointer-arith -Wwrite-strings -Wcast-qual -DXTSTRINGDEFINES -Werror -g -O3 -ffast-math -fstrict-aliasing -fomit-frame-pointer -MT tgbasafracomplement.lo -MD -MP -MF .deps/tgbasafracomplement.Tpo -c -o tgbasafracomplement.lo tgbasafracomplement.cc libtool: compile: g++-4.2 -DPACKAGE_NAME=\"spot\" -DPACKAGE_TARNAME=\"spot\" -DPACKAGE_VERSION=\"0.6\" "-DPACKAGE_STRING=\"spot 0.6\"" -DPACKAGE_BUGREPORT=\"spot(a)lrde.epita.fr\" -DPACKAGE_URL=\"\" -DPACKAGE=\"spot\" -DVERSION=\"0.6\" -DYYTEXT_POINTER=1 -DSTDC_HEADERS=1 -DHAVE_SYS_TYPES_H=1 -DHAVE_SYS_STAT_H=1 -DHAVE_STDLIB_H=1 -DHAVE_STRING_H=1 -DHAVE_MEMORY_H=1 -DHAVE_STRINGS_H=1 -DHAVE_INTTYPES_H=1 -DHAVE_STDINT_H=1 -DHAVE_UNISTD_H=1 -DHAVE_SRAND48=1 -DHAVE_DRAND48=1 -DHAVE_DLFCN_H=1 -DLT_OBJDIR=\".libs/\" -I./.. -I../../buddy/src -I/Users/hong/usr/include -DNDEBUG -W -Wall -Wcast-align -Wpointer-arith -Wwrite-strings -Wcast-qual -DXTSTRINGDEFINES -Werror -g -O3 -ffast-math -fstrict-aliasing -fomit-frame-pointer -MT tgbasafracomplement.lo -MD -MP -MF .deps/tgbasafracomplement.Tpo -c tgbasafracomplement.cc -fno-common -DPIC -o .libs/tgbasafracomplement.o cc1plus: warnings being treated as errors tgbasafracomplement.cc:57: warning: ‘spot::safra_tree_automaton’ has a field ‘spot::safra_tree_automaton::automaton’ whose type uses the anonymous namespace tgbasafracomplement.cc:57: warning: ‘spot::safra_tree_automaton’ has a field ‘spot::safra_tree_automaton::initial_state’ whose type uses the anonymous namespace Je connais pas très bien GIT, et j'espère avoir compilé la bonne branche, voici la commande que j'ai tapé pour récupérer le source : git clone --branch stable git://git.lrde.epita.fr/spot Un petit coup de pouce est la bienvenue ... Merci d'avance. Cordialement,

2 1

Re: [Spot] Parameters for the "ltl2tgba" tool
by Alexandre Duret-Lutz 01 Mar '10

01 Mar '10

Hi Ruediger, >>> "e" == ehlers <ehlers(a)alan.cs.uni-sb.de> writes: e> Dear all, e> included in the SPOT distribution is the tool "ltl2tgba" that converts LTL e> formulas to equivalent Büchi automata. For the research I am currently e> working on, I need to convert LTL formulas to as-small-as-possible Büchi e> automata (that are not transition-based, so I am using the tool with the e> "-N" parameter to obtain SPIN never-claims). So far, for all my e> benchmarks, I am calling the tool with the following parameter e> combinations: e> ltl2tgba -N -R3 -r4 e> ltl2tgba -N -R3 -r7 e> ltl2tgba -N -R3 -r4 e> ltl2tgba -N -R3 -r7 e> ltl2tgba -N -R3 -r4 e> ltl2tgba -N -R3 -r7 I presume you forgot to edit some of these lines? From the rest of your mail, you might be using -R2q and -R2t also. Have you seen cases where -r4 produces a smaller automaton than -r7 ? I would think that given that -r7 includes -r4 it should always be better. Of course these options only try to reduce the LTL formulae, not the resulting automata. However if you see cases where -r7 reduces the formula in a way that the translated automaton is bigger than one obtained after -r4, I would be interested to study them. e> After that, I take the smallest automata obtained. So far, I am only e> interested in the number of states. e> Now my question is: Given that I have enough time, which other parameter e> combinations might lead to automata that that are smaller than any e> automaton obtained when using the parameter combinations given above? As e> an example, can it be the case that "-R2q" is sometimes better than "-R3"? These switches are not exclusive. I would always use -R3, because removing dead states and useless acceptance conditions (-R3 does that) will improve the efficiency of other algorithms such as delayed simulations. You could try the following combinations ltl2tgba -f -N -R3 -R1q -R1t -r7 ltl2tgba -f -N -R3 -R2q -R2t -r7 ltl2tgba -f -N -R3 -R1q -R1t -R2q -R2t -r7 But I think the latter should always return the smaller automaton (when it is correct...). Unfortunately these -R1* and -R2* options are not always correct (this is the reason they are not available on the on-line translator script). They were implemented by a student during his master's thesis, but he struggled to adapt Etessami's paper to transition-based automata. I know of an easy case where the -R2* simplification is clearly wrong: ./ltl2tgba -f -R3 -R2t 'FG a' Apparently the structure of the automata generated by the "-f" translation is such that -R2* can be wrong only when it is mixed with -R3. But the bug really is in -R2*. I'm a bit more confident about -R1* for which I'm not aware of any problem (except that it does not work for generalized automata, but that should not be an issue for you). Still, personally I would only use -R3. Rewriting -R1* and -R2* has been on the TODO list for a while. I have seen some work, by Juvekar and Piterman, that generalizes the technique to generalized Büchi automata: it would probably be a better fit for Spot. So to summarize, I think you should be safe with ltl2tgba -f -N -R3 -R1q -R1t -r7 and I suggest you use -R2* only if you can check that the resulting automaton is correct. Although I think "-f" will create less states than the other translations, you can also try to replace it by one of -f -f -x -f -x -p -f -L -f -L -x -f -L -x -p -l -taa -c (If you encounter a case where -l or -taa is better than -f, please let me know!) -- Alexandre Duret-Lutz

1 0