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

@@ -1,3 +1,16 @@
+2010-01-30  Alexandre Duret-Lutz  <adl@lrde.epita.fr>
+
+	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  <adl@lrde.epita.fr>
 
 	Check for missing Copyright blurbs, and add them.

bench/scc-stats/stats.cc

@@ -1,6 +1,5 @@
-// Copyright (C) 2003, 2004, 2005, 2006, 2007, 2008, 2009 Laboratoire
+// Copyright (C) 2009, 2010 Laboratoire de Recherche et Développement
-// d'Informatique de Paris 6 (LIP6), département Systèmes Répartis
+// de l'Epita (LRDE).
-// Coopératifs (SRC), Université Pierre et Marie Curie.
 //
 // This file is part of Spot, a model checking library.
 //
@@ -23,7 +22,8 @@
 #include <math.h>
 #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<double> dead_paths;
   std::vector<double> spanning_paths;
   std::vector<double> 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.

bench/split-product/cutscc.cc

@@ -1,6 +1,5 @@
-// Copyright (C) 2003, 2004, 2005, 2006, 2007, 2008, 2009 Laboratoire
+// Copyright (C) 2009, 2010 Laboratoire de Recherche et Développement
-// d'Informatique de Paris 6 (LIP6), département Systèmes Répartis
+// de l'Epita (LRDE).
-// Coopératifs (SRC), Université Pierre et Marie Curie.
 //
 // This file is part of Spot, a model checking library.
 //
@@ -23,7 +22,8 @@
 #include <limits>
 #include <sys/time.h>
 #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();
+  spot::ltl::ltl_file formulae(argv[1]);
-  do
+  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;

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

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;
+    }
+
+  }
+}

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 <fstream>
+#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

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 \

src/tgba/tgbafromfile.cc

@@ -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_;
-  }
-}

src/tgba/tgbafromfile.hh

@@ -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 <iosfwd>
-#include <fstream>
-#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