Commit c494a347 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz

stutter: fiddle with the benchmark

* bench/stutter/stutter_bench.sh: Add headers in the CSV files, and also
run stutter_invariance_randomgraph.
* bench/stutter/stutter_invariance_formulas.cc: Remove space from CSV
output.
* bench/stutter/stutter_invariance_randomgraph.cc: Likewise, plus fix
the call to is_stutter_invariant(), and return an average time.
* bench/stutter/stutter.ipynb: Adjust.
* bench/stutter/README: Simplify.
* bench/stutter/Makefile.am: Distribute the script and python notebook.
parent 0beb148b
......@@ -17,15 +17,17 @@
## You should have received a copy of the GNU General Public License
## along with this program. If not, see <http://www.gnu.org/licenses/>.
SUBDIRS = .
AM_CPPFLAGS = -I$(top_srcdir)/src -I$(top_builddir)/src $(BUDDY_CPPFLAGS) \
-I$(top_builddir)/lib -I$(top_srcdir)/lib
AM_CXXFLAGS = $(WARNING_CXXFLAGS)
LDADD = $(top_builddir)/src/bin/libcommon.a ../../lib/libgnu.la ../../src/libspot.la
LDADD = $(top_builddir)/src/bin/libcommon.a ../../lib/libgnu.la \
../../src/libspot.la
bin_PROGRAMS = stutter_invariance_randomgraph \
stutter_invariance_formulas
stutter_invariance_randomgraph_SOURCES = stutter_invariance_randomgraph.cc
stutter_invariance_formulas_SOURCES = stutter_invariance_formulas.cc
EXTRA_DIST = stutter_bench.sh stutter.ipynb
This benchmark measures the performance of different algorithms to check
if a büchi automaton has the stutter-invariance property. If the
benchmark is run on formulas, the translation time is not included in
the measured time.
This benchmark measures the performance of different algorithms to
check if property (expressed as a formula or as a deterministic TGBA)
is stutter-invariant. When the benchmark is run on formulas, the
translation time is not included in the measured time.
You can specify which formulas are to be used for the benchmarks by
running:
% ./stutter_invariance_formulas -F FILE > bench_formulas.csv
Where FILE is a file containing a list of formulas (see
./stutter_invariance_formulas --help for other input options).
Or use the script which will call this executable on random formulas
ranging from 1 to 4 atomic propositions:
To reproduce the benchmark is to run
% ./stutter_bench.sh
This will create the file bench_formulas.csv.
Alternatively, the algorithms can be measured on random complete
deterministic automata with:
% ./stutter_invariance_randomgraph > bench_randgraph.csv
to create bench_formulas.csv and bench_randgraph.csv, and then
explore these data the provided ipython notbook
Assuming ipython is installed, the csv files can be visualized using the
provided ipython notebook. Run:
% ipython notebook --pylab=inline stutter.ipynb
% ipython notebook --matplotlib
in this directory, and open stutter.ipynb.
The time in bench_formulas.csv is reported in microseconds, while the
time in bench_randgraph.csv is in seconds.
This diff is collapsed.
#!/bin/sh
OUTPUT=bench_formulas.csv
RANDLTL=../../src/bin/randltl
LTLFILT=../../src/bin/ltlfilt
if test -f bench_formulas.csv; then
echo -n "$OUTPUT already exists. [a]ppend, [r]emove it or [q]uit?"
read ans
if test "$ans" = "r"; then
rm "$OUTPUT"
else if test "$ans" = "q" -o "$ans" != "a"; then
echo "abort."
exit 0
fi
fi
fi
OUTPUT=bench_formulas.csv
echo 'formula,algo,ap,states,result,time' > "$OUTPUT"
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"
done
echo "Generating benchmarks for random graphs..."
OUTPUT=bench_randgraph.csv
echo 'algo,ap,states,result,time' > "$OUTPUT"
./stutter_invariance_randomgraph >> "$OUTPUT"
......@@ -86,8 +86,9 @@ namespace
apdict, algo);
auto time = sw.stop();
std::cout << formula << ", " << algo << ", " << ap->size() << ", "
<< num_states << ", " << res << ", " << time * 1000000 << std::endl;
std::cout << formula << ',' << algo << ',' << ap->size() << ','
<< num_states << ',' << res << ',' << time * 1000000
<< '\n';
if (algo > '1')
assert(res == prev);
......
......@@ -64,13 +64,8 @@ main()
vec.push_back(aut_pair_t(a, na));
}
char algostr[2] = { 0, 0 };
for (char algo = '1'; algo <= '8'; ++algo)
for (int algo = 1; algo <= 8; ++algo)
{
// Select the algorithm for checking stutter-invariance
algostr[0] = algo;
setenv("SPOT_STUTTER_CHECK", algostr, true);
// Copy vec, because is_stutter_invariant modifies the
// automata.
std::vector<aut_pair_t> dup(vec);
......@@ -80,10 +75,10 @@ main()
for (auto& a: dup)
res = spot::is_stutter_invariant(std::move(a.first),
std::move(a.second),
apdict);
auto time = sw.stop();
std::cout << algo << ", " << props_n << ", " << states_n
<< ", " << res << ", " << time << std::endl;
apdict, algo);
auto time = sw.stop() / n;
std::cout << algo << ',' << props_n << ',' << states_n
<< ',' << res << ',' << time << '\n';
}
spot::ltl::destroy_atomic_prop_set(ap);
}
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment