diff --git a/ChangeLog b/ChangeLog index 9c44dbf4a..da83ff55f 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,5 +1,9 @@ 2005-04-06 Alexandre Duret-Lutz + * 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: diff --git a/src/tgbaalgos/save.cc b/src/tgbaalgos/save.cc index 4329c6eff..b87a36eff 100644 --- a/src/tgbaalgos/save.cc +++ b/src/tgbaalgos/save.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), +// Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (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(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); diff --git a/src/tgbaparse/tgbaparse.yy b/src/tgbaparse/tgbaparse.yy index e027e9144..af1702ed3 100644 --- a/src/tgbaparse/tgbaparse.yy +++ b/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);