print · source · login   

Model details

Scalable Register models

The following Benchmarks let you generate a model of size n using a python script:

  • BenchmarkFIFOset
  • BenchmarkQueue
  • BenchmarkStack
Benchmark NameInputs/OutputsRegistersConstantsStatesTransitions
FIFO-set(n)2/3n0n+13n+1
Queue(n)/stack(n)2/3n0n+12n+2

Register

modelstatesinputs/outputstransitionconstantsregistersinparams/outparams
BenchmarkPassport/model.register.xml59/248311/0
BenchmarkABP/model_ABP_Receiver3.registe22/36232/2
BenchmarkABP/model_ABP_output.register.x73/327222/2
BenchmarkABP/model_Channel_Frame.registe13/34032/2
BenchmarkLogin/model.register.xml33/210044/0
BenchmarkSIP/model.register.xml104/748023/6
BenchmarkFWGC/model.register.xml91/432451/0
BenchmarkMultiLogin/MultiLogin2.register74/245075/1
BenchmarkMultiLogin/MultiLogin1.register34/215055/1
BenchmarkRepdigitPalindrome/model.regist15/2100416/0
BenchmarkBRP/BRP_mutant1.register.xml23/320373/5
BenchmarkBRP/BRP_mutant6.register.xml23/321363/5
BenchmarkBRP/BRP_ref.register.xml23/318373/5
BenchmarkBRP/BRP_mutant4.register.xml23/318363/5
BenchmarkBRP/BRP_mutant3.register.xml23/318363/5
BenchmarkBRP/BRP_mutant2.register.xml23/318363/5
BenchmarkBRP/BRP_mutant5.register.xml23/316363/5

Mealy

