Hi Spot developers,
I just extended our automata library
https://ultimate.informatik.uni-freiburg.de/?ui=int&tool=automata_script_in…
with support to write Büchi automata in the HOA format.
Now, I just wanted to check a few results without implementing
support to read HOA files.
Syntactically my files seem to be correct, (example attached, file
is read by Spot), but I also wanted to do some semantic check,
e.g., test if a certain word is accepted.
Spot provides quite a number of sophisticated operations but I did not
find something "simple" like an acceptance check.
Have I overlooked it or is it not documented?
For my purpose it is sufficient if it works on the "usual" Büchi automata.
Best,
Matthias
Hi,
Can you please explain the api for creating a bdd?
How can I create a bdd?
How do I define it?
How do I give parameter names so that I can later use it to model check a
formula?
What is the meaning of bdd_ithvar and bdd_nithvar and the int parameter
they receive?
I would be very happy if you can supply a simple example.
Thank you very much and happy new year,
Miriam
Hi all,
I am a masters student of computer science at University of Bremen,
Germany. I am working with Büchi-Automata for a study at the moment.
Therefore I want to parse an HOA file representing a Büchi-Automaton
using Python. It would be great to get an object in Python representing
the automaton. So that I can iterate over the states and their edges,
read the labels, etc.
Can this be done using Spot? If so, how? It would be nice to have a code
example.
Thank you so much for your help!
Best regards from Germany,
Marcel Walter
