sat_minimize: improve logs and document Python bindings

* spot/priv/satcommon.cc, spot/priv/satcommon.hh: Make it possible to
set the log file without setting the environment variable.  Adjust
print_log to take the input state and print it as a new column.
* spot/twaalgos/dtbasat.cc, spot/twaalgos/dtwasat.cc: Adjust all
calls to print_log.  Fix log output for incremental approaches.
Prefer purge_unreachable_states() over stats_reachable().  Do
not call scc_filter() on colored automata.
* spot/twaalgos/dtwasat.hh: Document the new "log" option.
* NEWS: Mention the changes.
* tests/python/satmin.ipynb: New file.
* tests/Makefile.am: Add it.
* doc/org/satmin.org, doc/org/tut.org: Link to it.
* doc/org/satmin.org, bin/man/spot-x.x: Adjust description
of CSV files.
* bench/dtgbasat/gen.py, bench/dtgbasat/tabl.pl,
bench/dtgbasat/tabl1.pl, bench/dtgbasat/tabl2.pl,
bench/dtgbasat/tabl3.pl, bench/dtgbasat/tabl4.pl: Adjust for
the new column.
* spot/misc/satsolver.cc, spot/misc/satsolver.hh (stats): Make it
const.
* python/spot/__init__.py (sat_minimize): Add display_log and
return_log options.
* tests/python/ipnbdoctest.py: Adjust to not compare SAT-minimization
logs as they contain timings.

NEWS

@@ -40,6 +40,15 @@ New in spot 2.5.2.dev (not yet released)
     example, the translation of GF(a <-> XXb) to transition-based
     Büchi went from 9 to 5 states using that construction.
 
+  - Slightly improved log output for the SAT-based minimization
+    functions.  The CSV log files now include an additional column
+    with the size of the reference automaton, and they now have a
+    header line.  These log files give more details and are more
+    accurate in the case of incremental SAT-solving.  The python
+    bindings for sat_minimize() now have a display_log and return_log
+    options; there are demonstrated on the new
+    https://spot.lrde.epita.fr/ipynb/satmin.html page.
+
   Bugs fixed:
 
   - "autfilt --cobuchi --small/--det" would turn a transition-based

bench/dtgbasat/gen.py

@@ -1,5 +1,5 @@
 #!/usr/bin/env python3
-# Copyright (C) 2016, 2017 Laboratoire de Recherche et Développement de
+# Copyright (C) 2016-2018 Laboratoire de Recherche et Développement de
 # l'Epita (LRDE).
 #
 # This file is part of Spot, a model checking library.
@@ -272,7 +272,7 @@ def get_last_successful(n, category, pattern):
                    + '.satlog', 'r')
         log_csv = csv.reader(log)
         for line in log_csv:
-            min_val = line[1]
+            min_val = line[2]
         return '$\\le$' + min_val
     except Exception:
         return ''

bench/dtgbasat/tabl.pl

@@ -79,7 +79,7 @@ sub getlastsuccesful($$)
     while (my $line = <LOG>)
     {
 	my @f = split(/,/, $line);
-	$min = $f[1] if $f[1] ne '';
+	$min = $f[2] if $f[2] ne '';
     }
     $min = ", \$\\le\$$min" if $min ne "";
     return $min;

bench/dtgbasat/tabl1.pl

@@ -72,7 +72,7 @@ sub getlastsuccesful($$)
     while (my $line = <LOG>)
     {
 	my @f = split(/,/, $line);
-	$min = $f[1] if $f[1] ne '';
+	$min = $f[2] if $f[2] ne '';
     }
     $min = ", \$\\le\$$min" if $min ne "";
     return $min;

bench/dtgbasat/tabl2.pl

@@ -91,7 +91,7 @@ sub getlastsuccesful($$)
     while (my $line = <LOG>)
     {
 	my @f = split(/,/, $line);
-	$min = $f[1] if $f[1] ne '';
+	$min = $f[2] if $f[2] ne '';
     }
     $min = ", \$\\le\$$min" if $min ne "";
     return $min;

bench/dtgbasat/tabl3.pl

@@ -93,7 +93,7 @@ sub getlastsuccesful($$)
     while (my $line = <LOG>)
     {
 	my @f = split(/,/, $line);
-	$min = $f[1] if $f[1] ne '';
+	$min = $f[2] if $f[2] ne '';
     }
     $min = ", \$\\le\$$min" if $min ne "";
     return $min;

bench/dtgbasat/tabl4.pl

@@ -92,7 +92,7 @@ sub getlastsuccesful($$)
     while (my $line = <LOG>)
     {
 	my @f = split(/,/, $line);
-	$min = $f[1] if $f[1] ne '';
+	$min = $f[2] if $f[2] ne '';
     }
     $min = ", \$\\le\$$min" if $min ne "";
     return $min;

bin/man/spot-x.x

@@ -150,13 +150,14 @@ to the recurrence (or the persistence) class.
 \fBSPOT_SATLOG\fR
 If set to a filename, the SAT-based minimization routines will append
 statistics about each iteration to the named file.  Each line lists
-the following comma-separated values: requested number of states,
+the following comma-separated values: input number of states, target
-number of reachable states in the output, number of edges in the
+number of states, number of reachable states in the output, number of
-output, number of transitions in the output, number of variables in
+edges in the output, number of transitions in the output, number of
-the SAT problem, number of clauses in the SAT problem, user time for
+variables in the SAT problem, number of clauses in the SAT problem,
-encoding the SAT problem, system time for encoding the SAT problem,
+user time for encoding the SAT problem, system time for encoding the
-user time for solving the SAT problem, system time for solving the SAT
+SAT problem, user time for solving the SAT problem, system time for
-problem.
+solving the SAT problem, automaton produced at this step in HOA
+format.
 
 .TP
 \fBSPOT_SATSOLVER\fR

