Directed Model Checking for B: An Evaluation and New Techniques - Formal Methods: Foundations and Applications - page 14

Table 5. Relative times for checking models with deadlocks (Heuristics Analysis)

Deadlock Benchmarks DF33 (abs+rel) HashRand OutDegree OutDegHash TermSi ze
Abrial Earley3 v3

270 ms 1.00 0.74 1.22 0.70 1.22

Abrial Earley3 v5 4320 ms 1.00 0.41 5.88 0.16 7.95

Abrial Earley4 v3 90 ms 1.00 0.89 1.00 0.89 1.00

Alstom axl3 51270 ms 1.00 0.82 0.09 0.16 0.08

Alstom ex7 856320 ms 1.00 0.55 ** 1.91 1.10 **1.57

Bosch CrsCtl 3ms1.00 8.00 1.00 1.00 4.00

SAP MChoreography 20 ms 1.00 0.50 0.50 0.50 1.00

DiningPhil 1690 ms 1.00 1.16 0.05 0.03 1.59

CXCC0 10 ms 1.00 0.25 0.25 0.25 0.25

GEOMEAN 432 ms 1.00 0.80 0.58 0.34 1.07

Table 6. Relative times for checking models with goals to be found (Heuristics)

Goal DF33 HashRand OutDegree OutDeg- TermSi ze CUSTOM

Benchmarks (abs+rel) Hash

RussianPostal 220 ms 1 0.45 0.77 0.36 1.18 0.45

TrainTorch 350 ms 1 0.97 0.26 1.14 0.20 0.20

BlocksWorld 440 ms 1 1.16 0.07 0.07 1.20 0.02

Farmer 20 ms 1 1.00 1.00 0.50 1.00 1.00

Hanoi 500 ms 1 0.52 0.92 0.52 0.90 0.34

Puzzle8 59060 ms 1 20.54 1.31 2.69 0.71 0.03

RushHour 127020 ms 1 0.42 0.60 0.56 1.12 0.79

Abrial Press m13 800 ms 1 0.49 2.36 2.21 2.48 0.20

Abrial Queue m1 50 ms 1 0.40 16.60 0.60 2.80 0.40

SystemOnChip... 2050 ms 1 0.10 0.05 0.04 1.50 72.42

Wegenetz 120 ms 1 0.17 0.33 0.08 0.08 0.08

GEOMEAN 715 ms 1 0.64 0.63 0.41 0.85 0.34