- Spot - LRE

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

Utilisation de spot comme librarie d'automates
by Laurent Bartholdi 07 Dec '24

07 Dec '24

Bonjour, J'aimerais utiliser spot pour manipuler des automates de Buchi, parité,... en librairie (pour l'intégrer en fait à du code déjà existant). Il semble que c'est possible, mais mes automates devraient avoir un alphabet de la forme {0,...,n} ou {1,...,n}, et pas un BDD. Comment puis-je faire ? Ou, plus généralement, comment avoir accès à une documentation complète qui ne passe pas par doxygen? Merci beaucoup d'avance, Laurent

2 1

Is Spot parallel safe?
by Vlada Krsmanovic 07 Dec '24

07 Dec '24

Hello, Is it safe to use Spot with parallelism and python multiprocessing/multhreading? Thanks for the answer, Best regards, Vladimir Krsmanovic

2 1

Unmet Python Dependency Error
by david.arruga＠gmail.com 22 Nov '24

22 Nov '24

Hello everybody, While I noticed a similar post discussing a Python-related installation issue with Spot, I believe my case is distinct as the context and the errors I am facing differ significantly. In my case, I am attempting to install Spot on a clean virtual machine running Ubuntu 24.04. . I am encountering an unmet dependency issue when running the following command: " sudo apt-get install spot libspot-dev spot-doc python3-spot" The terminal output shows: " The following packages have unmet dependencies: python3-spot : Depends: python3 (< 3.12) but 3.12.3-0ubuntu2 is to be installed E: Unable to correct problems, you have held broken packages. " I have already tried the following steps: - Installing Python 3.10 manually and setting it as the default version using update-alternatives. - Adding the Spot Debian repository key and verifying it was added correctly. - Updating the package lists with sudo apt-get update. Despite these steps, the error persists, so I’m not sure if this is an issue with my system configuration, the Spot repository, or outdated requirements. Any insights or suggestions would be greatly appreciated. Thank you!

2 2

Python compatibility
by Vlada Krsmanovic 18 Nov '24

18 Nov '24

Hello, I have recently been attempting to get Spot to work on an ML cluster running 24.02 CUDA/PyTorch images (which have Python 3.10 installed). Following the installation instructions and trying to install spot using the Debian install approach causes installation error stating that python 3.11 is required The following packages have unmet dependencies: *libspotltsmin0 : Depends: libltdl7 (>= 2.4.7) but 2.4.6-15build2 is to be installedpython3-spot : Depends: python3 (>= 3.11~) but 3.10.6-1~22.04 is to be installedUnable to correct problems, you have held broken packages.* The website states that only python 3.6+ is required? Is the website requirement outdated, the debian installation too restrictive on the python version or am I doing something wrong? Thanks a bunch for your help, Best regards, Vladimir Krmsanovic

2 2

What happened to merge_states?
by Michaël Cadilhac 07 Oct '24

07 Oct '24

Howdy spotters, *Once upon a time, *right before a rewrite of ltlsynt at: https://gitlab.lre.epita.fr/spot/spot/-/blob/7d908b93207b983a4ced81dd2240a5… … ltlsynt was still aggressively calling "merge_states", see e.g., https://gitlab.lre.epita.fr/spot/spot/-/blob/25c75c55b1e1fe7d3a502e1658839f… Being the sheep that I am, I vaguely copied at that time this behavior without really understanding it: https://github.com/gaperez64/acacia-bonsai/blob/22cff19e55b3de4bf7b348ae770… (The goal therein is simply to remove some states, then execute some simplification of the automaton.) *But then, the fire nation attacked. *For some reason, with the most recent Spot master, I get a lot of crashes in merge_states, on that line specifically: https://gitlab.lre.epita.fr/spot/spot/-/blob/master/spot/twa/twagraph.cc?re… This is probably rooted in my incorrect use of that method, its companion simplification functions, and state deletion. *So, questions:* - Why did ltlsynt stop using merge_states/merge_edges? - What is it I'm doing wrong in my use case? Thank you! Michaël

2 1

Regarding Spot2.9 installation
by Harsh Bihany 19 Aug '24

19 Aug '24

Greetings, I was trying to install Spot2.9, and was `make`ing it. It however throws the following error: ` BIBINPUTS='./..' latexmk -pdf -ps- -dvi- -pvc- -e '$bibtex_use=2' -e '$pdflatex="pdflatex %O \"\\def\\SpotVersion{2.9}\\input{%S}\""' ./tl.tex Rc files read: NONE Latexmk: This is Latexmk, John Collins, 20 November 2021, version: 4.76. Latexmk: applying rule 'pdflatex'... Rule 'pdflatex': File changes, etc: Changed files, or newly in use since previous run(s): './tl.tex' ------------ Run number 1 of rule 'pdflatex' ------------ ------------ Running 'pdflatex -recorder "\def\SpotVersion{2.9}\input{"./tl.tex"}"' ------------ sh: 1: pdflatex: not found Latexmk: fls file doesn't appear to have been made. Latexmk: Errors, so I did not complete making targets Collected error summary (may duplicate other messages): pdflatex: Command for 'pdflatex' gave return code 127 Refer to 'tl.log' for details ---------------------- This message may duplicate earlier message. Latexmk: Failure in processing file './tl.tex': *LaTeX didn't generate the expected log file 'tl.log' ---------------------- Latexmk: Use the -f option to force complete processing, unless error was exceeding maximum runs, or warnings treated as errors. ….. ` The requirements do not mention a local TeX installation. Is there a way to bypass this? Thanks. Best, Harsh

2 1

Simplification of property formula in LTL/CTL
by Arianna Bianchi 04 Apr '24

04 Apr '24

Hello, I am a student in Computer Science at the Technical University of Denmark (DTU), currently working on my master's thesis and I am using the random generator for LTL formulas of Spot. Upon exploring the GitHub repository of the project, I noticed the presence of simplification functions for generating the random LTL formulas. For instance, with these functions, equivalences are simplified and non-reducible formulas are generated. Could you provide insight into how this simplification functionality operates? And which specific function is responsible for this process? Furthermore, I noticed that the files responsible for generating the formulas are located in "spot/gen/formulas.cc" and "spot/gen/formulas.hh". How can I execute the formulas.cc file using a terminal (command line) to generate the random LTL formulas? Thank you for your assistance. Best regards, Arianna

2 1

Accessing Condition Formulas
by John Komp 14 Feb '24

14 Feb '24

Hi, With the Python API, is it possible to directly access the condition formulas on the automata edges? Statements like "aut.show_storage("v”)” will display them in a table. Yet if I cycle through my edges (for ed in aut.out(s):) and look at ed.cond I see it’s a buddy BDD. I can’t go any further than that. Looking at the Buddy SWIG file included with Spot shows many functions that appear to be able to view or manipulate the bdd but most of them appear to not be populated for Python - much like the state exposure noted in the example Python Jupyter notebooks. I wrote a really crude lex/yacc routine to parse the dot file and get the formulas but that seems a bit of ugly work duplication. Any help or advice would be appreciated. Thank-you for your time, John Komp Department of Computer Science University of Colorado, Boulder

2 1

Issue with Spot Package in Python - Need Assistance
by andreas luo 16 Jan '24

16 Jan '24

Dear Spot Developer, My name is Jun, and I am reaching out to you regarding an issue I've encountered while working with the Spot package. I have successfully installed the Spot package on two different computers with Linux systems of different versions. The Spot package functions perfectly in Terminator, allowing me to execute all official website shell codes. However, I am encountering an issue in Python. While I can import the Spot package without errors, attempting to run any functions like spot.formula or spot.translate results in “AttributeError: module 'spot' has no attribute 'formula'”. I have tried simply copying and pasting any example codes from the official website, but the problem persists. Could you tell me how to solve this problem? If you need any further information, please don’t hesitate to ask. Many thanks in advance. Best regards, Jun Luo The original codes from the example on official website and the output: import sys sys.path.append('/u/halle/luju/home_at/spot') import spot print(spot.formula('[]<>p0 || <>[]p1')) f = spot.formula('& & G p0 p1 p2') print(f.to_str('latex')) print(f.to_str('lbt')) print(f.to_str('spin', parenth=True)) custom_print(spot.automaton("tut21.hoa")) *Output:* /u/halle/luju/home_at/Desktop/a.py Traceback (most recent call last): File "/u/halle/luju/home_at/Desktop/a.py", line 7, in <module> print(spot.formula('[]<>p0 || <>[]p1')) AttributeError: module 'spot' has no attribute 'formula' Process finished with exit code 1 Just input spot: import sys sys.path.append('/u/halle/luju/home_at/spot') import spot *Output:* /u/halle/luju/home_at/Desktop/a.py Process finished with exit code 0

2 1

Issue in translation from LTLf
by Marco Faella 29 Dec '23

29 Dec '23

Dear all, there seems to be a problem with the translation LTLf -> LTL, as supported by the "ltlfilt --from-ltlf" command from the SPOT distribution. It seems that subformulas of the type "X p" get translated into "X (!alive | p)" instead of "X (alive & p)", as they should be according to the LTLf semantics, as well as the translation outlined in the Memocode '14 paper by Dutta and Vardi. Do you agree or am I missing something? By the way, we are planning to use SPOT as part of a toolchain to check the satisfiability of a flavor of LTLf-modulo-theory. Thanks, Marco Faella -- Associate professor Electrical Engineering and Information Technologies University of Naples Federico II, Italy http://wpage.unina.it/m.faella

2 1

Checking Safety and Liveness
by Samuel Judson 15 Dec '23

15 Dec '23

Hello, Using the Spot C++ API I am having a strange issue testing whether a formula is safety or liveness. Specifically, many of the formulas I am testing are coming back as both safety and liveness, despite being non-trivial. My code snippet for the testing is (with some extraneous steps omitted): >>> int simplification_level = 3; spot::tl_simplifier_options tlopt(simplification_level); spot::tl_simplifier simpl(tlopt); spot::parsed_formula pf = spot::parse_infix_psl(ltl); spot::formula f = simpl.simplify(pf.f); spot::twa_graph_ptr aut = ltl_to_tgba_fm(f, simpl.get_dict(), true); safe = f.is_syntactic_safety() || is_safety_automaton(aut); live = is_liveness_automaton(aut); <<< Here `safe` and `live` are both booleans. It is based on similar code within `/bin/ltlfilt.cc <http://ltlfilt.cc/>` in the Spot codebase. However, for many formulas this code resolves both `safe` and `live` to true. As a concrete example, when I test ``` G((!"(P_0 == 'p1')" & !"(P_0 == 'p2')" & !"(P_0 == 'p3')") | F"(P_0 == 'CS')") ``` (after simplification, and derived from the BEEM benchmarks) both resolve to true. Am I using the testing API incorrectly? Is this a bug in Spot? Or is the formula malformed in some way that isn’t obvious to me? Thanks in advance for any help you can give. Samuel Judson

2 2

installation sur Macos M2.
by Mamoun FILALI-AMINE 24 Oct '23

24 Oct '23

Bonjour, J'ai installé spot sur macos(M2). Pour les logiciels cela a l'air de marcher. Par contre quand j'ai voulu uitiliser les bindings Python, j'ai eu des problèmes qui semblent dûs à l'architecture ARM. Voici mon test Python et le résulat: ----- import sys import os sys.path.insert(0, '/usr/local/lib/python3.10/site-packages') # homonymie avec un autre spot. import spot f = spot.formula("FGa -> (GFb & GF(c & b & d & e))") ----- résultat ------- dali:~ filali$ cd /Users/filali ; /usr/bin/env /opt/homebrew/bin/python3 /Users/filali/.vscode/extensions/ms-python.python-2023.19.12901009/pythonFiles/lib/python/debugpy/adapter/../../debugpy/launcher 57565 -- /Users/filali/test_spot.py Traceback (most recent call last): File "/Users/filali/test_spot.py", line 4, in <module> import spot File "/usr/local/lib/python3.10/site-packages/spot/__init__.py", line 49, in <module> from spot.impl import * File "/usr/local/lib/python3.10/site-packages/spot/impl.py", line 10, in <module> from . import _impl ImportError: dlopen(/usr/local/lib/python3.10/site-packages/spot/_impl.cpython-310-darwin.so, 0x0002): tried: '/usr/local/lib/python3.10/site-packages/spot/_impl.cpython-310-darwin.so' (mach-o file, but is an incompatible architecture (have 'x86_64', need 'arm64')), '/System/Volumes/Preboot/Cryptexes/OS/usr/local/lib/python3.10/site-packages/spot/_impl.cpython-310-darwin.so' (no such file), '/usr/local/lib/python3.10/site-packages/spot/_impl.cpython-310-darwin.so' (mach-o file, but is an incompatible architecture (have 'x86_64', need 'arm64')) ------ Merci pour votre aide. Mamoun Filali PS (je pense avoir installé la version de dev.)

