simulation: try pulling marks instead of pushing them for sbacc input

Suggested by František Blahoudek.

* spot/twaalgos/simulation.cc: When doing forward simulation with
state-based acceptance as input but transition-based acceptance as
output, pull acceptance marks on incoming edges instead of pushing
them to outgoing edges.
* tests/core/dra2dba.test, tests/core/exclusive-tgba.test,
tests/core/ltlcrossce.test, tests/core/satmin3.test,
tests/core/sim3.test, tests/python/satmin.ipynb: Adjust test cases.
* NEWS: Mention the change.

NEWS

@@ -19,6 +19,13 @@ New in spot 2.7.1.dev  (not yet released)
   - twa::accepting_run() now works on automata using Fin in
     their acceptance condition.
 
+  - simulation-based reductions have learned a trick that sometimes
+    improve transition-based output when the input is state-based.
+    (The automaton output by 'ltl2tgba -B GFa | autfilt --small' now
+    has 1 state instead of 2 in previous versions.  Similarly,
+    'ltldo ltl2dstar -f 'GFa -> GFb' | autfilt --small' produces 1
+    state instead of 4.)
+
 New in spot 2.7.1 (2019-02-14)
 
   Build

spot/twaalgos/simulation.cc

@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2012-2018 Laboratoire de Recherche et Développement
+// Copyright (C) 2012-2019 Laboratoire de Recherche et Développement
 // de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -30,6 +30,7 @@
 #include <spot/twaalgos/sepsets.hh>
 #include <spot/twaalgos/isdet.hh>
 #include <spot/misc/bddlt.hh>
+#include <spot/twaalgos/hoa.hh>
 
 //  Simulation-based reduction, implemented using bdd-based signatures.
 //
@@ -151,10 +152,12 @@ namespace spot
         return acc_cond::mark_t(res.begin(), res.end());
       }
 
-      direct_simulation(const const_twa_graph_ptr& in)
+      direct_simulation(const const_twa_graph_ptr& in,
+                        std::vector<bdd>* implications = nullptr)
         : po_size_(0),
           all_class_var_(bddtrue),
-          original_(in)
+          original_(in),
+          record_implications_(implications)
       {
         if (!has_separate_sets(in))
           throw std::runtime_error
@@ -211,8 +214,62 @@ namespace spot
         else
           {
             a_ = make_twa_graph(in, twa::prop_set::all());
-            for (auto& t: a_->edges())
+
-              t.acc ^= all_inf;
+            // When we reduce automata with state-based acceptance to
+            // obtain transition-based acceptance, it helps to pull
+            // the state-based acceptance on the incoming edges
+            // instead of the outgoing edges.  A typical example
+            //
+            // ltl2tgba -B GFa | autfilt --small
+            //
+            // The two-state Büchi automaton generated for GFa will
+            // not be reduced to one state if we push the acceptance
+            // marks to the outgoing edges.  However it will be
+            // reduced to one state if we pull the acceptance to the
+            // incoming edges.
+            if (!Sba && !in->prop_state_acc().is_false()
+                && !record_implications_)
+              {
+                // common_out[i] is the set of acceptance set numbers common to
+                // all outgoing edges of state i.
+                std::vector<acc_cond::mark_t> common_out(ns);
+                scc_info si(a_, scc_info_options::NONE);
+                for (unsigned s = 0; s < ns; ++s)
+                  {
+                    bool first = true;
+                    for (auto& e : a_->out(s))
+                      {
+                        if (first)
+                          {
+                            common_out[s] = e.acc;
+                            first = false;
+                          }
+                        else if (common_out[s] != e.acc)
+                          {
+                            // If the automaton does not have
+                            // state-based acceptance, do not change
+                            // pull the marks.  Mark the input as
+                            // "not-state-acc" so that we remember
+                            // that.
+                            std::const_pointer_cast<twa_graph>(in)
+                              ->prop_state_acc(false);
+                            goto donotpull;
+                          }
+                      }
+                  }
+                // Pull the common outgoing sets to the incoming
+                // edges.  Doing so seems to favor cases where states
+                // can be merged.
+                for (auto& e : a_->edges())
+                  e.acc = ((e.acc - common_out[e.src]) | common_out[e.dst])
+                    ^ all_inf;
+              }
+            else
+              {
+              donotpull:
+                for (auto& t: a_->edges())
+                  t.acc ^= all_inf;
+              }
           }
         assert(a_->num_states() == size_a_);
 
@@ -310,10 +367,10 @@ namespace spot
       }
 
       // The core loop of the algorithm.
