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

word: store the bdd dict for easier printing

Browse source 
* src/twaalgos/word.hh, src/twaalgos/word.cc: Store the
bdd_dict, and replace the print() method by a << overload.
* NEWS: Mention it.
* src/bin/ltlcross.cc, src/bin/common_aoutput.hh: Adjust.
This commit is contained in:
Alexandre Duret-Lutz 2015-12-01 00:12:45 +01:00
parent cff79b063b
commit 2052e73af8
5 changed files with 27 additions and 9 deletions
Download patch file Download diff file Expand all files Collapse all files

1
NEWS
View file

@ -81,6 +81,7 @@ New in spot 1.99.5a (not yet released)
* Renamings:
is_guarantee_automaton() -> is_terminal_automaton()
tgba_run -> twa_run
twa_word::print -> operator<<
dtgba_sat_synthetize() -> dtwa_sat_synthetize()
dtgba_sat_synthetize_dichotomy() -> dtwa_sat_synthetize_dichotomy()

2
src/bin/common_aoutput.hh
View file

@ -181,7 +181,7 @@ public:
spot::twa_word w(run->reduce());
w.simplify();
std::ostringstream out;
w.print(out, aut->get_dict());
out << w;
aut_word_ = out.str();
}
else

2
src/bin/ltlcross.cc
View file

@ -695,7 +695,7 @@ namespace
<< " ";
spot::twa_word w(run->reduce());
w.simplify();
w.print(example(), prod->get_dict()) << '\n';
example() << w << '\n';
}
else
{

13
src/twaalgos/word.cc
View file

@ -24,11 +24,13 @@
namespace spot
{
twa_word::twa_word(const twa_run_ptr run)
: dict_(run->aut->get_dict())
{
for (auto& i: run->prefix)
prefix.push_back(i.label);
for (auto& i: run->cycle)
cycle.push_back(i.label);
dict_->register_all_variables_of(run->aut, this);
}
void
@ -81,18 +83,19 @@ namespace spot
}
std::ostream&
twa_word::print(std::ostream& os, const bdd_dict_ptr& d) const
operator<<(std::ostream& os, const twa_word& w)
{
if (!prefix.empty())
for (auto& i: prefix)
auto d = w.get_dict();
if (!w.prefix.empty())
for (auto& i: w.prefix)
{
bdd_print_formula(os, d, i);
os << "; ";
}
assert(!cycle.empty());
assert(!w.cycle.empty());
bool notfirst = false;
os << "cycle{";
for (auto& i: cycle)
for (auto& i: w.cycle)
{
if (notfirst)
os << "; ";

18
src/twaalgos/word.hh
View file

@ -26,15 +26,29 @@ namespace spot
class bdd_dict;
/// \brief An infinite word stored as a lasso.
struct SPOT_API twa_word
struct SPOT_API twa_word final
{
twa_word(const twa_run_ptr run);
~twa_word()
{
dict_->unregister_all_my_variables(this);
}
void simplify();
std::ostream& print(std::ostream& os, const bdd_dict_ptr& d) const;
typedef std::list<bdd> seq_t;
seq_t prefix;
seq_t cycle;
bdd_dict_ptr get_dict() const
{
return dict_;
}
SPOT_API
friend std::ostream& operator<<(std::ostream& os, const twa_word& w);
private:
bdd_dict_ptr dict_;
};
}