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.
This commit is contained in:
Alexandre Duret-Lutz
parent
5d31094029
commit
bd414d4d4c
4 changed files with 153 additions and 76 deletions
|
|
@ -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
|
||||
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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),
|
||||
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;
|
||||
|
|
|
|||
|
|
@ -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 <cstdio>
|
||||
#include <cstring>
|
||||
#include <vector>
|
||||
|
||||
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;
|
||||
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)
|
||||
{
|
||||
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, a));
|
||||
apdict &= bdd_ithvar(dict->register_proposition(i, &ap));
|
||||
|
||||
std::vector<unsigned char> 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)
|
||||
{
|
||||
// generate n random automata
|
||||
typedef std::pair<spot::tgba_digraph_ptr, spot::tgba_digraph_ptr>
|
||||
aut_pair_t;
|
||||
std::vector<aut_pair_t> vec;
|
||||
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);
|
||||
na = spot::dtgba_complement(a);
|
||||
vec.push_back(aut_pair_t(a, na));
|
||||
}
|
||||
while (a->is_empty());
|
||||
auto na = spot::dtgba_complement(a);
|
||||
|
||||
std::cout << d << ',' << props_n << ',' << seed;
|
||||
stats.print(a);
|
||||
stats.print(na);
|
||||
|
||||
bool prev = true;
|
||||
for (int algo = 1; algo <= 8; ++algo)
|
||||
{
|
||||
// Copy vec, because is_stutter_invariant modifies the
|
||||
// automata.
|
||||
std::vector<aut_pair_t> dup(vec);
|
||||
std::cout << ',';
|
||||
if (disable_algo[algo - 1])
|
||||
continue;
|
||||
|
||||
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;
|
||||
for (auto& a: dup)
|
||||
res = spot::is_stutter_invariant(std::move(a.first),
|
||||
std::move(a.second),
|
||||
bool res = spot::is_stutter_invariant(std::move(dup_a),
|
||||
std::move(dup_na),
|
||||
apdict, algo);
|
||||
auto time = sw.stop() / n;
|
||||
std::cout << algo << ',' << props_n << ',' << states_n
|
||||
<< ',' << res << ',' << time << '\n';
|
||||
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;
|
||||
}
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue