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

Use more sba_explicit more often.

* src/tgbaalgos/minimize.cc, src/tgbaalgos/minimize.hh
(minimize_dfa, minimize_wdba): Return a sba_explicit_number automaton
instead of tgba_explicit_number.
* src/tgba/tgbaexplicit.hh (declare_acceptance_condition): Fix code
so it works on sba as well.
* src/tgbaalgos/dotty.cc, src/tgbaalgos/neverclaim.cc: Specialize
for sba instead of tgba_sba_proxy.
* src/tgbaalgos/neverclaim.hh: Point to degeneralize().
parent 807834ec
......@@ -598,7 +598,7 @@ namespace spot
neg_acceptance_conditions_ &= neg;
// Append neg to all acceptance conditions.
typename explicit_graph<State, tgba>::ls_map::iterator i;
typename ls_map::iterator i;
for (i = this->ls_.begin(); i != this->ls_.end(); ++i)
{
typename transitions_t::iterator i2;
......
......@@ -23,6 +23,7 @@
#include <ostream>
#include "tgba/tgba.hh"
#include "tgba/sba.hh"
#include "dotty.hh"
#include "dottydec.hh"
#include "tgba/bddprint.hh"
......@@ -42,7 +43,7 @@ namespace spot
dotty_decorator* dd)
: tgba_reachable_iterator_breadth_first(a), os_(os),
mark_accepting_states_(mark_accepting_states), dd_(dd),
sba_(dynamic_cast<const tgba_sba_proxy*>(a))
sba_(dynamic_cast<const sba*>(a))
{
}
......@@ -120,7 +121,7 @@ namespace spot
std::ostream& os_;
bool mark_accepting_states_;
dotty_decorator* dd_;
const tgba_sba_proxy* sba_;
const sba* sba_;
};
}
......
......@@ -114,7 +114,7 @@ namespace spot
// From the base automaton and the list of sets, build the minimal
// resulting automaton
tgba_explicit_number* build_result(const tgba* a,
sba_explicit_number* build_result(const tgba* a,
std::list<hash_set*>& sets,
hash_set* final)
{
......@@ -133,7 +133,7 @@ namespace spot
++num;
}
typedef state_explicit_number::transition trs;
tgba_explicit_number* res = new tgba_explicit_number(a->get_dict());
sba_explicit_number* res = new sba_explicit_number(a->get_dict());
// For each transition in the initial automaton, add the corresponding
// transition in res.
if (!final->empty())
......@@ -294,8 +294,8 @@ namespace spot
}
tgba_explicit_number* minimize_dfa(const tgba_explicit_number* det_a,
hash_set* final, hash_set* non_final)
sba_explicit_number* minimize_dfa(const tgba_explicit_number* det_a,
hash_set* final, hash_set* non_final)
{
typedef std::list<hash_set*> partition_t;
partition_t cur_run;
......@@ -484,7 +484,7 @@ namespace spot
#endif
// Build the result.
tgba_explicit_number* res = build_result(det_a, done, final_copy);
sba_explicit_number* res = build_result(det_a, done, final_copy);
// Free all the allocated memory.
delete final_copy;
......@@ -503,7 +503,7 @@ namespace spot
}
tgba_explicit_number* minimize_monitor(const tgba* a)
sba_explicit_number* minimize_monitor(const tgba* a)
{
hash_set* final = new hash_set;
hash_set* non_final = new hash_set;
......@@ -521,7 +521,7 @@ namespace spot
return minimize_dfa(det_a, final, non_final);
}
tgba_explicit_number* minimize_wdba(const tgba* a)
sba_explicit_number* minimize_wdba(const tgba* a)
{
hash_set* final = new hash_set;
hash_set* non_final = new hash_set;
......@@ -596,7 +596,7 @@ namespace spot
if (wdba_scc_is_accepting(det_a, m, a, sm, pm))
{
is_useless = false;
d[m] = (l | 1) - 1; // largest even number inferior or equal
d[m] = l & ~1; // largest even number inferior or equal
}
else
{
......@@ -608,7 +608,7 @@ namespace spot
if (!is_useless)
{
hash_set* dest_set = (d[m]&1) ? non_final : final;
hash_set* dest_set = (d[m] & 1) ? non_final : final;
const std::list<const state*>& l = sm.states_of(m);
std::list<const state*>::const_iterator il;
for (il = l.begin(); il != l.end(); ++il)
......@@ -625,7 +625,7 @@ namespace spot
const ltl::formula* f, const tgba* aut_neg_f,
bool reject_bigger)
{
tgba_explicit_number* min_aut_f = minimize_wdba(aut_f);
sba_explicit_number* min_aut_f = minimize_wdba(aut_f);
if (reject_bigger)
{
......
......@@ -59,7 +59,7 @@ namespace spot
/// \param a the automaton to convert into a minimal deterministic monitor
/// \pre Dead SCCs should have been removed from \a a before
/// calling this function.
tgba_explicit_number* minimize_monitor(const tgba* a);
sba_explicit_number* minimize_monitor(const tgba* a);
/// \brief Minimize a Büchi automaton in the WDBA class.
///
......@@ -95,7 +95,7 @@ namespace spot
/// month = oct
/// }
/// \endverbatim
tgba_explicit_number* minimize_wdba(const tgba* a);
sba_explicit_number* minimize_wdba(const tgba* a);
/// \brief Minimize an automaton if it represents an obligation property.
///
......
......@@ -24,7 +24,7 @@
#include <ostream>
#include <sstream>
#include "bdd.h"
#include "tgba/tgbatba.hh"
#include "tgba/sba.hh"
#include "neverclaim.hh"
#include "tgba/bddprint.hh"
#include "reachiter.hh"
......@@ -43,7 +43,7 @@ namespace spot
: tgba_reachable_iterator_breadth_first(a),
os_(os), f_(f), accept_all_(-1), fi_needed_(false),
comments_(comments), all_acc_conds_(a->all_acceptance_conditions()),
degen_(dynamic_cast<const tgba_sba_proxy*>(a))
sba_(dynamic_cast<const sba*>(a))
{
}
......@@ -75,10 +75,10 @@ namespace spot
bool
state_is_accepting(const state *s)
{
// If the automaton is degeneralized on-the-fly,
// it's easier to just query the state_is_accepting() method.
if (degen_)
return degen_->state_is_accepting(s);
// If the automaton is a SBA, it's easier to just query the
// state_is_accepting() method.
if (sba_)
return sba_->state_is_accepting(s);
// Otherwise, since we are dealing with a degeneralized
// automaton nonetheless, the transitions leaving an accepting
......@@ -197,7 +197,7 @@ namespace spot
state* init_;
bool comments_;
bdd all_acc_conds_;
const tgba_sba_proxy* degen_;
const sba* sba_;
};
} // anonymous
......
// Copyright (C) 2009, 2011 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
// Copyright (C) 2009, 2011, 2012 Laboratoire de Recherche et
// Développement de l'Epita (LRDE).
// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
// et Marie Curie.
......@@ -37,7 +37,8 @@ namespace spot
/// \param g The (state-based degeneralized) automaton to output.
/// There should be only one acceptance condition, and
/// all the transitions of a state should be either all accepting
/// or all unaccepting.
/// or all unaccepting. If your automaton does not satisfies
/// these requirements, call degeneralize() first.
/// \param f The (optional) formula associated to the automaton. If given
/// it will be output as a comment.
/// \param comments Whether to comment each state of the never clause
......
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