README 8.83 KB
Newer Older
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
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
=======

147
148
149
150
151
  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
     library, then come back into this directory.
152
153
154
155
156
157
158
159
160
161
162
163

  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
164
165
166
     run 13 emptiness-check algorithms against 18000 product-spaces!).
     Running ltl-random.sh took 4 hours on a 3GHz Intel Pentium 4,
     and ltl-human.sh took 9 hours.
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267

     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.