[Spot] Acceptance check in Spot

Matthias Heizmann heizmann at informatik.uni-freiburg.de
Tue Sep 29 17:09:21 CEST 2015


Hi Spot developers,

I just extended our automata library
https://ultimate.informatik.uni-freiburg.de/?ui=int&tool=automata_script_interpreter&task=automataScript&sample=1954831617
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




-------------- next part --------------
HOA: v1
States: 3
Start: 2
AP: 2 "b" "a"
Acceptance: 1 Inf(0)
acc-name: Buchi
tool: "Ultimate Automata Library"
--BODY--
State: 0 "f" {0}
[0] 0
[1] 1
State: 1 "s"
[0] 1
[1] 1
State: 2 "q"
[0] 0
[0] 2
[1] 2
--END--
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 819 bytes
Desc: This is a digitally signed message part.
URL: <http://lists.lrde.epita.fr/pipermail/spot/attachments/20150929/a545a850/attachment.sig>


More information about the Spot mailing list