Commit 450ec22b authored by Etienne Renault's avatar Etienne Renault Committed by Alexandre Duret-Lutz
Browse files

Heuristics for SCC strength

Provides 3 heurisitics to compute the strength of an SCC:
inherent, structural and syntactic

* src/tgbaalgos/isweakscc.cc: implementation
* src/tgbaalgos/isweakscc.hh: definition
parent b4fbbc95
......@@ -20,6 +20,8 @@
# define SPOT_TGBAALGOS_ISWEAKSCC_CC
#include "cycles.hh"
#include "tgba/tgbaexplicit.hh"
#include "ltlast/formula.hh"
namespace spot
{
......@@ -62,18 +64,17 @@ namespace spot
}
};
}
bool
is_weak_scc(scc_map& map, unsigned scc)
is_weak_scc(scc_map& map, unsigned scc, bool easydetect)
{
// If no cycle is accepting, the SCC is weak.
if (!map.accepting(scc))
return true;
// If all transitions use all acceptance conditions, the SCC is weak.
if (map.useful_acc_of(scc) ==
bdd_support(map.get_aut()->neg_acceptance_conditions()))
if (easydetect && map.useful_acc_of(scc) ==
bdd_support(map.get_aut()->neg_acceptance_conditions()))
return true;
// If the SCC is accepting, but one cycle is not, the SCC is not
// weak.
......@@ -82,7 +83,106 @@ namespace spot
return w.result;
}
bool
is_syntactic_weak_scc(const spot::tgba *a, scc_map& map, unsigned scc)
{
const std::list<const spot::state*> states = map.states_of(scc);
std::list<const spot::state*>::const_iterator it;
for (it = states.begin(); it != states.end(); it++)
{
const state_explicit_formula *s =
dynamic_cast<const state_explicit_formula *>(*it);
const ltl::formula *f = dynamic_cast<const ltl::formula*>
(((const tgba_explicit_formula*) a)->get_label(s));
if ((f->is_syntactic_obligation() ||
f->is_syntactic_persistence() ||
f->is_syntactic_safety()))
return true;
}
return false;
}
bool
is_syntactic_terminal_scc(const spot::tgba *a, scc_map& map, unsigned scc)
{
const std::list<const spot::state*> states = map.states_of(scc);
std::list<const spot::state*>::const_iterator it;
for (it = states.begin(); it != states.end(); it++)
{
const state_explicit_formula *s =
dynamic_cast<const state_explicit_formula *>(*it);
const ltl::formula *f = dynamic_cast<const ltl::formula*>
(((const tgba_explicit_formula*) a)->get_label(s));
if (f->is_syntactic_guarantee())
return true;
}
return false;
}
bool
is_weak_heuristic(scc_map& map, unsigned scc)
{
if (!map.accepting (scc))
return true;
if (map.useful_acc_of(scc) ==
bdd_support(map.get_aut()->neg_acceptance_conditions()))
return true;
return false;
}
bool
is_complete_scc(const spot::tgba *a, scc_map& map, unsigned scc)
{
const std::list<const spot::state*> states = map.states_of(scc);
std::list<const spot::state*>::const_iterator it;
for (it = states.begin(); it != states.end(); it++)
{
const state *s = (*it);
tgba_succ_iterator* it = a->succ_iter(s);
it->first();
// No successors cannot be complete
if (it->done())
{
delete it;
return false;
}
bdd sumall = bddfalse;
while (!it->done())
{
const state *next = it->current_state();
unsigned sccnum = map.scc_of_state(next);
// check it's the same scc
if (sccnum == scc)
sumall |= it->current_condition();
next->destroy();
it->next();
}
delete it;
if (sumall != bddtrue)
{
return false;
}
}
return true;
}
bool
is_terminal_heuristic (const tgba *a, scc_map& map, unsigned scc)
{
// If all transitions use all acceptance conditions, the SCC is weak.
if (map.useful_acc_of(scc) ==
bdd_support(map.get_aut()->neg_acceptance_conditions()))
return is_complete_scc(a, map, scc);
return false;
}
}
#endif // SPOT_TGBAALGOS_ISWEAKSCC_CC
......@@ -38,7 +38,50 @@ namespace spot
/// necessarily weak.
/// For other accepting SCCs, this function enumerates all cycles in
/// the given SCC (it stops if it find a non-accepting cycle).
bool is_weak_scc(scc_map& map, unsigned scc);
bool is_weak_scc(scc_map& map, unsigned scc, bool easydetect = true);
/// \brief Whether the SCC number \a scc in \a map is complete
///
/// A SCC is complete iff for all states for all label there exist
/// a transition that stay into this SCC.
bool
is_complete_scc(const tgba *a, scc_map& map, unsigned scc);
/// \brief Whether the SCC number \a scc in \a map is syntactically weak.
///
/// An SCC is syntactically weak iff the lowest label of states inside
/// this SCC corresponds to an obligation label
///
/// Work only on tgba where labels are formula
///
/// The scc_map \a map should have been built already. The absence
/// of accepting cycle is easy to check (the scc_map can tell
/// whether the SCC is non-accepting already). Similarly, an SCC in
/// which all transitions belong to all acceptance sets is
/// necessarily weak.
/// For other accepting SCCs, this function enumerates all cycles in
/// the given SCC (it stops if it find a non-accepting cycle).
bool is_syntactic_weak_scc(const tgba *a, scc_map& map, unsigned scc);
/// \brief wether a SCC is syntactically characterized by a gurarantee
/// formula
///
/// Work only on tgba where labels are formula
bool is_syntactic_terminal_scc(const tgba *a, scc_map& map, unsigned scc);
/// \brief wether a SCC is terminal using an heuristic
///
/// The heuristic try to characterize the SCC by loking if the SCC
/// is complete and all cycle are fully accepting ( all transitions
/// have all acceptance conditions)
bool
is_terminal_heuristic (const tgba *a, scc_map& map, unsigned scc);
/// \brief wether a SCC is weak using an heuristic
///
/// The heuristic looks if all path are fully accepting
bool
is_weak_heuristic(scc_map& map, unsigned scc);
/// @}
}
......
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