From 3c985a323525a7db81b2f80033909c7c87c275de Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 7 Feb 2014 14:10:07 +0100 Subject: [PATCH] sat: document the SPOT_SATLOG envvar * doc/org/satmin.org, src/bin/man/spot-x.x: Document it. * NEWS: Mention it. --- NEWS | 7 ++++++ doc/org/satmin.org | 54 ++++++++++++++++++++++++++++++++++++++++++++ src/bin/man/spot-x.x | 12 ++++++++++ 3 files changed, 73 insertions(+) diff --git a/NEWS b/NEWS index edf202962..83ef4f21c 100644 --- a/NEWS +++ b/NEWS @@ -1,5 +1,12 @@ New in spot 1.2.2a (not yet released) + * New features: + + - The SPOT_SATLOG environment variable can be set to a filename to + obtain statistics about the different iterations of the + SAT-based minimization. For an example, see + http://spot.lip6.fr/userdoc/satmin.html + * Bug fixes: - More fixes for Python 3 compatibility. diff --git a/doc/org/satmin.org b/doc/org/satmin.org index 1177b2d2d..53064681c 100644 --- a/doc/org/satmin.org +++ b/doc/org/satmin.org @@ -401,3 +401,57 @@ The following options can be used to fine-tune this procedure: When options =-B= and =-x sat-minimize= both used, =-x state-based= and =-x sat-acc=1= are implied. + + +* Logging statistics + +If the environment variable =SPOT_SATLOG= is set to the name of a +file, the minimization function will append statistics about each of +its iterations in this file. + +#+BEGIN_SRC sh :results verbatim :exports both +rm -f stats.csv +export SPOT_SATLOG=stats.csv +ltlfilt -f "Ga R (F!b & (c U b))" -l | +ltl2dstar --ltl2nba=spin:../../src/bin/ltl2tgba@-Ds - - | +dstar2tgba -D -x sat-minimize,sat-acc=2 --stats='input(states=%S) output(states=%s, acc-sets=%a, det=%d)' +echo +cat stats.csv +#+END_SRC + +#+RESULTS: +#+begin_example +input(states=11) output(states=5, acc-sets=2, det=1) + +9,9,44,72,44064,9043076,917,20,292,12 +8,7,31,56,22272,4203158,417,7,231,9 +6,6,28,48,10512,1369289,137,1,76,2 +5,,,,7200,785942,77,1,25,1 +#+end_example + +The generated CSV file use the following columns: +- the n passed to the SAT-based minimization algorithm + (it means the input automaton had n+1 states) +- number of reachable states in the output of + the minimization. +- number of edges in the output +- number of transitions +- number of variables in the SAT problem +- number of clauses in the SAT problem +- user time for encoding the SAT problem +- system time for encoding the SAT problem +- user time for solving the SAT problem +- system time for solving the SAT problem + +Times are measured with the times() function, and expressed +in ticks (usually: 1/100 of seconds). + +In the above example, you can see that also the input DRA had 11 +states, the minimization function received a 10-state DBA (one state +was probably simplified using simulation-based simplifications) and +started looking for an equivalent 9-state DTBA which it found. Then +looking for a 8-state DTBA, it found a solution with only 7 states, +etc. No solution where found when looking for a 5-state DTBA, so the +minimal complete DTBA has 6 states. The output of =dstar2tgba= has 5 +states just because it is not complete (the =--complete= option was +not given, so the useless sink state was removed). diff --git a/src/bin/man/spot-x.x b/src/bin/man/spot-x.x index af34ef95f..457a05671 100644 --- a/src/bin/man/spot-x.x +++ b/src/bin/man/spot-x.x @@ -11,6 +11,18 @@ spot-x \- Common fine-tuning options. [ENVIRONMENT VARIABLES] +.TP +\fBSPOT_SATLOG\fR +If set to a filename, the SAT-based minimization routines will append +statistics about each iteration to the named file. Each line lists +the following comma-separated values: requested number of states, +number of reachable states in the output, number of edges in the +output, number of transitions in the output, number of variables in +the SAT problem, number of clauses in the SAT problem, user time for +encoding the SAT problem, system time for encoding the SAT problem, +user time for solving the SAT problem, system time for solving the SAT +problem. + .TP \fBSPOT_SATSOLVER\fR If set, this variable should indicate how to call a SAT\-solver. This