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

rename tgba_reachable_iterator as twa_reachable_iterator

Browse source 
* spot/twaalgos/reachiter.cc, spot/twaalgos/reachiter.hh: Here.
* spot/twaalgos/stats.cc, spot/twaalgos/lbtt.cc: Adjust.
* doc/org/upgrade2.org, NEWS: Mention the renaming.
This commit is contained in:
Alexandre Duret-Lutz 2016-03-06 11:40:42 +01:00
parent ad08a585af
commit 61b1f200b6
6 changed files with 67 additions and 62 deletions
Download patch file Download diff file Expand all files Collapse all files

2
NEWS
View file

@ -7,6 +7,8 @@ New in spot 1.99.8a (not yet released)
emptiness_check_instantiator::max_acceptance_conditions() renamed
to emptiness_check_instantiator::min_sets() and
emptiness_check_instantiator::max_sets().
* tgba_reachable_iterator (and subclasses) was renamed to
twa_reachable_iterator for consistency.
Documentation:

3
doc/org/upgrade2.org
View file

@ -658,6 +658,9 @@ for (auto i: aut->succ(s))
| ~tgba_explicit_number~ | ~twa_graph~ | new implementation |
| ~tgba_explicit_string~ | | deleted |
| ~tgba_parse()~ | ~parse_aut()~ | single parser for all automata |
| ~tgba_reachable_iterator~ | ~twa_reachable_iterator~ | |
| ~tgba_reachable_iterator_breadth_first~ | ~twa_reachable_iterator_breadth_first~ | |
| ~tgba_reachable_iterator_depth_first~ | ~twa_reachable_iterator_depth_first~ | |
| ~tgba_run_to_tgba()~ | ~twa_run::as_twa()~ | |
| ~tgba_run~ | ~twa_run~ | |
| ~tgba_save_reachable()~ | ~print_hoa()~ | adhoc output format replaced by HOA |

4
spot/twaalgos/lbtt.cc
View file

