Inf(i)|Inf(j) -> Inf(k) and Fin(i)&Fin(j) -> Fin(k)

Implement those rules in simplify_acceptance_here().

* NEWS: Mention the change.
* spot/twa/acc.cc,
spot/twa/acc.hh (acc_cond::acc_code::used_once_sets): New method.
* spot/twaalgos/cleanacc.cc, spot/twaalgos/cleanacc.hh:
Implement the above rule.
* tests/core/remfin.test: Adjust expected results.
* tests/python/simplacc.py: New file.
* tests/Makefile.am: Add it.

NEWS

@@ -61,6 +61,13 @@ New in spot 2.8.5.dev (not yet released)
     degeneralization to get rid of conjunction of Inf terms in
     acceptance conditions.
 
+  - simplify_acceptance_here() and simplify_acceptance() learned to
+    simplify subformulas like Fin(i)&Fin(j) or Inf(i)|Inf(j), or some
+    more complex variants of those.  If i us uniquely used in the
+    acceptance condition these become respectively Fin(i) or Inf(i),
+    and the automaton is adjusted to that i also appears where j
+    appeared.
+
 New in spot 2.8.5 (2020-01-04)
 
   Bugs fixed:

spot/twa/acc.cc

@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2015-2019 Laboratoire de Recherche et Développement
+// Copyright (C) 2015-2020 Laboratoire de Recherche et Développement
 // de l'Epita.
 //
 // This file is part of Spot, a model checking library.
@@ -2340,6 +2340,7 @@ namespace spot
 
     std::swap(c, *this);
   }
+
   int acc_cond::acc_code::fin_one() const
   {
     if (empty() || is_f())
@@ -2398,4 +2399,34 @@ namespace spot
     while (pos >= &front());
     return res;
   }
+
+  acc_cond::mark_t acc_cond::acc_code::used_once_sets() const
+  {
+    mark_t seen = {};
+    mark_t dups = {};
+    if (empty())
+      return {};
+    const acc_cond::acc_word* pos = &back();
+    do
+      {
+        switch (pos->sub.op)
+          {
+          case acc_cond::acc_op::And:
+          case acc_cond::acc_op::Or:
+            --pos;
+            break;
+          case acc_cond::acc_op::Inf:
+          case acc_cond::acc_op::InfNeg:
+          case acc_cond::acc_op::FinNeg:
+          case acc_cond::acc_op::Fin:
+            auto m = pos[-1].mark;
+            pos -= 2;
+            dups |= m & seen;
+            seen |= m;
+            break;
+          }
+      }
+    while (pos >= &front());
+    return seen - dups;
+  }
 }

spot/twa/acc.hh

@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2014-2019 Laboratoire de Recherche et Développement
+// Copyright (C) 2014-2020 Laboratoire de Recherche et Développement
 // de l'Epita.
 //
 // This file is part of Spot, a model checking library.
@@ -1199,7 +1199,7 @@ namespace spot
       ///
       /// If multiple unit-Fin appear as unit-clauses, the set of
       /// those will be returned.  For instance applied to
-      /// `Fin(0)&Fin(1)&(Inf(2)|Fin(3))``, this will return `{0,1}`.
+      /// `Fin(0)&Fin(1)&(Inf(2)|Fin(3))`, this will return `{0,1}`.
       mark_t fin_unit() const;
 
       /// \brief Return one acceptance set i that appear as `Fin(i)`
@@ -1286,6 +1286,14 @@ namespace spot
       /// \brief Return the set of sets appearing in the condition.
       acc_cond::mark_t used_sets() const;
 
+      /// \brief Return the sets that appears only once in the
+      /// acceptance.
+      ///
+      /// For instance if the condition is
+      /// `Fin(0)&(Inf(1)|(Fin(1)&Inf(2)))`, this returns `{0,2}`,
+      /// because set `1` is used more than once.
+      mark_t used_once_sets() const;
+
       /// \brief  Return the sets used as Inf or Fin in the acceptance condition
       std::pair<acc_cond::mark_t, acc_cond::mark_t> used_inf_fin_sets() const;
 

spot/twaalgos/cleanacc.cc

