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

* src/tgbaalgos/emptinesscheck.hh

Browse source 
(emptiness_check::remove_component, emptiness_check::root_component,
emptiness_check::seen_state_num, emptiness_check::suffix): Move in
private part.
(emptiness_check::arc_accepting, emptiness_check::todo): Move ...
* src/tgbaalgos/emptinesscheck.cc
(emptiness_check::tgba_emptiness_check): ... as local variables
of this function.
* src/tgbaalgos/emptinesscheck.hh (emptiness_check::vec_component):
Move ...
(emptiness_check::counter_example): ... as local variable of this
function.
* src/tgbaalgos/emptinesscheck.hh (pair_state_iter, triplet):
Move ...
* src/tgbaalgos/emptinesscheck.cc (pair_state_iter, triplet):
... here.
This commit is contained in:
Alexandre Duret-Lutz 2003-10-23 13:05:35 +00:00
parent fda83b9c51
commit 636f5238d3
3 changed files with 24 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

17
ChangeLog
View file

@ -1,5 +1,22 @@
2003-10-23 Alexandre Duret-Lutz <adl@src.lip6.fr>
* src/tgbaalgos/emptinesscheck.hh
(emptiness_check::remove_component, emptiness_check::root_component,
emptiness_check::seen_state_num, emptiness_check::suffix): Move in
private part.
(emptiness_check::arc_accepting, emptiness_check::todo): Move ...
* src/tgbaalgos/emptinesscheck.cc
(emptiness_check::tgba_emptiness_check): ... as local variables
of this function.
* src/tgbaalgos/emptinesscheck.hh (emptiness_check::vec_component):
Move ...
(emptiness_check::counter_example): ... as local variable of this
function.
* src/tgbaalgos/emptinesscheck.hh (pair_state_iter, triplet):
Move ...
* src/tgbaalgos/emptinesscheck.cc (pair_state_iter, triplet):
... here.
* src/tgbaalgos/emptinesscheck.cc (emptiness_check::print_result):
Indent output as in the magic search.

11
src/tgbaalgos/emptinesscheck.cc
View file

@ -20,6 +20,9 @@
namespace spot
{
typedef std::pair<const spot::state*, tgba_succ_iterator*> pair_state_iter;
typedef std::pair<pair_state_iter, bdd> triplet;
connected_component::connected_component()
{
index = 0;
@ -90,7 +93,8 @@ namespace spot
bool
emptiness_check::tgba_emptiness_check(const spot::tgba* aut_check)
{
std::stack<pair_state_iter> todo;
std::stack<bdd> arc_accepting;
int nbstate = 1;
state* init = aut_check->get_init_state();
seen_state_num[init] = 1;
@ -238,9 +242,8 @@ namespace spot
int comp_size = root_component.size();
typedef std::vector<connected_component> vec_compo;
vec_compo vec_component;
vec_component.resize(comp_size);
vec_sequence.resize(comp_size);
vec_compo vec_component(comp_size);
std::vector<state_sequence> vec_sequence(comp_size);
state_sequence seq;
state_sequence tmp_lst;
state_sequence best_lst;

3
src/tgbaalgos/emptinesscheck.hh
View file

@ -44,8 +44,6 @@ namespace spot
class emptiness_check
{
typedef std::pair<const spot::state*, tgba_succ_iterator*> pair_state_iter;
typedef std::pair<pair_state_iter, bdd> triplet;
typedef std::map<const spot::state*, int, spot::state_ptr_less_than> seen;
typedef std::list<const state*> state_sequence;
typedef std::pair<const spot::state*, bdd> state_proposition;
@ -82,7 +80,6 @@ namespace spot
const tgba* restrict = 0) const;
private:
std::stack<bdd> arc_accepting;
std::stack<connected_component> root_component;
seen seen_state_num;
state_sequence suffix;