doc/org/satmin.org

@@ -29,7 +29,7 @@ Let us first state a few facts about this minimization procedure.
    use state-based acceptance. (They simply restrict all the outgoing
    transitions of a state to belong to the same acceptance sets.)
 4) Spot is built using PicoSAT call_version()[:results raw].
-   This solver was chosen for its performances, simplicity of
+   This solver was chosen for its performance, simplicity of
    integration and license compatibility.  However, it is
    still possible to use an external SAT solver (as described below).
 5) [[file:ltl2tgba.org][=ltl2tgba=]] and [[file:dstar2tgba.org][=dstar2tgba=]] will always try to output an automaton.
@@ -730,48 +730,52 @@ export SPOT_SATLOG=stats.csv
 ltlfilt -f 'Ga R (F!b & (c U b))' -l |
 ltl2dstar --ltl2nba=spin:ltl2tgba@-Ds - - |
 dstar2tgba -D -x sat-minimize,sat-acc=2 --stats='input(states=%S) output(states=%s, acc-sets=%a, det=%d)'
+echo ==== stats.csv ====
 cat stats.csv
 #+END_SRC
 #+RESULTS:
 : input(states=11) output(states=5, acc-sets=2, det=1)
-: 9,9,36,72,44064,9043076,616,18,258,24
+: ==== stats.csv ====
-: 8,7,29,56,19712,3493822,236,9,135,6
+: input.states,target.states,reachable.states,edges,transitions,variables,clauses,enc.user,enc.sys,sat.user,sat.sys,automaton
-: 6,6,25,48,10512,1362749,97,4,42,2
+: 10,5,,,,13600,1543042,59,3,187,0,
-: 5,,,,7200,784142,65,2,40,2
+: 10,7,7,33,56,26656,4247441,162,7,775,0,"HOA: v1 States: 7 Start: 0 AP: 3 ""a"" ""b"" ""c"" acc-name: generalized-Buchi 2 Acceptance: 2 Inf(0)&Inf(1) properties: trans-labels explicit-labels trans-acc complete deterministic --BODY-- State: 0 [!0&!1&2] 0 {1} [!0&1] 0 {0} [!0&!1&!2] 1 {0} [0&!1&!2] 1 [0&!1&2] 2 {1} [0&1&!2] 4 [0&1&2] 4 {0} State: 1 [0&!1] 1 {0} [!0&!1&!2 | 0&1] 1 [!0&1 | !0&2] 3 {0} State: 2 [!0&!1&2] 0 {1} [!0&1] 0 {0 1} [!0&!1&!2] 1 [0&!1&2] 2 [0&!1&!2] 3 {1} [0&1] 5 {0 1} State: 3 [!1&!2] 3 [1 | 2] 3 {0} State: 4 [!0&!1&2] 0 {0 1} [!0&1] 0 {0} [!0&!1&!2] 1 [0&1] 4 {0} [0&!1&2] 5 {0} [0&!1&!2] 6 State: 5 [!0&1 | !0&2] 0 {0 1} [!0&!1&!2] 1 [0&1 | 0&2] 5 {0 1} [0&!1&!2] 6 {0} State: 6 [!0&!1&!2] 1 [!0&1&!2] 1 {0 1} [!0&1&2] 1 {1} [!0&!1&2] 3 {0 1} [0] 6 {0 1} --END--"
+: 7,6,6,26,48,10512,1376507,50,0,269,0,"HOA: v1 States: 6 Start: 0 AP: 3 ""a"" ""b"" ""c"" acc-name: generalized-Buchi 2 Acceptance: 2 Inf(0)&Inf(1) properties: trans-labels explicit-labels trans-acc complete deterministic --BODY-- State: 0 [!0&!1&2] 0 {1} [!0&1] 0 {0} [!0&!1&!2] 1 [0&!1&!2] 1 {0 1} [0&!1&2] 2 {1} [0&1] 3 {0} State: 1 [t] 1 State: 2 [!0&!1&2] 0 {1} [!0&1] 0 {0} [!1&!2] 1 [0&!1&2] 2 {1} [0&1] 4 {1} State: 3 [!0&!1&2] 0 {1} [!0&1] 0 [!0&!1&!2] 1 [0&1] 3 [0&!1&2] 4 {1} [0&!1&!2] 5 {1} State: 4 [!0&!1&2 | !0&1&!2] 0 {0 1} [!0&1&2] 0 {0} [!0&!1&!2] 1 [0&1 | 0&2] 4 {0 1} [0&!1&!2] 5 State: 5 [!0&!1&!2] 1 [!0&1 | !0&2] 1 {0 1} [0] 5 {0 1} --END--"
 
 The generated CSV file use the following columns:
-- the n passed to the SAT-based minimization algorithm
+- =input.states=: the number of states of the reference automaton at this step
+- =target.states=: the n passed to the SAT-based minimization algorithm
   (it means the input automaton had n+1 states)
