README.md



Benchmarks

Execution
Executing benchmarks is done by executing make in each of the directories.

Technical Data

Java: Java HotSpot(TM) 64-Bit Server VM (build 12.0.1+12,mixed mode, sharing)
C++ Compiler: Apple LLVM version 10.0.1 (clang-1001.0.46.4) with -O1 and -O2
ProB: 1.9.0-nightly (c5a6e9d31022d0bfe40cbcdf68e910041665ec41)
B2Program Commit: edce3cc7

Device: MacBook Air with 8 GBof RAM and a 1.6 GHz Intel i5 processor with two cores


Results


Machines

ProB
Java BI
Java PI
C++ PI -O1
C++ PI -O2


Lift
Runtime
> 1800
156.63
27.43
78.42
0.00


Speedup
1
> 11.49
> 65.62
> 22.95
> 180 000


Memory
-
735 188
785 628
756
736


TrafficLight
Runtime
> 1800
47.04
9.05
69.09
0.00


Speedup
1
> 38.27
> 198.9
> 26.05
> 180 000


Memory
-
855 112
447 828
756
736


Sieve
Runtime
76.31
7.71
6.49
14.63
8.94


Speedup
1
9.9
11.76
5.22
8.54


Memory
398 980
1 415 428
1 096 284
32 472
35 732


Scheduler
Runtime
786.74
10.62
10.49
21.57
10.32


Speedup
1
74.08
74.99
36.47
76.23


Memory
5 341 316
414 772
398 924
816
820


sort_m2_data1000
Runtime
17.27
3.27
2.10
0.2
0.03


Speedup
1
5.28
8.22
86.35
575.67


Memory
577 808
191 280
143 864
1192
1104


CAN Bus
Runtime
273.58
7.23
6.81
7.23
2.91


Speedup
1
37.84
40.17
37.84
94.01


Memory
167 284
428 084
402 432
968
952


Train
Runtime
241.16
13.31
12.83
18.55
8.10


Speedup
1
18.11
18.8
13
29.77


Memory
163 476
377 292
376 540
984
1016


Cruise Controller
Runtime
> 1800
21.26
15.26
11.90
0.30


Speedup
1
> 84.67
> 117.96
> 151.26
> 6000


Memory
-
750 816
484 948
864
820


Runtime in Seconds
Memory Usage in KB
BI = Big Integer
PI = Primitive Integer