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

Change tgba_dupexp_bfs() and tgba_dupexp_dfs() to build numbered tgba.

Browse source 
* src/tgbaalgos/dupexp.cc, src/tgbaalgos/dupexp.hh: Change the return
type.
This commit is contained in:
Alexandre Duret-Lutz 2012-04-20 14:21:13 +02:00
parent 0821599db8
commit a9cccd11e6
2 changed files with 20 additions and 22 deletions
Download patch file Download diff file Expand all files Collapse all files

29
src/tgbaalgos/dupexp.cc
View file

@ -1,7 +1,8 @@
// Copyright (C) 2009, 2011 Laboratoire de Recherche et Développement // -*- coding: utf-8 -*-
// de l'Epita (LRDE). // Copyright (C) 2009, 2011, 2012 Laboratoire de Recherche et
// Développement de l'Epita (LRDE).
// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), // Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre // département Systèmes Répartis Coopératifs (SRC), Université Pierre
// et Marie Curie. // et Marie Curie.
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
@ -36,40 +37,34 @@ namespace spot
{ {
public: public:
dupexp_iter(const tgba* a) dupexp_iter(const tgba* a)
: T(a), out_(new tgba_explicit_string(a->get_dict())) : T(a), out_(new tgba_explicit_number(a->get_dict()))
{ {
out_->copy_acceptance_conditions_of(a); out_->copy_acceptance_conditions_of(a);
} }
tgba_explicit_string* tgba_explicit_number*
result() result()
{ {
return out_; return out_;
} }
void void
process_link(const state* in_s, int in, process_link(const state*, int in,
const state* out_s, int out, const state*, int out,
const tgba_succ_iterator* si) const tgba_succ_iterator* si)
{ {
std::ostringstream in_name; state_explicit_number::transition* t = out_->create_transition(in, out);
in_name << "(#" << in << ") " << this->aut_->format_state(in_s);
std::ostringstream out_name;
out_name << "(#" << out << ") " << this->aut_->format_state(out_s);
state_explicit_string::transition* t =
out_->create_transition(in_name.str(), out_name.str());
out_->add_conditions(t, si->current_condition()); out_->add_conditions(t, si->current_condition());
out_->add_acceptance_conditions(t, si->current_acceptance_conditions()); out_->add_acceptance_conditions(t, si->current_acceptance_conditions());
} }
private: private:
tgba_explicit_string* out_; tgba_explicit_number* out_;
}; };
} // anonymous } // anonymous
tgba_explicit_string* tgba_explicit_number*
tgba_dupexp_bfs(const tgba* aut) tgba_dupexp_bfs(const tgba* aut)
{ {
dupexp_iter<tgba_reachable_iterator_breadth_first> di(aut); dupexp_iter<tgba_reachable_iterator_breadth_first> di(aut);
@ -77,7 +72,7 @@ namespace spot
return di.result(); return di.result();
} }
tgba_explicit_string* tgba_explicit_number*
tgba_dupexp_dfs(const tgba* aut) tgba_dupexp_dfs(const tgba* aut)
{ {
dupexp_iter<tgba_reachable_iterator_depth_first> di(aut); dupexp_iter<tgba_reachable_iterator_depth_first> di(aut);

13
src/tgbaalgos/dupexp.hh
View file

@ -1,6 +1,9 @@
// Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), // -*- coding: utf-8 -*-
// département Systèmes Répartis Coopératifs (SRC), Université Pierre // Copyright (C) 2012 Laboratoire de Recherche et Développement de
// et Marie Curie. // l'Epita (LRDE).
// Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de Paris
// 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
// Université Pierre et Marie Curie.
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
// //
@ -29,11 +32,11 @@ namespace spot
/// \brief Build an explicit automata from all states of \a aut, /// \brief Build an explicit automata from all states of \a aut,
/// numbering states in bread first order as they are processed. /// numbering states in bread first order as they are processed.
/// \ingroup tgba_misc /// \ingroup tgba_misc
tgba_explicit_string* tgba_dupexp_bfs(const tgba* aut); tgba_explicit_number* tgba_dupexp_bfs(const tgba* aut);
/// \brief Build an explicit automata from all states of \a aut, /// \brief Build an explicit automata from all states of \a aut,
/// numbering states in depth first order as they are processed. /// numbering states in depth first order as they are processed.
/// \ingroup tgba_misc /// \ingroup tgba_misc
tgba_explicit_string* tgba_dupexp_dfs(const tgba* aut); tgba_explicit_number* tgba_dupexp_dfs(const tgba* aut);
} }
#endif // SPOT_TGBAALGOS_DUPEXP_HH #endif // SPOT_TGBAALGOS_DUPEXP_HH