introduce delay_branching_here

This is motivated by an example sent by Edmond Irani Liu,
that will be tested in next patch.

* spot/twaalgos/dbranch.cc, spot/twaalgos/dbranch.hh: New files.
* python/spot/impl.i, spot/twaalgos/Makefile.am: Add them.
* spot/twaalgos/translate.cc: Call delay_branching_here
unconditionally.
* spot/twa/twagraph.cc (defrag_states): Do not assume
that games are alternating.
* tests/core/genltl.test: Adjust expected numbers.
* tests/python/dbranch.py: New file.
* tests/Makefile.am: Add it.

NEWS

@@ -142,6 +142,15 @@ New in spot 2.10.6.dev  (not yet released)
     succesors, should be called before running simulation-based
     reductions.
 
+  - A new function delay_branching_here(aut) can be used to simplify
+    some non-deterministic branching.  If two transitions (q₁,ℓ,M,q₂)
+    and (q₁,ℓ,M,q₃) differ only by their destination state, and are
+    the only incoming transitions of their destination states, then q₂
+    and q₃ can be merged (taking the union of their outgoing
+    transitions).  This is cheap function is automatically called by
+    spot::translate() after translation of a formula to GBA, before
+    further simplification.
+
   - spot::parallel_policy is an object that can be passed to some
     algorithm to specify how many threads can be used if Spot has been
     compiled with --enable-pthread.  Currently, only

python/spot/impl.i

@@ -114,13 +114,14 @@
 #include <spot/twaalgos/aiger.hh>
 #include <spot/twaalgos/alternation.hh>
 #include <spot/twaalgos/cleanacc.hh>
-#include <spot/twaalgos/degen.hh>
-#include <spot/twaalgos/dot.hh>
-#include <spot/twaalgos/dualize.hh>
 #include <spot/twaalgos/cobuchi.hh>
 #include <spot/twaalgos/copy.hh>
 #include <spot/twaalgos/complete.hh>
 #include <spot/twaalgos/complement.hh>
+#include <spot/twaalgos/dbranch.hh>
+#include <spot/twaalgos/degen.hh>
+#include <spot/twaalgos/dot.hh>
+#include <spot/twaalgos/dualize.hh>
 #include <spot/twaalgos/emptiness.hh>
 #include <spot/twaalgos/gtec/gtec.hh>
 #include <spot/twaalgos/genem.hh>
@@ -678,11 +679,14 @@ def state_is_accepting(self, src) -> "bool":
 %include <spot/twaalgos/aiger.hh>
 %include <spot/twaalgos/alternation.hh>
 %include <spot/twaalgos/cleanacc.hh>
-%include <spot/twaalgos/degen.hh>
-%include <spot/twaalgos/dot.hh>
 %include <spot/twaalgos/cobuchi.hh>
 %include <spot/twaalgos/copy.hh>
 %include <spot/twaalgos/complete.hh>
+%include <spot/twaalgos/dbranch.hh>
+%include <spot/twaalgos/degen.hh>
+%include <spot/twaalgos/determinize.hh>
+%include <spot/twaalgos/dot.hh>
+%include <spot/twaalgos/dualize.hh>
 %feature("flatnested") spot::twa_run::step;
 %include <spot/twaalgos/emptiness.hh>
 %template(list_step) std::list<spot::twa_run::step>;
@@ -694,8 +698,6 @@ def state_is_accepting(self, src) -> "bool":
 %include <spot/twaalgos/gfguarantee.hh>
 %include <spot/twaalgos/compsusp.hh>
 %include <spot/twaalgos/contains.hh>
-%include <spot/twaalgos/determinize.hh>
-%include <spot/twaalgos/dualize.hh>
 %include <spot/twaalgos/langmap.hh>
 %include <spot/twaalgos/magic.hh>
 %include <spot/twaalgos/minimize.hh>

spot/twa/twagraph.cc

@@ -1323,18 +1323,6 @@ namespace spot
       }
     init_number_ = newst[init_number_];
     g_.defrag_states(newst, used_states);
-    // Make sure we did not mess up the structure
-    assert([&]()
-      {
-        if (auto sp = get_named_prop<std::vector<bool>>("state-player"))
-          {
-            for (const auto& e : edges())
-              if (sp->at(e.src) == sp->at(e.dst))
-                return false;
-            return true;
-          }
-        return true;
-      }() && "Game not alternating!");
   }
 
   void twa_graph::remove_unused_ap()

spot/twaalgos/Makefile.am

@@ -1,5 +1,5 @@
 ## -*- coding: utf-8 -*-
