sat: improve our algorithms

* src/tgbaalgos/dtbasat.cc, src/tgbaalgos/dtbasat.hh:
Rename dba_sat_minimize to dtba_sat_minimize.
Make it possible to produce state-based automata, and do
not output useless clauses.
* src/tgbaalgos/dtgbasat.cc, src/tgbaalgos/dtgbasat.hh:
likewise, but also add the possibility to set the
target number of states, as in dtba_sat_minimize.
* src/tgbaalgos/postproc.cc, src/tgbaalgos/postproc.hh:
Add new options for state-based computations and
setting acceptance and states number when using
dtgba_sat_minimize().
* src/tgbatest/ltl2tgba.cc: Adjust calls to
dtba_sat_minimize().
* src/tgbatest/satmin.test: Adjust calls.

src/tgbaalgos/dtbasat.cc

@@ -55,8 +55,6 @@
 #define dout while (0) out
 #endif
 
-
-
 namespace spot
 {
   namespace
@@ -216,9 +214,11 @@ namespace spot
       dict& d;
       int size_;
       bdd ap_;
+      bool state_based_;
     public:
-      filler_dfs(const tgba* aut, dict& d, bdd ap)
+      filler_dfs(const tgba* aut, dict& d, bdd ap, bool state_based)
-	:tgba_reachable_iterator_depth_first(aut), d(d), ap_(ap)
+	: tgba_reachable_iterator_depth_first(aut), d(d), ap_(ap),
+	  state_based_(state_based)
       {
 	d.nvars = 0;
       }
@@ -261,6 +261,12 @@ namespace spot
 	std::swap(d.state_to_int, seen);
 
 	for (int i = 1; i <= d.cand_size; ++i)
+	  {
+	    int transacc = -1;
+	    if (state_based_)
+	      // All outgoing transitions use the same acceptance variable.
+	      transacc = ++d.nvars;
+
 	    for (int j = 1; j <= d.cand_size; ++j)
 	      {
 		bdd all = bddtrue;
@@ -272,15 +278,18 @@ namespace spot
 		    transition t(i, one, j);
 		    d.transid[t] = ++d.nvars;
 		    d.revtransid.insert(dict::rev_map::value_type(d.nvars, t));
-		  d.transacc[t] = ++d.nvars;
+		    int ta = d.transacc[t] =
-		  d.revtransacc.insert(dict::rev_map::value_type(d.nvars, t));
+		      state_based_ ? transacc : ++d.nvars;
+		    d.revtransacc.insert(dict::rev_map::value_type(ta, t));
+		  }
 	      }
 	  }
       }
     };
 
     static
