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)/automata.ipynb
   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