hi!
With the aid of SPOT I am developing a counter-example guided synthesizer
in python. See [1] if interested for details.
My question is:
I am trying to parse twa_run in python,
namely, parse the labels of the each step (`spot.impl.step`).
Is there a python way to walk through BDD?
(The label is a simple cube expressed in BDD, and I need to convert it into
my internal structure)
(yes, this is rather a question about python interface for buddy)
(no, that is not feature request:) if not possible, I will simply print the
label and parse the string, that is not crucial)
[1]
The idea is
- guess the model,
- then model check it and get a counter-example
- then encode the counter-example into the "guesser" (which uses an SMT
solver)
thanks,
Ayrat
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
Dear Spot Fans,
It is frustrating that I encountered some problems when using ltlcross. I have implemented a tool to get BA from LTL formula. Then I want to use ltlcross to compare spot with my tools. When I ran the ltlcross, I got the following result：//failed to create lcr-o0-fdbDS4
Besides, I tried the following and still failed：//failed to create lcr-o0-kSl51L
I sincerely hope you can help to see my question I would appreciate it if I could get some guidance on the use of ltlcross from you. Looking forward to your reply!
Best Regards!
Shengping Shaw, ECNU
