* bench/emptchk/Makefile.am: Create reduced versions of the graphs.

* bench/emptchk/pml2tgba.pl: Add option -r.
* bench/emptchk/pml-clserv.sh, bench/emptchk/pml-eeaean.sh:
Also run on reduced graphs (this is fast).
* bench/emptchk/README: Adjust.

ChangeLog

+2005-04-06  Alexandre Duret-Lutz  <adl@src.lip6.fr>
+
+	* bench/emptchk/Makefile.am: Create reduced versions of the graphs.
+	* bench/emptchk/pml2tgba.pl: Add option -r.
+	* bench/emptchk/pml-clserv.sh, bench/emptchk/pml-eeaean.sh:
+	Also run on reduced graphs (this is fast).
+	* bench/emptchk/README: Adjust.
+
 2005-02-23  Alexandre Duret-Lutz  <adl@src.lip6.fr>
 
 	* src/ltlvisit/length.cc (length_visitor): Rewrite using

bench/emptchk/Makefile.am

@@ -42,36 +42,68 @@ dist_noinst_DATA = \
 
 nodist_noinst_DATA = \
   models/cl3serv1.tgba \
+  models/cl3serv1R.tgba \
   models/cl3serv1fair.tgba \
+  models/cl3serv1Rfair.tgba \
   models/cl3serv3.tgba \
+  models/cl3serv3R.tgba \
   models/cl3serv3fair.tgba \
+  models/cl3serv3Rfair.tgba \
   models/eeaean1.tgba \
-  models/eeaean2.tgba
+  models/eeaean1R.tgba \
+  models/eeaean2.tgba \
+  models/eeaean2R.tgba
 
 models/cl3serv1.tgba: $(srcdir)/models/cl3serv1.pml
 	$(mkdir_p) models
 	$(PML2TGBA) $(srcdir)/models/cl3serv1.pml w1 s1 >$@
 
+models/cl3serv1R.tgba: $(srcdir)/models/cl3serv1.pml
+	$(mkdir_p) models
+	$(PML2TGBA) -r $(srcdir)/models/cl3serv1.pml w1 s1 >$@
+
 models/cl3serv1fair.tgba: $(srcdir)/models/cl3serv1.pml
 	$(mkdir_p) models
 	$(PML2TGBA) -w $(srcdir)/models/cl3serv1.pml w1 s1 >$@
 
+models/cl3serv1Rfair.tgba: $(srcdir)/models/cl3serv1.pml
+	$(mkdir_p) models
+	$(PML2TGBA) -w -r $(srcdir)/models/cl3serv1.pml w1 s1 >$@
+
 models/cl3serv3.tgba: $(srcdir)/models/cl3serv3.pml
 	$(mkdir_p) models
 	$(PML2TGBA) $(srcdir)/models/cl3serv3.pml w1 s1 >$@
 
+models/cl3serv3R.tgba: $(srcdir)/models/cl3serv3.pml
+	$(mkdir_p) models
+	$(PML2TGBA) -r $(srcdir)/models/cl3serv3.pml w1 s1 >$@
+
 models/cl3serv3fair.tgba: $(srcdir)/models/cl3serv3.pml
 	$(mkdir_p) models
 	$(PML2TGBA) -w $(srcdir)/models/cl3serv3.pml w1 s1 >$@
 
+models/cl3serv3Rfair.tgba: $(srcdir)/models/cl3serv3.pml
+	$(mkdir_p) models
+	$(PML2TGBA) -w -r $(srcdir)/models/cl3serv3.pml w1 s1 >$@
+
 models/eeaean1.tgba: $(srcdir)/models/eeaean1.pml
 	$(mkdir_p) models
 	$(PML2TGBA) $(srcdir)/models/eeaean1.pml \
           noLeader zeroLeads oneLeads twoLeads threeLeads >$@
 
+models/eeaean1R.tgba: $(srcdir)/models/eeaean1.pml
+	$(mkdir_p) models
+	$(PML2TGBA) -r $(srcdir)/models/eeaean1.pml \
+          noLeader zeroLeads oneLeads twoLeads threeLeads >$@
+
 models/eeaean2.tgba: $(srcdir)/models/eeaean2.pml
 	$(mkdir_p) models
 	$(PML2TGBA) $(srcdir)/models/eeaean2.pml \
           noLeader zeroLeads oneLeads twoLeads threeLeads >$@
 
+models/eeaean2R.tgba: $(srcdir)/models/eeaean2.pml
+	$(mkdir_p) models
+	$(PML2TGBA) -r $(srcdir)/models/eeaean2.pml \
+          noLeader zeroLeads oneLeads twoLeads threeLeads >$@
+
 CLEANFILES = $(nodist_noinst_DATA)

bench/emptchk/README

 This directory contains the input files and scripts used to produce
 the measures in our paper "On-the-fly Emptiness Checks for Generalized
 Büchi Automata" (J.-M. Couvreur, A. Duret-Lutz, D. Poitrenaud),
-submitted to CAV'05.
+submitted to Spin'05.
 
 ==========
  CONTENTS
@@ -114,7 +114,7 @@ This directory contains:
 
 * pml2tgba.pl
 
-    A Perl script to translate Promela models into TGBA readble by Spot.
+    A Perl script to translate Promela models into TGBA readable by Spot.
     This requires a working spin in PATH.
 
 * ltl-random.sh
@@ -131,7 +131,7 @@ This directory contains:
 
     Check the two configurations of the client/server example against
     the formula in models/clserv.ltl, without and with fairness
