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

randltl: some code cleanup

Browse source 
* src/ltlvisit/randomltl.cc, src/ltlvisit/randomltl.hh: Throw
invalid_argument exceptions consistently (not std::string), and use
forwarding constructors to avoid the construct() method.
* src/bin/randltl.cc: Catch the above exceptions.  Destroy
the opts variable right after its use, so that we don't need
explicit destructor calls.
* src/ltltest/rand.test: Add a test.
This commit is contained in:
Alexandre Duret-Lutz 2015-03-08 13:50:12 +01:00
parent 72c7ad9fcd
commit 4ffb0cb98d
4 changed files with 117 additions and 127 deletions
Download patch file Download diff file Expand all files Collapse all files

136
src/bin/randltl.cc
View file

@ -245,71 +245,83 @@ main(int argc, char** argv)
program_name); program_name);
spot::srand(opt_seed); spot::srand(opt_seed);
try
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)
{ {
switch (output) spot::ltl::randltlgenerator rg
{ (aprops,
case OUTPUTLTL: [&] (){
std::cout spot::option_map opts;
<< "Use --ltl-priorities to set the following LTL priorities:\n"; opts.set("output", output);
rg.dump_ltl_priorities(std::cout); opts.set("tree_size_min", opt_tree_size.min);
break; opts.set("tree_size_max", opt_tree_size.max);
case OUTPUTBOOL: opts.set("opt_wf", opt_wf);
std::cout opts.set("opt_seed", opt_seed);
<< ("Use --boolean-priorities to set the following Boolean " opts.set("simplification_level", simplification_level);
"formula priorities:\n"); return opts;
rg.dump_bool_priorities(std::cout); }(), opt_pL, opt_pS, opt_pB);
break;
case OUTPUTPSL: if (opt_dump_priorities)
std::cout {
<< "Use --ltl-priorities to set the following LTL priorities:\n"; switch (output)
rg.dump_psl_priorities(std::cout); {
// Fall through. case OUTPUTLTL:
case OUTPUTSERE: std::cout <<
std::cout "Use --ltl-priorities to set the following LTL priorities:\n";
<< "Use --sere-priorities to set the following SERE priorities:\n"; rg.dump_ltl_priorities(std::cout);
rg.dump_sere_priorities(std::cout); break;
std::cout case OUTPUTBOOL:
<< ("Use --boolean-priorities to set the following Boolean " std::cout <<
"formula priorities:\n"); "Use --boolean-priorities to set the following Boolean "
rg.dump_sere_bool_priorities(std::cout); "formula priorities:\n";
break; rg.dump_bool_priorities(std::cout);
default: break;
error(2, 0, "internal error: unknown type of output"); case OUTPUTPSL:
} std::cout <<
opts.~option_map(); "Use --ltl-priorities to set the following LTL priorities:\n";
destroy_atomic_prop_set(aprops); rg.dump_psl_priorities(std::cout);
exit(0); // 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();
}
};
} }
catch (const std::runtime_error& e)
while (opt_formulas < 0 || opt_formulas--)
{ {
static int count = 0; destroy_atomic_prop_set(aprops);
spot::ltl::randltlgenerator rg2(aprops, opts); error(2, 0, "%s", e.what());
const spot::ltl::formula* f = rg.next(); }
if (!f) catch (const std::invalid_argument& e)
{ {
opts.~option_map(); destroy_atomic_prop_set(aprops);
error(2, 0, "failed to generate a new unique formula after %d "\ error(2, 0, "%s", e.what());
"trials", MAX_TRIALS); }
}
else
{
output_formula_checked(f, 0, ++count);
f->destroy();
}
};
destroy_atomic_prop_set(aprops); destroy_atomic_prop_set(aprops);
return 0; return 0;

4
src/ltltest/rand.test
View file

@ -136,3 +136,7 @@ run 0 $randltl -n5 2 -o test-all.ltl
run 0 $randltl -n5 2 -o test-%L.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 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 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