-## Copyright (C) 2008-2018, 2020-2021 Laboratoire de Recherche et
+## Copyright (C) 2008-2018, 2020-2022 Laboratoire de Recherche et
 ## Développement de l'Epita (LRDE).
 ## Copyright (C) 2003-2005 Laboratoire d'Informatique de Paris 6
 ## (LIP6), département Systèmes Répartis Coopératifs (SRC), Université
@@ -42,6 +42,7 @@ twaalgos_HEADERS = \
   contains.hh \
   copy.hh \
   cycles.hh \
+  dbranch.hh \
   degen.hh \
   determinize.hh \
   dot.hh \
@@ -115,6 +116,7 @@ libtwaalgos_la_SOURCES = \
   compsusp.cc \
   contains.cc \
   cycles.cc \
+  dbranch.cc \
   degen.cc \
   determinize.cc \
   dot.cc \

spot/twaalgos/dbranch.cc

@@ -0,0 +1,163 @@
+// -*- coding: utf-8 -*-
+// Copyright (C) 2022 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 "config.h"
+
+#include <spot/twaalgos/dbranch.hh>
+#include <spot/misc/bddlt.hh>
+#include <spot/priv/robin_hood.hh>
+#include <unordered_map>
+#include <utility>
+#include <stack>
+
+namespace spot
+{
+  namespace
+  {
+    typedef std::pair<bdd, acc_cond::mark_t> bdd_color;
+
+    struct bdd_color_hash
+    {
+      size_t
+      operator()(const bdd_color& bc) const noexcept
+      {
+        return bc.first.id() ^ bc.second.hash();
+      }
+    };
+
+    template<bool is_game>
+    bool delay_branching_aux(const twa_graph_ptr& aut, std::vector<bool>* owner)
+    {
+      unsigned ns = aut->num_states();
+      // number of predecessors of each state
+      std::vector<unsigned> pred_count(ns, 0);
+      unsigned init = aut->get_init_state_number();
+      pred_count[init] = 2; // pretend the initial state has too many
+                            // predecessors, so it does not get fused.
+      // for each state, number of successors that have a single predecessors
+      std::vector<unsigned> succ_cand(ns, 0);
+      for (auto& e: aut->edges())
+        for (unsigned d: aut->univ_dests(e))
+          {
+            // Note that e.dst might be a destination group in
+            // alternating automata.
+            unsigned pc = ++pred_count[d];
+            succ_cand[e.src] += (pc == 1) - (pc == 2);
+          }
+      bool changed = false;
+      typedef robin_hood::unordered_map<bdd_color, unsigned,
+                                        bdd_color_hash> hashmap_t;
+      hashmap_t first_dest[1 + is_game];
+      auto& g = aut->get_graph();
+
+      // setup a DFS
+      std::vector<bool> seen(ns);
+      std::stack<unsigned> todo;
+      auto push_state = [&](unsigned state)
+      {
+        todo.push(state);
+        seen[state] = true;
+      };
+      push_state(init);
+
+      while (!todo.empty())
+        {
+          unsigned src = todo.top();
+          todo.pop();
+          if (succ_cand[src] < 2) // nothing to merge
+            {
+              for (auto& e: aut->out(src))
+                for (unsigned d: aut->univ_dests(e))
+                  if (!seen[d])
+                    push_state(d);
+              continue;
+            }
+          first_dest[0].clear();
+          if constexpr (is_game)
+            first_dest[1].clear();
+          auto it = g.out_iteraser(src);
+          while (it)
+            {
+              unsigned canddst = it->dst;
+              for (unsigned d: aut->univ_dests(canddst))
+                if (!seen[d])
+                  push_state(d);
+              if (aut->is_univ_dest(canddst) || pred_count[canddst] != 1)
+                {
+                  ++it;
+                  continue;
+                }
+              if (it->cond == bddfalse)
+                {
+                  it.erase();
+                  continue;
+                }
+              unsigned mapidx = is_game ? (*owner)[canddst] : 0;
+              auto [it2, inserted] =
+                first_dest[mapidx].emplace(bdd_color{it->cond, it->acc},
+                                           canddst);
+              if (inserted)
+                {
+                  ++it;
+                  continue;
+                }
+              unsigned mergedst = it2->second;
+              // we have to merge canddst into mergedst.  This is as
+              // simple as:
+              // 1) connecting their list of transitions
+              unsigned& mergedfirst = g.state_storage(mergedst).succ;
+              unsigned& mergedlast = g.state_storage(mergedst).succ_tail;
+              unsigned& candfirst = g.state_storage(canddst).succ;
+              unsigned& candlast = g.state_storage(canddst).succ_tail;
+              if (mergedlast)
+                aut->edge_storage(mergedlast).next_succ = candfirst;
+              else              // mergedst had now successor
+                mergedfirst = candfirst;
+              mergedlast = candlast;
+              // 2) updating the source of the merged transitions
+              for (unsigned e2 = candfirst; e2 != 0;)
+                {
+                  auto& edge = aut->edge_storage(e2);
+                  edge.src = mergedst;
+                  e2 = edge.next_succ;
+                }
+              // 3) deleting the edge to canddst.
+              candfirst = candlast = 0;
+              it.erase();
+              // 4) updating succ_cand
+              succ_cand[mergedst] += succ_cand[canddst];
+              succ_cand[canddst] = 0;
+              changed = true;
+            }
+        }
+      return changed;
+    }
+  }
+
+  bool delay_branching_here(const twa_graph_ptr& aut)
+  {
+    if (aut->prop_universal())
+      return false;
+    auto owner = aut->get_named_prop<std::vector<bool>>("state-player");
+    if (SPOT_UNLIKELY(owner))
+      return delay_branching_aux<true>(aut, owner);
+    else
+      return delay_branching_aux<false>(aut, nullptr);
+  }
+}