@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2015, 2017-2019 Laboratoire de Recherche et Développement
+// Copyright (C) 2015, 2017-2020 Laboratoire de Recherche et Développement
 // de l'Epita.
 //
 // This file is part of Spot, a model checking library.
@@ -320,6 +320,292 @@ namespace spot
                                            complement));
       return aut;
     }
+
+
+    acc_cond::acc_code acc_rewrite_rec(const acc_cond::acc_word* pos)
+    {
+      auto start = pos - pos->sub.size;
+      switch (pos->sub.op)
+        {
+          case acc_cond::acc_op::And:
+            {
+              --pos;
+              auto res = acc_cond::acc_code::t();
+              do
+                {
+                  auto tmp = acc_rewrite_rec(pos);
+                  tmp &= std::move(res);
+                  std::swap(tmp, res);
+                  pos -= pos->sub.size + 1;
+                }
+              while (pos > start);
+              return res;
+            }
+         case acc_cond::acc_op::Or:
+            {
+              --pos;
+              auto res = acc_cond::acc_code::f();
+              do
+                {
+                  auto tmp = acc_rewrite_rec(pos);
+                  tmp |= std::move(res);
+                  std::swap(tmp, res);
+                  pos -= pos->sub.size + 1;
+                }
+              while (pos > start);
+              return res;
+            }
+          case acc_cond::acc_op::Fin:
+            return acc_cond::acc_code::fin(pos[-1].mark);
+          case acc_cond::acc_op::Inf:
+            return acc_cond::acc_code::inf(pos[-1].mark);
+          case acc_cond::acc_op::FinNeg:
+          case acc_cond::acc_op::InfNeg:
+            SPOT_UNREACHABLE();
+        };
+        SPOT_UNREACHABLE();
+        return {};
+    }
+
+    acc_cond::mark_t find_interm_rec(acc_cond::acc_word* pos)
+    {
+      acc_cond::acc_op wanted;
+      auto topop = pos->sub.op;
+      if (topop == acc_cond::acc_op::Or)
+        {
+          wanted = acc_cond::acc_op::Fin;
+        }
+      else
+        {
+          wanted = acc_cond::acc_op::Inf;
+          assert(topop == acc_cond::acc_op::And);
+        }
+      acc_cond::mark_t res = {};
+      const acc_cond::acc_word* rend = pos - (pos->sub.size + 1);
+      --pos;
+      do
+        switch (auto op = pos->sub.op)
+          {
+          case acc_cond::acc_op::Inf:
+          case acc_cond::acc_op::Fin:
+          case acc_cond::acc_op::InfNeg:
+          case acc_cond::acc_op::FinNeg:
+            {
+              auto m = pos[-1].mark;
+              if (op == wanted && m == m.lowest())
+                {
+                  res |= m;
+                }
+              else
+                {
+                  return {};
+                }
+              pos -= 2;
+              break;
+            }
+          case acc_cond::acc_op::And:
+          case acc_cond::acc_op::Or:
+            if (op == topop)
+              {
+                if (auto m = find_interm_rec(pos))
+                  res |= m;
+                else
+                  return {};
+                pos -= pos->sub.size + 1;
+              }
+            else
+              {
+                auto posend = pos - (pos->sub.size + 1);
+                --pos;
+                bool seen = false;
+                do
+                  {
+                    switch (auto op = pos->sub.op)
+                      {
+                      case acc_cond::acc_op::Inf:
+                      case acc_cond::acc_op::Fin:
+                      case acc_cond::acc_op::InfNeg:
+                      case acc_cond::acc_op::FinNeg:
+                        if (op == wanted)
+                          {
+                            auto m = pos[-1].mark;
+                            if (!seen && m == m.lowest())
+                              {
+                                seen = true;
+                                res |= m;
+                              }
+                            else
+                              {
+                                return {};
+                              }
+                          }
+                        pos -= 2;
+                        break;
+                      case acc_cond::acc_op::And:
+                      case acc_cond::acc_op::Or:
+                        return {};
+                      }
+                  }
+                while (pos > posend);
+              }
+            break;
+          }
+      while (pos > rend);
+      return res;
+    }
+
+    // Replace Inf(i)|Inf(j) by Inf(k)
+    //   or    Fin(i)&Fin(j) by Fin(k)
+    // For this to work, k must be one of i or j,
+    //                   k must be used only once in the acceptance
+    // the transitions have to be updated: every transition marked
+    // by i or j should be marked by k.
+    void fuse_marks_here(twa_graph_ptr aut)
+    {
+      acc_cond::acc_code acccopy = aut->get_acceptance();
+      acc_cond::mark_t once = acccopy.used_once_sets();
+      if (!once)
+        return;
+
+      acc_cond::acc_word* pos = &acccopy.back();
+      const acc_cond::acc_word* front = &acccopy.front();
+
+      // a list of pairs ({i}, {j, k, l, ...}) where i is a set
+      // occurring once that can be removed if all transitions in set
+      // i are added to sets j,k,l, ...
+      std::vector<std::pair<acc_cond::mark_t, acc_cond::mark_t>> to_fuse;
+
+      auto find_fusable = [&](acc_cond::acc_word* pos)
+                          {
+                            acc_cond::acc_op wanted;
+                            auto topop = pos->sub.op;
+                            if (topop == acc_cond::acc_op::And)
+                              {
+                                wanted = acc_cond::acc_op::Fin;
+                              }
+                            else
+                              {
+                                wanted = acc_cond::acc_op::Inf;
+                                assert(topop == acc_cond::acc_op::Or);
+                              }
+
+                            // Return a vector of "singleton-sets" of
+                            // the wanted type in the operand of the
+                            // pointed Or/And operator.  For instance,
+                            // assuming wanted=Inf and pos points to
+                            //
+                            // Inf({1})|Inf({2,3})|Fin({4})
+                            //         |Inf({5})|Inf({5})|Inf({6})
+                            //
+                            // This returns [({1}, Inf({1})),
+                            //               ({5}, Inf({5}))]].
+                            std::vector<std::pair<acc_cond::mark_t,
+                                                  acc_cond::acc_word*>>
+                                        singletons;
+                            const acc_cond::acc_word* rend =
+                              pos - (pos->sub.size + 1);
+                            --pos;
+                            do
+                              {
+                                switch (auto op = pos->sub.op)
+                                  {
+                                  case acc_cond::acc_op::InfNeg:
+                                  case acc_cond::acc_op::FinNeg:
+                                  case acc_cond::acc_op::Inf:
+                                  case acc_cond::acc_op::Fin:
+                                    {
+                                      auto m = pos[-1].mark;
+                                      if (op == wanted && m == m.lowest())
+                                        singletons.emplace_back(m, pos);
+                                      pos -= 2;
+                                    }
+                                    break;
+                                  case acc_cond::acc_op::And:
+                                  case acc_cond::acc_op::Or:
+                                    // On
+                                    // Fin(a)&(Fin(b)&Inf(c)|Fin(d))
+                                    // where we'd like to return [{a},
+                                    // {b,d}] and decide later that
+                                    // {b,d} can receive {a} if they
+                                    // (b and d) are both used once.
+                                    if (auto m = find_interm_rec(pos))
+                                      {
+                                        singletons.emplace_back(m, pos);
+                                        // move this to the front, to
+                                        // be sure it is the first
+                                        // recipient tried.
+                                        swap(singletons.front(),
+                                             singletons.back());
+                                      }
+                                    pos -= pos->sub.size + 1;
+                                    break;
+                                  }
+                              }
+                            while (pos > rend);
+
+                            acc_cond::mark_t can_receive = {};
+                            for (auto p: singletons)
+                              if ((p.first & once) == p.first)
+                                {
+                                  can_receive = p.first;
+                                  break;
+                                }
+                            if (!can_receive)
+                              return;
+                            for (auto p: singletons)
+                              if (p.first != can_receive)
+                                {
+                                  to_fuse.emplace_back(p.first, can_receive);
+                                  if (p.second->sub.op == acc_cond::acc_op::Fin)
+                                    p.second->sub.op = acc_cond::acc_op::Inf;
+                                  else
+                                    p.second->sub.op = acc_cond::acc_op::Fin;
+                                  p.second[-1].mark = {};
+                                }
+                          };
+
+      do
+        {
+          switch (pos->sub.op)
+            {
+            case acc_cond::acc_op::And:
+            case acc_cond::acc_op::Or:
+              find_fusable(pos);
+              // Don't skip to entire operands, as we might find
+              // fusable sub-parts.
+              --pos;
+              break;
+            case acc_cond::acc_op::Inf:
+            case acc_cond::acc_op::InfNeg:
+            case acc_cond::acc_op::FinNeg:
+            case acc_cond::acc_op::Fin:
+              pos -= 2;
+              break;
+            }
+        }
+      while (pos >= front);
+
+      if (to_fuse.empty())
+        return;
+
+      // Update the transition according to to_fuse.
+      for (auto pair: to_fuse)
+        if (pair.first & once) // can we remove pair.first?
+          {
+            for (auto& e: aut->edges())
+              if (e.acc & pair.first)
+                e.acc = (e.acc - pair.first) | pair.second;
+          }
+        else
+          {
+            for (auto& e: aut->edges())
+              if (e.acc & pair.first)
+                e.acc |= pair.second;
+          }
+
+      // Now rewrite the acceptance condition, removing all the "to_kill" terms.
+      aut->set_acceptance(aut->num_sets(), acc_rewrite_rec(&acccopy.back()));
+    }
   }
 
   twa_graph_ptr simplify_acceptance_here(twa_graph_ptr aut)
