
25 Apr
2019
25 Apr
'19
9:14 a.m.
Hi Alexandre, I run the experiments and found two formulas where ltl2tgba did not finish correctly. The formulas were & | G F p0 F G p1 | G F ! p1 F G p2 & & | G F p0 F G p1 | G F ! p1 F G p2 | G F ! p2 F G ! p0 The according command-line was: ltl2tgba -D --generic -C -S --lbt-input -f ${FORMULA} Output was: ltl2tgba: direct_simulation() requires separate Inf and Fin sets Best, David