-- number of reachable states in the output of
+- =reachable.states=: number of reachable states in the output of
-  the minimization.
+  the minimization (with any luck this can be smaller than =target.states=)
-- number of edges in the output
+- =edges=, =transitions=: number of edges or transitions in the output
-- number of transitions
+- =variables=, =clauses=: size of the SAT problem
-- number of variables in the SAT problem
+- =enc.user=, =enc.sys=: user and system time for encoding the SAT problem
-- number of clauses in the SAT problem
+- =sat.user=, =sat.sys=: user and system time for solving the SAT problem
-- user time for encoding the SAT problem
+- =automaton=: the automaton produced in HOA format.
-- system time for encoding the SAT problem
-- user time for solving the SAT problem
-- system time for solving the SAT problem
-- automaton produced
 
-Times are measured with the times() function, and expressed
+Times are measured with the times() function, and expressed in ticks
-in ticks (usually: 1/100 of seconds).
+(usually: 1/100 of seconds).  The encoding of the automaton in the CSV
+file follows RFC4180 in escaping double-quote by doubling them.
 
-In the above example, the input DRA had 11
+In the above example, the DRA produced by =ltl2dstar= had 11 states.
-states.  In the first line of the =stats.csv= file, you can see the
+In the first line of the =stats.csv= file, you can see the
-minimization function searching for a 9 state DTBA and obtaining a
+minimization function had a 10-state input, which means that
-8-state solution.  (Since the minimization function searched for a
+=dstar2tgba= first reduced the 11-state (complete) DRA into a 10-state
-9-state DTBA, it means it received a 10-state complete DTBA, so the
+(complete) DBA before calling the SAT-based minimization.  This first
-processings performed before the minimization procedure managed to
+line shows the SAT-based minimization for a (complete) 5-state DTGBA
-convert the 11-state DRA into a 10-state DTBA.)  Starting from the
+and failing to find one.  Then on the next line it looks for a 7-state
-8-state solution, it looked for (and found) a 7-state solution, and
+solution, finds one.  Finally, it finds a (complete) 6-state solution,
-then a 6-state solution.  The search for a 5-state complete DTBA
+now using the 7-state version as reference automaton to further
-failed.  The final output is reported with 5 states, because by
+simplify the problem.
-default we output trim automata. If the =--complete= option had been
-given, the useless sink state would have been kept and the output
-automaton would have 6 states.
 
+The final output is reported with 5 states, because by default we
+output trim automata. If the =--complete= option had been given, the
+useless sink state would have been kept and the output automaton would
+have 6 states.
 
 #+BEGIN_SRC sh :results silent :exports results
 rm -f output.hoa output2.hoa
 #+END_SRC
