Directed Model Checking for PROMELA
with Relaxation-Based Distance Functions

SPIN 2015 Supporting Material

This page provides supporting material for the paper Directed Model Checking for PROMELA with Relaxation-Based Distance Functions, submitted to 22nd Symposium on Model Checking of Software (SPIN 2015).

Grammar for Supported PROMELA Subset

grammar.pdf

1. Scatter Plot PDFs

Click on images to download PDF.

2. Figures and PROMELA Models


modeldist. fun.rangestatestrailtime (s)memory (MByte)
adding.1 c: [0..1] 1632 44 0.182.09
L: [0..10] 32 37 0.171.84
adding.4 c: [0..1] 845235 110 27.40132.00
L: [0..18] 12861 110 0.273.83
adding.5 c: [0..1] 1326148 91 68.40207.00
L: [0..18] 5124 89 0.222.58
adding.6 c: [0..1] 1907378 117 152.00297.00
L: [0..18] 29749 117 0.406.31
bakery.10 c: [0..1] 823 497 0.192.10
L: [0..16] 336 263 0.261.97
bakery.2 c: [0..1] 106 185 0.171.84
L: [0..14] 98 122 0.191.84
bakery.4 c: [0..1] 253 273 0.181.84
L: [0..15] 344 147 0.211.97
bakery.6 c: [0..1] 486 377 0.181.97
L: [0..17] 1320 298 0.442.22
bakery.9 c: [0..1] 486 377 0.191.97
L: [0..17] 1320 298 0.452.22
blocks.1 c: [0..1] 44 151 0.181.97
L: [0..20] 25 73 0.181.84
blocks.3 c: –––––
L: [0..20] 320402 27529 326.00122.00
bopdp.1 c: [0..3] 353 176 0.181.97
L: [0..39] 88 89 0.191.84
bopdp.2 c: [0..3] 6474 4178 0.253.65
L: [0..39] 92 84 0.191.84
bopdp.3 c: [0..3] 528 575 0.202.09
L: [0..39] 222 113 0.201.97
bridge.1 c: [0..1] 1482 101 0.192.21
L: [0..8] 150 64 0.201.84
bridge.2 c: [0..1] 12167 203 0.605.58
L: [0..10] 597 97 0.522.34
bridge.3 c:– – – ––
L: [0..12] 2083 131 23.7026.00
brp.2 c: [0..1] 8974 7316 0.294.87
L: [0..12] 956 137 0.342.20
brp.3 c: [0..1] 80441 46474 1.1129.00
L: [0..12] 5496 187 1.033.65
brp.4 c: [0..1] 302971 153304 3.70107.00
L: [0..12] 20536 287 3.458.86
brp.5 c: [0..1] 440281 218804 5.31156.00
L: [0..12] 30076 387 5.1212.00
brp.6 c: [0..1] 521294 254584 6.52184.00
L: [0..12] 35138 317 5.8613.00
elevator_planning.1 c: [0..1] 2605 3734 0.242.46
L: [0..10] 322 190 0.321.84
elevator_planning.2 c: –––––
L: [0..10] 31625 4310 10.3010.00
elevator_planning.3 c: [0..1] 47741 34824 0.6511.00
L: [0..6] 231 150 0.191.84
krebs.1 c: [0..1] 148 187 0.181.84
L: [0..10] 31 43 0.201.84
krebs.2 c: [0..1] 310 426 0.181.97
L: [0..25] 200 282 0.221.84
krebs.5 c: [0..1] 23677 628 0.8011.00
L: [0..47] 12838 588 14.807.27
lamport.1 c: [0..1] 93 86 0.171.84
L: [0..17] 93 34 0.201.84
lamport.2 c: [0..1] 93 88 0.191.84
L: [0..17] 93 34 0.181.84
lamport.3 c: [0..1] 554 168 0.181.97
L: [0..262] 93 34 0.181.84
lamport.5 c: [0..1] 130 90 0.191.84
L: [0..18] 282 40 0.181.84
lamport.6 c: [0..1] 130 92 0.181.84
L: [0..18] 282 40 0.191.84
lamport.7 c: [0..1] 169 94 0.181.84
L: [0..19] 1387 46 0.242.09
lamport.8 c: [0..1] 34162 204 0.528.92
L: [0..262] 1387 46 0.382.09
peterson.2 c: [0..1] 1071 1378 0.182.09
L: [0..13] 567 220 0.221.97
peterson.3 c: [0..1] 239 273 0.201.84
L: [0..13] 208 224 0.201.84
peterson.5 c: [0..1] 10669 10828 0.234.71
L: [0..14] 5544 5084 0.503.08
peterson.6 c: [0..1] 1667 1584 0.192.22
L: [0..14] 537 482 0.231.97
phils.1 c: [0..1] 25 24 0.251.84
L: [0..4] 16 14 0.211.84
phils.2 c: [0..1] 202 186 0.181.84
L: [0..6] 46 31 0.191.84
phils.3 c: [0..1] 182 140 0.181.84
L: [0..5] 42 25 0.181.84
phils.4 c: [0..1] 25282 9180 0.287.20
L: [0..6] 7485 2570 0.453.47
phils.5 c: [0..1] 30006 10963 0.348.55
L: [0..4] 116 38 0.181.84
phils.6 c: [0..1] 229875 66667 1.1756.00
L: [0..4] 178 47 0.181.84
phils.7 c: [0..1] 3107767 806978 16.10721.00
L: [0..6] 740007 172483 35.10176.00
phils.8 c: [0..1] 553128 149370 2.02138.00
L: [0..4] 202 50 0.191.84
production_cell.1 c: [0..1] 2 4 0.181.84
L: [0..1] 2 4 0.201.84
production_cell.2 c: [0..1] 418 480 0.181.97
L: [0..12] 418 480 0.221.97
production_cell.3 c: [0..1] 2 4 0.191.84
L: [0..1] 2 4 0.181.84
production_cell.4 c: [0..1] 392 418 0.202.08
L: [0..11] 393 418 0.242.09