- Spot - LRE

Spot_issue_timeout_0427
by cfyu 27 Apr '26

27 Apr '26

Dear Spot R&D and Maintenance Team, I am writing to report an issue with the web version of Spot. Earlier today, I noticed that the tool fails to parse and evaluate basic LTL formulas, a typical example being p U q. I think that this problem is not caused by timeouts or out-of-memory errors. Spot is a highly valuable and influential open-source project. Thank you sincerely for your long-term efforts and outstanding contributions to the research community. Chaofeng Yu Xidian University cfyu cfyu(a)stu.xidian.edu.cn

1 0

facing issue with spot
by Dewan Mohammed Abdul Ahad 26 Apr '26

26 Apr '26

Hi, I used it even yesterday. Is anything wrong happened? Is your website under maintenance ? I need this online tool. Requesting your guidance about how to use this online spot. Regards, Dewan.

1 0

LDBA Support
by Tim Quatmann 11 Jan '26

11 Jan '26

Dear Spot Team, thanks for this awesome library! We happily use this in Storm <https://stormchecker.org/>. I have a quick question: Does Spot offer any translation from LTL to LDBAs similar to the work by Sickert et al. (CAV'16) https://www7.in.tum.de/~sickert/publications/SickertEJK16.pdf ? I could not find any reference to that in the documentation. Thanks, Tim

2 1

spot bug, multiple initial states and empty transitions
by Beutner, Raven 07 Sep '25

07 Sep '25

Dear spot team, It seems like there is a bug in the current version of spot, that occurs under certain combinations of multiple initial states and states without any successors. In the example below, the automaton is clearly not empty, yet autfilt claims it is (tested with versions 2.14.1 and 2.12) $ cat foo.hoa HOA: v1 States: 3 Start: 1 Start: 2 AP: 0 acc-name: Buchi Acceptance: 1 Inf(0) --BODY-- State: 0 {0} [(t)] 0 State: 1 [(t)] 0 State: 2 --END-- $ autfilt --is-empty foo.hoa HOA: v1 States: 3 Start: 2 AP: 0 acc-name: Buchi Acceptance: 1 Inf(0) properties: trans-labels explicit-labels state-acc deterministic --BODY-- State: 0 {0} [t] 0 State: 1 State: 2 --END-- If I add some useless self-loop to state 2, or remove state 2 from the list of initial states, autfilt’s output is correct again. This seems very similar to a bug I reported a while ago (28.06.2024), not sure if this helps. FYI: the bug was found while using AutoHyper, leading to erroneous model-checking results. In AutoHyper, automata of the above form (multiple initial states and states without outgoing edges) occur quite frequently. Thanks, Raven

2 1

Re: Is Spot parallel safe?
by 龙方淞 13 Jun '25

13 Jun '25