-    void dtba_to_sat(std::ostream& out, const tgba* ref, dict& d)
+    void dtba_to_sat(std::ostream& out, const tgba* ref, dict& d,
+		     bool state_based)
     {
       int nclauses = 0;
       int ref_size = 0;
@@ -291,7 +300,7 @@ namespace spot
 
       // Number all the SAT variable we may need.
       {
-	filler_dfs f(ref, d, ap);
+	filler_dfs f(ref, d, ap, state_based);
 	f.run();
 	ref_size = f.size();
       }
@@ -386,6 +395,9 @@ namespace spot
 		      state_pair p2(q2, dp);
 		      int succ = d.prodid[p2];
 
+		      if (pit->second == succ)
+			continue;
+
 		      dout << pit->first << " ∧ " << t << "δ → " << p2 << "\n";
 		      out << -pit->second << " " << -ti << " "
 			  << succ << " 0\n";
@@ -450,6 +462,9 @@ namespace spot
 			      path p2 = path(q1, q1p, q3, dp);
 			      int pid2 = d.pathid_ref[p2];
 
+			      if (pid1 == pid2)
+				continue;
+
 			      bdd all = it->current_condition();
 			      while (all != bddfalse)
 				{
@@ -523,6 +538,9 @@ namespace spot
 			      path p2 = path(q1, q1p, q3, dp);
 			      int pid2 = d.pathid_cand[p2];
 
+			      if (pid1 == pid2)
+				continue;
+
 			      bdd all = it->current_condition();
 			      while (all != bddfalse)
 				{
@@ -570,7 +588,8 @@ namespace spot
 
 
     static tgba_explicit_number*
-    sat_build(const std::string& solution, dict& satdict, const tgba* aut)
+    sat_build(const std::string& solution, dict& satdict, const tgba* aut,
+	      bool state_based)
     {
       bdd_dict* autdict = aut->get_dict();
       tgba_explicit_number* a = new tgba_explicit_number(autdict);
@@ -598,6 +617,7 @@ namespace spot
 #endif
 
       dout << "--- transition variables ---\n";
+      std::set<int> acc_states;
       for (;;)
 	{
 	  int v;
@@ -622,19 +642,35 @@ namespace spot
 	      last_sat_trans = &t->second;
 
 	      dout << v << "\t" << t->second << "δ\n";
+
+	      // Mark the transition as accepting if the source is.
+	      if (state_based
+		  && acc_states.find(t->second.src) != acc_states.end())
+		last_aut_trans->acceptance_conditions = acc;
 	    }
 	  else
 	    {
 	      t = satdict.revtransacc.find(v);
-	      // This assumes that the sat solvers output variables in
-	      // increasing order.
 	      if (t != satdict.revtransacc.end())
 		{
 		  dout << v << "\t" << t->second << "F\n";
-
 		  if (last_sat_trans && t->second == *last_sat_trans)
+		    {
+		      assert(!state_based);
+		      // This assumes that the SAT solvers output
+		      // variables in increasing order.
 		      last_aut_trans->acceptance_conditions = acc;
 		    }
+		  else if (state_based)
+		    {
+		      // Accepting translations actually correspond to
+		      // states and are announced before listing
+		      // outgoing transitions.  Again, this assumes
+		      // that the SAT solvers output variables in
+		      // increasing order.
+		      acc_states.insert(t->second.src);
+		    }
+		}
 	    }
 	}
 #if DEBUG
@@ -676,7 +712,8 @@ namespace spot
   }
 
   tgba_explicit_number*
-  dba_sat_minimize(const tgba* a, int target_state_number)
+  dtba_sat_minimize(const tgba* a, int target_state_number,
+		    bool state_based)
   {
     int ref_states =
       target_state_number == -1
@@ -709,7 +746,7 @@ namespace spot
 
 	std::fstream cnfs(cnf->name(),
 			  std::ios_base::trunc | std::ios_base::out);
-	dtba_to_sat(cnfs, a, *current);
+	dtba_to_sat(cnfs, a, *current, state_based);
 	cnfs.close();
 
 	out = create_tmpfile("dtba-sat-", ".out");
@@ -721,8 +758,16 @@ namespace spot
     if (target_state_number != -1)
       {
 	std::swap(current_solution, last_solution);
+	if (last_solution.empty())
+	  {
+	    last = 0;
+	    delete current;
+	  }
+	else
+	  {
 	    last = current;
 	  }
+      }
     else
       {
 	delete current;
@@ -740,7 +785,7 @@ namespace spot
       }
     else
       {
-	res = sat_build(last_solution, *last, a);
+	res = sat_build(last_solution, *last, a, state_based);
 	delete last;
       }
 

src/tgbaalgos/dtbasat.hh

@@ -36,11 +36,16 @@ namespace spot
   /// to its default value of -1, this function will attempt to build
   /// the smallest possible deterministic TBA is can produce.
   ///
+  /// \param state_based set to true to force all outgoing transitions
+  /// of a state to share the same acceptance condition, effectively
+  /// turning the TBA into a BA.
+  ///
   /// If no automaton with \a target_state_number states is found, or
   /// (in case <code>target_state_number == -1</code>) if no smaller
   /// automaton is found, then a null pointer is returned.
   SPOT_API tgba_explicit_number*
-  dba_sat_minimize(const tgba* a, int target_state_number = -1);
+  dtba_sat_minimize(const tgba* a, int target_state_number = -1,
+		    bool state_based = false);
 }
 
 #endif // SPOT_TGBAALGOS_DTBASAT_HH

src/tgbaalgos/dtgbasat.cc

@@ -297,9 +297,11 @@ namespace spot
       dict& d;
       int size_;
       bdd ap_;
+      bool state_based_;
     public:
-      filler_dfs(const tgba* aut, dict& d, bdd ap)
+      filler_dfs(const tgba* aut, dict& d, bdd ap, bool state_based)
-	:tgba_reachable_iterator_depth_first(aut), d(d), ap_(ap)
+	: tgba_reachable_iterator_depth_first(aut), d(d), ap_(ap),
+	  state_based_(state_based)
       {
 	d.nvars = 0;
 
@@ -395,6 +397,8 @@ namespace spot
 
 	std::swap(d.state_to_int, seen);
 
+	if (!state_based_)
+	  {
 	    for (int i = 1; i <= d.cand_size; ++i)
 	      for (int j = 1; j <= d.cand_size; ++j)
 		{
@@ -406,7 +410,8 @@ namespace spot
 
 		      transition t(i, one, j);
 		      d.transid[t] = ++d.nvars;
-		  d.revtransid.insert(dict::rev_map::value_type(d.nvars, t));
+		      d.revtransid.insert(dict::rev_map::
+					  value_type(d.nvars, t));
 
 		      // Create the variable for the accepting transition
 		      // immediately afterwards.  It helps parsing the
@@ -421,10 +426,49 @@ namespace spot
 		    }
 		}
 	  }
+	else // state based
+	  {
+	    for (int i = 1; i <= d.cand_size; ++i)
+	      for (unsigned n = 0; n < d.cand_nacc; ++n)
+		{
+		  ++d.nvars;
+		  for (int j = 1; j <= d.cand_size; ++j)
+		    {
+		      bdd all = bddtrue;
+		      while (all != bddfalse)
+			{
+			  bdd one = bdd_satoneset(all, ap_, bddfalse);
+			  all -= one;
+
+			  transition_acc ta(i, one, d.cand_acc[n], j);
+			  d.transaccid[ta] = d.nvars;
+			  d.revtransaccid.insert(dict::rev_acc_map::
+						 value_type(d.nvars, ta));
+			}
+		    }
+		}
+	    for (int i = 1; i <= d.cand_size; ++i)
+	      for (int j = 1; j <= d.cand_size; ++j)
+		{
+		  bdd all = bddtrue;
+		  while (all != bddfalse)
+		    {
+		      bdd one = bdd_satoneset(all, ap_, bddfalse);
+		      all -= one;
+
+		      transition t(i, one, j);
+		      d.transid[t] = ++d.nvars;
+		      d.revtransid.insert(dict::rev_map::
+					  value_type(d.nvars, t));
+		    }
+		}
+	  }
+      }
     };
 
     static