-      twa_graph_ptr run(std::vector<bdd>* implications = nullptr)
+      twa_graph_ptr run()
       {
         main_loop();
-        return build_result(implications);
+        return build_result();
       }
 
       // Take a state and compute its signature.
@@ -440,7 +497,7 @@ namespace spot
       }
 
       // Build the minimal resulting automaton.
-      twa_graph_ptr build_result(std::vector<bdd>* implications = nullptr)
+      twa_graph_ptr build_result()
       {
         twa_graph_ptr res = make_twa_graph(a_->get_dict());
         res->copy_ap_of(a_);
@@ -455,8 +512,8 @@ namespace spot
 
         auto* gb = res->create_namer<int>();
 
-        if (implications)
+        if (record_implications_)
-          implications->resize(bdd_lstate_.size());
+          record_implications_->resize(bdd_lstate_.size());
         // Create one state per class.
         for (auto& p: sorted_classes_)
           {
@@ -468,8 +525,8 @@ namespace spot
             // update state_mapping
             for (auto& st : p->second)
               (*state_mapping)[st] = s;
-            if (implications)
+            if (record_implications_)
-              (*implications)[s] = relation_[cl];
+              (*record_implications_)[s] = relation_[cl];
           }
 
         // Acceptance of states.  Only used if Sba && Cosimulation.
@@ -597,13 +654,30 @@ namespace spot
                   t.acc = acc;
               }
           }
+        if (!Sba && !Cosimulation && original_->prop_state_acc()
+            && !record_implications_)
+          {
+            // common_in[i] is the set of acceptance set numbers
+            // common to all incoming edges of state i.
+            std::vector<acc_cond::mark_t>
+              common_in(res->num_states(), res->acc().all_sets());
+            for (auto& e : res->edges())
+              common_in[e.dst] &= e.acc;
+            // Push the common incoming sets to the outgoing edges.
+            // Doing so cancels the preprocessing we did in the other
+            // direction, to prevent marks from moving around the
+            // automaton if we apply simulation several times, and to
+            // favor state-based acceptance.
+            for (auto& e : res->edges())
+              e.acc = (e.acc - common_in[e.dst]) | common_in[e.src];
+          }
 
         // If we recorded implications for the determinization
         // procedure, we should not remove unreachable states, as that
         // will invalidate the contents of the IMPLICATIONS vector.
         // It's OK not to purge the result, as the determinization
         // will only explore the reachable part anyway.
-        if (!implications)
+        if (!record_implications_)
           res->purge_unreachable_states();
 
         delete gb;
@@ -708,6 +782,8 @@ namespace spot
       automaton_size stat;
 
       const const_twa_graph_ptr original_;
+
+      std::vector<bdd>* record_implications_;
     };
 
   } // End namespace anonymous.
@@ -724,8 +800,8 @@ namespace spot
   simulation(const const_twa_graph_ptr& t,
              std::vector<bdd>* implications)
   {
-    direct_simulation<false, false> simul(t);
+    direct_simulation<false, false> simul(t, implications);
-    return simul.run(implications);
+    return simul.run();
   }
 
   twa_graph_ptr

tests/core/dra2dba.test

@@ -1,7 +1,7 @@
 #!/bin/sh
 # -*- coding: utf-8 -*-
-# Copyright (C) 2014, 2017 Laboratoire de Recherche et Développement
+# Copyright (C) 2014, 2017, 2019 Laboratoire de Recherche et
-# de l'Epita (LRDE).
+# Développement de l'Epita (LRDE).
 #
 # This file is part of Spot, a model checking library.
 #
@@ -330,4 +330,4 @@ Acc-Sig: +2
 EOF
 
 autcross 'dstar2tgba -D' --language-preserved -F in.dra --csv=out.csv
-grep '3,23,143,184,1,2,0,0,0$' out.csv
+grep '3,18,107,144,1,2,0,0,0$' out.csv

tests/core/exclusive-tgba.test

@@ -1,7 +1,7 @@
 #! /bin/sh
 # -*- coding: utf-8 -*-