@@ -327,9 +613,11 @@ namespace spot
     cleanup_acceptance_here(aut, false);
     merge_identical_marks_here(aut);
     if (!aut->acc().is_generalized_buchi())
+      {
         simplify_complementary_marks_here(aut);
+        fuse_marks_here(aut);
+      }
     cleanup_acceptance_here(aut, true);
-
     return aut;
   }
 

spot/twaalgos/cleanacc.hh

@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2015, 2017-2019 Laboratoire de Recherche et
+// Copyright (C) 2015, 2017-2020 Laboratoire de Recherche et
 // Développement de l'Epita.
 //
 // This file is part of Spot, a model checking library.
@@ -57,6 +57,11 @@ namespace spot
   ///   - `Fin(i) | Inf(j) = Inf(j)`
   ///   - `Inf(i) | Inf(j) = t`
   ///   - `Fin(i) | Inf(i) = t`
+  /// And also merge terms like `Inf(i)|Inf(j)` or `Fin(i)&Fin(j)`
+  /// provided at least i or j is used uniquely in the formula.
+  /// (for instance if i is unique, `Inf(i)|Inf(j)` is rewritten
+  /// as `Inf(i)`, and `i` is added on all transitions where `j` is present
+  /// in the automaton.)
   ///
   /// simplify_acceptance_here() works in place, simplify_acceptance()
   /// returns a new automaton that has been simplified.

