diff --git a/ChangeLog b/ChangeLog index e526c25f0..92dc644fa 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,5 +1,13 @@ 2005-02-02 Alexandre Duret-Lutz + * bench/emptchk/models/eeaean1.pml: New file, from schwoon.05.tacas. + * bench/emptchk/Makefile.am: Distribute models/eeaean1.pml + and build models/eeaean1.tgba. + * bench/emptchk/pml-eeaean.sh: Check models/eeaean1.pml. + * bench/emptchk/README: Adjust. + * bench/emptchk/defs.in (RANDTGBA, LTL2TGBA): These tools are in + the build tree, not the source tree... + These tests are huge, and are obsoleted by randtgba-based checks, and by bench/emptchk/. * src/tgbatest/tba_samples_from_spin.test: Delete. diff --git a/bench/emptchk/Makefile.am b/bench/emptchk/Makefile.am index 0e9d1c4e6..ca4141117 100644 --- a/bench/emptchk/Makefile.am +++ b/bench/emptchk/Makefile.am @@ -34,6 +34,7 @@ dist_noinst_DATA = \ models/cl3serv1.pml \ models/cl3serv3.pml \ models/clserv.ltl \ + models/eeaean1.pml \ models/eeaean2.pml \ models/eeaean.ltl \ formulae.ltl \ @@ -44,6 +45,7 @@ nodist_noinst_DATA = \ models/cl3serv1fair.tgba \ models/cl3serv3.tgba \ models/cl3serv3fair.tgba \ + models/eeaean1.tgba \ models/eeaean2.tgba models/cl3serv1.tgba: $(srcdir)/models/cl3serv1.pml @@ -62,6 +64,11 @@ models/cl3serv3fair.tgba: $(srcdir)/models/cl3serv3.pml $(mkdir_p) models $(PML2TGBA) -w $(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/eeaean2.tgba: $(srcdir)/models/eeaean2.pml $(mkdir_p) models $(PML2TGBA) $(srcdir)/models/eeaean2.pml \ diff --git a/bench/emptchk/README b/bench/emptchk/README index 6e0ae17dd..3e2d78b3f 100644 --- a/bench/emptchk/README +++ b/bench/emptchk/README @@ -18,14 +18,15 @@ This directory contains: An LTL formula to verify on these examples. +* models/eeaean1.pml * models/eeaean2.pml - A variations of the leader election protocol with extinction from + 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 + winning the election. These specifications were originally + distributed alongside @InProceedings{ schwoon.05.tacas, author = {Stefan Schwoon and Javier Esparza}, @@ -40,6 +41,8 @@ This directory contains: month = apr } + We only presented results for the second model in the paper. + * models/eeaean.ltl Sample properties for the leader election protocols. These come from @@ -134,10 +137,10 @@ This directory contains: * 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. + 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 + run this script, so the state space are available. ======= diff --git a/bench/emptchk/defs.in b/bench/emptchk/defs.in index 03405833e..35ab0706b 100644 --- a/bench/emptchk/defs.in +++ b/bench/emptchk/defs.in @@ -34,6 +34,6 @@ test -f "$srcdir/defs.in" || { exit 1 } -RANDTGBA='@top_srcdir@/src/tgbatest/randtgba@EXEEXT@' -LTL2TGBA='@top_srcdir@/src/tgbatest/ltl2tgba@EXEEXT@' +RANDTGBA='@top_builddir@/src/tgbatest/randtgba@EXEEXT@' +LTL2TGBA='@top_builddir@/src/tgbatest/ltl2tgba@EXEEXT@' FORMULAE=$srcdir/formulae.ltl diff --git a/bench/emptchk/models/eeaean1.pml b/bench/emptchk/models/eeaean1.pml new file mode 100644 index 000000000..f4d0d3133 --- /dev/null +++ b/bench/emptchk/models/eeaean1.pml @@ -0,0 +1,116 @@ +/* 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}; +chan nr1 = [0] of {mtype}; +chan nr2 = [0] of {mtype}; + +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 < caw -> + 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; + + xr in1; xr in2; + xs out1; xs out2; + +restart: + nr?tok; + 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 { + 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; nr1!tok; nr2!tok; + done == 3; + od; +} diff --git a/bench/emptchk/pml-eeaean.sh b/bench/emptchk/pml-eeaean.sh index 3d086d91d..010cb96c2 100644 --- a/bench/emptchk/pml-eeaean.sh +++ b/bench/emptchk/pml-eeaean.sh @@ -28,7 +28,7 @@ ALGORITHMS=$srcdir/algorithms opts='-f -x -m' -for model in eeaean2.tgba +for model in eeaean1.tgba eeaean2.tgba do echo "+++++++++++++++++++++" echo " $model"