2 1

Support for tgba_powerset() in Python
by Marek Jankola 08 Sep '23

08 Sep '23

Dear Spot development team, I am currently working on a python project that uses Spot to process omega-automata. We want to use tgba_powerset() and obtain a map from states of the original automaton to the sets representing states of the deterministic automaton. There is a struct power_map, which one can obtain when passing it as an argument to tgba_powerset(). However, it returns SwigPyObject (obtained form C++ method) that is not iterable and we cannot convert the object to Python dictionary/list/set. One can use power_map.states_of(const int), however it is also not iterable. Is there a workaround for this problem? Could you add support for this in python or make power_map.states_of(const int) iterable? This fix would be a big help to our project from which we want to publish a paper soon. Thank you very much for the possible collaboration. Best regards, Marek Jankola

2 1

Re: Spot tool - installation error
by Alexandre Duret-Lutz 29 Aug '23

29 Aug '23

Ioana Huștiu <ioana.hustiu(a)academic.tuiasi.ro> writes: > Well, I am trying to install the 2.11.6 version (the latest that is > available on the website). > My computer has Windows, but I tried to install it on a virtual > machine with Debian 11. I have attached all the commands and their > outputs below. I see that "make check" failed only the randltl.ipynb test, but given than (1) all other Python tests passed, and (2) what the error looks like, I believe that tests/python/randltl.ipynb has been modified compared to was was in the tarball. Probably you tried to open it, execute the first cell, and that created an error message that was saved into the file. > A minor curiosity of mine: can the tool be used by using Visual > Studio Code and python after installation? No idea. I'm not familiar with Visual Studio or Windows.

2 1

Spot tool - installation error
by Ioana Huștiu 22 Aug '23

22 Aug '23

Dear authors, I am a PhD student at Technical University of Iasi, Romania and I also work with professor Cristian Mahulea from University of Zaragoza, Spain. During my research I'm finding the Spot tool to be very useful. I am writing to you as I encountered an error during the installation of Spot during the "make check" step. The generated file is attached below and it is not clear to me how I can solve this problem. I tried multiple times to install the tool, even by skipping the "make check" step, but in this case another error appeared when trying to install the stable package "python3-spot" - the python version that I have (meaning 3.9.7) is not >=3 python 3.5, which is quite strange. What would you recommend me to do? Thank you, Ioana Hustiu

2 1

The test ltlcross4.test fails
by Yuri 11 Jun '23

11 Jun '23