-    void dtgba_to_sat(std::ostream& out, const tgba* ref, dict& d)
+    void dtgba_to_sat(std::ostream& out, const tgba* ref, dict& d,
+		      bool state_based)
     {
       int nclauses = 0;
       int ref_size = 0;
@@ -439,7 +483,7 @@ namespace spot
 
       // Number all the SAT variable we may need.
       {
-	filler_dfs f(ref, d, ap);
+	filler_dfs f(ref, d, ap, state_based);
 	f.run();
 	ref_size = f.size();
       }
@@ -528,6 +572,9 @@ namespace spot
 		      state_pair p2(q2, dp);
 		      int succ = d.prodid[p2];
 
+		      if (pit->second == succ)
+			continue;
+
 		      dout << pit->first << " ∧ " << t << "δ → " << p2 << "\n";
 		      out << -pit->second << " " << -ti << " "
 			  << succ << " 0\n";
@@ -617,7 +664,8 @@ namespace spot
 					      bdd one = bdd_satone(all_f);
 					      all_f -= one;
 
-					      transition_acc ta(q2, l, one, q1);
+					      transition_acc ta(q2, l,
+								one, q1);
 					      int tai = d.transaccid[ta];
 					      assert(tai != 0);
 					      out << " " << -tai;
@@ -639,7 +687,8 @@ namespace spot
 					      bdd one = bdd_satone(all_);
 					      all_ -= one;
 
-					      transition_acc ta(q2, l, one, q1);
+					      transition_acc ta(q2, l,
+								one, q1);
 					      if (notfirst)
 						out << " ∧ ";
 					      else
@@ -656,7 +705,8 @@ namespace spot
 					      bdd one = bdd_satone(all_f);
 					      all_f -= one;
 
-					      transition_acc ta(q2, l, one, q1);
+					      transition_acc ta(q2, l,
+								one, q1);
 					      int tai = d.transaccid[ta];
 					      assert(tai != 0);
 
@@ -681,6 +731,9 @@ namespace spot
 
 					path p2(p.src_cand, p.src_ref,
 						q3, dp, f2, f2p);
+					int p2id = d.pathid[p2];
+					if (pid == p2id)
+					  continue;
 #if DEBUG
 					dout << "(13) " << p << " ∧ "
 					     << t << "δ ";
@@ -729,7 +782,6 @@ namespace spot
 					    out << tai << " ";
 					  }
 
