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
26 Apr
26 Apr
10:01 a.m.
On Fri, Apr 26, 2019 at 8:18 AM David Müller
<david.mueller2(a)tu-dresden.de> wrote:
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
Thanks. I'm looking into this.
You can somehow work around this problem by adding option
-x ba-simul=0
to this line. For historical reason, the name of this option suggests
that it is only for Büchi automata (and as a bonus bug, it's
unfortunately still documented this way), but it's actually
used for any state-based acceptance today.
2147
days inactive
2148
days old
1 comments
2 participants
participants (2)
-
Alexandre Duret-Lutz -
David Müller