Keep acceptance conditions on transitions going to accepting SCCs

by default in scc_filter().

Doing so helps the degeneralization algorithm, because it will
have more opportunity to be in an accepting level when it reaches
the accepting SCCs.

* src/tgbaalgos/sccfilter.cc (filter_iter::filter_iter): Take a
remove_all_useless argument.
(filter_iter::process_link): Use the flag to decide whether to
filter acceptance conditions going to accepting SCCs.
(scc_filter): Take a remove_all_useless argument and pass it to
filter_iter.
* src/tgbaalgos/sccfilter.hh (filter_iter): Add the new argument
and document the function.
* src/tgbatest/tgbatests/ltl2tgba.cc (main): Add option use -R3
for remove_all_useless=false and add -R3f for
remove_all_useless=true.
* src/tgbatest/ltl2tgba.test: Show one case where -R3f makes
the degeneralization worse than -R3.

ChangeLog

@@ -1,3 +1,26 @@
+2010-03-06  Alexandre Duret-Lutz  <adl@lrde.epita.fr>
+
+	Keep acceptance conditions on transitions going to accepting SCCs
+	by default in scc_filter().
+
+	Doing so helps the degeneralization algorithm, because it will
+	have more opportunity to be in an accepting level when it reaches
+	the accepting SCCs.
+
+	* src/tgbaalgos/sccfilter.cc (filter_iter::filter_iter): Take a
+	remove_all_useless argument.
+	(filter_iter::process_link): Use the flag to decide whether to
+	filter acceptance conditions going to accepting SCCs.
+	(scc_filter): Take a remove_all_useless argument and pass it to
+	filter_iter.
+	* src/tgbaalgos/sccfilter.hh (filter_iter): Add the new argument
+	and document the function.
+	* src/tgbatest/tgbatests/ltl2tgba.cc (main): Add option use -R3
+	for remove_all_useless=false and add -R3f for
+	remove_all_useless=true.
+	* src/tgbatest/ltl2tgba.test: Show one case where -R3f makes
+	the degeneralization worse than -R3.
+
 2010-03-05  Alexandre Duret-Lutz  <adl@lrde.epita.fr>
 
 	Simplify F(a)|F(b) as F(a|b).  Add similar rule for G(a)&G(b).

src/tgbaalgos/sccfilter.cc

@@ -1,5 +1,5 @@
-// Copyright (C) 2009 Laboratoire de Recherche et Developpement de
+// Copyright (C) 2009, 2010 Laboratoire de Recherche et Developpement
-// l'Epita (LRDE).
+// de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
 //
@@ -64,13 +64,14 @@ namespace spot
       filter_iter(const tgba* a,
 		  const scc_map& sm,
 		  const std::vector<bool>& useless,
-		  bdd useful, bdd strip)
+		  bdd useful, bdd strip, bool remove_all_useless)
 	: tgba_reachable_iterator_depth_first(a),
 	  out_(new T(a->get_dict())),
 	  sm_(sm),
 	  useless_(useless),
 	  useful_(useful),
-	  strip_(strip)
+	  strip_(strip),
+	  all_(remove_all_useless)
       {
 	out_->set_acceptance_conditions(useful);
       }
@@ -96,10 +97,16 @@ namespace spot
 	  create_transition(this->automata_, out_, in_s, in, out_s, out);
 	out_->add_conditions(t, si->current_condition());
 
-	// Do not output any acceptance condition if either the source or
+	// Regardless of all_, do not output any acceptance condition
-	// the destination state do not belong to an accepting state.
+	// if the destination is not in an accepting SCC.
-	if (sm_.accepting(sm_.scc_of_state(in_s))
+	//
-	    && sm_.accepting(sm_.scc_of_state(out_s)))
+	// If all_ is set, do not output any acceptance condition if the
+	// source is not in the same SCC as dest.
+	//
+	// (See the documentation of scc_filter() for a rational.)
+	unsigned u = sm_.scc_of_state(out_s);
+	if (sm_.accepting(u)
+	    && (!all_ || u == sm_.scc_of_state(in_s)))
 	  out_->add_acceptance_conditions
 	    (t, (bdd_exist(si->current_acceptance_conditions(), strip_)
 		 & useful_));
@@ -111,12 +118,13 @@ namespace spot
       const std::vector<bool>& useless_;
       bdd useful_;
       bdd strip_;
+      bool all_;
     };
 
   } // anonymous
 
 