+ cat + /usr/local/bin/python3.9 test.py Traceback (most recent call last): File "/usr/local/lib/python3.9/site-packages/pandas/core/groupby/groupby.py", line 1490, in array_func result = self.grouper._cython_operation( File "/usr/local/lib/python3.9/site-packages/pandas/core/groupby/ops.py", line 959, in _cython_operation return cy_op.cython_operation( File "/usr/local/lib/python3.9/site-packages/pandas/core/groupby/ops.py", line 657, in cython_operation return self._cython_op_ndim_compat( File "/usr/local/lib/python3.9/site-packages/pandas/core/groupby/ops.py", line 482, in _cython_op_ndim_compat res = self._call_cython_op( File "/usr/local/lib/python3.9/site-packages/pandas/core/groupby/ops.py", line 541, in _call_cython_op func = self._get_cython_function(self.kind, self.how, values.dtype, is_numeric) File "/usr/local/lib/python3.9/site-packages/pandas/core/groupby/ops.py", line 173, in _get_cython_function raise NotImplementedError( NotImplementedError: function is not implemented for this dtype: [how->mean,dtype->object] During handling of the above exception, another exception occurred: Traceback (most recent call last): File "/usr/local/lib/python3.9/site-packages/pandas/core/nanops.py", line 1692, in _ensure_numeric x = float(x) ValueError: could not convert string to float: '(G(F(p0))) & (G(F(p1)))!((G(F(p0))) & (G(F(p1))))(G(F(p0))) -> (G(F(p1)))!((G(F(p0))) -> (G(F(p1))))' During handling of the above exception, another exception occurred: Traceback (most recent call last): File "/usr/local/lib/python3.9/site-packages/pandas/core/nanops.py", line 1696, in _ensure_numeric x = complex(x) ValueError: complex() arg is a malformed string The above exception was the direct cause of the following exception: Traceback (most recent call last): File "/usr/ports/math/spot/work/spot-2.11.5/tests/core/ltlcross4.dir/test.py", line 12, in <module> print(x.filter(('formula', 'tool', File "/usr/local/lib/python3.9/site-packages/pandas/core/groupby/generic.py", line 1269, in aggregate result = op.agg() File "/usr/local/lib/python3.9/site-packages/pandas/core/apply.py", line 166, in agg return self.agg_list_like() File "/usr/local/lib/python3.9/site-packages/pandas/core/apply.py", line 355, in agg_list_like new_res = colg.aggregate(arg, *self.args, **self.kwargs) File "/usr/local/lib/python3.9/site-packages/pandas/core/groupby/generic.py", line 238, in aggregate ret = self._aggregate_multiple_funcs(func, *args, **kwargs) File "/usr/local/lib/python3.9/site-packages/pandas/core/groupby/generic.py", line 316, in _aggregate_multiple_funcs results[key] = self.aggregate(func, *args, **kwargs) File "/usr/local/lib/python3.9/site-packages/pandas/core/groupby/generic.py", line 250, in aggregate return getattr(self, cyfunc)() File "/usr/local/lib/python3.9/site-packages/pandas/core/groupby/groupby.py", line 1855, in mean result = self._cython_agg_general( File "/usr/local/lib/python3.9/site-packages/pandas/core/groupby/groupby.py", line 1507, in _cython_agg_general new_mgr = data.grouped_reduce(array_func) File "/usr/local/lib/python3.9/site-packages/pandas/core/internals/base.py", line 197, in grouped_reduce res = func(arr) File "/usr/local/lib/python3.9/site-packages/pandas/core/groupby/groupby.py", line 1503, in array_func result = self._agg_py_fallback(values, ndim=data.ndim, alt=alt) File "/usr/local/lib/python3.9/site-packages/pandas/core/groupby/groupby.py", line 1457, in _agg_py_fallback res_values = self.grouper.agg_series(ser, alt, preserve_dtype=True) File "/usr/local/lib/python3.9/site-packages/pandas/core/groupby/ops.py", line 994, in agg_series result = self._aggregate_series_pure_python(obj, func) Version: 2.11.5 FreeBSD 13.2 Yuri

1 0

SPOT questions
by Yoav Ben Shimon 06 Jun '23

06 Jun '23

Hi, I ran into a couple of issues when using SPOT in a project. I'll be glad for any assistance. 1) I am calling sat_minimize from a python script using the spot python library. Is there any way to set a timeout on this function call? Or do I have to use the CLI if I want a timeout? 2) I am manipulating an automaton generated from an LTL formula, and then printing it in HOA format. Is there a way to guarantee that the initial state is the state numbered 0? If not, is there any other way to control the naming of states? Thank you, Yoav Ben Shimon

2 3

Spot Compilation on Windows
by Jonah Romero 05 Jun '23

05 Jun '23

Hello, I was just curious if there were any plans to support building Spot on windows? Or maybe any plans to use CMake in the future? If not, are there any suggestions for building on windows? Thanks, Jonah

2 1

APT install of python3-spot requires python version <<3.10
by mgerber59＠gmail.com 09 May '23

09 May '23

Hi, I'm a master student at RWTH Aachen, and am using spot as part of my master thesis. Thank you very much for developing and providing this awesome tool! However, I noticed that when attempting to install python3-spot via `apt install`, it fails with: ``` The following packages have unmet dependencies: python3-spot : Depends: python3 (< 3.10) but 3.10.6-1~22.04 is to be installed E: Unable to correct problems, you have held broken packages. ``` Checking out the package index at https://www.lrde.epita.fr/repo/debian/stable/Packages (Cmd-F for `python3-spot_2.11.5.0-1`), I notice that the package indeed specifies `python3 >= 3.9, python3 << 3.10` as a dependency, making it so it can only be installed alongside Python 3.9. I don't know what this restriction is used for, and would greatly appreciate it if it can be removed. Thank you, Marcel

2 1

Possible to allow for product_or without completing left/right automata
by Marcel Gerber 09 May '23

09 May '23

Hello, I notice that `product_or` necessarily runs `complete` on both input automata [see this line in spot/twaalgos/product.cc <https://gitlab.lre.epita.fr/spot/spot/-/blob/b487ff4190cdec4094154486bb8c04…>]. In contrast, this is not the case for the "normal" `product`. If my thinking is correct, this would not be necessary if both input automata are Büchi automata, correct? Because the union of two incomplete Büchi automata is an incomplete Büchi automaton again, and the product automaton construction applies as normal as far as I can tell. Would it be possible to allow for this, potentially by introducing another method or exposing the `product_aux` function (incl. from Python)? Right now, running `product_or`, even on small input automata, produces absolutely unwieldy automata that are impossible to interpret. This is mostly due to my use case, where I'm using letters of an alphabet more akin to a standard DFA model, and encoding a symbol of `a` into the preposition formula `a & !b & !c` etc. This works well with single automata and with intersections, but not with unions sadly. Your help would be very much appreciated, Marcel

2 1

APT install of python3-spot requires python version <<3.10
by Marcel Gerber 28 Apr '23

28 Apr '23

Hi, I'm a master student at RWTH Aachen, and am using spot as part of my master thesis. Thank you very much for developing and providing this awesome tool! However, I noticed that when attempting to install python3-spot via `apt install`, it fails with: The following packages have unmet dependencies: python3-spot : Depends: python3 (< 3.10) but 3.10.6-1~22.04 is to be installed E: Unable to correct problems, you have held broken packages. Checking out the package index at https://www.lrde.epita.fr/repo/debian/stable/Packages (Cmd-F for `python3-spot_2.11.5.0-1`), I notice that the package indeed specifies `python3 >= 3.9, python3 << 3.10` as a dependency, making it so it can only be installed alongside Python 3.9. I don't know what this restriction is used for, and would greatly appreciate it if it can be removed. Thank you, Marcel

1 0

Spot bus error
by Beutner, Raven 20 Apr '23

20 Apr '23

Dear spot team, I think I found a bug in spot. When I run % cat foo.hoa HOA: v1 States: 1 Start: 0 AP: 3 "l0" "l1" "l2" acc-name: generalized-Buchi 0 Acceptance: 0 t --BODY-- State: 0 [(0&1)] 0 [(2)] 0 [(!2)] 0 —-END-- %autfilt --small -S foo.hoa I get a bus error. It seems that options —small and -S are both necessary to reproduce the bug. Similarly, none of the transitions in the automaton can be removed. I am running spot version 2.11.4 on an MacBook Pro with M1 Pro CPU compiled with --disable-python. Given that this seems to be a “low-level” system error, it could very well be that it is an issue with my machine setup. In this case: Do you have any idea how to fix this? Thanks already for your help! All the best, Raven PS: The current download link for the most recent version of spot (https://spot.lre.epita.fr/install.html) claims to download version 2.11.4 but actually still points to version 2.11.3.

2 1

Test suite for spot installation
by Fraca Santamaria, Estibaliz 21 Mar '23

21 Mar '23

Hi, I'm trying to install spot in my machine. I run make check and I got two errors (Fail : 2). I am just reporting it as it is asked. Please find test-suite.log attached. The installation did fail. I would like to ask if you know why did it fail and what could I do to install it. Thank you

2 2

Mac OS Spot Library Installation
by Samuel Hongang Lam 10 Mar '23

10 Mar '23

Hello All, I am a PhD student that has been working on a project recently with a code base using the Spot library. The code was written on a Linux machine, but I have a MacBook running macOS. There seem to be some dependencies in the Spot library on glibc functions, such as strverscmp. I am inexperienced with setting up the libraries and such properly. Is there anywhere I can get help with setting up Spot to be able to access the features I need on a Mac? Any assistance would be greatly appreciated. Thank you! Sincerely, Samuel Lam

2 1

Deadline Extension: On the Effectiveness of Temporal Logics on Finite Traces in AI
by Antonio Di Stasio 30 Jan '23

30 Jan '23

CALL FOR PAPERS "On the Effectiveness of Temporal Logics on Finite Traces in AI" Part of the AAAI 2023 Spring Symposium Series <https://aaai.org/Symposia/Spring/sss23.php> March 27-29, 2023, Hyatt Regency San Francisco Airport, CA, USA Website: https://ltlf-symposium.github.io/ Temporal logics, such as Linear Temporal Logic (LTL), are widely adopted as a logical specification language in Formal Methods. They are also getting increasing attention from the AI Community. In AI, however, there is often a need to interpret such logics over finite traces, rather than the traditional infinite-trace interpretation. This is evident, for instance, in works on Planning, Reinforcement Learning, and Business Process Management. An important computational feature of working with finite traces is that it allows one to use standard finite-state automata to model and reason, rather than the more complex omega-automata used for infinite traces. This is a great simplification that has already had a significant impact on many areas of AI and CS. This symposium aims to bring together researchers working with temporal logics on finite traces, in basic research and applications, in order to discuss current results and future directions, and to facilitate the emergence of teams working across different areas. Topics Topics of interest span the use of temporal logics over finite traces, including (but not limited to) the following areas: - AI Planning - Verification and Synthesis - Reinforcement Learning - Automated Reasoning - Knowledge Representation - Multi-Agent Systems - Robotics - Motion and Task Planning - Discrete-Event Control - Workflow Management - Conversational Systems - Automated Service Composition - Business Process Management - Fintech - Cyber Security - Human Computer Interaction - Natural Language Processing Submissions Submissions should have a single main author, who will be the speaker, and each speaker can have no more than one submission. Each submission must not exceed 2 pages, including references (in AAAI style), and may refer to joint work with other collaborators to be credited in the presentation. There will be no formal proceedings and we encourage submissions of work presented or submitted elsewhere (no copyright transfer is required, only permission to post the abstract on the workshop site). Submissions should be uploaded via the AAAI SSS-23 EasyChair site. <https://easychair.org/conferences/?conf=sss23> Important Dates - *February 6, 2023*: Paper submission deadline (AoE). - *February 11, 2023*: Author notification (AoE). - March 27-29: AAAI Spring Symposium Series. Invited Speakers - Rance Cleaveland <https://www.cs.umd.edu/people/wcleavel>, University of Maryland, USA - Giuseppe De Giacomo <https://www.diag.uniroma1.it//degiacom/>, University of Oxford & Sapienza University of Rome, Italy - Lydia Kavraki <https://www.cs.rice.edu/~kavraki/>, Rice University, Houston, TX, USA - Shiela A. Mcilraith <https://www.cs.toronto.edu/~sheila/>, University of Toronto, Canada - Marco Montali <https://www.unibz.it/it/faculties/computer-science/academic-staff/person/31…>, University of Bolzano, Italy - Kristin Y. Rozier <https://www.engineering.iastate.edu/people/profile/kyrozier/>, Iowa State University, USA - Ufuk Topcu <https://www.ae.utexas.edu/people/faculty/faculty-directory/topcu>, University of Texas at Austin, TX, USA - Moshe Vardi <https://www.cs.rice.edu/~vardi/>, Rice University, Houston, TX, USA Organizing Committee - Suguman Bansal <https://suguman.github.io/>, Co-Chair, Georgia Institute of Technology, suguman(a)gatech.edu - Antonio Di Stasio <https://antoniodistasio.github.io/>, Co-Chair, University of Oxford, antonio.distasio(a)cs.ox.ac.uk - Sasha Rubin <https://sasharubin.github.io/>, Co-Chair, University of Sydney, sasha.rubin(a)sydney.edu.au - Shufang Zhu <https://shufang-zhu.github.io/>, Co-Chair, Sapienza University of Rome, zhu(a)diag.uniroma1.it Format The symposium will be conducted in a hybrid style, in-presence and on Zoom. Website For more information, please see the symposium website: https://ltlf-symposium.github.io/

1 0

[CfP]-Second Call: On the Effectiveness of Temporal Logics on Finite Traces in AI
by Antonio Di Stasio 20 Jan '23

20 Jan '23

CALL FOR PAPERS "On the Effectiveness of Temporal Logics on Finite Traces in AI" Part of the AAAI 2023 Spring Symposium Series <https://aaai.org/Symposia/Spring/sss23.php> March 27-29, 2023, Hyatt Regency San Francisco Airport, CA, USA Website: https://ltlf-symposium.github.io/ Temporal logics, such as Linear Temporal Logic (LTL), are widely adopted as a logical specification language in Formal Methods. They are also getting increasing attention from the AI Community. In AI, however, there is often a need to interpret such logics over finite traces, rather than the traditional infinite-trace interpretation. This is evident, for instance, in works on Planning, Reinforcement Learning, and Business Process Management. An important computational feature of working with finite traces is that it allows one to use standard finite-state automata to model and reason, rather than the more complex omega-automata used for infinite traces. This is a great simplification that has already had a significant impact on many areas of AI and CS. This symposium aims to bring together researchers working with temporal logics on finite traces, in basic research and applications, in order to discuss current results and future directions, and to facilitate the emergence of teams working across different areas. Topics Topics of interest span the use of temporal logics over finite traces, including (but not limited to) the following areas: - AI Planning - Verification and Synthesis - Reinforcement Learning - Automated Reasoning - Knowledge Representation - Multi-Agent Systems - Robotics - Motion and Task Planning - Discrete-Event Control - Workflow Management - Conversational Systems - Automated Service Composition - Business Process Management - Fintech - Cyber Security - Human Computer Interaction - Natural Language Processing Submissions Submissions should have a single main author, who will be the speaker, and each speaker can have no more than one submission. Each submission must not exceed 2 pages, including references (in AAAI style), and may refer to joint work with other collaborators to be credited in the presentation. There will be no formal proceedings and we encourage submissions of work presented or submitted elsewhere (no copyright transfer is required, only permission to post the abstract on the workshop site). Submissions should be uploaded via the AAAI SSS-23 EasyChair site. <https://easychair.org/conferences/?conf=sss23> Important Dates - January 30, 2023: Paper submission deadline (AoE). - February 4, 2023: Author notification (AoE). - March 27-29: AAAI Spring Symposium Series. Invited Speakers - Rance Cleaveland <https://www.cs.umd.edu/people/wcleavel>, University of Maryland, USA - Giuseppe De Giacomo <https://www.diag.uniroma1.it//degiacom/>, University of Oxford & Sapienza University of Rome, Italy - Lydia Kavraki <https://www.cs.rice.edu/~kavraki/>, Rice University, Houston, TX, USA - Shiela A. Mcilraith <https://www.cs.toronto.edu/~sheila/>, University of Toronto, Canada - Marco Montali <https://www.unibz.it/it/faculties/computer-science/academic-staff/person/31…>, University of Bolzano, Italy - Kristin Y. Rozier <https://www.engineering.iastate.edu/people/profile/kyrozier/>, Iowa State University, USA - Ufuk Topcu <https://www.ae.utexas.edu/people/faculty/faculty-directory/topcu>, University of Texas at Austin, TX, USA - Moshe Vardi <https://www.cs.rice.edu/~vardi/>, Rice University, Houston, TX, USA Organizing Committee - Suguman Bansal <https://suguman.github.io/>, Co-Chair, Georgia Institute of Technology, suguman(a)seas.upenn.edu - Antonio Di Stasio <https://antoniodistasio.github.io/>, Co-Chair, University of Oxford, antonio.distasio(a)cs.ox.ac.uk - Sasha Rubin <https://sasharubin.github.io/>, Co-Chair, University of Sydney, sasha.rubin(a)sydney.edu.au - Shufang Zhu <https://shufang-zhu.github.io/>, Co-Chair, Sapienza University of Rome, zhu(a)diag.uniroma1.it Website For more information, please see the symposium website: https://ltlf-symposium.github.io/

1 0

Bug when checking for automata emptiness in print_hoa()
by Beutner, Raven 04 Jan '23

04 Jan '23

Dear spot Team, I think I have found a bug in the emptiness checker of spot. When I use the following automation: HOA: v1 States: 8 Start: 0 Start: 1 AP: 0 acc-name: generalized-Buchi 2 Acceptance: 2 Inf(0)&Inf(1) --BODY-- State: 0 {0} [(t)] 2 [(t)] 3 State: 1 {0} [(t)] 4 [(t)] 5 State: 2 {0} [(t)] 2 [(t)] 3 State: 3 {0} [(t)] 6 [(t)] 7 State: 4 {1} [(t)] 4 [(t)] 5 State: 5 {1} [(t)] 6 [(t)] 7 State: 6 [(t)] 6 [(t)] 7 State: 7 [(t)] 6 [(t)] 7 --END-- And invoke "autfilt --is-empty aut.hoa” (where aut.hoa contains the above automaton) I get the following error: autfilt: print_hoa(): automaton has transition-based acceptance despite prop_state_acc()==true This seems to be related to a similar bug that was fixed in version 2.7.1, so should (hopefully) be easy to fix. I used version 2.11.3 on a MacBook Pro with M1 Pro CPU. All the best, Raven

2 1

[CfP]: On the Effectiveness of Temporal Logics on Finite Traces in AI
by Antonio Di Stasio 24 Dec '22

24 Dec '22

CALL FOR PAPERS "On the Effectiveness of Temporal Logics on Finite Traces in AI" Part of the AAAI 2023 Spring Symposium Series <https://aaai.org/Symposia/Spring/sss23.php> March 27-29, 2023, Hyatt Regency San Francisco Airport, CA, USA Website: https://ltlf-symposium.github.io/ Temporal logics, such as Linear Temporal Logic (LTL), are widely adopted as a logical specification language in Formal Methods. They are also getting increasing attention from the AI Community. In AI, however, there is often a need to interpret such logics over finite traces, rather than the traditional infinite-trace interpretation. This is evident, for instance, in works on Planning, Reinforcement Learning, and Business Process Management. An important computational feature of working with finite traces is that it allows one to use standard finite-state automata to model and reason, rather than the more complex omega-automata used for infinite traces. This is a great simplification that has already had a significant impact on many areas of AI and CS. This symposium aims to bring together researchers working with temporal logics on finite traces, in basic research and applications, in order to discuss current results and future directions, and to facilitate the emergence of teams working across different areas. Topics Topics of interest span the use of temporal logics over finite traces, including (but not limited to) the following areas: - AI Planning - Verification and Synthesis - Reinforcement Learning - Automated Reasoning - Knowledge Representation - Multi-Agent Systems - Robotics - Motion and Task Planning - Discrete-Event Control - Workflow Management - Conversational Systems - Automated Service Composition - Business Process Management - Fintech - Cyber Security - Human Computer Interaction - Natural Language Processing Submissions Submissions should have a single main author, who will be the speaker, and each speaker can have no more than one submission. Each submission must not exceed 2 pages, including references (in AAAI style), and may refer to joint work with other collaborators to be credited in the presentation. There will be no formal proceedings and we encourage submissions of work presented or submitted elsewhere (no copyright transfer is required, only permission to post the abstract on the workshop site). Submissions should be uploaded via the AAAI SSS-23 EasyChair site. <https://easychair.org/conferences/?conf=sss23> Important Dates - January 30, 2023: Paper submission deadline (AoE). - February 4, 2023: Author notification (AoE). - March 27-29: AAAI Spring Symposium Series. Invited Speakers - Rance Cleaveland <https://www.cs.umd.edu/people/wcleavel>, University of Maryland, USA - Giuseppe De Giacomo <https://www.diag.uniroma1.it//degiacom/>, University of Oxford & Sapienza University of Rome, Italy - Lydia Kavraki <https://www.cs.rice.edu/~kavraki/>, Rice University, Houston, TX, USA - Shiela A. Mcilraith <https://www.cs.toronto.edu/~sheila/>, University of Toronto, Canada - Marco Montali <https://www.unibz.it/it/faculties/computer-science/academic-staff/person/31…>, University of Bolzano, Italy - Kristin Y. Rozier <https://www.engineering.iastate.edu/people/profile/kyrozier/>, Iowa State University, USA - Ufuk Topcu <https://www.ae.utexas.edu/people/faculty/faculty-directory/topcu>, University of Texas at Austin, TX, USA - Moshe Vardi <https://www.cs.rice.edu/~vardi/>, Rice University, Houston, TX, USA Organizing Committee - Suguman Bansal <https://suguman.github.io/>, Co-Chair, Georgia Institute of Technology, suguman(a)seas.upenn.edu - Antonio Di Stasio <https://antoniodistasio.github.io/>, Co-Chair, Sapienza University of Rome, distasio(a)diag.uniroma1.it - Sasha Rubin <https://sasharubin.github.io/>, Co-Chair, University of Sydney, sasha.rubin(a)sydney.edu.au - Shufang Zhu <https://shufang-zhu.github.io/>, Co-Chair, Sapienza University of Rome, zhu(a)diag.uniroma1.it Website For more information, please see the symposium website: https://ltlf-symposium.github.io/

1 0

Generating unsatisfiable LTL formulae using randltl
by Pert, Charles 12 Dec '22

12 Dec '22

Hi, I am specifically trying to generate unsatisfiable LTL formulae using the randltl tool in Spot. I am struggling because the default tool is so much more likely to produce consistent and satisfiable formulae. Have you got any tips on how I can alter the generation to produce these types of formulae? Best wishes, Charles Pert

2 1

Bug report: implication prefix
by Liu, Jason Xinyu 30 Nov '22

30 Nov '22

Hello, It seems that Spot cannot parse implication and equivalent operators in prefix order. I tried on both my local machine and the online translator <https://spot.lre.epita.fr/app/>. The installed Spot version is 2.11.1. The commands are - local: spot.formula("-> a b") - online translator: type in -> a b Error message: syntax error, unexpected implication operator Thank you very much for your help and creating the conda package for Spot, that makes the installation very convenient! Happy holidays! Best, Jason

2 2

[bug] ltl2tgba gets stuck with this formula
by Jacopo Binchi 31 Oct '22

31 Oct '22

Dear Spot support team, I am a researcher at Developair Technologies. I write you looking for help with a formula that ltl2tgba cannot handle, possibly a bug. Here at Developair we have been using Spot for the past few months with great satisfaction. However, it seems that *ltl2tgba *cannot process the formula in attached file gb_formula.ltl . We let it run for quite some time (like hours) and it didn't terminate. On the other hand, Owl can process the same formula in a matter of a few milliseconds. We don't have any problem using ltl2tgba with other, similar formulas. It seems strange to us that Spot gets stuck with such a relatively simple formula, especially since in our experience Spot worked reliably well with other, way more complex formulas. Is it maybe a bug or something that we are doing wrong? Could you please help us? Please find some more details (version and command) below. Thank you. Best regards, J. Spot version: ltl2tgba --version > ltl2tgba (spot) 2.10.6 > > Copyright (C) 2022 Laboratoire de Recherche et Développement de l'Epita. > License GPLv3+: GNU GPL version 3 or later < > http://gnu.org/licenses/gpl.html>. > This is free software: you are free to change and redistribute it. > There is NO WARRANTY, to the extent permitted by law. > Command: ltl2tgba -S --deterministic --dot=s --output=output.txt -F gb_formula.ltl Using the "simplest" command "ltl2tgba -F gb_formula.ltl" produces the same result (that is, no result). For comparison, with Owl we used command: owl ltl2ldgba --state-acceptance -i gb_formula.ltl -o owl_gb.txt -- Jacopo Binchi jbinchi(a)developair.es Paseo de Miramón 170 20014 San Sebastián – Donostia Gipuzkoa (Spain) www.developair.es

2 2

Number of states and transitions
by pierreganty＠gmail.com 28 Oct '22

28 Oct '22

Hi all, I did not find how to get the number of states (reachable or not) of an automaton using autfilt (in particular the `--stats` option). The option provided by `autfilt --stats` is for reachable states only. I did find a workaround with `--hoaf` which outputs the automaton in HOA format and then getting the number from the `States:` header. For the number of transitions (reachable or not) I don't have a workaround. Since spot can compute these numbers easily, it seems handy (at least for me) to have a direct access to them thru the `--stats` interface. Thank you, Pierre.

3 3

Issue with Debian package signature
by Ocan Sankur 07 Oct '22

07 Oct '22

Hi all, I am trying to install spot on Ubuntu 20.04 following instructions from: https://spot.lrde.epita.fr/install.html But apt update complains about the signature: W: An error occurred during the signature verification. The repository is not updated and the previous index files will be used. GPG error: http://www.lrde.epita.fr/repo/debian stable/ InRelease: The following signatures were invalid: EXPKEYSIG 03D99E7444F2A84A LRDE Repository <admin(a)lrde.epita.fr> W: Failed to fetch http://www.lrde.epita.fr/repo/debian/stable/InRelease The following signatures were invalid: EXPKEYSIG 03D99E7444F2A84A LRDE Repository <admin(a)lrde.epita.fr> Could the signature be expired? I can actually install spot from source but Debian packages are useful for preparing artifact submissions. Thanks, Ocan

2 4

How to identify invalid transitions
by Raven Rothkopf 05 Aug '22

05 Aug '22

Dear Spot developers, Thank you so much for your helpful tool! We are undergraduate researchers at Barnard college and are using your tool for our summer research project. We are writing to ask if you would be able to help us understand a behavior of spot on a spec we are working with. We have the following small spec: ASSUME { G (! ((i1) && (i2))); } GUARANTEE { G (((o1) && (! (o2))) || ((o2) && (! (o1)))); (G (! ((i1) && (i2)))) -> (G (F (o2))); } From this, ltlsynt gives us: AP: 4 "i1" "i2" "o1" "o2" acc-name: all Acceptance: 0 t properties: trans-labels explicit-labels state-acc deterministic --BODY-- State: 0 [0&1&!2&!3 | 0&1&2&3] 0 [!0&!2&3 | !1&!2&3] 0 --END– Due to the ASSUME { G (! ((i1) && (i2)));}, the first transition in the hoa output should never happen. We understand that if a transition violates an assumption, it's still generated in hoa format because the system is free to choose any behavior and make any update. Some questions we have are: how does spot figure out if an assumption has been violated? Is there a flag that spot gives a transition that violates an assumption so that it can be dealt with differently? Instead of generating every possible behavior for the invalid transition, we are interested in removing it altogether. Is this possible to do through spot or do we need to come up with our own postprocessing algorithm? For context, we are working on a tool that takes a spec written in temporal logic and generates program code in a mealy machine format. We want to optimize the generated code so that it is as human-readable as possible. We appreciate any advice you can provide! Best, Leyi and Raven

2 2

Kripke, twa_product and twa_graph
by Pierre 22 Jun '22

22 Jun '22

Dear Spot devs, I am not sure how I am supposed to work with Kripke structures (which I imported using ltsmin) or `twa_product` (which I obtained using `otf_product` on the Kripke structure). In the screenshot below I can invoke 'exclusive_word' with no problems on a `kripke` and `twa_product` but the same is not true for 'contains' which returns a type error. The way I found to invoke 'contains' without errors is to use 'save' and then 'automaton' to read that same file again in order to get `twa_graph` as expected by `contains`. I am not sure this workaround is what the devs had in mind. Thank you for clarifying, PierreG [image: image.png]

2 1

Alphabet abstraction
by Pierre 04 Jun '22

04 Jun '22

Dear Spot devs, Is there a way for Spot to perform the alphabet abstraction available in GOAL as triggered with the `-a` switch when invoking the `alphabet` command? I paste the GOAL documentation about it below. Thank you, Pierre. - Alphabet -NAMEalphabet - Manipulate the alphabet of an automaton or a game.SYNOPSISalphabet -s [ -ap ] FILE_OR_LVALalphabet -e EXPR [ -ap ] FILE_OR_LVALalphabet -c EXPR [ -ap ] FILE_OR_LVALalphabet -r EXPR [ -ap ] FILE_OR_LVALalphabet -a EXPR [-R | -A | -S EXPR | -P EXPR | -ap ] FILE_OR_LVALDESCRIPTIONManipulate the alphabet of an automaton (or a game). This operation is directly applied to the input automaton. The returned value is always the new alphabet of the automaton (or the new atomic propositions if -ap is present). -s Simply return the alphabet of the input automaton or game. -ap Return the atomic propositions (or classical symbols) instead of the alphabet. -e Expand the alphabet by a list of propositions. -c Contract the alphabet by removing a list of propositions. -r Rename the propositions based on a map from a proposition to its new name. -a Abstract the alphabet based on a map from a predicate to its definition. -R Retain the transition symbols in alphabet abstraction. -A Only annotate the transitions with properties specified by -S and -P. -S Specify the name of the property that will store the symbols on the transitions in alphabet abstraction. -P Specify the name of the property that will store the evaluations of the predicates in alphabet abstraction. EXAMPLE alphabet -e "r" aut.gff alphabet -c "p" aut.gff alphabet -r "p=>r,q=>s" aut.gff alphabet -a "r=>p/\q" aut.gff alphabet -a "r=>p/\q" -A -P "Predicates" aut.gff

2 3

Building with Clang (on Mac)
by Shachar Itzhaky 17 May '22

17 May '22

Hello, There is a small hack in the lexer definition files `scanlt.ll` and `scanaut.ll` which fails the compilation on my Mac (macOS 12.3 arm64, Clang 13.1.6); they override `__STDC_VERSION__` which in turn wreaks havoc in the libc includes. I was able to fix the compilation using this small patch, which includes `libc-config.h` at the top in addition to `config.h`. I hope it would be useful to you. Cheers.

2 1

Regarding LTL with past
by David Lidell 16 May '22

16 May '22

3 4

Question regarding Spot operations on automata
by Edmond Irani Liu 22 Apr '22

22 Apr '22

Dear Spot team, greetings. This is Edmond Irani Liu, a Ph.D student at the Cyber-Physical Systems Group, Technical University of Munich. First of all, I would say thank you for your effort in developing such a great platform and tool! I have been using Spot lately, and have a few questions regarding automata manipulation in Spot. I attach a Jupyter notebook explaining my use case: we are using spot to compute the product automata of some LTLf formulas and our system described in Kripke structure. If I understand this (https://spot.lrde.epita.fr/tut12.html) page correctly, we need to append a new state at the end of the system that holds a proposition which becomes inactive at the end of our system. Could you give us a quick feedback if our formulation in the notebook is correct? There states z1-z8 are system states, and z9 is the extra state for Spot to correctly handle LTLf formulas. As we are trying to obtain the product automaton of a relatively large formula with our system, we assume that breaking down the formula and paralellizing the computation will observe a speed up in the computation. We would like to inquire if there exist operations like taking the union or intersection of the accepting runs of the automata? The concrete example is illustrated in the note book. Is there a documentation available somewhere explaining the functions of objects in the Python wrapper? I tried looking around but couldn't find one explaining those. An example is also attached. Thank you for your attention. Looking forward to hearing from you. Kind Regards, Edmond

2 1

How to read disjunction output?
by Mark Santolucito 15 Feb '22

15 Feb '22

Hi there, Thanks so much for the great tool! I am having trouble understanding the disjunction on state transitions. For example, I have the following small spec: ASSUME { G (p1); } GUARANTEE { G ((x) && (! (y)) || ((y) && (! (x)))); G (F x); G (F y); } From this, ltlsynt gives me: AP: 3 "x" "y" "p1" acc-name: all Acceptance: 0 t properties: trans-labels explicit-labels state-acc deterministic --BODY-- State: 0 [!0&!1&!2 | 0&1&!2] 1 [!0&1&2] 1 State: 1 [!0&!1&!2 | 0&1&!2] 1 [0&!1&2] 0 --END-- Should I understand the "[!0&!1&!2 | 0&1&!2] 1" to mean that when !2 is true, the system is free to choose from !0&!1 or 0&1? On a related note, due to the ASSUME in the spec, !2 should never be true anyway. Is there a way to filter this out of the model? For context, I am really looking to get a Mealy Machine out of ltlsynt which I can then convert into program code that would run in an infinite loop. Maybe I am just going about this the wrong way? Mark

2 1

How to free the memory of an automaton in spot's Python API?
by Yechuan Xia 31 Jan '22

31 Jan '22

Hi, I'm building some automatons using spot's python interface. Simply, codes like: for i in n: temp_aut = spot.automaton(aut.to_str()) # copy an automaton ...something del temp_aut But I found that whenever it enters a new loop, the memory of the automaton assigned to temp_aut is not freed. And it leads to a memory overflow. I thought this might be solved with 'delete temp_aut' in the C++ version spot, but in the python interface 'del temp' doesn't seem to work. Is there any interface in Python or other operations to make it possible?

3 9

Question regarding SPOT's accepting_run behaviour
by Clément TAMINES 14 Jan '22

14 Jan '22

Hello, I am contacting this list because I have a question regarding the behaviour of SPOT’s accepting_run function. I created an example (see attached) where, if I am not mistaken, the accepting run that is yielded does not satisfy the acceptance formula. Could you confirm that this is a problem and not a mistake in my understanding of the function and/or acceptance formula ? In addition, the acceptance formula is somehow detected as being a gen. Streett condition, can this be prevented and does it have an influence on how the emptiness check/accepting run generation is handled ? Thank you for your help, Clément

2 1

ltlsynt and hoa input
by Ayrat Khalimov 06 Jan '22

06 Jan '22

hello, Is there a way to feed HOA file (as a nondet Buchi) instead of a formula to ltlsynt? I tried smth (see below), but I am getting 'unrealisable' for nondet Buchi automaton spec that is supposed to be realisable (see attached). Maybe I missing something? (like ltlsynt dualising the automaton, etc.) Here is what I tried. Into file synthesis.cc, add: #include "spot/parseaut/public.hh" Then in line 822, comment out: // auto aut = trans.run(f); and instead add: spot::bdd_dict_ptr dict = spot::make_bdd_dict(); auto parsed_aut = parse_aut("/tmp/spec.hoa", dict); if (parsed_aut->aborted) abort(); auto aut = parsed_aut->aut; This forces ltlsynt to read file "/tmp/spec.hoa" and ignore the formula. Further, when calling ltlsynt, pass the argument --decompose=no ('just in case'): ./ltlsynt --formula="GF a" --ins=x,y --dot --outs=a,b,c --decompose=no and provide the correct --ins and --outs arguments, and any formula with one of those propositions. The tool outputs expected implementations on toy examples, but on a larger example attached it outputs "unrealizable" instead of "realizable". That is why the question. best wishes, Ayrat

2 5

Spot Debian package not working due to expired certificate error for the LRDE website
by Young, David Clark 02 Jan '22

02 Jan '22

Hi, I am trying to install Spot using the Debian package at www.lrde.epita.fr/repo/debian/ but it looks as though the security certificate for www.lrde.epita.fr has expired. In fact, it looks like it expired yesterday (Dec. 29th). The reason I'm installing Spot is that it's a dependency of another project I would like to install, and that project's Dockerfile uses the Debian package. It is possible to compile Spot from the source, but it is more efficient to use a Debian package (and potentially eases reproducibility, which is nice when using Docker). Would it be possible for someone to update the certificate? Thanks! - David

2 1

SPOT: formula:is_literal shall be marked const?
by Ayrat Khalimov 02 Dec '21

02 Dec '21

hi Alexandre, Seems like the function formula::is_literal() should be marked const: /// \brief Whether the formula is an atomic proposition or its /// negation. bool is_literal() { return (is(op::ap) || // If f is in nenoform, Not can only occur in front of // an atomic proposition. So this way we do not have // to check the type of the child. (is(op::Not) && is_boolean() && is_in_nenoform())); } kind wishes, Ayrat

2 1

[BUG] Tests fail to build on FreeBSD: error: use of undeclared identifier 'sched_getcpu'
by Yuri 23 Nov '21

23 Nov '21

On FreeBSD 13 version 2.10 fails to build tests: c++ -DHAVE_CONFIG_H -I. -I.. -I.. -I.. -I../buddy/src \-I../lib -I../lib -fno-omit-frame-pointer -D_THREAD_SAFE -DNDEBUG -O2 -pipe -fno-omit-frame-pointer -fstack-protector-strong -fno-strict-aliasing -fno-omit-frame-pointer -fvisibility=hidden -fvisibility-inlines-hidden -DSPOT_BUILD -std=c++17 -g -O3 -ffast-math -fstrict-aliasing -fomit-frame-pointer -pthread -O2 -pipe -fno-omit-frame-pointer -fstack-protector-strong -fno-strict-aliasing -fno-omit-frame-pointer -fvisibility=hidden -fvisibility-inlines-hidden -DSPOT_BUILD -std=c++17 -g -O3 -ffast-math -fstrict-aliasing -fomit-frame-pointer -MT ltsmin/modelcheck-modelcheck.o -MD -MP -MF ltsmin/.deps/modelcheck-modelcheck.Tpo -c -o ltsmin/modelcheck-modelcheck.o `test -f 'ltsmin/modelcheck.cc' || echo './'`ltsmin/modelcheck.cc In file included from ltsmin/modelcheck.cc:27: ../spot/mc/mc_instanciator.hh:122:43: error: use of undeclared identifier 'sched_getcpu' << ": on CPU " << sched_getcpu() << '\n'; ^ ../spot/mc/mc_instanciator.hh:134:9: error: unknown type name 'cpu_set_t'; did you mean 'cpusetid_t'? cpu_set_t cpuset; ^~~~~~~~~ cpusetid_t /usr/include/sys/types.h:86:22: note: 'cpusetid_t' declared here typedef __cpusetid_t cpusetid_t; ^ In file included from ltsmin/modelcheck.cc:27: ../spot/mc/mc_instanciator.hh:135:9: error: use of undeclared identifier 'CPU_ZERO' CPU_ZERO(&cpuset); ^ ../spot/mc/mc_instanciator.hh:136:9: error: use of undeclared identifier 'CPU_SET' CPU_SET(i, &cpuset); ^ ../spot/mc/mc_instanciator.hh:137:18: error: use of undeclared identifier 'pthread_setaffinity_np' int rc = pthread_setaffinity_np(threads[i].native_handle(), ^ ../spot/mc/mc_instanciator.hh:138:48: error: use of undeclared identifier 'cpu_set_t' sizeof(cpu_set_t), &cpuset); ^ 6 errors generated. Thanks, Yuri

2 1

Re: [Spot] Assistance with Spot
by Alexandre Duret-Lutz 19 Nov '21

19 Nov '21

Roei Nahum <roeina(a)nvidia.com> writes: > I didn’t fully understand what utility I miss by lowering tls-impl to > 2 (or to lower values) - are there additional materials I can use? Implication-based simplifications of LTL formulas are described in section 5.4.3 of https://spot.lrde.epita.fr/tl.pdf tls-impl=1 corresponds to tl_simplifier_options::synt_impl tls-impl=2 corresponds to tl_simplifier_options::synt_impl + tl_simplifier_options::containment_checks tls-impl=3 corresponds to tl_simplifier_options::synt_impl + tl_simplifier_options::containment_checks + tl_simplifier_options::containment_checks_stronger One question is whether your formulas require such simplification at all.

2 4

Behavior change in autfilt from 2.9.7 to 2.10
by Pierre Ganty 17 Nov '21

17 Nov '21

Hi, When invoking `autfilt sub.aut --included-in=sup.aut` on the two enclosed Buchi automata with Spot 2.10 I am getting: ``` Too many acceptance sets used. The limit is 32. ``` With Spot 2.9.7 I was getting a non-terminating execution. Is it the expected result? If so, what is the explanation behind the too many acceptance sets? Is it the complementation procedure for `sup.aut` that fails? Thank you and keep up with the excellent work, Pierre.

2 1

Evaluating a word on an automaton/formula
by Fatma Faruq 17 Nov '21

17 Nov '21

Hi, I was wondering if someone could point me to resources in spot that show how to evaluate an LTL word or trace on an automaton. Or anyway to check whether a trace or word satisfies a particular LTL formula. I'm new to Spot. So far I've been able to use the python notebook - word, (and other examples) to iterate over an automaton generated from an LTL formula. Thank you so much, -- Regards, Fatma

2 1

Assistance with Spot
by Roei Nahum 16 Nov '21

16 Nov '21

HI, My name is Roei Nahum. Your wonderful platform helps me to translate temporal formulas into Buchi automata. I downloaded Spot (version 2.9.4), and wrote a C++ program based on Spot API. As the following code snippet shows, I configured Spot so it will produce small state-based Buchi automata. I also skip the wdba minimalization. spot::option_map extra_options; spot::bdd_dict_ptr dict = spot::make_bdd_dict(); spot::translator* trans; extra_options.set("wdba-minimize", 0); trans = new spot::translator(dict, &extra_options); trans->set_type(spot::postprocessor::BA); trans->set_pref(spot::postprocessor::Small); twa_graph_ptr aut = trans->run(pf.f); Spot works very well on few examples I checked, but having a hard time with the following formula, in which it runs for a very long time without finishing: (!G(!({{a ##[1:500] b} ##[1:500] c}))) Can you please help me understand why? Is there anything I can configure differently in order to help it to be converged? Thanks in advance, Roei

2 3

Converting LTL_f to a finite automaton and plotting it via Graphviz.
by Bhatia, Amit RTX 15 Oct '21

15 Oct '21

Hello Spot Team, I recently came across your tool while searching for existing implementations to convert an LTL formula with finite semantics into a finite automata together with rendering it pictorially (e.g., using graphviz tool) - I was wondering if you have any examples of how this could be accomplished when the end goal is also to plot the automaton using GraphViz? I did read through https://spot.lrde.epita.fr/tut11.html (Translating an LTL formula into a monitor) and https://spot.lrde.epita.fr/tut12.html (Working with LTL formulas with finite semantics), but I am not sure if the output is already compliant with Graphviz's required format or some parsing is required (my knowledge of Graphviz is also fairly limited). Thanks, Amit Amit Bhatia Raytheon Technologies Research Center Berkeley, CA Amit.Bhatia2(a)rtx.com<mailto:Amit.Bhatia2@rtx.com>

2 1

Re: [Spot] Spot question
by Roei Nahum 05 Oct '21

05 Oct '21

Hi, Following the attached thread from December 2020. When working with version 2.9.4 of Spot, I got an endless runtime when I tried to create a small BA of this formula: (!(G({(a)} |=> {(b)[*32]}))) Thanks to your help, I understood that there was a bug in the mechanism that should avoid the WDBA-minimization in cases it creates to much additional states. (alexandre opened an issue for me – https://gitlab.lrde.epita.fr/spot/spot/-/issues/443) Was this bug fixed in any of the later versions? I met some additional problematic formulas. Currently, my only option to process such formulas is to avoid the WDBA-minimization step. Thanks in advance, Roei ******************* -----Original Message----- From: Roei Nahum Sent: Tuesday, December 8, 2020 5:40 PM To: Alexandre Duret-Lutz <adl(a)lrde.epita.fr> Subject: RE: [Spot] Spot question Great, now I get it. Thanks for the clarifications and debugging. I appreciate the time you spent to help. Roei ******************* -----Original Message----- From: Alexandre Duret-Lutz <adl(a)lrde.epita.fr> Sent: Tuesday, December 8, 2020 3:13 PM To: Roei Nahum <roeina(a)nvidia.com> Subject: Re: [Spot] Spot question External email: Use caution opening links or attachments On Tue, Dec 8, 2020 at 12:32 PM Roei Nahum <roeina(a)nvidia.com> wrote: > > Thanks Alexandre! I really appreciate your help. > > Disabling WDBA-minimize indeed fixed the problem. > > I have few questions, for better understanding. > > (1) What is the WDBA-minimize optimization and what it is used for? > Is it just a way to try minimizing the size of the produced automata? > Will I get a state-based Buchi automata even if I'll disable this optimization? A subset of LTL formulas, representing what are known as "obligation properties", can be translated into Weak Deterministic Büchi Automata. Those WDBA can be minimized using techniques similar to DFA minimization, i.e. in O(n log n), while minimization of DBA in general is NP-complete. So whenever you translate an LTL formula with an optimization level set to High (the default), and even if you do not specifically asked for a deterministic automaton, the translator will try to determinize your automaton and check if it is a WDBA to minimize it. Quite often, the minimal WDBA obtained is smaller than the non-deterministic BA that we were able to construct otherwise. See https://nam11.safelinks.protection.outlook.com/?url=https:%2F%2Fwww.lrde.ep… for a high-level view of the LTL translation pipeline. And references to the WDBA papers. Using "!wdba-minimize" is simply disabling the bottom branch, but you still get some simulation-based reductions in the top branch. A quite dated benchmark from around the time when WDBA minimization was introduced in Spot shows the effect of activating it: https://nam11.safelinks.protection.outlook.com/?url=https%3A%2F%2Fwww.lrde.… (The option names at the bottom of the first page are unrelated to those used today.) I consider this option to be the most useful automaton simplification in Spot, and the reason why automata produced by Spot are often smaller than those of other tools. (Hence the reason why I called this the "secret weapon" of Spot in the aforementioned slides.) The main problem with WDBA is that it requires a determinization. In the case of !G({a} |=> {b[*32]}), which can also be written as F(a & F[1:32]!b), there is a non-deterministic choice on the first state (see attachment). The determinization (a simple powerset construction) creates an exponential number of states, before the minimization has a chance to reduce it to 34 states. In fact for this particular kind of automata (with a "terminal" accepting state), I believe I should be able to write a smarter determinization that would keep 34 states in this very case. > (2) What do you mean by saying "I can still reproduce it."? > I'm working with version 2.9.4 of spot. Is there a more updated version where the problem is fixed? Or do you talk about future release? The 2.9.x versions are just bug fixes above version 2.9 released in April. The latest is 2.9.5, but if 2.9.4 works for you, there is no serious reason to upgrade. On the development version of Spot, which will probably be released as 2.10 early next year, I have made some changes meant to abort some determinization-based algorithms when they are optional and take too long. In the case of WDBA-minimization, the determinization is now meant to be aborted whenever it would create more than 4096 additional states. But you just highlighted a bug in that implementation. With the fix, I now see this: % for i in $(seq 1 32); do ./ltl2tgba "F(a & F[1:$i]\!b)" --stats="i=$i: %s states, %rs, det=%d"; done i=1: 3 states, 0.00108319s, det=1 i=2: 4 states, 0.00154409s, det=1 i=3: 5 states, 0.00198193s, det=1 i=4: 6 states, 0.00286866s, det=1 i=5: 7 states, 0.00366207s, det=1 i=6: 8 states, 0.00516698s, det=1 i=7: 9 states, 0.00783739s, det=1 i=8: 10 states, 0.0136073s, det=1 i=9: 11 states, 0.0108086s, det=0 i=10: 12 states, 0.0147442s, det=0 i=11: 13 states, 0.0231776s, det=0 i=12: 14 states, 0.0161911s, det=0 i=13: 15 states, 0.0161992s, det=0 i=14: 16 states, 0.0164307s, det=0 i=15: 17 states, 0.017823s, det=0 i=16: 18 states, 0.0197592s, det=0 i=17: 19 states, 0.0197573s, det=0 i=18: 20 states, 0.0203755s, det=0 i=19: 21 states, 0.020358s, det=0 i=20: 22 states, 0.0218632s, det=0 i=21: 23 states, 0.0229568s, det=0 i=22: 24 states, 0.0234896s, det=0 i=23: 25 states, 0.0295049s, det=0 i=24: 26 states, 0.0254808s, det=0 i=25: 27 states, 0.0256344s, det=0 i=26: 28 states, 0.0266605s, det=0 i=27: 29 states, 0.028628s, det=0 i=28: 30 states, 0.0296059s, det=0 i=29: 31 states, 0.0304871s, det=0 i=30: 32 states, 0.0319202s, det=0 i=31: 33 states, 0.0332124s, det=0 i=32: 34 states, 0.0340735s, det=0 See how the translation stopped building deterministic automata at i=9. Without WDBA-minimization you'd get non-deterministic automata everywhere. If my plan for a better determinization for terminal automata works I hope to get deterministic automata on all those lines. -- Alexandre Duret-Lutz External email: Use caution opening links or attachments ******************* On Tue, Dec 8, 2020 at 8:07 AM Roei Nahum <roeina(a)nvidia.com> wrote: > The problems started when I processed this formula: > > !G({(a)} |=> {(b)[*32]}) > > The code is running for a long time (more than a hour) without giving a result. > > Did it get stuck? Is there any way I can make it work? Humm, this formula seems to be taking an exponential time to translate: % for i in $(seq 1 20); do ltl2tgba --small -B -f "(!(G({(a)} |=> {(b)[*$i]})))" --stats="i=$i: %s states, %rs"; done i=1: 3 states, 0.000980134s i=2: 4 states, 0.00161671s i=3: 5 states, 0.00199145s i=4: 6 states, 0.00283387s i=5: 7 states, 0.00336581s i=6: 8 states, 0.00495071s i=7: 9 states, 0.00683196s i=8: 10 states, 0.0120013s i=9: 11 states, 0.00975352s i=10: 12 states, 0.0136751s i=11: 13 states, 0.0231716s i=12: 14 states, 0.0372669s i=13: 15 states, 0.0729032s i=14: 16 states, 0.153856s i=15: 17 states, 0.299823s i=16: 18 states, 0.656352s i=17: 19 states, 1.48609s i=18: 20 states, 3.0405s i=19: 21 states, 6.51409s i=20: 22 states, 13.3897s Passing --low (that's "trans.set_level(spot::postprocessor::Low);" for you) to remove all simplifications seems to produce automata of equivalent size much faster: % for i in $(seq 16 32); do ltl2tgba --small -B --low -f "(!(G({(a)} |=> {(b)[*$i]})))" --stats="i=$i: %s states, %rs"; done i=16: 18 states, 0.0013444s i=17: 19 states, 0.00170704s i=18: 20 states, 0.00172487s i=19: 21 states, 0.00159999s i=20: 22 states, 0.00181502s i=21: 23 states, 0.00237525s i=22: 24 states, 0.00208415s i=23: 25 states, 0.00253886s i=24: 26 states, 0.00216258s i=25: 27 states, 0.00239979s i=26: 28 states, 0.00271767s i=27: 29 states, 0.0025924s i=28: 30 states, 0.00297612s i=29: 31 states, 0.00285316s i=30: 32 states, 0.00323873s i=31: 33 states, 0.00352748s i=32: 34 states, 0.00316449s Alternatively, it's possible to keep all simplifications on, but just disable WDBA-minimization with % ltl2tgba --small -B -x '!wdba-minimize' -f "(!(G({(a)} |=> {(b)[*32]})))" --stats="%s states, %rs" 34 states, 0.0236776s To do the above in C++, you need to create and option_map object and pass it to the translator object, as in : ... spot::option_map extra_options; extra_options.set("wdba-minimize", 0); spot::bdd_dict_ptr dict = spot::make_bdd_dict(); spot::translator trans(dict, &extra_options); ... I'll look more into it, because I thought I had fixed that problem in the development version of Spot a couple of months ago, but I can still reproduce it. I'll post updates on https://nam11.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgitlab.lr… -- Alexandre Duret-Lutz ******************* HI, My name is Roei Nahum. I recently got to know SPOT, and first of all, I want to thank you for this great platform. I’m having an issue and I’ll appreciate if you can assist. I use SPOT in order to translate temporal formulas into automata. To do so, I downloaded spot, and wrote a C++ program based on SPOT API. The program I wrote is basically like this: …get the formula… spot::parsed_formula cex_pf = spot::parse_infix_psl(formula); if(cex_pf.format_errors(std::cerr)){ cout << "Invalid formula syntax: " << formula << endl; exit(1) } spot::translator trans; trans.set_type(spot::postprocessor::BA); trans.set_pref(spot::postprocessor::Small); twa_graph_ptr aut = trans.run(cex_pf.f); …print the automata… I tried running this code on several formulas, and it works great. The problems started when I processed this formula: G({(a)} |=> {(b)[*32]}) The code is running for a long time (more than a hour) without giving a result. Did it get stuck? Is there any way I can make it work? Thanks, Roei Nahum

2 1

Unambiguous refinements of collections of BDDs
by Michaël Cadilhac 02 Aug '21

02 Aug '21

Hi there all, Since I started using BDDs in automata, I have faced the following computational problem a few times. If you have any insight on how to solve it more efficiently, I'd be very interested. In particular, is there a spot in spot where this is implemented? Let me spell the problem out in general terms, then tie it to BDDs. *Definitions.* - A collection C of sets over a finite universe U is *unambiguous* if all sets in C are pairwise disjoint. In other words, C is a partition of the union of its sets. - A collection C' refines a collection C if each set in C can be obtained as the union of sets in C'. *Problem.* Given a collection C, compute a (minimal) unambiguous refinement of C. [[For complexity purposes, the computational task can also be written as: Given C and k, does there exist an unambiguous refinement of C of size < k? This is certainly NP-complete ([SP7] in Garey and Johnson is that problem without "unambiguous").]] *Motivation.* In BDDs, my use case is to have C be a collection of BDDs and a BDD represent the set of its satisfying assignments. Building an unambiguous refinement of BDDs seems an essential step in determinization: If I have a state with two outgoing transitions labeled with BDDs {F, G} such that F&G is not False, then this state is nondeterministic. To determinize it, we will have to consider the transition labels {F&G, F&!G, !F&G}. Note that this set refines {F, G}, since F = (F&G)|(F&!G) and similarly for G. *Question.* What is known about that problem? Is there a good heuristic for it that would give an unambiguous refinement not far from the optimal? *Implementations.* I implemented it in a few different ways and would be interested in alternative implementations. Two options I have are: *- The straightforward way:* 1. C' = {U} (recall that U is our universe, with BDDs this would be True) 2. for each S in C: 3. for each S' in C': 4. if (S cap S' is not empty) 5. Remove S' from C' 6. Add (S cap S') and (S^c cap S') to C' (^c denotes complement). *- A slightly more complex implementation.* I encode C' as a BDD itself, introducing lots of fresh variables; namely, if C' = {F, G} for two BDDs F and G, I introduce two fresh variables X_F and X_G, and encode C' as (F & X_F) | (G & X_G). This allows lines 3 and 4 to become: 3. Compute C' & S and project it on the X_? variables. 4. Iterate through each of the variables that appear: if X_S' appears, this means that S cap S' is nonempty. Thanks for reading! Cheers, Michaël

2 1

Time to decide inclusion
by Pierre Ganty 02 Aug '21

02 Aug '21

Dear Spot devs, I want to measure how much time it takes Spot to decide whether the language of the automaton A is contained in that of B. I've been using the following command ``` autfilt '--stats=%r, %R' A.hoa --included-in=B.hoa ``` I think I am not interpreting the results correctly because `--stats` reports very small numbers while adding `time` in front of the command reports much much larger numbers (several orders of magnitude larger). What's the right way to measure the time it takes Spot to decide the inclusion? Thank you. Pierre.

2 1

latexmk required to build spot
by Maxime Bouton 29 May '21

29 May '21

Dear spot maintainers, I am trying to compile spot v2.9.7 from source but my build errors due to latexmk not being available in the environment. From what I understand from the log, it is used in making the doc, is there a way to skip this step in the build? I built it on ubuntu (gcc (Ubuntu 9.3.0-17ubuntu1~20.04) 9.3.0) and it did not complain about latexmk, this only happened when changing to a new platform (the end goal is to cross compile it). Any help would be appreciated, Maxime I am using a linux platform with gcc: x86_64-linux-gnu-g++ (GCC) 9.1.0 Here is what I run: ./configure --prefix=${prefix}/spot-build --build=${MACHTYPE} --host=${target} --disable-python make -j${nproc} && make install Here is the partial log: ``` [15:46:03] Making all in doc [15:46:03] make[2]: Entering directory '/workspace/srcdir/jlspot/spot-2.9.7/doc' [15:46:03] Making all in tl [15:46:03] make[3]: Entering directory '/workspace/srcdir/jlspot/spot-2.9.7/doc/tl' [15:46:03] BIBINPUTS='./..' latexmk -pdf -ps- -dvi- -pvc- -e '$bibtex_use=2' -e '$pdflatex="pdflatex %O \"\\def\\SpotVersion{2.9.7}\\input{%S}\""' ./tl.tex [15:46:03] /bin/sh: latexmk: not found [15:46:03] make[3]: *** [Makefile:1399: tl.pdf] Error 127 [15:46:03] make[3]: Leaving directory '/workspace/srcdir/jlspot/spot-2.9.7/doc/tl' [15:46:03] make[2]: *** [Makefile:1319: all-recursive] Error 1 [15:46:03] make[2]: Leaving directory '/workspace/srcdir/jlspot/spot-2.9.7/doc' [15:46:03] make[1]: *** [Makefile:1341: all-recursive] Error 1 [15:46:03] make[1]: Leaving directory '/workspace/srcdir/jlspot/spot-2.9.7' ````

2 2

[Not-really-Spot] BDD libraries
by Michaël Cadilhac 27 May '21

27 May '21

Hi there ADL & all, Apologies for the not-really-spot question, but the expertise on this list is quite unique! I'm about to embark on a new project that relies on BDD. My only experience with BDD libraries was through using Spot, so I'm familiar with BuDDy, but that's it. Starting something fresh, I'm pondering what's the best C++ BDD library available nowadays. I axed through BuDDy and refactored it so that it's template-only and encapsulated the global variables in a class (hoping for some performance boost from inlining). While I'm fairly happy with the result, I now realize that there's been some progress in the BDD landscape since 1997—crazy! This paper: https://www.tvandijk.nl/pdf/2015setta.pdf by the author of Sylvan seems to indicate that Sylvan offers good performances on a single core, and great perf on multicore. It also comes with a nice C++ interface. I guess my question is: If you had to go from scratch today, which BDD library would you use? Cheers, M.

2 3

Walking through BDD formula in python
by Ayrat Khalimov 26 May '21

26 May '21

hi! With the aid of SPOT I am developing a counter-example guided synthesizer in python. See [1] if interested for details. My question is: I am trying to parse twa_run in python, namely, parse the labels of the each step (`spot.impl.step`). Is there a python way to walk through BDD? (The label is a simple cube expressed in BDD, and I need to convert it into my internal structure) (yes, this is rather a question about python interface for buddy) (no, that is not feature request:) if not possible, I will simply print the label and parse the string, that is not crucial) [1] The idea is - guess the model, - then model check it and get a counter-example - then encode the counter-example into the "guesser" (which uses an SMT solver) thanks, Ayrat

2 5

fail to install spot
by Jueming Hu 15 Apr '21

15 Apr '21

Good afternoon, I am Jueming, a Ph. D. student at Arizona State University. I would like to use spot for my research, such as getting the graph of an LTL formula. I downloaded 'linux-64/spot-2.9.6-py38_2.tar.bz2' and ran 'conda install -c adl spot' within the extracted folder. 'spot 2.5.2' is shown in conda list and also in python packages. However, 'import spot' doesn't work. The error says, 'No module named 'spot''. I have also tried 'linux-64/spot-2.9.4-py38_2.tar.bz2', 'conda install -c adl/label/adl spot', 'conda install -c adl/label/dev spot', append system path before import spot, and export LD_LIBRARY_PATH. But spot still doesn't work on my pc. Could you please help me install spot? Thanks in advance and looking forward to hearing from you. Best, Jueming

2 1

Question about Transfoming from Non-deterministic Automata to Deterministic Automata
by Meng Ruijie 23 Mar '21

23 Mar '21

Dear Spot Team, Thanks for providing a wonderful tool. During constructing Buchi automata for LTL, Spot always shows non-determinism automata although I select the "deterministic" item. Would you mind telling me how to construct deterministic automata with Spot? Here is one LTL: !(false R (iusr2_ai3_re13 & (! X (true U iusr2_ai3_re14) | X (true U (iusr2_ai3_re14 & (true U ousr2_ai3_ce8)))))). The following is its automata but non-determinism. [cid:83ad2cd0-bc60-443c-b387-4bc7953c05d2] Looking forward to your response. Kind Regards, Ruijie

2 1

Translations to DPA
by Tobias Meggendorfer 18 Mar '21

18 Mar '21

Hi, I'm using / comparing Spot and other tools in the Rabin to Parity translation. I have two questions (to ensure my comparison is fair): 1) I want to minimize the input automata using Spot to remove the effects of preprocessing done by each tool as much as possible. However, I require that the acceptance condition remains a Rabin condition. Right now, I am using the call autfilt --remove-dead-states --cleanup-acceptance --remove-unused-ap --simplify-exclusive-ap --simplify-acc --partial-degeneralize --generalized-rabin --deterministic The last two are an effort to ensure that simplify-acc doesn't change the acceptance condition. 2) What are the ways to tell spot to translate DRA to DPA? Right now, I am using autfilt --hoa --deterministic --parity. This seems to be a sort of black box (which is fine with me). Just to make sure: Are there other DRA-to-DPA translations included in Spot which are worthwhile to be investigated? Cheers, Tobias

2 3

ltlfilt filtering duplicates
by David Müller 18 Mar '21

18 Mar '21

Hi Alexandre, I hope you are not affected too badly by COVID and you and your family can deal with it in a good way. Simon and I stumbled over some slight problems with ltlfilt in combination with the flags -u and --relabel-bool=pnn. We expected to remove the duplicates, and thus being idempotent. However, we came across a set of LTL formulas, where two applications of ltlfilt -u --relabel-bool=pnn delivered a different result from applying it once. I attach the set of LTL formulas (ltlfilt-duplicates/ base.ltl in the archive) and a short script to evaluate the problem (ltlfilt- duplicates/reproduce.sh). I also tried to input a sorted list, it changed the numbers, but not the problem of being not idempotent. Could you tell us, whether we misunderstood something? Best regards, David

2 1

Re: [Spot] set property "original-states" in function "purge_dead_states()
by Alexandre Duret-Lutz 06 Mar '21

06 Mar '21

Tobias John <tobias.john(a)tu-dresden.de> writes: > thanks for your quick response. Your suggestion solves my problem. > > I think a function like "set_default_original_states()" would be > helpful but it is not necessary. In my opinion, it is more important > to mention somewhere in the documentation, e.g. at > > https://spot.lrde.epita.fr/concepts.html#named-properties > > that one needs to set the property somewhen before transforming the > automaton. Yes. The usage is however not very uniform. Some functions, like degeneralize() have to maintain the equivalent of "original-states" in order to work. This function will always define "original-states" if it wasn't present, because that comes for free. However if "original-states" was defined previously, the two mappings will be composed at an extra-cost.

1 0

set property "original-states" in function "purge_dead_states()
by Tobias John 05 Mar '21

05 Mar '21

Hello, I am using Spot for my Master Thesis. I try to simplify omega-automata by removing unnecessary states, e.g. states that are unreachable. The function "purge_dead_states()" does the job but there is an issue: for my application, I need to know the original state numbers of the states in the resulting (smaller) automaton, i.e. I need to map the states of the resulting automaton to the states of the original automaton. Is there some way to get the original state numbers from the reduced automaton? My intuition is that the property "original-states" would be suitable to store the original state numbers but the function "purge_dead_states()" does not set this property. In my opinion, the function "purge_dead_states()" setting the property "original-states" would be a useful feature to be included in future releases of Spot. Best regards, Tobias

2 1

Encode input formula into URL
by John Lång 23 Feb '21

23 Feb '21

Hello, I'd like to thank the developers for the awesome Spot's online LTL toolset! It's helping me a lot with my model checking project with Spin. This is exactly how formal methods should look like in the 2020'ies... If I may be so bold to request a feature, would it be possible to encode the input formula into URL, so that I could share a link with my fellow students? Best regards, John Lång

2 1

defrag_states: does it delete edges to erased states?
by Michaël Cadilhac 18 Feb '21

18 Feb '21

Hi there, In a preprocessing step, I want to flush a few states from a TωA. The one method that seems to be available is defrag_states, the description of which having the expected semantics. However, after defrag, it sometimes happens that the dst of some transitions points to delete states (-1U). The code of defrag_states in graph.hh removes the outgoing transitions of deleted states but does not seem to flush the transitions *pointing to* deleted states—is this the expected behavior? Cheers, M.

2 2

LTLf simplification
by Walke, Homer 04 Jan '21

04 Jan '21

Hi! I know Spot doesn't provide much support for LTLf (LTL with finite trace semantics) but I need to simplify some LTLf formulas. I was wondering which tl_simplifier_options, if any, would simplify according to the semantics of LTLf, i.e reduce_basics, synt_impl, etc. I know that using all the rewritings wouldn't work since many of them only apply to LTL and not LTLf but I'd like to use any rewritings that do apply to LTLf. Would anyone be able to point me in the right direction? Alternatively do you know of another software package that might do LTLf simplification? Thanks! Homer

2 1

model checking using spot
by Philip Schwartz 31 Dec '20

31 Dec '20

Hello, If I have a deterministic automata and an LTL or python function which gets a word and return T/F. Is it possible to set model checking for the dfa? to get a counterexample which distinguishes the dfa and the LTL/ python target function? Regards, Phillip

2 1

Spot question
by Roei Nahum 08 Dec '20

08 Dec '20

HI, My name is Roei Nahum. I recently got to know SPOT, and first of all, I want to thank you for this great platform. I'm having an issue and I'll appreciate if you can assist. I use SPOT in order to translate temporal formulas into automata. To do so, I downloaded spot, and wrote a C++ program based on SPOT API. The program I wrote is basically like this: ...get the formula... spot::parsed_formula cex_pf = spot::parse_infix_psl(formula); if(cex_pf.format_errors(std::cerr)){ cout << "Invalid formula syntax: " << formula << endl; exit(1) } spot::translator trans; trans.set_type(spot::postprocessor::BA); trans.set_pref(spot::postprocessor::Small); twa_graph_ptr aut = trans.run(cex_pf.f); ...print the automata... I tried running this code on several formulas, and it works great. The problems started when I processed this formula: G({(a)} |=> {(b)[*32]}) The code is running for a long time (more than a hour) without giving a result. Did it get stuck? Is there any way I can make it work? Thanks, Roei Nahum

2 2

intersection spot automatas
by Philip Schwartz 24 Nov '20

24 Nov '20

Hello Prof. Alexandre Duret-Lutz Is it possible to do a straightforward intersection between 2 automatas and check if the intersection has an accepting state? Regards, Phillip

2 5

membership query using spot
by רועי פוגלר 24 Nov '20

24 Nov '20

Hello, Is there a way to "ask" an automata if it accepts a word? e.g. a = spot.translate('a U b') a.accepts('b') ?T/F Regards, Roi

2 3

Question regarding Spot and MTL
by Edmond Irani Liu 18 Nov '20

18 Nov '20

Dear Spot team, greetings. This is Edmond Irani Liu, a Ph.D student at the Cyber-Physical Systems Group, Technical University of Munich. First of all, I would say thank you for your effort in developing such a great platform and tool! I will explain a bit about how we have used Spot in our research and then pose my questions below. We are recently working on formalization of traffic rules to further obtain traffic rule-compliant motion trajectories for automated vehicles. As a simple prototype, we have used Spot to translated some simple rules in LTL into a Büchi Automaton and later obtained its product automaton with the transition system of the discrete states of the vehicle. We could obtain some nice results with it : ) We are now trying to take one step further and to formalize more traffic rules, but came across the limitations of LTL, and switched to MTL for the reason that it is able to specify timed constraints, e.g. Always keep a safe distance to a leading vehicle if it did not perform a cut-in maneuver for the last 3 seconds. My questions are as follows: By any chance, is there some kind of workaround in Spot with which one can incorporate the mentioned timed constraints? (Last x seconds, future x seconds, ..) Of course our system state is also discrete with a 0.1 seconds step in time. If it is not possible with Spot, do you know some related model checker which can potentially handle this situation? I have been looking around but so far did not come across a tool which handles MTL/timed-automaton as nicely as Spot handles LTL. Thank you very much for your time reading this mail. I appreciate in advance for any feedback regarding the content. Kind Regards, Edmond

2 1

compare automata with exclusive_word
by Philip Schwartz 16 Nov '20

16 Nov '20

Hello Prof. Alexandre Duret-Lutz Thank you again for all your answers. I tried to compare 2 automats created using spot and got a a counterexample although they seems to be equal: aut2 = spot.translate(spot.formula("p1 U p2")) aut = spot.make_twa_graph(aut2.get_dict()) p1 = buddy.bdd_ithvar(aut.register_ap("p1")) p2 = buddy.bdd_ithvar(aut.register_ap("p2")) aut.new_states(2) aut.set_init_state(0) aut.new_edge(0, 0, p1 & buddy.bdd_not(p2)) aut.new_edge(0, 1, p2) aut.new_edge(1, 1, p1 & buddy.bdd_not(p2)) aut.new_edge(1, 1, p2) aut.set_acceptance(1, "Inf(1)") print(aut2.exclusive_word(aut)) # actual result - “p2; cycle{p1 & !p2}” # expected - None Best Regards, Phillipp

2 8

LTL formula accepts/rejects a word
by Philipp schwartz 12 Nov '20

12 Nov '20

Hello, My name is Phillip and I tried to use Spot tool to "play" with LTL formulas. My question is, is it possible to get boolean result if LTL formula accepts or rejects a word? e.g. In case the LTL formula is "aUb" is it possible to check that the formula is accepting "cycle(b)"? Best regards, Phillip

3 10

comapre spot automata
by רועי פוגלר 08 Nov '20

08 Nov '20

Hello, 1. I tried to compare 2 spot automata as described here -> https://spot-sandbox.lrde.epita.fr/notebooks/examples%20(read%20only)/conta… (last section) but, I got a counterexample which I think is not correct since both automata are not accepting this counterexample: I tried to compare automata which presents P1 U p2 and automata which answers "no" to everything and I got cycle{P1 & !p2} as a counterexample. attached picture with the code and examples from Ide. 2. Is there a way to transfer spot automata to LTL? Regards, Roi

3 8

check if word exists in language
by רועי פוגלר 22 Oct '20

22 Oct '20

Hello, When my input is a word (string such as 'p1 & !p2; cycle{p2}') and spot automata, (e.g. f = spot.formula("p1 U p2") aut = spot.translate(f, 'low') ) is it possible to check if the word exists in automata? Regards, Roi

1 1

print spot automata using graphviz
by רועי פוגלר 21 Oct '20

21 Oct '20

Hello, How can I print the automata graph? aut.show() and display(aut) does not work in simple python file (not jupyter notebook) Regards, Roi

2 1

Spot tool
by רועי פוגלר 20 Oct '20

20 Oct '20

My name is Roi and I'm an Msc student at Bar Ilan University (Israel). I'm trying to use the spot tool (python version) and I'm trying to figure out how to build spot-automata (spot.twa_graph object) type when my input is the edges, states and accepting states. can you help me please with that? In addition, is there an example of Angluin implementation using Spot? Regards, Roi

2 4

Spot tool
by רועי פוגלר 19 Oct '20

19 Oct '20

My name is Roi and I'm an Msc student at Bar Ilan University (Israel). I'm trying to use the spot tool (python version) and I'm trying to figure out how to build spot-automata (spot.twa_graph object) type when my input is the edges, states and accepting states. can you help me please with that? In addition, is there an example of Angluin implementation using Spot? Regards, Roi

1 0

Re: [Spot] Explicit order of sub-formulas in formula constructor
by Alexandre Duret-Lutz 06 Oct '20

06 Oct '20

On Tue, Oct 6, 2020 at 5:09 PM Niklas Metzger <niklas.metzger(a)cispa.saarland> wrote: > > Hi Alexandre, > > thank you for your fast response! I’m a bit confused on the meaning of creation time: > > >>> import spot > >>> f = spot.formula("Fa") > >>> ff = spot.formula("Ga") > >>> spot.formula.Or([f, ff]) > spot.formula("Fa | Ga") > >>> f = spot.formula("Ga") > >>> ff = spot.formula("Fa") > >>> spot.formula.Or([f, ff]) > spot.formula("Fa | Ga") > >>> n = spot.formula("Ga") > >>> nn = spot.formula("Fa") > >>> spot.formula.Or([n, nn]) > spot.formula("Fa | Ga") > > Is there some internal representation that does not create new objects if seen before? Yes. You can also use print(f.id()) to display the "serial number" of formula f. That's an identifier incremented for each new formula (new in the sense "not seen before"). This value is used to sort formulas (e.g., order the operands), or as hash value. But it is not necessarily unique in the case that so many formulas are created that the counter loops. -- Alexandre Duret-Lutz

1 0

Explicit order of sub-formulas in formula constructor
by Niklas Metzger 06 Oct '20

06 Oct '20

Hi! I’m currently using Spot to manipulate LTL formulas (using Python) and encountered the following behaviour: The result of "spot.formula.Or([x,y])” possibly changes the order of the subformulas, e.g. globally will appear in front of finally. Is there a way to build formulas that stick to the given order? Best and thanks in advance Niklas

2 1

Question on LTL to buechi automata
by Zhen Dong 24 Sep '20

24 Sep '20

Dear Spot team, Thanks for developing the nice tool Spot. I am a researcher at National University of Singapore using Spot in my research. I have a question about translating LTL to buechi automata using spot. My LTL properties are constraints over input/output sequences of a program, e.g., output W, output P always responds to input B (false R (! iB | (true U (oW & X (true U oP))))) where iB indicates that input B and oP indicates output P. The buechi automata of the negation of above formula given by Spot is in the following: [image: image.png] Here is a input/output trace to be evaluated: iH oZ iH oR iC oR iH oX iC oR iH oX iD oZ iJ oT iD oT iF oR iH oP iH oR iH oP iH oR iH oP iH oR iH oP iH oR iH oP iH oR iH oP iH oR iH oP iH *What I do not understand is that the proposition on the transition from state 0 to state 2 is iB & oW. How can I interpret it?* Given the input/output trace, there is no element that is iB and at the same time is oW. I assume the verification feeds element in the trace to the automata one by one. Do I miss something e.g., wrong configuration on the translation or some basic knowledge about verification? Can you give me some advice on this issue? Thank you very much. Best regards Zhen -- Zhen Dong Senior Research Fellow National University of Singapore https://www.comp.nus.edu.sg/~dongz/

2 2

Spot Polish Notation Parsing
by Niklas Metzger 31 Jul '20

31 Jul '20

Hi Spot Team! First of all, thanks for providing and maintaining such a great tool! I stumbled over a problem with formulas in polish notation: Parsing a formula like “-> a b” returns the “syntax error, unexpected implication operator” (Also tested on the website). It seems like implication and equivalence are not supported by that parser. Is there a technical reason for that and if not, could you give me a hint how to implement it? Thanks in advance Niklas Metzger

2 1

Segfault when postprocessing large automaton
by Reed Oei 20 Apr '20

20 Apr '20

Hello, I am encountering a bug where Spot segfaults when I try to postprocess a relatively large automaton. I have uploaded the file to http://reedoei.com/files/smaller-inner.aut.zip; it has 113930 states and 1537155 edges. I tried to come up with a smaller example but was having trouble doing so. Below is the sequence of commands, using the Python bindings, to reproduce this bug for me: import spot A = spot.automaton('smaller-inner.aut') B = A.postprocess('BA', 'Deterministic', 'Low') # Crashes here B.save('postprocessed.aut') I also tried using various other others for postprocess such as Small and Low, or Any and High (because Any and Low/Medium does nothing). I am using Ubuntu 18.04, Python 3.6.9, and Spot 2.8.7 (but also tried with 2.8.6). Thank you, Reed Oei

2 3

accepting_run() returning words containing false
by Jens Kreber 10 Apr '20

10 Apr '20

Hello, I am using spot to check randomly generated LTL formulas for satisfiability and extract traces / words fulfilling the formula if satisfiable. I have come across behavior which I do not understand and am therefore asking on this list about it. I would be very happy if you could help me with the issue. I'm using the python interface and call some_formula.translate().accepting_run() which usually either returns None if unsatisfiable or a valid trace, which I then convert using spot.twa_word() and inspect afterwards. Most of the time, this works as expected, but I've experienced several cases now where the produced trace contains a False (0) literal. Here, two cases must be distinguished: 1. The formula is satisfiable There exist formulas like "!b & e U (a & b & c)" which are quite obviously satisfiable, but still accepting_run() returns a trace with 0 in it, although there are other valid traces without False in them. 2. The formula is unsatisfiable There also exist formulas like "X!c & X(b & c & d & a U e)" which are unsatisfiable, and accepting_run() returns a trace with 0 in it. Normally, for unsatisfiable formulas (like "a & !a") it just returns None. I'd find point 2 alone totally okay, but I think point 1 is actually problematic since the trace I'm looking for exists, but isn't returned. So my question is whether I'm using spot incorrectly somehow or if this is actually a bug. I also attached a small list of formulas and traces with the described behavior. BTW I'm on Linux, Ubuntu 16.04, using spot 2.8.7 compiled from the tar.gz. I'm looking forward to your responses! Regards, Jens Kreber

2 2

Re: [Spot] Site is not responding
by Alexandre Duret-Lutz 27 Feb '20

27 Feb '20

On Thu, Feb 27, 2020 at 10:33 AM Ranjana N <ranjana.nallamalli(a)gmail.com> wrote: > > The following website: > > spot.lrde.epita.fr Thanks. Our sysadmin said he banned all non-french IPs two days ago because of a DDOS attack that would fill the ram of our shared web server in just 1sec. Unfortunately he had no time yesterday to work on this. He tried to lift the ban a few minutes ago, and the server went down in a couple of seconds again. He is currently trying to look for a smaller range of IPs to block. -- Alexandre Duret-Lutz

2 2

Disable doc generation
by Jaime Arias 27 Feb '20

27 Feb '20

Dear all, I was wondering if there exists an option to disable the generation of the documentation. Thank you in advance, Best, Jaime -- -------------------------------------------------------------- Jaime Arias https://lipn.univ-paris13.fr/~arias CNRS Research Engineer (LoVe Team) LIPN, CNRS UMR 7030 Institut Galilée - Université Paris 13 99 Avenue Jean-Baptiste Clément, F-93430 Villetaneuse, France tel:[+33] 01 49 40 40 67 --------------------------------------------------------------

2 2

Site is not responding
by Ranjana N 27 Feb '20

27 Feb '20

Have been trying to access the resources at your website but not getting through. Is the site down? Kindly throw some light. Thanks & Regards Ranjana New Delhi

2 1

Python Binding Issue
by Yoonchang Sung 26 Feb '20

26 Feb '20

To whom it may concern, I am having Ubuntu 16.04 and my python3 version is 3.5.2 (default version from Ubuntu 16.04). After installing with the default configuration setting (installing from a tarball), I am able to import spot in python3 but "print(spot.version())" gives me this error: "AttributeError: module 'spot' has no attribute 'version'". Also, when trying "sudo apt-get install python3-spot", I am getting this error: "The following packages have unmet dependencies: python3-spot : Depends: python3 (>= 3.7~) but 3.5.1-3 is to be installed E: Unable to correct problems, you have held broken packages." I was wondering if you could help me with this issue. Thank you! Best, Yoon -- *Yoonchang Sung* Postdoctoral Associate Massachusetts Institute of Technology Computer Science and Artificial Intelligence Laboratory 32 Vassar St. / Room 32-335 Cambridge, MA 02139 USA

2 1

Bug in version 2.8.6
by Rowe, Reuben 26 Feb '20

26 Feb '20

Hi Spot Team, I am trying to compile Cyclist (cyclist-prover.org) against the latest version (2.8.6) of Spot, and I am getting an error. Cyclist is including spot/twa/twa.hh, and when compiling I get the following error: In file included from /home/cim/staff/uhac003/Academic/Resources/Spot/spot-2.8.6/install/include/spot/twa/acc.hh:28:0, from /home/cim/staff/uhac003/Academic/Resources/Spot/spot-2.8.6/install/include/spot/twa/twa.hh:27, from src/soundness/proof_aut.hpp:4, from src/soundness/proof_aut.c:1: /home/cim/staff/uhac003/Academic/Resources/Spot/spot-2.8.6/install/include/spot/misc/bitset.hh: In constructor ‘spot::bitset<N>::bitset(spot::bitset<N>::word_t)’: /home/cim/staff/uhac003/Academic/Resources/Spot/spot-2.8.6/install/include/spot/misc/bitset.hh:57:5: error: constexpr constructor does not have empty body } ^ In fact, I also get this error when trying to compile again versions 2.6.3 and 2.7.5 too. When I try to compile against version 2.5.3, I get the error that there is no such file spot/twa/twa.hh. Is this a bug, or has the API changed? If the latter, how should I update my code to use the newer versions? Thanks, Reuben -- Lecturer, Dept of Computer Science Royal Holloway, University of London Egham Surrey TW20 0EX Tel: +44 (0)1784 276827

2 1

Random formulas that cannot be converted to automaton
by Carlo Sengers 15 Dec '19

15 Dec '19

Dear Team, I am conducting an experiment to determine the performance/capacity of atomic propositions that SPOT can handle when an intersecting run is requested from a Buchi automaton and an LTL formula. The experiment uses standard SPOT functionality: The command line utility 'Randaut' and 'RandLtl'. Finally, I have been able to obtain the desired output and have no obstacles anymore. However, during the setup of the experiment, I observed that at least two random generated formulas resulted in an error: 1. a C++ program I made, eventually resulted in error: " terminate called after throwing an instance of 'std::bad_alloc' what(): std::bad_alloc" 2. The online translator at https://spot.lrde.epita.fr/app/ presented a timeout with the same formula. 3. The spot-sandbox automata notebook at https://spot-sandbox.lrde.epita.fr/notebooks/examples%20(read%20only)/autom… Presented the error: Kernel Restarting. The kernel appears to have died. It will restart automatically. There is no specific use for the specific formulas, so I removed those from the experiment. I successfully ran the remaining batches. The annoying part: It was not immediately obvious that my program actually froze due to a 'questionable' formula instead of doing some heavy lifiting on huge automatons. resulting in some useless waiting time. I am not aware if there is a way to determine upfront whether there such a formula will exist in a set. I did not investigate if the likelihood can be reduced by manipulating a specific operator priority (option of randltl). There are too few formulas that exbibit this behavior. Question: Are such formulas a natural aspect of LTL of is this maybe a bug? Is it an option to avoid or reduce the likelihood of occurrence of such formulas in RandLTL? (making it less random :-) ) The affected formulas were: 1. G((p0) & (((p15) <-> ((G((p5) & (((p14) xor (G(p2))) <-> (G(X(p1)))))) U ((G(p8)) M (p7)))) -> ((p12) M (p6)))) 2. (((G((F(p5)) <-> (G(p7)))) & ((p8) <-> (F(p9)))) xor ((!(p0)) U (p1))) M ((X(p5)) & (F(p4))) Kind regards Carlo Sengers Master Student Software Engineering

2 2

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