Babylon: Some preliminary results


On this page, you fill find some experimental collected thanks to Babyon, our integrated model-checker. For more information about Babylon, see here !

We tried a few examples, taken from our example list. As Babylon only works on Petri nets for the moment, they are only bounded or unbounded Petri nets.

For each of the examples, you will find:
Up to now, we let the examples run on two of the three algorithms that are presented on the Babylon homepage.

For each examples, you have access to the HTML file generated by Babylon. It contains all the details of the results.

Contents of this page:


Results with algorithm 1: Plain Backward Search

Number of iterations:

Example
IST
DDD
NDD
CST
Lamport
10
10
10

Peterson
9
9
9

Mesh3x2
21
21


CSM
11
11
11

MultiPool
18
18


Execution time (sec.):

Example
IST
DDD
NDD
CST
Lamport
0.15
0.19
134.77

Peterson
0.47
0.77
2246.52

Mesh3x2
810.55
195.15


CSM
0.54
0.84
247.3

MultiPool
10.97
3.55


Memory Usage:

Example
IST
DDD
NDD
CST
Lamport
2'196 kB, at iteration 6
75'376 kB, at iteration 5
7'232 kB, at iteration 5

Peterson
2'228 kB, at iteration 5
75'424 kB, at iteration 8
22'312 kB, at iteration 7

Mesh3x2
7'380 kB, at iteration 13
76'364 kB, at iteration 21


CSM
2'228 kB, at iteration 7
75'424 kB, at iteration 8
7'820 kB, at iteration 6

MultiPool
2'720 kB at iteration 12
75'568 kB, at iteration 10


Bottleneck operation (+percentage of the time consumed):

Example
IST
DDD
NDD
CST
Lamport
Union (57.14 %)
Pre (73.33 %)
Pre (88.58 %)

Peterson
Union (62.22 %)
Pre (63.89 %)
Pre (92.61 %)

Mesh3x2
Union (93.47 %)
Union (73.21 %)


CSM
Union (69.23 %)
Pre (44.19 %)
Pre (85.18 %)

MultiPool
Union (69.73 %)
Union (50.32 %)


Results with algorithm 3: Fully Symbolic Backward Search

Number of iterations:

Example
IST
DDD
NDD
CST
Lamport
10
10
10

Peterson
9
9
9

Mesh3x2
21
21


CSM
11
11
11

MultiPool
18
18


Execution time (sec.):

Example
IST
DDD
NDD
CST
Lamport
0.11
0.54
140.24

Peterson
0.35
0.77
2219.1

Mesh3x2
483.4
194.79


CSM
0.39
0.82
235.8

MultiPool
9.12
3.49


Memory Usage:

Example
IST
DDD
NDD
CST
Lamport
2'184 kB, at iteration 6
75'376 kB, at iteration 5
72'40 kB, at iteration 6

Peterson
2'540 kB, at iteration 8
75'424 kB, at iteration 8
22'128 kB, at iteration 5

Mesh3x2
5'8096 kB, at iteration 21
76'208 kB, at iteration 21


CSM
2'540 kB, at iteration 6
75'420 kB, at iteration 8
8'232 kB, at iteration 7

MultiPool
8'824 kB, at iteration 15
75'564 kB, at iteration 10


Bottleneck operation (+percentage of the time consumed):

Example
IST
DDD
NDD
CST
Lamport
Pre (60.00 %)
Pre (76.92 %)
Pre (98.07 %)

Peterson
Pre (78.79 %)
Pre (88.57 %)
Pre (98.86 %)

Mesh3x2
Pre (92.82 %)
Pre (95.18 %)


CSM
Pre (83.78 %)
Pre (90.24 %)
Pre (98.18 %)

MultiPool Pre (87.69 %)
Pre (94.10 %)


Description of the examples

For more details about the examples as well as the exact specifications we used, see the Example page.

Lamport


Peterson

Mesh3x2

CSM

MultiPool


Last update: Wed Feb 20 23:00:00 CET 2002