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

Fix rewriting of Negated constants and atomic propositions

Browse source 
* src/tgbaalgos/ltl2tgba_fm.cc (ratexp_trad_visitor): Take a
"negated" parameter and use it.
This commit is contained in:
Alexandre Duret-Lutz 2010-10-15 12:32:51 +02:00
parent c6a751b9d4
commit 4fd4f83ed6
1 changed files with 34 additions and 10 deletions
Download patch file Download diff file Expand all files Collapse all files

44
src/tgbaalgos/ltl2tgba_fm.cc
View file

@ -300,8 +300,11 @@ namespace spot
class ratexp_trad_visitor: public const_visitor class ratexp_trad_visitor: public const_visitor
{ {
public: public:
ratexp_trad_visitor(translate_dict& dict, formula* to_concat = 0) // negated should only be set for constants or atomic properties
: dict_(dict), to_concat_(to_concat) ratexp_trad_visitor(translate_dict& dict,
formula* to_concat = 0,
bool negated = false)
: dict_(dict), to_concat_(to_concat), negated_(negated)
{ {
} }
@ -321,7 +324,7 @@ namespace spot
bdd next_to_concat() bdd next_to_concat()
{ {
if (!to_concat_) if (!to_concat_)
return bddtrue; to_concat_ = constant::empty_word_instance();
int x = dict_.register_next_variable(to_concat_); int x = dict_.register_next_variable(to_concat_);
return bdd_ithvar(x); return bdd_ithvar(x);
} }
@ -337,13 +340,33 @@ namespace spot
void void
visit(const atomic_prop* node) visit(const atomic_prop* node)
{ {
res_ = (bdd_ithvar(dict_.register_proposition(node)) if (negated_)
& next_to_concat()); res_ = bdd_nithvar(dict_.register_proposition(node));
else
res_ = bdd_ithvar(dict_.register_proposition(node));
res_ &= next_to_concat();
} }
void void
visit(const constant* node) visit(const constant* node)
{ {
if (negated_)
{
switch (node->val())
{
case constant::True:
res_ = bddfalse;
return;
case constant::False:
res_ = next_to_concat();
return;
case constant::EmptyWord:
assert(!"EmptyWord should not be negated");
return;
}
}
switch (node->val()) switch (node->val())
{ {
case constant::True: case constant::True:
@ -380,7 +403,7 @@ namespace spot
const formula* f = node->child(); const formula* f = node->child();
assert(dynamic_cast<const atomic_prop*>(f) assert(dynamic_cast<const atomic_prop*>(f)
|| dynamic_cast<const constant*>(f)); || dynamic_cast<const constant*>(f));
res_ = !recurse(f) & next_to_concat(); res_ = recurse_and_concat(f, true);
return; return;
} }
} }
@ -667,23 +690,24 @@ namespace spot
} }
bdd bdd
recurse(const formula* f, formula* to_concat = 0) recurse(const formula* f, formula* to_concat = 0, bool negated = false)
{ {
ratexp_trad_visitor v(dict_, to_concat); ratexp_trad_visitor v(dict_, to_concat, negated);
f->accept(v); f->accept(v);
return v.result(); return v.result();
} }
bdd bdd
recurse_and_concat(const formula* f) recurse_and_concat(const formula* f, bool negated = false)
{ {
return recurse(f, to_concat_ ? to_concat_->clone() : 0); return recurse(f, to_concat_ ? to_concat_->clone() : 0, negated);
} }
private: private:
translate_dict& dict_; translate_dict& dict_;
bdd res_; bdd res_;
formula* to_concat_; formula* to_concat_;
bool negated_;
}; };