From bd414d4d4caec12f05f7d14700a2c39fb009dbf9 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 22 Jan 2015 11:31:20 +0100 Subject: [PATCH] bench/stutter: Update * bench/stutter/stutter_invariance_randomgraph.cc: Update to recent changes. If an algorithm took more that 30s on an average for a set of parameters, avoid running it with more states. Take the density and ap count as parameter. Output all the algorithms on the same line. Add additional statistics about automata. * bench/stutter/stutter_invariance_formulas.cc: Update to recent changes. Output all the algorithms on the same line. Add additional statistics about automata. * bench/stutter/stutter_bench.sh: Use a Makefile to manage concurrency. * bench/stutter/README: Update. --- bench/stutter/README | 8 +- bench/stutter/stutter_bench.sh | 36 +++-- bench/stutter/stutter_invariance_formulas.cc | 44 ++++-- .../stutter/stutter_invariance_randomgraph.cc | 141 ++++++++++++------ 4 files changed, 153 insertions(+), 76 deletions(-) diff --git a/bench/stutter/README b/bench/stutter/README index 1218c61d4..8400d65aa 100644 --- a/bench/stutter/README +++ b/bench/stutter/README @@ -6,10 +6,12 @@ translation time is not included in the measured time. To reproduce the benchmark is to run - % ./stutter_bench.sh + % ./stutter_bench.sh -j8 -to create bench_formulas.csv and bench_randgraph.csv, and then -explore these data the provided ipython notbook +to create bench_formulas.csv and bench_randgraph.csv. +(Adjust -j8 to the number of cores you have.) + +Then explore these data the provided ipython notebook % ipython notebook --pylab=inline stutter.ipynb diff --git a/bench/stutter/stutter_bench.sh b/bench/stutter/stutter_bench.sh index 76d5dc51f..76d180b24 100755 --- a/bench/stutter/stutter_bench.sh +++ b/bench/stutter/stutter_bench.sh @@ -3,15 +3,33 @@ RANDLTL=../../src/bin/randltl LTLFILT=../../src/bin/ltlfilt -OUTPUT=bench_formulas.csv -echo 'formula,algo,ap,states,result,time' > "$OUTPUT" +pos="pos.states,pos.trans,pos.edges,pos.scc,pos.nondet" +neg="neg.states,neg.trans,neg.edges,neg.scc,neg.nondet" +algos="time1,time2,time3,time4,time5,time6,time7,time8" + +OUTPUTF=bench_formulas.csv +( +all= for ap in 1 2 3 4; do - echo "Generating benchmarks for formulas with $ap atomic propositions..." - $RANDLTL $ap --tree-size=..30 -n 20000 | $LTLFILT --ap=$ap | - ./stutter_invariance_formulas -F- >> "$OUTPUT" + out=ltl-ap$ap.csv + echo "$out:; $RANDLTL $ap --tree-size=..30 -n -1 | $LTLFILT --ap=$ap | $LTLFILT -v --nox -n 10000 | ./stutter_invariance_formulas -F- > \$@" + all="$all $out" done -echo "Generating benchmarks for random graphs..." -OUTPUT=bench_randgraph.csv -echo 'algo,ap,states,result,time' > "$OUTPUT" -./stutter_invariance_randomgraph >> "$OUTPUT" +echo "$OUTPUTF:$all; (echo 'formula,ap,$pos,$neg,$algos,res'; cat $all) > \$@" +) > run.mk + +OUTPUTG=bench_randgraph.csv +( +all= +for d in 0.0 0.1 0.2 0.3 0.4 0.5 0.6 0.7 0.8 0.9 1.0; do + for ap in 1 2 3 4; do + out=graph-d$d-ap$ap.csv + echo "$out:; ./stutter_invariance_randomgraph $d $ap > \$@" + all="$all $out" + done +done +echo "$OUTPUTG:$all; (echo 'd,ap,seed,$pos,$neg,$algos,res'; cat $all) > \$@" +) >> run.mk + +make "$@" -f run.mk $OUTPUTF $OUTPUTG diff --git a/bench/stutter/stutter_invariance_formulas.cc b/bench/stutter/stutter_invariance_formulas.cc index 81593eb03..a84dd7b39 100644 --- a/bench/stutter/stutter_invariance_formulas.cc +++ b/bench/stutter/stutter_invariance_formulas.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2014 Laboratoire de Recherche et +// Copyright (C) 2014, 2015 Laboratoire de Recherche et // Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -22,8 +22,9 @@ #include "bin/common_finput.hh" #include "bin/common_output.hh" #include "tgbaalgos/translate.hh" -#include "tgbaalgos/stutter_invariance.hh" +#include "tgbaalgos/stutter.hh" #include "tgbaalgos/dupexp.hh" +#include "tgbaalgos/stats.hh" #include "ltlast/allnodes.hh" #include "ltlvisit/apcollect.hh" #include "ltlvisit/length.hh" @@ -47,8 +48,10 @@ namespace public: spot::translator& trans; std::string formula; + spot::stat_printer stats; - stut_processor(spot::translator& trans) : trans(trans) + stut_processor(spot::translator& trans) : + trans(trans), stats(std::cout, "%s,%t,%e,%S,%n,") { } @@ -69,31 +72,40 @@ namespace f->clone()); spot::tgba_digraph_ptr a = trans.run(f); spot::tgba_digraph_ptr na = trans.run(nf); - unsigned num_states = a->num_states(); spot::ltl::atomic_prop_set* ap = spot::ltl::atomic_prop_collect(f); bdd apdict = spot::ltl::atomic_prop_collect_as_bdd(f, a); - bool res; + + std::cout << formula << ',' << ap->size() << ','; + stats.print(a); + stats.print(na); + bool prev = true; for (int algo = 1; algo <= 8; ++algo) { - auto dup_a = spot::make_tgba_digraph(a); - auto dup_na = spot::make_tgba_digraph(na); + auto dup_a = spot::make_tgba_digraph(a, + spot::tgba::prop_set::all()); + auto dup_na = spot::make_tgba_digraph(na, + spot::tgba::prop_set::all()); spot::stopwatch sw; sw.start(); - res = spot::is_stutter_invariant(std::move(dup_a), - std::move(dup_na), - apdict, algo); + bool res = spot::is_stutter_invariant(std::move(dup_a), + std::move(dup_na), + apdict, algo); auto time = sw.stop(); + std::cout<< time << ','; - std::cout << formula << ',' << algo << ',' << ap->size() << ',' - << num_states << ',' << res << ',' << time * 1000000 - << '\n'; - - if (algo > '1') - assert(res == prev); + if (algo > 1 && prev != res) + { + std::cerr << "\nerror: algorithms " << algo - 1 + << " and " << algo << " disagree on formula " + << formula << "\n"; + exit(2); + } prev = res; } + std::cout << prev << '\n'; + f->destroy(); nf->destroy(); delete ap; diff --git a/bench/stutter/stutter_invariance_randomgraph.cc b/bench/stutter/stutter_invariance_randomgraph.cc index 5c8cf2a54..bc2303f53 100644 --- a/bench/stutter/stutter_invariance_randomgraph.cc +++ b/bench/stutter/stutter_invariance_randomgraph.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2014 Laboratoire de Recherche et +// Copyright (C) 2014, 2015 Laboratoire de Recherche et // Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -20,69 +20,114 @@ #include "misc/timer.hh" #include "ltlvisit/apcollect.hh" #include "tgbaalgos/dtgbacomp.hh" -#include "tgbaalgos/stutter_invariance.hh" #include "tgbaalgos/randomgraph.hh" #include "tgbaalgos/dotty.hh" #include "tgbaalgos/product.hh" -#include "tgbaalgos/stutterize.hh" -#include "tgbaalgos/closure.hh" +#include "tgbaalgos/stutter.hh" +#include "tgbaalgos/stats.hh" #include "tgba/tgbagraph.hh" #include "tgba/bdddict.hh" +#include "misc/random.hh" #include #include #include +constexpr unsigned algo_max = 8; + int -main() +main(int argc, char** argv) { + if (argc != 3) + { + std::cerr << "usage: " << argv[0] << " density n_ap\n"; + exit(2); + } + float d = strtof(argv[1], nullptr); + if (d < 0.0 || d > 1.0) + { + std::cerr << "density should be between 0 and 1"; + exit(2); + } + unsigned props_n = strtoul(argv[2], nullptr, 10); + + spot::bdd_dict_ptr dict = spot::make_bdd_dict(); - spot::tgba_digraph_ptr a; - spot::tgba_digraph_ptr na; - unsigned n = 10; + constexpr unsigned n = 10; + + // random ap set + auto ap = spot::ltl::create_atomic_prop_set(props_n); + // ap set as bdd + bdd apdict = bddtrue; + for (auto& i: ap) + apdict &= bdd_ithvar(dict->register_proposition(i, &ap)); + + std::vector disable_algo(algo_max); + unsigned algo_count = algo_max; + unsigned seed = 0; + + spot::stat_printer stats(std::cout, ",%s,%t,%e,%S,%n"); + for (unsigned states_n = 1; states_n <= 50; ++states_n) - for (float d = 0; d <= 1; d += 0.1) - { - for (unsigned props_n = 1; props_n <= 4; ++props_n) - { - // random ap set - auto ap = spot::ltl::create_atomic_prop_set(props_n); + { + // generate n random automata + for (unsigned i = 0; i < n; ++i) + { + spot::tgba_digraph_ptr a; + do + { + spot::srand(++seed); + a = spot::random_graph(states_n, d, &ap, dict, 2, 0.1, 0.5, + true); + } + while (a->is_empty()); + auto na = spot::dtgba_complement(a); - // ap set as bdd - bdd apdict = bddtrue; - for (auto& i: ap) - apdict &= bdd_ithvar(dict->register_proposition(i, a)); + std::cout << d << ',' << props_n << ',' << seed; + stats.print(a); + stats.print(na); - // generate n random automata - typedef std::pair - aut_pair_t; - std::vector vec; - for (unsigned i = 0; i < n; ++i) - { - a = spot::random_graph(states_n, d, &ap, dict, 2, 0.1, 0.5, - true); - na = spot::dtgba_complement(a); - vec.push_back(aut_pair_t(a, na)); - } + bool prev = true; + for (int algo = 1; algo <= 8; ++algo) + { + std::cout << ','; + if (disable_algo[algo - 1]) + continue; - for (int algo = 1; algo <= 8; ++algo) - { - // Copy vec, because is_stutter_invariant modifies the - // automata. - std::vector dup(vec); - spot::stopwatch sw; - sw.start(); - bool res; - for (auto& a: dup) - res = spot::is_stutter_invariant(std::move(a.first), - std::move(a.second), - apdict, algo); - auto time = sw.stop() / n; - std::cout << algo << ',' << props_n << ',' << states_n - << ',' << res << ',' << time << '\n'; - } - spot::ltl::destroy_atomic_prop_set(ap); - } - } + auto dup_a = spot::make_tgba_digraph(a, + spot::tgba::prop_set::all()); + auto dup_na = spot::make_tgba_digraph(na, + spot::tgba::prop_set::all()); + spot::stopwatch sw; + sw.start(); + bool res = spot::is_stutter_invariant(std::move(dup_a), + std::move(dup_na), + apdict, algo); + auto time = sw.stop(); + std::cout << time; + if (algo > 1 && res != prev) + { + std::cerr << "\nerror: algorithms " << algo - 1 + << " (" << prev << ") and " << algo << " (" + << res << ") disagree on seed " + << seed << "\n"; + exit(2); + } + if (time >= 30.0) + { + disable_algo[algo - 1] = 1; + --algo_count; + } + prev = res; + } + std::cout << ',' << prev << '\n';; + if (algo_count == 0) + break; + } + if (algo_count == 0) + break; + } + dict->unregister_all_my_variables(&ap); + spot::ltl::destroy_atomic_prop_set(ap); return 0; }