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
Hi Marcel,
On Sun, Jan 10, 2016 at 4:38 PM, Marcel Walter cavani@informatik.uni-bremen.de wrote:
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.
Python bindings for iterating over the structure of an automaton do not exist in version 1.99.6, but they will be in the next one, which I hope to release by the end of next week.
If you want to play with the current development version, download it from here: http://teamcity.lrde.epita.fr/viewLog.html?buildTypeId=bt16&buildId=last... or install the "unstable" Debian packages.
The NEWS file for the next release currently contains the following bits about Python:
| * Iterating over the transitions leaving a state (the | twa_graph::out() C++ function) is now possible in Python. | See https://spot.lrde.epita.fr/tut21.html for a demonstration. | | * Membership to acceptance sets can be specified using Python list | when calling for instance the Python version of twa_graph::new_edge(). | See https://spot.lrde.epita.fr/tut22.html for a demonstration. | | * Automaton states can be named via the set_state_names() method. | See https://spot.lrde.epita.fr/ipynb/product.html for an example.
The first two links show how to iterate over and how to create an automaton. The third one implements the product of two automata in Python.
However the above URLs will only contain the expected Python examples once 1.99.7 is released. In the meantime, replace spot.lrde.epita.fr by spot-dev.lrde.epita.fr to access the upcoming version of documentation. (I try to avoid posting direct links to spot-dev so that search engines only point to the main version.)
Hey Alexandre,
Just wow! Thank you so much for the quick and helpful response! I will look forward for the next release and I am going to play around a little with the unstable version in the meantime.
Again thank you so much!
Best regards, Marcel
Am 10.01.2016 20:26 schrieb Alexandre Duret-Lutz adl@lrde.epita.fr:
Hi Marcel,
On Sun, Jan 10, 2016 at 4:38 PM, Marcel Walter cavani@informatik.uni-bremen.de wrote:
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.
Python bindings for iterating over the structure of an automaton do not exist in version 1.99.6, but they will be in the next one, which I hope to release by the end of next week.
If you want to play with the current development version, download it from here: http://teamcity.lrde.epita.fr/viewLog.html?buildTypeId=bt16&buildId=last... or install the "unstable" Debian packages.
The NEWS file for the next release currently contains the following bits about Python:
| * Iterating over the transitions leaving a state (the | twa_graph::out() C++ function) is now possible in Python. | See https://spot.lrde.epita.fr/tut21.html for a demonstration. | | * Membership to acceptance sets can be specified using Python list | when calling for instance the Python version of twa_graph::new_edge(). | See https://spot.lrde.epita.fr/tut22.html for a demonstration. | | * Automaton states can be named via the set_state_names() method. | See https://spot.lrde.epita.fr/ipynb/product.html for an example.
The first two links show how to iterate over and how to create an automaton. The third one implements the product of two automata in Python.
However the above URLs will only contain the expected Python examples once 1.99.7 is released. In the meantime, replace spot.lrde.epita.fr by spot-dev.lrde.epita.fr to access the upcoming version of documentation. (I try to avoid posting direct links to spot-dev so that search engines only point to the main version.)
-- Alexandre Duret-Lutz
-
Alexandre Duret-Lutz -
Marcel Walter