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.
This commit is contained in:
Alexandre Duret-Lutz
parent
803f9a5dd8
commit
289b2383ad
4 changed files with 187 additions and 83 deletions
|
|
@ -133,6 +133,7 @@
|
|||
#include <spot/twaalgos/neverclaim.hh>
|
||||
#include <spot/twaalgos/randomize.hh>
|
||||
#include <spot/twaalgos/remfin.hh>
|
||||
#include <spot/twaalgos/sccinfo.hh>
|
||||
#include <spot/twaalgos/strength.hh>
|
||||
#include <spot/twaalgos/sccfilter.hh>
|
||||
#include <spot/twaalgos/stats.hh>
|
||||
|
|
@ -533,6 +534,9 @@ def state_is_accepting(self, src) -> "bool":
|
|||
%include <spot/twaalgos/neverclaim.hh>
|
||||
%include <spot/twaalgos/randomize.hh>
|
||||
%include <spot/twaalgos/remfin.hh>
|
||||
%traits_swigtype(spot::scc_info_node);
|
||||
%fragment(SWIG_Traits_frag(spot::scc_info_node));
|
||||
%include <spot/twaalgos/sccinfo.hh>
|
||||
%include <spot/twaalgos/strength.hh>
|
||||
%include <spot/twaalgos/sccfilter.hh>
|
||||
%include <spot/twaalgos/stats.hh>
|
||||
|
|
@ -780,6 +784,14 @@ def state_is_accepting(self, src) -> "bool":
|
|||
}
|
||||
}
|
||||
|
||||
%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 {
|
||||
std::string __repr__()
|
||||
{
|
||||
|
|
|
|||
|
|
@ -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,25 +24,12 @@
|
|||
|
||||
namespace spot
|
||||
{
|
||||
/// \brief Compute an SCC map and gather assorted information.
|
||||
///
|
||||
/// This takes twa_graph as input and compute its SCCs. This
|
||||
/// class maps all input states to their SCCs, and vice-versa.
|
||||
/// It allows iterating over all SCCs of the automaton, and check
|
||||
/// their acceptance or non-acceptance.
|
||||
///
|
||||
/// Additionally this class can be used on alternating automata, but
|
||||
/// in this case, universal transitions are handled like existential
|
||||
/// transitions. It still make sense to check which states belong
|
||||
/// to the same SCC, but the acceptance information computed by
|
||||
/// this class is meaningless.
|
||||
class SPOT_API scc_info
|
||||
|
||||
/// Storage for SCC related information.
|
||||
class SPOT_API scc_info_node
|
||||
{
|
||||
public:
|
||||
typedef std::vector<unsigned> scc_succs;
|
||||
|
||||
class scc_node
|
||||
{
|
||||
friend class scc_info;
|
||||
protected:
|
||||
scc_succs succ_;
|
||||
|
|
@ -53,13 +40,13 @@ namespace spot
|
|||
bool rejecting_:1; // Necessarily rejecting
|
||||
bool useful_:1;
|
||||
public:
|
||||
scc_node():
|
||||
scc_info_node():
|
||||
acc_(0U), trivial_(true), accepting_(false),
|
||||
rejecting_(false), useful_(false)
|
||||
{
|
||||
}
|
||||
|
||||
scc_node(acc_cond::mark_t acc, bool trivial):
|
||||
scc_info_node(acc_cond::mark_t acc, bool trivial):
|
||||
acc_(acc), trivial_(trivial), accepting_(false),
|
||||
rejecting_(false), useful_(false)
|
||||
{
|
||||
|
|
@ -109,6 +96,27 @@ namespace spot
|
|||
}
|
||||
};
|
||||
|
||||
|
||||
/// \brief Compute an SCC map and gather assorted information.
|
||||
///
|
||||
/// This takes twa_graph as input and compute its SCCs. This
|
||||
/// class maps all input states to their SCCs, and vice-versa.
|
||||
/// It allows iterating over all SCCs of the automaton, and check
|
||||
/// their acceptance or non-acceptance.
|
||||
///
|
||||
/// Additionally this class can be used on alternating automata, but
|
||||
/// in this case, universal transitions are handled like existential
|
||||
/// transitions. It still make sense to check which states belong
|
||||
/// to the same SCC, but the acceptance information computed by
|
||||
/// this class is meaningless.
|
||||
class SPOT_API scc_info
|
||||
{
|
||||
public:
|
||||
// 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:
|
||||
|
||||
std::vector<unsigned> sccof_;
|
||||
|
|
@ -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<scc_node>::const_iterator begin() const
|
||||
{
|
||||
return node_.begin();
|
||||
}
|
||||
|
||||
std::vector<scc_node>::const_iterator end() const
|
||||
{
|
||||
return node_.end();
|
||||
}
|
||||
|
||||
std::vector<scc_node>::const_iterator cbegin() const
|
||||
{
|
||||
return node_.cbegin();
|
||||
}
|
||||
|
||||
std::vector<scc_node>::const_iterator cend() const
|
||||
{
|
||||
return node_.cend();
|
||||
}
|
||||
|
||||
std::vector<scc_node>::const_reverse_iterator rbegin() const
|
||||
{
|
||||
return node_.rbegin();
|
||||
}
|
||||
|
||||
std::vector<scc_node>::const_reverse_iterator rend() const
|
||||
{
|
||||
return node_.rend();
|
||||
}
|
||||
|
||||
const std::vector<unsigned>& states_of(unsigned scc) const
|
||||
{
|
||||
|
|
|
|||
|
|
@ -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 \
|
||||
|
|
|
|||
66
tests/python/sccinfo.py
Normal file
66
tests/python/sccinfo.py
Normal file
|
|
@ -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 <http://www.gnu.org/licenses/>.
|
||||
|
||||
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)
|
||||
Loading…
Add table
Add a link
Reference in a new issue