-					int p2id = d.pathid[p2];
 					out << p2id << " 0\n";
 					++nclauses;
 				      }
@@ -766,7 +818,8 @@ namespace spot
 
 
     static tgba_explicit_number*
-    sat_build(const std::string& solution, dict& satdict, const tgba* aut)
+    sat_build(const std::string& solution, dict& satdict, const tgba* aut,
+	      bool state_based)
     {
       bdd_dict* autdict = aut->get_dict();
       tgba_explicit_number* a = new tgba_explicit_number(autdict);
@@ -792,6 +845,7 @@ namespace spot
 #endif
 
       dout << "--- transition variables ---\n";
+      std::map<int, bdd> state_acc;
       for (;;)
 	{
 	  int v;
@@ -816,6 +870,14 @@ namespace spot
 	      last_sat_trans = &t->second;
 
 	      dout << v << "\t" << t->second << "δ\n";
+
+	      if (state_based)
+		{
+		  std::map<int, bdd>::const_iterator i =
+		    state_acc.find(t->second.src);
+		  if (i != state_acc.end())
+		    last_aut_trans->acceptance_conditions = i->second;
+		}
 	    }
 	  else
 	    {
@@ -831,8 +893,15 @@ namespace spot
 		      ta->second.src == last_sat_trans->src &&
 		      ta->second.cond == last_sat_trans->cond &&
 		      ta->second.dst == last_sat_trans->dst)
+		    {
+		      assert(!state_based);
 		      last_aut_trans->acceptance_conditions |= ta->second.acc;
 		    }
+		  else if (state_based)
+		    {
+		      state_acc[ta->second.src] |= ta->second.acc;
+		    }
+		}
 	    }
 	}
 #if DEBUG
@@ -868,9 +937,13 @@ namespace spot
   }
 
   tgba_explicit_number*
-  dtgba_sat_minimize(const tgba* a, unsigned cand_nacc)
+  dtgba_sat_minimize(const tgba* a, unsigned cand_nacc,
+		     int target_state_number, bool state_based)
   {
-    int ref_states = stats_reachable(a).states;
+    int ref_states =
+      target_state_number == -1
+      ? stats_reachable(a).states - 1
+      : target_state_number;
 
     std::string current_solution;
     std::string last_solution;
@@ -892,23 +965,39 @@ namespace spot
 	delete last;
 	last = current;
 	current = new dict(a);
-	current->cand_size = --ref_states;
+	current->cand_size = ref_states--;
 	current->cand_nacc = cand_nacc;
 
 	cnf = create_tmpfile("dtgba-sat-", ".cnf");
 
 	std::fstream cnfs(cnf->name(),
 			  std::ios_base::trunc | std::ios_base::out);
-	dtgba_to_sat(cnfs, a, *current);
+	dtgba_to_sat(cnfs, a, *current, state_based);
 	cnfs.close();
 
-	out = create_tmpfile("dtba-sat-", ".out");
+	out = create_tmpfile("dtgba-sat-", ".out");
 	satsolver(cnf, out);
 	current_solution = get_solution(out->name());
       }
-    while (!current_solution.empty());
+    while (target_state_number == -1 && !current_solution.empty());
 
+    if (target_state_number != -1)
+      {
+	std::swap(current_solution, last_solution);
+	if (last_solution.empty())
+	  {
+	    last = 0;
 	    delete current;
+	  }
+	else
+	  {
+	    last = current;
+	  }
+      }
+    else
+      {
+	delete current;
+      }
 
     tgba_explicit_number* res;
     if (last == 0)
@@ -922,7 +1011,7 @@ namespace spot
       }
     else
       {
-	res = sat_build(last_solution, *last, a);
+	res = sat_build(last_solution, *last, a, state_based);
 	delete last;
       }
 

src/tgbaalgos/dtgbasat.hh

