[Spot] Nondeterministic behavior of ltl2tgba tool

Alexandre Duret-Lutz adl at lrde.epita.fr
Wed Aug 17 17:16:01 CEST 2011


Hi Tomáš!

Thank you for your email.

I noticed such a nondeterministic behavior a couple of months back
when preparing a benchmark with lbtt for a talk [1]: the figures
output by lbtt were not consistent between runs.  But at the time I
was in a rush, I didn't investigate, and then I simply forgot about
it.

I've now looked into it.  It turns out that the degeneralisation
algorithm used a std::map to merge the outgoing transitions sharing
the same destination.  This std::map was then used to output these
transitions.  Unfortunately, the order used to store these transitions
was based on the memory address of the destination state.  The
-r7/-r6/-r5 options seems unrelated (I was puzzled at first, because
they do not reduce the formula you gave) but because of all the
operations they involve (translations, products, emptiness checks)
they probably shake the memory allocator enough to get states at
different addresses in the different runs. I have fixed the
degeneralization as shown here:
http://git.lrde.epita.fr/?p=spot.git;a=commit;h=03aabf9a3afd39eb511cb812b0992edc3eab3a51

Note that this change should only avoid the nondeterminism in the
order of the states and transitions.

The difference in the number of states that you observed might be a
bug in the direct simulation algorithm behind "-R1t -R1q", but I'm not
sure.  Direct (-R1?) and delayed (-R2?) simulations were written
several years ago by a master student who tried to adapt the
game-theory-based algorithms to TGBA. Over the years these algorithms
have proved to be flaky, and I had to demote them into handling only
degeneralized Büchi automata.  Still, I have evidence that -R2?
mishandle some simple degeneralized automata (e.g.: ./ltl2tgba -DS
-R2t -R2q 'FGq' produces an "always true" automaton) and I although I
don't have similar evidence against -R1?, I don't trust this algorithm
either.  That is the reason there are no options for these simulations
on the online translator.
Another student should be working on a new implementation of these
game-theory-based simulations at the beginning of next year.  And
there is also a "bdd-simul" branch on the git repository, where there
is a preliminary implementation of a BDD-based direct simulation
algorithm that works with TGBA (unfortunately it won't work for
delayed simulation).

[1] slide 12/29 of http://www.lrde.epita.fr/~adl/dl/adl/duret.11.sumo.slides.pdf

Best regards,
-- 
Alexandre Duret-Lutz



More information about the Spot mailing list