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
Dear Spot developers,
Attached is an automaton accepting an empty language. I think it is
supposed to be unambiguous. But when I ran the following command, I
got 0.
autfilt --count --is-unambiguous empty.hoa
After tracing the code, I found that the problem might be caused by
get_init_state_number (called in the product function), which creates
a new state if the input automaton has no state.
--
Ming-Hsien
