From 5c9a5403fe661c567ba42f2ea144c7361f669b22 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 20 Aug 2014 10:03:21 +0200 Subject: [PATCH] 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. --- src/bin/common_output.hh | 2 +- src/bin/dstar2tgba.cc | 10 +++------- src/bin/ltlcross.cc | 5 ++--- src/tgbaalgos/simulation.cc | 16 +++++++--------- src/tgbaalgos/stats.cc | 15 ++++++--------- src/tgbaalgos/stats.hh | 4 ++-- 6 files changed, 21 insertions(+), 31 deletions(-) diff --git a/src/bin/common_output.hh b/src/bin/common_output.hh index fa12140ac..ac2cd70fb 100644 --- a/src/bin/common_output.hh +++ b/src/bin/common_output.hh @@ -73,7 +73,7 @@ public: } std::ostream& - print(const spot::const_tgba_ptr& aut, + print(const spot::const_tgba_digraph_ptr& aut, const spot::ltl::formula* f = 0, double run_time = -1.) { diff --git a/src/bin/dstar2tgba.cc b/src/bin/dstar2tgba.cc index 1580771e5..5ae92bb79 100644 --- a/src/bin/dstar2tgba.cc +++ b/src/bin/dstar2tgba.cc @@ -40,7 +40,7 @@ #include "tgba/bddprint.hh" #include "misc/optionmap.hh" #include "dstarparse/public.hh" -#include "tgbaalgos/scc.hh" +#include "tgbaalgos/sccinfo.hh" const char argp_program_doc[] ="\ Convert Rabin and Streett automata into Büchi automata.\n\n\ @@ -225,7 +225,7 @@ namespace /// to be output. std::ostream& 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) { filename_ = filename; @@ -252,11 +252,7 @@ namespace daut_acc_ = daut->accpair_count; if (has('C')) - { - spot::scc_map m(daut->aut); - m.build_map(); - daut_scc_ = m.scc_count(); - } + daut_scc_ = spot::scc_info(daut->aut).scc_count(); return this->spot::stat_printer::print(aut, 0, run_time); } diff --git a/src/bin/ltlcross.cc b/src/bin/ltlcross.cc index 39e1b898a..0e187faed 100644 --- a/src/bin/ltlcross.cc +++ b/src/bin/ltlcross.cc @@ -48,6 +48,7 @@ #include "tgba/tgbaproduct.hh" #include "tgbaalgos/gtec/gtec.hh" #include "tgbaalgos/randomgraph.hh" +#include "tgbaalgos/sccinfo.hh" #include "tgbaalgos/scc.hh" #include "tgbaalgos/dotty.hh" #include "tgbaalgos/isweakscc.hh" @@ -983,9 +984,7 @@ namespace st->in_transitions = s.sub_transitions; st->in_acc = aut->accpair_count; - spot::scc_map m(aut->aut); - m.build_map(); - st->in_scc = m.scc_count(); + st->in_scc = spot::scc_info(aut->aut).scc_count(); } // convert it into TGBA for further processing res = dstar_to_tgba(aut); diff --git a/src/tgbaalgos/simulation.cc b/src/tgbaalgos/simulation.cc index 8d1231160..6264a708c 100644 --- a/src/tgbaalgos/simulation.cc +++ b/src/tgbaalgos/simulation.cc @@ -28,7 +28,7 @@ #include "tgba/bddprint.hh" #include "tgbaalgos/reachiter.hh" #include "tgbaalgos/sccfilter.hh" -#include "tgbaalgos/scc.hh" +#include "tgbaalgos/sccinfo.hh" #include "tgbaalgos/dupexp.hh" // The way we developed this algorithm is the following: We take an @@ -224,14 +224,13 @@ namespace spot map_cst_(map_cst), 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 // the names (addresses) of the states in the automaton // returned by dupexp, and in automaton given in argument to // the constructor. a_ = tgba_dupexp_dfs(t, new_original_); - scc_map_ = new scc_map(a_); - scc_map_->build_map(); + scc_info_.reset(new scc_info(a_)); old_a_ = a_; @@ -323,7 +322,6 @@ namespace spot virtual ~direct_simulation() { a_->get_dict()->unregister_all_my_variables(this); - delete scc_map_; } // Update the name of the classes. @@ -770,7 +768,7 @@ namespace spot automaton_size stat; - scc_map* scc_map_; + std::unique_ptr scc_info_; std::vector new_original_; const map_constraint* map_cst_; @@ -822,15 +820,15 @@ namespace spot { bdd res = bddfalse; - unsigned scc = scc_map_->scc_of_state(old_a_->state_from_number(src)); - bool sccacc = scc_map_->accepting(scc); + unsigned scc = scc_info_->scc_of(src); + bool sccacc = scc_info_->is_accepting_scc(scc); for (auto& t: a_->out(src)) { bdd cl = previous_class_[t.dst]; 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_; else if (sccacc) acc = on_cycle_ & t.acc; diff --git a/src/tgbaalgos/stats.cc b/src/tgbaalgos/stats.cc index 507134158..3b6f5927b 100644 --- a/src/tgbaalgos/stats.cc +++ b/src/tgbaalgos/stats.cc @@ -1,5 +1,6 @@ -// Copyright (C) 2008, 2011, 2012, 2013 Laboratoire de Recherche et Développement -// de l'Epita (LRDE). +// -*- coding utf-8 -*- +// 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), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. @@ -25,7 +26,7 @@ #include "reachiter.hh" #include "ltlvisit/tostring.hh" #include "tgbaalgos/isdet.hh" -#include "tgbaalgos/scc.hh" +#include "tgbaalgos/sccinfo.hh" namespace spot { @@ -157,7 +158,7 @@ namespace spot } std::ostream& - stat_printer::print(const const_tgba_ptr& aut, + stat_printer::print(const const_tgba_digraph_ptr& aut, const ltl::formula* f, double run_time) { @@ -182,11 +183,7 @@ namespace spot acc_ = aut->number_of_acceptance_conditions(); if (has('c') || has('S')) - { - scc_map m(aut); - m.build_map(); - scc_ = m.scc_count(); - } + scc_ = scc_info(aut).scc_count(); if (has('n')) { diff --git a/src/tgbaalgos/stats.hh b/src/tgbaalgos/stats.hh index 5abbe3169..574db0400 100644 --- a/src/tgbaalgos/stats.hh +++ b/src/tgbaalgos/stats.hh @@ -1,5 +1,5 @@ // -*- 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). // Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), // 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 /// to be output, and so is \a run_time). 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.); private: