From 0957317ad7adf07edd63e21e7b32b186845f3657 Mon Sep 17 00:00:00 2001
From: Alexandre GBAGUIDI AISSE <gbagui_a@epita.fr>
Date: Sat, 17 Jun 2017 19:23:38 +0200
Subject: [PATCH] =?UTF-8?q?spot/twa:=20Add=20methods=20to=20set=20co-B?=
 =?UTF-8?q?=C3=BCchi=20acceptance?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

* spot/twa/acc.hh: Add set_generalized_co_buchi() method.
* spot/twa/twa.hh: Add set_generalized_co_buchi() and set_co_buchi()
wrappers.
---
 spot/twa/acc.hh |  5 +++++
 spot/twa/twa.hh | 39 +++++++++++++++++++++++++++++++++++++++
 2 files changed, 44 insertions(+)

diff --git a/spot/twa/acc.hh b/spot/twa/acc.hh
index eaaf8419a..224a0f40b 100644
--- a/spot/twa/acc.hh
+++ b/spot/twa/acc.hh
@@ -1027,6 +1027,11 @@ namespace spot
       set_acceptance(inf(all_sets()));
     }
 
+    void set_generalized_co_buchi()
+    {
+      set_acceptance(fin(all_sets()));
+    }
+
     bool is_generalized_buchi() const
     {
       unsigned s = code_.size();
diff --git a/spot/twa/twa.hh b/spot/twa/twa.hh
index cfc6007f0..f1a492666 100644
--- a/spot/twa/twa.hh
+++ b/spot/twa/twa.hh
@@ -963,6 +963,24 @@ namespace spot
       acc_.set_generalized_buchi();
     }
 
+    /// \brief Set generalized co-Büchi acceptance
+    ///
+    /// \param num the number of acceptance sets to use
+    ///
+    /// The acceptance formula of the form
+    /// \code
+    /// Fin(0)&Fin(1)&...&Fin(num-1)
+    /// \endcode
+    /// is generated.
+    ///
+    /// In the case where \a num is null, the state-acceptance
+    /// property is automatically turned on.
+    void set_generalized_co_buchi(unsigned num)
+    {
+      set_num_sets_(num);
+      acc_.set_generalized_co_buchi();
+    }
+
     /// \brief Set Büchi acceptance.
     ///
     /// This declares a single acceptance set, and \c Inf(0)
@@ -984,6 +1002,27 @@ namespace spot
       return acc_.mark(0);
     }
 
+    /// \brief Set co-Büchi acceptance.
+    ///
+    /// This declares a single acceptance set, and \c Fin(0)
+    /// acceptance.  The returned mark \c {0} can be used to tag
+    /// non-accepting transition.
+    ///
+    /// Note that this does not mark the automaton as using
+    /// state-based acceptance. If you want to create a co-Büchi
+    /// automaton with state-based acceptance, call
+    /// \code
+    /// prop_state_acc(true)
+    /// \endcode
+    /// in addition.
+    ///
+    /// \see prop_state_acc
+    acc_cond::mark_t set_co_buchi()
+    {
+      set_generalized_co_buchi(1);
+      return acc_.mark(0);
+    }
+
   private:
     std::vector<formula> aps_;
     bdd bddaps_;