[Spot] UBA-generation of ltl2tgba

Simon Jantsch simon.jantsch at tu-dresden.de
Fri Feb 1 09:15:39 CET 2019


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,

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.lrde.epita.fr/pipermail/spot/attachments/20190201/1f27869b/attachment.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: error
Type: application/octet-stream
Size: 2382 bytes
Desc: error
URL: <http://lists.lrde.epita.fr/pipermail/spot/attachments/20190201/1f27869b/attachment.obj>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.lrde.epita.fr/pipermail/spot/attachments/20190201/1f27869b/attachment.htm>

More information about the Spot mailing list