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
