rename tgba_run as twa_run
Fixes #122. * src/twaalgos/word.cc, src/twaalgos/word.hh: Here. * src/bin/ltlcross.cc, src/bin/common_aoutput.hh: Adjust. * NEWS: Mention the renaming.
This commit is contained in:
parent
d14f0998e0
commit
5a7abe8582
5 changed files with 25 additions and 29 deletions
1
NEWS
1
NEWS
|
|
@ -50,6 +50,7 @@ New in spot 1.99.5a (not yet released)
|
||||||
|
|
||||||
* Renamings:
|
* Renamings:
|
||||||
is_guarantee_automaton() -> is_terminal_automaton()
|
is_guarantee_automaton() -> is_terminal_automaton()
|
||||||
|
tgba_run -> twa_run
|
||||||
|
|
||||||
Python:
|
Python:
|
||||||
* Add bindings for is_unambiguous().
|
* Add bindings for is_unambiguous().
|
||||||
|
|
|
||||||
|
|
@ -178,7 +178,7 @@ public:
|
||||||
{
|
{
|
||||||
auto run = res->accepting_run();
|
auto run = res->accepting_run();
|
||||||
assert(run);
|
assert(run);
|
||||||
spot::tgba_word w(run->reduce());
|
spot::twa_word w(run->reduce());
|
||||||
w.simplify();
|
w.simplify();
|
||||||
std::ostringstream out;
|
std::ostringstream out;
|
||||||
w.print(out, aut->get_dict());
|
w.print(out, aut->get_dict());
|
||||||
|
|
|
||||||
|
|
@ -693,7 +693,7 @@ namespace
|
||||||
{
|
{
|
||||||
std::cerr << "; both automata accept the infinite word\n"
|
std::cerr << "; both automata accept the infinite word\n"
|
||||||
<< " ";
|
<< " ";
|
||||||
spot::tgba_word w(run->reduce());
|
spot::twa_word w(run->reduce());
|
||||||
w.simplify();
|
w.simplify();
|
||||||
w.print(example(), prod->get_dict()) << '\n';
|
w.print(example(), prod->get_dict()) << '\n';
|
||||||
}
|
}
|
||||||
|
|
|
||||||
|
|
@ -1,5 +1,5 @@
|
||||||
// -*- coding: utf-8 -*-
|
// -*- coding: utf-8 -*-
|
||||||
// Copyright (C) 2013, 2014 Laboratoire de Recherche et Développement
|
// Copyright (C) 2013, 2014, 2015 Laboratoire de Recherche et Développement
|
||||||
// de l'Epita (LRDE).
|
// de l'Epita (LRDE).
|
||||||
//
|
//
|
||||||
// This file is part of Spot, a model checking library.
|
// This file is part of Spot, a model checking library.
|
||||||
|
|
@ -23,18 +23,16 @@
|
||||||
|
|
||||||
namespace spot
|
namespace spot
|
||||||
{
|
{
|
||||||
tgba_word::tgba_word(const twa_run_ptr run)
|
twa_word::twa_word(const twa_run_ptr run)
|
||||||
{
|
{
|
||||||
for (twa_run::steps::const_iterator i = run->prefix.begin();
|
for (auto& i: run->prefix)
|
||||||
i != run->prefix.end(); ++i)
|
prefix.push_back(i.label);
|
||||||
prefix.push_back(i->label);
|
for (auto& i: run->cycle)
|
||||||
for (twa_run::steps::const_iterator i = run->cycle.begin();
|
cycle.push_back(i.label);
|
||||||
i != run->cycle.end(); ++i)
|
|
||||||
cycle.push_back(i->label);
|
|
||||||
}
|
}
|
||||||
|
|
||||||
void
|
void
|
||||||
tgba_word::simplify()
|
twa_word::simplify()
|
||||||
{
|
{
|
||||||
// If all the formulas on the cycle are compatible, reduce the
|
// If all the formulas on the cycle are compatible, reduce the
|
||||||
// cycle to a simple conjunction.
|
// cycle to a simple conjunction.
|
||||||
|
|
@ -45,8 +43,8 @@ namespace spot
|
||||||
// !a|!b; b; a&b; cycle{a&b}
|
// !a|!b; b; a&b; cycle{a&b}
|
||||||
{
|
{
|
||||||
bdd all = bddtrue;
|
bdd all = bddtrue;
|
||||||
for (seq_t::const_iterator i = cycle.begin(); i != cycle.end(); ++i)
|
for (auto& i: cycle)
|
||||||
all &= *i;
|
all &= i;
|
||||||
if (all != bddfalse)
|
if (all != bddfalse)
|
||||||
{
|
{
|
||||||
cycle.clear();
|
cycle.clear();
|
||||||
|
|
@ -76,35 +74,32 @@ namespace spot
|
||||||
// !a|!b; cycle{a&b}
|
// !a|!b; cycle{a&b}
|
||||||
// can be reduced to
|
// can be reduced to
|
||||||
// !a&!b; cycle{a&b}
|
// !a&!b; cycle{a&b}
|
||||||
for (seq_t::iterator i = prefix.begin(); i != prefix.end(); ++i)
|
for (auto& i: prefix)
|
||||||
*i = bdd_satone(*i);
|
i = bdd_satone(i);
|
||||||
for (seq_t::iterator i = cycle.begin(); i != cycle.end(); ++i)
|
for (auto& i: cycle)
|
||||||
*i = bdd_satone(*i);
|
i = bdd_satone(i);
|
||||||
|
|
||||||
}
|
}
|
||||||
|
|
||||||
std::ostream&
|
std::ostream&
|
||||||
tgba_word::print(std::ostream& os, const bdd_dict_ptr& d) const
|
twa_word::print(std::ostream& os, const bdd_dict_ptr& d) const
|
||||||
{
|
{
|
||||||
if (!prefix.empty())
|
if (!prefix.empty())
|
||||||
for (seq_t::const_iterator i = prefix.begin(); i != prefix.end(); ++i)
|
for (auto& i: prefix)
|
||||||
{
|
{
|
||||||
bdd_print_formula(os, d, *i);
|
bdd_print_formula(os, d, i);
|
||||||
os << "; ";
|
os << "; ";
|
||||||
}
|
}
|
||||||
assert(!cycle.empty());
|
assert(!cycle.empty());
|
||||||
bool notfirst = false;
|
bool notfirst = false;
|
||||||
os << "cycle{";
|
os << "cycle{";
|
||||||
for (seq_t::const_iterator i = cycle.begin(); i != cycle.end(); ++i)
|
for (auto& i: cycle)
|
||||||
{
|
{
|
||||||
if (notfirst)
|
if (notfirst)
|
||||||
os << "; ";
|
os << "; ";
|
||||||
notfirst = true;
|
notfirst = true;
|
||||||
bdd_print_formula(os, d, *i);
|
bdd_print_formula(os, d, i);
|
||||||
}
|
}
|
||||||
os << '}';
|
os << '}';
|
||||||
return os;
|
return os;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
||||||
}
|
}
|
||||||
|
|
|
||||||
|
|
@ -1,6 +1,6 @@
|
||||||
// -*- coding: utf-8 -*-
|
// -*- coding: utf-8 -*-
|
||||||
// Copyright (C) 2013, 2014 Laboratoire de Recherche et Développement de
|
// Copyright (C) 2013, 2014, 2015 Laboratoire de Recherche et
|
||||||
// l'Epita (LRDE).
|
// Développement de l'Epita (LRDE).
|
||||||
//
|
//
|
||||||
// This file is part of Spot, a model checking library.
|
// This file is part of Spot, a model checking library.
|
||||||
//
|
//
|
||||||
|
|
@ -26,9 +26,9 @@ namespace spot
|
||||||
class bdd_dict;
|
class bdd_dict;
|
||||||
|
|
||||||
/// \brief An infinite word stored as a lasso.
|
/// \brief An infinite word stored as a lasso.
|
||||||
struct SPOT_API tgba_word
|
struct SPOT_API twa_word
|
||||||
{
|
{
|
||||||
tgba_word(const twa_run_ptr run);
|
twa_word(const twa_run_ptr run);
|
||||||
void simplify();
|
void simplify();
|
||||||
std::ostream& print(std::ostream& os, const bdd_dict_ptr& d) const;
|
std::ostream& print(std::ostream& os, const bdd_dict_ptr& d) const;
|
||||||
|
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue