IMITATOR

The IMITATOR benchmarks library (v2.1)

This page presents the official IMITATOR benchmarks library (version 2.1), released 31st January 2024. These models have been accumulated over the years from scientific publications, and from industrial collaborations.

The library is described in [AMP21].

In its v2.1 version, the library contains 65 benchmarks with 137 different models and 235 properties.

The entire library v2.1 can be downloaded on Zenodo, including all models, properties, expected results and an HTML version of this page: doi.org/10.5281/zenodo.10600092.

This page and all results were generated thanks to a fully automated script by Dylan Marinho.

BenchmarkJaniSourceCategoriesMetricsProperties
Ac.Auto.Educ.Hard.Ind.Mon.Prod.Prot.RTSSched.SecurityToyUnsol.Scal.Gen.|IPTA||X|Inv.?<>1 clocks?L/U?Bound. Param.?Sil.?stDet.?|P||discr. Var||Act||L|avg(|L|)|T|avg(|T|)PropertyTime|States||comp. States|
accel accel-1000 HAF14
AHW18		 Auto. Ind. Mon. yes yes 2 2 true false not L/U false true true 3 0 11 2574 1287.0 2592 1296.0 EF 0.798 s. 6504 6504
EFpmin 0.954 s. 6502 6504
accel-10000 HAF14
AHW18		 Auto. Ind. Mon. yes yes 2 2 true false not L/U false true true 3 0 11 25152 12576.0 25170 12585.0 EF 8.739 s. 63773 63773
EFpmin 9.941 s. 63741 63759
accel-2000 HAF14
AHW18		 Auto. Ind. Mon. yes yes 2 2 true false not L/U false true true 3 0 11 4909 2454.5 4927 2463.5 EF 1.636 s. 12429 12429
EFpmin 1.837 s. 12426 12429
accel-3000 HAF14
AHW18		 Auto. Ind. Mon. yes yes 2 2 true false not L/U false true true 3 0 11 7814 3907.0 7832 3916.0 EF 2.632 s. 19922 19922
EFpmin 3.118 s. 19907 19916
accel-4000 HAF14
AHW18		 Auto. Ind. Mon. yes yes 2 2 true false not L/U false true true 3 0 11 10060 5030.0 10078 5039.0 EF 3.382 s. 25520 25520
EFpmin 3.797 s. 25514 25518
accel-5000 HAF14
AHW18		 Auto. Ind. Mon. yes yes 2 2 true false not L/U false true true 3 0 11 12546 6273.0 12564 6282.0 EF 4.248 s. 31951 31951
EFpmin 4.992 s. 31926 31939
accel-6000 HAF14
AHW18		 Auto. Ind. Mon. yes yes 2 2 true false not L/U false true true 3 0 11 15390 7695.0 15408 7704.0 EF 5.609 s. 39152 39152
EFpmin 6.195 s. 39129 39142
accel-7000 HAF14
AHW18		 Auto. Ind. Mon. yes yes 2 2 true false not L/U false true true 3 0 11 17703 8851.5 17721 8860.5 EF 6.096 s. 45065 45065
EFpmin 7.091 s. 45039 45053
accel-8000 HAF14
AHW18		 Auto. Ind. Mon. yes yes 2 2 true false not L/U false true true 3 0 11 20314 10157.0 20332 10166.0 EF 6.412 s. 51660 51660
EFpmin 8.002 s. 51629 51644
accel-9000 HAF14
AHW18		 Auto. Ind. Mon. yes yes 2 2 true false not L/U false true true 3 0 11 22706 11353.0 22724 11362.0 EF 7.470 s. 57534 57534
EFpmin 8.679 s. 57506 57522
ALR15_fig1 ALR15_fig1 ALR15 Ac. Toy Unsol. no no 1 2 false false U-PTA true true true 1 0 4 4 4.0 4 4.0 CycleThrough NE (Uns.)
EF NE (Uns.)
ALR15_fig2a ALR15_fig2a ALR15 Ac. Toy Unsol. no no 1 2 true false U-PTA true true true 1 0 2 2 2.0 2 2.0 EF TO (3600s)
AndOr AndOr CC05 Ac. Hard. no no 3 4 true false L/U-PTA false false true 12 0 8 20 6.6 44 14.6 IM 0.043 s. 21 32
pattern 1.659 s. 19 22
ATM fig1_DCLXZL18-fixed DCL18 Ac. Toy no no 1 3 true false not L/U false true true 3 0 9 5 5.0 9 9.0 CycleThrough 0.001 s. 11 14
DeadlockFree 0.007 s. 16 30
EF 0.000 s. 7 9
ATM_PTO ATM_PTO [ABLM22] Educ. Security Toy no no 2 5 true false not L/U false true false 1 8 45 28 14.0 54 27.0 EF 1298.570 s. 128631 196894
blowup blowup-1000 AHW18 Mon. Toy yes yes 2 3 true false not L/U false true true 5 0 5 1008 504.0 1011 505.5 EF TO (3600s)
EFpmin 0.780 s. 2681 3242
blowup-200 AHW18 Mon. Toy yes yes 2 3 true false not L/U false true true 5 0 5 208 104.0 211 105.5 EF 24.289 s. 20602 20602
EFpmin 0.143 s. 558 678
blowup-400 AHW18 Mon. Toy yes yes 2 3 true false not L/U false true true 5 0 5 408 204.0 411 205.5 EF TO (3600s)
EFpmin 0.287 s. 1091 1322
blowup-600 AHW18 Mon. Toy yes yes 2 3 true false not L/U false true true 5 0 5 608 304.0 611 305.5 EF TO (3600s)
EFpmin 0.446 s. 1615 1954
blowup-800 AHW18 Mon. Toy yes yes 2 3 true false not L/U false true true 5 0 5 808 404.0 811 405.5 EF TO (3600s)
EFpmin 0.612 s. 2159 2612
BlT09_fig1 BlT09_fig1 BT09 Toy no no 1 2 false false L/U-PTA false true true 2 0 7 4 4.0 7 7.0 CycleThrough 0.000 s. 4 8
BRPAAPP21 BRPAAPP21_GFSinRC AAPP21 Prot. yes (numbers of retransmissions and of chunks) no 5 4 true false not L/U false true false 4 9 18 16 3.2 30 6.0 CycleThrough 0.374 s. 653 887
BRPAAPP21_GSinFSdk AAPP21 Prot. no no 5 4 true false not L/U false true false 4 9 18 16 3.2 34 6.8 CycleThrough 8.307 s. 6795 9451
BRPAAPP21_GSinFSnok AAPP21 Prot. no no 5 4 true false not L/U false true false 4 9 18 16 3.2 33 6.6 CycleThrough 0.005 s. 35 36
BRPAAPP21_RC AAPP21 Prot. yes (numbers of retransmissions and of chunks) no 4 4 true false not L/U false true false 4 9 20 15 3.7 28 7.0 AGnot 0.393 s. 477 689
BRPDKRT97 BRPDKRT97 DKRT97 Ac. Ind. Prot. RTS no no 6 6 true false not L/U true true false 2 11 20 22 3.6 52 8.6 AGnot 44.476 s. 4153 6503
IM 2217.599 s. 74949 135718
Coffee coffee Educ. Toy no no 1 2 true false not L/U false false true 3 0 4 4 4.0 6 6.0 EF 0.000 s. 6 8
IM 0.013 s. 61 95
CoffeeDrinker coffeeDrinker Educ. Toy no no 2 4 true false not L/U false true false 6 1 7 8 4.0 14 7.0 AGnot 0.021 s. 46 72
IM 1.003 s. 995 1620
coffeeDrinker_toolpaper Educ. Toy no no 2 3 true false not L/U false true false 3 1 6 8 4.0 14 7.0 AGnot 0.009 s. 22 23
AGnot2 0.009 s. 22 23
AGnot3 0.009 s. 22 23
IM 0.005 s. 13 23
pattern 0.002 s. 15 15
pattern2 0.002 s. 15 15
coffeeDrinker_unbounded Educ. Toy no no 2 4 true false not L/U false true true 6 0 7 8 4.0 13 6.5 AGnot 0.008 s. 21 37
crossing_signals crossing_signals-20 AWUH22 Toy yes no 3 3 true true not L/U false false false 1 1 9 10 3.3 12 4.0 EF 0.676 s. 1707 5942
crossing_signals-200 AWUH22 Toy yes no 3 3 true true not L/U false false false 1 1 9 10 3.3 12 4.0 EF 15.453 s. 16828 59216
CSMACD CSMACD-bc1 KNSW07 Ac. Ind. Prot. RTS yes yes 3 3 true false not L/U false false false 3 0 9 19 6.3 39 13.0 EF 0.004 s. 37 60
IM 0.250 s. 511 1625
CSMACD-bc10 KNSW07 Ac. Ind. Prot. RTS yes yes 3 3 true false not L/U false false false 3 0 9 8213 2737.6 24567 8189.0 EF 0.006 s. 37 60
IM 3438.803 s. 680105 1706787
CSMACD-bc5 KNSW07 Ac. Ind. Prot. RTS yes yes 3 3 true false not L/U false false false 3 0 9 267 89.0 759 253.0 EF 0.005 s. 37 60
IM 11.107 s. 16221 42967
CSMACD-bc6 KNSW07 Ac. Ind. Prot. RTS yes yes 3 3 true false not L/U false false false 3 0 9 525 175.0 1527 509.0 EF 0.005 s. 37 60
IM 22.958 s. 37177 96179
CSMACD-bc9 KNSW07 Ac. Ind. Prot. RTS yes yes 3 3 true false not L/U false false false 3 0 9 4115 1371.6 12279 4093.0 EF 0.007 s. 57 100
IM 1319.913 s. 504337 1268139
Cycle1 Cycle1 Ac. Toy Unsol. no no 1 2 true false U-PTA false true true 1 0 1 1 1.0 1 1.0 Cycle NE (Uns.)
Cycles_2 infinite-2 [AAPP21] Ac. Toy Unsol. no no 1 2 true false U-PTA false true true 1 0 3 2 2.0 3 3.0 Cycle 0.000 s. 8 10
CycleThrough 0.000 s. 8 10
Cycles_5 infinite-5 [AAPP21] Ac. Toy Unsol. no no 1 2 true false U-PTA false true true 1 0 1 1 1.0 1 1.0 Cycle 5.000 s. 3333 3333
CycleThrough 5.001 s. 3315 3315
Cycles_5_6 infinite-5_6 [AAPP21] Ac. Toy Unsol. no no 1 2 true false U-PTA false true true 1 0 3 2 2.0 3 3.0 Cycle 5.003 s. 3256 6509
CycleThrough 5.003 s. 3228 6454
Cycles_exU_noloop exU_noloop Ac. Toy Unsol. no no 1 2 true false U-PTA false true true 1 0 2 2 2.0 2 2.0 CycleThrough NE (Uns.)
Cycles_noSolution infinite-noSolution [AAPP21] Ac. Toy Unsol. no no 1 2 true false U-PTA false true true 1 0 1 1 1.0 1 1.0 Cycle 5.005 s. 2613 2613
CycleThrough 5.004 s. 2610 2610
Cycles_notFiniteDisjunction infinite-notFiniteDisjunction [AAPP21] Ac. Toy Unsol. no no 1 2 true false not L/U false true true 1 0 3 2 2.0 3 3.0 Cycle 5.001 s. 3959 3959
CycleThrough 5.037 s. 431 645
Cycles_Rplus infinite-Rplus [AAPP21] Ac. Toy Unsol. no no 1 2 true false not L/U false true true 2 0 1 1 1.0 1 1.0 Cycle 5.004 s. 2543 2543
CycleThrough 5.006 s. 2540 2540
Cycles_Zero infinite-Zero Ac. Toy Unsol. no no 1 2 true false not L/U false true true 1 0 1 1 1.0 1 1.0 Cycle 5.002 s. 2503 2503
CycleThrough 5.000 s. 2509 2509
Fischer2 fischer_2 Ac. Prot. RTS no no 3 2 true false L/U-PTA false false true 2 1 11 9 3.0 23 7.6 AGnot 0.005 s. 35 90
IM TO (3600s)
FischerAHV93 FischerAHV93 AHV93 Ac. Prot. RTS no no 3 2 false false L/U-PTA false true true 4 0 16 13 4.3 32 10.6 AGnot 0.005 s. 33 71
FischerHRSV02 fischerHRSV02_2 HRSV02 Ac. Prot. RTS nb of proc. no 2 2 true false L/U-PTA false true true 4 1 12 8 4.0 12 6.0 AGnot TO (3600s)
IM TO (3600s)
fischerHRSV02_3 HRSV02 Ac. Prot. RTS nb of proc. no 3 3 true false L/U-PTA false true true 4 1 18 12 4.0 18 6.0 AGnot TO (3600s)
IM TO (3600s)
FischerPAT fischerPAT2 Ac. Prot. RTS nb of proc. no 2 2 true false L/U-PTA false false false 2 1 12 10 5.0 14 7.0 AGnot 0.009 s. 62 97
IM TO (3600s)
fischerPAT3 Ac. Prot. RTS nb of proc. no 3 3 true false L/U-PTA false false false 2 1 18 15 5.0 21 7.0 AGnot 0.188 s. 594 1077
IM TO (3600s)
FischerPS08 FischerPS08-10 PS08 Ac. Prot. RTS yes yes 12 10 false false L/U-PTA false true true 2 1 41 53 4.4 181 15.0 AGnot TO (3600s)
IM TO (3600s)
FischerPS08-2 PS08 Ac. Prot. RTS yes yes 4 2 false false L/U-PTA false true true 2 1 9 13 3.2 21 5.2 AGnot 0.004 s. 38 48
IM TO (3600s)
FischerPS08-3 PS08 Ac. Prot. RTS yes yes 5 3 false false L/U-PTA false true true 2 1 13 18 3.6 34 6.8 AGnot 0.068 s. 350 516
IM TO (3600s)
FischerPS08-4 PS08 Ac. Prot. RTS yes yes 6 4 false false L/U-PTA false true true 2 1 17 23 3.8 49 8.1 AGnot 2.416 s. 4794 8608
IM TO (3600s)
FischerPS08-5 PS08 Ac. Prot. RTS yes yes 7 5 false false L/U-PTA false true true 2 1 21 28 4.0 66 9.4 AGnot 219.449 s. 85825 176241
IM TO (3600s)
Flipflop flipflop-2D CC07 Ac. Hard. no no 5 5 true false U-PTA false false true 2 0 12 49 9.8 142 28.4 IM 0.002 s. 13 14
IM2 0.002 s. 11 13
pattern 0.003 s. 12 14
flipflop-4D CC07 Ac. Hard. no no 5 5 true false U-PTA false false true 4 0 12 49 9.8 142 28.4 IM 0.003 s. 13 15
IM2 0.003 s. 11 14
pattern 0.034 s. 53 60
FMTV1 FMTV_1_A1 SAL15 Ind. Prot. RTS No No 3 3 true false not L/U false true false 3 5 14 15 5.0 21 7.0 EF 1.334 s. 606 895
EFpmax 1.076 s. 598 916
EFpmin 1.261 s. 580 871
FMTV_1_A3 SAL15 Ind. Prot. RTS No No 3 3 true false not L/U false true false 3 7 18 15 5.0 28 9.3 EF TO (3600s)
EFpmax TO (3600s)
EFpmin TO (3600s)
FMTV2 FMTV_2 SAL15 Ind. Prot. RTS no no 6 9 true true not L/U false true true 2 0 28 87 14.5 129 21.5 EF 0.543 s. 499 585
gear gear-1000 HAF14
AHW18		 Auto. Ind. Mon. yes yes 2 2 true false not L/U false true true 3 0 7 1475 737.5 1481 740.5 EF 0.619 s. 4453 4453
EFpmin 0.588 s. 3374 3753
gear-10000 HAF14
AHW18		 Auto. Ind. Mon. yes yes 2 2 true false not L/U false true true 3 0 7 14665 7332.5 14671 7335.5 EF 6.326 s. 44581 44581
EFpmin 6.124 s. 33419 37235
gear-2000 HAF14
AHW18		 Auto. Ind. Mon. yes yes 2 2 true false not L/U false true true 3 0 7 2845 1422.5 2851 1425.5 EF 1.289 s. 8633 8633
EFpmin 1.189 s. 6485 7224
gear-3000 HAF14
AHW18		 Auto. Ind. Mon. yes yes 2 2 true false not L/U false true true 3 0 7 4603 2301.5 4609 2304.5 EF 2.146 s. 14181 14181
EFpmin 2.096 s. 10554 11801
gear-4000 HAF14
AHW18		 Auto. Ind. Mon. yes yes 2 2 true false not L/U false true true 3 0 7 5847 2923.5 5853 2926.5 EF 2.750 s. 17865 17865
EFpmin 2.632 s. 13354 14900
gear-5000 HAF14
AHW18		 Auto. Ind. Mon. yes yes 2 2 true false not L/U false true true 3 0 7 7309 3654.5 7315 3657.5 EF 3.404 s. 22501 22501
EFpmin 3.299 s. 16718 18692
gear-6000 HAF14
AHW18		 Auto. Ind. Mon. yes yes 2 2 true false not L/U false true true 3 0 7 9003 4501.5 9009 4504.5 EF 4.240 s. 27609 27609
EFpmin 4.011 s. 20603 23007
gear-7000 HAF14
AHW18		 Auto. Ind. Mon. yes yes 2 2 true false not L/U false true true 3 0 7 10323 5161.5 10329 5164.5 EF 5.265 s. 31753 31753
EFpmin 4.606 s. 23629 26409
gear-8000 HAF14
AHW18		 Auto. Ind. Mon. yes yes 2 2 true false not L/U false true true 3 0 7 11839 5919.5 11845 5922.5 EF 5.488 s. 36301 36301
EFpmin 5.307 s. 27062 30221
gear-9000 HAF14
AHW18		 Auto. Ind. Mon. yes yes 2 2 true false not L/U false true true 3 0 7 13191 6595.5 13197 6598.5 EF 6.211 s. 40025 40025
EFpmin 5.536 s. 30051 33465
IMPO IMPO ACR16 Ac. Hard. no no 5 5 true false L/U-PTA false false true 6 0 8 20 4.0 30 6.0 AGnot 0.003 s. 12 15
IM 0.002 s. 6 10
IMPOloop IMPOloop ACR16 Ac. Hard. no no 5 5 true false L/U-PTA false false true 10 0 9 22 4.4 37 7.4 AGnot 0.554 s. 56 71
IM 0.005 s. 4 8
IM2 TO (3600s)
JLR15_Fig6 JLR15_Fig6 JLR15 Toy Unsol. no no 1 2 true false L/U-PTA true true true 2 0 2 2 2.0 2 2.0 EF NE (Uns.)
Jobshop jobshop_2_4 AM01 RTS Sched. yes no 2 2 true false not L/U false false true 8 4 4 18 9.0 16 8.0 EF 0.020 s. 80 130
IM 0.572 s. 1213 1567
jobshop_3_4 AM01 RTS Sched. yes no 3 3 true false not L/U false false true 12 4 3 27 9.0 24 8.0 EF 2.343 s. 1459 3189
IM TO (3600s)
jobshop_4_4 AM01 RTS Sched. yes no 4 4 true false not L/U false false true 16 4 4 36 9.0 32 8.0 EF TO (3600s)
KSA22 KSA22_1 KSA22 Security no no 8 4 true false not L/U true true false 1 3 9 15 1.8 27 3.3 AGnot 0.116 s. 194 597
KSA22_2 KSA22 Security no no 7 2 false false not L/U true true false 2 9 18 15 2.1 31 4.4 AGnot TO (3600s)
KSA22_3 KSA22 Security no no 5 4 true false not L/U true true false 3 8 43 29 5.8 60 12.0 AGnot 1.503 s. 962 2292
KSA22_4 KSA22 Security no no 6 4 true false not L/U true true false 0 5 17 16 2.6 30 5.0 AGnot 0.120 s. 303 554
KSA22_5 KSA22 Security no no 8 5 true false not L/U false true false 1 5 20 19 2.3 39 4.8 AGnot 9.005 s. 4310 15820
LA02 LA02-2_10param [Tamura07] RTS no ? 3 3 true true not L/U false false true 10 0 21 36 12.0 222 74.0 EF 1916.940 s. 1307 1622
LA02-2_5param [Tamura07] RTS no ? 3 3 true true not L/U false false true 5 0 21 36 12.0 222 74.0 EF 2.111 s. 966 1211
LA02-2_inst [Tamura07] RTS no ? 3 3 true true not L/U true false true 0 0 21 36 12.0 222 74.0 EF 0.085 s. 366 517
LA02-3_15param [Tamura07] RTS no ? 4 4 true true not L/U false false true 15 0 31 53 13.2 588 147.0 EF TO (3600s)
LA02-3_1param_wm0j1 [Tamura07] RTS no ? 4 4 true true not L/U false false true 1 0 31 53 13.2 588 147.0 EF 32.340 s. 13412 25138
LA02-3_5param [Tamura07] RTS no ? 4 4 true true not L/U false false true 5 0 31 53 13.2 588 147.0 EF TO (3600s)
LA02-3_inst [Tamura07] RTS no ? 4 4 true true not L/U true false true 0 0 31 53 13.2 588 147.0 EF 8.946 s. 8590 17240
LA02_deadline-2_11param [Tamura07] RTS no ? 3 3 true true not L/U false false true 11 0 21 36 12.0 222 74.0 EF 215.137 s. 1307 1622
EFpmin 1.687 s. 1255 1622
LA02_deadline-2_1param [Tamura07] RTS no ? 3 3 true true not L/U false false true 1 0 21 36 12.0 222 74.0 EF 0.080 s. 439 583
EFpmin 0.073 s. 435 583
LA02_deadline-3_16param [Tamura07] RTS no ? 4 4 true true not L/U false false true 16 0 31 53 13.2 588 147.0 EF TO (3600s)
EFpmin TO (3600s)
LA02_deadline-3_1param [Tamura07] RTS no ? 4 4 true true not L/U false false true 1 0 31 53 13.2 588 147.0 EF 9.304 s. 11595 19664
EFpmin 8.225 s. 11500 19673
LA02_deadline-3_2param [Tamura07] RTS no ? 4 4 true true not L/U false false true 2 0 31 53 13.2 588 147.0 EF 25.394 s. 15978 26568
EFpmin 25.264 s. 15744 26527
LA02_deadline-3_6param [Tamura07] RTS no ? 4 4 true true not L/U false false true 6 0 31 53 13.2 588 147.0 EF TO (3600s)
EFpmin TO (3600s)
Noodles NoodlesCooking Educ. Toy no no 1 2 true false not L/U false false true 2 0 4 5 5.0 5 5.0 AGnot 0.000 s. 5 5
NP_FPS_3tasks JLR13_3tasks_npfp JLR13 Ac. Prot. RTS no no 4 6 true false not L/U true true true 2 0 15 17 4.2 54 13.5 AGnot 14.810 s. 668 1127
JLR13_3tasks_npfp-100_0 JLR13 Ac. Prot. RTS no no 4 6 true false U-PTA true true true 2 0 15 17 4.2 54 13.5 AGnot 0.510 s. 338 429
JLR13_3tasks_npfp-100_2 JLR13 Ac. Prot. RTS no no 4 6 true false U-PTA true true true 2 0 15 17 4.2 54 13.5 AGnot 21.833 s. 3202 4205
JLR13_3tasks_npfp-50_0 JLR13 Ac. Prot. RTS no no 4 6 true false U-PTA true true true 2 0 15 17 4.2 54 13.5 AGnot 0.427 s. 304 391
JLR13_3tasks_npfp-50_2 JLR13 Ac. Prot. RTS no no 4 6 true false U-PTA true true true 2 0 15 17 4.2 54 13.5 AGnot 6.102 s. 1433 1886
NuclearPlant NuclearPlant Educ. Toy no no 1 2 true false not L/U false false true 4 0 6 6 6.0 8 8.0 AGnot 0.001 s. 8 9
Packaging packaging ABBCR16 Ac. Prod. no no 3 2 true false L/U-PTA false false true 2 0 6 10 3.3 16 5.3 AGnot TO (3600s)
preemptive_scheduling uniproc_fp_sched_no_termination no no 6 9 true true not L/U false true false 2 2 13 26 4.3 39 6.5 AGnot TO (3600s)
IM TO (3600s)
ProdCons Pipeline_KP12_2_3 KP12 Ac. Prod. yes no 5 5 true false L/U-PTA false true true 6 0 12 16 3.2 15 3.0 EF TO (3600s)
Pipeline_KP12_2_5 KP12 Ac. Prod. yes no 5 5 true false L/U-PTA false true true 6 0 16 20 4.0 19 3.8 EF TO (3600s)
Pipeline_KP12_3_2 KP12 Ac. Prod. yes no 6 6 true false L/U-PTA false true true 6 0 13 18 3.0 17 2.8 EF TO (3600s)
Pipeline_KP12_3_3 KP12 Ac. Prod. yes no 6 6 true false L/U-PTA false true true 6 0 16 21 3.5 20 3.3 EF TO (3600s)
RCP RCP_CS01 CS01 Ind. Prot. RTS no no 5 6 true false L/U-PTA false true false 5 6 20 30 6.0 82 16.4 EF 0.419 s. 719 890
Researcher researcher Educ. Toy no no 1 2 true true not L/U false true false 4 1 6 4 4.0 9 9.0 AGnot 0.004 s. 11 20
CycleThrough 0.001 s. 7 8
CycleThrough2 0.321 s. 367 812
DeadlockFree 6.071 s. 2301 5644
EF 0.004 s. 11 20
EF2 0.058 s. 103 235
EFpmin 0.037 s. 63 160
IM 0.153 s. 179 464
pattern 0.255 s. 240 445
pattern2 0.004 s. 16 20
pattern3 0.000 s. 4 4
researcher_globaltime Educ. Toy no no 1 3 true true not L/U false true false 4 1 6 4 4.0 9 9.0 EFtmin 0.027 s. 45 99
SIMOP simop2 ACDFR09 Ind. no no 5 8 true false not L/U false true true 2 0 25 46 9.2 72 14.4 EF TO (3600s)
IM TO (3600s)
simop3 ACDFR09 Ind. no no 5 8 true false not L/U false true true 3 0 25 46 9.2 72 14.4 EF TO (3600s)
IM TO (3600s)
SLAF14 SLAF14_3 SLAF14 Ac. Prot. RTS yes no 8 13 true true not L/U true true false 2 3 20 47 5.8 81 10.1 AGnot 0.862 s. 517 702
SLAF14_5 SLAF14 Ac. Prot. RTS yes no 12 21 true true not L/U true true true 2 0 34 153 12.7 243 20.2 AGnot 9.269 s. 3249 6461
SPSMALL spsmall CEFX09 
Andre10		 Hard. Ind. no no 11 11 true false not L/U false false false 2 0 25 52 4.7 145 13.1 AGnot 0.399 s. 404 471
IM 0.024 s. 34 42
SSLAF13_1 SSLAF13_test1 SSLAF13 Prot. RTS yes yes 7 16 true true not L/U false false false 2 2 23 42 6.0 146 20.8 AGnot 0.133 s. 76 152
SSLAF13_2 SSLAF13_test2 SSLAF13 Prot. RTS yes yes 6 14 true true not L/U false false false 2 4 26 45 7.5 154 25.6 AGnot 293.581 s. 43324 43839
Synth_3N synth3N GH21 Ac. Toy Unsol. no no 1 2 false false not L/U false true true 1 0 4 3 3.0 4 4.0 EF NE (Uns.)
Synth_int01 synthint01 Ac. Toy Unsol. no no 1 2 true false U-PTA false true true 1 0 2 2 2.0 2 2.0 EF NE (Uns.)
Synth_InvN synthInvN Ac. Toy Unsol. no no 1 2 true false not L/U false true true 1 0 2 2 2.0 2 2.0 EF NE (Uns.)
Synth_N synthN Ac. Toy Unsol. no no 1 2 true false not L/U false true true 1 0 2 2 2.0 2 2.0 EF NE (Uns.)
Synth_pN synthpN Ac. Toy Unsol. no no 1 2 true false not L/U false true true 2 0 2 2 2.0 2 2.0 EF NE (Uns.)
Synth_pNplusq synthpNplusq AHV93 Ac. Toy Unsol. no no 1 2 false false not L/U false true true 3 0 2 2 2.0 2 2.0 EF NE (Uns.)
Synth_Rplus synthRplus Ac. Toy Unsol. no no 1 2 true false L-PTA false true true 1 0 2 2 2.0 2 2.0 EF NE (Uns.)
Thales AVTS_imitator no no 12 10 true true not L/U false true false 1 8 50 40 3.3 133 11.0 AGnot 9.286 s. 2376 4269
Therac therac25 no no 4 2 true false not L/U false true true 2 2 10 12 3.0 16 4.0 AGnot TO (3600s)
Train1PTA Train1PTA Educ. Toy no no 1 2 true false not L/U false false true 3 0 4 5 5.0 6 6.0 AGnot 0.000 s. 6 7
IM 0.001 s. 7 12
IM2 0.001 s. 7 12
IM3 0.000 s. 4 6
train_intruder train_intruder-1 no no 3 3 true false not L/U false true false 5 2 6 10 3.3 12 4.0 AGnot 0.006 s. 16 19
train_intruder-2 no no 3 3 true false not L/U false true false 6 2 9 13 4.3 21 7.0 AGnot 0.024 s. 32 37
train_intruder-3 no no 3 3 true false not L/U false true false 8 2 9 14 4.6 25 8.3 AGnot 0.068 s. 39 46
train_intruder-4 no no 3 3 true false not L/U false true false 9 2 10 15 5.0 32 10.6 AGnot 0.273 s. 78 94
train_intruder-converted_parameters no no 3 3 true false not L/U false true false 9 2 6 10 3.3 12 4.0 AGnot 0.020 s. 16 19
TrainAHV93 TrainAHV93 AHV93 Ac. no no 3 3 false false L/U-PTA false false true 6 0 8 12 4.0 12 4.0 AGnot 0.000 s. 4 4
IM 0.034 s. 79 116
UntimedLanguage untimedLanguage ALR16 Ac. Toy Unsol. no no 1 2 true false not L/U false false false 1 0 3 4 4.0 6 6.0 EF NE (Uns.)
WFAS WFAS_BBLS15 BBLS15 Ac. no no 3 4 true false not L/U false true false 2 0 10 10 3.3 23 7.6 AGnot TO (3600s)
IM 0.036 s. 27 64
IM2 0.009 s. 17 29

References

[AMP21]
Étienne André, Dylan Marinho and Jaco van de Pol. A Benchmarks Library for Extended Timed Automata. In Frédéric Loulergue and Franz Wotawa (eds.), TAP’21, Springer LNCS 12740, pages 39-50, June 2021. DOI: 10.1007/978-3-030-79379-1_3 (English) [PDF (author version) | BibTeX | data | Slides]🌐