From ef5b0417e791296042ae6b525fc20785080c5fa8 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 25 Nov 2014 11:37:29 +0100 Subject: [PATCH] hoa: fix handling of escaped characters in atomic propositions (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. --- NEWS | 1 + src/tgbaalgos/hoaf.cc | 7 ++++++- 2 files changed, 7 insertions(+), 1 deletion(-) diff --git a/NEWS b/NEWS index 8b469d5fd..c1c464f92 100644 --- a/NEWS +++ b/NEWS @@ -16,6 +16,7 @@ New in spot 1.2.5a (not yet released) state labels. - the acceptance specification in the HOA format output have been 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 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 diff --git a/src/tgbaalgos/hoaf.cc b/src/tgbaalgos/hoaf.cc index 152d5e506..afbe546be 100644 --- a/src/tgbaalgos/hoaf.cc +++ b/src/tgbaalgos/hoaf.cc @@ -32,6 +32,7 @@ #include "misc/minato.hh" #include "tgba/formula2bdd.hh" #include "ltlvisit/tostring.hh" +#include "ltlast/atomic_prop.hh" namespace spot { @@ -265,7 +266,11 @@ namespace spot bdd_dict* d = aut->get_dict(); for (metadata::vap_t::const_iterator i = md.vap.begin(); 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; unsigned num_acc = md.acc.size(); if (num_acc == 0)