tests/Makefile.am

@@ -1,6 +1,5 @@
 ## -*- coding: utf-8 -*-
-
+## Copyright (C) 2009-2020 Laboratoire de Recherche et Développement
-## Copyright (C) 2009-2019 Laboratoire de Recherche et Développement
 ## de l'Epita (LRDE).
 ## Copyright (C) 2003-2006 Laboratoire d'Informatique de Paris 6
 ## (LIP6), département Systèmes Répartis Coopératifs (SRC), Université
@@ -410,6 +409,7 @@ TESTS_python = \
   python/semidet.py \
   python/setacc.py \
   python/setxor.py \
+  python/simplacc.py \
   python/simstate.py \
   python/split.py \
   python/streett_totgba.py \

tests/core/remfin.test

@@ -1,8 +1,7 @@
 #!/bin/sh
 # -*- coding: utf-8 -*-
-
+# Copyright (C) 2015-2018, 2020 Laboratoire de Recherche et
-# Copyright (C) 2015-2018 Laboratoire de Recherche et Développement de
+# Développement de l'Epita (LRDE).
-# l'Epita (LRDE).
 #
 # This file is part of Spot, a model checking library.
 #
@@ -340,7 +339,7 @@ HOA: v1
 States: 4
 Start: 0
 AP: 2 "a" "b"
