Commit 6b5b002f authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

Introduce scc_filter_states().

The main motivation is the upcoming patch that introduces
simulation_sba() and requires this function.

* src/tgbaalgos/sccfilter.hh, src/tgbaalgos/sccfilter.cc: Implement it.
* src/tgbaalgos/postproc.cc: Use it for monitors, because we do not
care about acceptance conditions.
* NEWS: Mention it.
parent 2cab8197
...@@ -24,6 +24,12 @@ New in spot 1.1a (not yet released): ...@@ -24,6 +24,12 @@ New in spot 1.1a (not yet released):
Some illustrations of this point and the previous one can be Some illustrations of this point and the previous one can be
found in the man page for ltl2tgba(1). found in the man page for ltl2tgba(1).
- There is a new function scc_filter_states() that removes all
useless states from a TGBA. It is actually an abbridged version
of scc_filter() that does not alter the acceptance conditions of
the automaton. scc_filter_state() should be used when
post-processing TGBAs that actually represent BAs.
* Bug fixes: * Bug fixes:
- genltl --gh-r generated the wrong formulas due to a typo. - genltl --gh-r generated the wrong formulas due to a typo.
......
...@@ -110,12 +110,20 @@ namespace spot ...@@ -110,12 +110,20 @@ namespace spot
scc_filter_ = 1; scc_filter_ = 1;
// Remove useless SCCs. // Remove useless SCCs.
if (scc_filter_ > 0 || type_ == Monitor) if (type_ == Monitor)
{ {
const tgba* s = scc_filter(a, scc_filter_ > 1); // Do not bother about acceptance conditions, they we be
delete a; // ignored.
a = s; const tgba* s = scc_filter_states(a);
} delete a;
a = s;
}
else if (scc_filter_ > 0)
{
const tgba* s = scc_filter(a, scc_filter_ > 1);
delete a;
a = s;
}
if (type_ == Monitor) if (type_ == Monitor)
{ {
......
...@@ -65,6 +65,53 @@ namespace spot ...@@ -65,6 +65,53 @@ namespace spot
return out_aut->create_transition(in_f, out_f); return out_aut->create_transition(in_f, out_f);
} }
template<class T>
class filter_iter_states: public tgba_reachable_iterator_depth_first
{
public:
typedef T output_t;
filter_iter_states(const tgba* a,
const scc_map& sm,
const std::vector<bool>& useless)
: tgba_reachable_iterator_depth_first(a),
out_(new T(a->get_dict())),
sm_(sm),
useless_(useless)
{
a->get_dict()->register_all_variables_of(a, out_);
out_->set_acceptance_conditions(a->all_acceptance_conditions());
}
T*
result()
{
return out_;
}
bool
want_state(const state* s) const
{
return !useless_[sm_.scc_of_state(s)];
}
void
process_link(const state* in_s, int in,
const state* out_s, int out,
const tgba_succ_iterator* si)
{
typename output_t::state::transition* t =
create_transition(this->aut_, out_, in_s, in, out_s, out);
t->condition = si->current_condition();
t->acceptance_conditions = si->current_acceptance_conditions();
}
protected:
T* out_;
const scc_map& sm_;
const std::vector<bool>& useless_;
};
template<class T> template<class T>
class filter_iter: public tgba_reachable_iterator_depth_first class filter_iter: public tgba_reachable_iterator_depth_first
{ {
...@@ -495,4 +542,55 @@ namespace spot ...@@ -495,4 +542,55 @@ namespace spot
return ret; return ret;
} }
tgba* scc_filter_states(const tgba* aut, scc_map* given_sm)
{
scc_map* sm = given_sm;
if (!sm)
{
sm = new scc_map(aut);
sm->build_map();
}
scc_stats ss = build_scc_stats(*sm);
tgba* ret;
const tgba_explicit_formula* af =
dynamic_cast<const tgba_explicit_formula*>(aut);
if (af)
{
filter_iter_states<tgba_explicit_formula> fi(af, *sm,
ss.useless_scc_map);
fi.run();
tgba_explicit_formula* res = fi.result();
res->merge_transitions();
ret = res;
}
else
{
const tgba_explicit_string* as =
dynamic_cast<const tgba_explicit_string*>(aut);
if (as)
{
filter_iter_states<tgba_explicit_string> fi(aut, *sm,
ss.useless_scc_map);
fi.run();
tgba_explicit_string* res = fi.result();
res->merge_transitions();
ret = res;
}
else
{
filter_iter_states<tgba_explicit_number> fi(aut, *sm,
ss.useless_scc_map);
fi.run();
tgba_explicit_number* res = fi.result();
res->merge_transitions();
ret = res;
}
}
if (!given_sm)
delete sm;
return ret;
}
} }
// Copyright (C) 2009, 2010, 2012 Laboratoire de Recherche et // Copyright (C) 2009, 2010, 2012, 2013 Laboratoire de Recherche et
// Developpement de l'Epita (LRDE). // Developpement de l'Epita (LRDE).
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
...@@ -56,10 +56,24 @@ namespace spot ...@@ -56,10 +56,24 @@ namespace spot
/// variable are also removed from transitions entering an accepting /// variable are also removed from transitions entering an accepting
/// SCC. ignored is a conjunction of positive variables that should /// SCC. ignored is a conjunction of positive variables that should
/// be removed everywhere. /// be removed everywhere.
///
/// \warning Calling scc_filter on a TGBA that has the SBA property
/// (i.e., transitions leaving accepting states are all marked as
/// accepting) may destroy this property. Use scc_filter_states()
/// instead.
tgba* scc_filter(const tgba* aut, bool remove_all_useless = false, tgba* scc_filter(const tgba* aut, bool remove_all_useless = false,
scc_map* given_sm = 0, bdd susp = bddtrue, scc_map* given_sm = 0, bdd susp = bddtrue,
bool early_susp = false, bdd ignored = bddtrue); bool early_susp = false, bdd ignored = bddtrue);
/// \brief Prune unaccepting SCCs.
///
/// This is an abridged version of scc_filter(), that only remove
/// useless states, without touching at the acceptance conditions.
///
/// Especially, if the input TGBA has the SBA property, (i.e.,
/// transitions leaving accepting states are all marked as
/// accepting), then the output TGBA will also have that property.
tgba* scc_filter_states(const tgba* aut, scc_map* given_sm = 0);
} }
#endif // SPOT_TGBAALGOS_SCC_HH #endif // SPOT_TGBAALGOS_SCC_HH
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