@ -34,11 +34,11 @@ namespace spot
{
namespace
{
class lbtt_bfs : public tgba_reachable_iterator_breadth_first
class lbtt_bfs final : public twa_reachable_iterator_breadth_first
{
public:
lbtt_bfs(const const_twa_ptr& a, std::ostream& os, bool sba_format)
: tgba_reachable_iterator_breadth_first(a),
: twa_reachable_iterator_breadth_first(a),
os_(os),
sba_format_(sba_format),
sba_(nullptr)

72
spot/twaalgos/reachiter.cc
View file

@ -25,15 +25,15 @@
namespace spot
{
// tgba_reachable_iterator
// twa_reachable_iterator
//////////////////////////////////////////////////////////////////////
tgba_reachable_iterator::tgba_reachable_iterator(const const_twa_ptr& a)
twa_reachable_iterator::twa_reachable_iterator(const const_twa_ptr& a)
: aut_(a)
{
}
tgba_reachable_iterator::~tgba_reachable_iterator()
twa_reachable_iterator::~twa_reachable_iterator()
{
auto s = seen.begin();
while (s != seen.end())
@ -46,7 +46,7 @@ namespace spot
}
void
tgba_reachable_iterator::run()
twa_reachable_iterator::run()
{
int n = 0;
start();
@ -90,51 +90,51 @@ namespace spot
}
bool
tgba_reachable_iterator::want_state(const state*) const
twa_reachable_iterator::want_state(const state*) const
{
return true;
}
void
tgba_reachable_iterator::start()
twa_reachable_iterator::start()
{
}
void
tgba_reachable_iterator::end()
twa_reachable_iterator::end()
{
}
void
tgba_reachable_iterator::process_state(const state*, int,
twa_reachable_iterator::process_state(const state*, int,
twa_succ_iterator*)
{
}
void
tgba_reachable_iterator::process_link(const state*, int,
twa_reachable_iterator::process_link(const state*, int,
const state*, int,
const twa_succ_iterator*)
{
}
// tgba_reachable_iterator_breadth_first
// twa_reachable_iterator_breadth_first
//////////////////////////////////////////////////////////////////////
tgba_reachable_iterator_breadth_first::
tgba_reachable_iterator_breadth_first(const const_twa_ptr& a)
: tgba_reachable_iterator(a)
twa_reachable_iterator_breadth_first::
twa_reachable_iterator_breadth_first(const const_twa_ptr& a)
: twa_reachable_iterator(a)
{
}
void
tgba_reachable_iterator_breadth_first::add_state(const state* s)
twa_reachable_iterator_breadth_first::add_state(const state* s)
{
todo.push_back(s);
}
const state*
tgba_reachable_iterator_breadth_first::next_state()
twa_reachable_iterator_breadth_first::next_state()
{
if (todo.empty())
return nullptr;
@ -143,16 +143,16 @@ namespace spot
return s;
}
// tgba_reachable_iterator_depth_first
// twa_reachable_iterator_depth_first
//////////////////////////////////////////////////////////////////////
tgba_reachable_iterator_depth_first::
tgba_reachable_iterator_depth_first(const const_twa_ptr& a)
twa_reachable_iterator_depth_first::
twa_reachable_iterator_depth_first(const const_twa_ptr& a)
: aut_(a)
{
}
tgba_reachable_iterator_depth_first::~tgba_reachable_iterator_depth_first()
twa_reachable_iterator_depth_first::~twa_reachable_iterator_depth_first()
{
auto s = seen.begin();
while (s != seen.end())
@ -165,7 +165,7 @@ namespace spot
}
void
tgba_reachable_iterator_depth_first::push(const state* s, int sn)
twa_reachable_iterator_depth_first::push(const state* s, int sn)
{
twa_succ_iterator* si = aut_->succ_iter(s);
process_state(s, sn, si);
@ -175,7 +175,7 @@ namespace spot
}
void
tgba_reachable_iterator_depth_first::pop()
twa_reachable_iterator_depth_first::pop()
{
aut_->release_iter(todo.back().it);
todo.pop_back();
@ -184,7 +184,7 @@ namespace spot
}
void
tgba_reachable_iterator_depth_first::run()
twa_reachable_iterator_depth_first::run()
{
int n = 1;
start();
@ -240,60 +240,60 @@ namespace spot
}
bool
tgba_reachable_iterator_depth_first::want_state(const state*) const
twa_reachable_iterator_depth_first::want_state(const state*) const
{
return true;
}
void
tgba_reachable_iterator_depth_first::start()
twa_reachable_iterator_depth_first::start()
{
}
void
tgba_reachable_iterator_depth_first::end()
twa_reachable_iterator_depth_first::end()
{
}
void
tgba_reachable_iterator_depth_first::process_state(const state*, int,
twa_reachable_iterator_depth_first::process_state(const state*, int,
twa_succ_iterator*)
{
}
void
tgba_reachable_iterator_depth_first::process_link(const state*, int,
twa_reachable_iterator_depth_first::process_link(const state*, int,
const state*, int,
const twa_succ_iterator*)
{
}
// tgba_reachable_iterator_depth_first_stack
// twa_reachable_iterator_depth_first_stack
//////////////////////////////////////////////////////////////////////
tgba_reachable_iterator_depth_first_stack::
tgba_reachable_iterator_depth_first_stack(const const_twa_ptr& a)
: tgba_reachable_iterator_depth_first(a)
twa_reachable_iterator_depth_first_stack::
twa_reachable_iterator_depth_first_stack(const const_twa_ptr& a)
: twa_reachable_iterator_depth_first(a)
{
}
void
tgba_reachable_iterator_depth_first_stack::push(const state* s, int sn)
twa_reachable_iterator_depth_first_stack::push(const state* s, int sn)
{
stack_.insert(sn);
this->tgba_reachable_iterator_depth_first::push(s, sn);
this->twa_reachable_iterator_depth_first::push(s, sn);
}
void
tgba_reachable_iterator_depth_first_stack::pop()
twa_reachable_iterator_depth_first_stack::pop()
{
stack_.erase(todo.back().src_n);
this->tgba_reachable_iterator_depth_first::pop();
this->twa_reachable_iterator_depth_first::pop();
}
bool
tgba_reachable_iterator_depth_first_stack::on_stack(int sn) const
twa_reachable_iterator_depth_first_stack::on_stack(int sn) const
{
return stack_.find(sn) != stack_.end();
}

32
spot/twaalgos/reachiter.hh
View file

@ -31,11 +31,11 @@ namespace spot
{
/// \ingroup twa_generic
/// \brief Iterate over all reachable states of a spot::tgba.
class SPOT_API tgba_reachable_iterator
class SPOT_API twa_reachable_iterator
{
public:
tgba_reachable_iterator(const const_twa_ptr& a);
virtual ~tgba_reachable_iterator();
twa_reachable_iterator(const const_twa_ptr& a);
virtual ~twa_reachable_iterator();
/// \brief Iterate over all reachable states of a spot::tgba.
///
@ -47,7 +47,7 @@ namespace spot
/// \name Todo list management.
///
/// See e.g.
/// spot::tgba_reachable_iterator_breadth_first for precanned
/// spot::twa_reachable_iterator_breadth_first for precanned
/// implementations for these functions.
/// \{
/// \brief Called by run() to register newly discovered states.
@ -81,7 +81,7 @@ namespace spot
/// transition.
///
/// The in_s and out_s states are owned by the
/// spot::tgba_reachable_iterator instance and destroyed when the
/// spot::twa_reachable_iterator instance and destroyed when the
/// instance is destroyed.
virtual void process_link(const state* in_s, int in,
const state* out_s, int out,
@ -94,13 +94,13 @@ namespace spot
};
/// \ingroup twa_generic
/// \brief An implementation of spot::tgba_reachable_iterator that browses
/// \brief An implementation of spot::twa_reachable_iterator that browses
/// states breadth first.
class SPOT_API tgba_reachable_iterator_breadth_first :
public tgba_reachable_iterator
class SPOT_API twa_reachable_iterator_breadth_first :
public twa_reachable_iterator
{
public:
tgba_reachable_iterator_breadth_first(const const_twa_ptr& a);
twa_reachable_iterator_breadth_first(const const_twa_ptr& a);
virtual void add_state(const state* s) override;
virtual const state* next_state() override;
@ -111,11 +111,11 @@ namespace spot
/// \ingroup twa_generic
/// \brief Iterate over all states of an automaton using a DFS.
class SPOT_API tgba_reachable_iterator_depth_first
class SPOT_API twa_reachable_iterator_depth_first
{
public:
tgba_reachable_iterator_depth_first(const const_twa_ptr& a);
virtual ~tgba_reachable_iterator_depth_first();
twa_reachable_iterator_depth_first(const const_twa_ptr& a);
virtual ~twa_reachable_iterator_depth_first();
/// \brief Iterate over all reachable states of a spot::tgba.
///
@ -149,7 +149,7 @@ namespace spot
/// transition.
///
/// The in_s and out_s states are owned by the
/// spot::tgba_reachable_iterator instance and destroyed when the
/// spot::twa_reachable_iterator instance and destroyed when the
/// instance is destroyed.
virtual void process_link(const state* in_s, int in,
const state* out_s, int out,
@ -178,11 +178,11 @@ namespace spot
///
/// This variant also maintains a set of states that are on the DFS
/// stack. It can be checked using the on_stack() method.
class tgba_reachable_iterator_depth_first_stack
: public tgba_reachable_iterator_depth_first
class twa_reachable_iterator_depth_first_stack
: public twa_reachable_iterator_depth_first
{
public:
tgba_reachable_iterator_depth_first_stack(const const_twa_ptr& a);
twa_reachable_iterator_depth_first_stack(const const_twa_ptr& a);
/// \brief Whether state sn is on the DFS stack.
///
/// Note the destination state of a transition is only pushed to

16
spot/twaalgos/stats.cc
View file

@ -1,6 +1,6 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2008, 2011, 2012, 2013, 2014, 2015 Laboratoire de
// Recherche et Développement de l'Epita (LRDE).
// Copyright (C) 2008, 2011, 2012, 2013, 2014, 2015, 2016 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.
@ -33,23 +33,23 @@ namespace spot
{
namespace
{
class stats_bfs: public tgba_reachable_iterator_breadth_first
class stats_bfs: public twa_reachable_iterator_breadth_first
{
public:
stats_bfs(const const_twa_ptr& a, twa_statistics& s)
: tgba_reachable_iterator_breadth_first(a), s_(s)
: twa_reachable_iterator_breadth_first(a), s_(s)
{
}
void
process_state(const state*, int, twa_succ_iterator*)
process_state(const state*, int, twa_succ_iterator*) override final
{
++s_.states;
}
void
process_link(const state*, int, const state*, int,
const twa_succ_iterator*)
const twa_succ_iterator*) override
{
++s_.edges;
}
@ -58,7 +58,7 @@ namespace spot
twa_statistics& s_;
};
class sub_stats_bfs: public stats_bfs
class sub_stats_bfs final: public stats_bfs
{
public:
sub_stats_bfs(const const_twa_ptr& a, twa_sub_statistics& s)
@ -68,7 +68,7 @@ namespace spot
void
process_link(const state*, int, const state*, int,
const twa_succ_iterator* it)
const twa_succ_iterator* it) override
{
++s_.edges;