From e4158c21ee858890386d836238c0ed107c14b796 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 10 Dec 2014 15:10:28 +0100 Subject: [PATCH] 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 | 32 ++++++++------------------------ src/tgbaalgos/lbtt.cc | 18 +++++++----------- src/tgbaalgos/lbtt.hh | 3 +-- src/tgbaparse/public.hh | 4 ---- src/tgbaparse/tgbaparse.yy | 14 ++------------ src/tgbatest/ltl2tgba.cc | 7 +++---- src/tgbatest/tgbaread.cc | 3 +-- 7 files changed, 22 insertions(+), 59 deletions(-) diff --git a/src/priv/accmap.hh b/src/priv/accmap.hh index e82f57dd4..b053451fe 100644 --- a/src/priv/accmap.hh +++ b/src/priv/accmap.hh @@ -23,7 +23,6 @@ #include #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 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 vmap(count); aut->acc().add_sets(count); @@ -111,11 +98,8 @@ namespace spot std::map 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) { } diff --git a/src/tgbaalgos/lbtt.cc b/src/tgbaalgos/lbtt.cc index 56c025b4b..d3f02c93f 100644 --- a/src/tgbaalgos/lbtt.cc +++ b/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); } } diff --git a/src/tgbaalgos/lbtt.hh b/src/tgbaalgos/lbtt.hh index d9b8688bb..23b972812 100644 --- a/src/tgbaalgos/lbtt.hh +++ b/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 diff --git a/src/tgbaparse/public.hh b/src/tgbaparse/public.hh index 508a8f660..4861e408b 100644 --- a/src/tgbaparse/public.hh +++ b/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. diff --git a/src/tgbaparse/tgbaparse.yy b/src/tgbaparse/tgbaparse.yy index f7f21fedd..4ed3c90dd 100644 --- a/src/tgbaparse/tgbaparse.yy +++ b/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(); - 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(); diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc index b5acd3ee6..d305e4003 100644 --- a/src/tgbatest/ltl2tgba.cc +++ b/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) diff --git a/src/tgbatest/tgbaread.cc b/src/tgbatest/tgbaread.cc index a55e43b87..c519eeb89 100644 --- a/src/tgbatest/tgbaread.cc +++ b/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;