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
Good afternoon,
You are probably already aware of that, but the spot online translator is
not working anymore. I am trying to translate a LTL formula into a Buchi
Automaton. It was working until 2 days ago, but now i get this:
Traceback (most recent call last):
File "/var/www/html/cgi-bin/spotcgi.py", line 732, in <module>
render_automaton(degen, dont_run_dot)
File "/var/www/html/cgi-bin/spotcgi.py", line 318, in render_automaton
render_dot_maybe(dotsrc.str(), dont_run_dot, hoaname)
File "/var/www/html/cgi-bin/spotcgi.py", line 305, in render_dot_maybe
render_dot(autprefix, hoaname)
File "/var/www/html/cgi-bin/spotcgi.py", line 237, in render_dot
run_dot(basename, 'svg')
File "/var/www/html/cgi-bin/spotcgi.py", line 230, in run_dot
os.link(outname, tmpdir + "/" + ext)
FileNotFoundError: [Errno 2] No such file or directory:
'../spotimg/960f234ef7d2cd7d8fbab23c49603c6a66fc284d.svg' ->
'../spotimg/0f33f8af71a0356e3d63971bc8a4a7e39e64b7d9-154/svg'
Any fix to the problem?
Thank you!
Kind Regards,
Matteo Lucchi
Hello,
first I just want to say, thanks for creating Spot, it is immensely
useful! And I think that I might have found a bug (or two).
My inputs are classic state-based NBAs. I rely on Spot to compare and
verify my determinized automata, i.e. I compare the automaton that my
tool produces with the one I get from Spot using autfilt -D -S -p (to
get a deterministic parity automaton). I use autfilt --equivalent-to=...
for the equivalence test.
Yesterday I noticed something strange. When I compare the original NBA
and my DPA, it reports that they are equivalent. Same for the original
NBA and the DPA I get from Spot. But when I compare my automaton with
the one from Spot, it says that the languages are different! So the
first thought was - something must be broken in the equivalence test.
Apparently, at least one of the three answers I got is wrong. So I used
a little Python script using the Spot API to get a word where two of the
automata do not agree on. Let's call the original NBA A, my DPA B and
the one from Spot C.
There were no words found in A׬B, ¬A×B, A׬C, ¬A×C and also B׬C.
But there IS a word in ¬B×C.
I used this word with autfilt --accept-word=... to check A, B and C. And
it turned out that in fact A and B do not accept the word, but C does,
i.e. C is incorrect.
So, to conclude, there seems to be a bug in the determinization and the
problem is not detected by the equivalence test between A and C.
I don't know about Spot internals, but if the equivalence test is using
the same determinization procedure to complement A for the required
products, then the bug in the equivalence test is a consequence of the
problem in the determinization (i.e., the equiv. test compares the wrong
DPA with basically itself), so the issues might be related.
It might be useful to know that I found the problem using Spot 2.4.4 and
it is still present in the current version 2.5.1. I also attach the
smallest automata A, B and C that illustrate the issue and the script I
used to search for the counterexample.
You can check that:
cat aut_a.hoa | autfilt --accept-word='cycle{!p;p}' -c returns 0
and
autfilt -D -S -p aut_a.hoa | autfilt --accept-word='cycle{!p;p}' -c
returns 1.
I hope this helps.
Thanks and best regards,
Anton Pirogov