-# Copyright (C) 2015, 2016, 2018 Laboratoire de Recherche et Développement de
+# Copyright (C) 2015-2016, 2018-2019 Laboratoire de Recherche et
-# l'Epita (LRDE).
+# Développement de l'Epita (LRDE).
 #
 # This file is part of Spot, a model checking library.
 #
@@ -166,13 +166,13 @@ diff out2 expected-simpl
 test "6,50,14" = `ltl2tgba -B -f 'F(Ga | (GFb <-> GFc))' --stats='%s,%t,%e'`
 test "6,24,12" = `ltl2tgba -B -f 'F(Ga | (GFb <-> GFc))' |
                   autfilt --exclusive-ap=a,b,c --stats='%s,%t,%e'`
-test "5,22,10" = `ltl2tgba -B -f 'F(Ga | (GFb <-> GFc))' |
+test "4,18,8" = `ltl2tgba -B -f 'F(Ga | (GFb <-> GFc))' |
    autfilt --small --exclusive-ap=a,b,c --stats='%s,%t,%e' --ap=3`
 # The final automaton has 3 atomic propositions before
 # simplifications, but only 2 after that.
 ltl2tgba -B -f 'F(Ga | (GFb <-> GFc))' |
   autfilt --small --exclusive-ap=a,b,c --simplify-ex --ap=3 > out
-test "5,21,10" = `autfilt out --stats='%s,%t,%e' --ap=2`
+test "4,17,8" = `autfilt out --stats='%s,%t,%e' --ap=2`
 
 
 # Issue #363.

tests/core/ltlcrossce.test

@@ -1,6 +1,6 @@
 #!/bin/sh
 # -*- coding: utf-8 -*-
-# Copyright (C) 2013, 2016 Laboratoire de Recherche et
+# Copyright (C) 2013, 2016, 2019 Laboratoire de Recherche et
 # Développement de l'Epita (LRDE).
 #
 # This file is part of Spot, a model checking library.
@@ -95,7 +95,7 @@ test `grep '^error:' errors | wc -l` = 4
 run 1 ltlcross --verbose -D -f 'G(F(p0) & F(G(!p1))) | (F(G(!p0)) & G(F(p1)))' \
   "ltl2tgba --lbtt %f >%T" "./fake %l >%T" 2> errors
 cat errors
-test `grep 'info:	Comp(' errors | wc -l` = 4
+test `grep 'info:	Comp(' errors | wc -l` = 3
 grep 'error: P0\*N1 is nonempty' errors
 grep 'error: P1\*N0 is nonempty' errors
 grep 'error: P1\*N1 is nonempty' errors

tests/core/satmin3.test

@@ -1,6 +1,6 @@
 #!/bin/sh
 # -*- coding: utf-8 -*-
-# Copyright (C) 2017 Laboratoire de Recherche et Développement
+# Copyright (C) 2017, 2019 Laboratoire de Recherche et Développement
 # de l'Epita (LRDE).
 #
 # This file is part of Spot, a model checking library.
@@ -24,7 +24,8 @@ set -e
 
 # Make sure the SPOT_SATSOLVER envar works.
 
-# DRA produced by ltl2dstar for GFp0 -> GFp1
+# DRA produced by ltl2dstar for GFp0 -> GFp1, but manually modified
+# so that simulation-based reduction do not reduce it to 1 state right away.
 cat >test.hoa <<EOF
 HOA: v1
 States: 4
@@ -35,7 +36,7 @@ Start: 0
 AP: 2 "p0" "p1"
 --BODY--
 State: 0 {0}
-1
+1  {1}  /* manual addition */
 0
 3
 2

tests/core/sim3.test

@@ -1,6 +1,6 @@
 #! /bin/sh
 # -*- coding: utf-8 -*-
-# Copyright (C) 2015, 2018 Laboratoire de Recherche et Développement
+# Copyright (C) 2015, 2018, 2019 Laboratoire de Recherche et Développement
 # de l'Epita (LRDE).
 #
 # This file is part of Spot, a model checking library.
@@ -47,7 +47,7 @@ State: 6 {0 3}
 --END--
 EOF
 
-test "`autfilt --small input --stats=%S,%s`" = 7,5
+test "`autfilt --small input --stats=%S,%s`" = 7,2
 
 autfilt -S --high --small input -H > out
 cat >expected <<EOF