+* Python interface
+
+See the [[https://spot.lrde.epita.fr/ipynb/satmin.html][=satmin.ipynb=]] notebook.

doc/org/tut.org

@@ -82,3 +82,4 @@ real notebooks instead.
 - [[https://spot.lrde.epita.fr/ipynb/atva16-fig2b.html][=atva16-fig2b.ipynb=]] second example from our [[https://www.lrde.epita.fr/~adl/dl/adl/duret.16.atva2.pdf][ATVA'16 tool paper]].
 - [[https://spot.lrde.epita.fr/ipynb/alternation.html][=alternation.ipynb=]] examples of alternating automata.
 - [[https://spot.lrde.epita.fr/ipynb/stutter-inv.html][=stutter-inv.ipynb=]] working with stutter-invariant formulas properties.
+- [[https://spot.lrde.epita.fr/ipynb/satmin.html][=satmin.ipynb=]] Python interface for [[file:satmin.org][SAT-based minimization of deterministic ω-automata]].

python/spot/__init__.py

@@ -33,7 +33,7 @@ from spot.aux import \
 import subprocess
 import os
 import signal
-
+import tempfile
 
 # The parrameters used by default when show() is called on an automaton.
 _show_default = None
@@ -927,7 +927,8 @@ for fun in ['remove_x', 'relabel', 'relabel_bse',
 def sat_minimize(aut, acc=None, colored=False,
                  state_based=False, states=0,
                  max_states=0, sat_naive=False, sat_langmap=False,
-                 sat_incr=0, sat_incr_steps=0):
+                 sat_incr=0, sat_incr_steps=0,
+                 display_log=False, return_log=False):
     args=''
     if acc is not None:
         if type(acc) is not str:
@@ -950,9 +951,25 @@ def sat_minimize(aut, acc=None, colored=False,
     if sat_incr:
         args += ',sat-incr=' + str(sat_incr)
         args += ',sat-incr-steps=' + str(sat_incr_steps)
-
     from spot.impl import sat_minimize as sm
-    return sm(aut, args, state_based)
+
+    if display_log or return_log:
+        import pandas as pd
+        with tempfile.NamedTemporaryFile(dir='.', suffix='.satlog') as t:
+            args += ',log="{}"'.format(t.name)
+            aut = sm(aut, args, state_based)
+            dfrm = pd.read_csv(t.name, dtype=object)
+            if display_log:
+                # old versions of ipython do not import display by default
+                from IPython.display import display
+                del dfrm['automaton']
+                display(dfrm)
+            if return_log:
+                return aut, dfrm
+            else:
+                return aut
+    else:
+        return sm(aut, args, state_based)
 
 
 def parse_word(word, dic=_bdd_dict):

spot/misc/satsolver.cc

@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2013, 2014, 2015, 2016, 2017 Laboratoire de Recherche et
+// Copyright (C) 2013-2018 Laboratoire de Recherche et Développement
-// Développement de l'Epita.
+// de l'Epita.
 //
 // This file is part of Spot, a model checking library.
 //
@@ -209,7 +209,7 @@ namespace spot
     return nvars_;
   }
 
-  std::pair<int, int> satsolver::stats()
+  std::pair<int, int> satsolver::stats() const
   {
     return std::make_pair(get_nb_vars(), get_nb_clauses());
   }

spot/misc/satsolver.hh

@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2013, 2017 Laboratoire de Recherche et Développement
+// Copyright (C) 2013, 2017, 2018 Laboratoire de Recherche et
-// de l'Epita.
+// Développement de l'Epita.
 //
 // This file is part of Spot, a model checking library.
 //
@@ -95,7 +95,7 @@ namespace spot
     int get_nb_vars() const;
 
     /// \brief Returns std::pair<nvars, nclauses>;
-    std::pair<int, int> stats();
+    std::pair<int, int> stats() const;
 
     /// \brief Add a comment.
     /// It should be used only in debug mode after providing a satsolver.

spot/priv/satcommon.cc

@@ -142,50 +142,63 @@ namespace spot
     return buffer.str();
   }
 
+  static std::string satlog_filename;
+
   void
-  print_log(timer_map& t, int target_state_number,
+  set_satlog_filename(const std::string& filename)
-            twa_graph_ptr& res, satsolver& solver)
+  {
+    satlog_filename = filename;
+  }
+
+  void
+  print_log(timer_map& t,
+            int input_state_number, int target_state_number,
+            const twa_graph_ptr& res, const satsolver& solver)
   {
     // Always copy the environment variable into a static string,
     // so that we (1) look it up once, but (2) won't crash if the
     // environment is changed.
-    static std::string log = []()
+    static std::string envlog = []()
       {
         auto s = getenv("SPOT_SATLOG");
         return s ? s : "";
       }();
-    if (!log.empty())
+    const std::string log = satlog_filename.empty() ? envlog : satlog_filename;
+    if (log.empty())
+      return;
+
+    std::ofstream out(log, std::ios_base::ate | std::ios_base::app);
+    out.exceptions(std::ifstream::failbit | std::ifstream::badbit);
+    if (out.tellp() == 0)
+      out <<
+        ("input.states,target.states,reachable.states,edges,transitions,"
+         "variables,clauses,enc.user,enc.sys,sat.user,sat.sys,automaton\n");
+
+    const timer& te = t.timer("encode");
+    const timer& ts = t.timer("solve");
+    out << input_state_number << ',' << target_state_number << ',';
+    if (res)
       {
-        std::fstream out(log,
+        twa_sub_statistics st = sub_stats_reachable(res);
-                         std::ios_base::app | std::ios_base::out);
+        out << st.states << ',' << st.edges << ',' << st.transitions;
-        out.exceptions(std::ifstream::failbit | std::ifstream::badbit);
-        const timer& te = t.timer("encode");
-        const timer& ts = t.timer("solve");
-        out << target_state_number << ',';
-        if (res)
-          {
-            twa_sub_statistics st = sub_stats_reachable(res);
-            out << st.states << ',' << st.edges << ',' << st.transitions;
-          }
-        else
-          {
-            out << ",,";
-          }
-        std::pair<int, int> s = solver.stats(); // sat_stats
-        out << ','
-            << s.first << ',' << s.second << ','
-            << te.utime() + te.cutime() << ','
-            << te.stime() + te.cstime() << ','
-            << ts.utime() + ts.cutime() << ','
-            << ts.stime() + ts.cstime() << ",\"";
-        if (res)
-        {
-          std::ostringstream f;
-          print_hoa(f, res, "l");
-          escape_rfc4180(out, f.str());
-        }
-        out << "\"\n";
       }
+    else
+      {
+        out << ",,";
+      }
+    std::pair<int, int> s = solver.stats();
+    out << ',' << s.first << ',' << s.second << ','
+        << te.utime() + te.cutime() << ','
+        << te.stime() + te.cstime() << ','
+        << ts.utime() + ts.cutime() << ','
+        << ts.stime() + ts.cstime() << ',';
+    if (res)
+      {
+        std::ostringstream f;
+        print_hoa(f, res, "l");
+        escape_rfc4180(out << '"', f.str()) << '"';
+      }
+    out << std::endl;
   }
 
   int

spot/priv/satcommon.hh

@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2013, 2014, 2015 Laboratoire de Recherche et
+// Copyright (C) 2013-2016, 2018 Laboratoire de Recherche et
 // Développement de l'Epita.
 //
 // This file is part of Spot, a model checking library.
@@ -231,11 +231,17 @@ public:
         unsigned dst_ref);
   };
 
-  /// \brief Good old function that prints log is SPOT_SATLOG. It has been
+  /// \brief Give a filename to save the log of the SAT minimization.
-  /// moved from spot/twaalgos/dt*asat.cc files.
+  ///
-  void
+  /// This has priority over the SPOT_SATLOG environment variable.
-  print_log(timer_map& t, int target_state_number, twa_graph_ptr& res,
+  /// Pass en empty string to reset it.
-            satsolver& solver);
+  void set_satlog_filename(const std::string& filename);
+
+  /// \brief Prints a line in the SPOT_SATLOG file.
+  void print_log(timer_map& t,
+                 int input_state_number,
+                 int target_state_number, const twa_graph_ptr& res,
+                 const satsolver& solver);
 
   /// \brief Returns the number of distinct values containted in a vector.
   int

spot/twaalgos/dtbasat.cc

@@ -28,7 +28,6 @@
 #include <spot/twaalgos/dtbasat.hh>
 #include <spot/twaalgos/langmap.hh>
 #include <spot/twaalgos/sccinfo.hh>
-#include <spot/twaalgos/stats.hh>
 
 // If you set the SPOT_TMPKEEP environment variable the temporary
 // file used to communicate with the sat solver will be left in
@@ -708,6 +707,7 @@ namespace spot
       }
 #endif
       a->merge_edges();
+      a->purge_unreachable_states();
       return a;
     }
   }
@@ -744,7 +744,8 @@ namespace spot
     if (!solution.second.empty())
       res = sat_build(solution.second, d, a, state_based);
 
-    print_log(t, target_state_number, res, solver); // If SPOT_SATLOG is set.
+    print_log(t, a->num_states(),
+              target_state_number, res, solver); // If SPOT_SATLOG is set.
 
     trace << "dtba_sat_synthetize(...) = " << res << '\n';
     return res;
@@ -754,7 +755,6 @@ namespace spot
   dichotomy_dtba_research(int max,
                           dict& d,
                           satsolver& solver,
-                          timer_map& t1,
                           const_twa_graph_ptr& prev,
                           bool state_based)
   {
@@ -768,36 +768,47 @@ namespace spot
       target = (max + min) / 2;
       trace << "min:" << min << ", max:" << max << ", target:" << target
         << '\n';
-
+      timer_map t1;
+      t1.start("encode");
       solver.assume(d.nvars + target);
+      t1.stop("encode");
       trace << "solver.assume(" << d.nvars + target << ")\n";
-
+      t1.start("solve");
       satsolver::solution_pair solution = solver.get_solution();
+      t1.stop("solve");
       if (solution.second.empty())
       {
         trace << "UNSAT\n";
         max = target;
+        print_log(t1, prev->num_states(), d.cand_size - target,
+                  nullptr, solver);
       }
       else
       {
         trace << "SAT\n";
         res = sat_build(solution.second, d, prev, state_based);
-        min = d.cand_size - stats_reachable(res).states + 1;
+        min = d.cand_size - res->num_states() + 1;
+        print_log(t1, prev->num_states(), d.cand_size - target,
+                  res, solver);
       }
     }
 
     trace << "End with max:" << max << ", min:" << min << '\n';
     if (!res)
     {
-      trace << "All assumptions are UNSAT, let's try without...";
+      trace << "All assumptions are UNSAT, let's try without...\n";
+      timer_map t1;
+      t1.start("encode");
+      t1.stop("encode");
+      t1.start("solve");
+      t1.stop("solve");
       satsolver::solution_pair solution = solver.get_solution();
       trace << (solution.second.empty() ? "UNSAT!\n" : "SAT\n");
       res = solution.second.empty() ? nullptr :
         sat_build(solution.second, d, prev, state_based);
+      print_log(t1, prev->num_states(), d.cand_size - target, res, solver);
     }
 
-    t1.stop("solve");
-    print_log(t1, d.cand_size - target, res, solver); // SPOT_SATLOG.
     return res ? res : std::const_pointer_cast<spot::twa_graph>(prev);
   }
 
@@ -816,8 +827,7 @@ namespace spot
 
     const_twa_graph_ptr prev = a;
     dict d;
-    d.cand_size = (max_states < 0) ?
+    d.cand_size = (max_states < 0) ? prev->num_states() - 1 : max_states;
-      stats_reachable(prev).states - 1 : max_states;
     if (d.cand_size == 0)
       return nullptr;
 
@@ -829,7 +839,7 @@ namespace spot
     while (next && d.cand_size > 0)
     {
       // Warns the satsolver of the number of assumptions.
-      int n_assumptions = (int) d.cand_size < sat_incr_steps ?
+      int n_assumptions = (int) d.cand_size <= sat_incr_steps ?
         d.cand_size - 1 : sat_incr_steps;
       trace << "number of assumptions:" << n_assumptions << '\n';
       satsolver solver;
@@ -867,34 +877,36 @@ namespace spot
           solver.add({-assume_lit, assume_lit - 1, 0});
         }
       }
-      t1.stop("encode");
-
-      t1.start("solve");
       if (n_assumptions)
       {
         trace << "solver.assume(" << d.nvars + n_assumptions << ")\n";
         solver.assume(d.nvars + n_assumptions);
       }
+      t1.stop("encode");
+      t1.start("solve");
       satsolver::solution_pair solution = solver.get_solution();
+      t1.stop("solve");
 
       if (solution.second.empty() && n_assumptions) // UNSAT
       {
+        print_log(t1, prev->num_states(),
+                  d.cand_size - n_assumptions, nullptr, solver);
         trace << "UNSAT\n";
-        return dichotomy_dtba_research(n_assumptions, d, solver, t1, prev,
+        return dichotomy_dtba_research(n_assumptions, d, solver,
-                                       state_based);
+                                       prev, state_based);
       }
 
-      t1.stop("solve");
       trace << "SAT, restarting from zero\n";
       next = solution.second.empty() ? nullptr :
         sat_build(solution.second, d, prev, state_based);
-      print_log(t1, d.cand_size - n_assumptions, next, solver); // SPOT_SATLOG.
+      print_log(t1, prev->num_states(),
+                d.cand_size - n_assumptions, next, solver);
 
       if (next)
       {
         prev = next;
         d = dict();
-        d.cand_size = stats_reachable(prev).states - 1;
+        d.cand_size = prev->num_states() - 1;
         if (d.cand_size == 0)
           next = nullptr;
       }
@@ -912,8 +924,7 @@ namespace spot
         (": dtba_sat_minimize_incr() can only work with Büchi acceptance.");
     const_twa_graph_ptr prev = a;
     dict d;
-    d.cand_size = (max_states < 0) ?
+    d.cand_size = (max_states < 0) ? prev->num_states() - 1 : max_states;
-      stats_reachable(prev).states - 1 : max_states;
     if (d.cand_size == 0)
       return nullptr;
 
@@ -937,7 +948,7 @@ namespace spot
       t1.stop("solve");
       next = solution.second.empty() ? nullptr :
         sat_build(solution.second, d, prev, state_based);
-      print_log(t1, d.cand_size, next, solver); // If SPOT_SATLOG is set.
+      print_log(t1, prev->num_states(), d.cand_size, next, solver);
 
       trace << "First iteration done\n";
 
@@ -950,27 +961,27 @@ namespace spot
       for (int k = 0; next && d.cand_size > 0 && (naive || k < sat_incr_steps);
            ++k)
       {
-        t1.start("encode");
         prev = next;
-        int reach_states = stats_reachable(prev).states;
+        int reach_states = prev->num_states();
         cnf_comment("Next iteration: ", reach_states - 1, "\n");
-
         trace << "Encoding the deletion of state " << reach_states - 1 << '\n';
 
+        timer_map t2;
+        t2.start("encode");
         // Add new constraints.
         for (unsigned i = reach_states - 1; i < d.cand_size; ++i)
           for (unsigned l = 0; l < alpha_size; ++l)
             for (unsigned j = 0; j < orig_cand_size; ++j)
               solver.add({-d.transid(j, l, i), 0});
-
+        t2.stop("encode");
         d.cand_size = reach_states - 1;
-        t1.stop("encode");
+        t2.start("solve");
-        t1.start("solve");
         satsolver::solution_pair solution = solver.get_solution();
-        t1.stop("solve");
+        t2.stop("solve");
         next = solution.second.empty() ? nullptr :
           sat_build(solution.second, d, prev, state_based);
-        print_log(t1, d.cand_size, next, solver); // If SPOT_SATLOG is set.
+        print_log(t2, prev->num_states(),
+                  d.cand_size, next, solver);
       }
 
       if (next)
@@ -978,7 +989,7 @@ namespace spot
         trace << "Starting from scratch\n";
         prev = next;
         d = dict();
-        d.cand_size = stats_reachable(prev).states - 1;
+        d.cand_size = prev->num_states() - 1;
         if (d.cand_size == 0)
           next = nullptr;
       }
@@ -991,8 +1002,7 @@ namespace spot
   dtba_sat_minimize(const const_twa_graph_ptr& a,
                     bool state_based, int max_states)
   {
-    int n_states = (max_states < 0) ?
+    int n_states = (max_states < 0) ? a->num_states() : max_states + 1;
-      stats_reachable(a).states : max_states + 1;
 
     twa_graph_ptr prev = nullptr;
     for (;;)
@@ -1002,7 +1012,7 @@ namespace spot
         if (!next)
           return prev;
         else
-          n_states = stats_reachable(next).states;
+          n_states = next->num_states();
         prev = next;
       }
     SPOT_UNREACHABLE();
@@ -1014,7 +1024,7 @@ namespace spot
   {
     trace << "Dichomoty\n";
     if (max_states < 0)
-      max_states = stats_reachable(a).states - 1;
+      max_states = a->num_states() - 1;
     int min_states = 1;
     if (langmap)
     {
@@ -1036,7 +1046,7 @@ namespace spot
         else
           {
             prev = next;
-            max_states = stats_reachable(next).states - 1;
+            max_states = next->num_states() - 1;
           }
       }
     return prev;

spot/twaalgos/dtwasat.cc

@@ -36,7 +36,6 @@
 #include <spot/twaalgos/sbacc.hh>
 #include <spot/twaalgos/sccfilter.hh>
 #include <spot/twaalgos/sccinfo.hh>
-#include <spot/twaalgos/stats.hh>
 
 // If you set the SPOT_TMPKEEP environment variable the temporary
 // file used to communicate with the sat solver will be left in
@@ -624,7 +623,7 @@ namespace spot
         {
           unsigned nacc = d.cand_nacc;
           cnf_comment("transitions belong to exactly one of the", nacc,
-                      "acceptance set\n");
+                      "acceptance sets\n");
           for (unsigned l = 0; l < alpha_size; ++l)
             for (unsigned q1 = 0; q1 < d.cand_size; ++q1)
               for (unsigned q2 = 0; q2 < d.cand_size; ++q2)
@@ -982,6 +981,7 @@ namespace spot
 #endif
 
       a->merge_edges();
+      a->purge_unreachable_states();
       return a;
     }
   }
