Commit 9313222e authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz

python: allow iterating over the successors of a state

Fixes #118.

* spot/twa/twagraph.hh: Avoid using graph_t::state to help Swig.
* wrap/python/spot_impl.i: Add a __str__ function for acc_cond::mark_t.
* doc/org/ Add the Python version.
* doc/org/ Move to the Python/C++ section.
* NEWS: Update.
parent 4b853865
......@@ -35,6 +35,10 @@ New in spot 1.99.6a (not yet released)
* Iterating over the transitions leaving a state (the
twa_graph::out() C++ function) is now possible in Python. See for a demonstration.
* There is a new page explaining how to compile example programs and
......@@ -5,7 +5,7 @@
This section contains code examples for using Spot. This is a work in
progress. Feel free to [[][send]] suggestion of small tasks you would like
progress. Feel free to [[][send]] suggestions of small tasks you would like
to see illustrated here.
If you have difficulties compiling the C++ examples, check out [[][these
......@@ -25,14 +25,13 @@ three interfaces supported by Spot: shell commands, Python, or C++.
* Examples in Python and C++
- [[][Constructing and transforming formulas]]
- [[][Custom print of an automaton]]
* Examples in
C++ only
* Examples in C++ only
The following examples are too low-level to be implemented in shell or
Python (at least at the moment), so they are purely C++ so far.
- [[][Custom print of an automaton]]
- [[][Creating an automaton in C++]]
* Examples in Python only
......@@ -3,10 +3,23 @@
#+HTML_LINK_UP: tut.html
This example demonstrates how to iterate over an automaton. We will
only show how to do this in C++: the Python bindings for the automata
are not yet supporting these low-level iterations, and the shell
commands aren't up to the task either.
This example demonstrates how to iterate over an automaton in C++ and
Python. This case uses automata stored entirely in memory as a graph:
states are numbered by integers, and transitions can be seen as tuple
of the form
$(\mathit{src},\mathit{dst},\mathit{cond},\mathit{accsets})$ where
$\mathit{src}$ and $\mathit{dst}$ are integer denoting the extremities
of the transition, $\mathit{cond}$ is a BDD representing the label
(a.k.a. guard), and $\mathit{accsets}$ is an object of type
=acc_cond::mark_t= encoding the membership to each acceptance sets
(=acc_cond::mark_t= is basically a bit vector).
The interface available for those graph-based automata allows random
access to any state of the graph, hence the code given bellow can do a
simple loop over all states of the automaton. Spot also supports a
different kind of interface (not demonstrated here) to iterate over
automata that are constructed on-the-fly and where such a loop would
be impossible.
First let's create an example automaton in HOA format.
......@@ -42,9 +55,11 @@ State: 3
* C++
We now write some C++ to load this automaton [[][as we did before]], and in
=custom_print()= we print it out in a custom way by explicitly
iterating over it states and edges.
iterating over its states and edges.
The only tricky part is to print the edge labels. Since they are
BDDs, printing them directly would just show the identifiers of BDDs
......@@ -201,6 +216,111 @@ State 3:
acc sets = {}
* Python
Here is the very same example, but written in Python:
#+BEGIN_SRC python :results output :exports both
import spot
def maybe_yes(pos, neg=False):
if neg:
return "no"
return "yes" if pos else "maybe"
def custom_print(aut):
bdict = aut.get_dict()
print("Acceptance:", aut.get_acceptance())
print("Number of sets:", aut.num_sets())
print("Number of states: ", aut.num_states())
print("Initial states: ", aut.get_init_state_number())
print("Atomic propositions:", end='')
for ap in aut.ap():
print(' ', ap, ' (=', bdict.varnum(ap), ')', sep='', end='')
# Templated methods are not available in Python, so we cannot
# retrieve/attach arbitrary objects from/to the automaton. However the
# Python bindings have get_name() and set_name() to access the
# "automaton-name" property.
name = aut.get_name()
if name:
print("Name: ", name)
print("Deterministic:", maybe_yes(aut.prop_deterministic()))
print("Unambiguous:", maybe_yes(aut.prop_unambiguous()))
print("State-Based Acc:", maybe_yes(aut.prop_state_acc()))
print("Terminal:", maybe_yes(aut.prop_terminal()))
print("Weak:", maybe_yes(aut.prop_weak()))
print("Inherently Weak:", maybe_yes(aut.prop_inherently_weak()))
print("Stutter Invariant:", maybe_yes(aut.prop_stutter_invariant(),
for s in range(0, aut.num_states()):
print("State {}:".format(s))
for t in aut.out(s):
print(" edge({} -> {})".format(t.src, t.dst))
# bdd_print_formula() is designed to print on a std::ostream, and
# is inconveniant to use in Python. Instead we use
# bdd_format_formula() as this simply returns a string.
print(" label =", spot.bdd_format_formula(bdict, t.cond))
print(" acc sets =", t.acc)
Acceptance: Inf(0)&Inf(1)
Number of sets: 2
Number of states: 4
Initial states: 0
Atomic propositions: a (=0) b (=1) c (=2)
Name: Fa | G(Fb & Fc)
Deterministic: maybe
Unambiguous: yes
State-Based Acc: maybe
Terminal: maybe
Weak: maybe
Inherently Weak: maybe
Stutter Invariant: yes
State 0:
edge(0 -> 1)
label = a
acc sets = {}
edge(0 -> 2)
label = !a
acc sets = {}
edge(0 -> 3)
label = !a
acc sets = {}
State 1:
edge(1 -> 1)
label = 1
acc sets = {0,1}
State 2:
edge(2 -> 1)
label = a
acc sets = {}
edge(2 -> 2)
label = !a
acc sets = {}
State 3:
edge(3 -> 3)
label = !a & b & c
acc sets = {0,1}
edge(3 -> 3)
label = !a & !b & c
acc sets = {1}
edge(3 -> 3)
label = !a & b & !c
acc sets = {0}
edge(3 -> 3)
label = !a & !b & !c
acc sets = {}
#+BEGIN_SRC sh :results silent :exports results
rm -f tut21.hoa
......@@ -173,6 +173,12 @@ namespace spot
typedef digraph<twa_graph_state, twa_graph_edge_data> graph_t;
typedef graph_t::edge_storage_t edge_storage_t;
// We avoid using graph_t::state because graph_t is not
// instantiated in the SWIG bindings, and SWIG would therefore
// handle graph_t::state as an abstract type.
typedef unsigned state_num;
static_assert(std::is_same<typename graph_t::state, state_num>::value,
"type mismatch");
graph_t g_;
......@@ -247,7 +253,7 @@ namespace spot
return g_.num_edges();
void set_init_state(graph_t::state s)
void set_init_state(state_num s)
assert(s < num_states());
init_number_ = s;
......@@ -258,7 +264,7 @@ namespace spot
graph_t::state get_init_state_number() const
state_num get_init_state_number() const
if (num_states() == 0)
......@@ -290,7 +296,7 @@ namespace spot
return new twa_graph_succ_iterator<graph_t>(&g_, s->succ);
state_number(const state* st) const
auto s = down_cast<const typename graph_t::state_storage_t*>(st);
......@@ -299,7 +305,7 @@ namespace spot
const twa_graph_state*
state_from_number(graph_t::state n) const
state_from_number(state_num n) const
return &g_.state_data(n);
......@@ -476,6 +476,15 @@ namespace std {
%extend spot::acc_cond::mark_t {
std::string __str__()
std::ostringstream os;
os << *self;
return os.str();
%extend spot::twa_run {
std::string __str__()
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment