1This directory contains the input files and scripts used to produce 2the measures in our paper "On-the-fly Emptiness Checks for Generalized 3B�chi Automata" (J.-M. Couvreur, A. Duret-Lutz, D. Poitrenaud), 4submitted to Spin'05. 5 6========== 7 CONTENTS 8========== 9 10This directory contains: 11 12* models/cl3serv1.pml 13* models/cl3serv3.pml 14 15 Two simple client/server promela examples. 16 17* models/clserv.ltl 18 19 An LTL formula to verify on these examples. 20 21* models/eeaean1.pml 22* models/eeaean2.pml 23 24 Variations of the leader election protocol with extinction from 25 Tel, Introduction to Distributed Algorithms, 1994, Chapter 7. The 26 network in the model consists of three nodes. In Variant 1, the 27 same node wins every time, in Variant 2, each node gets a turn at 28 winning the election. These specifications were originally 29 distributed alongside 30 31 @InProceedings{ schwoon.05.tacas, 32 author = {Stefan Schwoon and Javier Esparza}, 33 title = {A note on on-the-fly verification algorithms.}, 34 booktitle = {Proceedings of the 11th International Conference 35 on Tools and Algorithms for the Construction and 36 Analysis of Systems 37 (TACAS'05)}, 38 year = {2005}, 39 series = {Lecture Notes in Computer Science}, 40 publisher = {Springer-Verlag}, 41 month = apr 42 } 43 44 We only presented results for the second model in the paper. 45 46* models/eeaean.ltl 47 48 Sample properties for the leader election protocols. These come from 49 50 @InProceedings{ geldenhuys.04.tacas, 51 author = {Jaco Geldenhuys and Antti Valmari}, 52 title = {Tarjan's Algorithm Makes On-the-Fly {LTL} Verification 53 More Efficient}, 54 booktitle = {Proceedings of the 10th International Conference on 55 Tools and Algorithms for the Construction and Analysis 56 of Systems 57 (TACAS'04)}, 58 editor = {Kurt Jensen and Andreas Podelski}, 59 pages = {205--219}, 60 year = {2004}, 61 publisher = {Springer-Verlag}, 62 series = {Lecture Notes in Computer Science}, 63 volume = {2988}, 64 isbn = {3-540-21299-X} 65 } 66 67* formulae.ltl 68 69 A list of 96 handwritten formulae with their negations. They come 70 from three sources: 71 72 @InProceedings{ dwyer.98.fmsp, 73 author = {Matthew B. Dwyer and George S. Avrunin and James C. 74 Corbett}, 75 title = {Property Specification Patterns for Finite-state 76 Verification}, 77 booktitle = {Proceedings of the 2nd Workshop on Formal Methods in 78 Software Practice (FMSP'98)}, 79 publisher = {ACM Press}, 80 address = {New York}, 81 editor = {Mark Ardis}, 82 month = mar, 83 year = {1998}, 84 pages = {7--15} 85 } 86 87 @InProceedings{ etessami.00.concur, 88 author = {Kousha Etessami and Gerard J. Holzmann}, 89 title = {Optimizing {B\"u}chi Automata}, 90 booktitle = {Proceedings of the 11th International Conference on 91 Concurrency Theory (Concur'00)}, 92 pages = {153--167}, 93 year = {2000}, 94 editor = {C. Palamidessi}, 95 volume = {1877}, 96 series = {Lecture Notes in Computer Science}, 97 address = {Pennsylvania, USA}, 98 publisher = {Springer-Verlag} 99 } 100 101 @InProceedings{ somenzi.00.cav, 102 author = {Fabio Somenzi and Roderick Bloem}, 103 title = {Efficient {B\"u}chi Automata for {LTL} Formul{\ae}}, 104 booktitle = {Proceedings of the 12th International Conference on 105 Computer Aided Verification (CAV'00)}, 106 pages = {247--263}, 107 year = {2000}, 108 volume = {1855}, 109 series = {Lecture Notes in Computer Science}, 110 address = {Chicago, Illinois, USA}, 111 publisher = {Springer-Verlag} 112 } 113 114 115* pml2tgba.pl 116 117 A Perl script to translate Promela models into TGBA readable by Spot. 118 This requires a working spin in PATH. 119 120* ltl-random.sh 121 122 Use all emptiness-check algorithms to test random graphs against 123 random LTL formulae. 124 125* ltl-human.sh 126 127 Use all emptiness-check algorithms to test random graphs against 128 all the formulae of the file `formulae.ltl' 129 130* pml-clserv.sh 131 132 Check the two configurations of the client/server example against 133 the formula in models/clserv.ltl, without and with fairness 134 assumptions, using all the algorithms of the file `algorithms'. 135 You should have run `make' before attempting to run this script, 136 so the state space are available. 137 138* pml-eeaean.sh 139 140 Check models/eeaean1.pml and models/eeaean2.pml against each 141 formulae in models/eeaean.ltl, using all the algorithms of the 142 file `algorithms'. You should have run `make' before attempting to 143 run this script, so the state space are available. 144 145* algorithms 146 147 The list of emptiness-check algorithms run by the above tests. 148 (See http://spot.lip6.fr/wiki/EmptinessCheckOptions for the syntax.) 149 150======= 151 USAGE 152======= 153 154 0. Install Spin (spinroot.com), and make sure the `spin' binary is in 155 your path. 156 157 1. If that is not done already, configure and compile all the Spot 158 library, then come back into this directory. 159 160 2. Run `make' in this directory. This will call pml2tgba.pl to 161 generate the TGBA input for the two pml-*.sh tests. 162 163 Promela inputs are translated in 4 different graphs. 164 For instance eeaean1.pml is translated as 165 - eeaean1.tgba full translation 166 - eeaean1fair.tgba full translation with weak fairness 167 - eeaean1R.tgba reduced translation 168 - eeaean1Rfair.tgba reduced translation with weak fairness 169 The "reduced" translation uses Spin's partial order reductions. 170 171 (The "R"educed variants are not shown in the paper.) 172 173 3. Run the tests you are interested in 174 175 - ltl-random.sh 176 - ltl-human.sh 177 - pml-clserv.sh 178 - pml-eeaean.sh 179 180 Beware that the two ltl-*.sh tests are very long (each of them 181 run 13 emptiness-check algorithms against 18000 product-spaces!). 182 Running ltl-random.sh took 4 hours on a 3GHz Intel Pentium 4, 183 and ltl-human.sh took 9 hours. 184 185 You can speed up all tests by removing some algorithms from the 186 `algorithms' file. 187 188========================== 189 INTERPRETING THE RESULTS 190========================== 191 192 Here are the short names for the algorithms presented in the outputs. 193 194 Cou99 195 Cou99(shy !group) 196 Cou99(shy group) 197 Cou99(shy group2) 198 > Cou99(poprem) # called `Cou99' in the paper 199 > Cou99(poprem shy !group) # called `Cou99 Shy-' in the paper 200 Cou99(poprem shy group) 201 > Cou99(poprem shy group2) # called `Cou99 Shy' in the paper 202 > CVWY90 203 > GV04 204 > SE05 205 > Tau03 206 > Tau03_opt 207 208 Only the algorithms marked with a `>' have been shown in the paper. 209 210 `Cou99(poprem*)' algorithms are using the `rem' field to remove the 211 SCC without recomputing the SCC as described in the paper. The 212 other `Cou99' algorithms are not. (Beware that in the paper we 213 presented the `Cou99(poprem*)' variants and called them `Cou99*'.) 214 215 (See also http://spot.lip6.fr/wiki/EmptinessCheckOptions) 216 217 218 The ltl-*.sh tests output look as follows: 219 220 | density: 0.001 221 | Emptiness check ratios 222 | Cou99 18.9 9.6 10.4 29 223 | Cou99(shy !group) 16.7 16.3 25.7 29 224 | ... 225 (A) (B) (C) (D) 226 | 227 | Accepting run ratios 228 | Cou99 8.6 13.5 229 | Cou99(shy !group) 7.3 12.2 230 | ... 231 (E) (F) 232 233 (A) mean number of distinct states visited 234 expressed as a % of the number of state of the product space 235 (B) mean number of distinct transitions visited 236 expressed as a % of the number of transition of the product space 237 (C) mean of the maximal stack size 238 expressed as a % of the number of state of the product space 239 (D) number of non-empty automata used for these statistics 240 (E) mean number of states in the search space for accepting runs 241 expressed as a % of the number of state of the product space 242 (F) mean number of states visited (possibly several times) while 243 computing the accepting run 244 expressed as a % of the number of state of the product space 245 246 247 The pml-*.sh tests output look as follows: 248 249 | Cou99 , 92681, 391160, 1, 92681, 391160, 46471, no accepting run found 250 | Cou99(shy !group) , 92681, 391160, 1, 92681, 391160, 47148, no accepting run found 251 | ... 252 (G) (H) (I) (K) (L) (M) (N) 253 254 (G) Number of states in the product. 255 (H) Number of transitions in the product. 256 (I) Number of acceptance conditions in the product. 257 (K) Number of distinct states visited by the emptiness-check algorithm. 258 (L) Number of transitions visited by the emptiness-check algorithm. 259 (M) Maximal size of the stack. 260 (N) Whether an accepting run was found. 261 262 263================= 264 MORE STATISTICS 265================= 266 267 The ltl-*.sh tests use spot/tests/randtgba to output statistics, 268 but randtgba is able to output a lot more data than what we have 269 shown above. Try removing the `-1' option from the script, or toying 270 with randtgba itself. 271 272 CVWY90 and SE05 have bit-state hashing implementations. Edit the 273 file `algorithms' and add lines like `CVWY90(bsh=5M)' or 274 `SE05(bsh=512K)' to try these. 275 (The `bsh=' argument gives the hash table size in bytes; see also 276 http://spot.lip6.fr/wiki/EmptinessCheckOptions) 277 278 Besides randtgba, two other tools that you might find handy when 279 experimenting are bin/randltl and tests/core/ikwiad. 280