From cce6dd34f8210ff06dc3557b5817257c9cbc90aa Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sun, 13 Feb 2011 22:38:29 +0100 Subject: [PATCH] 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. --- src/ltltest/randltl.cc | 166 ++++++++++++++++++++++++++--- src/ltlvisit/randomltl.cc | 219 ++++++++++++++++++++++++++++++-------- src/ltlvisit/randomltl.hh | 162 ++++++++++++++++++++++++++-- 3 files changed, 477 insertions(+), 70 deletions(-) diff --git a/src/ltltest/randltl.cc b/src/ltltest/randltl.cc index cc7a91689..62a89fcba 100644 --- a/src/ltltest/randltl.cc +++ b/src/ltltest/randltl.cc @@ -1,4 +1,4 @@ -// 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), département Systèmes Répartis Coopératifs (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_p = argv[++argn]; + 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_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) { - std::cerr << "failed to parse probabilities near `" - << tok << "'" << std::endl; + 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 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()) { diff --git a/src/ltlvisit/randomltl.cc b/src/ltlvisit/randomltl.cc index 97e5098b4..259e67fa5 100644 --- a/src/ltlvisit/randomltl.cc +++ b/src/ltlvisit/randomltl.cc @@ -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(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 - 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(rl); + return unop::instance(unop::Closure, rp->rs.generate(n - 1)); + } + template - 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 + static formula* + binop_SERELTL_builder(const random_formula* rl, int n) + { + assert(n >= 3); + --n; + const random_psl* rp = static_cast(rl); + int l = rrand(1, n - 1); + return binop::instance(Op, rp->rs.generate(l), rl->generate(n - l)); + } + + template + static formula* + bunop_unbounded_builder(const random_formula* rl, int n) + { + assert(n >= 2); + return bunop::instance(Op, rl->generate(n - 1)); + } + + template + 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 + 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(rl); + return bunop::instance(Op, rp->rb.generate(n - 1), min, max); + } + + template - 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); + proba_[3].setup("star_b", 2, bunop_bounded_builder); + proba_[4].setup("equal_b", 2, bunop_bool_bounded_builder); + proba_[5].setup("goto_b", 2, bunop_bool_bounded_builder); + proba_[6].setup("and", 3, multop_builder); + proba_[7].setup("andNLM", 3, multop_builder); + proba_[8].setup("or", 3, multop_builder); + proba_[9].setup("concat", 3, multop_builder); + proba_[10].setup("fusion", 3, multop_builder); - 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_ = proba_ + 3; + proba_2_or_more_ = proba_2_ = proba_ + 3; + proba_[3].setup("not", 2, unop_builder); + proba_[4].setup("equiv", 3, binop_builder); + proba_[5].setup("implies", 3, binop_builder); + proba_[6].setup("xor", 3, binop_builder); + proba_[7].setup("and", 3, multop_builder); + proba_[8].setup("or", 3, multop_builder); + + 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_or_more_ = proba_2_ = proba_ + 3; proba_[3].setup("not", 2, unop_builder); proba_[4].setup("F", 2, unop_builder); proba_[5].setup("G", 2, unop_builder); @@ -233,10 +336,36 @@ namespace spot proba_[13].setup("M", 3, binop_builder); proba_[14].setup("and", 3, multop_builder); proba_[15].setup("or", 3, multop_builder); + } - 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); + proba_[18].setup("UConcat", 3, binop_SERELTL_builder); + update_sums(); + } + } // ltl } // spot diff --git a/src/ltlvisit/randomltl.hh b/src/ltlvisit/randomltl.hh index 5f34853ac..0c12484fc 100644 --- a/src/ltlvisit/randomltl.hh +++ b/src/ltlvisit/randomltl.hh @@ -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 "xor=0, F=3" 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 + { + public: + /// Create a random Boolean formula generator using atomic + /// propositions from \a ap. + /// + /// The default priorities are defined as follows: + /// + /// \verbatim + /// ap n + /// false 1 + /// true 1 + /// not 1 + /// equiv 1 + /// implies 1 + /// xor 1 + /// and 1 + /// or 1 + /// \endverbatim + /// + /// Where \c n is the number of atomic propositions in the + /// set passed to the constructor. + /// + /// This means that each operator has equal chance to be + /// selected. Also, each atomic proposition has as much chance + /// as each constant (i.e., true and false) to be picked. + /// + /// These priorities can be changed use the parse_options method. + random_boolean(const atomic_prop_set* ap); + }; + + /// \brief Generate random SERE. + /// \ingroup ltl_io + /// + /// This class recursively constructs SERE 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 SERE operators supported by Spot. + /// + /// By default each operator has equal chance to be selected. + class random_sere: public random_formula + { + public: + /// Create a random SERE genere using atomic propositions from \a ap. + /// + /// The default priorities are defined as follows: + /// + /// \verbatim + /// eword 1 + /// boolform 1 + /// star 1 + /// star_b 1 + /// equal_b 1 + /// goto_b 1 + /// and 1 + /// andNLM 1 + /// or 1 + /// concat 1 + /// fusion 1 + /// \endverbatim + /// + /// Where "boolfrom" designates a Boolean formula generated + /// by random_boolean. + /// + /// These priorities can be changed use the parse_options method. + /// + /// In addition, you can set the properties of the Boolean + /// formula generator used to build Boolean subformulae using + /// the parse_options method of the \c rb attribute. + random_sere(const atomic_prop_set* ap); + + random_boolean rb; + }; + + /// \brief Generate random PSL formulae. + /// \ingroup ltl_io + /// + /// This class recursively constructs PSL 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 PSL operators supported by Spot. + class random_psl: public random_ltl + { + public: + /// Create a random PSL generator using atomic propositions from \a ap. + /// + /// PSL formulae are built by combining LTL operators, plus + /// three operators (EConcat, UConcat, Closure) taking a SERE + /// as parameter. + /// + /// The default priorities are defined as follows: + /// + /// \verbatim + /// ap n + /// false 1 + /// true 1 + /// not 1 + /// F 1 + /// G 1 + /// X 1 + /// Closure 1 + /// equiv 1 + /// implies 1 + /// xor 1 + /// R 1 + /// U 1 + /// W 1 + /// M 1 + /// and 1 + /// or 1 + /// EConcat 1 + /// UConcat 1 + /// \endverbatim + /// + /// Where \c n is the number of atomic propositions in the + /// set passed to the constructor. + /// + /// This means that each operator has equal chance to be + /// selected. Also, each atomic proposition has as much chance + /// as each constant (i.e., true and false) to be picked. + /// + /// These priorities can be changed use the parse_options method. + /// + /// In addition, you can set the properties of the SERE generator + /// used to build SERE subformulae using the parse_options method + /// of the \c rs attribute. + random_psl(const atomic_prop_set* ap); + + /// The SERE generator used to generate SERE subformulae. + random_sere rs; + }; + + + } }