@@ -1023,7 +1023,7 @@ namespace spot
     if (!solution.second.empty())
       res = sat_build(solution.second, d, a, state_based);
 
-    print_log(t, target_state_number, res, solver); // if SPOT_SATLOG is set.
+    print_log(t, a->num_states(), target_state_number, res, solver);
 
     trace << "dtwa_sat_synthetize(...) = " << res << '\n';
     return res;
@@ -1066,7 +1066,6 @@ namespace spot
   dichotomy_dtwa_research(int max,
                           dict& d,
                           satsolver& solver,
-                          timer_map& t1,
                           const_twa_graph_ptr& prev,
                           bool state_based)
   {
@@ -1081,35 +1080,46 @@ namespace spot
       trace << "min:" << min << ", max:" << max << ", target:" << target
         << '\n';
 
+      timer_map t1;
+      t1.start("encode");
       solver.assume(d.nvars + target);
+      t1.stop("encode");
       trace << "solver.assume(" << d.nvars + target << ")\n";
-
+      t1.start("solve");
       satsolver::solution_pair solution = solver.get_solution();
+      t1.stop("solve");
       if (solution.second.empty())
       {
         trace << "UNSAT\n";
         max = target;
+        print_log(t1, prev->num_states(), d.cand_size - target,
+                  nullptr, solver);
       }
       else
       {
         trace << "SAT\n";
         res = sat_build(solution.second, d, prev, state_based);
-        min = d.cand_size - stats_reachable(res).states + 1;
+        min = d.cand_size - res->num_states() + 1;
+        print_log(t1, prev->num_states(), d.cand_size - target,
+                  res, solver);
       }
     }
 
     trace << "End with max:" << max << ", min:" << min << '\n';
     if (!res)
     {
-      trace << "All assumptions are UNSAT, let's try without...";
+      trace << "All assumptions are UNSAT, let's try without...\n";
+      timer_map t1;
+      t1.start("encode");
+      t1.stop("encode");
+      t1.start("solve");
       satsolver::solution_pair solution = solver.get_solution();
+      t1.stop("solve");
       trace << (solution.second.empty() ? "UNSAT!\n" : "SAT\n");
       res = solution.second.empty() ? nullptr :
         sat_build(solution.second, d, prev, state_based);
+      print_log(t1, prev->num_states(), d.cand_size - target, res, solver);
     }
