Commit f22b59bf authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

* 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...
parent 2b68284d
2005-02-02 Alexandre Duret-Lutz <adl@src.lip6.fr>
* 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.
......
......@@ -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 \
......
......@@ -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.
=======
......
......@@ -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
/* 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;
}
......@@ -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"
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment