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