use scc_info instead of scc_map in a couple of easy places

* src/bin/dstar2tgba.cc, src/bin/ltlcross.cc, src/tgbaalgos/stats.cc,
src/tgbaalgos/simulation.cc: Use scc_info instead of scc_map.
* src/tgbaalgos/stats.hh, src/bin/common_output.hh: Change parameters
types to be tgba_digraph_ptr instead tgba_ptr, so that scc_info can be
used.
This commit is contained in:
Alexandre Duret-Lutz 2014-08-20 10:03:21 +02:00
parent 14570f62d0
commit 5c9a5403fe
6 changed files with 21 additions and 31 deletions

View file

@ -73,7 +73,7 @@ public:
} }
std::ostream& std::ostream&
print(const spot::const_tgba_ptr& aut, print(const spot::const_tgba_digraph_ptr& aut,
const spot::ltl::formula* f = 0, const spot::ltl::formula* f = 0,
double run_time = -1.) double run_time = -1.)
{ {

View file

@ -40,7 +40,7 @@
#include "tgba/bddprint.hh" #include "tgba/bddprint.hh"
#include "misc/optionmap.hh" #include "misc/optionmap.hh"
#include "dstarparse/public.hh" #include "dstarparse/public.hh"
#include "tgbaalgos/scc.hh" #include "tgbaalgos/sccinfo.hh"
const char argp_program_doc[] ="\ const char argp_program_doc[] ="\
Convert Rabin and Streett automata into Büchi automata.\n\n\ Convert Rabin and Streett automata into Büchi automata.\n\n\
@ -225,7 +225,7 @@ namespace
/// to be output. /// to be output.
std::ostream& std::ostream&
print(const spot::const_dstar_aut_ptr& daut, print(const spot::const_dstar_aut_ptr& daut,
const spot::const_tgba_ptr& aut, const spot::const_tgba_digraph_ptr& aut,
const char* filename, double run_time) const char* filename, double run_time)
{ {
filename_ = filename; filename_ = filename;
@ -252,11 +252,7 @@ namespace
daut_acc_ = daut->accpair_count; daut_acc_ = daut->accpair_count;
if (has('C')) if (has('C'))
{ daut_scc_ = spot::scc_info(daut->aut).scc_count();
spot::scc_map m(daut->aut);
m.build_map();
daut_scc_ = m.scc_count();
}
return this->spot::stat_printer::print(aut, 0, run_time); return this->spot::stat_printer::print(aut, 0, run_time);
} }

View file

@ -48,6 +48,7 @@
#include "tgba/tgbaproduct.hh" #include "tgba/tgbaproduct.hh"
#include "tgbaalgos/gtec/gtec.hh" #include "tgbaalgos/gtec/gtec.hh"
#include "tgbaalgos/randomgraph.hh" #include "tgbaalgos/randomgraph.hh"
#include "tgbaalgos/sccinfo.hh"
#include "tgbaalgos/scc.hh" #include "tgbaalgos/scc.hh"
#include "tgbaalgos/dotty.hh" #include "tgbaalgos/dotty.hh"
#include "tgbaalgos/isweakscc.hh" #include "tgbaalgos/isweakscc.hh"
@ -983,9 +984,7 @@ namespace
st->in_transitions = s.sub_transitions; st->in_transitions = s.sub_transitions;
st->in_acc = aut->accpair_count; st->in_acc = aut->accpair_count;
spot::scc_map m(aut->aut); st->in_scc = spot::scc_info(aut->aut).scc_count();
m.build_map();
st->in_scc = m.scc_count();
} }
// convert it into TGBA for further processing // convert it into TGBA for further processing
res = dstar_to_tgba(aut); res = dstar_to_tgba(aut);

View file

