Model details

Scalable Register models

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

BenchmarkFIFOset
BenchmarkQueue
BenchmarkStack

Benchmark Name	Inputs/Outputs	Registers	Constants	States	Transitions
FIFO-set(n)	2/3	n	0	n+1	3n+1
Queue(n)/stack(n)	2/3	n	0	n+1	2n+2

Register

model	states	inputs/outputs	transition	constants	registers	inparams/outparams
BenchmarkPassport/model.register.xml	5	9/2	48	3	1	1/0
BenchmarkABP/model_ABP_Receiver3.registe	2	2/3	6	2	3	2/2
BenchmarkABP/model_ABP_output.register.x	7	3/3	27	2	2	2/2
BenchmarkABP/model_Channel_Frame.registe	1	3/3	4	0	3	2/2
BenchmarkLogin/model.register.xml	3	3/2	10	0	4	4/0
BenchmarkSIP/model.register.xml	10	4/7	48	0	2	3/6
BenchmarkFWGC/model.register.xml	9	1/4	32	4	5	1/0
BenchmarkMultiLogin/MultiLogin2.register	7	4/2	45	0	7	5/1
BenchmarkMultiLogin/MultiLogin1.register	3	4/2	15	0	5	5/1
BenchmarkRepdigitPalindrome/model.regist	1	5/2	10	0	4	16/0
BenchmarkBRP/BRP_mutant1.register.xml	2	3/3	20	3	7	3/5
BenchmarkBRP/BRP_mutant6.register.xml	2	3/3	21	3	6	3/5
BenchmarkBRP/BRP_ref.register.xml	2	3/3	18	3	7	3/5
BenchmarkBRP/BRP_mutant4.register.xml	2	3/3	18	3	6	3/5
BenchmarkBRP/BRP_mutant3.register.xml	2	3/3	18	3	6	3/5
BenchmarkBRP/BRP_mutant2.register.xml	2	3/3	18	3	6	3/5
BenchmarkBRP/BRP_mutant5.register.xml	2	3/3	16	3	6	3/5

Mealy

