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
Hi Vincenzo,
(Sorry for the delay, I just found your email in the middle of hundreds of spams that were waiting to be moderated...)
Vincenzo Tramo vv.tramo@gmail.com writes:
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)))
The above looks like an LTL formula generated from LTLf, so a deterministic BA will always exist for that. Building this DBA is reasonably fast:
% ltl2tgba -D -F input1.ltl --stats="%s st., %e ed., %r sec." 381 st., 7269 ed., 0.67422 sec.
If I drop option -D, it becomes slow because Spot will try to simplify the non-deterministic Büchi automaton using simulation-based reductions. I've found that if we activate only direct-simulation, the translation is efficient:
% ltl2tgba -x simul=1 -F input1.ltl --stats="%s st., %e ed., %r sec." 395 st., 6290 ed., 0.601192 sec.
However, the reverse simulation is very slow: with ~390 equivalence classes and some state having a up to 250 incoming edges, building the BDD signature of some of these states is very expensive, and BuDDy spends a lot of time running its garbage collector and allocating more memory. At this point, it's not clear to me how we could improve that.
Switching to the matrix-based implementation of simulation-based reduction was successful too, but the size reduction is inferior:
% ltl2tgba -x simul-method=2 -F input1.ltl --stats="%s st., %e ed., %r sec." 420 st., 6356 ed., 1.2033 sec.
I've created an issue to track any progress on that https://gitlab.lre.epita.fr/spot/spot/-/issues/599
INPUT 2
That second formula has 80 atomic propositions and looks highly random to me. Since we are dealing with algorithms that have 2^AP worst cases, do we have any to reason to believe it show be translated efficiently?
Alexandre
-
Alexandre Duret-Lutz -
Vincenzo Tramo