-  tgba* scc_filter(const tgba* aut)
+  tgba* scc_filter(const tgba* aut, bool remove_all_useless)
   {
     scc_map sm(aut);
     sm.build_map();
@@ -160,7 +168,8 @@ namespace spot
     if (af)
       {
 	filter_iter<tgba_explicit_formula> fi(af, sm, ss.useless_scc_map,
-					     useful, strip);
+					      useful, strip,
+					      remove_all_useless);
 	fi.run();
 	tgba_explicit_formula* res = fi.result();
 	res->merge_transitions();
@@ -169,7 +178,8 @@ namespace spot
     else
       {
 	filter_iter<tgba_explicit_string> fi(aut, sm, ss.useless_scc_map,
-					      useful, strip);
+					     useful, strip,
+					     remove_all_useless);
 	fi.run();
 	tgba_explicit_string* res = fi.result();
 	res->merge_transitions();
@@ -177,6 +187,4 @@ namespace spot
       }
   }
 
-
-
 }

src/tgbaalgos/sccfilter.hh

@@ -1,5 +1,5 @@
-// Copyright (C) 2009 Laboratoire de Recherche et Developpement de
+// Copyright (C) 2009, 2010 Laboratoire de Recherche et Developpement
-// l'Epita (LRDE).
+// de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
 //
@@ -26,8 +26,28 @@
 namespace spot
 {
 
-  // Prune unaccepting SCCs and remove superfluous acceptance conditions.
+  /// \brief Prune unaccepting SCCs and remove superfluous acceptance
-  tgba* scc_filter(const tgba* aut);
+  /// conditions.
+  ///
+  /// This functions will explore the SCCs of the automaton and remove
+  /// dead SCCs (unaccepting, and with no exit path leading to an
+  /// accepting SCC).
+  ///
+  /// Additionally, this will try to remove useless acceptance
+  /// conditions.  This operation may diminish the number of
+  /// acceptance condition of the automaton, for instance when two
+  /// acceptance conditions are always used together we only keep one
+  /// (but it will never remove all acceptance conditions, even if it
+  /// would be OK to have zero).
+  ///
+  /// Acceptance conditions on transitions going to non-accepting SCC
+  /// are all removed.  Acceptance conditions going to an accepting
+  /// SCC and coming from another SCC are only removed if \a
+  /// remove_all_useless is set.  The default value of \a
+  /// remove_all_useless is \c false because some algorithms (like the
+  /// degeneralization) will work better if transition going to an
+  /// accepting SCC are accepting.
+  tgba* scc_filter(const tgba* aut, bool remove_all_useless = false);
 
 }
 

src/tgbatest/ltl2tgba.cc

@@ -195,6 +195,10 @@ syntax(char* prog)
 	    << "  -R2t  remove transitions using delayed simulation"
 	    << std::endl
 	    << "  -R3   use SCC to reduce the automata" << std::endl
+	    << "  -R3f  clean more acceptance conditions that -R3" << std::endl
+	    << "          "
+	    << "(prefer -R3 over -R3f if you degeneralize with -D, -DS, or -N)"
+	    << std::endl
 	    << "  -Rd   display the simulation relation" << std::endl
 	    << "  -RD   display the parity game (dot format)" << std::endl
 	    << std::endl
@@ -280,6 +284,7 @@ main(int argc, char** argv)
   bool from_file = false;
   int reduc_aut = spot::Reduce_None;
   int redopt = spot::ltl::Reduce_None;
+  bool scc_filter_all = false;
   bool symbolic_scc_pruning = false;
   bool display_reduce_form = false;
   bool display_rel_sim = false;
@@ -560,6 +565,11 @@ main(int argc, char** argv)
 	{
 	  reduc_aut |= spot::Reduce_Scc;
 	}
+      else if (!strcmp(argv[formula_index], "-R3f"))
+	{
+	  reduc_aut |= spot::Reduce_Scc;
+	  scc_filter_all = true;
+	}
       else if (!strcmp(argv[formula_index], "-R3b"))
 	{
 	  symbolic_scc_pruning = true;
@@ -806,7 +816,7 @@ main(int argc, char** argv)
       if (reduc_aut & spot::Reduce_Scc)
 	{
 	  tm.start("reducing A_f w/ SCC");
-	  a = aut_scc = spot::scc_filter(a);
+	  a = aut_scc = spot::scc_filter(a, scc_filter_all);
 	  tm.stop("reducing A_f w/ SCC");
 	}
 

src/tgbatest/ltl2tgba.test

@@ -75,3 +75,17 @@ for opt in '' -D -DS; do
   grep 'transitions: 6$' stdout
   grep 'states: 4$' stdout
 done
+
+# Make sure '(G (p -> F q)) && ((X (p) U q) || ! X (p U (p && q)))'
+# has 6 states and 15 transitions, before and after degeneralization.
+f='(G (p -> F q)) && ((X (p) U q) || ! X (p U (p && q)))'
+for opt in '' -D -DS; do
+  ../ltl2tgba -k -f -R3 $opt "$f" > stdout
+  grep 'transitions: 15$' stdout
+  grep 'states: 6$' stdout
+done
+
+# Note: this is worse with -R3f.
+../ltl2tgba -k -f -R3f -DS "$f" > stdout
+grep 'transitions: 17$' stdout
+grep 'states: 7$' stdout