tgbaparse, lbttparse: do not pass an environment for acceptance sets

* src/priv/accmap.hh, src/tgbaalgos/lbtt.cc, src/tgbaalgos/lbtt.hh,
src/tgbaparse/public.hh, src/tgbaparse/tgbaparse.yy,
src/tgbatest/ltl2tgba.cc, src/tgbatest/tgbaread.cc: Do not pass any
environment parameter to parse acceptance sets.  This is not used
anymore since we moved to int-labeled acceptance sets.

src/priv/accmap.hh

@@ -23,7 +23,6 @@
 #include <bddx.h>
 #include "misc/hash.hh"
 #include "ltlast/formula.hh"
-#include "ltlenv/defaultenv.hh"
 #include "tgba/tgbagraph.hh"
 
 namespace spot
@@ -33,18 +32,11 @@ namespace spot
   protected:
     bdd_dict_ptr dict_;
     tgba_digraph_ptr aut_;
-    ltl::environment& env_;
 
-    acc_mapper_common(const tgba_digraph_ptr& aut, ltl::environment& env)
-      : dict_(aut->get_dict()), aut_(aut), env_(env)
+    acc_mapper_common(const tgba_digraph_ptr& aut)
+      : dict_(aut->get_dict()), aut_(aut)
     {
     }
-
-  public:
-    const ltl::environment& get_env() const
-    {
-      return env_;
-    }
   };
 
   class acc_mapper_string: public acc_mapper_common
@@ -52,10 +44,8 @@ namespace spot
     std::unordered_map<std::string, unsigned> map_;
 
   public:
-    acc_mapper_string(const tgba_digraph_ptr& aut,
-		      ltl::environment& env
-		      = ltl::default_environment::instance())
-      : acc_mapper_common(aut, env)
+    acc_mapper_string(const tgba_digraph_ptr& aut)
+      : acc_mapper_common(aut)
     {
     }
 
@@ -84,11 +74,8 @@ namespace spot
   class acc_mapper_consecutive_int: public acc_mapper_common
   {
   public:
-    acc_mapper_consecutive_int(const tgba_digraph_ptr& aut,
-			       unsigned count,
-			       ltl::environment& env =
-			       ltl::default_environment::instance())
-      : acc_mapper_common(aut, env)
+    acc_mapper_consecutive_int(const tgba_digraph_ptr& aut, unsigned count)
+      : acc_mapper_common(aut)
     {
       std::vector<unsigned> vmap(count);
       aut->acc().add_sets(count);
@@ -111,11 +98,8 @@ namespace spot
     std::map<unsigned, acc_cond::mark_t> map_;
 
   public:
-    acc_mapper_int(const tgba_digraph_ptr& aut,
-		   unsigned count,
-		   ltl::environment& env =
-		   ltl::default_environment::instance())
-      : acc_mapper_consecutive_int(aut, count, env), used_(0)
+    acc_mapper_int(const tgba_digraph_ptr& aut, unsigned count)
+      : acc_mapper_consecutive_int(aut, count), used_(0)
     {
     }
 

src/tgbaalgos/lbtt.cc

@@ -135,11 +135,10 @@ namespace spot
     tgba_digraph_ptr
     lbtt_read_tgba(unsigned num_states, unsigned num_acc,
 		   std::istream& is, std::string& error,
-		   const bdd_dict_ptr& dict,
-		   ltl::environment& env, ltl::environment& envacc)
+		   const bdd_dict_ptr& dict, ltl::environment& env)
     {
       auto aut = make_tgba_digraph(dict);
-      acc_mapper_int acc_b(aut, num_acc, envacc);
+      acc_mapper_int acc_b(aut, num_acc);
       aut->new_states(num_states);
 
       for (unsigned n = 0; n < num_states; ++n)
@@ -200,11 +199,10 @@ namespace spot
     tgba_digraph_ptr
     lbtt_read_gba(unsigned num_states, unsigned num_acc,
 		  std::istream& is, std::string& error,
-		  const bdd_dict_ptr& dict,
-		  ltl::environment& env, ltl::environment& envacc)
+		  const bdd_dict_ptr& dict, ltl::environment& env)
     {
       auto aut = make_tgba_digraph(dict);
-      acc_mapper_int acc_b(aut, num_acc, envacc);
+      acc_mapper_int acc_b(aut, num_acc);
       aut->new_states(num_states);
       aut->prop_state_based_acc();
 
@@ -277,7 +275,7 @@ namespace spot
 
   tgba_digraph_ptr
   lbtt_parse(std::istream& is, std::string& error, const bdd_dict_ptr& dict,
-	     ltl::environment& env, ltl::environment& envacc)
+	     ltl::environment& env)
   {
     is >> std::skipws;
 
@@ -306,10 +304,8 @@ namespace spot
       type = is.get();
 
     if (type == 't' || type == 'T')
-      return lbtt_read_tgba(num_states, num_acc, is, error, dict,
-			    env, envacc);
+      return lbtt_read_tgba(num_states, num_acc, is, error, dict, env);
     else
-      return lbtt_read_gba(num_states, num_acc, is, error, dict,
-			   env, envacc);
+      return lbtt_read_gba(num_states, num_acc, is, error, dict, env);
   }
 }