-
-    t1.stop("solve");
-    print_log(t1, d.cand_size - target , res, solver); // SPOT_SATLOG.
     return res ? res : std::const_pointer_cast<spot::twa_graph>(prev);
   }
 
@@ -1128,8 +1138,7 @@ namespace spot
 
     const_twa_graph_ptr prev = a;
     dict d(prev);
-    d.cand_size = (max_states < 0) ?
+    d.cand_size = (max_states < 0) ? prev->num_states() - 1 : max_states;
-      stats_reachable(prev).states - 1 : max_states;
     d.cand_nacc = target_acc_number;
     d.cand_acc = target_acc;
     if (d.cand_size == 0)
@@ -1144,9 +1153,9 @@ namespace spot
     while (next && d.cand_size > 0)
     {
       // Warns the satsolver of the number of assumptions.
-      int n_assumptions = (int) d.cand_size < sat_incr_steps ?
+      int n_assumptions = (int) d.cand_size <= sat_incr_steps ?
         d.cand_size - 1 : sat_incr_steps;
-      trace << "number of assumptions:" << n_assumptions << '\n';
+      trace << "number of assumptions: " << n_assumptions << '\n';
       satsolver solver;
       solver.set_nassumptions_vars(n_assumptions);
 
@@ -1182,35 +1191,39 @@ namespace spot
           solver.add({-assume_lit, assume_lit - 1, 0});
         }
       }
