Commit 55715dfb authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

* src/tgbaalgos/ltl2tgba_fm.cc: Get rid of tgba_explicit_formula.

parent 6dc29547
...@@ -33,9 +33,10 @@ ...@@ -33,9 +33,10 @@
#include "ltlvisit/tostring.hh" #include "ltlvisit/tostring.hh"
#include <cassert> #include <cassert>
#include <memory> #include <memory>
#include <utility>
#include "ltl2tgba_fm.hh" #include "ltl2tgba_fm.hh"
#include "tgba/bddprint.hh" #include "tgba/bddprint.hh"
#include "tgbaalgos/scc.hh" #include "tgbaalgos/sccinfo.hh"
#include "tgba/tgbaexplicit.hh" #include "tgba/tgbaexplicit.hh"
//#include "tgbaalgos/dotty.hh" //#include "tgbaalgos/dotty.hh"
#include "priv/acccompl.hh" #include "priv/acccompl.hh"
...@@ -110,20 +111,23 @@ namespace spot ...@@ -110,20 +111,23 @@ namespace spot
class ratexp_to_dfa class ratexp_to_dfa
{ {
typedef typename tgba_digraph::namer<const formula*,
formula_ptr_hash>::type namer;
public: public:
ratexp_to_dfa(translate_dict& dict); ratexp_to_dfa(translate_dict& dict);
std::pair<tgba_explicit_formula*, const state*> succ(const formula* f); std::tuple<const tgba_digraph*, const namer*, const state*>
const formula* get_label(const formula* f, const state* s) const; succ(const formula* f);
~ratexp_to_dfa(); ~ratexp_to_dfa();
protected: protected:
tgba_explicit_formula* translate(const formula* f); typedef std::pair<tgba_digraph*, const namer*> labelled_aut;
labelled_aut translate(const formula* f);
private: private:
translate_dict& dict_; translate_dict& dict_;
std::vector<tgba_explicit_formula*> automata_; typedef std::unordered_map<const formula*, labelled_aut,
typedef std::unordered_map<const formula*, tgba_explicit_formula*,
formula_ptr_hash> f2a_t; formula_ptr_hash> f2a_t;
std::vector<labelled_aut> automata_;
f2a_t f2a_; f2a_t f2a_;
}; };
...@@ -972,23 +976,29 @@ namespace spot ...@@ -972,23 +976,29 @@ namespace spot
ratexp_to_dfa::~ratexp_to_dfa() ratexp_to_dfa::~ratexp_to_dfa()
{ {
for (auto i: automata_) for (auto i: automata_)
delete i; {
delete i.first;
for (auto n: i.second->names())
n->destroy();
delete i.second;
}
} }
tgba_explicit_formula* ratexp_to_dfa::labelled_aut
ratexp_to_dfa::translate(const formula* f) ratexp_to_dfa::translate(const formula* f)
{ {
assert(f->is_in_nenoform()); assert(f->is_in_nenoform());
tgba_explicit_formula* a = new tgba_explicit_formula(dict_.dict); auto a = new tgba_digraph(dict_.dict);
auto namer = a->create_namer<const formula*, formula_ptr_hash>();
typedef std::set<const formula*, formula_ptr_less_than> set_type; typedef std::set<const formula*, formula_ptr_less_than> set_type;
set_type formulae_to_translate; set_type formulae_to_translate;
f->clone(); f->clone();
formulae_to_translate.insert(f); formulae_to_translate.insert(f);
a->set_init_state(f); namer->new_state(f);
//a->set_init_state(f);
while (!formulae_to_translate.empty()) while (!formulae_to_translate.empty())
{ {
...@@ -1011,22 +1021,24 @@ namespace spot ...@@ -1011,22 +1021,24 @@ namespace spot
dict_.bdd_to_sere(bdd_exist(res & label, dict_.var_set)); dict_.bdd_to_sere(bdd_exist(res & label, dict_.var_set));
f2a_t::const_iterator i = f2a_.find(dest); f2a_t::const_iterator i = f2a_.find(dest);
if (i != f2a_.end() && i->second == 0) if (i != f2a_.end() && i->second.first == nullptr)
{ {
// This state is useless. Ignore it. // This state is useless. Ignore it.
dest->destroy(); dest->destroy();
continue; continue;
} }
bool seen = a->has_state(dest); if (!namer->has_state(dest))
state_explicit_formula::transition* t = {
a->create_transition(now, dest); formulae_to_translate.insert(dest);
t->condition = label; namer->new_state(dest);
}
if (!seen)
formulae_to_translate.insert(dest);
else else
dest->destroy(); {
dest->destroy();
}
namer->new_transition(now, dest, label);
} }
} }
...@@ -1042,10 +1054,9 @@ namespace spot ...@@ -1042,10 +1054,9 @@ namespace spot
// eliminating SCCs that are not coaccessible. It does not // eliminating SCCs that are not coaccessible. It does not
// actually remove the states, it simply marks the corresponding // actually remove the states, it simply marks the corresponding
// formulae as associated to the null pointer in the f2a_ map. // formulae as associated to the null pointer in the f2a_ map.
// The method succ() and get_label() interpret this as False. // The method succ() interprets this as False.
scc_map* sm = new scc_map(a); scc_info* sm = new scc_info(a);
sm->build_map();
unsigned scc_count = sm->scc_count(); unsigned scc_count = sm->scc_count();
// Remember whether each SCC is coaccessible. // Remember whether each SCC is coaccessible.
std::vector<bool> coaccessible(scc_count); std::vector<bool> coaccessible(scc_count);
...@@ -1055,9 +1066,9 @@ namespace spot ...@@ -1055,9 +1066,9 @@ namespace spot
// The SCC is coaccessible if any of its states // The SCC is coaccessible if any of its states
// is final (i.e., it accepts [*0])... // is final (i.e., it accepts [*0])...
bool coacc = false; bool coacc = false;
const std::list<const state*>& st = sm->states_of(n); auto& st = sm->states_of(n);
for (auto l: st) for (auto l: st)
if (a->get_label(l)->accepts_eword()) if (namer->get_name(l)->accepts_eword())
{ {
coacc = true; coacc = true;
break; break;
...@@ -1066,7 +1077,7 @@ namespace spot ...@@ -1066,7 +1077,7 @@ namespace spot
{ {
// ... or if any of its successors is coaccessible. // ... or if any of its successors is coaccessible.
for (auto& i: sm->succ(n)) for (auto& i: sm->succ(n))
if (coaccessible[i.first]) if (coaccessible[i.dst])
{ {
coacc = true; coacc = true;
break; break;
...@@ -1076,66 +1087,58 @@ namespace spot ...@@ -1076,66 +1087,58 @@ namespace spot
{ {
// Mark all formulas of this SCC as useless. // Mark all formulas of this SCC as useless.
for (auto f: st) for (auto f: st)
f2a_[a->get_label(f)] = nullptr; f2a_.emplace(std::piecewise_construct,
std::forward_as_tuple(namer->get_name(f)),
std::forward_as_tuple(nullptr, nullptr));
} }
else else
{ {
for (auto f: st) for (auto f: st)
f2a_[a->get_label(f)] = a; f2a_.emplace(std::piecewise_construct,
std::forward_as_tuple(namer->get_name(f)),
std::forward_as_tuple(a, namer));
} }
coaccessible[n] = coacc; coaccessible[n] = coacc;
} }
delete sm; delete sm;
if (coaccessible[scc_count - 1]) if (coaccessible[scc_count - 1])
{ {
automata_.push_back(a); automata_.emplace_back(a, namer);
return a; return labelled_aut(a, namer);
} }
else else
{ {
delete a; delete a;
return 0; for (auto n: namer->names())
n->destroy();
delete namer;
return labelled_aut(nullptr, nullptr);
} }
} }
// FIXME: use the new tgba::succ() interface // FIXME: use the new tgba::succ() interface
std::pair<tgba_explicit_formula*, const state*> std::tuple<const tgba_digraph*,
const ratexp_to_dfa::namer*,
const state*>
ratexp_to_dfa::succ(const formula* f) ratexp_to_dfa::succ(const formula* f)
{ {
f2a_t::const_iterator it = f2a_.find(f); f2a_t::const_iterator it = f2a_.find(f);
tgba_explicit_formula* a; labelled_aut a;
if (it != f2a_.end()) if (it != f2a_.end())
a = it->second; a = it->second;
else else
a = translate(f); a = translate(f);
// If a is nul, f has an empty language. // If a is null, f has an empty language.
if (!a) if (!a.first)
return {nullptr, nullptr}; return std::forward_as_tuple(nullptr, nullptr, nullptr);
assert(a->has_state(f));
// This won't create a new state.
return {a, a->add_state(f)};
}
const formula*
ratexp_to_dfa::get_label(const formula* f, const state* s) const
{
f2a_t::const_iterator it = f2a_.find(f);
assert(it != f2a_.end());
tgba_explicit_formula* a = it->second;
assert(a != 0);
const formula* f2 = a->get_label(s);
f2a_t::const_iterator it2 = f2a_.find(f2);
assert(it2 != f2a_.end());
if (it2->second == 0)
return constant::false_instance();
return f2->clone(); auto namer = a.second;
assert(namer->has_state(f));
auto st = a.first->state_from_number(namer->get_state(f));
return std::forward_as_tuple(a.first, namer, st);
} }
// The rewrite rules used here are adapted from Jean-Michel // The rewrite rules used here are adapted from Jean-Michel
// Couvreur's FM paper, augmented to support rational operators. // Couvreur's FM paper, augmented to support rational operators.
class ltl_trad_visitor: public visitor class ltl_trad_visitor: public visitor
...@@ -1328,22 +1331,25 @@ namespace spot ...@@ -1328,22 +1331,25 @@ namespace spot
const formula* f = node->child(); const formula* f = node->child();
auto p = dict_.transdfa.succ(f); auto p = dict_.transdfa.succ(f);
res_ = bddfalse; res_ = bddfalse;
if (!p.first) auto aut = std::get<0>(p);
auto namer = std::get<1>(p);
auto st = std::get<2>(p);
if (!aut)
break; break;
for (auto i: p.first->succ(p.second)) for (auto i: aut->succ(st))
{ {
bdd label = i->current_condition(); bdd label = i->current_condition();
state* s = i->current_state(); state* s = i->current_state();
const formula* dest = dict_.transdfa.get_label(f, s); const formula* dest =
s->destroy(); namer->get_name(aut->state_number(s));
if (dest->accepts_eword()) if (dest->accepts_eword())
{ {
dest->destroy();
res_ |= label; res_ |= label;
} }
else else
{ {
dest->clone();
const formula* dest2 = unop::instance(op, dest); const formula* dest2 = unop::instance(op, dest);
if (dest2 == constant::false_instance()) if (dest2 == constant::false_instance())
continue; continue;
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment