- Spot - LRE

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