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

* src/tgba/taa.cc, src/tgba/taa.hh: Fix it.

Browse source 
* src/tgbaalgos/ltl2taa.cc: Do NOT use the same bdd_dict for both
the translation and the language containment checker.
* src/tgbatest/spotlbtt.test: Update TAA related tests.
This commit is contained in:
Damien Lefortier 2009-11-10 16:45:29 +01:00
parent 007e2bd0b9
commit 1d8b115b83
5 changed files with 45 additions and 31 deletions
Download patch file Download diff file Expand all files Collapse all files

7
ChangeLog
View file

@ -1,3 +1,10 @@
2009-11-10 Damien Lefortier <dam@lrde.epita.fr>
* src/tgba/taa.cc, src/tgba/taa.hh: Fix it.
* src/tgbaalgos/ltl2taa.cc: Do NOT use the same bdd_dict for both
the translation and the language containment checker.
* src/tgbatest/spotlbtt.test: Update TAA related tests.
2009-11-10 Alexandre Duret-Lutz <adl@lrde.epita.fr>
Use tgba_explicit_formula instead of tgba_explicit_string in FM.

45
src/tgba/taa.cc
View file

@ -150,8 +150,7 @@ namespace spot
taa::get_init_state() const
{
assert(init_);
taa::state_set* ss = new taa::state_set(*init_);
return new spot::state_set(ss);
return new spot::state_set(init_);
}
tgba_succ_iterator*
@ -163,8 +162,7 @@ namespace spot
assert(s);
(void) global_state;
(void) global_automaton;
return new taa_succ_iterator(s->get_state(),
all_acceptance_conditions());
return new taa_succ_iterator(s->get_state(), all_acceptance_conditions());
}
bdd_dict*
@ -303,29 +301,29 @@ namespace spot
const taa::state_set* s1 = get_state();
const taa::state_set* s2 = o->get_state();
if (*s1 == *s2)
return 0;
if (s1->size() != s2->size())
return s1->size() - s2->size();
taa::state_set::const_iterator it1 = s1->begin();
taa::state_set::const_iterator it2 = s2->begin();
while (it2 != s2->end() && it1 != s1->end())
while (it2 != s2->end())
{
int i = *it1++ - *it2++;
if (i != 0)
return i;
}
return s1->size() - s2->size();
return 0;
}
size_t
state_set::hash() const
{
size_t res = wang32_hash(0);
size_t res = 0;
taa::state_set::const_iterator it = s_->begin();
while (it != s_->end())
{
res += reinterpret_cast<const char*>(*it++) - static_cast<char*>(0);
res ^= wang32_hash(res);
res ^= reinterpret_cast<const char*>(*it++) - static_cast<char*>(0);
res = wang32_hash(res);
}
return res;
}
@ -333,8 +331,10 @@ namespace spot
state_set*
state_set::clone() const
{
taa::state_set* s = new taa::state_set(*s_);
return new spot::state_set(s);
if (delete_me_ && s_)
return new spot::state_set(new taa::state_set(*s_), true);
else
return new spot::state_set(s_, false);
}
/*--------------.
@ -383,19 +383,20 @@ namespace spot
ss->insert(*j);
// Fill the new transition.
t->dst = ss;
t->condition &= (*pos[p])->condition;
t->acceptance_conditions |= (*pos[p])->acceptance_conditions;
}
// If p != pos.size() we have found a contradiction
} // If p != pos.size() we have found a contradiction
assert(p > 0);
t->dst = ss;
// Boxing to be able to insert ss in the map directly.
spot::state_set* b = new spot::state_set(ss);
// If no contradiction, then look for another transition to
// merge with the new one.
seen_map::iterator i;
if (t->condition != bddfalse)
{
for (i = seen_.find(ss); i != seen_.end(); ++i)
for (i = seen_.find(b); i != seen_.end(); ++i)
{
if (*i->second->dst == *t->dst
&& i->second->condition == t->condition)
@ -416,13 +417,14 @@ namespace spot
// or delete it otherwise.
if (t->condition != bddfalse && i == seen_.end())
{
seen_.insert(std::make_pair(ss, t));
seen_.insert(std::make_pair(b, t));
succ_.push_back(t);
}
else
{
delete t->dst;
delete t;
delete b;
}
for (int i = pos.size() - 1; i >= 0; --i)
@ -443,7 +445,12 @@ namespace spot
taa_succ_iterator::~taa_succ_iterator()
{
for (unsigned i = 0; i < succ_.size(); ++i)
{
delete succ_[i]->dst;
delete succ_[i];
}
for (seen_map::iterator i = seen_.begin(); i != seen_.end(); ++i)
delete i->first;
}
void
@ -468,7 +475,7 @@ namespace spot
taa_succ_iterator::current_state() const
{
assert(!done());
return new spot::state_set((*i_)->dst);
return new spot::state_set(new taa::state_set(*(*i_)->dst), true);
}
bdd

13
src/tgba/taa.hh
View file

@ -131,11 +131,8 @@ namespace spot
class state_set : public spot::state
{
public:
/// The taa::state_set has been allocated with \c new. It is the
/// responsability of the state_set to \c delete it when no longer
/// needed (cf. dtor).
state_set(const taa::state_set* s)
: s_(s)
state_set(const taa::state_set* s, bool delete_me = false)
: s_(s), delete_me_(delete_me)
{
}
@ -145,12 +142,14 @@ namespace spot
virtual ~state_set()
{
delete s_;
if (delete_me_)
delete s_;
}
const taa::state_set* get_state() const;
private:
const taa::state_set* s_;
bool delete_me_;
};
class taa_succ_iterator : public tgba_succ_iterator
@ -174,7 +173,7 @@ namespace spot
typedef std::pair<iterator, iterator> iterator_pair;
typedef std::vector<iterator_pair> bounds_t;
typedef Sgi::hash_multimap<
const taa::state_set*, taa::transition*, ptr_hash<taa::state_set>
const spot::state_set*, taa::transition*, state_ptr_hash, state_ptr_equal
> seen_map;
struct distance_sort :

3
src/tgbaalgos/ltl2taa.cc
View file

@ -382,8 +382,9 @@ namespace spot
f1->destroy();
spot::taa* res = new spot::taa(dict);
bdd_dict b;
language_containment_checker* lcc =
new language_containment_checker(dict, false, false, false, false);
new language_containment_checker(&b, false, false, false, false);
ltl2taa_visitor v(res, lcc, refined_rules);
f2->accept(v);
f2->destroy();

8
src/tgbatest/spotlbtt.test
View file

@ -270,17 +270,17 @@ Algorithm
Algorithm
{
Name = "Spot (Tauriainen -- TAA) pre reduction"
Name = "Spot (Tauriainen -- TAA) refined rules"
Path = "${LBTT_TRANSLATE}"
Parameters = "--spot '../ltl2tgba -F -taa -t -r7'"
Parameters = "--spot '../ltl2tgba -F -taa -t -c'"
Enabled = yes
}
Algorithm
{
Name = "Spot (Tauriainen -- TAA) pre reduction + refined rules"
Name = "Spot (Tauriainen -- TAA) refined rules + pre + post reduction"
Path = "${LBTT_TRANSLATE}"
Parameters = "--spot '../ltl2tgba -F -taa -t -r7 -c'"
Parameters = "--spot '../ltl2tgba -F -taa -t -c -r7 -R3'"
Enabled = yes
}