diff --git a/src/bin/randltl.cc b/src/bin/randltl.cc index a6bdd8013..9ce5f2f18 100644 --- a/src/bin/randltl.cc +++ b/src/bin/randltl.cc @@ -245,71 +245,83 @@ main(int argc, char** argv) program_name); spot::srand(opt_seed); - - spot::option_map opts; - opts.set("output", output); - opts.set("tree_size_min", opt_tree_size.min); - opts.set("tree_size_max", opt_tree_size.max); - opts.set("opt_wf", opt_wf); - opts.set("opt_seed", opt_seed); - opts.set("simplification_level", simplification_level); - spot::ltl::randltlgenerator rg(aprops, opts, opt_pL, opt_pS, opt_pB); - - if (opt_dump_priorities) + try { - switch (output) - { - case OUTPUTLTL: - std::cout - << "Use --ltl-priorities to set the following LTL priorities:\n"; - rg.dump_ltl_priorities(std::cout); - break; - case OUTPUTBOOL: - std::cout - << ("Use --boolean-priorities to set the following Boolean " - "formula priorities:\n"); - rg.dump_bool_priorities(std::cout); - break; - case OUTPUTPSL: - std::cout - << "Use --ltl-priorities to set the following LTL priorities:\n"; - rg.dump_psl_priorities(std::cout); - // Fall through. - case OUTPUTSERE: - std::cout - << "Use --sere-priorities to set the following SERE priorities:\n"; - rg.dump_sere_priorities(std::cout); - std::cout - << ("Use --boolean-priorities to set the following Boolean " - "formula priorities:\n"); - rg.dump_sere_bool_priorities(std::cout); - break; - default: - error(2, 0, "internal error: unknown type of output"); - } - opts.~option_map(); - destroy_atomic_prop_set(aprops); - exit(0); + spot::ltl::randltlgenerator rg + (aprops, + [&] (){ + spot::option_map opts; + opts.set("output", output); + opts.set("tree_size_min", opt_tree_size.min); + opts.set("tree_size_max", opt_tree_size.max); + opts.set("opt_wf", opt_wf); + opts.set("opt_seed", opt_seed); + opts.set("simplification_level", simplification_level); + return opts; + }(), opt_pL, opt_pS, opt_pB); + + if (opt_dump_priorities) + { + switch (output) + { + case OUTPUTLTL: + std::cout << + "Use --ltl-priorities to set the following LTL priorities:\n"; + rg.dump_ltl_priorities(std::cout); + break; + case OUTPUTBOOL: + std::cout << + "Use --boolean-priorities to set the following Boolean " + "formula priorities:\n"; + rg.dump_bool_priorities(std::cout); + break; + case OUTPUTPSL: + std::cout << + "Use --ltl-priorities to set the following LTL priorities:\n"; + rg.dump_psl_priorities(std::cout); + // Fall through. + case OUTPUTSERE: + std::cout << + "Use --sere-priorities to set the following SERE priorities:\n"; + rg.dump_sere_priorities(std::cout); + std::cout << + "Use --boolean-priorities to set the following Boolean " + "formula priorities:\n"; + rg.dump_sere_bool_priorities(std::cout); + break; + default: + error(2, 0, "internal error: unknown type of output"); + } + destroy_atomic_prop_set(aprops); + exit(0); + } + + while (opt_formulas < 0 || opt_formulas--) + { + static int count = 0; + const spot::ltl::formula* f = rg.next(); + if (!f) + { + error(2, 0, "failed to generate a new unique formula after %d " \ + "trials", MAX_TRIALS); + } + else + { + output_formula_checked(f, 0, ++count); + f->destroy(); + } + }; } - - while (opt_formulas < 0 || opt_formulas--) + catch (const std::runtime_error& e) { - static int count = 0; - spot::ltl::randltlgenerator rg2(aprops, opts); - const spot::ltl::formula* f = rg.next(); - if (!f) - { - opts.~option_map(); - error(2, 0, "failed to generate a new unique formula after %d "\ - "trials", MAX_TRIALS); - } - else - { - output_formula_checked(f, 0, ++count); - f->destroy(); - } - }; - + destroy_atomic_prop_set(aprops); + error(2, 0, "%s", e.what()); + } + catch (const std::invalid_argument& e) + { + destroy_atomic_prop_set(aprops); + error(2, 0, "%s", e.what()); + } destroy_atomic_prop_set(aprops); return 0; diff --git a/src/ltltest/rand.test b/src/ltltest/rand.test index bbf9b8ad6..c6d8a7a01 100755 --- a/src/ltltest/rand.test +++ b/src/ltltest/rand.test @@ -136,3 +136,7 @@ run 0 $randltl -n5 2 -o test-all.ltl run 0 $randltl -n5 2 -o test-%L.ltl cat test-1.ltl test-2.ltl test-3.ltl test-4.ltl test-5.ltl > test-cmp.ltl diff test-cmp.ltl test-all.ltl + + +$randltl 2 --ltl-prio=X 2>stderr && exit 1 +grep 'failed to parse LTL priorities near X' stderr diff --git a/src/ltlvisit/randomltl.cc b/src/ltlvisit/randomltl.cc index d58119ca6..0baba161b 100644 --- a/src/ltlvisit/randomltl.cc +++ b/src/ltlvisit/randomltl.cc @@ -404,12 +404,11 @@ namespace spot update_sums(); } - void - randltlgenerator::construct(atomic_prop_set aprops, option_map& opts, + randltlgenerator::randltlgenerator(atomic_prop_set aprops, + const option_map& opts, char* opt_pL, char* opt_pS, char* opt_pB) - { aprops_ = aprops; output_ = opts.get("output", OUTPUTLTL); @@ -429,10 +428,10 @@ namespace spot case OUTPUTLTL: rf_ = new random_ltl(&aprops_); if (opt_pS) - throw std::invalid_argument("Cannot set sere priorities with "\ + throw std::invalid_argument("Cannot set sere priorities with " "LTL output"); if (opt_pB) - throw std::invalid_argument("Cannot set boolean priorities with "\ + throw std::invalid_argument("Cannot set boolean priorities with " "LTL output"); tok_pL = rf_->parse_options(opt_pL); break; @@ -440,10 +439,10 @@ namespace spot rf_ = new random_boolean(&aprops_); tok_pB = rf_->parse_options(opt_pB); if (opt_pL) - throw std::invalid_argument("Cannot set ltl priorities with "\ + throw std::invalid_argument("Cannot set ltl priorities with " "Boolean output"); if (opt_pS) - throw std::invalid_argument("Cannot set sere priorities "\ + throw std::invalid_argument("Cannot set sere priorities " "with Boolean output"); break; case OUTPUTSERE: @@ -451,7 +450,7 @@ namespace spot tok_pS = rs_->parse_options(opt_pS); tok_pB = rs_->rb.parse_options(opt_pB); if (opt_pL) - throw std::invalid_argument("Cannot set ltl priorities "\ + throw std::invalid_argument("Cannot set ltl priorities " "with SERE output"); break; case OUTPUTPSL: @@ -464,47 +463,30 @@ namespace spot } if (tok_pL) - throw("failed to parse LTL priorities near '" + std::string(tok_pL)); + throw std::invalid_argument("failed to parse LTL priorities near " + + std::string(tok_pL)); if (tok_pS) - throw("failed to parse SERE priorities near " + std::string(tok_pS)); + throw std::invalid_argument("failed to parse SERE priorities near " + + std::string(tok_pS)); if (tok_pB) - throw("failed to parse Boolean priorities near " - + std::string(tok_pB)); + throw std::invalid_argument("failed to parse Boolean priorities near " + + std::string(tok_pB)); spot::srand(opt_seed_); ltl_simplifier_options simpl_opts(opt_simpl_level_); ltl_simplifier simpl_(simpl_opts); } - randltlgenerator::randltlgenerator(int aprops_n, option_map& opts, + randltlgenerator::randltlgenerator(int aprops_n, + const option_map& opts, char* opt_pL, char* opt_pS, char* opt_pB) - { - atomic_prop_set aprops_; - default_environment& e = - default_environment::instance(); - for (int i = 0; i < aprops_n; ++i) - { - std::ostringstream p; - p << 'p' << i; - aprops_.insert(static_cast - (e.require(p.str()))); - } - construct(aprops_, opts, opt_pL, opt_pS, opt_pB); - } - - randltlgenerator::randltlgenerator(atomic_prop_set aprops, - option_map& opts, - char* opt_pL, - char* opt_pS, - char* opt_pB) - + : randltlgenerator(create_atomic_prop_set(aprops_n), opts, + opt_pL, opt_pS, opt_pB) { - construct(aprops, opts, opt_pL, opt_pS, opt_pB); } - randltlgenerator::~randltlgenerator() { delete rf_; @@ -512,6 +494,7 @@ namespace spot for (auto i: unique_set_) i->destroy(); } + const formula* randltlgenerator::next() { unsigned trials = MAX_TRIALS; @@ -593,32 +576,32 @@ namespace spot void randltlgenerator::dump_ltl_priorities(std::ostream& os) - { - rf_->dump_priorities(os); - } + { + rf_->dump_priorities(os); + } void randltlgenerator::dump_bool_priorities(std::ostream& os) - { - rf_->dump_priorities(os); - } + { + rf_->dump_priorities(os); + } void randltlgenerator::dump_psl_priorities(std::ostream& os) - { - rp_->dump_priorities(os); - } + { + rp_->dump_priorities(os); + } void randltlgenerator::dump_sere_priorities(std::ostream& os) - { - rs_->dump_priorities(os); - } + { + rs_->dump_priorities(os); + } void randltlgenerator::dump_sere_bool_priorities(std::ostream& os) - { - rs_->rb.dump_priorities(os); - } + { + rs_->rb.dump_priorities(os); + } } } diff --git a/src/ltlvisit/randomltl.hh b/src/ltlvisit/randomltl.hh index d14f3243b..cc0e50691 100644 --- a/src/ltlvisit/randomltl.hh +++ b/src/ltlvisit/randomltl.hh @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2010, 2011, 2012, 2013, 2014 Laboratoire de Recherche -// et Développement de l'Epita (LRDE). +// Copyright (C) 2010, 2011, 2012, 2013, 2014, 2015 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 // et Marie Curie. @@ -310,40 +310,31 @@ namespace spot const spot::ptr_hash> fset_t; - public: - randltlgenerator(int aprops_n, option_map& opts, + public: + randltlgenerator(int aprops_n, const option_map& opts, char* opt_pL = nullptr, char* opt_pS = nullptr, char* opt_pB = nullptr); - randltlgenerator(atomic_prop_set aprops, option_map& opts, + randltlgenerator(atomic_prop_set aprops, const option_map& opts, char* opt_pL = nullptr, char* opt_pS = nullptr, char* opt_pB = nullptr); - void construct(atomic_prop_set aprops, option_map& opts, - char* opt_pL, char* opt_pS, - char* opt_pB); - ~randltlgenerator(); const spot::ltl::formula* next(); void dump_ltl_priorities(std::ostream& os); - void dump_bool_priorities(std::ostream& os); - void dump_psl_priorities(std::ostream& os); - void dump_sere_priorities(std::ostream& os); - void dump_sere_bool_priorities(std::ostream& os); - void remove_some_props(atomic_prop_set& s); const formula* GF_n(); - private: + private: fset_t unique_set_; atomic_prop_set aprops_;