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

Implementent tba_determinize(), based on Dax et al (ATVA'07).

* src/tgbaalgos/powerset.hh,
src/tgbaalgos/powerset.cc (tba_determinize): New function.
* src/tgbatest/ltl2tgba.cc (-RQ): New option, for testing.
parent 29bc087d
// Copyright (C) 2009, 2010, 2011 Laboratoire de Recherche et Dveloppement
// de l'Epita (LRDE).
// Copyright (C) 2009, 2010, 2011, 2013 Laboratoire de Recherche et
// Dveloppement de l'Epita (LRDE).
// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
// dpartement Systmes Rpartis Coopratifs (SRC), Universit Pierre
// et Marie Curie.
......@@ -21,15 +21,23 @@
#include <set>
#include <deque>
#include <iterator>
#include <vector>
#include "powerset.hh"
#include "misc/hash.hh"
#include "tgbaalgos/powerset.hh"
#include "bdd.h"
#include "tgbaalgos/scc.hh"
#include "tgbaalgos/cycles.hh"
#include "tgbaalgos/gtec/gtec.hh"
#include "tgba/tgbaproduct.hh"
#include "tgba/bddprint.hh"
#include "tgbaalgos/dotty.hh"
namespace spot
{
tgba_explicit_number*
tgba_powerset(const tgba* aut, power_map& pm)
tgba_powerset(const tgba* aut, power_map& pm, bool merge)
{
typedef power_map::power_state power_state;
typedef std::map<power_map::power_state, int> power_set;
......@@ -104,7 +112,8 @@ namespace spot
res->add_conditions(t, cond);
}
}
res->merge_transitions();
if (merge)
res->merge_transitions();
return res;
}
......@@ -114,4 +123,190 @@ namespace spot
power_map pm;
return tgba_powerset(aut, pm);
}
namespace
{
class fix_scc_acceptance: protected enumerate_cycles
{
public:
typedef dfs_stack::const_iterator cycle_iter;
typedef state_explicit_number::transition trans;
typedef std::set<trans*> trans_set;
typedef std::vector<trans_set> set_set;
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
public:
fix_scc_acceptance(const scc_map& sm, const tgba* ref, power_map& refmap)
: enumerate_cycles(sm), ref_(ref), refmap_(refmap)
{
}
void fix_scc(const int m)
{
reject_.clear();
accept_.clear();
run(m);
// std::cerr << "SCC #" << m << "\n";
// std::cerr << "REJECT: ";
// print_set(std::cerr, reject_) << "\n";
// std::cerr << "ALL: ";
// print_set(std::cerr, all_) << "\n";
// for (set_set::const_iterator j = accept_.begin();
// j != accept_.end(); ++j)
// {
// std::cerr << "ACCEPT: ";
// print_set(std::cerr, *j) << "\n";
// }
bdd acc = aut_->all_acceptance_conditions();
for (trans_set::iterator i = all_.begin(); i != all_.end(); ++i)
{
(*i)->acceptance_conditions = acc;
}
}
bool is_cycle_accepting(cycle_iter begin, trans_set& ts) const
{
tgba_explicit_number* a =
down_cast<tgba_explicit_number*>(const_cast<tgba*>(aut_));
// Build an automaton representing this loop.
tgba_explicit_number loop_a(aut_->get_dict());
int loop_size = std::distance(begin, dfs_.end());
int n;
cycle_iter i;
for (n = 1, i = begin; n <= loop_size; ++n, ++i)
{
trans* t = a->get_transition(i->succ);
loop_a.create_transition(n - 1, n % loop_size)->condition =
t->condition;
if (reject_.find(t) == reject_.end())
ts.insert(t);
}
assert(i == dfs_.end());
const state* loop_a_init = loop_a.get_init_state();
assert(loop_a.get_label(loop_a_init) == 0);
// Check if the loop is accepting in the original automaton.
bool accepting = false;
// Iterate on each original state corresponding to the
// start of the loop in the determinized automaton.
const power_map::power_state& ps =
refmap_.states_of(a->get_label(begin->ts->first));
for (power_map::power_state::const_iterator it = ps.begin();
it != ps.end() && !accepting; ++it)
{
// Construct a product between
// LOOP_A, and ORIG_A starting in *IT.
tgba* p = new tgba_product_init(&loop_a, ref_,
loop_a_init, *it);
//spot::dotty_reachable(std::cout, p);
couvreur99_check* ec = down_cast<couvreur99_check*>(couvreur99(p));
assert(ec);
emptiness_check_result* res = ec->check();
if (res)
accepting = true;
delete res;
delete ec;
delete p;
}
loop_a_init->destroy();
return accepting;
}
std::ostream&
print_set(std::ostream& o, const trans_set& s) const
{
o << "{ ";
for (trans_set::const_iterator i = s.begin(); i != s.end(); ++i)
o << *i << " ";
o << "}";
return o;
}
virtual bool
cycle_found(const state* start)
{
cycle_iter i = dfs_.begin();
while (i->ts->first != start)
++i;
trans_set ts;
bool is_acc = is_cycle_accepting(i, ts);
do
{
// std::cerr << aut_->format_state(i->ts->first) << " ";
++i;
}
while (i != dfs_.end());
// std::cerr << " acc=" << is_acc << " (";
// bdd_print_accset(std::cerr, aut_->get_dict(), s) << ") ";
// print_set(std::cerr, ts) << "\n";
if (is_acc)
{
accept_.push_back(ts);
all_.insert(ts.begin(), ts.end());
}
else
{
for (trans_set::const_iterator i = ts.begin(); i != ts.end(); ++i)
{
trans* t = *i;
reject_.insert(t);
for (set_set::iterator j = accept_.begin();
j != accept_.end(); ++j)
{
j->erase(t);
}
all_.erase(t);
}
}
return true;
}
};
static void
fix_dba_acceptance(tgba_explicit_number* det,
const tgba* ref, power_map& refmap)
{
det->copy_acceptance_conditions_of(ref);
scc_map sm(det);
sm.build_map();
unsigned scc_count = sm.scc_count();
fix_scc_acceptance fsa(sm, ref, refmap);
for (unsigned m = 0; m < scc_count; ++m)
fsa.fix_scc(m);
}
}
tgba_explicit_number*
tba_determinize(const tgba* aut)
{
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);
fix_dba_acceptance(det, aut, pm);
det->merge_transitions();
return det;
}
}
......@@ -86,12 +86,44 @@ namespace spot
///
/// If \a pm is supplied it will be filled with the set of original states
/// associated to each state of the deterministic automaton.
/// The \a merge argument can be set to false to prevent merging of
/// transitions.
//@{
SPOT_API tgba_explicit_number*
tgba_powerset(const tgba* aut, power_map& pm);
tgba_powerset(const tgba* aut, power_map& pm, bool merge = true);
SPOT_API tgba_explicit_number*
tgba_powerset(const tgba* aut);
//@}
/// \brief Determinize a TBA using the powerset construction.
///
/// The input automaton should have at most one acceptance
/// condition. Beware that not all Büchi automata can be
/// determinized, and this procedure does not ensure that the
/// produced automaton is equivalent to \a aut.
///
/// The construction is adapted from Section 3.2 of:
/// \verbatim
/// @InProceedings{ dax.07.atva,
/// author = {Christian Dax and Jochen Eisinger and Felix Klaedtke},
/// title = {Mechanizing the Powerset Construction for Restricted
/// Classes of {$\omega$}-Automata},
/// year = 2007,
/// series = {Lecture Notes in Computer Science},
/// publisher = {Springer-Verlag},
/// volume = 4762,
/// booktitle = {Proceedings of the 5th International Symposium on
/// Automated Technology for Verification and Analysis
/// (ATVA'07)},
/// editor = {Kedar S. Namjoshi and Tomohiro Yoneda and Teruo Higashino
/// and Yoshio Okamura},
/// month = oct
/// }
/// \endverbatim
/// only adapted to work on TBA rather than BA.
SPOT_API tgba_explicit_number*
tba_determinize(const tgba* aut);
}
#endif // SPOT_TGBAALGOS_POWERSET_HH
......@@ -69,6 +69,7 @@
#include "kripkeparse/public.hh"
#include "tgbaalgos/simulation.hh"
#include "tgbaalgos/compsusp.hh"
#include "tgbaalgos/powerset.hh"
#include "taalgos/tgba2ta.hh"
#include "taalgos/dotty.hh"
......@@ -234,6 +235,7 @@ syntax(char* prog)
<< std::endl
<< " -RM attempt to WDBA-minimize the automaton unless the "
<< "result is bigger" << std::endl
<< " -RQ determinize a TGBA (assuming it's legal!)" << std::endl
<< std::endl
<< "Automaton conversion:" << std::endl
......@@ -385,6 +387,7 @@ main(int argc, char** argv)
bool graph_run_tgba_opt = false;
bool opt_reduce = false;
bool opt_minimize = false;
bool opt_determinize = false;
bool reject_bigger = false;
bool opt_bisim_ta = false;
bool opt_monitor = false;
......@@ -784,6 +787,10 @@ main(int argc, char** argv)
opt_minimize = true;
reject_bigger = true;
}
else if (!strcmp(argv[formula_index], "-RQ"))
{
opt_determinize = true;
}
else if (!strcmp(argv[formula_index], "-RT"))
{
opt_bisim_ta = true;
......@@ -1425,6 +1432,15 @@ main(int argc, char** argv)
// pointless.
}
spot::tgba* determinized = 0;
if (opt_determinize && a->number_of_acceptance_conditions() <= 1
&& f->is_syntactic_recurrence())
{
tm.start("determinization");
a = determinized = tba_determinize(a);
tm.stop("determinization");
}
const spot::tgba* expl = 0;
switch (dupexp)
{
......@@ -1878,6 +1894,7 @@ main(int argc, char** argv)
delete expl;
delete monitor;
delete minimized;
delete determinized;
delete degeneralized;
delete aut_scc;
delete to_free;
......
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