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.
This commit is contained in:
Alexandre Duret-Lutz
parent
565e25502c
commit
fc0ed01a45
6 changed files with 33 additions and 37 deletions
|
|
@ -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
|
||||
{
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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);
|
||||
|
|
|
|||
|
|
@ -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 <spot/misc/hash.hh>
|
||||
#include <spot/tl/simplify.hh>
|
||||
|
||||
#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,
|
||||
|
|
|
|||
|
|
@ -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)
|
||||
|
|
|
|||
|
|
@ -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)
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue