diff --git a/python/spot/impl.i b/python/spot/impl.i index e7546eae8..6aa6178a4 100644 --- a/python/spot/impl.i +++ b/python/spot/impl.i @@ -144,6 +144,7 @@ #include #include #include +#include #include #include #include diff --git a/spot/twaalgos/Makefile.am b/spot/twaalgos/Makefile.am index e372d75fd..133327fa1 100644 --- a/spot/twaalgos/Makefile.am +++ b/spot/twaalgos/Makefile.am @@ -49,6 +49,7 @@ twaalgos_HEADERS = \ emptiness_stats.hh \ gv04.hh \ hoa.hh \ + iscolored.hh \ isdet.hh \ isunamb.hh \ isweakscc.hh \ @@ -110,6 +111,7 @@ libtwaalgos_la_SOURCES = \ emptiness.cc \ gv04.cc \ hoa.cc \ + iscolored.cc \ isdet.cc \ isunamb.cc \ isweakscc.cc \ diff --git a/spot/twaalgos/iscolored.cc b/spot/twaalgos/iscolored.cc new file mode 100644 index 000000000..871ab6bc4 --- /dev/null +++ b/spot/twaalgos/iscolored.cc @@ -0,0 +1,32 @@ +// -*- coding: utf-8 -*- +// Copyright (C) 2017 Laboratoire de Recherche et Développement de l'Epita +// (LRDE). +// +// 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 . + +#include + +namespace spot +{ + bool + is_colored(const const_twa_graph_ptr& aut) + { + for (auto t: aut->edges()) + if (t.acc.count() != 1) + return false; + return true; + } +} diff --git a/spot/twaalgos/iscolored.hh b/spot/twaalgos/iscolored.hh new file mode 100644 index 000000000..fd8fd2eb6 --- /dev/null +++ b/spot/twaalgos/iscolored.hh @@ -0,0 +1,34 @@ +// -*- coding: utf-8 -*- +// Copyright (C) 2017 Laboratoire de Recherche et Développement de l'Epita +// (LRDE). +// +// 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 . + +#pragma once + +#include + +namespace spot +{ + /// \addtogroup twa_misc + /// + /// \brief Return true iff \a aut is colored + /// + /// An automaton is colored iff all the transitions belong to exactly one + /// acceptance set. This function simply iterates over all the transitions. + SPOT_API bool + is_colored(const const_twa_graph_ptr& aut); +}