diff --git a/benchmarks/model_checking/README.md b/benchmarks/model_checking/README.md index a5e76b0ecf8c38d668aea4101f7980f2d080f180..4161725bfc4dee5bd3097de03917283db82c6995 100644 --- a/benchmarks/model_checking/README.md +++ b/benchmarks/model_checking/README.md @@ -60,35 +60,35 @@ Executing benchmarks is done by executing ``make`` in each of the directories. #### System B -| Machines | | ProB OP | ProB ST | Java | C++ -O1 | C++ -O2 | Rust | -|-------------------|----------|---------|---------|------------------------|---------|---------|-----------------------| -| Lift_MC_Large | Runtime | | | 2.23 / 2.7 | | | 00.42 / 00.50 | -| | Speed-up | | | | | | | -| | Memory | | | 700.824 / 721.548 | | | 54.734 / 54.742 | -| Cruise Controller | Runtime | | | 1.73 / 2.28 | | | 00.07 / 00.18 | -| | Speed-up | | | | | | | -| | Memory | | | 159.292 / 161.860 | | | 5011 / 5226 | -| Landing Gear | Runtime | | | 11.16 / 13.52 | | | 09.84 / 19.23 | -| | Speed-up | | | | | | | -| | Memory | | | 1.063.784 / 1.352.408 | | | 734.749 / 854.914 | -| CAN BUS | Runtime | | | 3.79 / 4.47 | | | 02.3 / 02.45 | -| | Speed-up | | | | | | | -| | Memory | | | 542.680 / 1.080.708 | | | 1.012.179 / 1.049.515 | -| Train1_Lukas | Runtime | | | 13.0 / 12.25 | | | 07.08 / 07.14 | -| | Speed-up | | | | | | | -| | Memory | | | 701.600 / 1.044.600 | | | 187.201 / 255.626 | -| Train_1_beebook | Runtime | | | 626.39 / 545.66 | | | 445.79 / 416.89 | -| | Speed-up | | | | | | | -| | Memory | | | 1.451.340 / 3.110.416 | | | 4.735.570 / 6.047.158 | -| nota | Runtime | | | 10.75 / 9.58 | | | 20.12 / 20.77 | -| | Speed-up | | | | | | | -| | Memory | | | 1.201.656 / 1.512.316 | | | 1.321.891 / 1.269.008 | -| sort_1000 | Runtime | | | 988.25 / 85.87 | | | 516 / 95.12 | -| | Speed-up | | | | | | | -| | Memory | | | 1.202.264 / 1.361.680 | | | 269.996 / 269.939 | -| N Queens (N=4) | Runtime | | | 34.41 / 35.73 | | | 22.34 / 22.74 | -| | Speed-up | | | | | | | -| | Memory | | | 511.568 / 503.032 | | | 345.376 / 345.386 | +| Machines | | ProB OP | ProB ST | Java | C++ -O1 | C++ -O2 | Rust | +|-------------------|----------|---------|---------|------------------------|---------|-----------------------|-----------------------| +| Lift_MC_Large | Runtime | | | 2.23 / 2.7 | | 0.74 / 00.96 | 00.42 / 00.50 | +| | Speed-up | | | | | | | +| | Memory | | | 700.824 / 721.548 | | 250.388 / 250.405 | 54.734 / 54.742 | +| Cruise Controller | Runtime | | | 1.73 / 2.28 | | 0.11 / 00.12 | 00.07 / 00.18 | +| | Speed-up | | | | | | | +| | Memory | | | 159.292 / 161.860 | | 6.310 / 6.489 | 5011 / 5226 | +| Landing Gear | Runtime | | | 11.16 / 13.52 | | 8.79 / 9.59 | 09.84 / 19.23 | +| | Speed-up | | | | | | | +| | Memory | | | 1.063.784 / 1.352.408 | | 329.672 / 332.976 | 734.749 / 854.914 | +| CAN BUS | Runtime | | | 3.79 / 4.47 | | 1.71 / 2.02 | 02.3 / 02.45 | +| | Speed-up | | | | | | | +| | Memory | | | 542.680 / 1.080.708 | | 316.873 / 326.791 | 1.012.179 / 1.049.515 | +| Train1_Lukas | Runtime | | | 13.0 / 12.25 | | 4.93 / 2.31 | 07.08 / 07.14 | +| | Speed-up | | | | | | | +| | Memory | | | 701.600 / 1.044.600 | | 59.299 / 62.798 | 187.201 / 255.626 | +| Train_1_beebook | Runtime | | | 626.39 / 545.66 | | 311.83 / 135.69 | 445.79 / 416.89 | +| | Speed-up | | | | | | | +| | Memory | | | 1.451.340 / 3.110.416 | | 1.559.626 / 1.667.335 | 4.735.570 / 6.047.158 | +| nota | Runtime | | | 10.75 / 9.58 | | 22.43 / 21.4 | 20.12 / 20.77 | +| | Speed-up | | | | | | | +| | Memory | | | 1.201.656 / 1.512.316 | | 280.518 / 413.597 | 1.321.891 / 1.269.008 | +| sort_1000 | Runtime | | | 988.25 / 85.87 | | 1424.95 / 1251.89 | 516 / 95.12 | +| | Speed-up | | | | | | | +| | Memory | | | 1.202.264 / 1.361.680 | | 338.626 / 342.083 | 269.996 / 269.939 | +| N Queens (N=4) | Runtime | | | 34.41 / 35.73 | | 27.79 / 27.16 | 22.34 / 22.74 | +| | Speed-up | | | | | | | +| | Memory | | | 511.568 / 503.032 | | 61.762 / 61.814 | 345.376 / 345.386 | ### Multi-threaded (6 Threads) @@ -140,35 +140,35 @@ Current implementation requires an additional coordinator thread. #### System B -| Machines | | ProB OP | ProB ST | Java | C++ -O1 | C++ -O2 | Rust | -|-------------------|----------|---------|---------|-----------------------|---------|---------|-----------------------| -| Lift_MC_Large | Runtime | | | 67.14 / 67.37 | | | 09.82 / 09.96 | -| | Speed-up | | | | | | | -| | Memory | | | 548.128 / 522.388 | | | 38.637 / 38.590 | -| Cruise Controller | Runtime | | | 1.76 / 1.78 | | | 00.04 / 00.06 | -| | Speed-up | | | | | | | -| | Memory | | | 171.916 / 180.132 | | | 6978 / 6959 | -| Landing Gear | Runtime | | | 6.42 / 6.69 | | | 03.41 / 04.56 | -| | Speed-up | | | | | | | -| | Memory | | | 1.405.280 / 2.043.336 | | | 727.461 / 847.765 | -| CAN BUS | Runtime | | | 3.52 / 4.29 | | | 01.64 / 01.64 | -| | Speed-up | | | | | | | -| | Memory | | | 550.004 / 1.159.472 | | | 1.047.918 / 1.050.520 | -| Train1_Lukas | Runtime | | | 5.96 / 5.44 | | | 01.61 / 01.46 | -| | Speed-up | | | | | | -| | Memory | | | 1.468.360 / 1.772.524 | | | 189.500 / 250.548 | -| Train_1_beebook | Runtime | | | 174.56 / 147.29 | | | 89.65 / 76.61 | -| | Speed-up | | | 2.555.344 / 3.094.376 | | | | -| | Memory | | | | | | 4.998.943 / 5.484.696 | -| nota | Runtime | | | 5.12 / 4.74 | | | 05.02 / 05.24 | -| | Speed-up | | | | | | | -| | Memory | | | 2.185.468 / 2.464.928 | | | 1.390.200 / 1.369.317 | -| sort_1000 | Runtime | | | 208.82 / 37.32 | | | 110.91 / 27.47 | -| | Speed-up | | | | | | | -| | Memory | | | 2.359.820 / 2.420.428 | | | 243.784 / 243.330 | -| N Queens (N=4) | Runtime | | | 32.87 / 32.2 | | | 21.34 / 22.46 | -| | Speed-up | | | | | | | -| | Memory | | | 508.736 / 499.924 | | | 345.888 / 345.855 | +| Machines | | ProB OP | ProB ST | Java | C++ -O1 | C++ -O2 | Rust | +|-------------------|----------|---------|---------|-----------------------|---------|-----------------------|-----------------------| +| Lift_MC_Large | Runtime | | | 67.14 / 67.37 | | 64.37 / 61.59 | 09.82 / 09.96 | +| | Speed-up | | | | | | | +| | Memory | | | 548.128 / 522.388 | | 250.822 / 250.832 | 38.637 / 38.590 | +| Cruise Controller | Runtime | | | 1.76 / 1.78 | | 0.05 / 00.06 | 00.04 / 00.06 | +| | Speed-up | | | | | | | +| | Memory | | | 171.916 / 180.132 | | 6.697 / 7.018 | 6.978 / 6.959 | +| Landing Gear | Runtime | | | 6.42 / 6.69 | | 7.03 / 6.76 | 03.41 / 04.56 | +| | Speed-up | | | | | | | +| | Memory | | | 1.405.280 / 2.043.336 | | 341.353 / 345.930 | 727.461 / 847.765 | +| CAN BUS | Runtime | | | 3.52 / 4.29 | | 4.12 / 4.35 | 01.64 / 01.64 | +| | Speed-up | | | | | | | +| | Memory | | | 550.004 / 1.159.472 | | 317.437 / 326.536 | 1.047.918 / 1.050.520 | +| Train1_Lukas | Runtime | | | 5.96 / 5.44 | | 4.36 / 1.91 | 01.61 / 01.46 | +| | Speed-up | | | | | | +| | Memory | | | 1.468.360 / 1.772.524 | | 60.320 / 64.956 | 189.500 / 250.548 | +| Train_1_beebook | Runtime | | | 174.56 / 147.29 | | 250.92 / 111.71 | 89.65 / 76.61 | +| | Speed-up | | | | | | | +| | Memory | | | 2.555.344 / 3.094.376 | | 1.572.735 / 1.814.287 | 4.998.943 / 5.484.696 | +| nota | Runtime | | | 5.12 / 4.74 | | 26.12 / 21.58 | 05.02 / 05.24 | +| | Speed-up | | | | | | | +| | Memory | | | 2.185.468 / 2.464.928 | | 299.167 / 433.206 | 1.390.200 / 1.369.317 | +| sort_1000 | Runtime | | | 208.82 / 37.32 | | 336.3 / 273.14 | 110.91 / 27.47 | +| | Speed-up | | | | | | | +| | Memory | | | 2.359.820 / 2.420.428 | | 323.596 / 341.784 | 243.784 / 243.330 | +| N Queens (N=4) | Runtime | | | 32.87 / 32.2 | | 30.88 / 25.98 | 21.34 / 22.46 | +| | Speed-up | | | | | | | +| | Memory | | | 508.736 / 499.924 | | 62.630 / 62.742 | 345.888 / 345.855 |