From d309c01941b7399e46dfe74daaf30fd7f4794e8c Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 6 Apr 2005 16:31:32 +0000 Subject: [PATCH] * 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 | 8 ++++++++ bench/emptchk/Makefile.am | 34 +++++++++++++++++++++++++++++++++- bench/emptchk/README | 34 ++++++++++++++++++++++------------ bench/emptchk/pml-clserv.sh | 4 +++- bench/emptchk/pml-eeaean.sh | 2 +- bench/emptchk/pml2tgba.pl | 24 ++++++++++++++++++++---- 6 files changed, 87 insertions(+), 19 deletions(-) diff --git a/ChangeLog b/ChangeLog index a195418ee..9c44dbf4a 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,11 @@ +2005-04-06 Alexandre Duret-Lutz + + * 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 * src/ltlvisit/length.cc (length_visitor): Rewrite using diff --git a/bench/emptchk/Makefile.am b/bench/emptchk/Makefile.am index ca4141117..239cf5747 100644 --- a/bench/emptchk/Makefile.am +++ b/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) diff --git a/bench/emptchk/README b/bench/emptchk/README index 0b22eac5a..6352d5ee1 100644 --- a/bench/emptchk/README +++ b/bench/emptchk/README @@ -1,7 +1,7 @@ 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. ================= diff --git a/bench/emptchk/pml-clserv.sh b/bench/emptchk/pml-clserv.sh index b439efae5..3e2cf9d29 100644 --- a/bench/emptchk/pml-clserv.sh +++ b/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" diff --git a/bench/emptchk/pml-eeaean.sh b/bench/emptchk/pml-eeaean.sh index 967522d94..265fa68d2 100644 --- a/bench/emptchk/pml-eeaean.sh +++ b/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" diff --git a/bench/emptchk/pml2tgba.pl b/bench/emptchk/pml2tgba.pl index 9bfaa4fc4..ef6167ddc 100755 --- a/bench/emptchk/pml2tgba.pl +++ b/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 </dev/null"; +system "gcc -DCHECK$reduce -O -o pan pan.c 2>/dev/null"; # Match Büchi states to propositions my $buechitrans = 'BUG';