From 1e0f99e82406a18c473563600d284f1284358ed5 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sat, 6 Nov 2010 17:56:27 +0100 Subject: [PATCH] Cosmetics to please sanity checks. * src/neverparse/public.hh, src/neverparse/parsedecl.hh: Fix inclusion guards. * src/tgba/tgbaexplicit.hh, src/tgbatest/emptchk.test, src/tgbatest/ltl2tgba.cc: Fix trailing whitespaces. --- ChangeLog | 19 ++++++++++++++----- src/neverparse/parsedecl.hh | 9 ++++----- src/neverparse/public.hh | 4 ++-- src/tgba/tgbaexplicit.hh | 4 ++-- src/tgbatest/emptchk.test | 4 ++-- src/tgbatest/ltl2tgba.cc | 7 +++---- 6 files changed, 27 insertions(+), 20 deletions(-) diff --git a/ChangeLog b/ChangeLog index 25fe0a2de..d61398a0f 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,12 @@ +2010-11-06 Alexandre Duret-Lutz + + Cosmetics to please sanity checks. + + * src/neverparse/public.hh, src/neverparse/parsedecl.hh: Fix + inclusion guards. + * src/tgba/tgbaexplicit.hh, src/tgbatest/emptchk.test, + src/tgbatest/ltl2tgba.cc: Fix trailing whitespaces. + 2010-11-06 Alexandre Duret-Lutz * src/tgbatest/ltl2tgba.cc: Clock the time spent reading -P file. @@ -29,14 +38,14 @@ single instruction for a state. * src/neverparse/neverclaimscan.ll: Recognize "false" specifically, and remove the ";" hack. - * src/tgba/tgbaexplicit.cc + * src/tgba/tgbaexplicit.cc (tgba_explicit_string::~tgba_explicit_string): Adjust not to destroy a state twice. * src/tgba/tgbaexplicit.hh (tgba_explicit_string::add_state_alias): New function. * src/tgbatest/defs.in (SPIN, LTL2BA): New variables. * src/tgbatest/neverclaimread.test: Check error messages for - syntax errors in guards. Make sure we can read the output + syntax errors in guards. Make sure we can read the output of `spin -f' and `ltl2ba -f' on a few test formulae. 2010-11-06 Alexandre Duret-Lutz @@ -49,9 +58,9 @@ removed by previous patch. * README: Adjust, and keep the file's width under 80 columns. * configure.ac: Adjust. - * src/neverparse/Makefile.am, src/neverparse/fmterror.cc, - src/neverparse/neverclaimparse.yy, - src/neverparse/neverclaimscan.ll, src/neverparse/public.hh: + * src/neverparse/Makefile.am, src/neverparse/fmterror.cc, + src/neverparse/neverclaimparse.yy, + src/neverparse/neverclaimscan.ll, src/neverparse/public.hh: Fix copyright. * src/tgbatest/Makefile.am (check_PROGRAMS): Remove neverclaimread. * src/tgbatest/ltl2tgba.cc: Add option -XN to read a neverclaim. diff --git a/src/neverparse/parsedecl.hh b/src/neverparse/parsedecl.hh index 49df9bcf3..75b1aa2f6 100644 --- a/src/neverparse/parsedecl.hh +++ b/src/neverparse/parsedecl.hh @@ -1,6 +1,5 @@ -// Copyright (C) 2003, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), -// département Systèmes Répartis Coopératifs (SRC), Université Pierre -// et Marie Curie. +// Copyright (C) 2010 Laboratoire de Recherche et Développement de +// l'EPITA. // // This file is part of Spot, a model checking library. // @@ -19,8 +18,8 @@ // Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA // 02111-1307, USA. -#ifndef SPOT_NEVERCLAIMPARSE_PARSEDECL_HH -# define SPOT_NEVERCLAIMPARSE_PARSEDECL_HH +#ifndef SPOT_NEVERPARSE_PARSEDECL_HH +# define SPOT_NEVERPARSE_PARSEDECL_HH #include #include "neverclaimparse.hh" diff --git a/src/neverparse/public.hh b/src/neverparse/public.hh index 1831de5fd..394f7f03b 100644 --- a/src/neverparse/public.hh +++ b/src/neverparse/public.hh @@ -18,8 +18,8 @@ // Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA // 02111-1307, USA. -#ifndef SPOT_NEVERCLAIMPARSE_PUBLIC_HH -# define SPOT_NEVERCLAIMPARSE_PUBLIC_HH +#ifndef SPOT_NEVERPARSE_PUBLIC_HH +# define SPOT_NEVERPARSE_PUBLIC_HH # include "tgba/tgbaexplicit.hh" // Unfortunately Bison 2.3 uses the same guards in all parsers :( diff --git a/src/tgba/tgbaexplicit.hh b/src/tgba/tgbaexplicit.hh index 2b8519019..7dc7a3267 100644 --- a/src/tgba/tgbaexplicit.hh +++ b/src/tgba/tgbaexplicit.hh @@ -212,7 +212,7 @@ namespace spot } return i->second; } - + state* set_init_state(const label& state) { @@ -327,7 +327,7 @@ namespace spot /// Create an alias for a state. Any reference to \a alias_name /// will act as a reference to \a real_name. virtual - void add_state_alias(const std::string& alias_name, + void add_state_alias(const std::string& alias_name, const std::string& real_name) { name_state_map_[alias_name] = add_state(real_name); diff --git a/src/tgbatest/emptchk.test b/src/tgbatest/emptchk.test index 9a6e9b2ed..17b221d09 100755 --- a/src/tgbatest/emptchk.test +++ b/src/tgbatest/emptchk.test @@ -54,9 +54,9 @@ expect_ce() run 0 ../ltl2tgba -CR -eTau03_opt -f "$1" run 0 ../ltl2tgba -CR -eGV04 -f "$1" # Expect multiple accepting runs - test `../ltl2tgba -CR -e'CVWY90(repeated)' -l "$1" | + test `../ltl2tgba -CR -e'CVWY90(repeated)' -l "$1" | grep Prefix: | wc -l` -ge $2 - test `../ltl2tgba -CR -e'SE05(repeated)' -l "$1" | + test `../ltl2tgba -CR -e'SE05(repeated)' -l "$1" | grep Prefix: | wc -l` -ge $2 } diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc index 491462e9d..9a788c2f0 100644 --- a/src/tgbatest/ltl2tgba.cc +++ b/src/tgbatest/ltl2tgba.cc @@ -784,15 +784,15 @@ main(int argc, char** argv) { spot::neverclaim_parse_error_list pel; tm.start("parsing neverclaim"); - to_free = a = e = spot::neverclaim_parse(input, pel, dict, - env, debug_opt); + to_free = a = e = spot::neverclaim_parse(input, pel, dict, + env, debug_opt); tm.stop("parsing neverclaim"); if (spot::format_neverclaim_parse_errors(std::cerr, input, pel)) { delete to_free; delete dict; return 2; - } + } } e->merge_transitions(); } @@ -1166,7 +1166,6 @@ main(int argc, char** argv) else { spot::print_tgba_run(std::cout, a, run); - if (accepting_run_replay && !spot::replay_tgba_run(std::cout, a, run, true))