Commit 637aeff2 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

compsusp: Use new implem of scc_filter to remove suspended variables

* src/tgbaalgos/sccfilter.cc, src/tgbaalgos/sccfilter.hh: Rewrite all
composable filters in a way that allow arguments to be passed.
(scc_filter_susp): New function.
* src/tgbaalgos/sccinfo.cc, src/tgbaalgos/sccinfo.hh (scc_ap_support):
New method.
* src/tgbaalgos/compsusp.cc: Adjust to use tgba_digraph, and
call the new scc_filter_susp().
parent 1244b617
...@@ -19,12 +19,13 @@ ...@@ -19,12 +19,13 @@
#include "compsusp.hh" #include "compsusp.hh"
#include "sccfilter.hh" #include "sccfilter.hh"
#include "scc.hh" #include "sccinfo.hh"
#include "tgba/tgbagraph.hh" #include "tgba/tgbagraph.hh"
#include "ltl2tgba_fm.hh" #include "ltl2tgba_fm.hh"
#include "minimize.hh" #include "minimize.hh"
#include "simulation.hh" #include "simulation.hh"
#include "safety.hh" #include "safety.hh"
#include "dupexp.hh"
#include "ltlast/allnodes.hh" #include "ltlast/allnodes.hh"
#include "ltlvisit/tostring.hh" #include "ltlvisit/tostring.hh"
#include "ltlvisit/clone.hh" #include "ltlvisit/clone.hh"
...@@ -211,15 +212,15 @@ namespace spot ...@@ -211,15 +212,15 @@ namespace spot
typedef std::deque<state_pair> pair_queue; typedef std::deque<state_pair> pair_queue;
static static
tgba* tgba_digraph*
susp_prod(tgba* left, const ltl::formula* f, bdd v) susp_prod(tgba* left, const ltl::formula* f, bdd v)
{ {
bdd_dict* dict = left->get_dict(); bdd_dict* dict = left->get_dict();
const tgba* a1 = ltl_to_tgba_fm(f, dict, true, true); const tgba_digraph* a1 = ltl_to_tgba_fm(f, dict, true, true);
const tgba* a2 = scc_filter(a1, false); const tgba_digraph* a2 = scc_filter(a1, false);
delete a1; delete a1;
const tgba* right = iterated_simulations(a2); const tgba_digraph* right = iterated_simulations(a2);
delete a2; delete a2;
tgba_digraph* res = new tgba_digraph(dict); tgba_digraph* res = new tgba_digraph(dict);
...@@ -359,10 +360,11 @@ namespace spot ...@@ -359,10 +360,11 @@ namespace spot
ltl_suspender_visitor v(g2s, a2o, oblig); ltl_suspender_visitor v(g2s, a2o, oblig);
const ltl::formula* g = v.recurse(f); const ltl::formula* g = v.recurse(f);
tgba* res; tgba_digraph* res;
{ {
// Translate the patched formula, and remove useless SCCs. // Translate the patched formula, and remove useless SCCs.
tgba* aut = spot::ltl_to_tgba_fm(g, dict, true, true, false, false, 0, 0); tgba_digraph* aut =
spot::ltl_to_tgba_fm(g, dict, true, true, false, false, 0, 0);
res = scc_filter(aut, false); res = scc_filter(aut, false);
delete aut; delete aut;
} }
...@@ -373,14 +375,21 @@ namespace spot ...@@ -373,14 +375,21 @@ namespace spot
if (min != res) if (min != res)
{ {
delete res; delete res;
res = min; // FIXME: minimize_obligation does not yet return a
// tgba_digraph, so we convert the result using dupexp.
// Once minimize_obligation is fixed, we should remove the
// call to dupexp.
assert(dynamic_cast<tgba_digraph*>(min) == nullptr);
res = tgba_dupexp_dfs(min);
delete min;
//res = min;
no_simulation = true; no_simulation = true;
} }
} }
if (!no_simulation) if (!no_simulation)
{ {
tgba* sim = spot::iterated_simulations(res); tgba_digraph* sim = spot::iterated_simulations(res);
delete res; delete res;
res = sim; res = sim;
} }
...@@ -407,21 +416,20 @@ namespace spot ...@@ -407,21 +416,20 @@ namespace spot
suspvars &= i->second; suspvars &= i->second;
bdd allaccap = bddtrue; // set of atomic prop used in accepting SCCs. bdd allaccap = bddtrue; // set of atomic prop used in accepting SCCs.
tgba* aut = res; tgba_digraph* aut = res;
{ {
scc_map sm(aut); scc_info si(aut);
sm.build_map();
// Restrict suspvars to the set of suspension labels that occur // Restrict suspvars to the set of suspension labels that occur
// in accepting SCC. // in accepting SCC.
unsigned sn = sm.scc_count(); unsigned sn = si.scc_count();
for (unsigned n = 0; n < sn; n++) for (unsigned n = 0; n < sn; n++)
if (sm.accepting(n)) if (si.is_accepting_scc(n))
allaccap &= sm.ap_set_of(n); allaccap &= si.scc_ap_support(n);
bdd ignored = bdd_exist(suspvars, allaccap); bdd ignored = bdd_exist(suspvars, allaccap);
suspvars = bdd_existcomp(suspvars, allaccap); suspvars = bdd_existcomp(suspvars, allaccap);
res = scc_filter(aut, false, &sm, suspvars, early_susp, ignored); res = scc_filter_susp(aut, false, suspvars, ignored, early_susp, &si);
} }
delete aut; delete aut;
......
...@@ -254,80 +254,11 @@ namespace spot ...@@ -254,80 +254,11 @@ namespace spot
remap_t remap_; remap_t remap_;
}; };
template<class T>
class filter_iter_susp: public filter_iter<T>
{
public:
typedef filter_iter<T> super;
filter_iter_susp(const tgba* a,
const scc_map& sm,
const std::vector<bool>& useless,
remap_table_t& remap_table,
unsigned max_num,
bool remove_all_useless,
bdd susp_pos, bool early_susp, bdd ignored)
: super(a, sm, useless, remap_table, max_num, remove_all_useless),
susp_pos(susp_pos), early_susp(early_susp), ignored(ignored)
{
}
void
process_link(const state* in_s, int in,
const state* out_s, int out,
const tgba_succ_iterator* si)
{
unsigned u = this->sm_.scc_of_state(out_s);
unsigned v = this->sm_.scc_of_state(in_s);
bool destacc = this->sm_.accepting(u);
typename super::output_t::state::transition* t =
create_transition(this->aut_, this->out_, in_s, in, out_s, out);
bdd cond = bdd_exist(si->current_condition(), ignored);
// Remove suspended variables on transitions going to
// non-accepting SCC, or on transition between SCC unless
// early_susp is set.
if (!destacc || (!early_susp && (u != this->sm_.scc_of_state(in_s))))
cond = bdd_exist(cond, susp_pos);
this->out_->add_conditions(t, cond);
// Regardless of all_, do not output any acceptance condition
// if the destination is not in an accepting SCC.
//
// If all_ is set, do not output any acceptance condition if the
// source is not in the same SCC as dest.
//
// (See the documentation of scc_filter() for a rational.)
if (destacc && (!this->all_ || u == v))
{
bdd acc = si->current_acceptance_conditions();
if (acc == bddfalse)
return;
typename super::map_t::const_iterator i =
this->remap_[u].find(acc.id());
if (i != this->remap_[u].end())
{
t->acceptance_conditions = i->second;
}
else
{
// t->acceptance_conditions = this->remap_[v][acc.id()];
}
}
}
protected:
bdd susp_pos;
bool early_susp;
bdd ignored;
};
} // anonymous } // anonymous
tgba* scc_filter(const tgba* aut, bool remove_all_useless, tgba* scc_filter(const tgba* aut, bool remove_all_useless,
scc_map* given_sm, bdd susp, bool early_susp, bdd ignored) scc_map* given_sm)
{ {
scc_map* sm = given_sm; scc_map* sm = given_sm;
if (!sm) if (!sm)
...@@ -482,30 +413,14 @@ namespace spot ...@@ -482,30 +413,14 @@ namespace spot
dynamic_cast<const tgba_explicit_formula*>(aut); dynamic_cast<const tgba_explicit_formula*>(aut);
if (af) if (af)
{ {
if (susp == bddtrue) filter_iter<tgba_explicit_formula> fi(af, *sm,
{ ss.useless_scc_map,
filter_iter<tgba_explicit_formula> fi(af, *sm, remap_table, max_num,
ss.useless_scc_map, remove_all_useless);
remap_table, max_num, fi.run();
remove_all_useless); tgba_explicit_formula* res = fi.result();
fi.run(); res->merge_transitions();
tgba_explicit_formula* res = fi.result(); ret = res;
res->merge_transitions();
ret = res;
}
else
{
filter_iter_susp<tgba_explicit_formula> fi(af, *sm,
ss.useless_scc_map,
remap_table, max_num,
remove_all_useless,
susp, early_susp,
ignored);
fi.run();
tgba_explicit_formula* res = fi.result();
res->merge_transitions();
ret = res;
}
} }
else else
{ {
...@@ -523,30 +438,14 @@ namespace spot ...@@ -523,30 +438,14 @@ namespace spot
} }
else else
{ {
if (susp == bddtrue) filter_iter<tgba_explicit_number> fi(aut, *sm,
{ ss.useless_scc_map,
filter_iter<tgba_explicit_number> fi(aut, *sm, remap_table, max_num,
ss.useless_scc_map, remove_all_useless);
remap_table, max_num, fi.run();
remove_all_useless); tgba_explicit_number* res = fi.result();
fi.run(); res->merge_transitions();
tgba_explicit_number* res = fi.result(); ret = res;
res->merge_transitions();
ret = res;
}
else
{
filter_iter_susp<tgba_explicit_number> fi(aut, *sm,
ss.useless_scc_map,
remap_table, max_num,
remove_all_useless,
susp, early_susp,
ignored);
fi.run();
tgba_explicit_number* res = fi.result();
res->merge_transitions();
ret = res;
}
} }
} }
if (!given_sm) if (!given_sm)
...@@ -621,6 +520,7 @@ namespace spot ...@@ -621,6 +520,7 @@ namespace spot
typedef std::tuple<bool, bdd, bdd> filtered_trans; typedef std::tuple<bool, bdd, bdd> filtered_trans;
typedef std::pair<bdd, bdd> acc_pair; typedef std::pair<bdd, bdd> acc_pair;
// SCC filters are objects with two methods: // SCC filters are objects with two methods:
// state(src) return true iff s should be kept // state(src) return true iff s should be kept
// trans(src, dst, cond, acc) returns a triplet // trans(src, dst, cond, acc) returns a triplet
...@@ -654,87 +554,153 @@ namespace spot ...@@ -654,87 +554,153 @@ namespace spot
}; };
// Remove useless states. // Remove useless states.
struct state_filter: id_filter template <class next_filter = id_filter>
struct state_filter: next_filter
{ {
state_filter(scc_info* si) template<typename... Args>
: id_filter(si) state_filter(scc_info* si, Args&&... args)
: next_filter(si, std::forward<Args>(args)...)
{ {
} }
bool state(unsigned s) bool state(unsigned s)
{ {
return si->is_useful_state(s); return this->next_filter::state(s) && this->si->is_useful_state(s);
}
};
// Suspension filter, used only by compsusp.cc
template <class next_filter = id_filter>
struct susp_filter: next_filter
{
bdd suspvars;
bdd ignoredvars;
bool early_susp;
template<typename... Args>
susp_filter(scc_info* si,
bdd suspvars, bdd ignoredvars, bool early_susp,
Args&&... args)
: next_filter(si, std::forward<Args>(args)...),
suspvars(suspvars),
ignoredvars(ignoredvars),
early_susp(early_susp)
{
}
filtered_trans trans(unsigned src, unsigned dst,
bdd cond, bdd acc)
{
bool keep;
std::tie(keep, cond, acc) =
this->next_filter::trans(src, dst, cond, acc);
if (keep)
{
// Always remove ignored variables
cond = bdd_exist(cond, ignoredvars);
// Remove the suspension variables only if
// the destination in not in an accepting SCC,
// or if we are between SCC with early_susp unset.
unsigned u = this->si->scc_of(dst);
if (!this->si->is_accepting_scc(u)
|| (!early_susp && (u != this->si->scc_of(src))))
cond = bdd_exist(cond, suspvars);
}
return filtered_trans(keep, cond, acc);
} }
}; };
// Remove acceptance conditions from all transitions outside of // Remove acceptance conditions from all transitions outside of
// non-accepting SCCs. // non-accepting SCCs.
struct acc_filter_all: id_filter template <class next_filter = id_filter>
struct acc_filter_all: next_filter
{ {
acc_filter_all(scc_info* si) template<typename... Args>
: id_filter(si) acc_filter_all(scc_info* si, Args&&... args)
: next_filter(si, std::forward<Args>(args)...)
{ {
} }
filtered_trans trans(unsigned src, unsigned dst, filtered_trans trans(unsigned src, unsigned dst,
bdd cond, bdd acc) bdd cond, bdd acc)
{ {
unsigned u = si->scc_of(src); bool keep;
// If the transition is between two SCCs, or in a std::tie(keep, cond, acc) =
// non-accepting SCC. Remove the acceptance sets. this->next_filter::trans(src, dst, cond, acc);
if (!si->is_accepting_scc(u) || u != si->scc_of(dst))
acc = bddfalse;
return filtered_trans(true, cond, acc); if (keep)
{
unsigned u = this->si->scc_of(src);
// If the transition is between two SCCs, or in a
// non-accepting SCC. Remove the acceptance sets.
if (!this->si->is_accepting_scc(u) || u != this->si->scc_of(dst))
acc = bddfalse;
}
return filtered_trans(keep, cond, acc);
} }
}; };
// Remove acceptance conditions from all transitions whose // Remove acceptance conditions from all transitions whose
// destination is not an accepting SCCs. // destination is not an accepting SCCs.
struct acc_filter_some: id_filter template <class next_filter = id_filter>
struct acc_filter_some: next_filter
{ {
acc_filter_some(scc_info* si) template<typename... Args>
: id_filter(si) acc_filter_some(scc_info* si, Args&&... args)
: next_filter(si, std::forward<Args>(args)...)
{ {
} }
filtered_trans trans(unsigned, unsigned dst, filtered_trans trans(unsigned src, unsigned dst,
bdd cond, bdd acc) bdd cond, bdd acc)
{ {
if (!si->is_accepting_scc(si->scc_of(dst))) bool keep;
std::tie(keep, cond, acc) =
this->next_filter::trans(src, dst, cond, acc);
if (!this->si->is_accepting_scc(this->si->scc_of(dst)))
acc = bddfalse; acc = bddfalse;
return filtered_trans(true, cond, acc); return filtered_trans(keep, cond, acc);
} }
}; };
// // Simplify redundant acceptance sets used in each SCCs.
struct acc_filter_simplify: id_filter template <class next_filter = id_filter>
struct acc_filter_simplify: next_filter
{ {
std::vector<bdd> acc_; std::vector<bdd> acc_;
typedef std::map<int, bdd> map_t; typedef std::map<int, bdd> map_t;
typedef std::vector<map_t> remap_t; typedef std::vector<map_t> remap_t;
remap_t remap_; remap_t remap_;
acc_filter_simplify(scc_info* si) template<typename... Args>
: id_filter(si) acc_filter_simplify(scc_info* si, Args&&... args)
: next_filter(si, std::forward<Args>(args)...)
{ {
} }
acc_pair accsets(bdd in_all, bdd in_all_neg) acc_pair accsets(bdd in_all, bdd in_all_neg)
{ {
unsigned scc_count = si->scc_count(); std::tie(in_all, in_all_neg) =
this->next_filter::accsets(in_all, in_all_neg);
unsigned scc_count = this->si->scc_count();
remap_table_t remap_table(scc_count); remap_table_t remap_table(scc_count);
std::vector<unsigned> max_table(scc_count); std::vector<unsigned> max_table(scc_count);
std::vector<bdd> useful_table(scc_count); std::vector<bdd> useful_table(scc_count);
std::vector<bdd> useless_table(scc_count); std::vector<bdd> useless_table(scc_count);
unsigned max_num = 1; unsigned max_num = 1;
const tgba_digraph* aut = si->get_aut(); const tgba_digraph* aut = this->si->get_aut();
std::vector<bdd> used_acc = si->used_acc(); std::vector<bdd> used_acc = this->si->used_acc();
for (unsigned n = 0; n < scc_count; ++n) for (unsigned n = 0; n < scc_count; ++n)
{ {
if (!si->is_accepting_scc(n)) if (!this->si->is_accepting_scc(n))
continue; continue;
bdd all = used_acc[n]; bdd all = used_acc[n];
...@@ -834,7 +800,7 @@ namespace spot ...@@ -834,7 +800,7 @@ namespace spot
// that do not have enough. // that do not have enough.
for (unsigned n = 0; n < scc_count; ++n) for (unsigned n = 0; n < scc_count; ++n)
{ {
if (!si->is_accepting_scc(n)) if (!this->si->is_accepting_scc(n))
continue; continue;
//std::cerr << "SCC " << n << '\n'; //std::cerr << "SCC " << n << '\n';
bdd useful = useful_table[n]; bdd useful = useful_table[n];
...@@ -898,7 +864,7 @@ namespace spot ...@@ -898,7 +864,7 @@ namespace spot
for (unsigned n = 0; n < scc_count; ++n) for (unsigned n = 0; n < scc_count; ++n)
{ {
//std::cerr << "SCC #" << n << '\n'; //std::cerr << "SCC #" << n << '\n';
if (!si->is_accepting_scc(n)) if (!this->si->is_accepting_scc(n))
continue; continue;
bdd all = used_acc[n]; bdd all = used_acc[n];
...@@ -929,80 +895,37 @@ namespace spot ...@@ -929,80 +895,37 @@ namespace spot
return acc_pair{all, all_neg}; return acc_pair{all, all_neg};
} }
filtered_trans trans(unsigned src, unsigned, bdd cond, bdd acc) filtered_trans trans(unsigned src, unsigned dst, bdd cond, bdd acc)
{ {
if (acc != bddfalse) bool keep;
std::tie(keep, cond, acc) =
this->next_filter::trans(src, dst, cond, acc);
if (keep && acc != bddfalse)
{ {
unsigned u = si->scc_of(src); unsigned u = this->si->scc_of(src);
auto i = remap_[u].find(acc.id()); auto i = remap_[u].find(acc.id());
if (i != remap_[u].end()) if (i != remap_[u].end())
acc = i->second; acc = i->second;
else else
acc = bddfalse; acc = bddfalse;
} }
return filtered_trans{true, cond, acc}; return filtered_trans{keep, cond, acc};
} }
}; };