Commit cce6dd34 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

Add random generators of Boolean, SERE, and PSL formula.

* src/ltlvisit/randomltl.cc, src/ltlvisit/randomltl.hh:
(random_boolean, random_sere, random_psl): Add new classes.
* src/ltltest/randltl.cc: Add options to support the above.
Nore: the -p option was renamed to -pL for consistency, but
it is still understood.
parent cc889a7f
// Copyright (C) 2008, 2009 Laboratoire de Recherche et Développement
// Copyright (C) 2008, 2009, 2011 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
// Copyright (C) 2003, 2005 Laboratoire d'Informatique de
// Paris 6 (LIP6), dpartement Systmes Rpartis Coopratifs (SRC),
......@@ -39,14 +39,22 @@ void
syntax(char* prog)
{
std::cerr << "Usage: "<< prog << " [OPTIONS...] PROPS..." << std::endl
<< std::endl
<< "Output selection:" << std::endl
<< " -B generate Boolean formulae" << std::endl
<< " -L generate LTL formulae [default]" << std::endl
<< " -S generate SERE" << std::endl
<< " -P generate PSL formulae" << std::endl
<< std::endl
<< "Options:" << std::endl
<< " -d dump priorities, do not generate any formula"
<< std::endl
<< " -f N the size of the formula [15]" << std::endl
<< " -F N number of formulae to generate [1]" << std::endl
<< " -p S priorities to use" << std::endl
<< " -r N simplify formulae using all available reductions"
<< " -f N the size of the formula [15]" << std::endl
<< " -F N number of formulae to generate [1]" << std::endl
<< " -pL S priorities to use for LTL formula" << std::endl
<< " -pS S priorities to use for SERE" << std::endl
<< " -pB S priorities to use for Boolean formulae" << std::endl
<< " -r N simplify formulae using all available reductions"
<< " and reject those" << std::endl
<< " strictly smaller than N" << std::endl
<< " -u generate unique formulae"
......@@ -79,11 +87,14 @@ to_int(const char* s)
int
main(int argc, char** argv)
{
enum { OutputBool, OutputLTL, OutputSERE, OutputPSL } output = OutputLTL;
bool opt_d = false;
int opt_s = 0;
int opt_f = 15;
int opt_F = 1;
char* opt_p = 0;
char* opt_pL = 0;
char* opt_pS = 0;
char* opt_pB = 0;
int opt_r = 0;
bool opt_u = false;
......@@ -97,7 +108,11 @@ main(int argc, char** argv)
while (++argn < argc)
{
if (!strcmp(argv[argn], "-d"))
if (!strcmp(argv[argn], "-B"))
{
output = OutputBool;
}
else if (!strcmp(argv[argn], "-d"))
{
opt_d = true;
}
......@@ -113,11 +128,31 @@ main(int argc, char** argv)
syntax(argv[0]);
opt_F = to_int(argv[++argn]);
}
else if (!strcmp(argv[argn], "-p"))
else if (!strcmp(argv[argn], "-L"))
{
output = OutputLTL;
}
else if ((!strcmp(argv[argn], "-p")) || (!strcmp(argv[argn], "-pL")))
{
if (argc < argn + 2)
syntax(argv[0]);
opt_pL = argv[++argn];
}
else if (!strcmp(argv[argn], "-pS"))
{
if (argc < argn + 2)
syntax(argv[0]);
opt_pS = argv[++argn];
}
else if (!strcmp(argv[argn], "-pB"))
{
if (argc < argn + 2)
syntax(argv[0]);
opt_p = argv[++argn];
opt_pB = argv[++argn];
}
else if (!strcmp(argv[argn], "-P"))
{
output = OutputPSL;
}
else if (!strcmp(argv[argn], "-r"))
{
......@@ -131,6 +166,10 @@ main(int argc, char** argv)
syntax(argv[0]);
opt_s = to_int(argv[++argn]);
}
else if (!strcmp(argv[argn], "-S"))
{
output = OutputSERE;
}
else if (!strcmp(argv[argn], "-u"))
{
opt_u = true;
......@@ -142,14 +181,79 @@ main(int argc, char** argv)
}
}
spot::ltl::random_ltl rl(ap);
const char* tok = rl.parse_options(opt_p);
if (tok)
spot::ltl::random_formula* rf = 0;
spot::ltl::random_psl* rp = 0;
spot::ltl::random_sere* rs = 0;
const char* tok_pL = 0;
const char* tok_pS = 0;
const char* tok_pB = 0;
switch (output)
{
case OutputLTL:
rf = new spot::ltl::random_ltl(ap);
tok_pL = rf->parse_options(opt_pL);
if (opt_pS)
{
std::cerr << "option -pS unsupported for LTL output" << std::endl;
exit(2);
}
if (opt_pB)
{
std::cerr << "option -pB unsupported for LTL output" << std::endl;
exit(2);
}
break;
case OutputBool:
rf = new spot::ltl::random_boolean(ap);
tok_pB = rf->parse_options(opt_pB);
if (opt_pL)
{
std::cerr << "option -pL unsupported for Boolean output" << std::endl;
exit(2);
}
if (opt_pS)
{
std::cerr << "option -pS unsupported for Boolean output" << std::endl;
exit(2);
}
break;
case OutputSERE:
rf = rs = new spot::ltl::random_sere(ap);
tok_pS = rf->parse_options(opt_pS);
if (opt_pL)
{
std::cerr << "option -pL unsupported for SERE output" << std::endl;
exit(2);
}
break;
case OutputPSL:
rf = rp = new spot::ltl::random_psl(ap);
rs = &rp->rs;
tok_pL = rp->parse_options(opt_pL);
tok_pS = rs->parse_options(opt_pS);
tok_pB = rs->rb.parse_options(opt_pB);
break;
}
if (tok_pL)
{
std::cerr << "failed to parse probabilities near `"
<< tok << "'" << std::endl;
std::cerr << "failed to parse priorities (option -pL) near `"
<< tok_pL << "'" << std::endl;
exit(2);
}
if (tok_pS)
{
std::cerr << "failed to parse priorities (option -pS) near `"
<< tok_pS << "'" << std::endl;
exit(2);
}
if (tok_pB)
{
std::cerr << "failed to parse priorities (option -pB) near `"
<< tok_pB << "'" << std::endl;
exit(2);
}
if (opt_r > opt_f)
{
......@@ -160,7 +264,32 @@ main(int argc, char** argv)
if (opt_d)
{
rl.dump_priorities(std::cout);
switch (output)
{
case OutputLTL:
std::cout << "Use option -pL to set the following LTL priorities:"
<< std::endl;
rf->dump_priorities(std::cout);
break;
case OutputBool:
std::cout << "Use option -pB to set the following Boolean "
<< "formula priorities:" << std::endl;
rf->dump_priorities(std::cout);
break;
case OutputPSL:
std::cout << "Use option -pL to set the following LTL priorities:"
<< std::endl;
rp->dump_priorities(std::cout);
// Fall through.
case OutputSERE:
std::cout << "Use option -pS to set the following SERE priorities:"
<< std::endl;
rs->dump_priorities(std::cout);
std::cout << "Use option -pB to set the following Boolean "
<< "formula priorities:" << std::endl;
rs->rb.dump_priorities(std::cout);
break;
}
}
else
{
......@@ -176,7 +305,7 @@ main(int argc, char** argv)
int max_tries_r = 1000;
while (max_tries_r--)
{
f = rl.generate(opt_f);
f = rf->generate(opt_f);
if (opt_r)
{
spot::ltl::formula* g = reduce(f);
......@@ -201,7 +330,8 @@ main(int argc, char** argv)
<< "of size " << opt_r << " or more." << std::endl;
exit(2);
}
std::string txt = spot::ltl::to_string(f);
std::string txt = spot::ltl::to_string(f, false,
output == OutputSERE);
f->destroy();
if (!opt_u || unique.insert(txt).second)
{
......@@ -219,6 +349,8 @@ main(int argc, char** argv)
}
}
delete rf;
spot::ltl::atomic_prop_set::const_iterator i = ap->begin();
while (i != ap->end())
{
......
......@@ -35,7 +35,7 @@ namespace spot
{
namespace
{
formula*
static formula*
ap_builder(const random_formula* rl, int n)
{
assert(n == 1);
......@@ -45,7 +45,7 @@ namespace spot
return (*i)->clone();
}
formula*
static formula*
true_builder(const random_formula*, int n)
{
assert(n == 1);
......@@ -53,7 +53,15 @@ namespace spot
return constant::true_instance();
}
formula*
static formula*
boolform_builder(const random_formula* rl, int n)
{
assert(n >= 1);
const random_sere* rs = static_cast<const random_sere*>(rl);
return rs->rb.generate(n);
}
static formula*
false_builder(const random_formula*, int n)
{
assert(n == 1);
......@@ -61,16 +69,32 @@ namespace spot
return constant::false_instance();
}
static formula*
eword_builder(const random_formula*, int n)
{
assert(n == 1);
(void) n;
return constant::empty_word_instance();
}
template <unop::type Op>
formula*
static formula*
unop_builder(const random_formula* rl, int n)
{
assert(n >= 2);
return unop::instance(Op, rl->generate(n - 1));
}
static formula*
closure_builder(const random_formula* rl, int n)
{
assert(n >= 2);
const random_psl* rp = static_cast<const random_psl*>(rl);
return unop::instance(unop::Closure, rp->rs.generate(n - 1));
}
template <binop::type Op>
formula*
static formula*
binop_builder(const random_formula* rl, int n)
{
assert(n >= 3);
......@@ -79,8 +103,49 @@ namespace spot
return binop::instance(Op, rl->generate(l), rl->generate(n - l));
}
template <binop::type Op>
static formula*
binop_SERELTL_builder(const random_formula* rl, int n)
{
assert(n >= 3);
--n;
const random_psl* rp = static_cast<const random_psl*>(rl);
int l = rrand(1, n - 1);
return binop::instance(Op, rp->rs.generate(l), rl->generate(n - l));
}
template <bunop::type Op>
static formula*
bunop_unbounded_builder(const random_formula* rl, int n)
{
assert(n >= 2);
return bunop::instance(Op, rl->generate(n - 1));
}
template <bunop::type Op>
static formula*
bunop_bounded_builder(const random_formula* rl, int n)
{
assert(n >= 2);
int min = rrand(0, 3);
int max = rrand(min, 4);
return bunop::instance(Op, rl->generate(n - 1), min, max);
}
template <bunop::type Op>
static formula*
bunop_bool_bounded_builder(const random_formula* rl, int n)
{
assert(n >= 2);
int min = rrand(0, 3);
int max = rrand(min, 4);
const random_sere* rp = static_cast<const random_sere*>(rl);
return bunop::instance(Op, rp->rb.generate(n - 1), min, max);
}
template <multop::type Op>
formula*
static formula*
multop_builder(const random_formula* rl, int n)
{
assert(n >= 3);
......@@ -109,15 +174,24 @@ namespace spot
for (unsigned i = 0; i < proba_size_; ++i)
{
if (proba_[i].min_n == 1)
total_1_ += proba_[i].proba;
{
total_1_ += proba_[i].proba;
if (proba_ + i >= proba_2_)
total_2_ += proba_[i].proba;;
if (proba_ + i >= proba_2_or_more_)
total_2_and_more_ += proba_[i].proba;
}
else if (proba_[i].min_n == 2)
total_2_ += proba_[i].proba;
{
total_2_ += proba_[i].proba;
if (proba_ + i >= proba_2_or_more_)
total_2_and_more_ += proba_[i].proba;
}
else if (proba_[i].min_n > 2)
total_2_and_more_ += proba_[i].proba;
else
assert(!"unexpected max_n");
}
total_2_and_more_ += total_2_;
assert(total_1_ != 0.0);
assert(total_2_ != 0.0);
assert(total_2_and_more_ != 0.0);
......@@ -127,45 +201,34 @@ namespace spot
random_formula::generate(int n) const
{
assert(n > 0);
double r = drand();
op_proba* p;
if (n == 1)
{
double r = drand() * total_1_;
op_proba* p = proba_;
double s = p->proba;
while (s < r)
{
++p;
s += p->proba;
}
assert(p->min_n == 1);
return p->build(this, n);
r *= total_1_;
p = proba_;
}
else if (n == 2)
{
double r = drand() * total_2_;
op_proba* p = proba_2_;
double s = p->proba;
while (s < r)
{
++p;
s += p->proba;
}
assert(p->min_n == 2);
return p->build(this, n);
r *= total_2_;
p = proba_2_;
}
else
{
double r = drand() * total_2_and_more_;
op_proba* p = proba_2_;
double s = p->proba;
while (s < r)
{
++p;
s += p->proba;
}
assert(p->min_n >= 2);
return p->build(this, n);
r *= total_2_and_more_;
p = proba_2_or_more_;
}
double s = p->proba;
while (s < r)
{
++p;
s += p->proba;
}
return p->build(this, n);
}
const char*
......@@ -211,15 +274,55 @@ namespace spot
return os;
}
// LTL formulae
// SEREs
random_sere::random_sere(const atomic_prop_set* ap)
: random_formula(11, ap), rb(ap)
{
proba_[0].setup("eword", 1, eword_builder);
proba_2_ = proba_ + 1;
proba_2_or_more_ = proba_ + 1;
proba_[1].setup("boolform", 1, boolform_builder);
proba_[2].setup("star", 2, bunop_unbounded_builder<bunop::Star>);
proba_[3].setup("star_b", 2, bunop_bounded_builder<bunop::Star>);
proba_[4].setup("equal_b", 2, bunop_bool_bounded_builder<bunop::Equal>);
proba_[5].setup("goto_b", 2, bunop_bool_bounded_builder<bunop::Goto>);
proba_[6].setup("and", 3, multop_builder<multop::And>);
proba_[7].setup("andNLM", 3, multop_builder<multop::AndNLM>);
proba_[8].setup("or", 3, multop_builder<multop::Or>);
proba_[9].setup("concat", 3, multop_builder<multop::Concat>);
proba_[10].setup("fusion", 3, multop_builder<multop::Fusion>);
random_ltl::random_ltl(const atomic_prop_set* ap)
: random_formula(16, ap)
update_sums();
}
// Boolean formulae
random_boolean::random_boolean(const atomic_prop_set* ap)
: random_formula(9, ap)
{
proba_[0].setup("ap", 1, ap_builder);
proba_[0].proba = ap_->size();
proba_[1].setup("false", 1, false_builder);
proba_[2].setup("true", 1, true_builder);
proba_2_or_more_ = proba_2_ = proba_ + 3;
proba_[3].setup("not", 2, unop_builder<unop::Not>);
proba_[4].setup("equiv", 3, binop_builder<binop::Equiv>);
proba_[5].setup("implies", 3, binop_builder<binop::Implies>);
proba_[6].setup("xor", 3, binop_builder<binop::Xor>);
proba_[7].setup("and", 3, multop_builder<multop::And>);
proba_[8].setup("or", 3, multop_builder<multop::Or>);
update_sums();
}
// LTL formulae
void
random_ltl::setup_proba_()
{
proba_[0].setup("ap", 1, ap_builder);
proba_[0].proba = ap_->size();
proba_[1].setup("false", 1, false_builder);
proba_[2].setup("true", 1, true_builder);
proba_2_ = proba_ + 3;
proba_2_or_more_ = proba_2_ = proba_ + 3;
proba_[3].setup("not", 2, unop_builder<unop::Not>);
proba_[4].setup("F", 2, unop_builder<unop::F>);
proba_[5].setup("G", 2, unop_builder<unop::G>);
......@@ -233,10 +336,36 @@ namespace spot
proba_[13].setup("M", 3, binop_builder<binop::M>);
proba_[14].setup("and", 3, multop_builder<multop::And>);
proba_[15].setup("or", 3, multop_builder<multop::Or>);
}
proba_[0].proba = ap_->size();
random_ltl::random_ltl(const atomic_prop_set* ap)
: random_formula(16, ap)
{
setup_proba_();
update_sums();
}
random_ltl::random_ltl(int size, const atomic_prop_set* ap)
: random_formula(size, ap)
{
setup_proba_();
// No call to update_sums(), this functions is always
// called by the random_psl constructor.
}
// PSL
random_psl::random_psl(const atomic_prop_set* ap)
: random_ltl(19, ap), rs(ap)
{
// FIXME: This looks very fragile.
memmove(proba_ + 8, proba_ + 7,
((proba_ + 16) - (proba_ + 7)) * sizeof(*proba_));
proba_[7].setup("Closure", 2, closure_builder);
proba_[17].setup("EConcat", 3, binop_SERELTL_builder<binop::EConcat>);
proba_[18].setup("UConcat", 3, binop_SERELTL_builder<binop::UConcat>);
update_sums();
}
} // ltl
} // spot
......@@ -45,7 +45,7 @@ namespace spot
~random_formula()
{
delete proba_;
delete[] proba_;
}
/// Return the set of atomic proposition used to build formulae.
......@@ -69,9 +69,6 @@ namespace spot
/// \brief Update the priorities used to generate the formulae.
///
/// The initial priorities are defined in each sub class as follows.
///
/// These priorities can be altered using this function.
/// \a options should be comma-separated list of KEY=VALUE
/// assignments, using keys from the above list.
/// For instance <code>"xor=0, F=3"</code> will prevent \c xor
......@@ -96,6 +93,7 @@ namespace spot
double total_1_;
op_proba* proba_2_;
double total_2_;
op_proba* proba_2_or_more_;
double total_2_and_more_;
const atomic_prop_set* ap_;
};
......@@ -104,10 +102,10 @@ namespace spot
/// \brief Generate random LTL formulae.
/// \ingroup ltl_io
///
/// This class recursively construct LTL formulae of a given size.
/// The formulae will use the use atomic propositions from the
/// set of proposition passed to the constructor, in addition to the
/// constant and all LTL operators supported by Spot.
/// This class recursively constructs LTL formulae of a given
/// size. The formulae will use the use atomic propositions from
/// the set of propositions passed to the constructor, in addition
/// to the constant and all LTL operators supported by Spot.
///
/// By default each operator has equal chance to be selected.
/// Also, each atomic proposition has as much chance as each
......@@ -148,7 +146,155 @@ namespace spot
///
/// These priorities can be changed use the parse_options method.
random_ltl(const atomic_prop_set* ap);
protected:
void setup_proba_();
random_ltl(int size, const atomic_prop_set* ap);
};
/// \brief Generate random Boolean formulae.
/// \ingroup ltl_io
///
/// This class recursively constructs Boolean formulae of a given size.
/// The formulae will use the use atomic propositions from the
/// set of propositions passed to the constructor, in addition to the
/// constant and all Boolean operators supported by Spot.
///
/// By default each operator has equal chance to be selected.
class random_boolean: public random_formula
{