-    assumptions, using all the algorithms of the file `algorihms'.
+    assumptions, using all the algorithms of the file `algorithms'.
     You should have run `make' before attempting to run this script,
     so the state space are available.
 
@@ -139,7 +139,7 @@ This directory contains:
 
     Check models/eeaean1.pml and models/eeaean2.pml against each
     formulae in models/eeaean.ltl, using all the algorithms of the
-    file `algorihms'.  You should have run `make' before attempting to
+    file `algorithms'.  You should have run `make' before attempting to
     run this script, so the state space are available.
 
 * algorithms
@@ -150,7 +150,7 @@ This directory contains:
  USAGE
 =======
 
-  0. Install SPIN (spinroot.com), and make sure the `spin' binary is in
+  0. Install Spin (spinroot.com), and make sure the `spin' binary is in
      your path.
 
   1. If that is not done already, configure and compile all the Spot
@@ -159,12 +159,22 @@ This directory contains:
   2. Run `make' in this directory.  This will call pml2tgba.pl to
      generate the TGBA input for the two pml-*.sh tests.
 
+     Promela inputs are translated in 4 different graphs.
+     For instance eeaean1.pml is translated as
+       - eeaean1.tgba        full translation
+       - eeaean1fair.tgba    full translation with weak fairness
+       - eeaean1R.tgba       reduced translation
+       - eeaean1Rfair.tgba   reduced translation with weak fairness
+     The "reduced" translation uses Spin's partial order reductions.
+
+     (The "R"educed variants are not shown in the paper.)
+
   3. Run the tests you are interested in
 
-     - ltl-random.sh
-     - ltl-human.sh
-     - pml-clserv.sh
-     - pml-eeaean.sh
+      - ltl-random.sh
+      - ltl-human.sh
+      - pml-clserv.sh
+      - pml-eeaean.sh
 
      Beware that the two ltl-*.sh tests are very long (each of them
      run 13 emptiness-check algorithms against 18000 product-spaces!).
@@ -221,11 +231,11 @@ This directory contains:
       expressed as a % of the number of transition of the product space
   (C) mean of the maximal stack size
       expressed as a % of the number of state of the product space
-  (D) number of non-empy automata used for these statistics
+  (D) number of non-empty automata used for these statistics
   (E) mean number of states in the search space for accepting runs
       expressed as a % of the number of state of the product space
   (F) mean number of states visited (possibly several times) while
-      computing the acceptin run
+      computing the accepting run
       expressed as a % of the number of state of the product space
 
 
@@ -242,7 +252,7 @@ This directory contains:
   (K) Number of distinct states visited by the emptiness-check algorithm.
   (L) Number of transitions visited by the emptiness-check algorithm.
   (M) Maximal size of the stack.
-  (N) Whehter an accepting run was found.
+  (N) Whether an accepting run was found.
 
 
 =================

bench/emptchk/pml-clserv.sh

@@ -27,7 +27,9 @@ FORMULAE=$srcdir/models/clserv.ltl
 
 opts='-f -x -m'
 
-for model in cl3serv1.tgba cl3serv1fair.tgba cl3serv3.tgba cl3serv3fair.tgba
+for model in \
+  cl3serv1.tgba  cl3serv1fair.tgba  cl3serv3.tgba  cl3serv3fair.tgba \
+  cl3serv1R.tgba cl3serv1Rfair.tgba cl3serv3R.tgba cl3serv3Rfair.tgba
 do
   echo "+++++++++++++++++++++"
   echo "  $model"

bench/emptchk/pml-eeaean.sh

@@ -27,7 +27,7 @@ FORMULAE=$srcdir/models/eeaean.ltl
 
 opts='-f -x -m'
 
-for model in eeaean1.tgba eeaean2.tgba
+for model in eeaean1.tgba eeaean2.tgba eeaean1R.tgba eeaean2R.tgba
 do
   echo "+++++++++++++++++++++"
   echo "  $model"

bench/emptchk/pml2tgba.pl

@@ -36,6 +36,7 @@
 #     (we want to use the LTL->TGBA translation of Spot, not that of Spin)
 #   - output the state space in Spot's format
 #   - optionally output weak fairness constraints
+#   - allow partial order or not
 
 use strict;
 
@@ -47,7 +48,10 @@ sub usage()
   print <<EOF;
 Usage: pml2tgba.pl [-w] promela-model properties...
 Extract the state-space of the promela-model, observing properties.
-If -w is given, output acceptance conditions to ensure weak fairness.
+
+Options:
+  -w    output acceptance conditions to ensure weak fairness
+  -r    let Spin reduce the state-space using partial order
 EOF
   exit 1;
 }
@@ -88,9 +92,21 @@ sub create_2n_automaton (@)
 usage unless @ARGV;
 
 my $weak = 0;
-if ($ARGV[0] eq '-w')
+my $reduce = ' -DNOREDUCE';
+while (1)
 {
-  $weak = 1;
+  if ($ARGV[0] eq '-w')
+    {
+      $weak = 1;
+    }
+  elsif ($ARGV[0] eq '-r')
+    {
+      $reduce = '';
+    }
+  else
+    {
+      last;
+    }
   shift;
 }
 
@@ -106,7 +122,7 @@ close NEVER;
 
 system "spin -a -N never.$$ \"$model\"";
 unlink "never.$$";
-system "gcc -DCHECK -DNOREDUCE -O -o pan pan.c 2>/dev/null";
+system "gcc -DCHECK$reduce -O -o pan pan.c 2>/dev/null";
 
 # Match Büchi states to propositions
 my $buechitrans = 'BUG';