From b9dd72b29bde6bba85daa2fb3eda7e790fe5110e Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 5 Jan 2011 23:12:33 +0100 Subject: [PATCH] * src/tgbatest/Makefile.am: Remove the unused minimize program. * src/tgbatest/minimize.cc: Delete. --- ChangeLog | 5 ++ src/tgbatest/Makefile.am | 4 +- src/tgbatest/minimize.cc | 141 --------------------------------------- 3 files changed, 6 insertions(+), 144 deletions(-) delete mode 100644 src/tgbatest/minimize.cc diff --git a/ChangeLog b/ChangeLog index c0515eee5..59efc0dff 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,8 @@ +2011-01-05 Alexandre Duret-Lutz + + * src/tgbatest/Makefile.am: Remove the unused minimize program. + * src/tgbatest/minimize.cc: Delete. + 2011-01-05 Alexandre Duret-Lutz Cleanup the minimize.hh interface. diff --git a/src/tgbatest/Makefile.am b/src/tgbatest/Makefile.am index 0d3c5cdf3..59fe4a5f0 100644 --- a/src/tgbatest/Makefile.am +++ b/src/tgbatest/Makefile.am @@ -1,4 +1,4 @@ -## Copyright (C) 2009, 2010 Laboratoire de Recherche et Développement +## Copyright (C) 2009, 2010, 2011 Laboratoire de Recherche et Développement ## de l'Epita (LRDE). ## Copyright (C) 2003, 2004, 2005, 2006 Laboratoire d'Informatique de ## Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), @@ -38,7 +38,6 @@ check_PROGRAMS = \ expldot \ explprod \ ltlprod \ - minimize \ mixprod \ powerset \ reductgba \ @@ -57,7 +56,6 @@ expldot_CXXFLAGS = -DDOTTY explprod_SOURCES = explprod.cc ltl2tgba_SOURCES = ltl2tgba.cc ltlprod_SOURCES = ltlprod.cc -minimize_SOURCES = minimize.cc mixprod_SOURCES = mixprod.cc powerset_SOURCES = powerset.cc randtgba_SOURCES = randtgba.cc diff --git a/src/tgbatest/minimize.cc b/src/tgbatest/minimize.cc deleted file mode 100644 index 4008fe1a1..000000000 --- a/src/tgbatest/minimize.cc +++ /dev/null @@ -1,141 +0,0 @@ -// Copyright (C) 2010 Laboratoire de Recherche et Développement -// de l'Epita (LRDE). -// -// This file is part of Spot, a model checking library. -// -// Spot is free software; you can redistribute it and/or modify it -// under the terms of the GNU General Public License as published by -// the Free Software Foundation; either version 2 of the License, or -// (at your option) any later version. -// -// Spot is distributed in the hope that it will be useful, but WITHOUT -// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY -// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public -// License for more details. -// -// You should have received a copy of the GNU General Public License -// along with Spot; see the file COPYING. If not, write to the Free -// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA -// 02111-1307, USA. - -#include -#include -#include "ltlast/unop.hh" -#include "tgbaalgos/dotty.hh" -#include "tgbaalgos/minimize.hh" -#include "tgbaalgos/powerset.hh" -#include "ltlparse/public.hh" -#include "tgba/tgbaexplicit.hh" -#include "ltlparse/ltlfile.hh" -#include "tgbaalgos/ltl2tgba_fm.hh" - -namespace spot -{ - unsigned tgba_size(const tgba* a) - { - typedef Sgi::hash_set hash_type; - hash_type seen; - std::queue tovisit; - // Perform breadth-first search. - state* init = a->get_init_state(); - tovisit.push(init); - seen.insert(init); - unsigned count = 0; - // While there are still states to visit. - while (!tovisit.empty()) - { - ++count; - state* cur = tovisit.front(); - tovisit.pop(); - tgba_succ_iterator* sit = a->succ_iter(cur); - for (sit->first(); !sit->done(); sit->next()) - { - state* dst = sit->current_state(); - // Is it a new state ? - if (seen.find(dst) == seen.end()) - { - // Yes, register the successor for later processing. - tovisit.push(dst); - seen.insert(dst); - } - else - // No, free dst. - delete dst; - } - delete sit; - } - hash_type::iterator it2; - // Free visited states. - for (it2 = seen.begin(); it2 != seen.end(); it2++) - delete *it2; - return count; - } -} - -// Compare the sizes of the initial and the minimal automata. -void compare_automata(const spot::tgba* a, - const spot::tgba* min_a) -{ - unsigned init_size = spot::tgba_size(a); - unsigned min_size = spot::tgba_size(min_a); - unsigned diff_size = init_size - min_size; - std::cout << init_size << " " << min_size << " " << diff_size << std::endl; -} - -void usage(const char* prog) -{ - std::cout << "Usage: " << prog << " ltl_file" << std::endl - << " " << prog << " -f formula" << std::endl; -} - -int main(int argc, char* argv[]) -{ - if (argc == 1) - { - usage(argv[0]); - return 1; - } - spot::bdd_dict* dict = new spot::bdd_dict(); - // Use the formula in argv[2] - if (!strcmp(argv[1], "-f")) - { - if (argc != 3) - { - usage(argv[0]); - return 1; - } - std::ofstream out_dot ("auto.dot"); - spot::ltl::parse_error_list pel; - spot::ltl::formula* f = spot::ltl::parse(argv[2], pel); - spot::tgba_explicit* a = ltl_to_tgba_fm(f, dict, true); -// spot::tgba_explicit* det = spot::tgba_powerset(a); - spot::tgba_explicit* res = minimize(a); - compare_automata(a, res); - spot::dotty_reachable(out_dot, res); -// delete det; - delete a; - delete res; - f->destroy(); - } - else - { - // Read a serie of formulae in a file. - spot::ltl::ltl_file formulae(argv[1]); - spot::ltl::formula* f; - while ((f = formulae.next())) - { - spot::ltl::formula* f_neg = - spot::ltl::unop::instance(spot::ltl::unop::Not, - f->clone()); - spot::tgba_explicit* a = ltl_to_tgba_fm(f_neg, dict, true); - spot::tgba_explicit* res = minimize(a); - compare_automata(a, res); - delete a; - delete res; - f->destroy(); - f_neg->destroy(); - } - } - delete dict; -}