spot/twaalgos/dbranch.hh

@@ -0,0 +1,36 @@
+// -*- coding: utf-8 -*-
+// Copyright (C) 2022 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
+{
+  /// \ingroup twa_algorithms
+  /// \brief Merge states to delay
+  ///
+  /// If a state (x) has two outgoing transitions (x,l,m,y) and
+  /// (x,l,m,z) going to states (x) and (y) that have no other
+  /// incoming edges, then (y) and (z) can be merged (keeping the
+  /// union of their outgoing destinations).
+  ///
+  /// \return true iff the automaton was modified.
+  SPOT_API bool delay_branching_here(const twa_graph_ptr& aut);
+}

spot/twaalgos/translate.cc

@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2013-2018, 2020-2021 Laboratoire de Recherche et
+// Copyright (C) 2013-2018, 2020-2022 Laboratoire de Recherche et
 // Développement de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -29,6 +29,7 @@
 #include <spot/twaalgos/product.hh>
 #include <spot/twaalgos/sccinfo.hh>
 #include <spot/twaalgos/hoa.hh>
+#include <spot/twaalgos/dbranch.hh>
 
 namespace spot
 {
@@ -401,6 +402,11 @@ namespace spot
         aut = ltl_to_tgba_fm(r, simpl_->get_dict(), exprop,
                              true, false, false, nullptr, nullptr,
                              unambiguous);
+        if (delay_branching_here(aut))
+          {
+            aut->purge_unreachable_states();
+            aut->merge_edges();
+          }
       }
 
     aut = this->postprocessor::run(aut, r);

tests/Makefile.am

@@ -405,6 +405,7 @@ TESTS_python = \
   python/bddnqueen.py \
   python/bugdet.py \
   python/complement_semidet.py \
+  python/dbranch.py \
   python/declenv.py \
   python/decompose_scc.py \
   python/det.py \

tests/core/genltl.test

@@ -1,6 +1,6 @@
 #!/bin/sh
 # -*- coding: utf-8 -*-
-# Copyright (C) 2016-2021 Laboratoire de Recherche et Développement
+# Copyright (C) 2016-2022 Laboratoire de Recherche et Développement
 # de l'Epita (LRDE).
 #
 # This file is part of Spot, a model checking library.
@@ -134,8 +134,8 @@ genltl --kr-n2=1..2 --kr-nlogn=1..2 --kr-n=1..2 --gxf-and=0..3 --fxg-or=0..3 \
        --pps-arbiter-standard=2..3 --pps-arbiter-strict=2..3 --format=%F=%L,%f |
     ltl2tgba --low --det -F-/2 --stats='%<,%s' > out
 cat >exp<<EOF
-kv-psi=1,10
-kv-psi=2,24
+kv-psi=1,9
+kv-psi=2,19
 kr-nlogn=1,16
 kr-nlogn=2,44
 kr-n=1,10

tests/python/dbranch.py

