From c39d35d0685553b9fadb4413b0942de761607f41 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 15 Dec 2015 19:01:33 +0100 Subject: [PATCH] python: port the tut22.org example to Python * wrap/python/spot_impl.i: Extend acc_cond::mark_t to with a constructor that takes a vector. * doc/org/tut22.org: Add a Python version. * doc/org/tut.org: Adjust the list, we don't have any C++-specific example. * NEWS: Mention it. --- NEWS | 4 +++ doc/org/tut.org | 8 +---- doc/org/tut22.org | 75 ++++++++++++++++++++++++++++++++++++----- wrap/python/spot_impl.i | 10 ++++++ 4 files changed, 82 insertions(+), 15 deletions(-) diff --git a/NEWS b/NEWS index 077daedae..b11ff3322 100644 --- a/NEWS +++ b/NEWS @@ -39,6 +39,10 @@ New in spot 1.99.6a (not yet released) 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. + 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 21cd90600..dc191f031 100644 --- a/doc/org/tut.org +++ b/doc/org/tut.org @@ -26,13 +26,7 @@ three interfaces supported by Spot: shell commands, Python, or C++. - [[file:tut03.org][Constructing and transforming formulas]] - [[file:tut21.org][Custom print of an automaton]] - -* 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:tut22.org][Creating an automaton in C++]] +- [[file:tut22.org][Creating an automaton by adding states and transitions]] * Examples in Python only diff --git a/doc/org/tut22.org b/doc/org/tut22.org index 1413eae30..ac529d7aa 100644 --- a/doc/org/tut22.org +++ b/doc/org/tut22.org @@ -1,9 +1,11 @@ # -*- coding: utf-8 -*- -#+TITLE: Creating an automaton in C++ +#+TITLE: Creating an automaton by adding states and transitions #+SETUPFILE: setup.org #+HTML_LINK_UP: tut.html -This example demonstrates how to create an automaton in C++, and then print it. +This example demonstrates how to create an automaton and then print it. + +* C++ #+BEGIN_SRC C++ :results verbatim :exports both :wrap SRC hoa #include @@ -12,8 +14,8 @@ This example demonstrates how to create an automaton in C++, and then print it. int main(void) { - // The dict is used to maintain the correspondence between the - // atomic propositions and the BDD variables to label the edges of + // The bdd_dict is used to maintain the correspondence between the + // atomic propositions and the BDD variables that label the edges of // the automaton. spot::bdd_dict_ptr dict = spot::make_bdd_dict(); // This creates an empty automaton that we have yet to fill. @@ -31,10 +33,9 @@ This example demonstrates how to create an automaton in C++, and then print it. // States are numbered from 0. aut->new_states(3); - // new_edge() takes 3 mandatory parameters: - // source state, destination state, label - // and a last optional parameter can be used - // to specify membership to acceptance sets. + // new_edge() takes 3 mandatory parameters: source state, + // destination state, and label. A last optional parameter can be + // used to specify membership to acceptance sets. aut->new_edge(0, 1, p1); aut->new_edge(1, 1, p1 & p2, {0}); aut->new_edge(1, 2, p2, {1}); @@ -65,3 +66,61 @@ State: 2 [0 | 1] 1 {0 1} --END-- #+END_SRC + +* Python + +#+BEGIN_SRC python :results output :exports both :wrap SRC hoa + import spot + import buddy + + # The bdd_dict is used to maintain the correspondence between the + # atomic propositions and the BDD variables that label the edges of + # the automaton. + bdict = spot.make_bdd_dict(); + # This creates an empty automaton that we have yet to fill. + aut = spot.make_twa_graph(bdict) + + # Since a BDD is associated to every atomic proposition, the register_ap() + # function returns a BDD variable number that can be converted into a BDD using + # bdd_ithvar() from the BuDDy library. + p1 = buddy.bdd_ithvar(aut.register_ap("p1")) + p2 = buddy.bdd_ithvar(aut.register_ap("p2")) + + # Set the acceptance condition of the automaton to Inf(0)&Inf(1) + aut.set_generalized_buchi(2) + + # States are numbered from 0. + aut.new_states(3) + + # new_edge() takes 3 mandatory parameters: source state, destination state, and + # label. A last optional parameter can be used to specify membership to + # acceptance sets. In the Python version, the list of acceptance sets the + # transition belongs to should be specified as a list. + aut.new_edge(0, 1, p1) + aut.new_edge(1, 1, p1 & p2, [0]) + aut.new_edge(1, 2, p2, [1]); + aut.new_edge(2, 1, p1 | p2, [0, 1]); + + # Print the resulting automaton. + print(aut.to_str('hoa')) +#+END_SRC + +#+RESULTS: +#+BEGIN_SRC hoa +HOA: v1 +States: 3 +Start: 0 +AP: 2 "p1" "p2" +acc-name: generalized-Buchi 2 +Acceptance: 2 Inf(0)&Inf(1) +properties: trans-labels explicit-labels trans-acc +--BODY-- +State: 0 +[0] 1 +State: 1 +[0&1] 1 {0} +[1] 2 {1} +State: 2 +[0 | 1] 1 {0 1} +--END-- +#+END_SRC diff --git a/wrap/python/spot_impl.i b/wrap/python/spot_impl.i index ef03bb214..20385cb84 100644 --- a/wrap/python/spot_impl.i +++ b/wrap/python/spot_impl.i @@ -317,6 +317,7 @@ namespace swig namespace std { %template(liststr) list; %template(vectorformula) vector; + %template(vectorunsigned) vector; %template(atomic_prop_set) set; %template(relabeling_map) map; } @@ -330,6 +331,7 @@ namespace std { %include %include %include +%implicitconv spot::acc_cond::mark_t; %feature("flatnested") spot::acc_cond::mark_t; %feature("flatnested") spot::acc_cond::acc_code; %apply bool* OUTPUT {bool& max, bool& odd}; @@ -439,6 +441,14 @@ namespace std { std::string __str__() { return spot::str_psl(*self); } } +%extend spot::acc_cond::mark_t { + // http://comments.gmane.org/gmane.comp.programming.swig/14822 + mark_t(const std::vector& f) + { + return new spot::acc_cond::mark_t(f.begin(), f.end()); + } +} + %extend spot::twa { void set_name(std::string name) {