Commit 07ab225c authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz

dba_determinize: Add a threshold argument.

* src/tgbaalgos/powerset.cc, src/tgbaalgos/powerset.hh
(dba_determinize, dba_determinize_check): Add a threshold
argument.
* src/tgbatest/ltl2tgba.cc (-O, -RQ): Accept a threshold
argument.
parent 4ac6468b
......@@ -303,13 +303,19 @@ namespace spot
}
tgba_explicit_number*
tba_determinize(const tgba* aut)
tba_determinize(const tgba* aut, unsigned threshold)
{
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))
{
delete det;
return 0;
}
fix_dba_acceptance(det, aut, pm);
det->merge_transitions();
return det;
......@@ -317,6 +323,7 @@ namespace spot
tgba*
tba_determinize_check(const tgba* aut,
unsigned threshold,
const ltl::formula* f,
const tgba* neg_aut)
{
......@@ -326,7 +333,10 @@ namespace spot
if (aut->number_of_acceptance_conditions() > 1)
return 0;
tgba_explicit_number* det = tba_determinize(aut);
tgba_explicit_number* det = tba_determinize(aut, threshold);
if (!det)
return 0;
if (neg_aut == 0)
{
......
......@@ -122,8 +122,12 @@ 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.
SPOT_API tgba_explicit_number*
tba_determinize(const tgba* aut);
tba_determinize(const tgba* aut, unsigned threshold = 0);
/// \brief Determinize a TBA and make sure it is correct.
///
......@@ -134,15 +138,22 @@ namespace spot
/// \a neg_aut is not given, it will be built from \a f.
///
/// \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 f the formula represented by the original automaton
///
/// \param neg_aut an automaton representing the negation of \a aut
///
/// \return a new tgba if the automaton could be determinized, \a aut if
/// the automaton cannot be determinized, 0 if we do not know if the
/// determinization is correct because neither \a f nor \a neg_aut
/// were supplied.
tgba*
SPOT_API tgba*
tba_determinize_check(const tgba* aut,
unsigned threshold = 0,
const ltl::formula* f = 0,
const tgba* neg_aut = 0);
......
......@@ -337,11 +337,13 @@ to_int(const char* s)
char* endptr;
int res = strtol(s, &endptr, 10);
if (*endptr)
return -1;
{
std::cerr << "Failed to parse `" << s << "' as an integer." << std::endl;
exit(1);
}
return res;
}
int
main(int argc, char** argv)
{
......@@ -389,6 +391,8 @@ main(int argc, char** argv)
bool opt_reduce = false;
bool opt_minimize = false;
bool opt_determinize = false;
unsigned opt_determinize_threshold = 0;
unsigned opt_o_threshold = 0;
bool opt_dbacomp = false;
bool reject_bigger = false;
bool opt_bisim_ta = false;
......@@ -649,10 +653,12 @@ main(int argc, char** argv)
output = 8;
spin_comments = true;
}
else if (!strcmp(argv[formula_index], "-O"))
else if (!strncmp(argv[formula_index], "-O", 2))
{
output = 14;
opt_minimize = true;
if (argv[formula_index][2] != 0)
opt_o_threshold = to_int(argv[formula_index] + 2);
}
else if (!strcmp(argv[formula_index], "-p"))
{
......@@ -793,9 +799,11 @@ main(int argc, char** argv)
opt_minimize = true;
reject_bigger = true;
}
else if (!strcmp(argv[formula_index], "-RQ"))
else if (!strncmp(argv[formula_index], "-RQ", 3))
{
opt_determinize = true;
if (argv[formula_index][3] != 0)
opt_determinize_threshold = to_int(argv[formula_index] + 3);
}
else if (!strcmp(argv[formula_index], "-RT"))
{
......@@ -1443,8 +1451,10 @@ main(int argc, char** argv)
&& (!f || f->is_syntactic_recurrence()))
{
tm.start("determinization");
a = determinized = tba_determinize(a);
determinized = tba_determinize(a, opt_determinize_threshold);
tm.stop("determinization");
if (determinized)
a = determinized;
}
spot::tgba* complemented = 0;
......@@ -1702,7 +1712,8 @@ main(int argc, char** argv)
if (minimized == 0)
{
std::cout << "this is not an obligation property";
const spot::tgba* tmp = tba_determinize_check(a, f);
const spot::tgba* tmp =
tba_determinize_check(a, opt_o_threshold, f, 0);
if (tmp != 0 && tmp != a)
{
std::cout << ", but it is a recurrence property";
......
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