@@ -0,0 +1,147 @@
+# -*- mode: python; coding: utf-8 -*-
+# Copyright (C) 2022 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/>.
+
+# Test that the spot.gen package works, in particular, we want
+# to make sure that the objects created from spot.gen methods
+# are usable with methods from the spot package.
+
+
+import spot
+from unittest import TestCase
+tc = TestCase()
+
+aut5 = spot.automaton("""HOA: v1 States: 28 Start: 0 AP: 4 "alive" "b"
+"a" "c" acc-name: Buchi Acceptance: 1 Inf(0) properties: trans-labels
+explicit-labels state-acc very-weak --BODY-- State: 0 [0] 1 [0] 2 [0]
+3 [0] 4 [0] 5 [0&!1] 6 [0] 7 State: 1 [0] 8 State: 2 [!0] 9 [0] 10
+State: 3 [!0] 9 [0] 11 State: 4 [!0] 9 [0] 12 State: 5 [!0] 9 [0] 13
+State: 6 [!0] 9 [0&!1] 14 State: 7 [!0] 9 [0&!1&!2] 14 State: 8 [0] 15
+State: 9 {0} [!0] 9 State: 10 [!0] 9 [0] 16 State: 11 [!0] 9 [0] 17
+State: 12 [!0] 9 [0] 18 State: 13 [!0] 9 [0&!1&!2] 19 State: 14 [!0] 9
+[0&!1] 19 State: 15 [0] 20 State: 16 [!0] 9 [0] 21 State: 17 [!0] 9
+[0] 22 State: 18 [!0] 9 [0&!1&!2] 23 State: 19 [!0] 9 [0&!1] 23 State:
+20 [0] 24 State: 21 [!0] 9 [0] 25 State: 22 [!0] 9 [0&!1&!2] 26 State:
+23 [!0] 9 [0&!1] 26 State: 24 [0&3] 27 State: 25 [!0] 9 [0&!1&!2] 27
+State: 26 [!0] 9 [0&!1] 27 State: 27 [!0] 9 [0] 27 --END--""")
+
+copy = spot.make_twa_graph(aut5, spot.twa_prop_set.all())
+
+tc.assertFalse(spot.is_deterministic(aut5))
+if spot.delay_branching_here(aut5):
+    aut5.purge_unreachable_states()
+    aut5.merge_edges()
+tc.assertEqual(aut5.num_states(), 13)
+tc.assertEqual(aut5.num_edges(), 29)
+tc.assertTrue(spot.are_equivalent(copy, aut5))
+
+a = spot.automaton("""HOA: v1 States: 8 Start: 0 AP: 3 "a" "b" "c"
+Acceptance: 0 t --BODY-- State: 0 [0] 1 [0] 2 [0] 3 State: 1 [!1] 4&5
+[1] 5&6 State: 2 [0] 4&6 State: 3 [0] 3&6 State: 4 [!0] 7 State: 5
+[!0] 7 State: 6 [!0] 6 State: 7 [0] 7 --END--""")
+
+copy = spot.make_twa_graph(a, spot.twa_prop_set.all())
+if spot.delay_branching_here(a):
+    a.purge_unreachable_states()
+    a.merge_edges()
+tc.assertEqual(a.to_str(), """HOA: v1
+States: 7
+Start: 0
+AP: 3 "b" "a" "c"
+acc-name: all
+Acceptance: 0 t
+properties: trans-labels explicit-labels state-acc univ-branch
+--BODY--
+State: 0
+[1] 1
+[1] 2
+State: 1
+[1] 3&5
+[0] 4&5
+[!0] 3&4
+State: 2
+[1] 2&5
+State: 3
+[!1] 6
+State: 4
+[!1] 6
+State: 5
+[!1] 5
+State: 6
+[1] 6
+--END--""")
+
+a = spot.automaton("""HOA: v1
+States: 9
+Start: 0 AP: 2 "a" "b"
+spot.state-player: 0 1 1 0 0 0 0 1 1
+Acceptance: 0 t
+--BODY--
+State: 0
+[0] 1
+[0] 2
+[0] 3
+[0] 4
+State: 1
+[1] 5
+State: 2
+[!1] 6
+State: 3
+[1] 7
+State: 4
+[!1] 8
+State: 5
+[t] 5
+State: 6
+[t] 6
+State: 7
+[t] 7
+State: 8
+[t] 8
+--END--""")
+copy = spot.make_twa_graph(a, spot.twa_prop_set.all())
+if spot.delay_branching_here(a):
+    a.purge_unreachable_states()
+tc.assertTrue(spot.are_equivalent(a, copy))
+tc.assertEqual(a.to_str(), """HOA: v1
+States: 7
+Start: 0
+AP: 2 "b" "a"
+acc-name: all
+Acceptance: 0 t
+properties: trans-labels explicit-labels state-acc very-weak
+spot-state-player: 0 1 0 0 0 1 1
+--BODY--
+State: 0
+[1] 1
+[1] 2
+State: 1
+[0] 3
+[!0] 4
+State: 2
+[0] 5
+[!0] 6
+State: 3
+[t] 3
+State: 4
+[t] 4
+State: 5
+[t] 5
+State: 6
+[t] 6
+--END--""")