January 2016 - Spot

Acceptance check in Spot
by Matthias Heizmann 14 Mar '16

14 Mar '16

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

2 3

Creating bdds
by Miriam Blank 10 Jan '16

10 Jan '16

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

2 5

Parsing HOA using Python
by Marcel Walter 10 Jan '16

10 Jan '16

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

2 2