-Acceptance: 5 (Inf(0)&Inf(1)&Inf(4)) | Inf(0) | (Inf(2)&Inf(3))
+Acceptance: 4 (Inf(0)&Inf(1)) | Inf(0) | (Inf(2)&Inf(3))
 properties: trans-labels explicit-labels trans-acc
 --BODY--
 State: 0
@@ -357,7 +356,7 @@ State: 2
 [!0&!1] 2 {0}
 [!0&!1] 3
 State: 3
-[!0&!1] 3 {0 1 4}
+[!0&!1] 3 {0 1}
 --END--
 HOA: v1
 States: 1
@@ -402,7 +401,8 @@ HOA: v1
 States: 10
 Start: 2
 AP: 1 "p1"
-Acceptance: 2 Inf(1) | Inf(0)
+acc-name: Buchi
+Acceptance: 1 Inf(0)
 properties: trans-labels explicit-labels state-acc
 --BODY--
 State: 0
@@ -410,29 +410,29 @@ State: 0
 [!0] 6
 [0] 8
 [0] 9
-State: 1 {0 1}
+State: 1
 [t] 3
-State: 2 {0 1}
+State: 2
 [0] 1
 [!0] 5
-State: 3 {0 1}
+State: 3
 [0] 0
 [!0] 6
-State: 4 {0 1}
+State: 4 {0}
 [0] 4
 [!0] 6
-State: 5 {0 1}
+State: 5
 [0] 3
 [!0] 7
 State: 6
 [0] 0
 [!0] 6
-State: 7 {1}
+State: 7
 [0] 4
 [!0] 6
 State: 8
 [0] 8
-State: 9 {1}
+State: 9 {0}
 [0] 9
 --END--
 HOA: v1
@@ -765,7 +765,7 @@ acc-name: Buchi
 Acceptance: 1 Inf(0)
 properties: trans-labels explicit-labels state-acc
 --BODY--
-State: 0 {0}
+State: 0
 [!0&1] 5
 [!0&1] 7
 State: 1

tests/python/simplacc.py

@@ -0,0 +1,54 @@
+# -*- mode: python; coding: utf-8 -*-
+# Copyright (C) 2020 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/>.
+
+import spot
+
+
+auts = list(spot.automata("""
+HOA: v1 States: 2 Start: 0 AP: 2 "a" "b" Acceptance: 2 Inf(0) | Inf(1) --BODY--
+State: 0 [1] 0 [0] 1 {0} State: 1 [0] 1 [1] 0 {1} --END--
+HOA: v1 States: 2 Start: 0 AP: 2 "a" "b" Acceptance: 2 (Inf(0) | Inf(1)) &
+Fin(0) --BODY-- State: 0 [1] 0 [0] 1 {0} State: 1 [0] 1 [1] 0 {1} --END--
+HOA: v1 States: 2 Start: 0 AP: 2 "a" "b" Acceptance: 3 (Inf(0) | Inf(1)) &
+(Fin(0) | Inf(2)) --BODY-- State: 0 [1] 0 [0] 1 {0} State: 1 [0] 1 {2} [1] 0
+{1} --END--
+HOA: v1 States: 2 Start: 0 AP: 2 "a" "b" Acceptance: 4 (Inf(0) |
+(Inf(1)&(Inf(3)|Fin(2)))) --BODY-- State: 0 [1] 0 {3} [0] 1 {0} State: 1 [0] 1
+{2} [1] 0 {1} --END--
+"""))
+
+res = []
+for a in auts:
+    b = spot.simplify_acceptance(a)
+    assert b.equivalent_to(a)
+    res.append(str(b.get_acceptance()))
+
+    a.set_acceptance(a.num_sets(), a.get_acceptance().complement())
+    b = spot.simplify_acceptance(a)
+    assert b.equivalent_to(a)
+    res.append(str(b.get_acceptance()))
+
+assert res == ['Inf(0)',
+               'Fin(0)',
+               'Inf(1) & Fin(0)',
+               'Fin(1) | Inf(0)',
+               'Inf(1) & (Fin(0) | Inf(2))',
+               'Fin(1) | (Fin(2) & Inf(0))',
+               '(Fin(1) | Inf(2)) & Inf(0)',
+               'Fin(0) | (Fin(2) & Inf(1))']