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