diff --git a/ChangeLog b/ChangeLog index 5efcf9815..811c6ae4a 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,5 +1,15 @@ 2006-02-10 Alexandre Duret-Lutz + * src/tgbaparse/public.hh (tgba_parse): Take two environments + instead of one : one for the atomic propositions, and one + for the acceptance conditions. This way it's easy for + the tools in iface/gspn/ to require some atomic proposition + to be declared and allow any acceptance conditions (there is nothing + to adjust in this files because of the default value of the argument). + * src/tgbaparse/tgbaparse.yy: Adjust. + * src/tgbatest/ltl2tgba.cc, src/tgbatest/readsave.cc, + src/tgbatest/reductgba.cc, src/tgbatest/tgbaread.cc: Adjust calls. + * src/tgbaparse/tgbaparse.yy (acc_decl): Diagnose acceptance conditions rejected by the environment. diff --git a/src/tgbaparse/public.hh b/src/tgbaparse/public.hh index 0c79c16ce..869d85b9c 100644 --- a/src/tgbaparse/public.hh +++ b/src/tgbaparse/public.hh @@ -1,6 +1,6 @@ -// Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), -// département Systèmes Répartis Coopératifs (SRC), Université Pierre -// et Marie Curie. +// Copyright (C) 2003, 2004, 2005, 2006 Laboratoire d'Informatique de +// Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), +// Université Pierre et Marie Curie. // // This file is part of Spot, a model checking library. // @@ -45,7 +45,10 @@ namespace spot /// \param error_list A list that will be filled with /// parse errors that occured during parsing. /// \param dict The BDD dictionary where to use. - /// \param env The environment into which parsing should take place. + /// \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. @@ -61,6 +64,8 @@ namespace spot bdd_dict* 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 1eea064fd..e5b11b18b 100644 --- a/src/tgbaparse/tgbaparse.yy +++ b/src/tgbaparse/tgbaparse.yy @@ -26,6 +26,7 @@ %parse-param {spot::tgba_parse_error_list& error_list} %parse-param {spot::ltl::environment& parse_environment} +%parse-param {spot::ltl::environment& parse_envacc} %parse-param {spot::tgba_explicit*& result} %parse-param {formula_cache& fcache} %debug @@ -175,7 +176,7 @@ acc_list: } else if (*$2 != "" && *$2 != "false") { - formula* f = parse_environment.require(*$2); + formula* f = parse_envacc.require(*$2); if (! result->has_acceptance_condition(f)) { error_list.push_back(spot::tgba_parse_error(@2, @@ -195,13 +196,13 @@ acc_list: acc_decl: | acc_decl strident { - formula* f = parse_environment.require(*$2); + formula* f = parse_envacc.require(*$2); if (! f) { std::string s = "acceptance condition `"; s += *$2; s += "' unknown in environment `"; - s += parse_environment.name(); + s += parse_envacc.name(); s += "'"; error_list.push_back(spot::tgba_parse_error(@2, s)); YYERROR; @@ -226,6 +227,7 @@ namespace spot tgba_parse_error_list& error_list, bdd_dict* dict, environment& env, + environment& envacc, bool debug) { if (tgbayyopen(name)) @@ -237,7 +239,7 @@ namespace spot } formula_cache fcache; tgba_explicit* result = new tgba_explicit(dict); - tgbayy::parser parser(error_list, env, result, fcache); + tgbayy::parser parser(error_list, env, envacc, result, fcache); parser.set_debug_level(debug); parser.parse(); tgbayyclose(); diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc index 311511bac..fbb5a81f8 100644 --- a/src/tgbatest/ltl2tgba.cc +++ b/src/tgbatest/ltl2tgba.cc @@ -1,6 +1,6 @@ -// Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), -// département Systèmes Répartis Coopératifs (SRC), Université Pierre -// et Marie Curie. +// Copyright (C) 2003, 2004, 2005, 2006 Laboratoire d'Informatique de +// Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), +// Université Pierre et Marie Curie. // // This file is part of Spot, a model checking library. // @@ -306,7 +306,7 @@ main(int argc, char** argv) { spot::tgba_parse_error_list pel; system = spot::tgba_parse(argv[formula_index] + 2, - pel, dict, env, debug_opt); + pel, dict, env, env, debug_opt); if (spot::format_tgba_parse_errors(std::cerr, argv[formula_index] + 2, pel)) return 2; @@ -473,7 +473,7 @@ main(int argc, char** argv) { spot::tgba_parse_error_list pel; spot::tgba_explicit* e; - to_free = a = e = spot::tgba_parse(input, pel, dict, env, debug_opt); + to_free = a = e = spot::tgba_parse(input, pel, dict, env, env, debug_opt); if (spot::format_tgba_parse_errors(std::cerr, input, pel)) { delete to_free; diff --git a/src/tgbatest/readsave.cc b/src/tgbatest/readsave.cc index aa8562faf..0e3056acd 100644 --- a/src/tgbatest/readsave.cc +++ b/src/tgbatest/readsave.cc @@ -1,6 +1,6 @@ -// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), -// département Systèmes Répartis Coopératifs (SRC), Université Pierre -// et Marie Curie. +// Copyright (C) 2003, 2004, 2006 Laboratoire d'Informatique de Paris 6 +// (LIP6), département Systèmes Répartis Coopératifs (SRC), +// Université Pierre et Marie Curie. // // This file is part of Spot, a model checking library. // @@ -57,7 +57,7 @@ main(int argc, char** argv) spot::ltl::environment& env(spot::ltl::default_environment::instance()); spot::tgba_parse_error_list pel; spot::tgba_explicit* a = spot::tgba_parse(argv[filename_index], - pel, dict, env, debug); + pel, dict, env, env, debug); exit_code = spot::format_tgba_parse_errors(std::cerr, argv[filename_index], pel); diff --git a/src/tgbatest/reductgba.cc b/src/tgbatest/reductgba.cc index fc463e1ec..5ae491e1f 100644 --- a/src/tgbatest/reductgba.cc +++ b/src/tgbatest/reductgba.cc @@ -1,6 +1,6 @@ -// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), -// département Systèmes Répartis Coopératifs (SRC), Université Pierre -// et Marie Curie. +// Copyright (C) 2003, 2004, 2006 Laboratoire d'Informatique de Paris 6 +// (LIP6), département Systèmes Répartis Coopératifs (SRC), +// Université Pierre et Marie Curie. // // This file is part of Spot, a model checking library. // @@ -105,7 +105,7 @@ main(int argc, char** argv) #ifdef REDUCCMP spot::tgba_parse_error_list pel; - automata = spot::tgba_parse(argv[2], pel, dict, env, false); + automata = spot::tgba_parse(argv[2], pel, dict, env, env, false); if (spot::format_tgba_parse_errors(std::cerr, argv[2], pel)) return 2; #else diff --git a/src/tgbatest/tgbaread.cc b/src/tgbatest/tgbaread.cc index 0fddc0816..b3baec66c 100644 --- a/src/tgbatest/tgbaread.cc +++ b/src/tgbatest/tgbaread.cc @@ -1,6 +1,6 @@ -// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), -// département Systèmes Répartis Coopératifs (SRC), Université Pierre -// et Marie Curie. +// Copyright (C) 2003, 2004, 2006 Laboratoire d'Informatique de Paris 6 +// (LIP6), département Systèmes Répartis Coopératifs (SRC), Université +// Pierre et Marie Curie. // // This file is part of Spot, a model checking library. // @@ -55,7 +55,7 @@ main(int argc, char** argv) spot::ltl::environment& env(spot::ltl::default_environment::instance()); spot::tgba_parse_error_list pel; spot::tgba_explicit* a = spot::tgba_parse(argv[filename_index], - pel, dict, env, debug); + pel, dict, env, env, debug); if (spot::format_tgba_parse_errors(std::cerr, argv[filename_index], pel)) return 2;