* src/tgbaparse/tgbaparse.yy (acc_list): Do not explicitly delete

an undeclared acceptance condition.
* src/tgbaalgos/save.cc (print_acc): Unquote atomic propositions.

ChangeLog

 2005-04-06  Alexandre Duret-Lutz  <adl@src.lip6.fr>
 
+	* src/tgbaparse/tgbaparse.yy (acc_list): Do not explicitly delete
+	an undeclared acceptance condition.
+	* src/tgbaalgos/save.cc (print_acc): Unquote atomic propositions.
+
 	* bench/emptchk/Makefile.am: Create reduced versions of the graphs.
 	* bench/emptchk/pml2tgba.pl: Add option -r.
 	* bench/emptchk/pml-clserv.sh, bench/emptchk/pml-eeaean.sh:

src/tgbaalgos/save.cc

-// Copyright (C) 2003, 2004  Laboratoire d'Informatique de Paris 6 (LIP6),
+// Copyright (C) 2003, 2004, 2005  Laboratoire d'Informatique de Paris 6 (LIP6),
 // dpartement Systmes Rpartis Coopratifs (SRC), Universit Pierre
 // et Marie Curie.
 //
@@ -23,6 +23,7 @@
 #include "save.hh"
 #include "tgba/bddprint.hh"
 #include "ltlvisit/tostring.hh"
+#include "ltlast/atomic_prop.hh"
 #include "reachiter.hh"
 #include "misc/escape.hh"
 
@@ -84,8 +85,16 @@ namespace spot
 		    bdd_dict::vf_map::const_iterator vi =
 		      d->acc_formula_map.find(v);
 		    assert(vi != d->acc_formula_map.end());
+		    std::string s = ltl::to_string(vi->second);
+		    if (dynamic_cast<const ltl::atomic_prop*>(vi->second)
+			&& s[0] == '"')
+		      {
+			// Unquote atomic propositions.
+			s.erase(s.begin());
+			s.resize(s.size() - 1);
+		      }
 		    os_ << " \"";
-		    escape_str(os_, ltl::to_string(vi->second)) << "\"";
+		    escape_str(os_, s) << "\"";
 		    break;
 		  }
 		cube = bdd_low(cube);

src/tgbaparse/tgbaparse.yy

@@ -179,9 +179,9 @@ acc_list:
 	     if (! result->has_acceptance_condition(f))
 	       {
 		 error_list.push_back(spot::tgba_parse_error(@2,
-			 "undeclared acceptance condition"));
+			 "undeclared acceptance condition `" + *$2 + "'"));
 		 destroy(f);
-		 delete $2;
+		 // $2 will be destroyed on error recovery.
 		 YYERROR;
 	       }
 	     $1->push_back(f);