Hello, I'm glad to see my question has already been asked and answered. I was wondering if there has been any consideration given to making this specific fork of BuDDy thread-safe, or it’s just because there would be too much work. Are there any plans to make this parallel in the future? If it's a matter of simply wrapping static variables into a "Context" argument, I might be able to assist (I assume breaking the C API of BuDDy would be acceptable, as it's not intended for direct user access). ----- To provide some context, for my master's thesis, I'm using Spot for ω-automata operations, specifically performing product and product-or operations on a large number of automata. While other parts of my program are multithreaded, I've found that the only way to parallelize the product and product-or operations is by starting multiple autfilt processes. I did attempt to achieve parallelism by importing Spot via FFI and do stuff in threads. However, after reviewing some of the code of Spot, I noticed the extensive use of static variables. Fangsong Long

2 1

Thank you for hosting a Jupyter sandbox
by Saaltink, C. (Caz, Student M-CS) 05 Jun '25

05 Jun '25

Hi, I just wanted to say thank you for hosting a Jupyter sandbox. It helped me out a lot!. Cheers, Caz

1 0

Occasional unavailability of Spot website
by Matthias Volk 06 May '25

06 May '25

Dear Spot developers, first, thanks for the great library. We use it in our probabilistic model checker Storm (https://www.stormchecker.org/) for LTL model checking. In our CI we have a daily job building the Storm tool which also downloads the latest Spot version. In the last couple of days, the download link https://www.lrde.epita.fr/dload/spot/spot-2.13.tar.gz was unavailable. See for example this CI job: https://github.com/moves-rwth/storm/actions/runs/14830395085/job/4163028321… I now checked and it seems the link is working again. So a big thanks for fixing the issue. We have seen the unavailability of the website occasionally throughout the last months. Is there something we can do in these instances? Should we notify you or are you already aware of it anyway? Or is there perhaps a mirror which we could try if the main website is down? Best regards, Matthias Volk

2 2

bug report for ltlsynt
by 叶昕 30 Jan '25

30 Jan '25

Dear LTLSYNT Team, I'm an associate researcher from Harbin Institute of Technology. When I was using LTLSYNT for experiments, I may find a bug. Consider a LTL formula G(a-> X b) and G(b-> X not b) where a is the input and b is the output. Obviously, it is unrealizable. As whenever the input event ’a’ holds in two consecutive steps, the system can not produce a value for the output event ’b’. However, when I try it in LTLSYNT, I got 'realizable'. I'm assuming it is a bug and report it to you. Best regards, Xin Ye

2 1

[BUG] Bug translate LTL formula into automata
by Vincenzo Tramo 24 Jan '25

24 Jan '25

Dear Spot developers, My name is Vincenzo, and I am a Master's student in Computer Science at the University of Naples, Italy. I am developing a tool using the Spot library, and I have encountered a bug that I would like to report. When attempting to translate an LTL formula into a Büchi automaton with the following inputs, the function does not terminate: INPUT 1 alive & sing & (alive U G!alive) & G(!alive | last | (sing <-> X(alive & !sing))) & F(alive & last & sing) & (p0 R (!alive | (p0 & !sing) | ((p1 R (!alive | p3 | (p1 & !sing))) & F(alive & p1 & p3)))) & (p4 U (alive & p5 & (p4 | sing))) & (Xp0 U (alive & (p3 R (!alive | (p3 & !sing) | (p4 U (alive & (p4 | sing) & (p2 | (p2 U (alive & (p2 | sing) & (p3 R (!alive | p10 | (p3 & !sing)))))))) | G(!alive | p4))) & (sing | Xp0))) INPUT 2 (((p9 R ((p13 xor Fp48) M (Fp15 -> p6))) M (p68 W (p68 | p74))) & (((p63 W p7) xor !(p51 xor FGp65)) U (((p97 -> p77) <-> GFp42) <-> G(((!p76 U p2) M G((p32 & Fp26) R p37)) R ((Fp73 U F(p53 U p99)) W (p25 & (Fp58 W !p47))))))) M (F(p96 | G(p99 U FGp18) | G((((p67 <-> p93) M F!(p3 -> (p87 & Fp65))) xor ((G(Gp69 W (p82 M G((p82 U (Fp1 -> (p58 M p34))) -> (F(p16 W p65) -> (p70 xor Fp80))))) M (p38 W (!p43 <-> p49))) -> (F(Fp9 W p31) W (p17 xor p65)))) W Fp10)) & ((!G(!Fp33 xor ((F(Fp80 M (!Gp61 M ((p64 | ((!p13 -> !p50) U p45)) W FGp51))) xor ((p63 U p45) -> F((p8 <-> (GF((G(p13 <-> (p17 & Gp6)) U (p18 R p82)) xor G(((p12 | p31) -> (p56 R p13)) & G(Fp92 <-> (p97 -> Fp16)))))))) -> (!(!(p4 | Fp93) R (p31 <-> (p71 | Gp32))) U F((!p33 xor p50) xor ((p61 R p47) & Fp57))))) W ((!(Fp69 M (p35 W p38)) -> ((Fp98 R (p63 xor F(p29 -> Fp17))) | (p49 M (Fp1 & (F(p10 & p65) M F(p67 W p33)))))) -> ((((!p39 & !p66 & p74) M p36) -> ((!p22 U F((p72 U p98) R Fp52)) & (p15 xor (Fp54 xor (Fp97 | Fp60))))) | (((F(p28 xor p96) U ((p73 W p92) -> (Fp80 M !p99))) R (p29 W !p11)) & G((p35 & ((Gp72 M (p63 xor !p64)) R ((p19 xor (GF!p22 M p44)) U (p1 R p54)))) | (G(p4 -> p44) -> !p25) | F(!FG((!(p77 -> ((p92 M p8) & (((p62 U (p36 M p18)) R Fp74) M F(p37 W p49)))) M (!p32 | (F((p34 <-> (p49 <-> FG(p27 M p21))) xor FGF(p95 xor (!p35 U Fp43))) M Fp49))) xor F(Fp44 xor (F(p99 M p94) W F((p36 xor p91) xor Gp37)))) M F((!p23 U (p13 <-> p38)) R (p53 R p68)))))))) -> (F((p1 | Gp46) W GF(((p93 xor (p77 -> p53)) | (!p25 <-> (((p56 -> p38) R (p75 W p28)) | (Fp58 M Fp6)))) M (p1 | Fp29))) -> Gp15))) The issue appears to be in the function |twa_graph_ptr translator::run_aux(formula r)| in the file |translate.cc|, specifically at line 428 when the following function is called (in postproc.hh): aut = this->postprocessor::run(aut, r); /// \brief Optimize an automaton. /// /// The returned automaton might be a new automaton, /// or an in-place modification of the \a input automaton. After this function is called, the automaton does not return, and the translation never terminates. I hope these details can help you diagnose the problem. If you need further information, please don't hesitate to ask. Thank you for your support! Best regards, Vincenzo

2 1

Re: Utilisation de spot comme librarie d'automates
by Alexandre Duret-Lutz 09 Dec '24

09 Dec '24

Laurent Bartholdi <laurent.bartholdi(a)gmail.com> writes: > Ah, OK, thanks. > Is there a good reason to do the log-encoding, or is it actually fine > to have a classical alphabet a,b,c, ... and encode each letter as (a > & !b & !c, !a & b & !c, !a & !b & c, ...)? It all depends on what operations you plan to do on those automata. Some operations are exponential in the number of atomic propositions, so it is often best to have fewer of those. If you only plan to two intersections and emptiness checks, a one-hot encoding (what you suggested) is probably fine. If you need to work with complete automata at some point (e.g., maybe for complementation), one-hot encoding will be hard to work with. You want the disjunction of the encodings of all letters in your alphabet to be equal to true, so that completing an automaton does not "invent" encodings that correspond to no letters.

1 0