src/tgbaalgos/lbtt.hh

@@ -54,8 +54,7 @@ namespace spot
   SPOT_API tgba_digraph_ptr
   lbtt_parse(std::istream& is, std::string& error,
 	     const bdd_dict_ptr& dict,
-	     ltl::environment& env = ltl::default_environment::instance(),
-	     ltl::environment& envacc = ltl::default_environment::instance());
+	     ltl::environment& env = ltl::default_environment::instance());
 }
 
 #endif // SPOT_TGBAALGOS_LBTT_HH

src/tgbaparse/public.hh

@@ -53,8 +53,6 @@ namespace spot
   /// \param dict The BDD dictionary where to use.
   /// \param env The environment of atomic proposition into which parsing
   ///        should take place.
-  /// \param envacc The environment of acceptance conditions into which parsing
-  ///        should take place.
   /// \param debug When true, causes the parser to trace its execution.
   /// \return A pointer to the tgba built from \a filename, or
   ///        0 if the file could not be opened.
@@ -71,8 +69,6 @@ namespace spot
 			   bdd_dict_ptr dict,
 			   ltl::environment& env
 			   = ltl::default_environment::instance(),
-			   ltl::environment& envacc
-			   = ltl::default_environment::instance(),
 			   bool debug = false);
 
   /// \brief Format diagnostics produced by spot::tgba_parse.

src/tgbaparse/tgbaparse.yy

@@ -190,16 +190,7 @@ acc_list:
 acc_decl:
        | acc_decl strident
        {
-	 if (! acc_map.declare(*$2))
-	   {
-	     std::string s = "acceptance condition `";
-	     s += *$2;
-	     s += "' unknown in environment `";
-	     s += acc_map.get_env().name();
-	     s += "'";
-	     error_list.emplace_back(@2, s);
-	     YYERROR;
-	   }
+	 acc_map.declare(*$2);
 	 delete $2;
        }
        ;
@@ -220,7 +211,6 @@ namespace spot
 	     tgba_parse_error_list& error_list,
 	     bdd_dict_ptr dict,
 	     environment& env,
-	     environment& envacc,
 	     bool debug)
   {
     if (tgbayyopen(name))
@@ -232,7 +222,7 @@ namespace spot
     formula_cache fcache;
     auto result = make_tgba_digraph(dict);
     auto namer = result->create_namer<std::string>();
-    spot::acc_mapper_string acc_map(result, envacc);
+    spot::acc_mapper_string acc_map(result);
     tgbayy::parser parser(error_list, env, acc_map, result, namer, fcache);
     parser.set_debug_level(debug);
     parser.parse();

src/tgbatest/ltl2tgba.cc

@@ -633,7 +633,7 @@ checked_main(int argc, char** argv)
 	  spot::tgba_parse_error_list pel;
 	  spot::tgba_digraph_ptr s;
 	  s = spot::tgba_parse(argv[formula_index] + 2,
-			       pel, dict, env, env, debug_opt);
+			       pel, dict, env, debug_opt);
 	  if (spot::format_tgba_parse_errors(std::cerr,
 					     argv[formula_index] + 2, pel))
 	    return 2;
@@ -1021,8 +1021,7 @@ checked_main(int argc, char** argv)
 		  spot::tgba_digraph_ptr e;
 		  spot::tgba_parse_error_list pel;
 		  tm.start("parsing automaton");
-		  a = e = spot::tgba_parse(input, pel, dict,
-						     env, env, debug_opt);
+		  a = e = spot::tgba_parse(input, pel, dict, env, debug_opt);
 		  tm.stop("parsing automaton");
 		  if (spot::format_tgba_parse_errors(std::cerr, input, pel))
 		    return 2;
@@ -1044,7 +1043,7 @@ checked_main(int argc, char** argv)
 		      }
 		  }
 		tm.start("parsing lbtt");
-		a = spot::lbtt_parse(*in, error, dict, env, env);
+		a = spot::lbtt_parse(*in, error, dict, env);
 		tm.stop("parsing lbtt");
 		delete f;
 		if (!a)

src/tgbatest/tgbaread.cc

@@ -57,8 +57,7 @@ main(int argc, char** argv)
 
     spot::ltl::environment& env(spot::ltl::default_environment::instance());
     spot::tgba_parse_error_list pel;
-    auto a = spot::tgba_parse(argv[filename_index],
-			      pel, dict, env, env, debug);
+    auto a = spot::tgba_parse(argv[filename_index], pel, dict, env, debug);
 
     if (spot::format_tgba_parse_errors(std::cerr, argv[filename_index], pel))
       return 2;