From 4ff875f40267e0463bd59a940c2efe7443848447 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sat, 30 Jan 2010 17:31:34 +0100 Subject: [PATCH] Replace spot::ltl_file by a rewritten spot::ltl::ltl_file. * src/tgba/tgbafromfile.cc, src/tgba/tgbafromfile.hh: Delete these files. * src/tgba/Makefile.am: Remove them. * src/ltl/ltlparse/ltlfile.hh, src/ltl/ltlparse/ltlfile.cc: New files. * src/ltl/ltlparse/Makefile.am: Add them. * bench/scc-stats/stats.cc, bench/split-product/cutscc.cc: Rewrite using the new class. --- ChangeLog | 13 +++++ bench/scc-stats/stats.cc | 29 ++++++----- bench/split-product/cutscc.cc | 27 +++++----- src/ltlparse/Makefile.am | 6 ++- src/ltlparse/ltlfile.cc | 71 ++++++++++++++++++++++++++ src/ltlparse/ltlfile.hh | 48 ++++++++++++++++++ src/tgba/Makefile.am | 2 - src/tgba/tgbafromfile.cc | 93 ----------------------------------- src/tgba/tgbafromfile.hh | 61 ----------------------- 9 files changed, 167 insertions(+), 183 deletions(-) create mode 100644 src/ltlparse/ltlfile.cc create mode 100644 src/ltlparse/ltlfile.hh delete mode 100644 src/tgba/tgbafromfile.cc delete mode 100644 src/tgba/tgbafromfile.hh diff --git a/ChangeLog b/ChangeLog index 7fd048901..4e483cb70 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,16 @@ +2010-01-30 Alexandre Duret-Lutz + + Replace spot::ltl_file by a rewritten spot::ltl::ltl_file. + + * src/tgba/tgbafromfile.cc, src/tgba/tgbafromfile.hh: Delete these + files. + * src/tgba/Makefile.am: Remove them. + * src/ltl/ltlparse/ltlfile.hh, src/ltl/ltlparse/ltlfile.cc: New + files. + * src/ltl/ltlparse/Makefile.am: Add them. + * bench/scc-stats/stats.cc, bench/split-product/cutscc.cc: Rewrite + using the new class. + 2010-01-30 Alexandre Duret-Lutz Check for missing Copyright blurbs, and add them. diff --git a/bench/scc-stats/stats.cc b/bench/scc-stats/stats.cc index 024ce7680..ecc31495c 100644 --- a/bench/scc-stats/stats.cc +++ b/bench/scc-stats/stats.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, 2010 Laboratoire de Recherche et Développement +// de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -23,7 +22,8 @@ #include #include "tgbaalgos/scc.hh" #include "tgbaalgos/cutscc.hh" -#include "tgba/tgbafromfile.hh" +#include "ltlparse/ltlfile.hh" +#include "tgbaalgos/ltl2tgba_fm.hh" namespace spot { @@ -121,14 +121,15 @@ int main (int argc, char* argv[]) std::vector dead_paths; std::vector spanning_paths; std::vector self_loops; - // Get each LTL formula. - spot::ltl_file* formulae = new spot::ltl_file (argv[1], dict); - formulae->begin(); unsigned k = 0; - do + // Get each LTL formula. + spot::ltl::ltl_file formulae(argv[1]); + spot::ltl::formula* f; + while((f = formulae.next())) { ++k; - spot::tgba* a = formulae->current_automaton(); + spot::tgba* a = ltl_to_tgba_fm(f, dict, /* exprop */ true); + f->destroy(); // Get number of spanning paths. spot::scc_map m (a); m.build_map(); @@ -156,9 +157,13 @@ int main (int argc, char* argv[]) for (j = 0; j < (*paths)[i].size(); ++j) delete (*paths)[i][j]; delete paths; - formulae->next(); - } while (!formulae->done()); - delete formulae; + } + + if (count == 0) + { + std::cerr << "Nothing read." << std::endl; + exit(1); + } // We could have inserted at the right place instead of // sorting at the end. diff --git a/bench/split-product/cutscc.cc b/bench/split-product/cutscc.cc index e8a04a658..289f35c20 100644 --- a/bench/split-product/cutscc.cc +++ b/bench/split-product/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, 2010 Laboratoire de Recherche et Développement +// de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -23,7 +22,8 @@ #include #include #include "tgbaalgos/scc.hh" -#include "tgba/tgbafromfile.hh" +#include "ltlparse/ltlfile.hh" +#include "ltlvisit/tostring.hh" #include "tgbaalgos/dotty.hh" #include "tgbaalgos/randomgraph.hh" #include "tgbaalgos/emptiness.hh" @@ -33,6 +33,7 @@ #include "ltlvisit/apcollect.hh" #include "tgbaparse/public.hh" #include "tgbaalgos/cutscc.hh" +#include "tgbaalgos/ltl2tgba_fm.hh" namespace spot { @@ -162,18 +163,19 @@ int main(int argc, char* argv[]) unsigned iter_count = 1; std::cout << "Each operation is repeated " << iter_count << " times to improve precision." << std::endl << std::endl; - spot::ltl_file* formulae = new spot::ltl_file (argv[1], dict); - formulae->begin(); - do + + spot::ltl::ltl_file formulae(argv[1]); + spot::ltl::formula* f; + while((f = formulae.next())) { + spot::tgba* a = ltl_to_tgba_fm(f, dict, /* exprop */ true); ++i; - spot::tgba* a = formulae->current_automaton(); std::cout << "Formula " << i << std::endl; - std::cout << formulae->current_formula_string() << std::endl << std::endl; + std::cout << spot::ltl::to_string(f) << std::endl << std::endl; if (argc != 4) { spot::ltl::atomic_prop_set* s; - s = spot::ltl::atomic_prop_collect(formulae->current_formula(), 0); + s = spot::ltl::atomic_prop_collect(f, 0); spot::ltl::atomic_prop_set::iterator sit; delete r; r = spot::random_graph(10000, 0.0001, s, dict, 0, 0.15, 0.5); @@ -332,14 +334,13 @@ int main(int argc, char* argv[]) split_sum += (accepting_vector[i]) ? min:max; delete a; + f->destroy(); std::string next = "----------------------------------------"; std::cout << next << next << std::endl; std::cout << std::endl; - formulae->next(); - } while (!formulae->done()); + } delete r; delete dict; - delete formulae; std::cout << "Full " << full_sum << "s" << std::endl << "Cutting " << cut_sum << "s" << std::endl << "Split " << split_sum << "s" << std::endl; diff --git a/src/ltlparse/Makefile.am b/src/ltlparse/Makefile.am index bdbb7efb0..e815ba04e 100644 --- a/src/ltlparse/Makefile.am +++ b/src/ltlparse/Makefile.am @@ -1,4 +1,4 @@ -## Copyright (C) 2008, 2009 Laboratoire de Recherche et Développement +## Copyright (C) 2008, 2009, 2010 Laboratoire de Recherche et Développement ## de l'Epita (LRDE). ## Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris ## 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), @@ -56,10 +56,12 @@ EXTRA_DIST = $(LTLPARSE_YY) libltlparse_la_SOURCES = \ fmterror.cc \ $(FROM_LTLPARSE_YY) \ + ltlfile.cc \ ltlscan.ll \ parsedecl.hh ltlparse_HEADERS = \ - public.hh \ + ltlfile.hh \ location.hh \ + public.hh \ position.hh diff --git a/src/ltlparse/ltlfile.cc b/src/ltlparse/ltlfile.cc new file mode 100644 index 000000000..20b944b4a --- /dev/null +++ b/src/ltlparse/ltlfile.cc @@ -0,0 +1,71 @@ +// 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 "ltlfile.hh" +#include "public.hh" + +namespace spot +{ + namespace ltl + { + + ltl_file::ltl_file(const std::string& filename) + : in(filename.c_str()) + { + if (!in) + { + std::cerr << "Cannot open " << filename << std::endl; + exit(2); + } + } + + ltl_file::ltl_file(const char* filename) + : in(filename) + { + if (!in) + { + std::cerr << "Cannot open " << filename << std::endl; + exit(2); + } + } + + formula* ltl_file::next() + { + if (!in.good()) + return 0; + + std::string input; + do + { + if (!std::getline(in, input)) + return 0; + } + while (input == ""); + + spot::ltl::parse_error_list pel; + formula* f = parse(input, pel); + int ret = spot::ltl::format_parse_errors(std::cerr, input, pel); + if (ret) + exit(ret); + return f; + } + + } +} diff --git a/src/ltlparse/ltlfile.hh b/src/ltlparse/ltlfile.hh new file mode 100644 index 000000000..f143ef667 --- /dev/null +++ b/src/ltlparse/ltlfile.hh @@ -0,0 +1,48 @@ +// 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. + +#ifndef SPOT_LTLPARSE_LTLFILE_HH +# define SPOT_LTLPARSE_LTLFILE_HH +#include +#include "ltlast/formula.hh" + + +namespace spot +{ + namespace ltl + { + + /// \brief Read LTL formulae from a file, one by one + /// \ingroup ltl_io + class ltl_file + { + public: + ltl_file(const std::string& filename); + ltl_file(const char* filename); + /// Return the next parsed LTL formula, and 0 at end of file. + formula* next(); + private: + std::ifstream in; + }; + + } +} + +#endif diff --git a/src/tgba/Makefile.am b/src/tgba/Makefile.am index 8cbfe6d78..4b8b2d3a7 100644 --- a/src/tgba/Makefile.am +++ b/src/tgba/Makefile.am @@ -44,7 +44,6 @@ tgba_HEADERS = \ tgbabddcoredata.hh \ tgbabddfactory.hh \ tgbaexplicit.hh \ - tgbafromfile.hh \ tgbakvcomplement.hh \ tgbascc.hh \ tgbaproduct.hh \ @@ -69,7 +68,6 @@ libtgba_la_SOURCES = \ tgbabddconcreteproduct.cc \ tgbabddcoredata.cc \ tgbaexplicit.cc \ - tgbafromfile.cc \ tgbakvcomplement.cc \ tgbaproduct.cc \ tgbareduc.cc \ diff --git a/src/tgba/tgbafromfile.cc b/src/tgba/tgbafromfile.cc deleted file mode 100644 index 9907e6e6b..000000000 --- a/src/tgba/tgbafromfile.cc +++ /dev/null @@ -1,93 +0,0 @@ -// Copyright (C) 2009, 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 "tgba/public.hh" -#include "tgbafromfile.hh" - -namespace spot -{ - ltl_file::ltl_file(const char* filename, bdd_dict* dict) - { - input_file_.open(filename); - assert(input_file_.is_open()); - done_ = false; - env_ = &(ltl::default_environment::instance()); - dict_ = dict; - f_ = 0; - fm_exprop_opt_ = false; - fm_symb_merge_opt_ = true; - post_branching_ = false; - fair_loop_approx_ = false; - unobservables_ = 0; - fm_red_ = ltl::Reduce_None; - } - - ltl_file::~ltl_file() - { - input_file_.close(); - } - - bool ltl_file::done() - { - return(input_file_.eof()); - } - - void ltl_file::next() - { - if (f_) - { - f_->destroy(); - f_ = 0; - } - std::string line = ""; - while (line == "" && !input_file_.eof()) - getline(input_file_, line); - formula_ = line; - } - - void ltl_file::begin() - { - next(); - } - - tgba* ltl_file::current_automaton() - { - spot::tgba* a = 0; - f_ = spot::ltl::parse(formula_, pel_, *env_, false); - if (spot::ltl::format_parse_errors(std::cerr, formula_, pel_)) - return 0; - // Generate the automaton corresponding to the formula - a = spot::ltl_to_tgba_fm(f_, dict_, fm_exprop_opt_, - fm_symb_merge_opt_, post_branching_, - fair_loop_approx_, unobservables_, - fm_red_); - return a; - } - - ltl::formula* ltl_file::current_formula() - { - return f_; - } - - std::string ltl_file::current_formula_string() - { - return formula_; - } -} diff --git a/src/tgba/tgbafromfile.hh b/src/tgba/tgbafromfile.hh deleted file mode 100644 index 2d47703a4..000000000 --- a/src/tgba/tgbafromfile.hh +++ /dev/null @@ -1,61 +0,0 @@ -// Copyright (C) 2009, 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. - -#ifndef SPOT_TGBA_TGBAFROMFILE_HH -# define SPOT_TGBA_TGBAFROMFILE_HH -#include -#include -#include "tgba/public.hh" -#include "tgbaalgos/ltl2tgba_fm.hh" -#include "tgbaalgos/save.hh" -#include "ltlparse/public.hh" - -namespace spot -{ - class ltl_file - { - public: - ltl_file(const char* filename, bdd_dict* dict); - ~ltl_file(); - bool done(); - void next(); - void begin(); - tgba* current_automaton(); - std::string current_formula_string(); - ltl::formula* current_formula(); - private: - bool done_; - std::string formula_; - ltl::formula* f_; - std::ifstream input_file_; - ltl::parse_error_list pel_; - ltl::environment* env_; - bdd_dict* dict_; - bool fm_exprop_opt_; - bool fm_symb_merge_opt_; - bool post_branching_; - bool fair_loop_approx_; - ltl::atomic_prop_set* unobservables_; - int fm_red_; - }; -} - - -#endif // SPOT_TGBA_TGBAFROMFILE_HH