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
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
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.
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
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!
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
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
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
