From 38148f87f8581fa062dc85b591df548d1db7e666 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 17 Nov 2009 16:48:42 +0100 Subject: [PATCH] * src/tgbaalgos/cutscc.cc (cut_scc): Pass `s' by reference instead of by pointer. * src/tgbaalgos/cutscc.cc, src/tgbaalgos/cutscc.hh: Fix copyright header. --- ChangeLog | 7 +++++++ src/tgbaalgos/cutscc.cc | 26 ++++++++------------------ src/tgbaalgos/cutscc.hh | 5 ++--- 3 files changed, 17 insertions(+), 21 deletions(-) diff --git a/ChangeLog b/ChangeLog index c1128d07a..99526b42a 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,10 @@ +2009-11-17 Alexandre Duret-Lutz + + * src/tgbaalgos/cutscc.cc (cut_scc): Pass `s' by reference instead + of by pointer. + * src/tgbaalgos/cutscc.cc, src/tgbaalgos/cutscc.hh: Fix copyright + header. + 2009-11-13 Alexandre Duret-Lutz Replace the hash key construction of LTL formulae by a simple diff --git a/src/tgbaalgos/cutscc.cc b/src/tgbaalgos/cutscc.cc index 101f5246f..b029f858d 100644 --- a/src/tgbaalgos/cutscc.cc +++ b/src/tgbaalgos/cutscc.cc @@ -1,6 +1,5 @@ -// Copyright (C) 2003, 2004, 2005, 2006, 2007, 2008, 2009 Laboratoire -// d'Informatique de Paris 6 (LIP6), département Systèmes Répartis -// Coopératifs (SRC), Université Pierre et Marie Curie. +// Copyright (C) 2009 Laboratoire de Recherche et Developpement de +// l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -20,24 +19,15 @@ // 02111-1307, USA. #include -#include -#include -#include -#include #include #include -#include -#include -#include -#include -#include "tgbaalgos/scc.hh" #include "tgba/tgbaexplicit.hh" #include "cutscc.hh" namespace spot { tgba* cut_scc(const tgba* a, const scc_map& m, - const std::set* s) + const std::set& s) { tgba_explicit_string* sub_a = new tgba_explicit_string(a->get_dict()); state* cur = a->get_init_state(); @@ -50,15 +40,15 @@ namespace spot std::string cur_format = a->format_state(cur); std::set::iterator it; // Check if we have at least one accepting SCC. - for (it = s->begin(); it != s->end() && !m.accepting(*it); it++) + for (it = s.begin(); it != s.end() && !m.accepting(*it); it++) continue; - assert(it != s->end()); + assert(it != s.end()); tovisit.push(cur); seen.insert(cur); sub_a->add_state(cur_format); sub_a->copy_acceptance_conditions_of(a); // If the initial is not part of one of the desired SCC, exit - assert(s->find(m.scc_of_state(cur)) != s->end()); + assert(s.find(m.scc_of_state(cur)) != s.end()); // Perform BFS to visit each state. while (!tovisit.empty()) @@ -73,7 +63,7 @@ namespace spot std::string dst_format = a->format_state(dst); scc_number= m.scc_of_state(dst); // Is the successor included in one of the desired SCC ? - if (s->find(scc_number) != s->end()) + if (s.find(scc_number) != s.end()) { if (seen.find(dst) == seen.end()) { @@ -358,7 +348,7 @@ namespace spot if (is_valid[i] == true) { //print_set((*final_sets)[i]); - result.push_back(cut_scc(a, m, &(*final_sets)[i]->sccs)); + result.push_back(cut_scc(a, m, (*final_sets)[i]->sccs)); } // Free everything. diff --git a/src/tgbaalgos/cutscc.hh b/src/tgbaalgos/cutscc.hh index 88f0528b0..ba0d0a3ec 100644 --- a/src/tgbaalgos/cutscc.hh +++ b/src/tgbaalgos/cutscc.hh @@ -1,6 +1,5 @@ -// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), -// département Systèmes Répartis Coopératifs (SRC), Université Pierre -// et Marie Curie. +// Copyright (C) 2009 Laboratoire de Recherche et Developpement de +// l'Epita (LRDE). // // This file is part of Spot, a model checking library. //