Commit ad37cacb authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

twa: fix duplicate propositions in ap()

Calling register_ap() with same atomic proposition several time, for
instance via copy_ap() in a product, would create duplicate atomic
propositions.  This fix will be exercised by the next patch.

* spot/twa/twa.hh: Here.
* spot/twaalgos/compsusp.cc, spot/twaalgos/ltl2taa.cc: Fix
to correctly register atomic propositions.
* NEWS: Mention it.
parent fbf5ac0e
...@@ -71,6 +71,9 @@ New in spot 1.99.6a (not yet released) ...@@ -71,6 +71,9 @@ New in spot 1.99.6a (not yet released)
Bug fixes: Bug fixes:
* twa::ap() would contain duplicates when an atomic proposition
was registered several times.
New in spot 1.99.6 (2015-12-04) New in spot 1.99.6 (2015-12-04)
Command-line tools: Command-line tools:
......
...@@ -597,9 +597,13 @@ namespace spot ...@@ -597,9 +597,13 @@ namespace spot
/// \return The BDD variable number. /// \return The BDD variable number.
int register_ap(formula ap) int register_ap(formula ap)
{ {
aps_.push_back(ap); int res = dict_->has_registered_proposition(ap, this);
int res = dict_->register_proposition(ap, this); if (res < 0)
bddaps_ &= bdd_ithvar(res); {
aps_.push_back(ap);
res = dict_->register_proposition(ap, this);
bddaps_ &= bdd_ithvar(res);
}
return res; return res;
} }
...@@ -720,7 +724,6 @@ namespace spot ...@@ -720,7 +724,6 @@ namespace spot
void copy_ap_of(const const_twa_ptr& a) void copy_ap_of(const const_twa_ptr& a)
{ {
get_dict()->register_all_propositions_of(a, this);
for (auto f: a->ap()) for (auto f: a->ap())
this->register_ap(f); this->register_ap(f);
} }
......
...@@ -164,9 +164,19 @@ namespace spot ...@@ -164,9 +164,19 @@ namespace spot
false)); false));
twa_graph_ptr res = make_twa_graph(dict); twa_graph_ptr res = make_twa_graph(dict);
dict->register_all_variables_of(left, res); {
dict->register_all_variables_of(right, res); // Copy all atomic propositions, except the one corresponding
dict->unregister_variable(bdd_var(v), res); // to the variable v used for synchronization.
int vn = bdd_var(v);
assert(dict->bdd_map[vn].type = bdd_dict::var);
formula vf = dict->bdd_map[vn].f;
for (auto a: left->ap())
if (a != vf)
res->register_ap(a);
for (auto a: right->ap())
if (a != vf)
res->register_ap(a);
}
unsigned lsets = left->num_sets(); unsigned lsets = left->num_sets();
res->set_generalized_buchi(lsets + right->num_sets()); res->set_generalized_buchi(lsets + right->num_sets());
......
...@@ -72,6 +72,7 @@ namespace spot ...@@ -72,6 +72,7 @@ namespace spot
SPOT_UNIMPLEMENTED(); SPOT_UNIMPLEMENTED();
case op::ap: case op::ap:
{ {
res_->register_ap(f);
if (negated_) if (negated_)
f = formula::Not(f); f = formula::Not(f);
init_ = f; init_ = f;
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment