14 Dec
2019
14 Dec
'19
3:52 p.m.
Dear Team,
I am conducting an experiment to determine the performance/capacity of
atomic propositions that SPOT can handle when an intersecting run is
requested from a Buchi automaton and an LTL formula.
The experiment uses standard SPOT functionality: The command line utility
'Randaut' and 'RandLtl'.
Finally, I have been able to obtain the desired output and have no
obstacles anymore.
However, during the setup of the experiment, I observed that at least two
random generated formulas resulted in an error:
1. a C++ program I made, eventually resulted in error: " terminate
called after throwing an instance of 'std::bad_alloc' what():
std::bad_alloc"
2. The online translator at https://spot.lrde.epita.fr/app/ presented a
timeout with the same formula.
3. The spot-sandbox automata notebook at
https://spot-sandbox.lrde.epita.fr/notebooks/examples%20(read%20only)/autom…
Presented the error: Kernel Restarting. The kernel appears to have
died. It will restart automatically.
There is no specific use for the specific formulas, so I removed those from
the experiment. I successfully ran the remaining batches.
The annoying part: It was not immediately obvious that my program
actually froze due to a 'questionable' formula instead of doing some
heavy lifiting on huge automatons. resulting in some useless waiting time.
I am not aware if there is a way to determine upfront whether there such a
formula will exist in a set.
I did not investigate if the likelihood can be reduced by manipulating a
specific operator priority (option of randltl). There are too few formulas
that exbibit this behavior.
Question:
Are such formulas a natural aspect of LTL of is this maybe a bug?
Is it an option to avoid or reduce the likelihood of occurrence of such
formulas in RandLTL? (making it less random :-) )
The affected formulas were:
1. G((p0) & (((p15) <-> ((G((p5) & (((p14) xor (G(p2))) <->
(G(X(p1)))))) U ((G(p8)) M (p7)))) -> ((p12) M (p6))))
2. (((G((F(p5)) <-> (G(p7)))) & ((p8) <-> (F(p9)))) xor ((!(p0)) U
(p1))) M ((X(p5)) & (F(p4)))
Kind regards
Carlo Sengers
Master Student Software Engineering
15 Dec
15 Dec
10:03 a.m.
Hi Carlo,
On Sun, Dec 15, 2019 at 8:30 AM Carlo Sengers <cejm.sengers(a)studie.ou.nl> wrote:
However, during the setup of the experiment, I
observed that at least two random generated formulas resulted in an error:
a C++ program I made, eventually resulted in error: " terminate called after
throwing an instance of 'std::bad_alloc' what(): std::bad_alloc"
The online translator at https://spot.lrde.epita.fr/app/ presented a timeout with the
same formula.
The spot-sandbox automata notebook at
https://spot-sandbox.lrde.epita.fr/notebooks/examples%20(read%20only)/autom…
Presented the error: Kernel Restarting. The kernel appears to have died. It will restart
automatically.
All these are symptoms of the same issue : out of memory (or timeout)
during the simplification of the automaton.
I managed to translate the second of your formulas on my laptop (and
get a 63-state automaton), but the first one failed for the same
reason.
The annoying part: It was not immediately obvious that
my program actually froze due to a 'questionable' formula instead of doing some
heavy lifiting on huge automatons. resulting in some useless waiting time.
It's not clear to me what is the distinction you make here. The
formulas are problematic because their translation involve huge
automata.
Translating an LTL formula into a TGBA or BA can involve an
exponential blowup in the size of the formula (it's exponential in the
number of subformulas, and exponential in the number of atomic
propositions).
Simplifiying the resulting automata also involves some algorithms that
are exponential in the size of the automata. So that's doubly
exponential by default. Usually, none of this matters because
formulas used in practice are small and yield small automata.
If your goal is to obtain any automaton from the LTL formula, and not
necessarily a small automaton, you can translate the formula with
"ltl2tgba --low" (or call trans.set_level(spot::postprocessor::Low) in
C++). This will skip the simplifications, getting you a
single-exponential worst case. With this setting, I get 390 states
for the first formula and 67 for the second.
Are such formulas a natural aspect of LTL of is this
maybe a bug?
It's natural to find doubly-exponential worst cases with the
simplifications used in Spot.
Is it an option to avoid or reduce the likelihood of
occurrence of such formulas in RandLTL? (making it less random :-) )
Reduce the size of your formulas or the number of atomic propositions
used. Or disable automaton simplifications.
Anyway thanks for reporting your issues. I'll look at the behavior of
the culprit algorithm on your first formula, and see if anything can
be improved. Its memory consumption was already improved last year,
but maybe that can be improved again.
https://gitlab.lrde.epita.fr/spot/spot/issues/395
Best regards,
--
Alexandre Duret-Lutz
1:18 p.m.
Hi Alexander,
Thank you for your prompt reply.
Currently, any automaton will suffice for my test, so I applied your
suggestion on skipping the simplifications and that works like a charm.
This makes my program more robust for future use.
Actually, the second formula timed-out when trying to translate the negated
formula. Sorry, I did not explicitly mention that in the text, only
implicit in the attachment.
The root cause remains the same as with the first case.
I will include a user instruction, for future users of my program, on
formula sizing and number of ap's.
Thanks again.
Kind regards
Carlo Sengers
Op zo 15 dec. 2019 om 10:04 schreef Alexandre Duret-Lutz <adl(a)lrde.epita.fr
:
Hi Carlo,
On Sun, Dec 15, 2019 at 8:30 AM Carlo Sengers <cejm.sengers(a)studie.ou.nl>
wrote:
--
Met vriendelijke groet
Carlo Sengers
However, during the setup of the experiment, I
observed that at least
two random generated formulas resulted in an error:
a C++ program I made, eventually resulted in error: " terminate called
after
throwing an instance of 'std::bad_alloc' what(): std::bad_alloc"
The online translator at
https://spot.lrde.epita.fr/app/ presented a
timeout with the same formula.
The spot-sandbox automata notebook at
https://spot-sandbox.lrde.epita.fr/notebooks/examples%20(read%20only)/autom…
Presented the error: Kernel Restarting. The
kernel appears to have
died. It will restart automatically.
All these are symptoms of the same issue : out of memory (or timeout)
during the simplification of the automaton.
I managed to translate the second of your formulas on my laptop (and
get a 63-state automaton), but the first one failed for the same
reason.
The annoying part: It was not immediately obvious
that my program
actually froze due to a 'questionable' formula instead
of doing some
heavy lifiting on huge automatons. resulting in some useless waiting time.
It's not clear to me what is the distinction you make here. The
formulas are problematic because their translation involve huge
automata.
Translating an LTL formula into a TGBA or BA can involve an
exponential blowup in the size of the formula (it's exponential in the
number of subformulas, and exponential in the number of atomic
propositions).
Simplifiying the resulting automata also involves some algorithms that
are exponential in the size of the automata. So that's doubly
exponential by default. Usually, none of this matters because
formulas used in practice are small and yield small automata.
If your goal is to obtain any automaton from the LTL formula, and not
necessarily a small automaton, you can translate the formula with
"ltl2tgba --low" (or call trans.set_level(spot::postprocessor::Low) in
C++). This will skip the simplifications, getting you a
single-exponential worst case. With this setting, I get 390 states
for the first formula and 67 for the second.
Are such formulas a natural aspect of LTL of is
this maybe a bug?
It's natural to find doubly-exponential worst cases with the
simplifications used in Spot.
Is it an option to avoid or reduce the likelihood
of occurrence of such
formulas in RandLTL? (making it less random :-) )
Reduce the size of your formulas or the number of atomic propositions
used. Or disable automaton simplifications.
Anyway thanks for reporting your issues. I'll look at the behavior of
the culprit algorithm on your first formula, and see if anything can
be improved. Its memory consumption was already improved last year,
but maybe that can be improved again.
https://gitlab.lrde.epita.fr/spot/spot/issues/395
Best regards,
--
Alexandre Duret-Lutz
1879
days inactive
1880
days old
2 comments
2 participants
participants (2)
-
Alexandre Duret-Lutz -
Carlo Sengers