alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

hoa: fix handling of escaped characters in atomic propositions

Browse source 
(No test, this is just a simple backport of a fix from the development
branch, where it is tested.)

* src/tgbaalgos/hoaf.cc: Do not call to_string() to display names, as
this would add another level of escaping.
* NEWS: Mention it.
This commit is contained in:
Alexandre Duret-Lutz 2014-11-25 11:37:29 +01:00
parent f8cf2aa9b3
commit ef5b0417e7
2 changed files with 7 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

1
NEWS
View file

@ -16,6 +16,7 @@ New in spot 1.2.5a (not yet released)
state labels. state labels.
- the acceptance specification in the HOA format output have been - the acceptance specification in the HOA format output have been
adjusted to match recent changes in the format specifications. adjusted to match recent changes in the format specifications.
- atomic propositions are correctly escaped in the HOA output.
- the build rules for documentation have been made compatible with - the build rules for documentation have been made compatible with
version 8.0 of Org-mode. (This was only a problem if you build version 8.0 of Org-mode. (This was only a problem if you build
from the git repository, or if you want to edit the from the git repository, or if you want to edit the

7
src/tgbaalgos/hoaf.cc
View file

@ -32,6 +32,7 @@
#include "misc/minato.hh" #include "misc/minato.hh"
#include "tgba/formula2bdd.hh" #include "tgba/formula2bdd.hh"
#include "ltlvisit/tostring.hh" #include "ltlvisit/tostring.hh"
#include "ltlast/atomic_prop.hh"
namespace spot namespace spot
{ {
@ -265,7 +266,11 @@ namespace spot
bdd_dict* d = aut->get_dict(); bdd_dict* d = aut->get_dict();
for (metadata::vap_t::const_iterator i = md.vap.begin(); for (metadata::vap_t::const_iterator i = md.vap.begin();
i != md.vap.end(); ++i) i != md.vap.end(); ++i)
escape_str(os << " \"", to_string(d->bdd_map[*i].f)) << '"'; {
const ltl::atomic_prop* f = ltl::is_atomic_prop(d->bdd_map[*i].f);
assert(f);
escape_str(os << " \"", f->name()) << '"';
}
os << nl; os << nl;
unsigned num_acc = md.acc.size(); unsigned num_acc = md.acc.size();
if (num_acc == 0) if (num_acc == 0)