83
src/ltlvisit/randomltl.cc
View file

@ -404,12 +404,11 @@ namespace spot
update_sums(); update_sums();
} }
void randltlgenerator::randltlgenerator(atomic_prop_set aprops,
randltlgenerator::construct(atomic_prop_set aprops, option_map& opts, const option_map& opts,
char* opt_pL, char* opt_pL,
char* opt_pS, char* opt_pS,
char* opt_pB) char* opt_pB)
{ {
aprops_ = aprops; aprops_ = aprops;
output_ = opts.get("output", OUTPUTLTL); output_ = opts.get("output", OUTPUTLTL);
@ -429,10 +428,10 @@ namespace spot
case OUTPUTLTL: case OUTPUTLTL:
rf_ = new random_ltl(&aprops_); rf_ = new random_ltl(&aprops_);
if (opt_pS) if (opt_pS)
throw std::invalid_argument("Cannot set sere priorities with "\ throw std::invalid_argument("Cannot set sere priorities with "
"LTL output"); "LTL output");
if (opt_pB) if (opt_pB)
throw std::invalid_argument("Cannot set boolean priorities with "\ throw std::invalid_argument("Cannot set boolean priorities with "
"LTL output"); "LTL output");
tok_pL = rf_->parse_options(opt_pL); tok_pL = rf_->parse_options(opt_pL);
break; break;
@ -440,10 +439,10 @@ namespace spot
rf_ = new random_boolean(&aprops_); rf_ = new random_boolean(&aprops_);
tok_pB = rf_->parse_options(opt_pB); tok_pB = rf_->parse_options(opt_pB);
if (opt_pL) if (opt_pL)
throw std::invalid_argument("Cannot set ltl priorities with "\ throw std::invalid_argument("Cannot set ltl priorities with "
"Boolean output"); "Boolean output");
if (opt_pS) if (opt_pS)
throw std::invalid_argument("Cannot set sere priorities "\ throw std::invalid_argument("Cannot set sere priorities "
"with Boolean output"); "with Boolean output");
break; break;
case OUTPUTSERE: case OUTPUTSERE:
@ -451,7 +450,7 @@ namespace spot
tok_pS = rs_->parse_options(opt_pS); tok_pS = rs_->parse_options(opt_pS);
tok_pB = rs_->rb.parse_options(opt_pB); tok_pB = rs_->rb.parse_options(opt_pB);
if (opt_pL) if (opt_pL)
throw std::invalid_argument("Cannot set ltl priorities "\ throw std::invalid_argument("Cannot set ltl priorities "
"with SERE output"); "with SERE output");
break; break;
case OUTPUTPSL: case OUTPUTPSL:
@ -464,47 +463,30 @@ namespace spot
} }
if (tok_pL) 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) 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) if (tok_pB)
throw("failed to parse Boolean priorities near " throw std::invalid_argument("failed to parse Boolean priorities near "
+ std::string(tok_pB)); + std::string(tok_pB));
spot::srand(opt_seed_); spot::srand(opt_seed_);
ltl_simplifier_options simpl_opts(opt_simpl_level_); ltl_simplifier_options simpl_opts(opt_simpl_level_);
ltl_simplifier simpl_(simpl_opts); 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_pL,
char* opt_pS, char* opt_pS,
char* opt_pB) char* opt_pB)
{ : randltlgenerator(create_atomic_prop_set(aprops_n), opts,
atomic_prop_set aprops_; opt_pL, opt_pS, opt_pB)
default_environment& e =
default_environment::instance();
for (int i = 0; i < aprops_n; ++i)
{
std::ostringstream p;
p << 'p' << i;
aprops_.insert(static_cast<const atomic_prop*>
(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)
{ {
construct(aprops, opts, opt_pL, opt_pS, opt_pB);
} }
randltlgenerator::~randltlgenerator() randltlgenerator::~randltlgenerator()
{ {
delete rf_; delete rf_;
@ -512,6 +494,7 @@ namespace spot
for (auto i: unique_set_) for (auto i: unique_set_)
i->destroy(); i->destroy();
} }
const formula* randltlgenerator::next() const formula* randltlgenerator::next()
{ {
unsigned trials = MAX_TRIALS; unsigned trials = MAX_TRIALS;
@ -593,32 +576,32 @@ namespace spot
void void
randltlgenerator::dump_ltl_priorities(std::ostream& os) randltlgenerator::dump_ltl_priorities(std::ostream& os)
{ {
rf_->dump_priorities(os); rf_->dump_priorities(os);
} }
void void
randltlgenerator::dump_bool_priorities(std::ostream& os) randltlgenerator::dump_bool_priorities(std::ostream& os)
{ {
rf_->dump_priorities(os); rf_->dump_priorities(os);
} }
void void
randltlgenerator::dump_psl_priorities(std::ostream& os) randltlgenerator::dump_psl_priorities(std::ostream& os)
{ {
rp_->dump_priorities(os); rp_->dump_priorities(os);
} }
void void
randltlgenerator::dump_sere_priorities(std::ostream& os) randltlgenerator::dump_sere_priorities(std::ostream& os)
{ {
rs_->dump_priorities(os); rs_->dump_priorities(os);
} }
void void
randltlgenerator::dump_sere_bool_priorities(std::ostream& os) randltlgenerator::dump_sere_bool_priorities(std::ostream& os)
{ {
rs_->rb.dump_priorities(os); rs_->rb.dump_priorities(os);
} }
} }
} }

21
src/ltlvisit/randomltl.hh
View file

@ -1,6 +1,6 @@
// -*- coding: utf-8 -*- // -*- coding: utf-8 -*-
// Copyright (C) 2010, 2011, 2012, 2013, 2014 Laboratoire de Recherche // Copyright (C) 2010, 2011, 2012, 2013, 2014, 2015 Laboratoire de
// et Développement de l'Epita (LRDE). // Recherche et Développement de l'Epita (LRDE).
// Copyright (C) 2005 Laboratoire d'Informatique de Paris 6 (LIP6), // Copyright (C) 2005 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre // département Systèmes Répartis Coopératifs (SRC), Université Pierre
// et Marie Curie. // et Marie Curie.
@ -310,40 +310,31 @@ namespace spot
const spot::ptr_hash<const spot::ltl::formula>> fset_t; const spot::ptr_hash<const spot::ltl::formula>> fset_t;
public: public:
randltlgenerator(int aprops_n, option_map& opts, randltlgenerator(int aprops_n, const option_map& opts,
char* opt_pL = nullptr, char* opt_pL = nullptr,
char* opt_pS = nullptr, char* opt_pS = nullptr,
char* opt_pB = 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_pL = nullptr,
char* opt_pS = nullptr, char* opt_pS = nullptr,
char* opt_pB = nullptr); char* opt_pB = nullptr);
void construct(atomic_prop_set aprops, option_map& opts,
char* opt_pL, char* opt_pS,
char* opt_pB);
~randltlgenerator(); ~randltlgenerator();
const spot::ltl::formula* next(); const spot::ltl::formula* next();
void dump_ltl_priorities(std::ostream& os); void dump_ltl_priorities(std::ostream& os);
void dump_bool_priorities(std::ostream& os); void dump_bool_priorities(std::ostream& os);
void dump_psl_priorities(std::ostream& os); void dump_psl_priorities(std::ostream& os);
void dump_sere_priorities(std::ostream& os); void dump_sere_priorities(std::ostream& os);
void dump_sere_bool_priorities(std::ostream& os); void dump_sere_bool_priorities(std::ostream& os);
void remove_some_props(atomic_prop_set& s); void remove_some_props(atomic_prop_set& s);
const formula* GF_n(); const formula* GF_n();
private: private:
fset_t unique_set_; fset_t unique_set_;
atomic_prop_set aprops_; atomic_prop_set aprops_;