From 7bba6dc63d1dbba86af45c37b5cb56a0bc19c4cd Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 28 Jan 2005 23:55:33 +0000 Subject: [PATCH] * src/tgbaalgos/emptiness_stats.hh: Make sure depth() >= 0. * src/tgbaalgos/gtec/gtec.hh (couvreur99_check, couvreur99_check_shy): Add the poprem option. * src/tgbaalgos/gtec/gtec.cc: Implement it. * src/tgbaalgos/gtec/sccstack.cc, src/tgbaalgos/gtec/sccstack.hh (scc_stack::rem, scc_stack::clear_rem, scc_stack::connected_component::rem): New. * src/tgbatest/ltl2tgba.cc, src/tgbatest/randtgba.cc: Add rem variants. --- Makefile.am | 11 +- README | 5 +- bench/.cvsignore | 2 + bench/Makefile.am | 22 +++ bench/emptchk/.cvsignore | 4 + bench/emptchk/Makefile.am | 68 ++++++++ bench/emptchk/README | 262 ++++++++++++++++++++++++++++++ bench/emptchk/algorithms | 11 ++ bench/emptchk/defs.in | 39 +++++ bench/emptchk/ltl-human.sh | 40 +++++ bench/emptchk/ltl-random.sh | 40 +++++ bench/emptchk/models/.cvsignore | 1 + bench/emptchk/models/cl3serv1.pml | 43 +++++ bench/emptchk/models/cl3serv3.pml | 43 +++++ bench/emptchk/models/clserv.ltl | 1 + bench/emptchk/models/eeaean.ltl | 9 + bench/emptchk/models/eeaean2.pml | 118 ++++++++++++++ bench/emptchk/pml-clserv.sh | 46 ++++++ bench/emptchk/pml-eeaean.sh | 46 ++++++ bench/emptchk/pml2tgba.pl | 209 ++++++++++++++++++++++++ configure.ac | 7 +- 21 files changed, 1023 insertions(+), 4 deletions(-) create mode 100644 bench/.cvsignore create mode 100644 bench/Makefile.am create mode 100644 bench/emptchk/.cvsignore create mode 100644 bench/emptchk/Makefile.am create mode 100644 bench/emptchk/README create mode 100644 bench/emptchk/algorithms create mode 100644 bench/emptchk/defs.in create mode 100644 bench/emptchk/ltl-human.sh create mode 100644 bench/emptchk/ltl-random.sh create mode 100644 bench/emptchk/models/.cvsignore create mode 100644 bench/emptchk/models/cl3serv1.pml create mode 100644 bench/emptchk/models/cl3serv3.pml create mode 100644 bench/emptchk/models/clserv.ltl create mode 100644 bench/emptchk/models/eeaean.ltl create mode 100644 bench/emptchk/models/eeaean2.pml create mode 100644 bench/emptchk/pml-clserv.sh create mode 100644 bench/emptchk/pml-eeaean.sh create mode 100755 bench/emptchk/pml2tgba.pl diff --git a/Makefile.am b/Makefile.am index 6505df1a4..0a330457d 100644 --- a/Makefile.am +++ b/Makefile.am @@ -1,4 +1,4 @@ -## Copyright (C) 2003 Laboratoire d'Informatique de Paris 6 (LIP6), +## Copyright (C) 2003, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), ## département Systèmes Répartis Coopératifs (SRC), Université Pierre ## et Marie Curie. ## @@ -25,8 +25,15 @@ endif WITH_INCLUDED_BUDDY if WITH_INCLUDED_LBTT MAYBE_LBTT = lbtt endif WITH_INCLUDED_LBTT +if NEVER + # For Automake a conditional directory + # is conditionally built, but unconditionally distributed. + # So using NEVER here ensures that `make all' will not + # recurse in bench/, but `make dist' will. + NEVER_BENCH = bench +endif -SUBDIRS = $(MAYBE_BUDDY) $(MAYBE_LBTT) doc src wrap iface +SUBDIRS = $(MAYBE_BUDDY) $(MAYBE_LBTT) $(NEVER_BENCH) doc src wrap iface ACLOCAL_AMFLAGS = -I m4 EXTRA_DIST = HACKING diff --git a/README b/README index a942978f2..a9b2409c8 100644 --- a/README +++ b/README @@ -101,13 +101,16 @@ src/ Sources for libspot. misc/ Miscellaneous support files. tgba/ TGBA objects and cousins. tgbaalgos/ Algorithms on TGBA. - gtec/ Generalized Tarjan Emptiness-Check. + gtec/ Couvreur's Emptiness-Check. tgbaparse/ Parser for explicit TGBA. tgbatest/ Tests for tgba/, tgbaalgos/, and tgbaparse/. + evtgba*/ Ignore these for now. doc/ Documentation for libspot. spot.html/ HTML reference manual. spot.latex/ Sources for the PDF manual. (No distributed, can be rebuilt.) spotref.pdf PDF reference manual. +bench/ Benchmarks... + emptchk/ ... for emptiness-check algorithms. (Paper submitted to CAV'05) wrap/ Wrappers for other languages. python/ Python bindings for Spot and BuDDy tests/ Tests for these bindings diff --git a/bench/.cvsignore b/bench/.cvsignore new file mode 100644 index 000000000..282522db0 --- /dev/null +++ b/bench/.cvsignore @@ -0,0 +1,2 @@ +Makefile +Makefile.in diff --git a/bench/Makefile.am b/bench/Makefile.am new file mode 100644 index 000000000..04d1ed5e6 --- /dev/null +++ b/bench/Makefile.am @@ -0,0 +1,22 @@ +## Copyright (C) 2005 Laboratoire d'Informatique de Paris 6 (LIP6), +## département Systèmes Répartis Coopératifs (SRC), Université Pierre +## et Marie Curie. +## +## This file is part of Spot, a model checking library. +## +## Spot is free software; you can redistribute it and/or modify it +## under the terms of the GNU General Public License as published by +## the Free Software Foundation; either version 2 of the License, or +## (at your option) any later version. +## +## Spot is distributed in the hope that it will be useful, but WITHOUT +## ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +## or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +## License for more details. +## +## You should have received a copy of the GNU General Public License +## along with Spot; see the file COPYING. If not, write to the Free +## Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA +## 02111-1307, USA. + +SUBDIRS = emptchk diff --git a/bench/emptchk/.cvsignore b/bench/emptchk/.cvsignore new file mode 100644 index 000000000..5dd394a31 --- /dev/null +++ b/bench/emptchk/.cvsignore @@ -0,0 +1,4 @@ +Makefile +Makefile.in +defs +pan* diff --git a/bench/emptchk/Makefile.am b/bench/emptchk/Makefile.am new file mode 100644 index 000000000..dfbbe065e --- /dev/null +++ b/bench/emptchk/Makefile.am @@ -0,0 +1,68 @@ +## Copyright (C) 2005 Laboratoire d'Informatique de Paris 6 (LIP6), +## département Systèmes Répartis Coopératifs (SRC), Université Pierre +## et Marie Curie. +## +## This file is part of Spot, a model checking library. +## +## Spot is free software; you can redistribute it and/or modify it +## under the terms of the GNU General Public License as published by +## the Free Software Foundation; either version 2 of the License, or +## (at your option) any later version. +## +## Spot is distributed in the hope that it will be useful, but WITHOUT +## ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +## or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +## License for more details. +## +## You should have received a copy of the GNU General Public License +## along with Spot; see the file COPYING. If not, write to the Free +## Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA +## 02111-1307, USA. + + +PML2TGBA = $(PERL) $(srcdir)/pml2tgba.pl + +noinst_SCRIPTS = defs +dist_noinst_SCRIPTS = \ + pml2tgba.pl \ + ltl-human.sh \ + ltl-random.sh + +dist_noinst_DATA = \ + models/cl3serv1.pml \ + models/cl3serv3.pml \ + models/clserv.ltl \ + models/eeaean2.pml \ + models/eeaean.ltl \ + formulae.ltl \ + algorithms + +nodist_noinst_DATA = \ + models/cl3serv1.tgba \ + models/cl3serv1fair.tgba \ + models/cl3serv3.tgba \ + models/cl3serv3fair.tgba \ + models/eeaean2.tgba + +models/cl3serv1.tgba: $(srcdir)/models/cl3serv1.pml + $(mkdir_p) models + $(PML2TGBA) $(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/cl3serv3.tgba: $(srcdir)/models/cl3serv3.pml + $(mkdir_p) models + $(PML2TGBA) $(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/eeaean2.tgba: $(srcdir)/models/eeaean2.pml + $(mkdir_p) models + $(PML2TGBA) $(srcdir)/models/eeaean2.pml \ + noLeader zeroLeads oneLeads twoLeads threeLeads >$@ + +CLEANFILES = $(nodist_noinst_DATA) diff --git a/bench/emptchk/README b/bench/emptchk/README new file mode 100644 index 000000000..943ec870f --- /dev/null +++ b/bench/emptchk/README @@ -0,0 +1,262 @@ +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. + +========== + CONTENTS +========== + +This directory contains: + +* models/cl3serv1.pml +* models/cl3serv3.pml + + Two simple client/server promela examples. + +* models/clserv.ltl + + An LTL formula to verify on these examples. + +* models/eeaean2.pml + + A variations of the leader election protocol with extinction from + Tel, Introduction to Distributed Algorithms, 1994, Chapter 7. The + network in the model consists of three nodes. In Variant 1, the + same node wins every time, in Variant 2, each node gets a turn at + winning the election. This script was originally distributed + alongside with + + @InProceedings{ schwoon.05.tacas, + author = {Stefan Schwoon and Javier Esparza}, + title = {A note on on-the-fly verification algorithms.}, + booktitle = {Proceedings of the 11th International Conference + on Tools and Algorithms for the Construction and + Analysis of Systems + (TACAS'05)}, + year = {2005}, + series = {Lecture Notes in Computer Science}, + publisher = {Springer-Verlag}, + month = apr + } + +* models/eeaean.ltl + + Sample properties for the leader election protocols. These come from + + @InProceedings{ geldenhuys.04.tacas, + author = {Jaco Geldenhuys and Antti Valmari}, + title = {Tarjan's Algorithm Makes On-the-Fly {LTL} Verification + More Efficient}, + booktitle = {Proceedings of the 10th International Conference on + Tools and Algorithms for the Construction and Analysis + of Systems + (TACAS'04)}, + editor = {Kurt Jensen and Andreas Podelski}, + pages = {205--219}, + year = {2004}, + publisher = {Springer-Verlag}, + series = {Lecture Notes in Computer Science}, + volume = {2988}, + isbn = {3-540-21299-X} + } + +* formulae.ltl + + A list of 96 handwritten formulae with their negations. They come + from three sources: + + @InProceedings{ dwyer.98.fmsp, + author = {Matthew B. Dwyer and George S. Avrunin and James C. + Corbett}, + title = {Property Specification Patterns for Finite-state + Verification}, + booktitle = {Proceedings of the 2nd Workshop on Formal Methods in + Software Practice (FMSP'98)}, + publisher = {ACM Press}, + address = {New York}, + editor = {Mark Ardis}, + month = mar, + year = {1998}, + pages = {7--15} + } + + @InProceedings{ etessami.00.concur, + author = {Kousha Etessami and Gerard J. Holzmann}, + title = {Optimizing {B\"u}chi Automata}, + booktitle = {Proceedings of the 11th International Conference on + Concurrency Theory (Concur'00)}, + pages = {153--167}, + year = {2000}, + editor = {C. Palamidessi}, + volume = {1877}, + series = {Lecture Notes in Computer Science}, + address = {Pennsylvania, USA}, + publisher = {Springer-Verlag} + } + + @InProceedings{ somenzi.00.cav, + author = {Fabio Somenzi and Roderick Bloem}, + title = {Efficient {B\"u}chi Automata for {LTL} Formul{\ae}}, + booktitle = {Proceedings of the 12th International Conference on + Computer Aided Verification (CAV'00)}, + pages = {247--263}, + year = {2000}, + volume = {1855}, + series = {Lecture Notes in Computer Science}, + address = {Chicago, Illinois, USA}, + publisher = {Springer-Verlag} + } + + +* pml2tgba.pl + + A Perl script to translate Promela models into TGBA readble by Spot. + This requires a working spin in PATH. + +* ltl-random.sh + + Use all emptiness-check algorithms to test random graphs against + random LTL formulae. + +* ltl-human.sh + + Use all emptiness-check algorithms to test random graphs against + all the formulae of the file `formulae.ltl' + +* pml-clserv.sh + + 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'. + You should have run `make' before attempting to run this script, + so the state space are available. + +* pml-eeaean.sh + + Check 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 run + this script, so the state space are available. + + +======= + USAGE +======= + + 1. If that is not done already, configure and compile all Spot library, + then come back into this directory. + + 2. Run `make' in this directory. This will call pml2tgba.pl to + generate the TGBA input for the two pml-*.sh tests. + + 3. Run the tests you are interested in + + - 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 state-spaces!) + + You can speed up the pml-*.sh tests by removing some algorithms + from the `algorithms' file. + +========================== + INTERPRETING THE RESULTS +========================== + + Here are the short names for the algorithms used in the outputs. + + Cou99 + Cou99_shy- + Cou99_shy + > Cou99_rem + > Cou99_rem_shy- + > Cou99_rem_shy + > CVWY90 + CVWY90_bsh + > GV04 + > SE05 + SE05_bsh + > Tau03 + > Tau03_opt + + Only the algorithms marked with a `>' have been shown in the paper. + `bsh' stands for `bit-state hashing'. + + `Cou99_rem*' algorithms are using the `rem' field to remove + the SCC without recomputing the SCC as described in the paper. + The other `Cou99*' algorithms are not. (Beware that in the paper + we showed the `Cou99_rem*' variants and called them `Cou99*'.) + + + The ltl-*.sh tests output look as follows: + + | density: 0.001 + | Ratios about empt. check (all tests) + | CVWY90 5.5 4.4 6.3 25 + | CVWY90_bsh 5.7 4.8 6.3 25 + | Cou99 5.5 3.3 4.3 25 + | Cou99_rem 5.5 3.0 4.3 25 + | ... + (A) (B) (C) (D) + | + | Ratios about search space + | CVWY90 5.5 + | Cou99 2.0 + | Cou99_rem 2.0 + | Cou99_rem_shy 1.2 + | ... + (E) + | + | Ratios about acc. run computation + | CVWY90 2.6 + | CVWY90_bsh 2.6 + | Cou99 2.1 + | Cou99_rem 2.1 + | ... + (F) + + (A) mean number of distinct states visited + expressed as a % of the number of state of the product space + (B) mean number of distinct transitions visited + 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 + (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 + expressed as a % of the number of state of the product space + + + The pml-*.sh tests output look as follows: + + | Cou99 , 783, 2371, 5, 783, 4742, 237, no accepting run found + | Cou99_shy- , 783, 2371, 5, 783, 4742, 537, no accepting run found + | ... + (G) (H) (I) (K) (L) (M) (N) + + (G) Number of states in the product. + (H) Number of transitions in the product. + (I) Number of acceptance conditions in the product. + (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. + + +================= + MORE STATISTICS +================= + + The ltl-*.sh tests use src/tgbatest/randtgba to output statistics, + but randtgba is able to output a lot more data than what we have + shown above. Try removing the `-1' option from the script, or toying + with randtgba itself. + + Besides randtgba, two other tools that you might find handy we + experimenting are src/ltltest/randltl and src/tgbatest/ltl2tgba. diff --git a/bench/emptchk/algorithms b/bench/emptchk/algorithms new file mode 100644 index 000000000..be8d65906 --- /dev/null +++ b/bench/emptchk/algorithms @@ -0,0 +1,11 @@ +Cou99 +Cou99_shy- +Cou99_shy +Cou99_rem +Cou99_rem_shy- +Cou99_rem_shy +GV04 +CVWY90 +SE05 +Tau03 +Tau03_opt diff --git a/bench/emptchk/defs.in b/bench/emptchk/defs.in new file mode 100644 index 000000000..03405833e --- /dev/null +++ b/bench/emptchk/defs.in @@ -0,0 +1,39 @@ +# -*- shell-script -*- +# Copyright (C) 2005 Laboratoire d'Informatique de Paris 6 (LIP6), +# département Systèmes Répartis Coopératifs (SRC), Université Pierre +# et Marie Curie. +# +# This file is part of Spot, a model checking library. +# +# Spot is free software; you can redistribute it and/or modify it +# under the terms of the GNU General Public License as published by +# the Free Software Foundation; either version 2 of the License, or +# (at your option) any later version. +# +# Spot is distributed in the hope that it will be useful, but WITHOUT +# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +# or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +# License for more details. +# +# You should have received a copy of the GNU General Public License +# along with Spot; see the file COPYING. If not, write to the Free +# Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA +# 02111-1307, USA. + +# Ensure we are running from the right directory. +test -f ./defs || { + echo "defs: not found in current directory" 1>&2 + exit 1 +} + +srcdir='@srcdir@' + +# Ensure $srcdir is set correctly. +test -f "$srcdir/defs.in" || { + echo "$srcdir/defs.in not found, check \$srcdir" 1>&2 + exit 1 +} + +RANDTGBA='@top_srcdir@/src/tgbatest/randtgba@EXEEXT@' +LTL2TGBA='@top_srcdir@/src/tgbatest/ltl2tgba@EXEEXT@' +FORMULAE=$srcdir/formulae.ltl diff --git a/bench/emptchk/ltl-human.sh b/bench/emptchk/ltl-human.sh new file mode 100644 index 000000000..1bde52588 --- /dev/null +++ b/bench/emptchk/ltl-human.sh @@ -0,0 +1,40 @@ +#!/bin/sh +# Copyright (C) 2005 Laboratoire d'Informatique de Paris 6 (LIP6), +# département Systèmes Répartis Coopératifs (SRC), Université Pierre +# et Marie Curie. +# +# This file is part of Spot, a model checking library. +# +# Spot is free software; you can redistribute it and/or modify it +# under the terms of the GNU General Public License as published by +# the Free Software Foundation; either version 2 of the License, or +# (at your option) any later version. +# +# Spot is distributed in the hope that it will be useful, but WITHOUT +# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +# or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +# License for more details. +# +# You should have received a copy of the GNU General Public License +# along with Spot; see the file COPYING. If not, write to the Free +# Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA +# 02111-1307, USA. + +. ./defs +set -e + +opts="-1 -D -e 15 -n 1024 -t 0.5 -r -z -i $FORMULAE" + +echo "WITHOUT ADDITIONAL ACCEPTING CONDITIONS" + +for d in 0.001 0.002 0.1; do + echo "density: $d" + $RANDTGBA -d $d $opts +done + +echo "WITH 3 ADDITIONAL ACCEPTING CONDITIONS" + +for d in 0.001 0.002 0.1; do + echo "density: $d" + $RANDTGBA -a 3 0.0133333 -d $d $opts +done diff --git a/bench/emptchk/ltl-random.sh b/bench/emptchk/ltl-random.sh new file mode 100644 index 000000000..c630636d4 --- /dev/null +++ b/bench/emptchk/ltl-random.sh @@ -0,0 +1,40 @@ +#!/bin/sh +# Copyright (C) 2005 Laboratoire d'Informatique de Paris 6 (LIP6), +# département Systèmes Répartis Coopératifs (SRC), Université Pierre +# et Marie Curie. +# +# This file is part of Spot, a model checking library. +# +# Spot is free software; you can redistribute it and/or modify it +# under the terms of the GNU General Public License as published by +# the Free Software Foundation; either version 2 of the License, or +# (at your option) any later version. +# +# Spot is distributed in the hope that it will be useful, but WITHOUT +# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +# or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +# License for more details. +# +# You should have received a copy of the GNU General Public License +# along with Spot; see the file COPYING. If not, write to the Free +# Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA +# 02111-1307, USA. + +. ./defs +set -e + +opts="-1 -D -e 15 -n 1024 -t 0.5 -f 5 -F 200 -l 5 -u -r -z a b c d" + +echo "WITHOUT ADDITIONAL ACCEPTING CONDITIONS" + +for d in 0.001 0.002 0.01; do + echo "density: $d" + $RANDTGBA -d $d $opts +done + +echo "WITH 3 ADDITIONAL ACCEPTING CONDITIONS" + +for d in 0.001 0.002 0.01; do + echo "density: $d" + $RANDTGBA -a 3 0.0133333 -d $d $opts +done diff --git a/bench/emptchk/models/.cvsignore b/bench/emptchk/models/.cvsignore new file mode 100644 index 000000000..d16d9dc34 --- /dev/null +++ b/bench/emptchk/models/.cvsignore @@ -0,0 +1 @@ +*.tgba diff --git a/bench/emptchk/models/cl3serv1.pml b/bench/emptchk/models/cl3serv1.pml new file mode 100644 index 000000000..532408d7e --- /dev/null +++ b/bench/emptchk/models/cl3serv1.pml @@ -0,0 +1,43 @@ +#define w1 client[0]@wait +#define s1 client[0]@served + +#define C 3 +#define S 1 + +chan clserv = [C] of { int }; +chan servcl = [S] of { int }; + +active [C] proctype client() { + /* the _pid's are: 0 .. C-1 */ + +served: + if + :: (1) -> goto request; + fi; +request: + if + :: (1) -> clserv!_pid; goto wait; + fi; +wait: + if + :: servcl?eval(_pid); goto served; + fi; +} + +active [S] proctype server() { + /* the _pid's are: 0 .. S-1 */ + byte id; + +wait: + if + :: clserv?id -> goto work; + fi; +work: + if + :: (1) -> goto reply; + fi; +reply: + if + :: (1) -> servcl!id; goto wait; + fi; +} diff --git a/bench/emptchk/models/cl3serv3.pml b/bench/emptchk/models/cl3serv3.pml new file mode 100644 index 000000000..ae2e510b0 --- /dev/null +++ b/bench/emptchk/models/cl3serv3.pml @@ -0,0 +1,43 @@ +#define w1 client[0]@wait +#define s1 client[0]@served + +#define C 3 +#define S 3 + +chan clserv = [C] of { int }; +chan servcl = [S] of { int }; + +active [C] proctype client() { + /* the _pid's are: 0 .. C-1 */ + +served: + if + :: (1) -> goto request; + fi; +request: + if + :: (1) -> clserv!_pid; goto wait; + fi; +wait: + if + :: servcl?eval(_pid); goto served; + fi; +} + +active [S] proctype server() { + /* the _pid's are: 0 .. S-1 */ + byte id; + +wait: + if + :: clserv?id -> goto work; + fi; +work: + if + :: (1) -> goto reply; + fi; +reply: + if + :: (1) -> servcl!id; goto wait; + fi; +} diff --git a/bench/emptchk/models/clserv.ltl b/bench/emptchk/models/clserv.ltl new file mode 100644 index 000000000..1ecbfe7fc --- /dev/null +++ b/bench/emptchk/models/clserv.ltl @@ -0,0 +1 @@ +!([] (w1 -> <> s1)) diff --git a/bench/emptchk/models/eeaean.ltl b/bench/emptchk/models/eeaean.ltl new file mode 100644 index 000000000..23666bb82 --- /dev/null +++ b/bench/emptchk/models/eeaean.ltl @@ -0,0 +1,9 @@ +!(<>[](noLeader U zeroLeads)) +!(<>[](noLeader U threeLeads)) +!(<>zeroLeads) +!([]<>zeroLeads) +!(<>threeLeads) +!([](noLeader -> <>zeroLeads)) +!([](noLeader || zeroLeads)) +!((<>[](noLeader || zeroLeads || oneLeads || twoLeads)) && (<>[]((zeroLeads -> (zeroLeads U (noLeader U oneLeads))))) && (<>[]((oneLeads -> (oneLeads U (noLeader U twoLeads))))) && (<>[]((twoLeads -> (twoLeads U (noLeader U zeroLeads)))))) +!((<>[](noLeader || zeroLeads || oneLeads || twoLeads)) && (<>[]((zeroLeads -> (zeroLeads U (noLeader U twoLeads))))) && (<>[]((oneLeads -> (oneLeads U (noLeader U zeroLeads))))) && (<>[]((twoLeads -> (twoLeads U (noLeader U oneLeads)))))) diff --git a/bench/emptchk/models/eeaean2.pml b/bench/emptchk/models/eeaean2.pml new file mode 100644 index 000000000..03828adbe --- /dev/null +++ b/bench/emptchk/models/eeaean2.pml @@ -0,0 +1,118 @@ +/* Echo Election Algorithm with Extinction in an Arbitrary Network. */ +/* Variation 1: Node 0 wins every time. */ + +#define L 10 /* size of buffer */ +#define udef 3 + +#define noLeader (nr_leaders == 0) +#define zeroLeads (nr_leaders == 1 && leader == 0) +#define oneLeads (nr_leaders == 1 && leader == 1) +#define twoLeads (nr_leaders == 1 && leader == 2) +#define threeLeads (nr_leaders == 1 && leader == 3) + +mtype = { tok, ldr }; +chan zero_one = [L] of { mtype, byte}; +chan zero_two = [L] of { mtype, byte}; +chan one_zero = [L] of { mtype, byte}; +chan one_two = [L] of { mtype, byte}; +chan two_zero = [L] of { mtype, byte}; +chan two_one = [L] of { mtype, byte}; + +chan nr0 = [0] of {mtype, byte}; +chan nr1 = [0] of {mtype, byte}; +chan nr2 = [0] of {mtype, byte}; + +byte nr_leaders, done, leader; + +inline recvldr () +{ + if + :: lrec == 0 && r != myid -> + out1!ldr(r); + out2!ldr(r); + :: else -> skip; + fi; + lrec++; + win = r; +} + +inline recvtok (q,c) +{ + if + :: (r+turn)%3 < (caw+turn)%3 -> + caw = r; + rec = 0; + father = q; + c!tok(r); + :: else -> skip; + fi; + + if + :: r == caw -> + rec++; + if + :: rec == 2 && caw == myid + -> out1!ldr(myid); out2!ldr(myid); + :: rec == 2 && caw != myid && father == neigh1 + -> out1!tok(caw) + :: rec == 2 && caw != myid && father == neigh2 + -> out2!tok(caw) + :: else -> skip; + fi; + :: else -> skip; + fi; +} + +proctype node (chan nr; byte neigh1; chan out1, in1; + byte neigh2; chan out2, in2) +{ byte myid = 3 - neigh1 - neigh2; + byte caw, rec, father, lrec, win, r, turn; + + xr in1; xr in2; + xs out1; xs out2; + +restart: + nr?tok(turn); + caw = myid; rec = 0; lrec = 0; + father = udef; win = udef; r = udef; + + out1!tok(myid); + out2!tok(myid); + do + :: lrec == 2 -> break; + :: in1?ldr(r) -> recvldr(); + :: in2?ldr(r) -> recvldr(); + :: in1?tok(r) -> recvtok(neigh1,out2); + :: in2?tok(r) -> recvtok(neigh2,out1); + od; + + if + :: win == myid -> + leader = myid; + nr_leaders++; + assert(nr_leaders == 1); + :: else -> + skip; + fi; + + done++; + goto restart; +} + +init { + byte turn = 0; + atomic { + run node (nr0,1,zero_one,one_zero,2,zero_two,two_zero); + run node (nr1,0,one_zero,zero_one,2,one_two,two_one); + run node (nr2,0,two_zero,zero_two,1,two_one,one_two); + } + do + :: true -> + done = 0; + nr_leaders = 0; + leader = udef; + nr0!tok(turn); nr1!tok(turn); nr2!tok(turn); + done == 3; + turn = (turn+1)%3; + od; +} diff --git a/bench/emptchk/pml-clserv.sh b/bench/emptchk/pml-clserv.sh new file mode 100644 index 000000000..9f410f228 --- /dev/null +++ b/bench/emptchk/pml-clserv.sh @@ -0,0 +1,46 @@ +#!/bin/sh +# Copyright (C) 2005 Laboratoire d'Informatique de Paris 6 (LIP6), +# département Systèmes Répartis Coopératifs (SRC), Université Pierre +# et Marie Curie. +# +# This file is part of Spot, a model checking library. +# +# Spot is free software; you can redistribute it and/or modify it +# under the terms of the GNU General Public License as published by +# the Free Software Foundation; either version 2 of the License, or +# (at your option) any later version. +# +# Spot is distributed in the hope that it will be useful, but WITHOUT +# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +# or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +# License for more details. +# +# You should have received a copy of the GNU General Public License +# along with Spot; see the file COPYING. If not, write to the Free +# Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA +# 02111-1307, USA. + +. ./defs +set -e + +FORMULAE=$srcdir/models/clserv.ltl +ALGORITHMS=$srcdir/algorithms + +opts='-f -x -m' + +for model in cl3serv1.tgba cl3serv1fair.tgba cl3serv3.tgba cl3serv3fair.tgba +do + echo "+++++++++++++++++++++" + echo " $model" + echo "+++++++++++++++++++++" + + cat $FORMULAE | + while read formula; do + echo "-----------------------------------------------------------" + # echo "### formula: $formula" + cat $ALGORITHMS | + while read algo; do + $LTL2TGBA -0 -e$algo $opts -Pmodels/$model "$formula" + done + done +done diff --git a/bench/emptchk/pml-eeaean.sh b/bench/emptchk/pml-eeaean.sh new file mode 100644 index 000000000..3d086d91d --- /dev/null +++ b/bench/emptchk/pml-eeaean.sh @@ -0,0 +1,46 @@ +#!/bin/sh +# Copyright (C) 2005 Laboratoire d'Informatique de Paris 6 (LIP6), +# département Systèmes Répartis Coopératifs (SRC), Université Pierre +# et Marie Curie. +# +# This file is part of Spot, a model checking library. +# +# Spot is free software; you can redistribute it and/or modify it +# under the terms of the GNU General Public License as published by +# the Free Software Foundation; either version 2 of the License, or +# (at your option) any later version. +# +# Spot is distributed in the hope that it will be useful, but WITHOUT +# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +# or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +# License for more details. +# +# You should have received a copy of the GNU General Public License +# along with Spot; see the file COPYING. If not, write to the Free +# Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA +# 02111-1307, USA. + +. ./defs +set -e + +FORMULAE=$srcdir/models/eeaean.ltl +ALGORITHMS=$srcdir/algorithms + +opts='-f -x -m' + +for model in eeaean2.tgba +do + echo "+++++++++++++++++++++" + echo " $model" + echo "+++++++++++++++++++++" + + cat $FORMULAE | + while read formula; do + echo "-----------------------------------------------------------" + echo "### formula: $formula" + cat $ALGORITHMS | + while read algo; do + $LTL2TGBA -0 -e$algo $opts -Pmodels/$model "$formula" + done + done +done diff --git a/bench/emptchk/pml2tgba.pl b/bench/emptchk/pml2tgba.pl new file mode 100755 index 000000000..c2cb71b62 --- /dev/null +++ b/bench/emptchk/pml2tgba.pl @@ -0,0 +1,209 @@ +#!/usr/bin/perl -w +# +# Copyright (C) 2004 Stefan Schwoon +# +# This program is free software; you can redistribute it and/or modify +# it under the terms of the GNU General Public License as published by +# the Free Software Foundation; either version 2 of the License, or +# (at your option) any later version. +# +# This program is distributed in the hope that it will be useful, +# but WITHOUT ANY WARRANTY; without even the implied warranty of +# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +# GNU General Public License for more details. +# +# You should have received a copy of the GNU General Public License +# along with this program; if not, write to the Free Software +# Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307, USA +# +# +# This script was originally distributed by Schwoon alongside with +# +# @InProceedings{ schwoon.05.tacas, +# author = {Stefan Schwoon and Javier Esparza}, +# title = {A note on on-the-fly verification algorithms.}, +# booktitle = {Proceedings of the 11th International Conference on Tools +# and Algorithms for the Construction and Analysis of Systems +# (TACAS'05)}, +# year = {2005}, +# series = {Lecture Notes in Computer Science}, +# publisher = {Springer-Verlag}, +# month = apr +# } +# +# It has been modified in 2005 by Alexandre Duret-Lutz to +# - extract the system's state space instead of the product space +# (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 + +use strict; + +my @prop_list; +my %props; + +sub usage() +{ + print <never.$$"; +print NEVER create_2n_automaton (@ARGV); +close NEVER; + +system "spin -a -N never.$$ \"$model\""; +unlink "never.$$"; +system "gcc -DCHECK -DNOREDUCE -O -o pan pan.c 2>/dev/null"; + +# Match Büchi states to propositions +my $buechitrans = 'BUG'; +open PAN, "./pan -d|"; +while () +{ + last if /^proctype :never/; +} +while () +{ + next + unless (/\s+state\s+\d+\s+-\(tr\s+(\d+)\s*\)->.* line $neverstartline =>/o); + # We are assuming that transition are output by -d in the same order + # as we specified them in the neverclaim. + my $prop = shift @prop_list; + $props{$1} = $prop; +} +close PAN; + +# Build the state graph from pan's DFS output +open PAN, "./pan 2>/dev/null |"; + +my $dfsstate = 0; +my @stack = (); +while () { + last if (/ New state 0/); +} +my %acc = (); +push @stack, [$dfsstate, $buechitrans, %acc]; + +my %allaccs = (); +my %trans_list; +my $prop = "BUG"; +while () { + if (/^\d*: Down/) { + push @stack, [$dfsstate, $buechitrans, %acc]; + } elsif (/^ New state (\d+)/) { + pop @stack; + push (@{$trans_list{$dfsstate}}, ["S$dfsstate, S$1, \"$prop\"", %acc]); + %acc = (); + $dfsstate = $1; + push @stack, [$dfsstate, $buechitrans, %acc]; + } elsif (/^ (Old|Stack) state (\d+)/) { + push (@{$trans_list{$dfsstate}}, ["S$dfsstate, S$2, \"$prop\"", %acc]); + %acc = (); + } elsif (/^ *\d+: proc 0 exec (\d+), \d+ to \d+/) { + $buechitrans = $1; + $prop = $props{$buechitrans}; + } elsif (/^ *\d+: proc (\d+) exec \d+, \d+ to \d+/) { + $acc{"PR$1"} = 1; + $allaccs{"PR$1"} = 1; + } elsif (/^\d*: Up/) { + pop @stack; + ($dfsstate, $buechitrans, %acc) = @{$stack[$#stack]}; + $prop = $props{$buechitrans}; + } +} +close PAN; + +unlink "pan", "pan.exe", "pan.c", "pan.h", "pan.b", "pan.t", "pan.m"; + + +print "acc = @{[sort keys %allaccs]};\n" if $weak; +for my $state (sort {$a <=> $b} (keys %trans_list)) +{ + my %missing = %allaccs; + for my $t (@{$trans_list{$state}}) + { + my ($trans, %acc) = @$t; + for my $key (keys %acc) + { + delete $missing{$key}; + } + } + for my $t (@{$trans_list{$state}}) + { + my ($trans, %acc) = @$t; + print "$trans,"; + print " @{[sort keys(%acc)]} @{[sort keys(%missing)]}" if $weak; + print ";\n"; + } +} +exit 0; + +### Setup "GNU" style for perl-mode and cperl-mode. +## Local Variables: +## perl-indent-level: 2 +## perl-continued-statement-offset: 2 +## perl-continued-brace-offset: 0 +## perl-brace-offset: 0 +## perl-brace-imaginary-offset: 0 +## perl-label-offset: -2 +## cperl-indent-level: 2 +## cperl-brace-offset: 0 +## cperl-continued-brace-offset: 0 +## cperl-label-offset: -2 +## cperl-extra-newline-before-brace: t +## cperl-merge-trailing-else: nil +## cperl-continued-statement-offset: 2 +## End: diff --git a/configure.ac b/configure.ac index 8d54c3974..148d72fcb 100644 --- a/configure.ac +++ b/configure.ac @@ -1,4 +1,4 @@ -# Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), +# Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), # département Systèmes Répartis Coopératifs (SRC), Université Pierre # et Marie Curie. # @@ -55,11 +55,16 @@ adl_ENABLE_DEBUG ad_GCC_OPTIM adl_NDEBUG +AM_CONDITIONAL([NEVER], [false]) AC_CHECK_PROG([DOT], [dot], [dot]) +AC_CHECK_PROG([PERL], [perl], [perl]) AC_CHECK_PROG([VALGRIND], [valgrind], [valgrind]) AC_CONFIG_FILES([ Makefile + bench/Makefile + bench/emptchk/Makefile + bench/emptchk/defs doc/Doxyfile doc/Makefile iface/Makefile