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

tba_determinize: add a cycle_threshold

Browse source 
* src/tgbaalgos/powerset.cc, src/tgbaalgos/powerset.hh
(tba_determinize, tba_determinize_check): Add a cycle_threshold
argument.
* src/tgbaalgos/postproc.cc: Use it.
* src/tgbatest/ltl2tgba.cc: Adjust calls.
This commit is contained in:
Alexandre Duret-Lutz 2013-01-22 18:53:45 +01:00
parent 0117fc2c36
commit 63b7cdb6c8
4 changed files with 77 additions and 36 deletions
Download patch file Download diff file Expand all files Collapse all files

24
src/tgbaalgos/postproc.cc
View file

@ -224,16 +224,24 @@ namespace spot
&& sim->number_of_acceptance_conditions() > 1)
tmpd = new tgba_tba_proxy(sim);
// This threshold is arbitrary. For producing Small automata,
// we assume that a deterministic automaton that is twice the
// size of the original will never get reduced to a smaller
// one. For Deterministic automata, we accept automata that
// are 4 times bigger. The larger the value, the more likely
// the cycle enumeration algorithm will encounter an automaton
// that takes *eons* to explore.
const tgba* in = tmpd ? tmpd : sim;
// These thresholds is arbitrary.
//
// For producing Small automata, we assume that a
// deterministic automaton that is twice the size of the
// original will never get reduced to a smaller one. We also
// do not want more than 2^13 cycles in an SCC.
//
// For Deterministic automata, we accept automata that
// are 8 times bigger, with no more that 2^15 cycle per SCC.
// The cycle threshold is the most important limit here. You
// may up it if you want to try producing larger automata.
const tgba* tmp =
tba_determinize_check(in, (pref_ == Small) ? 2 : 4, f);
tba_determinize_check(in,
(pref_ == Small) ? 2 : 8,
1 << ((pref_ == Small) ? 13 : 15),
f);
if (tmp != 0 && tmp != in)
{
// There is no point in running the reverse simulation on

56
src/tgbaalgos/powerset.cc
View file

@ -143,20 +143,25 @@ namespace spot
protected:
const tgba* ref_;
power_map& refmap_;
trans_set reject_; // set of rejecting transitions
set_set accept_; // set of cycles that are accepting
trans_set all_; // all non rejecting transitions
trans_set reject_; // set of rejecting transitions
set_set accept_; // set of cycles that are accepting
trans_set all_; // all non rejecting transitions
unsigned threshold_; // maximum count of enumerated cycles
unsigned cycles_left_; // count of cycles left to explore
public:
fix_scc_acceptance(const scc_map& sm, const tgba* ref, power_map& refmap)
: enumerate_cycles(sm), ref_(ref), refmap_(refmap)
fix_scc_acceptance(const scc_map& sm, const tgba* ref, power_map& refmap,
unsigned threshold)
: enumerate_cycles(sm), ref_(ref), refmap_(refmap),
threshold_(threshold)
{
}
void fix_scc(const int m)
bool fix_scc(const int m)
{
reject_.clear();
accept_.clear();
cycles_left_ = threshold_;
run(m);
// std::cerr << "SCC #" << m << "\n";
@ -176,6 +181,7 @@ namespace spot
{
(*i)->acceptance_conditions = acc;
}
return threshold_ != 0 && cycles_left_ == 0;
}
bool is_cycle_accepting(cycle_iter begin, trans_set& ts) const
@ -279,13 +285,17 @@ namespace spot
}
}
return true;
// Abort this algorithm if we have seen too much cycles, i.e.,
// when cycle_left_ *reaches* 0. (If cycle_left_ == 0, that
// means we had no limit.)
return (cycles_left_ == 0) || --cycles_left_;
}
};
static void
static bool
fix_dba_acceptance(tgba_explicit_number* det,
const tgba* ref, power_map& refmap)
const tgba* ref, power_map& refmap,
unsigned threshold)
{
det->copy_acceptance_conditions_of(ref);
@ -294,36 +304,45 @@ namespace spot
unsigned scc_count = sm.scc_count();
fix_scc_acceptance fsa(sm, ref, refmap);
fix_scc_acceptance fsa(sm, ref, refmap, threshold);
for (unsigned m = 0; m < scc_count; ++m)
fsa.fix_scc(m);
if (!sm.trivial(m))
if (fsa.fix_scc(m))
return true;
return false;
}
}
tgba_explicit_number*
tba_determinize(const tgba* aut, unsigned threshold)
tba_determinize(const tgba* aut,
unsigned threshold_states, unsigned threshold_cycles)
{
power_map pm;
// Do not merge transitions in the deterministic automaton. If we
// add two self-loops labeled by "a" and "!a", we do not want
// these to be merged as "1" before the acceptance has been fixed.
tgba_explicit_number* det = tgba_powerset(aut, pm, false);
if ((threshold > 0)
&& (pm.map_.size() > pm.states.size() * threshold))
if ((threshold_states > 0)
&& (pm.map_.size() > pm.states.size() * threshold_states))
{
delete det;
return 0;
}
if (fix_dba_acceptance(det, aut, pm, threshold_cycles))
{
delete det;
return 0;
}
fix_dba_acceptance(det, aut, pm);
det->merge_transitions();
return det;
}
tgba*
tba_determinize_check(const tgba* aut,
unsigned threshold,
unsigned threshold_states,
unsigned threshold_cycles,
const ltl::formula* f,
const tgba* neg_aut)
{
@ -333,7 +352,8 @@ namespace spot
if (aut->number_of_acceptance_conditions() > 1)
return 0;
tgba_explicit_number* det = tba_determinize(aut, threshold);
tgba_explicit_number* det =
tba_determinize(aut, threshold_states, threshold_cycles);
if (!det)
return 0;

29
src/tgbaalgos/powerset.hh
View file

@ -123,11 +123,18 @@ namespace spot
/// \endverbatim
/// only adapted to work on TBA rather than BA.
///
/// If \a threshold is non null, abort the construction whenever it
/// would build an automaton that is more than \a threshold time
/// bigger (in term of states) than the original automaton.
/// If \a threshold_states is non null, abort the construction
/// whenever it would build an automaton that is more than \a
/// threshold_states time bigger (in term of states) than the
/// original automaton.
///
/// If \a threshold_cycles is non null, abort the construction
/// whenever an SCC of the constructed automaton has more than \a
/// threshold_cycles cycles.
SPOT_API tgba_explicit_number*
tba_determinize(const tgba* aut, unsigned threshold = 0);
tba_determinize(const tgba* aut,
unsigned threshold_states = 0,
unsigned threshold_cycles = 0);
/// \brief Determinize a TBA and make sure it is correct.
///
@ -139,9 +146,14 @@ namespace spot
///
/// \param aut the automaton to minimize
///
/// \param threshold if non null, abort the construction whenever it
/// would build an automaton that is more than \a threshold time
/// bigger (in term of states) than the original automaton.
/// \param threshold_states if non null, abort the construction
/// whenever it would build an automaton that is more than \a
/// threshold time bigger (in term of states) than the original
/// automaton.
///
/// \param threshold_cycles can be used to abort the construction
/// if the number of cycles in a SCC of the constructed automaton
/// is bigger than the supplied value.
///
/// \param f the formula represented by the original automaton
///
@ -153,7 +165,8 @@ namespace spot
/// were supplied.
SPOT_API tgba*
tba_determinize_check(const tgba* aut,
unsigned threshold = 0,
unsigned threshold_states = 0,
unsigned threshold_cycles = 0,
const ltl::formula* f = 0,
const tgba* neg_aut = 0);

4
src/tgbatest/ltl2tgba.cc
View file

@ -1451,7 +1451,7 @@ main(int argc, char** argv)
&& (!f || f->is_syntactic_recurrence()))
{
tm.start("determinization");
determinized = tba_determinize(a, opt_determinize_threshold);
determinized = tba_determinize(a, 0, opt_determinize_threshold);
tm.stop("determinization");
if (determinized)
a = determinized;
@ -1713,7 +1713,7 @@ main(int argc, char** argv)
{
std::cout << "this is not an obligation property";
const spot::tgba* tmp =
tba_determinize_check(a, opt_o_threshold, f, 0);
tba_determinize_check(a, 0, opt_o_threshold, f, 0);
if (tmp != 0 && tmp != a)
{
std::cout << ", but it is a recurrence property";