-      t1.stop("encode");
 
-      t1.start("solve");
       if (n_assumptions)
       {
         trace << "solver.assume(" << d.nvars + n_assumptions << ")\n";
         solver.assume(d.nvars + n_assumptions);
       }
+      t1.stop("encode");
+      t1.start("solve");
       satsolver::solution_pair solution = solver.get_solution();
+      t1.stop("solve");
 
       if (solution.second.empty() && n_assumptions) // UNSAT
       {
+        print_log(t1, prev->num_states(),
+                  d.cand_size - n_assumptions, nullptr, solver);
         trace << "UNSAT\n";
         twa_graph_ptr res = dichotomy_dtwa_research(n_assumptions, d, solver,
-                                                    t1, prev, state_based);
+                                                    prev, state_based);
         return res == a ? nullptr : res;
       }
 
-      t1.stop("solve");
       trace << "SAT, restarting from zero\n";
       next = solution.second.empty() ? nullptr :
         sat_build(solution.second, d, prev, state_based);
-      print_log(t1, d.cand_size - n_assumptions, next, solver); // SPOT_SATLOG.
+      print_log(t1, prev->num_states(),
+                d.cand_size - n_assumptions, next, solver);
 
       if (next)
       {
         prev = next;
+        trace << "prev has " << prev->num_states() << '\n';
         d = dict(prev);
-        d.cand_size = stats_reachable(prev).states - 1;
+        d.cand_size = prev->num_states() - 1;
         d.cand_nacc = target_acc_number;
         d.cand_acc = target_acc;
         if (d.cand_size == 0)
@@ -1233,7 +1246,7 @@ namespace spot
 
     dict d(prev);
     d.cand_size = (max_states < 0) ?
-      stats_reachable(prev).states - 1 : max_states;
+      prev->num_states() - 1 : max_states;
     d.cand_nacc = target_acc_number;
     d.cand_acc = target_acc;
     if (d.cand_size == 0)
@@ -1260,9 +1273,9 @@ namespace spot
       t1.stop("solve");
       next = solution.second.empty() ? nullptr :
         sat_build(solution.second, d, prev, state_based);
-      print_log(t1, d.cand_size, next, solver); // If SPOT_SATLOG is set.
+      print_log(t1, prev->num_states(), d.cand_size, next, solver);
 
-      trace << "First iteraton done\n";
+      trace << "First iteration done\n";
 
       // Compute the AP used.
       bdd ap = prev->ap_vars();
@@ -1273,27 +1286,25 @@ namespace spot
       for (int k = 0; next && d.cand_size > 0 && (naive || k < sat_incr_steps);
            ++k)
       {
-        t1.start("encode");
         prev = next;
-        int reach_states = stats_reachable(prev).states;
+        int reach_states = prev->num_states();
-        cnf_comment("Next iteration:", reach_states - 1, "\n");
-
         trace << "Encoding the deletion of state " << reach_states - 1 << '\n';
-
+        cnf_comment("Next iteration:", reach_states - 1, "\n");
+        timer_map t2;
+        t2.start("encode");
         // Add new constraints.
         for (unsigned i = reach_states - 1; i < d.cand_size; ++i)
           for (unsigned l = 0; l < alpha_size; ++l)
             for (unsigned j = 0; j < orig_cand_size; ++j)
               solver.add({-d.transid(j, l, i), 0});
-
+        t2.stop("encode");
         d.cand_size = reach_states - 1;
-        t1.stop("encode");
+        t2.start("solve");
-        t1.start("solve");
         solution = solver.get_solution();
-        t1.stop("solve");
+        t2.stop("solve");
         next = solution.second.empty() ? nullptr :
           sat_build(solution.second, d, prev, state_based);
-        print_log(t1, d.cand_size, next, solver); // If SPOT_SATLOG is set.
+        print_log(t2, prev->num_states(), d.cand_size, next, solver);
       }
 
       if (next)
@@ -1301,7 +1312,7 @@ namespace spot
         trace << "Starting from scratch\n";
         prev = next;
         d = dict(prev);
-        d.cand_size = stats_reachable(prev).states - 1;
+        d.cand_size = prev->num_states() - 1;
         d.cand_nacc = target_acc_number;
         d.cand_acc = target_acc;
         if (d.cand_size == 0)
@@ -1320,8 +1331,7 @@ namespace spot
                     bool state_based, int max_states,
                     bool colored)
   {
-    int n_states = (max_states < 0) ?
+    int n_states = (max_states < 0) ? a->num_states() : max_states + 1;
-      stats_reachable(a).states : max_states + 1;
 
     twa_graph_ptr prev = nullptr;
     for (;;)
@@ -1333,7 +1343,7 @@ namespace spot
         if (!next)
           return prev;
         else
-          n_states = stats_reachable(next).states;
+          n_states = next->num_states();
         prev = next;
       }
     SPOT_UNREACHABLE();