@ -28,7 +28,7 @@
#include "tgba/bddprint.hh" #include "tgba/bddprint.hh"
#include "tgbaalgos/reachiter.hh" #include "tgbaalgos/reachiter.hh"
#include "tgbaalgos/sccfilter.hh" #include "tgbaalgos/sccfilter.hh"
#include "tgbaalgos/scc.hh" #include "tgbaalgos/sccinfo.hh"
#include "tgbaalgos/dupexp.hh" #include "tgbaalgos/dupexp.hh"
// The way we developed this algorithm is the following: We take an // The way we developed this algorithm is the following: We take an
@ -224,14 +224,13 @@ namespace spot
map_cst_(map_cst), map_cst_(map_cst),
original_(t) original_(t)
{ {
// We need to do a dupexp for being able to run scc_map later. // We need to do a dupexp for being able to run scc_info later.
// new_original_ is the map that contains the relation between // new_original_ is the map that contains the relation between
// the names (addresses) of the states in the automaton // the names (addresses) of the states in the automaton
// returned by dupexp, and in automaton given in argument to // returned by dupexp, and in automaton given in argument to
// the constructor. // the constructor.
a_ = tgba_dupexp_dfs(t, new_original_); a_ = tgba_dupexp_dfs(t, new_original_);
scc_map_ = new scc_map(a_); scc_info_.reset(new scc_info(a_));
scc_map_->build_map();
old_a_ = a_; old_a_ = a_;
@ -323,7 +322,6 @@ namespace spot
virtual ~direct_simulation() virtual ~direct_simulation()
{ {
a_->get_dict()->unregister_all_my_variables(this); a_->get_dict()->unregister_all_my_variables(this);
delete scc_map_;
} }
// Update the name of the classes. // Update the name of the classes.
@ -770,7 +768,7 @@ namespace spot
automaton_size stat; automaton_size stat;
scc_map* scc_map_; std::unique_ptr<scc_info> scc_info_;
std::vector<const state*> new_original_; std::vector<const state*> new_original_;
const map_constraint* map_cst_; const map_constraint* map_cst_;
@ -822,15 +820,15 @@ namespace spot
{ {
bdd res = bddfalse; bdd res = bddfalse;
unsigned scc = scc_map_->scc_of_state(old_a_->state_from_number(src)); unsigned scc = scc_info_->scc_of(src);
bool sccacc = scc_map_->accepting(scc); bool sccacc = scc_info_->is_accepting_scc(scc);
for (auto& t: a_->out(src)) for (auto& t: a_->out(src))
{ {
bdd cl = previous_class_[t.dst]; bdd cl = previous_class_[t.dst];
bdd acc; bdd acc;
if (scc != scc_map_->scc_of_state(old_a_->state_from_number(t.dst))) if (scc != scc_info_->scc_of(t.dst))
acc = !on_cycle_; acc = !on_cycle_;
else if (sccacc) else if (sccacc)
acc = on_cycle_ & t.acc; acc = on_cycle_ & t.acc;

View file

@ -1,5 +1,6 @@
// Copyright (C) 2008, 2011, 2012, 2013 Laboratoire de Recherche et Développement // -*- coding utf-8 -*-
// de l'Epita (LRDE). // Copyright (C) 2008, 2011, 2012, 2013, 2014 Laboratoire de Recherche
// et Développement de l'Epita (LRDE).
// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), // Copyright (C) 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.
@ -25,7 +26,7 @@
#include "reachiter.hh" #include "reachiter.hh"
#include "ltlvisit/tostring.hh" #include "ltlvisit/tostring.hh"
#include "tgbaalgos/isdet.hh" #include "tgbaalgos/isdet.hh"
#include "tgbaalgos/scc.hh" #include "tgbaalgos/sccinfo.hh"
namespace spot namespace spot
{ {
@ -157,7 +158,7 @@ namespace spot
} }
std::ostream& std::ostream&
stat_printer::print(const const_tgba_ptr& aut, stat_printer::print(const const_tgba_digraph_ptr& aut,
const ltl::formula* f, const ltl::formula* f,
double run_time) double run_time)
{ {
@ -182,11 +183,7 @@ namespace spot
acc_ = aut->number_of_acceptance_conditions(); acc_ = aut->number_of_acceptance_conditions();
if (has('c') || has('S')) if (has('c') || has('S'))
{ scc_ = scc_info(aut).scc_count();
scc_map m(aut);
m.build_map();
scc_ = m.scc_count();
}
if (has('n')) if (has('n'))
{ {

View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*- // -*- coding: utf-8 -*-
// Copyright (C) 2008, 2011, 2012, 2013 Laboratoire de Recherche et // Copyright (C) 2008, 2011, 2012, 2013, 2014 Laboratoire de Recherche et
// Développement de l'Epita (LRDE). // Développement de l'Epita (LRDE).
// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), // Copyright (C) 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
@ -85,7 +85,7 @@ namespace spot
/// The \a f argument is not needed if the Formula does not need /// The \a f argument is not needed if the Formula does not need
/// to be output, and so is \a run_time). /// to be output, and so is \a run_time).
std::ostream& std::ostream&
print(const const_tgba_ptr& aut, const ltl::formula* f = 0, print(const const_tgba_digraph_ptr& aut, const ltl::formula* f = 0,
double run_time = -1.); double run_time = -1.);
private: private: