typo
This commit is contained in:
Alexandre Duret-Lutz
parent
2f19a35e97
commit
c4c90de3f6
8 changed files with 64 additions and 50 deletions
|
|
@ -1,3 +1,10 @@
|
|||
2003-06-03 Alexandre Duret-Lutz <adl@gnu.org>
|
||||
|
||||
* src/tgba/dictunion.cc, src/tgba/ltl2tgba.cc,
|
||||
src/tgba/succiterconcrete.cc, src/tgba/tgbabddconcrete.cc,
|
||||
src/tgba/tgbabddprod.cc, src/tgba/tgbabddtranslatefactory.cc,
|
||||
src/tgba/tgbabddtranslateproxy.cc: Include <cassert>.
|
||||
|
||||
2003-06-02 Alexandre Duret-Lutz <aduret@src.lip6.fr>
|
||||
|
||||
* src/tgba/tgbabdddict.cc, src/tgba/tgbabdddict.hh: New files.
|
||||
|
|
@ -92,7 +99,7 @@
|
|||
not a bdd.
|
||||
* src/tgba/tgbabddconcrete.cc: Likewise.
|
||||
|
||||
Initial code for TGBA (Transition Generalized BŽüchi Automata).
|
||||
Initial code for TGBA (Transition Generalized Büchi Automata).
|
||||
Contains tgba_bdd, a BDD-encoded TGBA, and ltl_to_tgba,
|
||||
a LTL-to-TGBA translator using Couvreur's algorithm.
|
||||
|
||||
|
|
|
|||
|
|
@ -1,6 +1,7 @@
|
|||
#include <set>
|
||||
#include "dictunion.hh"
|
||||
#include <bdd.h>
|
||||
#include <cassert>
|
||||
|
||||
namespace spot
|
||||
{
|
||||
|
|
@ -9,45 +10,45 @@ namespace spot
|
|||
tgba_bdd_dict_union(const tgba_bdd_dict& l, const tgba_bdd_dict& r)
|
||||
{
|
||||
tgba_bdd_dict res;
|
||||
|
||||
|
||||
std::set<const ltl::formula*> now;
|
||||
std::set<const ltl::formula*> var;
|
||||
std::set<const ltl::formula*> prom;
|
||||
|
||||
|
||||
tgba_bdd_dict::fv_map::const_iterator i;
|
||||
|
||||
|
||||
// Merge Now variables.
|
||||
for (i = l.now_map.begin(); i != l.now_map.end(); ++i)
|
||||
now.insert(i->first);
|
||||
for (i = r.now_map.begin(); i != r.now_map.end(); ++i)
|
||||
now.insert(i->first);
|
||||
|
||||
|
||||
// Merge atomic propositions.
|
||||
for (i = l.var_map.begin(); i != l.var_map.end(); ++i)
|
||||
var.insert(i->first);
|
||||
for (i = r.var_map.begin(); i != r.var_map.end(); ++i)
|
||||
var.insert(i->first);
|
||||
|
||||
|
||||
// Merge promises.
|
||||
for (i = l.prom_map.begin(); i != l.prom_map.end(); ++i)
|
||||
prom.insert(i->first);
|
||||
for (i = r.prom_map.begin(); i != r.prom_map.end(); ++i)
|
||||
prom.insert(i->first);
|
||||
|
||||
|
||||
// Ensure we have enough BDD variables.
|
||||
int have = bdd_extvarnum(0);
|
||||
int want = now.size() * 2 + var.size() + prom.size();
|
||||
if (have < want)
|
||||
bdd_setvarnum(want);
|
||||
|
||||
|
||||
// Fill in the "defragmented" union dictionary.
|
||||
|
||||
|
||||
// FIXME: Make some experiments with ordering of prom/var/now variables.
|
||||
// Maybe there is one order that usually produces smaller BDDs?
|
||||
|
||||
|
||||
// Next BDD variable to use.
|
||||
int v = 0;
|
||||
|
||||
|
||||
std::set<const ltl::formula*>::const_iterator f;
|
||||
for (f = prom.begin(); f != prom.end(); ++f)
|
||||
{
|
||||
|
|
@ -67,7 +68,7 @@ namespace spot
|
|||
res.now_formula_map[v] = *f;
|
||||
v += 2;
|
||||
}
|
||||
|
||||
|
||||
assert (v == want);
|
||||
return res;
|
||||
}
|
||||
|
|
|
|||
|
|
@ -1,6 +1,7 @@
|
|||
#include "ltlast/visitor.hh"
|
||||
#include "ltlast/allnodes.hh"
|
||||
#include "tgbabddconcretefactory.hh"
|
||||
#include <cassert>
|
||||
|
||||
#include "ltl2tgba.hh"
|
||||
|
||||
|
|
|
|||
|
|
@ -1,4 +1,5 @@
|
|||
#include "succiterconcrete.hh"
|
||||
#include <cassert>
|
||||
|
||||
namespace spot
|
||||
{
|
||||
|
|
|
|||
|
|
@ -1,5 +1,6 @@
|
|||
#include "tgbabddconcrete.hh"
|
||||
#include "bddprint.hh"
|
||||
#include <cassert>
|
||||
|
||||
namespace spot
|
||||
{
|
||||
|
|
|
|||
|
|
@ -1,6 +1,7 @@
|
|||
#include "tgbabddprod.hh"
|
||||
#include "tgbabddtranslateproxy.hh"
|
||||
#include "dictunion.hh"
|
||||
#include <cassert>
|
||||
|
||||
namespace spot
|
||||
{
|
||||
|
|
@ -14,7 +15,7 @@ namespace spot
|
|||
delete right_;
|
||||
}
|
||||
|
||||
int
|
||||
int
|
||||
state_bdd_product::compare(const state* other) const
|
||||
{
|
||||
const state_bdd_product* o = dynamic_cast<const state_bdd_product*>(other);
|
||||
|
|
@ -33,7 +34,7 @@ namespace spot
|
|||
: left_(left), right_(right)
|
||||
{
|
||||
}
|
||||
|
||||
|
||||
void
|
||||
tgba_bdd_product_succ_iterator::step_()
|
||||
{
|
||||
|
|
@ -63,7 +64,7 @@ namespace spot
|
|||
}
|
||||
}
|
||||
|
||||
void
|
||||
void
|
||||
tgba_bdd_product_succ_iterator::first()
|
||||
{
|
||||
left_->first();
|
||||
|
|
@ -71,21 +72,21 @@ namespace spot
|
|||
next_non_false_();
|
||||
}
|
||||
|
||||
void
|
||||
void
|
||||
tgba_bdd_product_succ_iterator::next()
|
||||
{
|
||||
step_();
|
||||
next_non_false_();
|
||||
}
|
||||
|
||||
bool
|
||||
bool
|
||||
tgba_bdd_product_succ_iterator::done()
|
||||
{
|
||||
return right_->done();
|
||||
}
|
||||
|
||||
|
||||
state_bdd*
|
||||
|
||||
|
||||
state_bdd*
|
||||
tgba_bdd_product_succ_iterator::current_state()
|
||||
{
|
||||
state_bdd* ls = dynamic_cast<state_bdd*>(left_->current_state());
|
||||
|
|
@ -94,13 +95,13 @@ namespace spot
|
|||
assert(rs);
|
||||
return new state_bdd_product(ls, rs);
|
||||
}
|
||||
|
||||
bdd
|
||||
|
||||
bdd
|
||||
tgba_bdd_product_succ_iterator::current_condition()
|
||||
{
|
||||
return current_cond_;
|
||||
}
|
||||
|
||||
|
||||
bdd tgba_bdd_product_succ_iterator::current_promise()
|
||||
{
|
||||
return left_->current_promise() & right_->current_promise();
|
||||
|
|
@ -145,17 +146,17 @@ namespace spot
|
|||
delete right_;
|
||||
}
|
||||
|
||||
state*
|
||||
state*
|
||||
tgba_bdd_product::get_init_state() const
|
||||
{
|
||||
state_bdd* ls = dynamic_cast<state_bdd*>(left_->get_init_state());
|
||||
state_bdd* rs = dynamic_cast<state_bdd*>(right_->get_init_state());
|
||||
assert(ls);
|
||||
assert(rs);
|
||||
return new state_bdd_product(ls, rs);
|
||||
return new state_bdd_product(ls, rs);
|
||||
}
|
||||
|
||||
tgba_bdd_product_succ_iterator*
|
||||
tgba_bdd_product_succ_iterator*
|
||||
tgba_bdd_product::succ_iter(const state* state) const
|
||||
{
|
||||
const state_bdd_product* s = dynamic_cast<const state_bdd_product*>(state);
|
||||
|
|
@ -166,21 +167,21 @@ namespace spot
|
|||
return new tgba_bdd_product_succ_iterator(li, ri);
|
||||
}
|
||||
|
||||
const tgba_bdd_dict&
|
||||
const tgba_bdd_dict&
|
||||
tgba_bdd_product::get_dict() const
|
||||
{
|
||||
return dict_;
|
||||
}
|
||||
|
||||
std::string
|
||||
std::string
|
||||
tgba_bdd_product::format_state(const state* state) const
|
||||
{
|
||||
const state_bdd_product* s = dynamic_cast<const state_bdd_product*>(state);
|
||||
assert(s);
|
||||
return (left_->format_state(s->left())
|
||||
+ " * "
|
||||
return (left_->format_state(s->left())
|
||||
+ " * "
|
||||
+ right_->format_state(s->right()));
|
||||
}
|
||||
|
||||
|
||||
|
||||
|
||||
}
|
||||
|
|
|
|||
|
|
@ -1,5 +1,6 @@
|
|||
#include "tgbabddtranslatefactory.hh"
|
||||
#include "dictunion.hh"
|
||||
#include <cassert>
|
||||
|
||||
namespace spot
|
||||
{
|
||||
|
|
|
|||
|
|
@ -1,38 +1,39 @@
|
|||
#include "tgbabddtranslateproxy.hh"
|
||||
#include "bddprint.hh"
|
||||
#include <cassert>
|
||||
|
||||
namespace spot
|
||||
{
|
||||
|
||||
// tgba_bdd_translate_proxy_succ_iterator
|
||||
// --------------------------------------
|
||||
|
||||
|
||||
tgba_bdd_translate_proxy_succ_iterator::
|
||||
tgba_bdd_translate_proxy_succ_iterator(tgba_succ_iterator_concrete* it,
|
||||
bddPair* rewrite)
|
||||
: iter_(it), rewrite_(rewrite)
|
||||
{
|
||||
}
|
||||
|
||||
void
|
||||
|
||||
void
|
||||
tgba_bdd_translate_proxy_succ_iterator::first()
|
||||
{
|
||||
iter_->first();
|
||||
}
|
||||
|
||||
void
|
||||
|
||||
void
|
||||
tgba_bdd_translate_proxy_succ_iterator::next()
|
||||
{
|
||||
iter_->next();
|
||||
}
|
||||
|
||||
bool
|
||||
|
||||
bool
|
||||
tgba_bdd_translate_proxy_succ_iterator::done()
|
||||
{
|
||||
return iter_->done();
|
||||
}
|
||||
|
||||
state_bdd*
|
||||
state_bdd*
|
||||
tgba_bdd_translate_proxy_succ_iterator::current_state()
|
||||
{
|
||||
state_bdd* s = iter_->current_state();
|
||||
|
|
@ -40,13 +41,13 @@ namespace spot
|
|||
return s;
|
||||
}
|
||||
|
||||
bdd
|
||||
bdd
|
||||
tgba_bdd_translate_proxy_succ_iterator::current_condition()
|
||||
{
|
||||
return bdd_replace(iter_->current_condition(), rewrite_);
|
||||
}
|
||||
|
||||
bdd
|
||||
bdd
|
||||
tgba_bdd_translate_proxy_succ_iterator::current_promise()
|
||||
{
|
||||
return bdd_replace(iter_->current_promise(), rewrite_);
|
||||
|
|
@ -56,7 +57,7 @@ namespace spot
|
|||
// tgba_bdd_translate_proxy
|
||||
// ------------------------
|
||||
|
||||
tgba_bdd_translate_proxy::tgba_bdd_translate_proxy(const tgba& from,
|
||||
tgba_bdd_translate_proxy::tgba_bdd_translate_proxy(const tgba& from,
|
||||
const tgba_bdd_dict& to)
|
||||
: from_(from), to_(to)
|
||||
{
|
||||
|
|
@ -97,8 +98,8 @@ namespace spot
|
|||
bdd_freepair(rewrite_from_);
|
||||
bdd_freepair(rewrite_to_);
|
||||
}
|
||||
|
||||
state_bdd*
|
||||
|
||||
state_bdd*
|
||||
tgba_bdd_translate_proxy::get_init_state() const
|
||||
{
|
||||
state_bdd* s = dynamic_cast<state_bdd*>(from_.get_init_state());
|
||||
|
|
@ -107,24 +108,24 @@ namespace spot
|
|||
return s;
|
||||
}
|
||||
|
||||
tgba_bdd_translate_proxy_succ_iterator*
|
||||
tgba_bdd_translate_proxy_succ_iterator*
|
||||
tgba_bdd_translate_proxy::succ_iter(const state* state) const
|
||||
{
|
||||
const state_bdd* s = dynamic_cast<const state_bdd*>(state);
|
||||
assert(s);
|
||||
state_bdd s2(bdd_replace(s->as_bdd(), rewrite_from_));
|
||||
tgba_succ_iterator_concrete* it =
|
||||
state_bdd s2(bdd_replace(s->as_bdd(), rewrite_from_));
|
||||
tgba_succ_iterator_concrete* it =
|
||||
dynamic_cast<tgba_succ_iterator_concrete*>(from_.succ_iter(&s2));
|
||||
assert(it);
|
||||
return new tgba_bdd_translate_proxy_succ_iterator(it, rewrite_to_);
|
||||
}
|
||||
|
||||
const tgba_bdd_dict&
|
||||
const tgba_bdd_dict&
|
||||
tgba_bdd_translate_proxy::get_dict() const
|
||||
{
|
||||
return to_;
|
||||
}
|
||||
|
||||
|
||||
std::string
|
||||
tgba_bdd_translate_proxy::format_state(const state* state) const
|
||||
{
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue