Hello,

I have noticed two types of errors that seem to occur when telling ltl2tgba to output unambiguous Büchi automata (UBA).

One seems to be some kind of assertion triggering and happens only in combination with the flag „—low“. That is,

on running:

ltl2tgba —low -U -B -f $FRML

the tool occasionally exits with exit code 2 and:

„ltl2tgba: print_hoa(): automaton has transition-based acceptance despite prop_state_acc()==true“

This happens for example for the formula:

(G(!(G("2")))) & (("1") | (F("2")))

In some cases the UBA generated by ltl2tgba seem to be incorrect as well, and I don’t think this has to do with the „—low“

flag. An example formula is

(("2") W (G("1"))) -> (G("1"))

To reproduce these behaviors you can run ltlcross on the attached file „error“, as follows:

cat error | ltlcross —-lbt-input ‚ltl2tgba -U -B —-low -f %f >%O' 'ltl2tgba -f %f >%O'

Best regards,

Simon