From 289b2383ada4ad18521ae59f8250b97c3b5370e3 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Mon, 20 Feb 2017 14:29:25 +0100 Subject: [PATCH] scc_info: add Python bindings Related to #172, where we discussed that scc_info bindings were missing. * spot/twaalgos/sccinfo.hh (spot::scc_info::scc_node): Move... (spot::scc_info_node): ... here to help Swig. * python/spot/impl.i: Add bindings for scc_info. * tests/python/sccinfo.py: New file. * tests/Makefile.am: Add it. --- python/spot/impl.i | 12 +++ spot/twaalgos/sccinfo.hh | 191 ++++++++++++++++++++++----------------- tests/Makefile.am | 1 + tests/python/sccinfo.py | 66 ++++++++++++++ 4 files changed, 187 insertions(+), 83 deletions(-) create mode 100644 tests/python/sccinfo.py diff --git a/python/spot/impl.i b/python/spot/impl.i index 8dfefa14e..87a5de307 100644 --- a/python/spot/impl.i +++ b/python/spot/impl.i @@ -133,6 +133,7 @@ #include #include #include +#include #include #include #include @@ -533,6 +534,9 @@ def state_is_accepting(self, src) -> "bool": %include %include %include +%traits_swigtype(spot::scc_info_node); +%fragment(SWIG_Traits_frag(spot::scc_info_node)); +%include %include %include %include @@ -778,6 +782,14 @@ def state_is_accepting(self, src) -> "bool": throw std::runtime_error ("universal destinations should be explored with univ_dest()"); } + } + +%extend spot::scc_info { + swig::SwigPyIterator* __iter__(PyObject **PYTHON_SELF) + { + return swig::make_forward_iterator(self->begin(), self->begin(), + self->end(), *PYTHON_SELF); + } } %extend spot::acc_cond::acc_code { diff --git a/spot/twaalgos/sccinfo.hh b/spot/twaalgos/sccinfo.hh index 15f4017e8..0ed2f2cf0 100644 --- a/spot/twaalgos/sccinfo.hh +++ b/spot/twaalgos/sccinfo.hh @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2014, 2015, 2016 Laboratoire de Recherche et -// Développement de l'Epita. +// Copyright (C) 2014-2017 Laboratoire de Recherche et Développement +// de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -24,6 +24,79 @@ namespace spot { + + /// Storage for SCC related information. + class SPOT_API scc_info_node + { + public: + typedef std::vector scc_succs; + friend class scc_info; + protected: + scc_succs succ_; + acc_cond::mark_t acc_; + std::vector states_; // States of the component + bool trivial_:1; + bool accepting_:1; // Necessarily accepting + bool rejecting_:1; // Necessarily rejecting + bool useful_:1; + public: + scc_info_node(): + acc_(0U), trivial_(true), accepting_(false), + rejecting_(false), useful_(false) + { + } + + scc_info_node(acc_cond::mark_t acc, bool trivial): + acc_(acc), trivial_(trivial), accepting_(false), + rejecting_(false), useful_(false) + { + } + + bool is_trivial() const + { + return trivial_; + } + + /// \brief True if we are sure that the SCC is accepting + /// + /// Note that both is_accepting() and is_rejecting() may return + /// false if an SCC interesects a mix of Fin and Inf sets. + bool is_accepting() const + { + return accepting_; + } + + // True if we are sure that the SCC is rejecting + /// + /// Note that both is_accepting() and is_rejecting() may return + /// false if an SCC interesects a mix of Fin and Inf sets. + bool is_rejecting() const + { + return rejecting_; + } + + bool is_useful() const + { + return useful_; + } + + acc_cond::mark_t acc_marks() const + { + return acc_; + } + + const std::vector& states() const + { + return states_; + } + + const scc_succs& succ() const + { + return succ_; + } + }; + + /// \brief Compute an SCC map and gather assorted information. /// /// This takes twa_graph as input and compute its SCCs. This @@ -39,75 +112,10 @@ namespace spot class SPOT_API scc_info { public: - typedef std::vector scc_succs; - - class scc_node - { - friend class scc_info; - protected: - scc_succs succ_; - acc_cond::mark_t acc_; - std::vector states_; // States of the component - bool trivial_:1; - bool accepting_:1; // Necessarily accepting - bool rejecting_:1; // Necessarily rejecting - bool useful_:1; - public: - scc_node(): - acc_(0U), trivial_(true), accepting_(false), - rejecting_(false), useful_(false) - { - } - - scc_node(acc_cond::mark_t acc, bool trivial): - acc_(acc), trivial_(trivial), accepting_(false), - rejecting_(false), useful_(false) - { - } - - bool is_trivial() const - { - return trivial_; - } - - /// \brief True if we are sure that the SCC is accepting - /// - /// Note that both is_accepting() and is_rejecting() may return - /// false if an SCC interesects a mix of Fin and Inf sets. - bool is_accepting() const - { - return accepting_; - } - - // True if we are sure that the SCC is rejecting - /// - /// Note that both is_accepting() and is_rejecting() may return - /// false if an SCC interesects a mix of Fin and Inf sets. - bool is_rejecting() const - { - return rejecting_; - } - - bool is_useful() const - { - return useful_; - } - - acc_cond::mark_t acc_marks() const - { - return acc_; - } - - const std::vector& states() const - { - return states_; - } - - const scc_succs& succ() const - { - return succ_; - } - }; + // scc_node used to be an inner class, but Swig 3.0.10 does not + // support that yet. + typedef scc_info_node scc_node; + typedef scc_info_node::scc_succs scc_succs; protected: @@ -146,18 +154,35 @@ namespace spot return sccof_[st]; } - auto begin() const - SPOT_RETURN(node_.begin()); - auto end() const - SPOT_RETURN(node_.end()); - auto cbegin() const - SPOT_RETURN(node_.cbegin()); - auto cend() const - SPOT_RETURN(node_.cend()); - auto rbegin() const - SPOT_RETURN(node_.rbegin()); - auto rend() const - SPOT_RETURN(node_.rend()); + std::vector::const_iterator begin() const + { + return node_.begin(); + } + + std::vector::const_iterator end() const + { + return node_.end(); + } + + std::vector::const_iterator cbegin() const + { + return node_.cbegin(); + } + + std::vector::const_iterator cend() const + { + return node_.cend(); + } + + std::vector::const_reverse_iterator rbegin() const + { + return node_.rbegin(); + } + + std::vector::const_reverse_iterator rend() const + { + return node_.rend(); + } const std::vector& states_of(unsigned scc) const { diff --git a/tests/Makefile.am b/tests/Makefile.am index b8cf1f2ea..5e04bb9c5 100644 --- a/tests/Makefile.am +++ b/tests/Makefile.am @@ -331,6 +331,7 @@ TESTS_python = \ python/alternating.py \ python/bddnqueen.py \ python/bugdet.py \ + python/sccinfo.py \ python/implies.py \ python/interdep.py \ python/ltl2tgba.test \ diff --git a/tests/python/sccinfo.py b/tests/python/sccinfo.py new file mode 100644 index 000000000..38295fc4f --- /dev/null +++ b/tests/python/sccinfo.py @@ -0,0 +1,66 @@ +#!/usr/bin/python3 +# -*- mode: python; coding: utf-8 -*- +# Copyright (C) 2017 Laboratoire de Recherche et Développement de +# l'EPITA. +# +# This file is part of Spot, a model checking library. +# +# Spot is free software; you can redistribute it and/or modify it +# under the terms of the GNU General Public License as published by +# the Free Software Foundation; either version 3 of the License, or +# (at your option) any later version. +# +# Spot is distributed in the hope that it will be useful, but WITHOUT +# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +# or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +# License for more details. +# +# You should have received a copy of the GNU General Public License +# along with this program. If not, see . + +import spot + +a = spot.translate('(Ga -> Gb) W c') + +si = spot.scc_info(a) +n = si.scc_count() +assert n == 4 + +acc = 0 +rej = 0 +triv = 0 +for i in range(n): + acc += si.is_accepting_scc(i) + rej += si.is_rejecting_scc(i) + triv += si.is_trivial(i) +assert acc == 3 +assert rej == 1 +assert triv == 0 + +for scc in si: + acc -= scc.is_accepting() + rej -= scc.is_rejecting() + triv -= scc.is_trivial() +assert acc == 0 +assert rej == 0 +assert triv == 0 + +l0 = si.states_of(0) +l1 = si.states_of(1) +l2 = si.states_of(2) +l3 = si.states_of(3) +l = sorted(list(l0) + list(l1) + list(l2) + list(l3)) +assert l == [0, 1, 2, 3, 4] + +i = si.initial() +todo = {i} +seen = {i} +while todo: + e = todo.pop() + for s in si.succ(e): + if s not in seen: + seen.add(s) + todo.add(s) +assert seen == {0, 1, 2, 3} + +assert not spot.is_weak_automaton(a, si) -- GitLab