model	states	inputs/outputs	transition
BenchmarkQUICprotocol/QUICprotocolwithout0RTT.dot	5	4/6	20
BenchmarkQUICprotocol/QUICprotocolwith0RTT.dot	7	5/6	35
BenchmarkMQTT/VerneMQ__two_client_will_retain.dot	17	9/18	153
BenchmarkMQTT/hbmqtt__single_client.dot	10	11/10	110
BenchmarkMQTT/mosquitto__mosquitto.dot	3	7/7	21
BenchmarkMQTT/ActiveMQ__two_client_will_retain.dot	18	9/21	162
BenchmarkMQTT/mosquitto__two_client_same_id.dot	7	11/13	77
BenchmarkMQTT/hbmqtt__invalid.dot	3	11/6	33
BenchmarkMQTT/mosquitto__non_clean.dot	12	6/18	72
BenchmarkMQTT/emqtt__non_clean.dot	12	6/20	72
BenchmarkMQTT/hbmqtt__two_client.dot	9	9/27	81
BenchmarkMQTT/mosquitto__single_client.dot	10	11/10	110
BenchmarkMQTT/emqtt__simple.dot	3	7/7	21
BenchmarkMQTT/hbmqtt__non_clean.dot	10	6/17	60
BenchmarkMQTT/hbmqtt__simple.dot	5	7/8	35
BenchmarkMQTT/ActiveMQ__invalid.dot	5	11/8	55
BenchmarkMQTT/mosquitto__two_client_will_retain.dot	18	9/21	162
BenchmarkMQTT/mosquitto__invalid.dot	3	11/7	33
BenchmarkMQTT/VerneMQ__two_client_same_id.dot	7	11/13	77
BenchmarkMQTT/mosquitto__two_client.dot	16	9/42	144
BenchmarkMQTT/VerneMQ__simple.dot	3	7/7	21
BenchmarkMQTT/emqtt__two_client_same_id.dot	7	11/13	77
BenchmarkMQTT/emqtt__single_client.dot	10	11/10	110
BenchmarkMQTT/emqtt__two_client.dot	16	9/48	144
BenchmarkMQTT/VerneMQ__two_client.dot	16	9/42	144
BenchmarkMQTT/emqtt__invalid.dot	3	11/6	33
BenchmarkMQTT/emqtt__two_client_will_retain.dot	18	9/21	162
BenchmarkMQTT/VerneMQ__invalid.dot	3	11/7	33
BenchmarkMQTT/VerneMQ__non_clean.dot	12	6/18	72
BenchmarkMQTT/ActiveMQ__simple.dot	4	7/7	28
BenchmarkMQTT/hbmqtt__two_client_will_retain.dot	17	9/22	153
BenchmarkMQTT/ActiveMQ__single_client.dot	8	11/10	88
BenchmarkMQTT/ActiveMQ__non_clean.dot	12	6/18	72
BenchmarkMQTT/VerneMQ__single_client.dot	10	11/10	110
BenchmarkEdentifier2/learnresult_new_device-simple_fix.dot	3	5/4	15
BenchmarkEdentifier2/learnresult_old_500_10-15_fix.dot	22	8/9	176
BenchmarkEdentifier2/learnresult_new_Rand_500_10-15_MC_fix.d	11	8/9	88
BenchmarkEdentifier2/learnresult_new_W-method_fix.dot	8	8/8	64
BenchmarkEdentifier2/learnresult_old_device-simple_fix.dot	4	5/4	20
BenchmarkCoffeeMachine/coffeemachine.dot	6	4/3	24
BenchmarkToyModels/cacm.dot	3	2/3	6
BenchmarkToyModels/lee_yannakakis_non_distinguishable.dot	3	2/2	6
BenchmarkToyModels/naiks.dot	4	2/2	8
BenchmarkToyModels/lee_yannakakis_distinguishable.dot	6	2/2	12
BenchmarkFromRhapsodyToDezyne/model3.dot	58	22/16	1276
BenchmarkFromRhapsodyToDezyne/model2.dot	33	14/15	324
BenchmarkFromRhapsodyToDezyne/model1.dot	35	15/27	525
BenchmarkFromRhapsodyToDezyne/model4.dot	34	14/10	476
BenchmarkSSH/DropBear.dot	17	13/14	221
BenchmarkSSH/BitVise.dot	66	13/16	858
BenchmarkSSH/OpenSSH.dot	31	22/19	682
BenchmarkBankcard/4_learnresult_SecureCode Aut_fix.dot	4	14/9	56
BenchmarkBankcard/Volksbank_learnresult_MAESTRO_fix.dot	7	14/11	98
BenchmarkBankcard/ASN_learnresult_MAESTRO_fix.dot	6	14/10	84
BenchmarkBankcard/Rabo_learnresult_SecureCode_Aut_fix.dot	6	15/12	90
BenchmarkBankcard/10_learnresult_MasterCard_fix.dot	6	14/9	84
BenchmarkBankcard/ASN_learnresult_SecureCode Aut_fix.dot	4	14/9	56
BenchmarkBankcard/4_learnresult_PIN_fix.dot	6	14/10	84
BenchmarkBankcard/Rabo_learnresult_MAESTRO_fix.dot	6	14/10	84
BenchmarkBankcard/4_learnresult_MAESTRO_fix.dot	6	14/10	84
BenchmarkBankcard/learnresult_fix.dot	9	15/11	135
BenchmarkBankcard/1_learnresult_MasterCard_fix.dot	5	15/9	75
BenchmarkTLS/OpenSSL_1.0.2_server_regular.dot	7	7/7	49
BenchmarkTLS/OpenSSL_1.0.1j_server_regular.dot	11	7/9	77
BenchmarkTLS/OpenSSL_1.0.1g_server_regular.dot	16	7/11	112
BenchmarkTLS/OpenSSL_1.0.1l_client_regular.dot	6	7/5	42
BenchmarkTLS/miTLS_0.1.3_server_regular.dot	6	8/8	48
BenchmarkTLS/GnuTLS_3.3.8_server_full.dot	16	11/12	176
BenchmarkTLS/NSS_3.17.4_client_regular.dot	7	8/7	56
BenchmarkTLS/OpenSSL_1.0.2_client_regular.dot	6	7/5	42
BenchmarkTLS/OpenSSL_1.0.1g_client_regular.dot	10	7/7	70
BenchmarkTLS/OpenSSL_1.0.1j_client_regular.dot	6	7/5	42
BenchmarkTLS/OpenSSL_1.0.1l_server_regular.dot	10	7/8	70
BenchmarkTLS/RSA_BSAFE_Java_6.1.1_server_regular.dot	6	8/7	48
BenchmarkTLS/NSS_3.17.4_server_regular.dot	8	8/9	64
BenchmarkTLS/GnuTLS_3.3.12_client_full.dot	9	12/7	108
BenchmarkTLS/OpenSSL_1.0.2_client_full.dot	9	10/6	90
BenchmarkTLS/GnuTLS_3.3.12_server_regular.dot	7	8/10	56
BenchmarkTLS/GnuTLS_3.3.8_client_full.dot	15	12/8	180
BenchmarkTLS/GnuTLS_3.3.8_client_regular.dot	11	8/6	88
BenchmarkTLS/NSS_3.17.4_client_full.dot	11	12/9	132
BenchmarkTLS/GnuTLS_3.3.12_client_regular.dot	7	8/10	56
BenchmarkTLS/GnuTLS_3.3.8_server_regular.dot	12	8/10	96
BenchmarkTLS/GnuTLS_3.3.12_server_full.dot	9	12/12	108
BenchmarkTLS/RSA_BSAFE_C_4.0.4_server_regular.dot	9	8/11	72
BenchmarkTCP/TCP_Windows8_Server.dot	38	13/10	494
BenchmarkTCP/TCP_FreeBSD_Server.dot	55	13/11	715
BenchmarkTCP/TCP_Linux_Server.dot	57	12/9	684
BenchmarkTCP/TCP_Linux_Client.dot	15	10/11	150
BenchmarkTCP/TCP_Windows8_Client.dot	13	10/12	130
BenchmarkTCP/TCP_FreeBSD_Client.dot	12	10/12	120
BenchmarkX-ray-system-PCS/learnresult5.dot	9	12/9	66
BenchmarkX-ray-system-PCS/learnresult4.dot	7	9/7	37
BenchmarkX-ray-system-PCS/learnresult6.dot	9	12/9	66
BenchmarkX-ray-system-PCS/learnresult3.dot	7	9/7	37
BenchmarkX-ray-system-PCS/learnresult2.dot	3	9/4	9
BenchmarkX-ray-system-PCS/learnresult1.dot	8	9/7	44
BenchmarkESMcontroller/run3_hyp.101.obf.dot	3410	78/151	265980
BenchmarkESMcontroller/run1_hyp.135.obf.dot	3410	78/151	265980
BenchmarkESMcontroller/esm-manual-controller.dot	3410	78/151	265980
BenchmarkESMcontroller/run2_hyp.89.obf.dot	3338	78/151	260364

Automata Wiki

Model details

Scalable Register models

Register

Mealy