From 9313222e9532e51e7746d6b0ed72cf33f2a9a7e3 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Mon, 14 Dec 2015 11:51:57 +0100 Subject: [PATCH] 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/tut21.org: Add the Python version. * doc/org/tut.org: Move tut21.org to the Python/C++ section. * NEWS: Update. --- NEWS | 4 ++ doc/org/tut.org | 7 +-- doc/org/tut21.org | 130 ++++++++++++++++++++++++++++++++++++++-- spot/twa/twagraph.hh | 14 +++-- wrap/python/spot_impl.i | 9 +++ 5 files changed, 151 insertions(+), 13 deletions(-) diff --git a/NEWS b/NEWS index 643e67e52..077daedae 100644 --- a/NEWS +++ b/NEWS @@ -35,6 +35,10 @@ New in spot 1.99.6a (not yet released) 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. + Documentation: * There is a new page explaining how to compile example programs and diff --git a/doc/org/tut.org b/doc/org/tut.org index 19ef37ef7..21cd90600 100644 --- a/doc/org/tut.org +++ b/doc/org/tut.org @@ -5,7 +5,7 @@ This section contains code examples for using Spot. This is a work in -progress. Feel free to [[mailto:spot@lrde.epita.fr][send]] suggestion of small tasks you would like +progress. Feel free to [[mailto:spot@lrde.epita.fr][send]] suggestions of small tasks you would like to see illustrated here. If you have difficulties compiling the C++ examples, check out [[file:compile.org][these @@ -25,14 +25,13 @@ three interfaces supported by Spot: shell commands, Python, or C++. * Examples in Python and C++ - [[file:tut03.org][Constructing and transforming formulas]] +- [[file:tut21.org][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. -- [[file:tut21.org][Custom print of an automaton]] - [[file:tut22.org][Creating an automaton in C++]] * Examples in Python only diff --git a/doc/org/tut21.org b/doc/org/tut21.org index 4b114f27a..6bb55b0f5 100644 --- a/doc/org/tut21.org +++ b/doc/org/tut21.org @@ -3,10 +3,23 @@ #+SETUPFILE: setup.org #+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 --END-- #+END_SRC +* C++ + We now write some C++ to load this automaton [[file:tut20.org][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 = {} #+end_example +* 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='') + print() + # 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(), + aut.prop_stutter_sensitive())) + + 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) + + + custom_print(spot.automaton("tut21.hoa")) +#+END_SRC + +#+RESULTS: +#+begin_example +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 = {} +#+end_example + #+BEGIN_SRC sh :results silent :exports results rm -f tut21.hoa diff --git a/spot/twa/twagraph.hh b/spot/twa/twagraph.hh index a00705be6..cb486ada2 100644 --- a/spot/twa/twagraph.hh +++ b/spot/twa/twagraph.hh @@ -173,6 +173,12 @@ namespace spot public: typedef digraph 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::value, + "type mismatch"); protected: 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 set_init_state(state_number(s)); } - graph_t::state get_init_state_number() const + state_num get_init_state_number() const { if (num_states() == 0) const_cast(g_).new_state(); @@ -290,7 +296,7 @@ namespace spot return new twa_graph_succ_iterator(&g_, s->succ); } - graph_t::state + state_num state_number(const state* st) const { auto s = down_cast(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); } diff --git a/wrap/python/spot_impl.i b/wrap/python/spot_impl.i index cbf9b72d1..ef03bb214 100644 --- a/wrap/python/spot_impl.i +++ b/wrap/python/spot_impl.i @@ -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__() {