Running ltl2tgba -R1q -R1t -N would degeneralize before and

after the simulation-reduction.

Report from Tomáš Babiak <xbabiak@fi.muni.cz>.

* src/tgbaalgos/neverclaim.hh (never_claim_reachable): Take
a tgba as input.
* src/tgbaalgos/neverclaim.cc (never_claim_bfs): Call
state_is_accepting() only if this tgba turns out to be
a tgba_sba_proxy.  Otherwise check the acceptance of one
outgoing transition as we do in dotty_bfs since 2011-03-05.
* src/tgbatest/ltl2tgba.cc: Do not redegeneralize before
calling never_claim_reachable() if we know the automaton is
degeneralized already.
* src/tgbatest/ltl2tgba.test: Add a test case.

ChangeLog

@@ -1,3 +1,21 @@
+2011-08-25  Alexandre Duret-Lutz  <adl@lrde.epita.fr>
+
+	Running `ltl2tgba -R1q -R1t -N` would degeneralize before and
+	after the simulation-reduction.
+
+	Report from Tomáš Babiak <xbabiak@fi.muni.cz>.
+
+	* src/tgbaalgos/neverclaim.hh (never_claim_reachable): Take
+	a tgba as input.
+	* src/tgbaalgos/neverclaim.cc (never_claim_bfs): Call
+	state_is_accepting() only if this tgba turns out to be
+	a tgba_sba_proxy.  Otherwise check the acceptance of one
+	outgoing transition as we do in dotty_bfs since 2011-03-05.
+	* src/tgbatest/ltl2tgba.cc: Do not redegeneralize before
+	calling never_claim_reachable() if we know the automaton is
+	degeneralized already.
+	* src/tgbatest/ltl2tgba.test: Add a test case.
+
 2011-08-17  Alexandre Duret-Lutz  <adl@lrde.epita.fr>
 
 	Please GCC 4.6.

src/tgbaalgos/neverclaim.cc

@@ -38,11 +38,12 @@ namespace spot
     class never_claim_bfs : public tgba_reachable_iterator_breadth_first
     {
     public:
-      never_claim_bfs(const tgba_sba_proxy* a, std::ostream& os,
+      never_claim_bfs(const tgba* a, std::ostream& os,
 		      const ltl::formula* f, bool comments)
 	: tgba_reachable_iterator_breadth_first(a),
 	  os_(os), f_(f), accept_all_(-1), fi_needed_(false),
-	  comments_(comments)
+	  comments_(comments), all_acc_conds_(a->all_acceptance_conditions()),
+	  degen_(dynamic_cast<const tgba_sba_proxy*>(a))
       {
       }
 
@@ -77,8 +78,23 @@ namespace spot
       bool
       state_is_accepting(const state *s)
       {
-	return
-	  dynamic_cast<const tgba_sba_proxy*>(automata_)->state_is_accepting(s);
+	// If the automaton is degeneralized on-the-fly,
+	// it's easier to just query the state_is_accepting() method.
+	if (degen_)
+	  return degen_->state_is_accepting(s);
+
+	// Otherwise, since we are dealing with a degeneralized
+	// automaton nonetheless, the transitions leaving an accepting
+	// state are either all accepting, or all non-accepting.  So
+	// we just check the acceptance of the first transition.  This
+	// is not terribly efficient since we have to create the
+	// iterator.
+	tgba_succ_iterator* it = automata_->succ_iter(s);
+	it->first();
+	bool accepting =
+	  !it->done() && it->current_acceptance_conditions() == all_acc_conds_;
+	delete it;
+	return accepting;
       }
 
       std::string
@@ -185,13 +201,16 @@ namespace spot
       bool fi_needed_;
       state* init_;
       bool comments_;
+      bdd all_acc_conds_;
+      const tgba_sba_proxy* degen_;
     };
   } // anonymous
 
   std::ostream&
-  never_claim_reachable(std::ostream& os, const tgba_sba_proxy* g,
+  never_claim_reachable(std::ostream& os, const tgba* g,
 			const ltl::formula* f, bool comments)
   {
+    assert(g->number_of_acceptance_conditions() <= 1);
     never_claim_bfs n(g, os, f, comments);
     n.run();
     return os;

src/tgbaalgos/neverclaim.hh

@@ -1,4 +1,4 @@
-// Copyright (C) 2009 Laboratoire de Recherche et Développement
+// Copyright (C) 2009, 2011 Laboratoire de Recherche et Développement
 // de l'Epita (LRDE).
 // Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
 // département Systèmes Répartis Coopératifs (SRC), Université Pierre
@@ -34,13 +34,16 @@ namespace spot
   /// \ingroup tgba_io
   ///
   /// \param os The output stream to print on.
-  /// \param g The degeneralized automaton to output.
+  /// \param g The (state-based degeneralized) automaton to output.
+  ///          There should be only one acceptance condition, and
+  ///          all the transitions of a state should be either all accepting
+  ///          or all unaccepting.
   /// \param f The (optional) formula associated to the automaton.  If given
   ///          it will be output as a comment.
   /// \param comments Whether to comment each state of the never clause
   ///          with the label of the \a g automaton.
   std::ostream& never_claim_reachable(std::ostream& os,
-				      const tgba_sba_proxy* g,
+				      const tgba* g,
 				      const ltl::formula* f = 0,
 				      bool comments = false);
 }

src/tgbatest/ltl2tgba.cc

@@ -1142,16 +1142,14 @@ main(int argc, char** argv)
 	    case 8:
 	      {
 		assert(degeneralize_opt == DegenSBA);
-		const spot::tgba_sba_proxy* s =
-		  dynamic_cast<const spot::tgba_sba_proxy*>(a);
-		if (s)
-		  spot::never_claim_reachable(std::cout, s, f, spin_comments);
+		if (assume_sba || dynamic_cast<const spot::tgba_sba_proxy*>(a))
+		  spot::never_claim_reachable(std::cout, a, f, spin_comments);
 		else
 		  {
 		    // It is possible that we have applied other
 		    // operations to the automaton since its initial
 		    // degeneralization.  Let's degeneralize again!
-		    s = new spot::tgba_sba_proxy(a);
+		    spot::tgba_sba_proxy* s = new spot::tgba_sba_proxy(a);
 		    spot::never_claim_reachable(std::cout, s, f, spin_comments);
 		    delete s;
 		  }

src/tgbatest/ltl2tgba.test

@@ -124,3 +124,13 @@ grep 'states: 3$' stdout
 run 0 ../ltl2tgba -R3 -Rm -ks -f "Gq|Gr|(G(q|FGp)&G(r|FG!p))" >stdout
 grep 'transitions: 5$' stdout
 grep 'states: 3$' stdout
+
+# Make sure FGa|GFb has the same number of states/transitions when
+# output as a never claim or are a degeneralized BA in Spot's textual
+# format.  The option -R1q -R1t used to cause two degeneralizations to
+# occur.
+run 0 ../ltl2tgba -R1q -R1t -N 'FGa|FGb' > out.never
+run 0 ../ltl2tgba -XN -kt out.never > count.never
+run 0 ../ltl2tgba -R1q -R1t -DS -b 'FGa|FGb' > out.spot
+run 0 ../ltl2tgba -X -kt out.spot > count.spot
+cmp count.never count.spot