From fc0ed01a45c5214385ab6dc0596c9fc887a52974 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 16 May 2018 17:38:59 +0200 Subject: [PATCH] randomltl: avoid #define As this pollutes the user's namespace. * spot/tl/randomltl.hh: Use class-level enum and constexpr instead of #define. * spot/tl/randomltl.cc, python/spot/__init__.py, bin/randltl.cc, tests/python/dualize.py, tests/python/sum.py: Adjust usage. --- bin/randltl.cc | 25 ++++++++++++------------- python/spot/__init__.py | 18 +++++++++--------- spot/tl/randomltl.cc | 10 +++++----- spot/tl/randomltl.hh | 11 ++++------- tests/python/dualize.py | 4 ++-- tests/python/sum.py | 2 +- 6 files changed, 33 insertions(+), 37 deletions(-) diff --git a/bin/randltl.cc b/bin/randltl.cc index 8da179e8e..b364e434f 100644 --- a/bin/randltl.cc +++ b/bin/randltl.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012, 2013, 2014, 2015, 2016 Laboratoire de Recherche +// Copyright (C) 2012, 2013, 2014, 2015, 2016, 2018 Laboratoire de Recherche // et Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -142,7 +142,8 @@ static struct opt_t spot::atomic_prop_set aprops; }* opt; -static int output = OUTPUTLTL; +static spot::randltlgenerator::output_type output = + spot::randltlgenerator::LTL; static char* opt_pL = nullptr; static char* opt_pS = nullptr; static char* opt_pB = nullptr; @@ -161,22 +162,22 @@ parse_opt(int key, char* arg, struct argp_state* as) switch (key) { case 'B': - output = OUTPUTBOOL; + output = spot::randltlgenerator::Bool; break; case 'L': - output = OUTPUTLTL; + output = spot::randltlgenerator::LTL; break; case 'n': opt_formulas = to_int(arg); break; case 'P': - output = OUTPUTPSL; + output = spot::randltlgenerator::PSL; break; case OPT_R: parse_r(arg); break; case 'S': - output = OUTPUTSERE; + output = spot::randltlgenerator::SERE; break; case OPT_BOOLEAN_PRIORITIES: opt_pB = arg; @@ -275,23 +276,23 @@ main(int argc, char** argv) { switch (output) { - case OUTPUTLTL: + case spot::randltlgenerator::LTL: std::cout << "Use --ltl-priorities to set the following LTL priorities:\n"; rg.dump_ltl_priorities(std::cout); break; - case OUTPUTBOOL: + case spot::randltlgenerator::Bool: std::cout << "Use --boolean-priorities to set the following Boolean " "formula priorities:\n"; rg.dump_bool_priorities(std::cout); break; - case OUTPUTPSL: + case spot::randltlgenerator::PSL: std::cout << "Use --ltl-priorities to set the following LTL priorities:\n"; rg.dump_psl_priorities(std::cout); SPOT_FALLTHROUGH; - case OUTPUTSERE: + case spot::randltlgenerator::SERE: std::cout << "Use --sere-priorities to set the following SERE priorities:\n"; rg.dump_sere_priorities(std::cout); @@ -300,8 +301,6 @@ main(int argc, char** argv) "formula priorities:\n"; rg.dump_sere_bool_priorities(std::cout); break; - default: - error(2, 0, "internal error: unknown type of output"); } exit(0); } @@ -313,7 +312,7 @@ main(int argc, char** argv) if (!f) { error(2, 0, "failed to generate a new unique formula after %d " \ - "trials", MAX_TRIALS); + "trials", spot::randltlgenerator::MAX_TRIALS); } else { diff --git a/python/spot/__init__.py b/python/spot/__init__.py index 4e47f29bd..74131f8e5 100644 --- a/python/spot/__init__.py +++ b/python/spot/__init__.py @@ -851,10 +851,10 @@ def randltl(ap, n=-1, **kwargs): """ opts = option_map() output_map = { - "ltl": OUTPUTLTL, - "psl": OUTPUTPSL, - "bool": OUTPUTBOOL, - "sere": OUTPUTSERE + "ltl": randltlgenerator.LTL, + "psl": randltlgenerator.PSL, + "bool": randltlgenerator.Bool, + "sere": randltlgenerator.SERE } if isinstance(ap, list): @@ -889,18 +889,18 @@ def randltl(ap, n=-1, **kwargs): dump_priorities = kwargs.get("dump_priorities", False) if dump_priorities: dumpstream = ostringstream() - if output == OUTPUTLTL: + if output == randltlgenerator.LTL: print('Use argument ltl_priorities=STRING to set the following ' 'LTL priorities:\n') rg.dump_ltl_priorities(dumpstream) print(dumpstream.str()) - elif output == OUTPUTBOOL: + elif output == randltlgenerator.Bool: print('Use argument boolean_priorities=STRING to set the ' 'following Boolean formula priorities:\n') rg.dump_bool_priorities(dumpstream) print(dumpstream.str()) - elif output == OUTPUTPSL or output == OUTPUTSERE: - if output != OUTPUTSERE: + elif output == randltlgenerator.PSL or output == randltlgenerator.SERE: + if output != randltlgenerator.SERE: print('Use argument ltl_priorities=STRING to set the ' 'following LTL priorities:\n') rg.dump_psl_priorities(dumpstream) @@ -933,7 +933,7 @@ def randltl(ap, n=-1, **kwargs): if f is None: sys.stderr.write("Warning: could not generate a new " "unique formula after {} trials.\n" - .format(MAX_TRIALS)) + .format(randltlgenerator.MAX_TRIALS)) raise StopIteration self.i += 1 return f diff --git a/spot/tl/randomltl.cc b/spot/tl/randomltl.cc index a284b0690..5f2754750 100644 --- a/spot/tl/randomltl.cc +++ b/spot/tl/randomltl.cc @@ -411,7 +411,7 @@ namespace spot simpl_(tl_simplifier_options{opt_simpl_level_}) { aprops_ = aprops; - output_ = opts.get("output", OUTPUTLTL); + output_ = opts.get("output", randltlgenerator::LTL); opt_seed_ = opts.get("seed", 0); opt_tree_size_min_ = opts.get("tree_size_min", 15); opt_tree_size_max_ = opts.get("tree_size_max", 15); @@ -424,7 +424,7 @@ namespace spot switch (output_) { - case OUTPUTLTL: + case randltlgenerator::LTL: rf_ = new random_ltl(&aprops_); if (opt_pS) throw std::invalid_argument("Cannot set sere priorities with " @@ -434,7 +434,7 @@ namespace spot "LTL output"); tok_pL = rf_->parse_options(opt_pL); break; - case OUTPUTBOOL: + case randltlgenerator::Bool: rf_ = new random_boolean(&aprops_); tok_pB = rf_->parse_options(opt_pB); if (opt_pL) @@ -444,7 +444,7 @@ namespace spot throw std::invalid_argument("Cannot set sere priorities " "with Boolean output"); break; - case OUTPUTSERE: + case randltlgenerator::SERE: rf_ = rs_ = new random_sere(&aprops_); tok_pS = rs_->parse_options(opt_pS); tok_pB = rs_->rb.parse_options(opt_pB); @@ -452,7 +452,7 @@ namespace spot throw std::invalid_argument("Cannot set ltl priorities " "with SERE output"); break; - case OUTPUTPSL: + case randltlgenerator::PSL: rf_ = rp_ = new random_psl(&aprops_); rs_ = &rp_->rs; tok_pL = rp_->parse_options(opt_pL); diff --git a/spot/tl/randomltl.hh b/spot/tl/randomltl.hh index 2fe4892f0..2811c18ac 100644 --- a/spot/tl/randomltl.hh +++ b/spot/tl/randomltl.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2010, 2011, 2012, 2013, 2014, 2015, 2016 Laboratoire de +// Copyright (C) 2010-2016, 2018 Laboratoire de // Recherche et Développement de l'Epita (LRDE). // Copyright (C) 2005 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre @@ -30,12 +30,6 @@ #include #include -#define OUTPUTBOOL 1 -#define OUTPUTLTL 2 -#define OUTPUTSERE 3 -#define OUTPUTPSL 4 -#define MAX_TRIALS 100000 - namespace spot { /// \ingroup tl_io @@ -305,6 +299,9 @@ namespace spot public: + enum output_type { Bool, LTL, SERE, PSL }; + static constexpr unsigned MAX_TRIALS = 100000U; + randltlgenerator(int aprops_n, const option_map& opts, char* opt_pL = nullptr, char* opt_pS = nullptr, diff --git a/tests/python/dualize.py b/tests/python/dualize.py index 0d0e2fcec..abd3d2ddf 100755 --- a/tests/python/dualize.py +++ b/tests/python/dualize.py @@ -1,6 +1,6 @@ #!/usr/bin/python3 # -*- mode: python; coding: utf-8 -*- -# Copyright (C) 2017 Laboratoire de Recherche et Développement de +# Copyright (C) 2017, 2018 Laboratoire de Recherche et Développement de # l'EPITA. # # This file is part of Spot, a model checking library. @@ -585,7 +585,7 @@ State: 5 --END--""" opts = spot.option_map() -opts.set('output', spot.OUTPUTLTL) +opts.set('output', spot.randltlgenerator.LTL) opts.set('tree_size_min', 15) opts.set('tree_size_max', 15) opts.set('seed', 0) diff --git a/tests/python/sum.py b/tests/python/sum.py index 9aaa7e331..cafc0a963 100644 --- a/tests/python/sum.py +++ b/tests/python/sum.py @@ -34,7 +34,7 @@ except RuntimeError: opts = spot.option_map() -opts.set('output', spot.OUTPUTLTL) +opts.set('output', spot.randltlgenerator.LTL) opts.set('tree_size_min', 15) opts.set('tree_size_max', 15) opts.set('wf', False)