@@ -33,11 +33,23 @@ namespace spot
   ///
   /// \param cand_nacc is the number of acceptance sets in the result.
   ///
-  /// This functions attempts to find the smallest TGBA with \a
+  /// \param state_based set to true to force all outgoing transitions
-  /// cand_nacc acceptance sets that is equivalent to \a a.  If no
+  /// of a state to share the same acceptance conditions, effectively
-  /// smaller TGBA is found, a null pointer is returned.
+  /// turning the TGBA into a TBA.
+  ///
+  /// \param target_state_number the expected number of states wanted
+  /// in the resulting automaton.  If \a target_state_number is left
+  /// to its default value of -1, this function will attempt to build
+  /// the smallest possible deterministic TGBA is can produce.
+  ///
+  /// This functions attempts to find a TGBA with \a cand_nacc
+  /// acceptance sets and target_state_number states that is
+  /// equivalent to \a a.  If no such TGBA is found, a null pointer is
+  /// returned.
   SPOT_API tgba_explicit_number*
-  dtgba_sat_minimize(const tgba* a, unsigned cand_nacc);
+  dtgba_sat_minimize(const tgba* a, unsigned cand_nacc,
+		     int target_state_number = -1,
+		     bool state_based = false);
 }
 
 #endif // SPOT_TGBAALGOS_DTGBASAT_HH

src/tgbaalgos/postproc.cc

@@ -51,8 +51,14 @@ namespace spot
 	scc_filter_ = opt->get("scc-filter", -1);
 	ba_simul_ = opt->get("ba-simul", -1);
 	tba_determinisation_ = opt->get("tba-det", 0);
-	sat_minimize_ = opt->get("sat-minimize", 0);
+	dtba_sat_minimize_ = opt->get("dtba-sat-minimize", -1);
 	dtgba_sat_minimize_ = opt->get("dtgba-sat-minimize", -1);
+	dtgba_sat_minimize_acc_ = opt->get("dtgba-sat-minimize-acc", -1);
+	if (dtgba_sat_minimize_ >= 0 && dtgba_sat_minimize_acc_ == -1)
+	  dtgba_sat_minimize_acc_ = 0;
+	if (dtgba_sat_minimize_ == -1 && dtgba_sat_minimize_acc_ >= 0)
+	  dtgba_sat_minimize_ = 0;
+	state_based_ = opt->get("state-based", 0);
       }
   }
 
@@ -188,6 +194,7 @@ namespace spot
       }
 
     bool dba_is_wdba = false;
+    bool dba_is_minimal = false;
     const tgba* dba = 0;
     const tgba* sim = 0;
 
@@ -200,7 +207,7 @@ namespace spot
 	if (dba == a)	// Minimization failed.
 	  dba = 0;
 	else
-	  dba_is_wdba = true;
+	  dba_is_minimal = dba_is_wdba = true;
 	// The WDBA is a BA, so no degeneralization is required.
       }
 
@@ -242,7 +249,7 @@ namespace spot
 
 	const tgba* in = tmpd ? tmpd : sim;
 
-	// These thresholds is arbitrary.
+	// These thresholds are arbitrary.
 	//
 	// For producing Small automata, we assume that a
 	// deterministic automaton that is twice the size of the
@@ -281,25 +288,40 @@ namespace spot
     // TBA-determinization (dba_is_wdba=false in both cases).
 
     // Attempt SAT-minimization if requested.
-    if (sat_minimize_ && dba && !dba_is_wdba)
+    if (dtba_sat_minimize_ >= 0 && dba && !dba_is_wdba)
       {
 	// This only work on deterministic TBA, so degeneralize
 	// if needed.
 	const tgba* tmpd = 0;
 	if (dba->number_of_acceptance_conditions() != 1)
+	  {
+	    // If we are seeking a minimal DBA with unknown number of
+	    // states, then we should start from the degeneralized,
+	    // because the input TBA might be smaller.
+	    if (state_based_ && dtba_sat_minimize_ == 0)
+	      tmpd = degeneralize(dba);
+	    else
 	      tmpd = new tgba_tba_proxy(dba);
+	  }
 
 	const tgba* in = tmpd ? tmpd : dba;
 
 	const tgba* cmp = tgba_complete(in);
-	const tgba* res = dba_sat_minimize(cmp);
+	const tgba* res = dtba_sat_minimize(cmp,
+					    dtba_sat_minimize_ == 0
+					    ? -1 : dtba_sat_minimize_,
+					    state_based_);
 	delete cmp;
 	delete tmpd;
 	if (res != 0)
 	  {
 	    delete dba;
+	    if (state_based_)
+	      dba = scc_filter_states(res);
+	    else
 	      dba = scc_filter(res, true);
 	    delete res;
+	    dba_is_minimal = true;
 	  }
       }
     else if (dtgba_sat_minimize_ >= 0 && dba && !dba_is_wdba)
