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 
* src/hoaparse/hoascan.ll: Remove superfluous line.
* src/tgbaalgos/hoaf.cc: Do not call to_string() to display names, as
this would add another level of escaping.
* src/tgbatest/hoaparse.test: Test it.
This commit is contained in:
Alexandre Duret-Lutz 2014-11-25 11:37:29 +01:00
parent a9fa7d33c5
commit 0d59e55f4d
3 changed files with 8 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/hoaparse/hoascan.ll
View file

@ -118,7 +118,6 @@ identifier [[:alpha:]_][[:alnum:]_-]*
yylval->str = new std::string(s); yylval->str = new std::string(s);
return token::STRING; return token::STRING;
} }
\\\" s += '"';
\\. s += yytext[1]; \\. s += yytext[1];
[^\\\"]+ s.append(yytext, yyleng); [^\\\"]+ s.append(yytext, yyleng);
<<EOF>> { <<EOF>> {

7
src/tgbaalgos/hoaf.cc
View file

@ -31,6 +31,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
{ {
@ -252,7 +253,11 @@ namespace spot
auto d = aut->get_dict(); auto 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)) << '"'; {
auto f = ltl::is_atomic_prop(d->bdd_map[*i].f);
assert(f);
escape_str(os << " \"", f->name()) << '"';
}
os << nl; os << nl;
unsigned num_acc = aut->acc().num_sets(); unsigned num_acc = aut->acc().num_sets();
if (num_acc == 0) if (num_acc == 0)

4
src/tgbatest/hoaparse.test
View file

@ -456,7 +456,7 @@ States: 2
Start: 0 Start: 0
Start: 1 Start: 1
Start: 0 /* duplicate */ Start: 0 /* duplicate */
AP: 2 "a" "b" AP: 2 "a" "\"b\""
Acceptance: 1 Inf(0) Acceptance: 1 Inf(0)
--BODY-- --BODY--
State: 0 {0} State: 0 {0}
@ -472,7 +472,7 @@ expectok input <<EOF
HOA: v1 HOA: v1
States: 3 States: 3
Start: 0 Start: 0
AP: 2 "a" "b" AP: 2 "a" "\"b\""
acc-name: Buchi acc-name: Buchi
Acceptance: 1 Inf(0) Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels state-acc complete properties: trans-labels explicit-labels state-acc complete