From b7ef7c55d71d6cac85d916286c14f161c1c426c4 Mon Sep 17 00:00:00 2001
From: Laurent XU <laurent.xu@lrde.epita.fr>
Date: Wed, 22 Mar 2017 18:01:37 +0100
Subject: [PATCH] misc: add spot::is_colored()

This function checks whether an automaton is colored, an automaton
is said to be colored iff all the transitions belong to exactly one
acceptance set.

* spot/twaalgos/iscolored.cc, spot/twaalgos/iscolored.hh: Here.
* spot/twaalgos/Makefile.am: add spot/twaalgos/iscolored.{cc,hh}
* python/spot/impl.i: add spot/twaalgos/iscolored.hh
---
 python/spot/impl.i         |  1 +
 spot/twaalgos/Makefile.am  |  2 ++
 spot/twaalgos/iscolored.cc | 32 ++++++++++++++++++++++++++++++++
 spot/twaalgos/iscolored.hh | 34 ++++++++++++++++++++++++++++++++++
 4 files changed, 69 insertions(+)
 create mode 100644 spot/twaalgos/iscolored.cc
 create mode 100644 spot/twaalgos/iscolored.hh

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 <spot/twaalgos/sccfilter.hh>
 #include <spot/twaalgos/stats.hh>
 #include <spot/twaalgos/isdet.hh>
+#include <spot/twaalgos/iscolored.hh>
 #include <spot/twaalgos/isunamb.hh>
 #include <spot/twaalgos/isweakscc.hh>
 #include <spot/twaalgos/langmap.hh>
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 <http://www.gnu.org/licenses/>.
+
+#include <spot/twaalgos/iscolored.hh>
+
+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 <http://www.gnu.org/licenses/>.
+
+#pragma once
+
+#include <spot/twa/twagraph.hh>
+
+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);
+}