Commit 4ac6468b authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

Implement tba_determinize_check(), following Dax et al. (ATVA'07).

* src/tgbaalgos/powerset.cc, src/tgbaalgos/powerset.hh
(tba_determinize_check): New function.
* src/tgbatest/ltl2tgba.cc (-O): Use it.
parent bd2e78c1
......@@ -33,6 +33,11 @@
#include "tgba/tgbaproduct.hh"
#include "tgba/bddprint.hh"
#include "tgbaalgos/dotty.hh"
#include "tgbaalgos/gtec/gtec.hh"
#include "tgbaalgos/sccfilter.hh"
#include "tgbaalgos/ltl2tgba_fm.hh"
#include "tgbaalgos/dbacomp.hh"
#include "ltlast/unop.hh"
namespace spot
{
......@@ -309,4 +314,73 @@ namespace spot
det->merge_transitions();
return det;
}
tgba*
tba_determinize_check(const tgba* aut,
const ltl::formula* f,
const tgba* neg_aut)
{
const tgba* built = 0;
if (f == 0 && neg_aut == 0)
return 0;
if (aut->number_of_acceptance_conditions() > 1)
return 0;
tgba_explicit_number* det = tba_determinize(aut);
if (neg_aut == 0)
{
const ltl::formula* neg_f =
ltl::unop::instance(ltl::unop::Not, f->clone());
neg_aut = ltl_to_tgba_fm(neg_f, aut->get_dict());
neg_f->destroy();
// Remove useless SCCs.
const tgba* tmp = scc_filter(neg_aut, true);
delete neg_aut;
built = neg_aut = tmp;
}
bool ok = false;
tgba* p = new tgba_product(det, neg_aut);
emptiness_check* ec = couvreur99(p);
emptiness_check_result* res = ec->check();
if (!res)
{
delete ec;
delete p;
// Complement the DBA.
tgba* neg_det = dba_complement(det);
tgba* p = new tgba_product(aut, neg_det);
emptiness_check* ec = couvreur99(p);
res = ec->check();
if (!res)
{
// Finally, we are now sure that it was safe
// to determinize the automaton.
ok = true;
}
delete res;
delete ec;
delete p;
delete neg_det;
}
else
{
delete res;
delete ec;
delete p;
}
delete built;
if (ok)
return det;
delete det;
return const_cast<tgba*>(aut);
}
}
......@@ -124,6 +124,28 @@ namespace spot
/// only adapted to work on TBA rather than BA.
SPOT_API tgba_explicit_number*
tba_determinize(const tgba* aut);
/// \brief Determinize a TBA and make sure it is correct.
///
/// Apply tba_determinize(), then check that the result is
/// equivalent. If it isn't, return the original automaton.
///
/// Only one of \a f or \a neg_aut needs to be supplied. If
/// \a neg_aut is not given, it will be built from \a f.
///
/// \param aut the automaton to minimize
/// \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*
tba_determinize_check(const tgba* aut,
const ltl::formula* f = 0,
const tgba* neg_aut = 0);
}
#endif // SPOT_TGBAALGOS_POWERSET_HH
......@@ -1440,7 +1440,7 @@ main(int argc, char** argv)
spot::tgba* determinized = 0;
if (opt_determinize && a->number_of_acceptance_conditions() <= 1
&& f->is_syntactic_recurrence())
&& (!f || f->is_syntactic_recurrence()))
{
tm.start("determinization");
a = determinized = tba_determinize(a);
......@@ -1702,6 +1702,12 @@ 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);
if (tmp != 0 && tmp != a)
{
std::cout << ", but it is a recurrence property";
delete tmp;
}
}
else
{
......
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