From 649e8e2def87173a5f05e5b46ddbd86cd098c8b5 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 7 Sep 2012 14:24:06 +0200 Subject: [PATCH] Kill src/ltltest/randltl and replace it by src/bin/randltl. * src/ltltest/randltl.cc: Delete. * src/ltltest/Makefile.am (noinst_PROGRAMS, randltl_SOURCES): Remove. * src/ltltest/reduc.test, src/ltltest/reducpsl.test, src/ltltest/utf8.test, src/tgbatest/randpsl.test, bench/emptchk/README: Adjust to use bin/randltl. --- bench/emptchk/README | 2 +- src/ltltest/Makefile.am | 4 - src/ltltest/randltl.cc | 429 -------------------------------------- src/ltltest/reduc.test | 10 +- src/ltltest/reducpsl.test | 8 +- src/ltltest/utf8.test | 4 +- src/tgbatest/randpsl.test | 8 +- 7 files changed, 20 insertions(+), 445 deletions(-) delete mode 100644 src/ltltest/randltl.cc diff --git a/bench/emptchk/README b/bench/emptchk/README index 66baf0633..4ffd68ee3 100644 --- a/bench/emptchk/README +++ b/bench/emptchk/README @@ -276,4 +276,4 @@ This directory contains: http://spot.lip6.fr/wiki/EmptinessCheckOptions) Besides randtgba, two other tools that you might find handy we - experimenting are src/ltltest/randltl and src/tgbatest/ltl2tgba. + experimenting are src/bin/randltl and src/tgbatest/ltl2tgba. diff --git a/src/ltltest/Makefile.am b/src/ltltest/Makefile.am index bb75c4121..6cefb7b49 100644 --- a/src/ltltest/Makefile.am +++ b/src/ltltest/Makefile.am @@ -45,9 +45,6 @@ check_PROGRAMS = \ tunabbrev \ tunenoform -noinst_PROGRAMS = \ - randltl - consterm_SOURCES = consterm.cc equals_SOURCES = equals.cc kind_SOURCES = kind.cc @@ -59,7 +56,6 @@ lunabbrev_SOURCES = equals.cc lunabbrev_CPPFLAGS = $(AM_CPPFLAGS) -DLUNABBREV nenoform_SOURCES = equals.cc nenoform_CPPFLAGS = $(AM_CPPFLAGS) -DNENOFORM -randltl_SOURCES = randltl.cc reduc_SOURCES = reduc.cc reduccmp_SOURCES = equals.cc reduccmp_CPPFLAGS = $(AM_CPPFLAGS) -DREDUC diff --git a/src/ltltest/randltl.cc b/src/ltltest/randltl.cc deleted file mode 100644 index 130684c8f..000000000 --- a/src/ltltest/randltl.cc +++ /dev/null @@ -1,429 +0,0 @@ -// -*- coding: utf-8 -*- -// Copyright (C) 2008, 2009, 2011, 2012 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), -// Université Pierre et Marie Curie. -// -// This file is part of Spot, a model checking library. -// -// Spot is free software; you can redistribute it and/or modify it -// under the terms of the GNU General Public License as published by -// the Free Software Foundation; either version 2 of the License, or -// (at your option) any later version. -// -// Spot is distributed in the hope that it will be useful, but WITHOUT -// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY -// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public -// License for more details. -// -// You should have received a copy of the GNU General Public License -// along with Spot; see the file COPYING. If not, write to the Free -// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA -// 02111-1307, USA. - -#include -#include -#include -#include -#include -#include -#include -#include "ltlast/atomic_prop.hh" -#include "ltlvisit/randomltl.hh" -#include "ltlvisit/tostring.hh" -#include "ltlvisit/length.hh" -#include "ltlvisit/simplify.hh" -#include "ltlenv/defaultenv.hh" -#include "misc/random.hh" - -#include "ltlast/allnodes.hh" - - -using namespace spot; -using namespace spot::ltl; - -environment& env(default_environment::instance()); - -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 - << " -8 output in UTF-8" << 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 - << " -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" - << std::endl - << " -s N seed for the random number generator" << std::endl - << " -wf append weak fairness conditions to all formulae\n" - << std::endl - << "Where:" << std::endl - << " F are floating values" << std::endl - << " S are `KEY=F, KEY=F, ...' strings" << std::endl - << " N are positive integers" << std::endl - << " PROPS are the atomic properties to use on transitions" - << std::endl - << "Use -d to see the list of KEYs." << std::endl; - exit(2); -} - -int -to_int(const char* s) -{ - char* endptr; - int res = strtol(s, &endptr, 10); - if (*endptr) - { - std::cerr << "Failed to parse `" << s << "' as an integer." << std::endl; - exit(1); - } - return res; -} - - -// GF(p_1) & GF(p_2) & ... & GF(p_n) -const formula* GF_n(spot::ltl::atomic_prop_set* ap) -{ - const formula* result = 0; - spot::ltl::atomic_prop_set::const_iterator i = ap->begin(); - while (i != ap->end()) - { - std::ostringstream p; - p << (*i)->name(); - ++i; - const formula* f = - unop::instance(unop::G, - unop::instance(unop::F, - env.require(p.str()))); - if (result) - result = multop::instance(multop::And, f, result); - else - result = f; - } - return result; -} - - -int -main(int argc, char** argv) -{ - enum { OutputBool, OutputLTL, OutputSERE, OutputPSL } output = OutputLTL; - bool opt_d = false; - bool utf8 = false; - int opt_s = 0; - int opt_f = 15; - int opt_F = 1; - char* opt_pL = 0; - char* opt_pS = 0; - char* opt_pB = 0; - int opt_r = 0; - bool opt_u = false; - spot::ltl::ltl_simplifier_options simpopt(true, true, true, true, true); - spot::ltl::ltl_simplifier simp(simpopt); - bool opt_wfair = false; - - spot::ltl::environment& env(spot::ltl::default_environment::instance()); - spot::ltl::atomic_prop_set* ap = new spot::ltl::atomic_prop_set; - - int argn = 0; - - if (argc <= 1) - syntax(argv[0]); - - while (++argn < argc) - { - if (!strcmp(argv[argn], "-8")) - { - utf8 = true; - } - else if (!strcmp(argv[argn], "-B")) - { - output = OutputBool; - } - else if (!strcmp(argv[argn], "-d")) - { - opt_d = true; - } - else if (!strcmp(argv[argn], "-f")) - { - if (argc < argn + 2) - syntax(argv[0]); - opt_f = to_int(argv[++argn]); - } - else if (!strcmp(argv[argn], "-F")) - { - if (argc < argn + 2) - syntax(argv[0]); - opt_F = to_int(argv[++argn]); - } - 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_pB = argv[++argn]; - } - else if (!strcmp(argv[argn], "-P")) - { - output = OutputPSL; - } - else if (!strcmp(argv[argn], "-r")) - { - if (argc < argn + 2) - syntax(argv[0]); - opt_r = to_int(argv[++argn]); - } - else if (!strcmp(argv[argn], "-s")) - { - if (argc < argn + 2) - 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; - } - else if (!strcmp(argv[argn], "-wf")) - { - opt_wfair = true; - } - else - { - ap->insert(static_cast - (env.require(argv[argn]))); - } - } - - 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 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) - { - std::cerr << "-r's argument (" << opt_r << ") should not be larger than " - << "-f's (" << opt_f << ")" << std::endl; - exit(2); - } - - if (opt_d) - { - 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 - { - std::set unique; - - while (opt_F--) - { - int max_tries_u = 1000; - while (max_tries_u--) - { - spot::srand(opt_s++); - const spot::ltl::formula* f = 0; - int max_tries_r = 1000; - while (max_tries_r--) - { - f = rf->generate(opt_f); - if (opt_r) - { - const spot::ltl::formula* g = simp.simplify(f); - f->destroy(); - if (spot::ltl::length(g) < opt_r) - { - g->destroy(); - continue; - } - f = g; - } - else - { - assert(spot::ltl::length_boolone(f) <= opt_f); - - // We might have a formula bigger than opt_f - // because {e}[]->f of length 3 gets trivially reduced - // to f|!e of length 4. - if (spot::ltl::length(f) > opt_f) - { - f->destroy(); - continue; - } - } - - if (opt_wfair) - { - const spot::ltl::formula* g = - GF_n(atomic_prop_collect(f, 0)); - f = spot::ltl::unop::instance(unop::Not, - spot::ltl::binop::instance(binop::Implies, g, f)); - } - - break; - } - if (max_tries_r < 0) - { - assert(opt_r); - std::cerr << "Failed to generate non-reducible formula " - << "of size " << opt_r << " or more." << std::endl; - exit(2); - } - std::string txt = utf8 - ? spot::ltl::to_utf8_string(f, false, output == OutputSERE) - : spot::ltl::to_string(f, false, output == OutputSERE); - f->destroy(); - if (!opt_u || unique.insert(txt).second) - { - std::cout << txt << std::endl; - break; - } - } - if (max_tries_u < 0) - { - assert(opt_u); - std::cerr << "Failed to generate another unique formula." - << std::endl; - exit(2); - } - } - } - - delete rf; - - spot::ltl::atomic_prop_set::const_iterator i = ap->begin(); - while (i != ap->end()) - { - spot::ltl::atomic_prop_set::const_iterator j = i; - ++i; - (*j)->destroy(); - } - delete ap; -} diff --git a/src/ltltest/reduc.test b/src/ltltest/reduc.test index db356eaee..75a51eecc 100755 --- a/src/ltltest/reduc.test +++ b/src/ltltest/reduc.test @@ -1,6 +1,6 @@ #! /bin/sh -# Copyright (C) 2009, 2010 Laboratoire de Recherche et Développement de -# l'Epita (LRDE). +# Copyright (C) 2009, 2010, 2012 Laboratoire de Recherche et +# Développement de l'Epita (LRDE). # Copyright (C) 2004, 2005, 2006 Laboratoire d'Informatique de Paris 6 # (LIP6), département Systèmes Répartis Coopératifs (SRC), Université # Pierre et Marie Curie. @@ -28,12 +28,14 @@ set -e +randltl=../../bin/randltl + FILE=formulae : > $FILE # for i in 10 11 12 13 14 15 16 17 18 19 20; do for i in 10 12 14 16 18 20; do - run 0 ../randltl -u -s 0 -f $i a b c -F 100 >> $FILE - run 0 ../randltl -u -s 100 -f $i a b c d e f -F 100 >> $FILE + run 0 $randltl --seed 0 --tree-size $i a b c -n 100 >> $FILE + run 0 $randltl --seed 100 --tree-size $i a b c d e f -n 100 >> $FILE done for opt in 0 1 2 3 7; do diff --git a/src/ltltest/reducpsl.test b/src/ltltest/reducpsl.test index aff0c6b77..df0b6a1e4 100755 --- a/src/ltltest/reducpsl.test +++ b/src/ltltest/reducpsl.test @@ -1,5 +1,5 @@ #! /bin/sh -# Copyright (C) 2011 Laboratoire de Recherche et Développement de +# Copyright (C) 2011, 2012 Laboratoire de Recherche et Développement de # l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -25,11 +25,13 @@ set -e +randltl=../../bin/randltl + FILE=formulae : > $FILE for i in 10 12 14 16 18 20; do - run 0 ../randltl -P -u -s 0 -f $i a b c -F 100 >> $FILE - run 0 ../randltl -P -u -s 100 -f $i a b c d e f -F 100 >> $FILE + run 0 $randltl --psl --seed 0 --tree-size $i a b c -n 100 >> $FILE + run 0 $randltl --psl --seed 100 --tree-size $i a b c d e f -n 100 >> $FILE done for opt in 0 1 2 3 7; do diff --git a/src/ltltest/utf8.test b/src/ltltest/utf8.test index 3527f10bd..092a2a12a 100755 --- a/src/ltltest/utf8.test +++ b/src/ltltest/utf8.test @@ -72,5 +72,5 @@ EOF cmp exp err -../randltl -P -8 -u -s 0 -f 16 a b c -F 100 > formulae -../reduc -f -h 0 formulae \ No newline at end of file +../../bin/randltl --psl -8 --seed 0 --tree-size 16 a b c -n 100 > formulae +../reduc -f -h 0 formulae diff --git a/src/tgbatest/randpsl.test b/src/tgbatest/randpsl.test index ee465ee72..3ea757a2a 100755 --- a/src/tgbatest/randpsl.test +++ b/src/tgbatest/randpsl.test @@ -1,5 +1,5 @@ #!/bin/sh -# Copyright (C) 2011 Laboratoire de Recherche et Développement +# Copyright (C) 2011, 2012 Laboratoire de Recherche et Développement # de l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -36,7 +36,11 @@ check_psl() ../ltl2tgba -f -x -R3 -Pout.tgba -E "!($1)" } -../../ltltest/randltl -F 50 -f 30 -r 12 -u -s 0 -P a b c | +# Generate 50 random unique PSL formula that do not simplify to LTL +# formulae, and that have a size of at lease 12. +../../bin/randltl -n -1 --tree-size 30 --seed 0 --psl a b c | +../../bin/ltlfilt -r --size-min 12 --unique | +../../bin/ltlfilt -v --ltl | head -n 50 | while read formula; do check_psl "$formula" done