@@ -307,15 +329,26 @@ namespace spot
 	const tgba* cmp = tgba_complete(dba);
 	const tgba* res =
 	  dtgba_sat_minimize(cmp,
-			     dtgba_sat_minimize_
+			     dtgba_sat_minimize_acc_
-			     ? dtgba_sat_minimize_
+			     ? dtgba_sat_minimize_acc_
-			     : dba->number_of_acceptance_conditions());
+			     : dba->number_of_acceptance_conditions(),
+			     dtgba_sat_minimize_ == 0
+			     ? -1 : dtgba_sat_minimize_,
+			     state_based_);
 	delete cmp;
 	if (res != 0)
 	  {
 	    delete dba;
+	    if (state_based_)
+	      // FIXME: This does not simplify generalized acceptance
+	      // conditions, but calling scc_filter() would break the
+	      // BA-typeness of res by removing acceptance marks from
+	      // out-of-SCC transitions.
+	      dba = scc_filter_states(res);
+	    else
 	      dba = scc_filter(res, true);
 	    delete res;
+	    dba_is_minimal = true;
 	  }
       }
 
@@ -346,10 +379,8 @@ namespace spot
 
     if (type_ == TGBA && level_ == High && scc_filter_ != 0)
       {
-	if (dba && !dba_is_wdba) // WDBA is already clean.
+	if (dba && !dba_is_minimal) // WDBA is already clean.
 	  {
-	    // FIXME: if dba_sat_minimize has been run, scc_filter has
-	    // also been run.
 	    const tgba* s = scc_filter(dba, true);
 	    delete dba;
 	    return s;

src/tgbaalgos/postproc.hh

@@ -106,8 +106,10 @@ namespace spot
     int scc_filter_;
     int ba_simul_;
     bool tba_determinisation_;
-    bool sat_minimize_;
+    int dtba_sat_minimize_;
     int dtgba_sat_minimize_;
+    int dtgba_sat_minimize_acc_;
+    bool state_based_;
   };
   /// @}
 }

src/tgbatest/ltl2tgba.cc

@@ -1528,7 +1528,7 @@ main(int argc, char** argv)
       if (opt_dtbasat >= 0)
 	{
 	  tm.start("dtbasat");
-	  satminimized = dba_sat_minimize(a, opt_dtbasat);
+	  satminimized = dtba_sat_minimize(a, opt_dtbasat);
 	  tm.stop("dtbasat");
 	  if (satminimized)
 	    a = satminimized;

src/tgbatest/satmin.test

@@ -89,8 +89,8 @@ $ltlcross -F formulas \
   --timeout=60 \
   "$ltl2tgba --det --lbtt %f >%T" \
   "$ltl2tgba --det --lbtt -x tba-det %f >%T" \
-  "$ltl2tgba --det --lbtt -x tba-det,sat-minimize %f >%T" \
+  "$ltl2tgba --det --lbtt -x tba-det,dtba-sat-minimize=0 %f >%T" \
-  "$ltl2tgba --det --lbtt -x tba-det,dtgba-sat-minimize=0 %f >%T" \
+  "$ltl2tgba --det --lbtt -x tba-det,dtgba-sat-minimize-acc=0 %f >%T" \
-  "$ltl2tgba --det --lbtt -x dtgba-sat-minimize=0 %f >%T" \
+  "$ltl2tgba --det --lbtt -x dtgba-sat-minimize-acc=0 %f >%T" \
-  "$ltl2tgba --det --lbtt -x tba-det,dtgba-sat-minimize=3 %f >%T" \
+  "$ltl2tgba --det --lbtt -x tba-det,dtgba-sat-minimize-acc=3 %f >%T" \
   --json=det.json