alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

isweakscc: cleanup interfaces and code

Browse source 
* src/tgbaalgos/isweakscc.cc, src/tgbaalgos/isweakscc.hh: Do not pass
automata since they are known from the scc.  Avoid several dynamic
casts.  Try to match the established vocabulary wrt "weak" and
"inherently weak".  The old is_weak_scc() that used to enumerate cycles
is therefore renamed to is_inherently_weak_scc(), while the new
is_weak_scc() will should ensure all transitions are fully accepting.
* NEWS: Mention the new interface.
This commit is contained in:
Alexandre Duret-Lutz 2013-04-27 20:02:11 +02:00
parent 450ec22bc3
commit cb7cd868a5
3 changed files with 116 additions and 99 deletions
Download patch file Download diff file Expand all files Collapse all files

13
NEWS
View file

@ -56,6 +56,19 @@ New in spot 1.0.2a (not released):
with the favor_event_univ option of ltl_simplifier. As
always please check doc/tl/tl.tex for the list of rules.
- Several functions have been introduced to check the
strength of an SCC.
is_inherently_weak_scc()
is_weak_scc()
is_syntactic_weak_scc()
is_complete_scc()
is_terminal_scc()
is_syntactic_terminal_scc()
Beware that the costly is_weak_scc() function introduced in Spot
1.0, which is based on a cycle enumeration, has been renammed to
is_inherently_weak_scc() to match established vocabulary.
* Command-line tools:
- ltl2tgba and ltl2tgta now honor a new --extra-options (or -x)

106
src/tgbaalgos/isweakscc.cc
View file

@ -1,5 +1,5 @@
// Copyright (C) 2012 Laboratoire de Recherche et Developpement de
// l'Epita (LRDE).
// Copyright (C) 2012, 2013 Laboratoire de Recherche et Developpement
// de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
//
@ -67,15 +67,11 @@ namespace spot
}
bool
is_weak_scc(scc_map& map, unsigned scc, bool easydetect)
is_inherently_weak_scc(scc_map& map, unsigned scc)
{
// 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 (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.
weak_checker w(map);
@ -84,104 +80,106 @@ namespace spot
}
bool
is_syntactic_weak_scc(const spot::tgba *a, scc_map& map, unsigned scc)
is_weak_scc(scc_map& map, unsigned scc)
{
// 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.
return (map.useful_acc_of(scc)
== bdd_support(map.get_aut()->neg_acceptance_conditions()));
}
bool
is_syntactic_weak_scc(scc_map& map, unsigned scc)
{
const tgba_explicit_formula* aut =
dynamic_cast<const tgba_explicit_formula*>(map.get_aut());
if (!aut)
return false;
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++)
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()))
const state_explicit_formula* s =
down_cast<const state_explicit_formula*>(*it);
assert(s);
if (aut->get_label(s)->is_syntactic_persistence())
return true;
}
return false;
}
bool
is_syntactic_terminal_scc(const spot::tgba *a, scc_map& map, unsigned scc)
is_syntactic_terminal_scc(scc_map& map, unsigned scc)
{
const tgba_explicit_formula* aut =
dynamic_cast<const tgba_explicit_formula*>(map.get_aut());
if (!aut)
return false;
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++)
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())
const state_explicit_formula* s =
down_cast<const state_explicit_formula*>(*it);
assert(s);
if (aut->get_label(s)->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)
is_complete_scc(scc_map& map, unsigned scc)
{
const spot::tgba *a = map.get_aut();
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++)
for (it = states.begin(); it != states.end(); ++it)
{
const state *s = (*it);
const state *s = *it;
tgba_succ_iterator* it = a->succ_iter(s);
it->first();
// No successors cannot be complete
// If a state has no successors, the SCC is not complete.
if (it->done())
{
delete it;
return false;
}
// Sum guards on all outgoing transitions.
bdd sumall = bddfalse;
while (!it->done())
do
{
const state *next = it->current_state();
unsigned sccnum = map.scc_of_state(next);
// check it's the same scc
if (sccnum == scc)
if (map.scc_of_state(next) == scc)
sumall |= it->current_condition();
next->destroy();
if (sumall == bddtrue)
break;
it->next();
}
while (!it->done());
delete it;
if (sumall != bddtrue)
{
return false;
}
return false;
}
return true;
}
bool
is_terminal_heuristic (const tgba *a, scc_map& map, unsigned scc)
is_terminal_scc(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;
return ((map.useful_acc_of(scc) ==
bdd_support(map.get_aut()->neg_acceptance_conditions()))
&& is_complete_scc(map, scc));
}
}

96
src/tgbaalgos/isweakscc.hh
View file

@ -1,4 +1,4 @@
// Copyright (C) 2012 Laboratoire de Recherche et Developpement de
// Copyright (C) 2012, 2013 Laboratoire de Recherche et Developpement de
// l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
@ -26,62 +26,68 @@ namespace spot
/// \addtogroup tgba_misc
/// @{
/// \brief Whether the SCC number \a scc in \a map is inherently
/// weak.
///
/// An SCC is inherently weak if either its cycles are all
/// accepting, or they are all non-accepting.
///
/// Note the terminal SCCs are also inherently weak with that
/// definition.
///
/// 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_inherently_weak_scc(scc_map& map, unsigned scc);
/// \brief Whether the SCC number \a scc in \a map is weak.
///
/// An SCC is weak if either its cycles are all accepting, or they
/// are all non-accepting.
/// An SCC is weak if its non-accepting, or if all its transition
/// are fully accepting (i.e., the belong to all acceptance sets).
///
/// 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_weak_scc(scc_map& map, unsigned scc, bool easydetect = true);
/// Note that terminal SCCs are also weak with that definition.
///
/// The scc_map \a map should have been built already.
bool is_weak_scc(scc_map& map, unsigned scc);
/// \brief Whether the SCC number \a scc in \a map is complete
/// \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);
/// An SCC is complete iff for all states and all label there exists
/// a transition that stays into this SCC.
///
/// The scc_map \a map should have been built already.
bool is_complete_scc(scc_map& map, unsigned scc);
/// \brief Whether the SCC number \a scc in \a map is syntactically weak.
/// \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
/// This works only on tgba whose labels are formulas. An SCC is
/// syntactically weak if one of its states is labeled by a
/// syntactic-persistence formula.
///
/// 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);
/// The scc_map \a map should have been built already.
bool is_syntactic_weak_scc(scc_map& map, unsigned scc);
/// \brief wether a SCC is syntactically characterized by a gurarantee
/// formula
/// \brief Whether the SCC number \a scc in \a map is syntactically
/// terminal.
///
/// 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
/// This works only on tgba whose labels are formulas. An SCC is
/// syntactically terminal if one of its states is labeled by a
/// syntactic-guarantee formula.
///
/// 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);
/// The scc_map \a map should have been built already.
bool is_syntactic_terminal_scc(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);
/// \brief Whether the SCC number \a scc in \a map is terminal.
///
/// An SCC is terminal if it is weak, complete, and accepting.
///
/// The scc_map \a map should have been built already.
bool is_terminal_scc(scc_map& map, unsigned scc);
/// @}
}