@@ -1348,7 +1358,7 @@ namespace spot
   {
     trace << "Dichotomy\n";
     if (max_states < 1)
-      max_states = stats_reachable(a).states - 1;
+      max_states = a->num_states() - 1;
     int min_states = 1;
     if (langmap)
     {
@@ -1373,7 +1383,7 @@ namespace spot
         else
           {
             prev = next;
-            max_states = stats_reachable(next).states - 1;
+            max_states = next->num_states() - 1;
           }
       }
     return prev;
@@ -1401,10 +1411,10 @@ namespace spot
     bool sat_langmap = om.get("sat-langmap", 0);
     int states = om.get("states", -1);
     int max_states = om.get("max-states", -1);
-    auto accstr = om.get_str("acc");
+    std::string accstr = om.get_str("acc");
     bool colored = om.get("colored", 0);
     int preproc = om.get("preproc", 3);
-
+    set_satlog_filename(om.get_str("log"));
 
     // Set default sat-incr-steps value if not provided and used.
     if (sat_incr == 1 && !sat_incr_steps) // Assume
@@ -1551,7 +1561,7 @@ namespace spot
 
     if (a)
       {
-        if (state_based)
+        if (state_based || colored)
           a = scc_filter_states(a);
         else
           a = scc_filter(a);

spot/twaalgos/dtwasat.hh

@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2013, 2014, 2015 Laboratoire de Recherche et
+// Copyright (C) 2013, 2014, 2015, 2018 Laboratoire de Recherche et
 // Développement de l'Epita.
 //
 // This file is part of Spot, a model checking library.
@@ -140,6 +140,7 @@ namespace spot
   ///                       fixed number of states before starting from scratch
   ///   incr < 0         // use satsolver incrementally, never restart
   ///   colored = 1      // build a colored TωA
+  ///   log = "filename"
   ///
   SPOT_API twa_graph_ptr
   sat_minimize(twa_graph_ptr aut, const char* opt, bool state_based = false);

tests/Makefile.am

@@ -342,6 +342,7 @@ TESTS_ipython = \
   python/product.ipynb \
   python/randaut.ipynb \
   python/randltl.ipynb \
+  python/satmin.ipynb \
   python/stutter-inv.ipynb \
   python/testingaut.ipynb \
   python/word.ipynb

tests/python/ipnbdoctest.py

@@ -118,6 +118,10 @@ def canonicalize(s, type, ignores):
     # Different Pandas versions produce different CSS styles (when there is a
     # style).
     s = re.sub(r'<style[ a-z]*>.*</style>\n', '', s, flags=re.DOTALL)
+    # Table that contains enc.user are log from the SAT-solver.  They contain
+    # timing result we cannot compare between runs.
+    s = re.sub(r'<table.*dataframe.*enc.user.*</table>', '<table></table>', s,
+               flags=re.DOTALL)
 
     for n, p in enumerate(ignores):
         s = re.sub(p, 'IGN{}'.format(n), s)
@@ -134,8 +138,11 @@ def canonical_dict(dict, ignores):
         dict['text'] = canonicalize(dict['text'], 'text', ignores)
 
     if 'data' in dict:
-        for k in dict['data']:
+        d = dict['data']
-            dict['data'][k] = canonicalize(dict['data'][k], k, ignores)
+        if "text/html" in d and "text/plain" in d:
+            del d["text/plain"]
+        for k in d:
+            d[k] = canonicalize(d[k], k, ignores)
 
     if ('ename' in dict and
             dict['ename'] == 'SystemExit' and dict['evalue'] == '77'):