modelstatesinputs/outputstransition
BenchmarkQUICprotocol/QUICprotocolwithout0RTT.dot54/620
BenchmarkQUICprotocol/QUICprotocolwith0RTT.dot75/635
BenchmarkMQTT/VerneMQ__two_client_will_retain.dot179/18153
BenchmarkMQTT/hbmqtt__single_client.dot1011/10110
BenchmarkMQTT/mosquitto__mosquitto.dot37/721
BenchmarkMQTT/ActiveMQ__two_client_will_retain.dot189/21162
BenchmarkMQTT/mosquitto__two_client_same_id.dot711/1377
BenchmarkMQTT/hbmqtt__invalid.dot311/633
BenchmarkMQTT/mosquitto__non_clean.dot126/1872
BenchmarkMQTT/emqtt__non_clean.dot126/2072
BenchmarkMQTT/hbmqtt__two_client.dot99/2781
BenchmarkMQTT/mosquitto__single_client.dot1011/10110
BenchmarkMQTT/emqtt__simple.dot37/721
BenchmarkMQTT/hbmqtt__non_clean.dot106/1760
BenchmarkMQTT/hbmqtt__simple.dot57/835
BenchmarkMQTT/ActiveMQ__invalid.dot511/855
BenchmarkMQTT/mosquitto__two_client_will_retain.dot189/21162
BenchmarkMQTT/mosquitto__invalid.dot311/733
BenchmarkMQTT/VerneMQ__two_client_same_id.dot711/1377
BenchmarkMQTT/mosquitto__two_client.dot169/42144
BenchmarkMQTT/VerneMQ__simple.dot37/721
BenchmarkMQTT/emqtt__two_client_same_id.dot711/1377
BenchmarkMQTT/emqtt__single_client.dot1011/10110
BenchmarkMQTT/emqtt__two_client.dot169/48144
BenchmarkMQTT/VerneMQ__two_client.dot169/42144
BenchmarkMQTT/emqtt__invalid.dot311/633
BenchmarkMQTT/emqtt__two_client_will_retain.dot189/21162
BenchmarkMQTT/VerneMQ__invalid.dot311/733
BenchmarkMQTT/VerneMQ__non_clean.dot126/1872
BenchmarkMQTT/ActiveMQ__simple.dot47/728
BenchmarkMQTT/hbmqtt__two_client_will_retain.dot179/22153
BenchmarkMQTT/ActiveMQ__single_client.dot811/1088
BenchmarkMQTT/ActiveMQ__non_clean.dot126/1872
BenchmarkMQTT/VerneMQ__single_client.dot1011/10110
BenchmarkEdentifier2/learnresult_new_device-simple_fix.dot35/415
BenchmarkEdentifier2/learnresult_old_500_10-15_fix.dot228/9176
BenchmarkEdentifier2/learnresult_new_Rand_500_10-15_MC_fix.d118/988
BenchmarkEdentifier2/learnresult_new_W-method_fix.dot88/864
BenchmarkEdentifier2/learnresult_old_device-simple_fix.dot45/420
BenchmarkCoffeeMachine/coffeemachine.dot64/324
BenchmarkToyModels/cacm.dot32/36
BenchmarkToyModels/lee_yannakakis_non_distinguishable.dot32/26
BenchmarkToyModels/naiks.dot42/28
BenchmarkToyModels/lee_yannakakis_distinguishable.dot62/212
BenchmarkFromRhapsodyToDezyne/model3.dot5822/161276
BenchmarkFromRhapsodyToDezyne/model2.dot3314/15324
BenchmarkFromRhapsodyToDezyne/model1.dot3515/27525
BenchmarkFromRhapsodyToDezyne/model4.dot3414/10476
BenchmarkSSH/DropBear.dot1713/14221
BenchmarkSSH/BitVise.dot6613/16858
BenchmarkSSH/OpenSSH.dot3122/19682
BenchmarkBankcard/4_learnresult_SecureCode Aut_fix.dot414/956
BenchmarkBankcard/Volksbank_learnresult_MAESTRO_fix.dot714/1198
BenchmarkBankcard/ASN_learnresult_MAESTRO_fix.dot614/1084
BenchmarkBankcard/Rabo_learnresult_SecureCode_Aut_fix.dot615/1290
BenchmarkBankcard/10_learnresult_MasterCard_fix.dot614/984
BenchmarkBankcard/ASN_learnresult_SecureCode Aut_fix.dot414/956
BenchmarkBankcard/4_learnresult_PIN_fix.dot614/1084
BenchmarkBankcard/Rabo_learnresult_MAESTRO_fix.dot614/1084
BenchmarkBankcard/4_learnresult_MAESTRO_fix.dot614/1084
BenchmarkBankcard/learnresult_fix.dot915/11135
BenchmarkBankcard/1_learnresult_MasterCard_fix.dot515/975
BenchmarkTLS/OpenSSL_1.0.2_server_regular.dot77/749
BenchmarkTLS/OpenSSL_1.0.1j_server_regular.dot117/977
BenchmarkTLS/OpenSSL_1.0.1g_server_regular.dot167/11112
BenchmarkTLS/OpenSSL_1.0.1l_client_regular.dot67/542
BenchmarkTLS/miTLS_0.1.3_server_regular.dot68/848
BenchmarkTLS/GnuTLS_3.3.8_server_full.dot1611/12176
BenchmarkTLS/NSS_3.17.4_client_regular.dot78/756
BenchmarkTLS/OpenSSL_1.0.2_client_regular.dot67/542
BenchmarkTLS/OpenSSL_1.0.1g_client_regular.dot107/770
BenchmarkTLS/OpenSSL_1.0.1j_client_regular.dot67/542
BenchmarkTLS/OpenSSL_1.0.1l_server_regular.dot107/870
BenchmarkTLS/RSA_BSAFE_Java_6.1.1_server_regular.dot68/748
BenchmarkTLS/NSS_3.17.4_server_regular.dot88/964
BenchmarkTLS/GnuTLS_3.3.12_client_full.dot912/7108
BenchmarkTLS/OpenSSL_1.0.2_client_full.dot910/690
BenchmarkTLS/GnuTLS_3.3.12_server_regular.dot78/1056
BenchmarkTLS/GnuTLS_3.3.8_client_full.dot1512/8180
BenchmarkTLS/GnuTLS_3.3.8_client_regular.dot118/688
BenchmarkTLS/NSS_3.17.4_client_full.dot1112/9132
BenchmarkTLS/GnuTLS_3.3.12_client_regular.dot78/1056
BenchmarkTLS/GnuTLS_3.3.8_server_regular.dot128/1096
BenchmarkTLS/GnuTLS_3.3.12_server_full.dot912/12108
BenchmarkTLS/RSA_BSAFE_C_4.0.4_server_regular.dot98/1172
BenchmarkTCP/TCP_Windows8_Server.dot3813/10494
BenchmarkTCP/TCP_FreeBSD_Server.dot5513/11715
BenchmarkTCP/TCP_Linux_Server.dot5712/9684
BenchmarkTCP/TCP_Linux_Client.dot1510/11150
BenchmarkTCP/TCP_Windows8_Client.dot1310/12130
BenchmarkTCP/TCP_FreeBSD_Client.dot1210/12120
BenchmarkX-ray-system-PCS/learnresult5.dot912/966
BenchmarkX-ray-system-PCS/learnresult4.dot79/737
BenchmarkX-ray-system-PCS/learnresult6.dot912/966
BenchmarkX-ray-system-PCS/learnresult3.dot79/737
BenchmarkX-ray-system-PCS/learnresult2.dot39/49
BenchmarkX-ray-system-PCS/learnresult1.dot89/744
BenchmarkESMcontroller/run3_hyp.101.obf.dot341078/151265980
BenchmarkESMcontroller/run1_hyp.135.obf.dot341078/151265980
BenchmarkESMcontroller/esm-manual-controller.dot341078/151265980
BenchmarkESMcontroller/run2_hyp.89.obf.dot333878/151260364