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

hoaparse: detect duplicate atomic propositions

Browse source 
Reported by Joachim Klein.

* src/hoaparse/hoaparse.yy: Add a std::set to keep track of duplicate
propositions.
* src/tgbatest/hoaparse.test: Test it.
This commit is contained in:
Alexandre Duret-Lutz 2015-02-03 09:21:13 +01:00
parent d7dc584992
commit cbee5c1a3f
2 changed files with 16 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

17
src/hoaparse/hoaparse.yy
View file

@ -83,6 +83,7 @@
spot::acc_cond::mark_t pos_acc_sets = 0U;
std::vector<std::string>* state_names = nullptr;
std::map<unsigned, unsigned> states_map;
std::set<int> ap_set;
unsigned cur_state;
int states = -1;
int ap_count = -1;
@ -523,17 +524,27 @@ ap-name: STRING
if (!res.ignore_more_ap)
{
auto f = res.env->require(*$1);
auto d = res.h->aut->get_dict();
int b = 0;
if (f == nullptr)
{
std::ostringstream out;
out << "unknown atomic proposition \"" << *$1 << "\"";
delete $1;
error(@1, out.str());
f = spot::ltl::default_environment::instance()
.require("$unknown$");
b = d->register_proposition(f, res.h->aut);
}
else
{
b = d->register_proposition(f, res.h->aut);
if (!res.ap_set.emplace(b).second)
{
std::ostringstream out;
out << "duplicate atomic proposition \"" << *$1 << "\"";
error(@1, out.str());
}
}
auto b =
res.h->aut->get_dict()->register_proposition(f, res.h->aut);
f->destroy();
res.ap.push_back(b);
}

3
src/tgbatest/hoaparse.test
View file

@ -145,7 +145,7 @@ EOF
cat >input <<EOF
HOA: v1
AP: 1 "a"
AP: 2 "a" "a"
States: 0
Start: 1
--BODY--
@ -155,6 +155,7 @@ State: 0 {0 1}
EOF
expecterr input <<EOF
input:2.11-13: duplicate atomic proposition "a"
input:4.1-8: initial state number is larger than state count...
input:3.1-9: ... declared here.
input:1.1-4.8: missing 'Acceptance:' header