Do not comment states in the never claim by default. It takes too

much time when the formula is large, and it is useless when the
purpose is model-checking with Spin.

* src/tgbaalgos/neverclaim.hh (never_claim_reachable): Add the
comments option.
* src/tgbaalgos/neverclaim.cc (never_claim_bfs,
never_claim_reachable): Honor the comment option.
* src/tgba/tests/ltl2tgba.cc (-N): Do not comment states.
(-NN) New option to output a commented never claim.

ChangeLog

@@ -1,3 +1,16 @@
+2009-11-10  Alexandre Duret-Lutz  <adl@lrde.epita.fr>
+
+	Do not comment states in the never claim by default.  It takes too
+	much time when the formula is large, and it is useless when the
+	purpose is model-checking with Spin.
+
+	* src/tgbaalgos/neverclaim.hh (never_claim_reachable): Add the
+	comments option.
+	* src/tgbaalgos/neverclaim.cc (never_claim_bfs,
+	never_claim_reachable): Honor the comment option.
+	* src/tgba/tests/ltl2tgba.cc (-N): Do not comment states.
+	(-NN) New option to output a commented never claim.
+
 2009-11-10  Damien Lefortier <dam@lrde.epita.fr>
 
 	* src/tgba/taa.cc, src/tgba/taa.hh: Fix it.

src/tgbaalgos/neverclaim.cc

@@ -37,9 +37,10 @@ namespace spot
     {
     public:
       never_claim_bfs(const tgba_sba_proxy* a, std::ostream& os,
-		      const ltl::formula* f)
+		      const ltl::formula* f, bool comments)
 	: tgba_reachable_iterator_breadth_first(a),
-	  os_(os), f_(f), accept_all_(-1), fi_needed_(false)
+	  os_(os), f_(f), accept_all_(-1), fi_needed_(false),
+	  comments_(comments)
       {
       }
 
@@ -126,8 +127,9 @@ namespace spot
 	  {
 	    if (fi_needed_ != 0)
 	      os_ << "  fi;" << std::endl;
-	    os_ << get_state_label(s, n) << ": ";
+	    os_ << get_state_label(s, n) << ":";
-	    os_ << "/* " << automata_->format_state(s) << " */";
+	    if (comments_)
+	      os_ << " /* " << automata_->format_state(s) << " */";
 	    os_ << std::endl;
 	    os_ << "  if" << std::endl;
 	    os_ << "  :: (0) -> goto " << get_state_label(s, n) << std::endl;
@@ -145,8 +147,9 @@ namespace spot
 	      {
 		if (fi_needed_)
 		  os_ << "  fi;" << std::endl;
-		os_ << get_state_label(s, n) << ": ";
+		os_ << get_state_label(s, n) << ":";
-		os_ << "/* " << automata_->format_state(s) << " */";
+		if (comments_)
+		  os_ << " /* " << automata_->format_state(s) << " */";
 		os_ << std::endl;
 		os_ << "  if" << std::endl;
 		fi_needed_ = true;
@@ -179,14 +182,15 @@ namespace spot
       int accept_all_;
       bool fi_needed_;
       state* init_;
+      bool comments_;
     };
   } // anonymous
 
   std::ostream&
   never_claim_reachable(std::ostream& os, const tgba_sba_proxy* g,
-			const ltl::formula* f)
+			const ltl::formula* f, bool comments)
   {
-    never_claim_bfs n(g, os, f);
+    never_claim_bfs n(g, os, f, comments);
     n.run();
     return os;
   }

src/tgbaalgos/neverclaim.hh

@@ -1,4 +1,4 @@
-// Copyright (C) 2004  Laboratoire d'Informatique de Paris 6 (LIP6),
+// Copyright (C) 2004, 2009  Laboratoire d'Informatique de Paris 6 (LIP6),
 // département Systèmes Répartis Coopératifs (SRC), Université Pierre
 // et Marie Curie.
 //
@@ -35,9 +35,12 @@ namespace spot
   /// \param g The degeneralized automaton to output.
   /// \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 ltl::formula* f = 0);
+				      const ltl::formula* f = 0,
+				      bool comments = false);
 }
 
 #endif // SPOT_TGBAALGOS_NEVERCLAIM_HH

src/tgbatest/ltl2tgba.cc

@@ -106,8 +106,10 @@ syntax(char* prog)
             << "  -lS   label acceptance conditions on states" << std::endl
 	    << "  -m    try to reduce accepting runs, in a second pass"
 	    << std::endl
-	    << "  -N    display the never clain for Spin "
+	    << "  -N    display the never clain for Spin (implies -D)"
-	    << "(implies -D)" << std::endl
+	    << std::endl
+	    << "  -NN   display the never clain for Spin, with commented states"
+	    << " (implies -D)" << std::endl
             << "  -p    branching postponement (implies -f)" << std::endl
 	    << "  -Pfile  multiply the formula with the automaton from `file'."
 	    << std::endl
@@ -200,6 +202,7 @@ main(int argc, char** argv)
   bool opt_reduce = false;
   bool containment = false;
   bool show_fc = false;
+  bool spin_comments = false;
   spot::ltl::environment& env(spot::ltl::default_environment::instance());
   spot::ltl::atomic_prop_set* unobservables = 0;
   spot::tgba_explicit_string* system = 0;
@@ -377,6 +380,12 @@ main(int argc, char** argv)
 	  degeneralize_opt = DegenSBA;
 	  output = 8;
 	}
+      else if (!strcmp(argv[formula_index], "-NN"))
+	{
+	  degeneralize_opt = DegenSBA;
+	  output = 8;
+	  spin_comments = true;
+	}
       else if (!strcmp(argv[formula_index], "-p"))
 	{
 	  post_branching = true;
@@ -794,7 +803,7 @@ main(int argc, char** argv)
 		assert(degeneralize_opt == DegenSBA);
 		const spot::tgba_sba_proxy* s =
 		  static_cast<const spot::tgba_sba_proxy*>(degeneralized);
-		spot::never_claim_reachable(std::cout, s, f);
+		spot::never_claim_reachable(std::cout, s, f, spin_comments);
 		break;
 	      }
 	    case 9: