alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

* src/tgbaparse/public.hh (tgba_parse): Take two environments

Browse source 
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.
This commit is contained in:
Alexandre Duret-Lutz 2006-02-10 16:41:17 +00:00
parent e5481ee3ac
commit 5891679ce0
7 changed files with 42 additions and 25 deletions
Download patch file Download diff file Expand all files Collapse all files

10
ChangeLog
View file

@ -1,5 +1,15 @@
2006-02-10 Alexandre Duret-Lutz <adl@src.lip6.fr>
* 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.

13
src/tgbaparse/public.hh
View file

@ -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.

10
src/tgbaparse/tgbaparse.yy
View file

@ -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();

10
src/tgbatest/ltl2tgba.cc
View file

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

8
src/tgbatest/readsave.cc
View file

@ -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);

8
src/tgbatest/reductgba.cc
View file

@ -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

8
src/tgbatest/tgbaread.cc
View file

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