diff --git a/Benchmarking/StochasticAlgComparison.py b/Benchmarking/StochasticAlgComparison.py new file mode 100644 index 00000000..417f7262 --- /dev/null +++ b/Benchmarking/StochasticAlgComparison.py @@ -0,0 +1,84 @@ +import random +import time +from statistics import mean + +import aalpy.paths + +from aalpy.SULs import MdpSUL +from aalpy.learning_algs import run_stochastic_Lstar, run_Alergia +from aalpy.oracles.RandomWordEqOracle import RandomWordEqOracle +from aalpy.utils import load_automaton_from_file, get_properties_file, get_correct_prop_values +from aalpy.utils import model_check_experiment +from aalpy.automata.StochasticMealyMachine import smm_to_mdp_conversion + +path_to_dir = '../DotModels/MDPs/' +files = ['first_grid.dot', 'second_grid.dot', 'slot_machine.dot', 'mqtt.dot', 'tcp.dot', 'bluetooth.dot'] # + +prop_folder = 'prism_eval_props/' + +aalpy.paths.path_to_prism = "C:/Program Files/prism-4.6/bin/prism.bat" +aalpy.paths.path_to_properties = "prism_eval_props/" + +model_dict = {m.split('.')[0]: load_automaton_from_file(path_to_dir + m, automaton_type='mdp') for m in files} + +for file in files: + print(file) + + exp_name = file.split('.')[0] + + print('--------------------------------------------------') + print('Experiment:', exp_name) + + original_mdp = model_dict[exp_name] + input_alphabet = original_mdp.get_input_alphabet() + + mdp_sul = MdpSUL(original_mdp) + + eq_oracle = RandomWordEqOracle(input_alphabet, mdp_sul, num_walks=500, min_walk_len=5, + max_walk_len=16, reset_after_cex=True) + + learned_classic_mdp, data_mdp = run_stochastic_Lstar(input_alphabet, mdp_sul, eq_oracle, automaton_type='mdp', + min_rounds=10, strategy='classic', n_c=20, n_resample=500, + max_rounds=200, return_data=True, target_unambiguity=0.95, + print_level=1) + + del mdp_sul + del eq_oracle + + mdp_sul = MdpSUL(original_mdp) + + eq_oracle = RandomWordEqOracle(input_alphabet, mdp_sul, num_walks=150, min_walk_len=5, + max_walk_len=15, reset_after_cex=True) + + learned_smm, data_smm = run_stochastic_Lstar(input_alphabet, mdp_sul, eq_oracle, automaton_type='smm', + min_rounds=10, strategy='normal', + max_rounds=200, return_data=True, target_unambiguity=0.95, + print_level=1) + + smm_2_mdp = smm_to_mdp_conversion(learned_smm) + + mdp_results, mdp_err = model_check_experiment(get_properties_file(exp_name), + get_correct_prop_values(exp_name), learned_classic_mdp) + smm_results, smm_err = model_check_experiment(get_properties_file(exp_name), + get_correct_prop_values(exp_name), smm_2_mdp) + + num_alergia_samples = max([data_mdp["queries_learning"] + data_mdp["queries_eq_oracle"], + data_smm["queries_learning"] + data_smm["queries_eq_oracle"]]) + + alergia_samples = [] + for _ in range(num_alergia_samples): + sample = [mdp_sul.pre()] + for _ in range(random.randint(5, 25)): + action = random.choice(input_alphabet) + output = mdp_sul.step(action) + sample.append((action, output)) + alergia_samples.append(sample) + + alergia_model = run_Alergia(alergia_samples, automaton_type='mdp') + + alergia_results, alergia_error = model_check_experiment(get_properties_file(exp_name), + get_correct_prop_values(exp_name), alergia_model) + + print('Classic MDP learning', mean(mdp_err.values()), mdp_err) + print('SMM learning', mean(smm_err.values()), smm_err) + print('Alergia learning', mean(alergia_error.values()), alergia_error) \ No newline at end of file diff --git a/Benchmarking/StopWithErorrRate.py b/Benchmarking/StopWithErorrRate.py new file mode 100644 index 00000000..c81ac6a4 --- /dev/null +++ b/Benchmarking/StopWithErorrRate.py @@ -0,0 +1,49 @@ +import random +import time +from statistics import mean + +import aalpy.paths + +from aalpy.SULs import MdpSUL +from aalpy.learning_algs import run_stochastic_Lstar, run_Alergia +from aalpy.oracles.RandomWordEqOracle import RandomWordEqOracle +from aalpy.utils import load_automaton_from_file, get_properties_file, get_correct_prop_values, model_check_properties +from aalpy.utils import model_check_experiment +from aalpy.automata.StochasticMealyMachine import smm_to_mdp_conversion + +path_to_dir = '../DotModels/MDPs/' +files = ['slot_machine.dot', 'bluetooth.dot'] # +files.reverse() + +prop_folder = 'prism_eval_props/' + +aalpy.paths.path_to_prism = "C:/Program Files/prism-4.6/bin/prism.bat" +aalpy.paths.path_to_properties = "prism_eval_props/" + +model_dict = {m.split('.')[0]: load_automaton_from_file(path_to_dir + m, automaton_type='mdp') for m in files} + +model_type = ['mdp', 'smm'] +model_type.reverse() + +for file in files: + for mt in model_type: + exp_name = file.split('.')[0] + + print('--------------------------------------------------') + print('Experiment:', exp_name, ) + + original_mdp = model_dict[exp_name] + input_alphabet = original_mdp.get_input_alphabet() + + mdp_sul = MdpSUL(original_mdp) + + eq_oracle = RandomWordEqOracle(input_alphabet, mdp_sul, num_walks=500, min_walk_len=5, + max_walk_len=20, reset_after_cex=True) + + pbs = ((get_properties_file(exp_name), + get_correct_prop_values(exp_name), 0.02)) + learned_classic_mdp, data_mdp = run_stochastic_Lstar(input_alphabet, mdp_sul, eq_oracle, automaton_type=mt, + min_rounds=10, + property_based_stopping=pbs, + return_data=True, target_unambiguity=1.1, + print_level=2) diff --git a/DotModels/MDPs/bluetooth.dot b/DotModels/MDPs/bluetooth.dot index d9ed6049..48c74a5c 100644 --- a/DotModels/MDPs/bluetooth.dot +++ b/DotModels/MDPs/bluetooth.dot @@ -1,1042 +1,895 @@ -digraph CYW43455_stochastic { +digraph "CC2640R2-no-feature-req-stochastic" { 0 [label=___start___]; -s00 [label="BTLE|BTLE_CTRL|BTLE_DATA|LL_LENGTH_RSP"]; -s01 [label=E]; -s02 [label="BTLE|BTLE_CTRL|BTLE_DATA|LL_FEATURE_RSP"]; -s03 [label=SYSTEM_CRASH]; -s04 [label="BTLE|BTLE_CTRL|BTLE_DATA|LL_REJECT_IND"]; -s10 [label="BTLE|BTLE_CTRL|BTLE_DATA|LL_FEATURE_RSP"]; -s11 [label="BTLE|BTLE_DATA"]; -s12 [label="BTLE|BTLE_CTRL|BTLE_DATA|LL_LENGTH_RSP"]; -s13 [label="BTLE|BTLE_CTRL|BTLE_DATA|LL_REJECT_IND"]; -s20 [label="BTLE|BTLE_CTRL|BTLE_DATA|LL_FEATURE_RSP"]; -s21 [label="BTLE|BTLE_DATA"]; -s22 [label="BTLE|BTLE_CTRL|BTLE_DATA|LL_LENGTH_RSP"]; -s23 [label="BTLE|BTLE_CTRL|BTLE_DATA|LL_REJECT_IND"]; -s30 [label="BTLE|BTLE_DATA"]; -s31 [label="BTLE|BTLE_CTRL|BTLE_DATA|LL_LENGTH_RSP"]; -s32 [label="BTLE|BTLE_CTRL|BTLE_DATA|LL_VERSION_IND"]; -s33 [label="BTLE|BTLE_CTRL|BTLE_DATA|LL_FEATURE_RSP"]; -s34 [label="BTLE|BTLE_CTRL|BTLE_DATA|LL_REJECT_IND"]; -s40 [label="BTLE|BTLE_DATA"]; -s41 [label="BTLE|BTLE_CTRL|BTLE_DATA|LL_LENGTH_RSP"]; -s42 [label="ATT_Exchange_MTU_Request|ATT_Exchange_MTU_Response|ATT_Hdr|BTLE|BTLE_CTRL|BTLE_DATA|L2CAP_CmdHdr|L2CAP_Connection_Parameter_Update_Request|L2CAP_Hdr|LL_LENGTH_REQ"]; -s43 [label="BTLE|BTLE_CTRL|BTLE_DATA|LL_FEATURE_RSP"]; -s44 [label="ATT_Exchange_MTU_Response|ATT_Hdr|BTLE|BTLE_DATA|L2CAP_Hdr"]; -s45 [label="ATT_Exchange_MTU_Request|ATT_Hdr|BTLE|BTLE_CTRL|BTLE_DATA|L2CAP_CmdHdr|L2CAP_Connection_Parameter_Update_Request|L2CAP_Hdr|LL_LENGTH_REQ"]; -s50 [label="BTLE|BTLE_DATA"]; -s51 [label="BTLE|BTLE_CTRL|BTLE_DATA|LL_LENGTH_RSP"]; -s52 [label="BTLE|BTLE_CTRL|BTLE_DATA|LL_FEATURE_RSP"]; -s53 [label="ATT_Exchange_MTU_Response|ATT_Hdr|BTLE|BTLE_DATA|L2CAP_Hdr"]; -s54 [label="BTLE|BTLE_CTRL|BTLE_DATA|LL_REJECT_IND"]; -s60 [label="BTLE|BTLE_DATA"]; -s61 [label="BTLE|BTLE_CTRL|BTLE_DATA|LL_LENGTH_RSP"]; -s62 [label="BTLE|BTLE_CTRL|BTLE_DATA|LL_VERSION_IND"]; -s63 [label="ATT_Exchange_MTU_Request|ATT_Exchange_MTU_Response|ATT_Hdr|BTLE|BTLE_CTRL|BTLE_DATA|L2CAP_CmdHdr|L2CAP_Connection_Parameter_Update_Request|L2CAP_Hdr|LL_LENGTH_REQ"]; -s64 [label="BTLE|BTLE_CTRL|BTLE_DATA|LL_FEATURE_RSP"]; -s65 [label="ATT_Exchange_MTU_Response|ATT_Hdr|BTLE|BTLE_DATA|L2CAP_Hdr"]; -s66 [label="ATT_Exchange_MTU_Request|ATT_Hdr|BTLE|BTLE_CTRL|BTLE_DATA|L2CAP_CmdHdr|L2CAP_Connection_Parameter_Update_Request|L2CAP_Hdr|LL_LENGTH_REQ"]; -s70 [label="BTLE|BTLE_DATA"]; -s71 [label="BTLE|BTLE_CTRL|BTLE_DATA|LL_LENGTH_RSP"]; -s72 [label="BTLE|BTLE_CTRL|BTLE_DATA|LL_VERSION_IND"]; -s73 [label="BTLE|BTLE_CTRL|BTLE_DATA|LL_FEATURE_RSP"]; -s74 [label="BTLE|BTLE_CTRL|BTLE_DATA|LL_REJECT_IND"]; -s80 [label="BTLE|BTLE_CTRL|BTLE_DATA|LL_FEATURE_RSP"]; -s81 [label="BTLE|BTLE_DATA"]; -s82 [label="BTLE|BTLE_CTRL|BTLE_DATA|LL_LENGTH_RSP"]; -s90 [label="BTLE|BTLE_DATA"]; -s91 [label="BTLE|BTLE_CTRL|BTLE_DATA|LL_LENGTH_RSP"]; -s92 [label="BTLE|BTLE_CTRL|BTLE_DATA|LL_VERSION_IND"]; -s93 [label="BTLE|BTLE_CTRL|BTLE_DATA|LL_FEATURE_RSP"]; -s94 [label="BTLE|BTLE_CTRL|BTLE_DATA|LL_REJECT_IND"]; -s100 [label="BTLE|BTLE_DATA"]; -s101 [label="BTLE|BTLE_CTRL|BTLE_DATA|LL_LENGTH_RSP"]; -s102 [label="ATT_Exchange_MTU_Request|ATT_Hdr|BTLE|BTLE_CTRL|BTLE_DATA|L2CAP_CmdHdr|L2CAP_Connection_Parameter_Update_Request|L2CAP_Hdr|LL_LENGTH_REQ|SM_Hdr|SM_Pairing_Response"]; -s103 [label="BTLE|BTLE_CTRL|BTLE_DATA|LL_FEATURE_RSP"]; -s104 [label="ATT_Exchange_MTU_Response|ATT_Hdr|BTLE|BTLE_DATA|L2CAP_Hdr"]; -s105 [label="ATT_Exchange_MTU_Request|ATT_Exchange_MTU_Response|ATT_Hdr|BTLE|BTLE_CTRL|BTLE_DATA|L2CAP_CmdHdr|L2CAP_Connection_Parameter_Update_Request|L2CAP_Hdr|LL_LENGTH_REQ|SM_Hdr|SM_Pairing_Response"]; -s106 [label="BTLE|BTLE_DATA|L2CAP_Hdr|SM_Hdr|SM_Pairing_Response"]; -s110 [label="BTLE|BTLE_DATA"]; -s111 [label="BTLE|BTLE_CTRL|BTLE_DATA|LL_LENGTH_RSP"]; -s112 [label="BTLE|BTLE_CTRL|BTLE_DATA|LL_VERSION_IND"]; -s113 [label="BTLE|BTLE_CTRL|BTLE_DATA|LL_FEATURE_RSP"]; -s114 [label="BTLE|BTLE_CTRL|BTLE_DATA|LL_REJECT_IND"]; -s120 [label="BTLE|BTLE_DATA"]; -s121 [label="BTLE|BTLE_CTRL|BTLE_DATA|LL_LENGTH_RSP"]; -s122 [label="BTLE|BTLE_CTRL|BTLE_DATA|LL_VERSION_IND"]; -s123 [label="ATT_Exchange_MTU_Request|ATT_Hdr|BTLE|BTLE_CTRL|BTLE_DATA|L2CAP_CmdHdr|L2CAP_Connection_Parameter_Update_Request|L2CAP_Hdr|LL_LENGTH_REQ|SM_Hdr|SM_Pairing_Response"]; -s124 [label="BTLE|BTLE_CTRL|BTLE_DATA|LL_FEATURE_RSP"]; -s125 [label="ATT_Exchange_MTU_Response|ATT_Hdr|BTLE|BTLE_DATA|L2CAP_Hdr"]; -s126 [label="ATT_Exchange_MTU_Request|ATT_Exchange_MTU_Response|ATT_Hdr|BTLE|BTLE_CTRL|BTLE_DATA|L2CAP_CmdHdr|L2CAP_Connection_Parameter_Update_Request|L2CAP_Hdr|LL_LENGTH_REQ|SM_Hdr|SM_Pairing_Response"]; -s127 [label="BTLE|BTLE_DATA|L2CAP_Hdr|SM_Hdr|SM_Pairing_Response"]; -s130 [label="BTLE|BTLE_DATA"]; -s131 [label="BTLE|BTLE_CTRL|BTLE_DATA|LL_LENGTH_RSP"]; -s132 [label="BTLE|BTLE_CTRL|BTLE_DATA|LL_FEATURE_RSP"]; -s133 [label="ATT_Exchange_MTU_Response|ATT_Hdr|BTLE|BTLE_DATA|L2CAP_Hdr"]; -s134 [label="BTLE|BTLE_CTRL|BTLE_DATA|LL_REJECT_IND"]; -s135 [label="BTLE|BTLE_DATA|L2CAP_Hdr|SM_Hdr|SM_Pairing_Response"]; -s140 [label="BTLE|BTLE_DATA"]; -s141 [label="BTLE|BTLE_CTRL|BTLE_DATA|LL_LENGTH_RSP"]; -s142 [label="BTLE|BTLE_CTRL|BTLE_DATA|LL_VERSION_IND"]; -s143 [label="BTLE|BTLE_CTRL|BTLE_DATA|LL_FEATURE_RSP"]; -s144 [label="ATT_Exchange_MTU_Response|ATT_Hdr|BTLE|BTLE_DATA|L2CAP_Hdr"]; -s145 [label="BTLE|BTLE_CTRL|BTLE_DATA|LL_REJECT_IND"]; -s150 [label="BTLE|BTLE_DATA"]; -s151 [label="BTLE|BTLE_CTRL|BTLE_DATA|LL_LENGTH_RSP"]; -s152 [label="BTLE|BTLE_CTRL|BTLE_DATA|LL_VERSION_IND"]; -s153 [label="BTLE|BTLE_CTRL|BTLE_DATA|LL_FEATURE_RSP"]; -s154 [label="ATT_Exchange_MTU_Response|ATT_Hdr|BTLE|BTLE_DATA|L2CAP_Hdr"]; -s155 [label="BTLE|BTLE_CTRL|BTLE_DATA|LL_REJECT_IND"]; -s156 [label="BTLE|BTLE_DATA|L2CAP_Hdr|SM_Hdr|SM_Pairing_Response"]; -0 -> s01 [label="length_req:0.2"]; -0 -> s00 [label="length_req:0.8"]; -0 -> s00 [label="length_req:1.0"]; -0 -> s01 [label="length_rsp:0.2"]; -0 -> s04 [label="length_rsp:0.8"]; -0 -> s04 [label="length_rsp:1.0"]; -0 -> s01 [label="feature_req:0.2"]; -0 -> s02 [label="feature_req:0.8"]; -0 -> s02 [label="feature_req:1.0"]; -0 -> s01 [label="feature_rsp:0.2"]; -0 -> s45 [label="feature_rsp:0.8"]; -0 -> s45 [label="feature_rsp:1.0"]; -0 -> s01 [label="version_req:0.2"]; -0 -> s32 [label="version_req:0.8"]; -0 -> s32 [label="version_req:1.0"]; -0 -> s01 [label="mtu_req:0.2"]; -0 -> s21 [label="mtu_req:0.8"]; -0 -> s21 [label="mtu_req:1.0"]; -0 -> s01 [label="pairing_req:0.2"]; -0 -> s11 [label="pairing_req:0.8"]; -0 -> s11 [label="pairing_req:1.0"]; -s00 -> s01 [label="length_req:0.2"]; -s00 -> s00 [label="length_req:0.8"]; -s00 -> s00 [label="length_req:1.0"]; -s00 -> s01 [label="length_rsp:0.2"]; -s00 -> s04 [label="length_rsp:0.8"]; -s00 -> s04 [label="length_rsp:1.0"]; -s00 -> s01 [label="feature_req:0.2"]; -s00 -> s02 [label="feature_req:0.8"]; -s00 -> s02 [label="feature_req:1.0"]; -s00 -> s01 [label="feature_rsp:0.2"]; -s00 -> s45 [label="feature_rsp:0.8"]; -s00 -> s45 [label="feature_rsp:1.0"]; -s00 -> s01 [label="version_req:0.2"]; -s00 -> s32 [label="version_req:0.8"]; -s00 -> s32 [label="version_req:1.0"]; -s00 -> s01 [label="mtu_req:0.2"]; -s00 -> s21 [label="mtu_req:0.8"]; -s00 -> s21 [label="mtu_req:1.0"]; -s00 -> s01 [label="pairing_req:0.2"]; -s00 -> s11 [label="pairing_req:0.8"]; -s00 -> s11 [label="pairing_req:1.0"]; -s01 -> s01 [label="length_req:0.2"]; -s01 -> s00 [label="length_req:0.8"]; -s01 -> s00 [label="length_req:1.0"]; -s01 -> s01 [label="length_rsp:0.2"]; -s01 -> s04 [label="length_rsp:0.8"]; -s01 -> s04 [label="length_rsp:1.0"]; -s01 -> s01 [label="feature_req:0.2"]; -s01 -> s02 [label="feature_req:0.8"]; -s01 -> s02 [label="feature_req:1.0"]; -s01 -> s01 [label="feature_rsp:0.2"]; -s01 -> s45 [label="feature_rsp:0.8"]; -s01 -> s45 [label="feature_rsp:1.0"]; -s01 -> s01 [label="version_req:0.2"]; -s01 -> s32 [label="version_req:0.8"]; -s01 -> s32 [label="version_req:1.0"]; -s01 -> s01 [label="mtu_req:0.2"]; -s01 -> s21 [label="mtu_req:0.8"]; -s01 -> s21 [label="mtu_req:1.0"]; -s01 -> s01 [label="pairing_req:0.2"]; -s01 -> s11 [label="pairing_req:0.8"]; -s01 -> s11 [label="pairing_req:1.0"]; -s02 -> s01 [label="length_req:0.2"]; -s02 -> s00 [label="length_req:0.8"]; -s02 -> s00 [label="length_req:1.0"]; -s02 -> s01 [label="length_rsp:0.2"]; -s02 -> s04 [label="length_rsp:0.8"]; -s02 -> s04 [label="length_rsp:1.0"]; -s02 -> s01 [label="feature_req:0.2"]; -s02 -> s02 [label="feature_req:0.8"]; -s02 -> s02 [label="feature_req:1.0"]; -s02 -> s01 [label="feature_rsp:0.2"]; -s02 -> s45 [label="feature_rsp:0.8"]; -s02 -> s45 [label="feature_rsp:1.0"]; -s02 -> s01 [label="version_req:0.2"]; -s02 -> s32 [label="version_req:0.8"]; -s02 -> s32 [label="version_req:1.0"]; -s02 -> s01 [label="mtu_req:0.2"]; -s02 -> s21 [label="mtu_req:0.8"]; -s02 -> s21 [label="mtu_req:1.0"]; -s02 -> s01 [label="pairing_req:0.2"]; -s02 -> s11 [label="pairing_req:0.8"]; -s02 -> s11 [label="pairing_req:1.0"]; -s03 -> s01 [label="length_req:0.2"]; -s03 -> s00 [label="length_req:0.8"]; -s03 -> s00 [label="length_req:1.0"]; -s03 -> s01 [label="length_rsp:0.2"]; -s03 -> s04 [label="length_rsp:0.8"]; -s03 -> s04 [label="length_rsp:1.0"]; -s03 -> s01 [label="feature_req:0.2"]; -s03 -> s02 [label="feature_req:0.8"]; -s03 -> s02 [label="feature_req:1.0"]; -s03 -> s01 [label="feature_rsp:0.2"]; -s03 -> s45 [label="feature_rsp:0.8"]; -s03 -> s45 [label="feature_rsp:1.0"]; -s03 -> s01 [label="version_req:0.2"]; -s03 -> s32 [label="version_req:0.8"]; -s03 -> s32 [label="version_req:1.0"]; -s03 -> s01 [label="mtu_req:0.2"]; -s03 -> s21 [label="mtu_req:0.8"]; -s03 -> s21 [label="mtu_req:1.0"]; -s03 -> s01 [label="pairing_req:0.2"]; -s03 -> s11 [label="pairing_req:0.8"]; -s03 -> s11 [label="pairing_req:1.0"]; -s04 -> s01 [label="length_req:0.2"]; -s04 -> s00 [label="length_req:0.8"]; -s04 -> s00 [label="length_req:1.0"]; -s04 -> s01 [label="length_rsp:0.2"]; -s04 -> s04 [label="length_rsp:0.8"]; -s04 -> s04 [label="length_rsp:1.0"]; -s04 -> s01 [label="feature_req:0.2"]; -s04 -> s02 [label="feature_req:0.8"]; -s04 -> s02 [label="feature_req:1.0"]; -s04 -> s01 [label="feature_rsp:0.2"]; -s04 -> s45 [label="feature_rsp:0.8"]; -s04 -> s45 [label="feature_rsp:1.0"]; -s04 -> s01 [label="version_req:0.2"]; -s04 -> s32 [label="version_req:0.8"]; -s04 -> s32 [label="version_req:1.0"]; -s04 -> s01 [label="mtu_req:0.2"]; -s04 -> s21 [label="mtu_req:0.8"]; -s04 -> s21 [label="mtu_req:1.0"]; -s04 -> s01 [label="pairing_req:0.2"]; -s04 -> s11 [label="pairing_req:0.8"]; -s04 -> s11 [label="pairing_req:1.0"]; +s00 [label=BTLE_BTLE_CTRL_BTLE_DATA_LL_REJECT_IND]; +s01 [label=crash]; +s02 [label=BTLE_BTLE_CTRL_BTLE_DATA_LL_LENGTH_RSP]; +s03 [label=no_response]; +s04 [label=BTLE_BTLE_CTRL_BTLE_DATA_LL_FEATURE_RSP]; +s10 [label=BTLE_BTLE_DATA]; +s11 [label=BTLE_BTLE_CTRL_BTLE_DATA_LL_FEATURE_RSP]; +s12 [label=BTLE_BTLE_CTRL_BTLE_DATA_LL_LENGTH_RSP]; +s13 [label=BTLE_BTLE_CTRL_BTLE_DATA_LL_REJECT_IND]; +s20 [label=BTLE_BTLE_DATA]; +s21 [label=BTLE_BTLE_CTRL_BTLE_DATA_LL_FEATURE_RSP]; +s22 [label=BTLE_BTLE_CTRL_BTLE_DATA_LL_LENGTH_RSP]; +s23 [label=BTLE_BTLE_CTRL_BTLE_DATA_LL_REJECT_IND]; +s30 [label=BTLE_BTLE_DATA]; +s31 [label=BTLE_BTLE_CTRL_BTLE_DATA_LL_REJECT_IND]; +s32 [label=BTLE_BTLE_CTRL_BTLE_DATA_LL_LENGTH_RSP]; +s33 [label=BTLE_BTLE_CTRL_BTLE_DATA_LL_VERSION_IND]; +s34 [label=BTLE_BTLE_CTRL_BTLE_DATA_LL_FEATURE_RSP]; +s40 [label=BTLE_BTLE_DATA]; +s41 [label=ATT_Exchange_MTU_Request_ATT_Exchange_MTU_Response_ATT_Hdr_BTLE_BTLE_CTRL_BTLE_DATA_L2CAP_CmdHdr_L2CAP_Connection_Parameter_Update_Request_L2CAP_Hdr_LL_LENGTH_REQ]; +s42 [label=BTLE_BTLE_CTRL_BTLE_DATA_LL_LENGTH_RSP]; +s43 [label=ATT_Exchange_MTU_Request_ATT_Hdr_BTLE_BTLE_CTRL_BTLE_DATA_L2CAP_CmdHdr_L2CAP_Connection_Parameter_Update_Request_L2CAP_Hdr_LL_LENGTH_REQ]; +s44 [label=ATT_Exchange_MTU_Response_ATT_Hdr_BTLE_BTLE_DATA_L2CAP_Hdr]; +s45 [label=BTLE_BTLE_CTRL_BTLE_DATA_LL_FEATURE_RSP]; +s50 [label=BTLE_BTLE_DATA]; +s51 [label=BTLE_BTLE_CTRL_BTLE_DATA_LL_REJECT_IND]; +s52 [label=BTLE_BTLE_CTRL_BTLE_DATA_LL_LENGTH_RSP]; +s53 [label=ATT_Exchange_MTU_Response_ATT_Hdr_BTLE_BTLE_DATA_L2CAP_Hdr]; +s54 [label=BTLE_BTLE_CTRL_BTLE_DATA_LL_FEATURE_RSP]; +s60 [label=BTLE_BTLE_DATA]; +s61 [label=ATT_Exchange_MTU_Request_ATT_Exchange_MTU_Response_ATT_Hdr_BTLE_BTLE_CTRL_BTLE_DATA_L2CAP_CmdHdr_L2CAP_Connection_Parameter_Update_Request_L2CAP_Hdr_LL_LENGTH_REQ]; +s62 [label=BTLE_BTLE_CTRL_BTLE_DATA_LL_LENGTH_RSP]; +s63 [label=ATT_Exchange_MTU_Request_ATT_Hdr_BTLE_BTLE_CTRL_BTLE_DATA_L2CAP_CmdHdr_L2CAP_Connection_Parameter_Update_Request_L2CAP_Hdr_LL_LENGTH_REQ]; +s64 [label=ATT_Exchange_MTU_Response_ATT_Hdr_BTLE_BTLE_DATA_L2CAP_Hdr]; +s65 [label=BTLE_BTLE_CTRL_BTLE_DATA_LL_VERSION_IND]; +s66 [label=BTLE_BTLE_CTRL_BTLE_DATA_LL_FEATURE_RSP]; +s70 [label=BTLE_BTLE_DATA]; +s71 [label=BTLE_BTLE_CTRL_BTLE_DATA_LL_REJECT_IND]; +s72 [label=BTLE_BTLE_CTRL_BTLE_DATA_LL_LENGTH_RSP]; +s73 [label=BTLE_BTLE_CTRL_BTLE_DATA_LL_VERSION_IND]; +s74 [label=BTLE_BTLE_CTRL_BTLE_DATA_LL_FEATURE_RSP]; +s80 [label=BTLE_BTLE_DATA]; +s81 [label=BTLE_BTLE_CTRL_BTLE_DATA_LL_FEATURE_RSP]; +s82 [label=BTLE_BTLE_CTRL_BTLE_DATA_LL_LENGTH_RSP]; +s90 [label=BTLE_BTLE_DATA]; +s91 [label=BTLE_BTLE_CTRL_BTLE_DATA_LL_REJECT_IND]; +s92 [label=BTLE_BTLE_CTRL_BTLE_DATA_LL_LENGTH_RSP]; +s93 [label=BTLE_BTLE_CTRL_BTLE_DATA_LL_VERSION_IND]; +s94 [label=BTLE_BTLE_CTRL_BTLE_DATA_LL_FEATURE_RSP]; +s100 [label=BTLE_BTLE_DATA]; +s101 [label=BTLE_BTLE_DATA_L2CAP_Hdr_SM_Hdr_SM_Pairing_Response]; +s102 [label=BTLE_BTLE_CTRL_BTLE_DATA_LL_LENGTH_RSP]; +s103 [label=BTLE_BTLE_CTRL_BTLE_DATA_LL_FEATURE_RSP]; +s104 [label=ATT_Exchange_MTU_Request_ATT_Hdr_BTLE_BTLE_CTRL_BTLE_DATA_L2CAP_CmdHdr_L2CAP_Connection_Parameter_Update_Request_L2CAP_Hdr_LL_LENGTH_REQ_SM_Hdr_SM_Pairing_Response]; +s105 [label=ATT_Exchange_MTU_Response_ATT_Hdr_BTLE_BTLE_DATA_L2CAP_Hdr]; +s106 [label=ATT_Exchange_MTU_Request_ATT_Exchange_MTU_Response_ATT_Hdr_BTLE_BTLE_CTRL_BTLE_DATA_L2CAP_CmdHdr_L2CAP_Connection_Parameter_Update_Request_L2CAP_Hdr_LL_LENGTH_REQ_SM_Hdr_SM_Pairing_Response]; +s110 [label=BTLE_BTLE_DATA]; +s111 [label=BTLE_BTLE_CTRL_BTLE_DATA_LL_REJECT_IND]; +s112 [label=BTLE_BTLE_CTRL_BTLE_DATA_LL_LENGTH_RSP]; +s113 [label=BTLE_BTLE_CTRL_BTLE_DATA_LL_VERSION_IND]; +s114 [label=BTLE_BTLE_CTRL_BTLE_DATA_LL_FEATURE_RSP]; +s120 [label=BTLE_BTLE_DATA]; +s121 [label=BTLE_BTLE_DATA_L2CAP_Hdr_SM_Hdr_SM_Pairing_Response]; +s122 [label=BTLE_BTLE_CTRL_BTLE_DATA_LL_LENGTH_RSP]; +s123 [label=BTLE_BTLE_CTRL_BTLE_DATA_LL_FEATURE_RSP]; +s124 [label=ATT_Exchange_MTU_Request_ATT_Hdr_BTLE_BTLE_CTRL_BTLE_DATA_L2CAP_CmdHdr_L2CAP_Connection_Parameter_Update_Request_L2CAP_Hdr_LL_LENGTH_REQ_SM_Hdr_SM_Pairing_Response]; +s125 [label=ATT_Exchange_MTU_Response_ATT_Hdr_BTLE_BTLE_DATA_L2CAP_Hdr]; +s126 [label=BTLE_BTLE_CTRL_BTLE_DATA_LL_VERSION_IND]; +s127 [label=ATT_Exchange_MTU_Request_ATT_Exchange_MTU_Response_ATT_Hdr_BTLE_BTLE_CTRL_BTLE_DATA_L2CAP_CmdHdr_L2CAP_Connection_Parameter_Update_Request_L2CAP_Hdr_LL_LENGTH_REQ_SM_Hdr_SM_Pairing_Response]; +s130 [label=BTLE_BTLE_DATA]; +s131 [label=BTLE_BTLE_CTRL_BTLE_DATA_LL_REJECT_IND]; +s132 [label=BTLE_BTLE_DATA_L2CAP_Hdr_SM_Hdr_SM_Pairing_Response]; +s133 [label=BTLE_BTLE_CTRL_BTLE_DATA_LL_LENGTH_RSP]; +s134 [label=ATT_Exchange_MTU_Response_ATT_Hdr_BTLE_BTLE_DATA_L2CAP_Hdr]; +s135 [label=BTLE_BTLE_CTRL_BTLE_DATA_LL_FEATURE_RSP]; +s140 [label=BTLE_BTLE_DATA]; +s141 [label=BTLE_BTLE_CTRL_BTLE_DATA_LL_REJECT_IND]; +s142 [label=BTLE_BTLE_CTRL_BTLE_DATA_LL_LENGTH_RSP]; +s143 [label=ATT_Exchange_MTU_Response_ATT_Hdr_BTLE_BTLE_DATA_L2CAP_Hdr]; +s144 [label=BTLE_BTLE_CTRL_BTLE_DATA_LL_VERSION_IND]; +s145 [label=BTLE_BTLE_CTRL_BTLE_DATA_LL_FEATURE_RSP]; +s150 [label=BTLE_BTLE_DATA]; +s151 [label=BTLE_BTLE_CTRL_BTLE_DATA_LL_REJECT_IND]; +s152 [label=BTLE_BTLE_DATA_L2CAP_Hdr_SM_Hdr_SM_Pairing_Response]; +s153 [label=BTLE_BTLE_CTRL_BTLE_DATA_LL_LENGTH_RSP]; +s154 [label=ATT_Exchange_MTU_Response_ATT_Hdr_BTLE_BTLE_DATA_L2CAP_Hdr]; +s155 [label=BTLE_BTLE_CTRL_BTLE_DATA_LL_VERSION_IND]; +s156 [label=BTLE_BTLE_CTRL_BTLE_DATA_LL_FEATURE_RSP]; +0 -> s03 [label="length_req:0.2"]; +0 -> s02 [label="length_req:0.8"]; +0 -> s03 [label="length_rsp:0.2"]; +0 -> s00 [label="length_rsp:0.8"]; +0 -> s03 [label="feature_req:0.2"]; +0 -> s04 [label="feature_req:0.8"]; +0 -> s03 [label="feature_rsp:0.2"]; +0 -> s43 [label="feature_rsp:0.8"]; +0 -> s03 [label="version_req:0.2"]; +0 -> s33 [label="version_req:0.8"]; +0 -> s03 [label="mtu_req:0.2"]; +0 -> s20 [label="mtu_req:0.8"]; +0 -> s03 [label="pairing_req:0.2"]; +0 -> s10 [label="pairing_req:0.8"]; +s00 -> s03 [label="length_req:0.2"]; +s00 -> s02 [label="length_req:0.8"]; +s00 -> s03 [label="length_rsp:0.2"]; +s00 -> s00 [label="length_rsp:0.8"]; +s00 -> s03 [label="feature_req:0.2"]; +s00 -> s04 [label="feature_req:0.8"]; +s00 -> s03 [label="feature_rsp:0.2"]; +s00 -> s43 [label="feature_rsp:0.8"]; +s00 -> s03 [label="version_req:0.2"]; +s00 -> s33 [label="version_req:0.8"]; +s00 -> s03 [label="mtu_req:0.2"]; +s00 -> s20 [label="mtu_req:0.8"]; +s00 -> s03 [label="pairing_req:0.2"]; +s00 -> s10 [label="pairing_req:0.8"]; +s01 -> s03 [label="length_req:0.2"]; +s01 -> s02 [label="length_req:0.8"]; +s01 -> s03 [label="length_rsp:0.2"]; +s01 -> s00 [label="length_rsp:0.8"]; +s01 -> s03 [label="feature_req:0.2"]; +s01 -> s04 [label="feature_req:0.8"]; +s01 -> s03 [label="feature_rsp:0.2"]; +s01 -> s43 [label="feature_rsp:0.8"]; +s01 -> s03 [label="version_req:0.2"]; +s01 -> s33 [label="version_req:0.8"]; +s01 -> s03 [label="mtu_req:0.2"]; +s01 -> s20 [label="mtu_req:0.8"]; +s01 -> s03 [label="pairing_req:0.2"]; +s01 -> s10 [label="pairing_req:0.8"]; +s02 -> s03 [label="length_req:0.2"]; +s02 -> s02 [label="length_req:0.8"]; +s02 -> s03 [label="length_rsp:0.2"]; +s02 -> s00 [label="length_rsp:0.8"]; +s02 -> s03 [label="feature_req:0.2"]; +s02 -> s04 [label="feature_req:0.8"]; +s02 -> s03 [label="feature_rsp:0.2"]; +s02 -> s43 [label="feature_rsp:0.8"]; +s02 -> s03 [label="version_req:0.2"]; +s02 -> s33 [label="version_req:0.8"]; +s02 -> s03 [label="mtu_req:0.2"]; +s02 -> s20 [label="mtu_req:0.8"]; +s02 -> s03 [label="pairing_req:0.2"]; +s02 -> s10 [label="pairing_req:0.8"]; +s03 -> s03 [label="length_req:0.2"]; +s03 -> s02 [label="length_req:0.8"]; +s03 -> s03 [label="length_rsp:0.2"]; +s03 -> s00 [label="length_rsp:0.8"]; +s03 -> s03 [label="feature_req:0.2"]; +s03 -> s04 [label="feature_req:0.8"]; +s03 -> s03 [label="feature_rsp:0.2"]; +s03 -> s43 [label="feature_rsp:0.8"]; +s03 -> s03 [label="version_req:0.2"]; +s03 -> s33 [label="version_req:0.8"]; +s03 -> s03 [label="mtu_req:0.2"]; +s03 -> s20 [label="mtu_req:0.8"]; +s03 -> s03 [label="pairing_req:0.2"]; +s03 -> s10 [label="pairing_req:0.8"]; +s04 -> s03 [label="length_req:0.2"]; +s04 -> s02 [label="length_req:0.8"]; +s04 -> s03 [label="length_rsp:0.2"]; +s04 -> s00 [label="length_rsp:0.8"]; +s04 -> s03 [label="feature_req:0.2"]; +s04 -> s04 [label="feature_req:0.8"]; +s04 -> s03 [label="feature_rsp:0.2"]; +s04 -> s43 [label="feature_rsp:0.8"]; +s04 -> s03 [label="version_req:0.2"]; +s04 -> s33 [label="version_req:0.8"]; +s04 -> s03 [label="mtu_req:0.2"]; +s04 -> s20 [label="mtu_req:0.8"]; +s04 -> s03 [label="pairing_req:0.2"]; +s04 -> s10 [label="pairing_req:0.8"]; s10 -> s12 [label="length_req:1.0"]; s10 -> s13 [label="length_rsp:1.0"]; -s10 -> s10 [label="feature_req:1.0"]; -s10 -> s102 [label="feature_rsp:1.0"]; -s10 -> s92 [label="version_req:1.0"]; -s10 -> s81 [label="mtu_req:1.0"]; -s10 -> s11 [label="pairing_req:1.0"]; +s10 -> s11 [label="feature_req:1.0"]; +s10 -> s104 [label="feature_rsp:1.0"]; +s10 -> s93 [label="version_req:1.0"]; +s10 -> s80 [label="mtu_req:1.0"]; +s10 -> s10 [label="pairing_req:1.0"]; s11 -> s12 [label="length_req:1.0"]; s11 -> s13 [label="length_rsp:1.0"]; -s11 -> s10 [label="feature_req:1.0"]; -s11 -> s102 [label="feature_rsp:1.0"]; -s11 -> s92 [label="version_req:1.0"]; -s11 -> s81 [label="mtu_req:1.0"]; -s11 -> s11 [label="pairing_req:1.0"]; +s11 -> s11 [label="feature_req:1.0"]; +s11 -> s104 [label="feature_rsp:1.0"]; +s11 -> s93 [label="version_req:1.0"]; +s11 -> s80 [label="mtu_req:1.0"]; +s11 -> s10 [label="pairing_req:1.0"]; s12 -> s12 [label="length_req:1.0"]; s12 -> s13 [label="length_rsp:1.0"]; -s12 -> s10 [label="feature_req:1.0"]; -s12 -> s102 [label="feature_rsp:1.0"]; -s12 -> s92 [label="version_req:1.0"]; -s12 -> s81 [label="mtu_req:1.0"]; -s12 -> s11 [label="pairing_req:1.0"]; +s12 -> s11 [label="feature_req:1.0"]; +s12 -> s104 [label="feature_rsp:1.0"]; +s12 -> s93 [label="version_req:1.0"]; +s12 -> s80 [label="mtu_req:1.0"]; +s12 -> s10 [label="pairing_req:1.0"]; s13 -> s12 [label="length_req:1.0"]; s13 -> s13 [label="length_rsp:1.0"]; -s13 -> s10 [label="feature_req:1.0"]; -s13 -> s102 [label="feature_rsp:1.0"]; -s13 -> s92 [label="version_req:1.0"]; -s13 -> s81 [label="mtu_req:1.0"]; -s13 -> s11 [label="pairing_req:1.0"]; +s13 -> s11 [label="feature_req:1.0"]; +s13 -> s104 [label="feature_rsp:1.0"]; +s13 -> s93 [label="version_req:1.0"]; +s13 -> s80 [label="mtu_req:1.0"]; +s13 -> s10 [label="pairing_req:1.0"]; s20 -> s22 [label="length_req:1.0"]; s20 -> s23 [label="length_rsp:1.0"]; -s20 -> s20 [label="feature_req:1.0"]; -s20 -> s42 [label="feature_rsp:1.0"]; -s20 -> s72 [label="version_req:1.0"]; -s20 -> s21 [label="mtu_req:1.0"]; -s20 -> s81 [label="pairing_req:1.0"]; +s20 -> s21 [label="feature_req:1.0"]; +s20 -> s41 [label="feature_rsp:1.0"]; +s20 -> s73 [label="version_req:1.0"]; +s20 -> s20 [label="mtu_req:1.0"]; +s20 -> s80 [label="pairing_req:1.0"]; s21 -> s22 [label="length_req:1.0"]; s21 -> s23 [label="length_rsp:1.0"]; -s21 -> s20 [label="feature_req:1.0"]; -s21 -> s42 [label="feature_rsp:1.0"]; -s21 -> s72 [label="version_req:1.0"]; -s21 -> s21 [label="mtu_req:1.0"]; -s21 -> s81 [label="pairing_req:1.0"]; +s21 -> s21 [label="feature_req:1.0"]; +s21 -> s41 [label="feature_rsp:1.0"]; +s21 -> s73 [label="version_req:1.0"]; +s21 -> s20 [label="mtu_req:1.0"]; +s21 -> s80 [label="pairing_req:1.0"]; s22 -> s22 [label="length_req:1.0"]; s22 -> s23 [label="length_rsp:1.0"]; -s22 -> s20 [label="feature_req:1.0"]; -s22 -> s42 [label="feature_rsp:1.0"]; -s22 -> s72 [label="version_req:1.0"]; -s22 -> s21 [label="mtu_req:1.0"]; -s22 -> s81 [label="pairing_req:1.0"]; +s22 -> s21 [label="feature_req:1.0"]; +s22 -> s41 [label="feature_rsp:1.0"]; +s22 -> s73 [label="version_req:1.0"]; +s22 -> s20 [label="mtu_req:1.0"]; +s22 -> s80 [label="pairing_req:1.0"]; s23 -> s22 [label="length_req:1.0"]; s23 -> s23 [label="length_rsp:1.0"]; -s23 -> s20 [label="feature_req:1.0"]; -s23 -> s42 [label="feature_rsp:1.0"]; -s23 -> s72 [label="version_req:1.0"]; -s23 -> s21 [label="mtu_req:1.0"]; -s23 -> s81 [label="pairing_req:1.0"]; -s30 -> s31 [label="length_req:1.0"]; -s30 -> s34 [label="length_rsp:1.0"]; -s30 -> s33 [label="feature_req:1.0"]; -s30 -> s66 [label="feature_rsp:1.0"]; +s23 -> s21 [label="feature_req:1.0"]; +s23 -> s41 [label="feature_rsp:1.0"]; +s23 -> s73 [label="version_req:1.0"]; +s23 -> s20 [label="mtu_req:1.0"]; +s23 -> s80 [label="pairing_req:1.0"]; +s30 -> s32 [label="length_req:1.0"]; +s30 -> s31 [label="length_rsp:1.0"]; +s30 -> s34 [label="feature_req:1.0"]; +s30 -> s63 [label="feature_rsp:1.0"]; s30 -> s30 [label="version_req:1.0"]; s30 -> s70 [label="mtu_req:1.0"]; s30 -> s90 [label="pairing_req:1.0"]; -s31 -> s31 [label="length_req:1.0"]; -s31 -> s34 [label="length_rsp:1.0"]; -s31 -> s33 [label="feature_req:1.0"]; -s31 -> s66 [label="feature_rsp:1.0"]; +s31 -> s32 [label="length_req:1.0"]; +s31 -> s31 [label="length_rsp:1.0"]; +s31 -> s34 [label="feature_req:1.0"]; +s31 -> s63 [label="feature_rsp:1.0"]; s31 -> s30 [label="version_req:1.0"]; s31 -> s70 [label="mtu_req:1.0"]; s31 -> s90 [label="pairing_req:1.0"]; -s32 -> s31 [label="length_req:1.0"]; -s32 -> s34 [label="length_rsp:1.0"]; -s32 -> s33 [label="feature_req:1.0"]; -s32 -> s66 [label="feature_rsp:1.0"]; +s32 -> s32 [label="length_req:1.0"]; +s32 -> s31 [label="length_rsp:1.0"]; +s32 -> s34 [label="feature_req:1.0"]; +s32 -> s63 [label="feature_rsp:1.0"]; s32 -> s30 [label="version_req:1.0"]; s32 -> s70 [label="mtu_req:1.0"]; s32 -> s90 [label="pairing_req:1.0"]; -s33 -> s31 [label="length_req:1.0"]; -s33 -> s34 [label="length_rsp:1.0"]; -s33 -> s33 [label="feature_req:1.0"]; -s33 -> s66 [label="feature_rsp:1.0"]; +s33 -> s32 [label="length_req:1.0"]; +s33 -> s31 [label="length_rsp:1.0"]; +s33 -> s34 [label="feature_req:1.0"]; +s33 -> s63 [label="feature_rsp:1.0"]; s33 -> s30 [label="version_req:1.0"]; s33 -> s70 [label="mtu_req:1.0"]; s33 -> s90 [label="pairing_req:1.0"]; -s34 -> s31 [label="length_req:1.0"]; -s34 -> s34 [label="length_rsp:1.0"]; -s34 -> s33 [label="feature_req:1.0"]; -s34 -> s66 [label="feature_rsp:1.0"]; +s34 -> s32 [label="length_req:1.0"]; +s34 -> s31 [label="length_rsp:1.0"]; +s34 -> s34 [label="feature_req:1.0"]; +s34 -> s63 [label="feature_rsp:1.0"]; s34 -> s30 [label="version_req:1.0"]; s34 -> s70 [label="mtu_req:1.0"]; s34 -> s90 [label="pairing_req:1.0"]; -s40 -> s41 [label="length_req:1.0"]; +s40 -> s42 [label="length_req:1.0"]; s40 -> s50 [label="length_rsp:1.0"]; -s40 -> s43 [label="feature_req:1.0"]; +s40 -> s45 [label="feature_req:1.0"]; s40 -> s40 [label="feature_rsp:1.0"]; -s40 -> s62 [label="version_req:1.0"]; +s40 -> s65 [label="version_req:1.0"]; s40 -> s44 [label="mtu_req:1.0"]; -s40 -> s106 [label="pairing_req:1.0"]; -s41 -> s41 [label="length_req:1.0"]; +s40 -> s101 [label="pairing_req:1.0"]; +s41 -> s42 [label="length_req:1.0"]; s41 -> s50 [label="length_rsp:1.0"]; -s41 -> s43 [label="feature_req:1.0"]; +s41 -> s45 [label="feature_req:1.0"]; s41 -> s40 [label="feature_rsp:1.0"]; -s41 -> s62 [label="version_req:1.0"]; +s41 -> s65 [label="version_req:1.0"]; s41 -> s44 [label="mtu_req:1.0"]; -s41 -> s106 [label="pairing_req:1.0"]; -s42 -> s41 [label="length_req:1.0"]; +s41 -> s101 [label="pairing_req:1.0"]; +s42 -> s42 [label="length_req:1.0"]; s42 -> s50 [label="length_rsp:1.0"]; -s42 -> s43 [label="feature_req:1.0"]; +s42 -> s45 [label="feature_req:1.0"]; s42 -> s40 [label="feature_rsp:1.0"]; -s42 -> s62 [label="version_req:1.0"]; +s42 -> s65 [label="version_req:1.0"]; s42 -> s44 [label="mtu_req:1.0"]; -s42 -> s106 [label="pairing_req:1.0"]; -s43 -> s41 [label="length_req:1.0"]; +s42 -> s101 [label="pairing_req:1.0"]; +s43 -> s42 [label="length_req:1.0"]; s43 -> s50 [label="length_rsp:1.0"]; -s43 -> s43 [label="feature_req:1.0"]; +s43 -> s45 [label="feature_req:1.0"]; s43 -> s40 [label="feature_rsp:1.0"]; -s43 -> s62 [label="version_req:1.0"]; +s43 -> s65 [label="version_req:1.0"]; s43 -> s44 [label="mtu_req:1.0"]; -s43 -> s106 [label="pairing_req:1.0"]; -s44 -> s41 [label="length_req:1.0"]; +s43 -> s101 [label="pairing_req:1.0"]; +s44 -> s42 [label="length_req:1.0"]; s44 -> s50 [label="length_rsp:1.0"]; -s44 -> s43 [label="feature_req:1.0"]; +s44 -> s45 [label="feature_req:1.0"]; s44 -> s40 [label="feature_rsp:1.0"]; -s44 -> s62 [label="version_req:1.0"]; +s44 -> s65 [label="version_req:1.0"]; s44 -> s44 [label="mtu_req:1.0"]; -s44 -> s106 [label="pairing_req:1.0"]; -s45 -> s41 [label="length_req:1.0"]; +s44 -> s101 [label="pairing_req:1.0"]; +s45 -> s42 [label="length_req:1.0"]; s45 -> s50 [label="length_rsp:1.0"]; -s45 -> s43 [label="feature_req:1.0"]; +s45 -> s45 [label="feature_req:1.0"]; s45 -> s40 [label="feature_rsp:1.0"]; -s45 -> s62 [label="version_req:1.0"]; +s45 -> s65 [label="version_req:1.0"]; s45 -> s44 [label="mtu_req:1.0"]; -s45 -> s106 [label="pairing_req:1.0"]; -s50 -> s03 [label="length_req:0.1"]; -s50 -> s51 [label="length_req:0.9"]; -s50 -> s03 [label="length_rsp:0.1"]; -s50 -> s54 [label="length_rsp:0.9"]; -s50 -> s52 [label="feature_req:1.0"]; -s50 -> s03 [label="feature_rsp:0.1"]; +s45 -> s101 [label="pairing_req:1.0"]; +s50 -> s01 [label="length_req:0.1"]; +s50 -> s52 [label="length_req:0.9"]; +s50 -> s01 [label="length_rsp:0.1"]; +s50 -> s51 [label="length_rsp:0.9"]; +s50 -> s54 [label="feature_req:1.0"]; +s50 -> s01 [label="feature_rsp:0.1"]; s50 -> s50 [label="feature_rsp:0.9"]; -s50 -> s142 [label="version_req:1.0"]; +s50 -> s144 [label="version_req:1.0"]; s50 -> s53 [label="mtu_req:1.0"]; -s50 -> s135 [label="pairing_req:1.0"]; -s51 -> s03 [label="length_req:0.1"]; -s51 -> s51 [label="length_req:0.9"]; -s51 -> s03 [label="length_rsp:0.1"]; -s51 -> s54 [label="length_rsp:0.9"]; -s51 -> s52 [label="feature_req:1.0"]; -s51 -> s03 [label="feature_rsp:0.1"]; +s50 -> s132 [label="pairing_req:1.0"]; +s51 -> s01 [label="length_req:0.1"]; +s51 -> s52 [label="length_req:0.9"]; +s51 -> s01 [label="length_rsp:0.1"]; +s51 -> s51 [label="length_rsp:0.9"]; +s51 -> s54 [label="feature_req:1.0"]; +s51 -> s01 [label="feature_rsp:0.1"]; s51 -> s50 [label="feature_rsp:0.9"]; -s51 -> s142 [label="version_req:1.0"]; +s51 -> s144 [label="version_req:1.0"]; s51 -> s53 [label="mtu_req:1.0"]; -s51 -> s135 [label="pairing_req:1.0"]; -s52 -> s03 [label="length_req:0.1"]; -s52 -> s51 [label="length_req:0.9"]; -s52 -> s03 [label="length_rsp:0.1"]; -s52 -> s54 [label="length_rsp:0.9"]; -s52 -> s52 [label="feature_req:1.0"]; -s52 -> s03 [label="feature_rsp:0.1"]; +s51 -> s132 [label="pairing_req:1.0"]; +s52 -> s01 [label="length_req:0.1"]; +s52 -> s52 [label="length_req:0.9"]; +s52 -> s01 [label="length_rsp:0.1"]; +s52 -> s51 [label="length_rsp:0.9"]; +s52 -> s54 [label="feature_req:1.0"]; +s52 -> s01 [label="feature_rsp:0.1"]; s52 -> s50 [label="feature_rsp:0.9"]; -s52 -> s142 [label="version_req:1.0"]; +s52 -> s144 [label="version_req:1.0"]; s52 -> s53 [label="mtu_req:1.0"]; -s52 -> s135 [label="pairing_req:1.0"]; -s53 -> s03 [label="length_req:0.1"]; -s53 -> s51 [label="length_req:0.9"]; -s53 -> s03 [label="length_rsp:0.1"]; -s53 -> s54 [label="length_rsp:0.9"]; -s53 -> s52 [label="feature_req:1.0"]; -s53 -> s03 [label="feature_rsp:0.1"]; +s52 -> s132 [label="pairing_req:1.0"]; +s53 -> s01 [label="length_req:0.1"]; +s53 -> s52 [label="length_req:0.9"]; +s53 -> s01 [label="length_rsp:0.1"]; +s53 -> s51 [label="length_rsp:0.9"]; +s53 -> s54 [label="feature_req:1.0"]; +s53 -> s01 [label="feature_rsp:0.1"]; s53 -> s50 [label="feature_rsp:0.9"]; -s53 -> s142 [label="version_req:1.0"]; +s53 -> s144 [label="version_req:1.0"]; s53 -> s53 [label="mtu_req:1.0"]; -s53 -> s135 [label="pairing_req:1.0"]; -s54 -> s03 [label="length_req:0.1"]; -s54 -> s51 [label="length_req:0.9"]; -s54 -> s03 [label="length_rsp:0.1"]; -s54 -> s54 [label="length_rsp:0.9"]; -s54 -> s52 [label="feature_req:1.0"]; -s54 -> s03 [label="feature_rsp:0.1"]; +s53 -> s132 [label="pairing_req:1.0"]; +s54 -> s01 [label="length_req:0.1"]; +s54 -> s52 [label="length_req:0.9"]; +s54 -> s01 [label="length_rsp:0.1"]; +s54 -> s51 [label="length_rsp:0.9"]; +s54 -> s54 [label="feature_req:1.0"]; +s54 -> s01 [label="feature_rsp:0.1"]; s54 -> s50 [label="feature_rsp:0.9"]; -s54 -> s142 [label="version_req:1.0"]; +s54 -> s144 [label="version_req:1.0"]; s54 -> s53 [label="mtu_req:1.0"]; -s54 -> s135 [label="pairing_req:1.0"]; -s60 -> s66 [label="length_req:0.2"]; -s60 -> s61 [label="length_req:0.8"]; -s60 -> s61 [label="length_req:1.0"]; -s60 -> s66 [label="length_rsp:0.2"]; +s54 -> s132 [label="pairing_req:1.0"]; +s60 -> s63 [label="length_req:0.2"]; +s60 -> s62 [label="length_req:0.8"]; +s60 -> s63 [label="length_rsp:0.2"]; s60 -> s140 [label="length_rsp:0.8"]; -s60 -> s140 [label="length_rsp:1.0"]; -s60 -> s66 [label="feature_req:0.2"]; -s60 -> s64 [label="feature_req:0.8"]; -s60 -> s64 [label="feature_req:1.0"]; -s60 -> s66 [label="feature_rsp:0.2"]; +s60 -> s63 [label="feature_req:0.2"]; +s60 -> s66 [label="feature_req:0.8"]; +s60 -> s63 [label="feature_rsp:0.2"]; s60 -> s60 [label="feature_rsp:0.8"]; -s60 -> s60 [label="feature_rsp:1.0"]; -s60 -> s66 [label="version_req:0.2"]; +s60 -> s63 [label="version_req:0.2"]; s60 -> s60 [label="version_req:0.8"]; -s60 -> s60 [label="version_req:1.0"]; -s60 -> s66 [label="mtu_req:0.2"]; -s60 -> s65 [label="mtu_req:0.8"]; -s60 -> s65 [label="mtu_req:1.0"]; -s60 -> s66 [label="pairing_req:0.2"]; -s60 -> s127 [label="pairing_req:0.8"]; -s60 -> s127 [label="pairing_req:1.0"]; -s61 -> s66 [label="length_req:0.2"]; -s61 -> s61 [label="length_req:0.8"]; -s61 -> s61 [label="length_req:1.0"]; -s61 -> s66 [label="length_rsp:0.2"]; +s60 -> s63 [label="mtu_req:0.2"]; +s60 -> s64 [label="mtu_req:0.8"]; +s60 -> s63 [label="pairing_req:0.2"]; +s60 -> s121 [label="pairing_req:0.8"]; +s61 -> s63 [label="length_req:0.2"]; +s61 -> s62 [label="length_req:0.8"]; +s61 -> s63 [label="length_rsp:0.2"]; s61 -> s140 [label="length_rsp:0.8"]; -s61 -> s140 [label="length_rsp:1.0"]; -s61 -> s66 [label="feature_req:0.2"]; -s61 -> s64 [label="feature_req:0.8"]; -s61 -> s64 [label="feature_req:1.0"]; -s61 -> s66 [label="feature_rsp:0.2"]; +s61 -> s63 [label="feature_req:0.2"]; +s61 -> s66 [label="feature_req:0.8"]; +s61 -> s63 [label="feature_rsp:0.2"]; s61 -> s60 [label="feature_rsp:0.8"]; -s61 -> s60 [label="feature_rsp:1.0"]; -s61 -> s66 [label="version_req:0.2"]; +s61 -> s63 [label="version_req:0.2"]; s61 -> s60 [label="version_req:0.8"]; -s61 -> s60 [label="version_req:1.0"]; -s61 -> s66 [label="mtu_req:0.2"]; -s61 -> s65 [label="mtu_req:0.8"]; -s61 -> s65 [label="mtu_req:1.0"]; -s61 -> s66 [label="pairing_req:0.2"]; -s61 -> s127 [label="pairing_req:0.8"]; -s61 -> s127 [label="pairing_req:1.0"]; -s62 -> s66 [label="length_req:0.2"]; -s62 -> s61 [label="length_req:0.8"]; -s62 -> s61 [label="length_req:1.0"]; -s62 -> s66 [label="length_rsp:0.2"]; +s61 -> s63 [label="mtu_req:0.2"]; +s61 -> s64 [label="mtu_req:0.8"]; +s61 -> s63 [label="pairing_req:0.2"]; +s61 -> s121 [label="pairing_req:0.8"]; +s62 -> s63 [label="length_req:0.2"]; +s62 -> s62 [label="length_req:0.8"]; +s62 -> s63 [label="length_rsp:0.2"]; s62 -> s140 [label="length_rsp:0.8"]; -s62 -> s140 [label="length_rsp:1.0"]; -s62 -> s66 [label="feature_req:0.2"]; -s62 -> s64 [label="feature_req:0.8"]; -s62 -> s64 [label="feature_req:1.0"]; -s62 -> s66 [label="feature_rsp:0.2"]; +s62 -> s63 [label="feature_req:0.2"]; +s62 -> s66 [label="feature_req:0.8"]; +s62 -> s63 [label="feature_rsp:0.2"]; s62 -> s60 [label="feature_rsp:0.8"]; -s62 -> s60 [label="feature_rsp:1.0"]; -s62 -> s66 [label="version_req:0.2"]; +s62 -> s63 [label="version_req:0.2"]; s62 -> s60 [label="version_req:0.8"]; -s62 -> s60 [label="version_req:1.0"]; -s62 -> s66 [label="mtu_req:0.2"]; -s62 -> s65 [label="mtu_req:0.8"]; -s62 -> s65 [label="mtu_req:1.0"]; -s62 -> s66 [label="pairing_req:0.2"]; -s62 -> s127 [label="pairing_req:0.8"]; -s62 -> s127 [label="pairing_req:1.0"]; -s63 -> s66 [label="length_req:0.2"]; -s63 -> s61 [label="length_req:0.8"]; -s63 -> s61 [label="length_req:1.0"]; -s63 -> s66 [label="length_rsp:0.2"]; +s62 -> s63 [label="mtu_req:0.2"]; +s62 -> s64 [label="mtu_req:0.8"]; +s62 -> s63 [label="pairing_req:0.2"]; +s62 -> s121 [label="pairing_req:0.8"]; +s63 -> s63 [label="length_req:0.2"]; +s63 -> s62 [label="length_req:0.8"]; +s63 -> s63 [label="length_rsp:0.2"]; s63 -> s140 [label="length_rsp:0.8"]; -s63 -> s140 [label="length_rsp:1.0"]; -s63 -> s66 [label="feature_req:0.2"]; -s63 -> s64 [label="feature_req:0.8"]; -s63 -> s64 [label="feature_req:1.0"]; -s63 -> s66 [label="feature_rsp:0.2"]; +s63 -> s63 [label="feature_req:0.2"]; +s63 -> s66 [label="feature_req:0.8"]; +s63 -> s63 [label="feature_rsp:0.2"]; s63 -> s60 [label="feature_rsp:0.8"]; -s63 -> s60 [label="feature_rsp:1.0"]; -s63 -> s66 [label="version_req:0.2"]; +s63 -> s63 [label="version_req:0.2"]; s63 -> s60 [label="version_req:0.8"]; -s63 -> s60 [label="version_req:1.0"]; -s63 -> s66 [label="mtu_req:0.2"]; -s63 -> s65 [label="mtu_req:0.8"]; -s63 -> s65 [label="mtu_req:1.0"]; -s63 -> s66 [label="pairing_req:0.2"]; -s63 -> s127 [label="pairing_req:0.8"]; -s63 -> s127 [label="pairing_req:1.0"]; -s64 -> s66 [label="length_req:0.2"]; -s64 -> s61 [label="length_req:0.8"]; -s64 -> s61 [label="length_req:1.0"]; -s64 -> s66 [label="length_rsp:0.2"]; +s63 -> s63 [label="mtu_req:0.2"]; +s63 -> s64 [label="mtu_req:0.8"]; +s63 -> s63 [label="pairing_req:0.2"]; +s63 -> s121 [label="pairing_req:0.8"]; +s64 -> s63 [label="length_req:0.2"]; +s64 -> s62 [label="length_req:0.8"]; +s64 -> s63 [label="length_rsp:0.2"]; s64 -> s140 [label="length_rsp:0.8"]; -s64 -> s140 [label="length_rsp:1.0"]; -s64 -> s66 [label="feature_req:0.2"]; -s64 -> s64 [label="feature_req:0.8"]; -s64 -> s64 [label="feature_req:1.0"]; -s64 -> s66 [label="feature_rsp:0.2"]; +s64 -> s63 [label="feature_req:0.2"]; +s64 -> s66 [label="feature_req:0.8"]; +s64 -> s63 [label="feature_rsp:0.2"]; s64 -> s60 [label="feature_rsp:0.8"]; -s64 -> s60 [label="feature_rsp:1.0"]; -s64 -> s66 [label="version_req:0.2"]; +s64 -> s63 [label="version_req:0.2"]; s64 -> s60 [label="version_req:0.8"]; -s64 -> s60 [label="version_req:1.0"]; -s64 -> s66 [label="mtu_req:0.2"]; -s64 -> s65 [label="mtu_req:0.8"]; -s64 -> s65 [label="mtu_req:1.0"]; -s64 -> s66 [label="pairing_req:0.2"]; -s64 -> s127 [label="pairing_req:0.8"]; -s64 -> s127 [label="pairing_req:1.0"]; -s65 -> s66 [label="length_req:0.2"]; -s65 -> s61 [label="length_req:0.8"]; -s65 -> s61 [label="length_req:1.0"]; -s65 -> s66 [label="length_rsp:0.2"]; +s64 -> s63 [label="mtu_req:0.2"]; +s64 -> s64 [label="mtu_req:0.8"]; +s64 -> s63 [label="pairing_req:0.2"]; +s64 -> s121 [label="pairing_req:0.8"]; +s65 -> s63 [label="length_req:0.2"]; +s65 -> s62 [label="length_req:0.8"]; +s65 -> s63 [label="length_rsp:0.2"]; s65 -> s140 [label="length_rsp:0.8"]; -s65 -> s140 [label="length_rsp:1.0"]; -s65 -> s66 [label="feature_req:0.2"]; -s65 -> s64 [label="feature_req:0.8"]; -s65 -> s64 [label="feature_req:1.0"]; -s65 -> s66 [label="feature_rsp:0.2"]; +s65 -> s63 [label="feature_req:0.2"]; +s65 -> s66 [label="feature_req:0.8"]; +s65 -> s63 [label="feature_rsp:0.2"]; s65 -> s60 [label="feature_rsp:0.8"]; -s65 -> s60 [label="feature_rsp:1.0"]; -s65 -> s66 [label="version_req:0.2"]; +s65 -> s63 [label="version_req:0.2"]; s65 -> s60 [label="version_req:0.8"]; -s65 -> s60 [label="version_req:1.0"]; -s65 -> s66 [label="mtu_req:0.2"]; -s65 -> s65 [label="mtu_req:0.8"]; -s65 -> s65 [label="mtu_req:1.0"]; -s65 -> s66 [label="pairing_req:0.2"]; -s65 -> s127 [label="pairing_req:0.8"]; -s65 -> s127 [label="pairing_req:1.0"]; -s66 -> s66 [label="length_req:0.2"]; -s66 -> s61 [label="length_req:0.8"]; -s66 -> s61 [label="length_req:1.0"]; -s66 -> s66 [label="length_rsp:0.2"]; +s65 -> s63 [label="mtu_req:0.2"]; +s65 -> s64 [label="mtu_req:0.8"]; +s65 -> s63 [label="pairing_req:0.2"]; +s65 -> s121 [label="pairing_req:0.8"]; +s66 -> s63 [label="length_req:0.2"]; +s66 -> s62 [label="length_req:0.8"]; +s66 -> s63 [label="length_rsp:0.2"]; s66 -> s140 [label="length_rsp:0.8"]; -s66 -> s140 [label="length_rsp:1.0"]; -s66 -> s66 [label="feature_req:0.2"]; -s66 -> s64 [label="feature_req:0.8"]; -s66 -> s64 [label="feature_req:1.0"]; -s66 -> s66 [label="feature_rsp:0.2"]; +s66 -> s63 [label="feature_req:0.2"]; +s66 -> s66 [label="feature_req:0.8"]; +s66 -> s63 [label="feature_rsp:0.2"]; s66 -> s60 [label="feature_rsp:0.8"]; -s66 -> s60 [label="feature_rsp:1.0"]; -s66 -> s66 [label="version_req:0.2"]; +s66 -> s63 [label="version_req:0.2"]; s66 -> s60 [label="version_req:0.8"]; -s66 -> s60 [label="version_req:1.0"]; -s66 -> s66 [label="mtu_req:0.2"]; -s66 -> s65 [label="mtu_req:0.8"]; -s66 -> s65 [label="mtu_req:1.0"]; -s66 -> s66 [label="pairing_req:0.2"]; -s66 -> s127 [label="pairing_req:0.8"]; -s66 -> s127 [label="pairing_req:1.0"]; -s70 -> s71 [label="length_req:1.0"]; -s70 -> s74 [label="length_rsp:1.0"]; -s70 -> s73 [label="feature_req:1.0"]; -s70 -> s63 [label="feature_rsp:1.0"]; +s66 -> s63 [label="mtu_req:0.2"]; +s66 -> s64 [label="mtu_req:0.8"]; +s66 -> s63 [label="pairing_req:0.2"]; +s66 -> s121 [label="pairing_req:0.8"]; +s70 -> s72 [label="length_req:1.0"]; +s70 -> s71 [label="length_rsp:1.0"]; +s70 -> s74 [label="feature_req:1.0"]; +s70 -> s61 [label="feature_rsp:1.0"]; s70 -> s70 [label="version_req:1.0"]; s70 -> s70 [label="mtu_req:1.0"]; s70 -> s110 [label="pairing_req:1.0"]; -s71 -> s71 [label="length_req:1.0"]; -s71 -> s74 [label="length_rsp:1.0"]; -s71 -> s73 [label="feature_req:1.0"]; -s71 -> s63 [label="feature_rsp:1.0"]; +s71 -> s72 [label="length_req:1.0"]; +s71 -> s71 [label="length_rsp:1.0"]; +s71 -> s74 [label="feature_req:1.0"]; +s71 -> s61 [label="feature_rsp:1.0"]; s71 -> s70 [label="version_req:1.0"]; s71 -> s70 [label="mtu_req:1.0"]; s71 -> s110 [label="pairing_req:1.0"]; -s72 -> s71 [label="length_req:1.0"]; -s72 -> s74 [label="length_rsp:1.0"]; -s72 -> s73 [label="feature_req:1.0"]; -s72 -> s63 [label="feature_rsp:1.0"]; +s72 -> s72 [label="length_req:1.0"]; +s72 -> s71 [label="length_rsp:1.0"]; +s72 -> s74 [label="feature_req:1.0"]; +s72 -> s61 [label="feature_rsp:1.0"]; s72 -> s70 [label="version_req:1.0"]; s72 -> s70 [label="mtu_req:1.0"]; s72 -> s110 [label="pairing_req:1.0"]; -s73 -> s71 [label="length_req:1.0"]; -s73 -> s74 [label="length_rsp:1.0"]; -s73 -> s73 [label="feature_req:1.0"]; -s73 -> s63 [label="feature_rsp:1.0"]; +s73 -> s72 [label="length_req:1.0"]; +s73 -> s71 [label="length_rsp:1.0"]; +s73 -> s74 [label="feature_req:1.0"]; +s73 -> s61 [label="feature_rsp:1.0"]; s73 -> s70 [label="version_req:1.0"]; s73 -> s70 [label="mtu_req:1.0"]; s73 -> s110 [label="pairing_req:1.0"]; -s74 -> s71 [label="length_req:1.0"]; -s74 -> s74 [label="length_rsp:1.0"]; -s74 -> s73 [label="feature_req:1.0"]; -s74 -> s63 [label="feature_rsp:1.0"]; +s74 -> s72 [label="length_req:1.0"]; +s74 -> s71 [label="length_rsp:1.0"]; +s74 -> s74 [label="feature_req:1.0"]; +s74 -> s61 [label="feature_rsp:1.0"]; s74 -> s70 [label="version_req:1.0"]; s74 -> s70 [label="mtu_req:1.0"]; s74 -> s110 [label="pairing_req:1.0"]; s80 -> s82 [label="length_req:1.0"]; s80 -> s23 [label="length_rsp:1.0"]; -s80 -> s80 [label="feature_req:1.0"]; -s80 -> s105 [label="feature_rsp:1.0"]; -s80 -> s112 [label="version_req:1.0"]; -s80 -> s81 [label="mtu_req:1.0"]; -s80 -> s81 [label="pairing_req:1.0"]; +s80 -> s81 [label="feature_req:1.0"]; +s80 -> s106 [label="feature_rsp:1.0"]; +s80 -> s113 [label="version_req:1.0"]; +s80 -> s80 [label="mtu_req:1.0"]; +s80 -> s80 [label="pairing_req:1.0"]; s81 -> s82 [label="length_req:1.0"]; s81 -> s23 [label="length_rsp:1.0"]; -s81 -> s80 [label="feature_req:1.0"]; -s81 -> s105 [label="feature_rsp:1.0"]; -s81 -> s112 [label="version_req:1.0"]; -s81 -> s81 [label="mtu_req:1.0"]; -s81 -> s81 [label="pairing_req:1.0"]; +s81 -> s81 [label="feature_req:1.0"]; +s81 -> s106 [label="feature_rsp:1.0"]; +s81 -> s113 [label="version_req:1.0"]; +s81 -> s80 [label="mtu_req:1.0"]; +s81 -> s80 [label="pairing_req:1.0"]; s82 -> s82 [label="length_req:1.0"]; s82 -> s23 [label="length_rsp:1.0"]; -s82 -> s80 [label="feature_req:1.0"]; -s82 -> s105 [label="feature_rsp:1.0"]; -s82 -> s112 [label="version_req:1.0"]; -s82 -> s81 [label="mtu_req:1.0"]; -s82 -> s81 [label="pairing_req:1.0"]; -s90 -> s91 [label="length_req:1.0"]; -s90 -> s94 [label="length_rsp:1.0"]; -s90 -> s93 [label="feature_req:1.0"]; -s90 -> s123 [label="feature_rsp:1.0"]; +s82 -> s81 [label="feature_req:1.0"]; +s82 -> s106 [label="feature_rsp:1.0"]; +s82 -> s113 [label="version_req:1.0"]; +s82 -> s80 [label="mtu_req:1.0"]; +s82 -> s80 [label="pairing_req:1.0"]; +s90 -> s92 [label="length_req:1.0"]; +s90 -> s91 [label="length_rsp:1.0"]; +s90 -> s94 [label="feature_req:1.0"]; +s90 -> s124 [label="feature_rsp:1.0"]; s90 -> s90 [label="version_req:1.0"]; s90 -> s110 [label="mtu_req:1.0"]; s90 -> s90 [label="pairing_req:1.0"]; -s91 -> s91 [label="length_req:1.0"]; -s91 -> s94 [label="length_rsp:1.0"]; -s91 -> s93 [label="feature_req:1.0"]; -s91 -> s123 [label="feature_rsp:1.0"]; +s91 -> s92 [label="length_req:1.0"]; +s91 -> s91 [label="length_rsp:1.0"]; +s91 -> s94 [label="feature_req:1.0"]; +s91 -> s124 [label="feature_rsp:1.0"]; s91 -> s90 [label="version_req:1.0"]; s91 -> s110 [label="mtu_req:1.0"]; s91 -> s90 [label="pairing_req:1.0"]; -s92 -> s91 [label="length_req:1.0"]; -s92 -> s94 [label="length_rsp:1.0"]; -s92 -> s93 [label="feature_req:1.0"]; -s92 -> s123 [label="feature_rsp:1.0"]; +s92 -> s92 [label="length_req:1.0"]; +s92 -> s91 [label="length_rsp:1.0"]; +s92 -> s94 [label="feature_req:1.0"]; +s92 -> s124 [label="feature_rsp:1.0"]; s92 -> s90 [label="version_req:1.0"]; s92 -> s110 [label="mtu_req:1.0"]; s92 -> s90 [label="pairing_req:1.0"]; -s93 -> s91 [label="length_req:1.0"]; -s93 -> s94 [label="length_rsp:1.0"]; -s93 -> s93 [label="feature_req:1.0"]; -s93 -> s123 [label="feature_rsp:1.0"]; +s93 -> s92 [label="length_req:1.0"]; +s93 -> s91 [label="length_rsp:1.0"]; +s93 -> s94 [label="feature_req:1.0"]; +s93 -> s124 [label="feature_rsp:1.0"]; s93 -> s90 [label="version_req:1.0"]; s93 -> s110 [label="mtu_req:1.0"]; s93 -> s90 [label="pairing_req:1.0"]; -s94 -> s91 [label="length_req:1.0"]; -s94 -> s94 [label="length_rsp:1.0"]; -s94 -> s93 [label="feature_req:1.0"]; -s94 -> s123 [label="feature_rsp:1.0"]; +s94 -> s92 [label="length_req:1.0"]; +s94 -> s91 [label="length_rsp:1.0"]; +s94 -> s94 [label="feature_req:1.0"]; +s94 -> s124 [label="feature_rsp:1.0"]; s94 -> s90 [label="version_req:1.0"]; s94 -> s110 [label="mtu_req:1.0"]; s94 -> s90 [label="pairing_req:1.0"]; -s100 -> s03 [label="length_req:0.1"]; -s100 -> s101 [label="length_req:0.9"]; -s100 -> s03 [label="length_rsp:0.1"]; +s100 -> s01 [label="length_req:0.1"]; +s100 -> s102 [label="length_req:0.9"]; +s100 -> s01 [label="length_rsp:0.1"]; s100 -> s130 [label="length_rsp:0.9"]; s100 -> s103 [label="feature_req:1.0"]; -s100 -> s03 [label="feature_rsp:0.1"]; +s100 -> s01 [label="feature_rsp:0.1"]; s100 -> s100 [label="feature_rsp:0.9"]; -s100 -> s122 [label="version_req:1.0"]; -s100 -> s104 [label="mtu_req:1.0"]; +s100 -> s126 [label="version_req:1.0"]; +s100 -> s105 [label="mtu_req:1.0"]; s100 -> s100 [label="pairing_req:1.0"]; -s101 -> s03 [label="length_req:0.1"]; -s101 -> s101 [label="length_req:0.9"]; -s101 -> s03 [label="length_rsp:0.1"]; +s101 -> s01 [label="length_req:0.1"]; +s101 -> s102 [label="length_req:0.9"]; +s101 -> s01 [label="length_rsp:0.1"]; s101 -> s130 [label="length_rsp:0.9"]; s101 -> s103 [label="feature_req:1.0"]; -s101 -> s03 [label="feature_rsp:0.1"]; +s101 -> s01 [label="feature_rsp:0.1"]; s101 -> s100 [label="feature_rsp:0.9"]; -s101 -> s122 [label="version_req:1.0"]; -s101 -> s104 [label="mtu_req:1.0"]; +s101 -> s126 [label="version_req:1.0"]; +s101 -> s105 [label="mtu_req:1.0"]; s101 -> s100 [label="pairing_req:1.0"]; -s102 -> s03 [label="length_req:0.1"]; -s102 -> s101 [label="length_req:0.9"]; -s102 -> s03 [label="length_rsp:0.1"]; +s102 -> s01 [label="length_req:0.1"]; +s102 -> s102 [label="length_req:0.9"]; +s102 -> s01 [label="length_rsp:0.1"]; s102 -> s130 [label="length_rsp:0.9"]; s102 -> s103 [label="feature_req:1.0"]; -s102 -> s03 [label="feature_rsp:0.1"]; +s102 -> s01 [label="feature_rsp:0.1"]; s102 -> s100 [label="feature_rsp:0.9"]; -s102 -> s122 [label="version_req:1.0"]; -s102 -> s104 [label="mtu_req:1.0"]; +s102 -> s126 [label="version_req:1.0"]; +s102 -> s105 [label="mtu_req:1.0"]; s102 -> s100 [label="pairing_req:1.0"]; -s103 -> s03 [label="length_req:0.1"]; -s103 -> s101 [label="length_req:0.9"]; -s103 -> s03 [label="length_rsp:0.1"]; +s103 -> s01 [label="length_req:0.1"]; +s103 -> s102 [label="length_req:0.9"]; +s103 -> s01 [label="length_rsp:0.1"]; s103 -> s130 [label="length_rsp:0.9"]; s103 -> s103 [label="feature_req:1.0"]; -s103 -> s03 [label="feature_rsp:0.1"]; +s103 -> s01 [label="feature_rsp:0.1"]; s103 -> s100 [label="feature_rsp:0.9"]; -s103 -> s122 [label="version_req:1.0"]; -s103 -> s104 [label="mtu_req:1.0"]; +s103 -> s126 [label="version_req:1.0"]; +s103 -> s105 [label="mtu_req:1.0"]; s103 -> s100 [label="pairing_req:1.0"]; -s104 -> s03 [label="length_req:0.1"]; -s104 -> s101 [label="length_req:0.9"]; -s104 -> s03 [label="length_rsp:0.1"]; +s104 -> s01 [label="length_req:0.1"]; +s104 -> s102 [label="length_req:0.9"]; +s104 -> s01 [label="length_rsp:0.1"]; s104 -> s130 [label="length_rsp:0.9"]; s104 -> s103 [label="feature_req:1.0"]; -s104 -> s03 [label="feature_rsp:0.1"]; +s104 -> s01 [label="feature_rsp:0.1"]; s104 -> s100 [label="feature_rsp:0.9"]; -s104 -> s122 [label="version_req:1.0"]; -s104 -> s104 [label="mtu_req:1.0"]; +s104 -> s126 [label="version_req:1.0"]; +s104 -> s105 [label="mtu_req:1.0"]; s104 -> s100 [label="pairing_req:1.0"]; -s105 -> s03 [label="length_req:0.1"]; -s105 -> s101 [label="length_req:0.9"]; -s105 -> s03 [label="length_rsp:0.1"]; +s105 -> s01 [label="length_req:0.1"]; +s105 -> s102 [label="length_req:0.9"]; +s105 -> s01 [label="length_rsp:0.1"]; s105 -> s130 [label="length_rsp:0.9"]; s105 -> s103 [label="feature_req:1.0"]; -s105 -> s03 [label="feature_rsp:0.1"]; +s105 -> s01 [label="feature_rsp:0.1"]; s105 -> s100 [label="feature_rsp:0.9"]; -s105 -> s122 [label="version_req:1.0"]; -s105 -> s104 [label="mtu_req:1.0"]; +s105 -> s126 [label="version_req:1.0"]; +s105 -> s105 [label="mtu_req:1.0"]; s105 -> s100 [label="pairing_req:1.0"]; -s106 -> s03 [label="length_req:0.1"]; -s106 -> s101 [label="length_req:0.9"]; -s106 -> s03 [label="length_rsp:0.1"]; +s106 -> s01 [label="length_req:0.1"]; +s106 -> s102 [label="length_req:0.9"]; +s106 -> s01 [label="length_rsp:0.1"]; s106 -> s130 [label="length_rsp:0.9"]; s106 -> s103 [label="feature_req:1.0"]; -s106 -> s03 [label="feature_rsp:0.1"]; +s106 -> s01 [label="feature_rsp:0.1"]; s106 -> s100 [label="feature_rsp:0.9"]; -s106 -> s122 [label="version_req:1.0"]; -s106 -> s104 [label="mtu_req:1.0"]; +s106 -> s126 [label="version_req:1.0"]; +s106 -> s105 [label="mtu_req:1.0"]; s106 -> s100 [label="pairing_req:1.0"]; -s110 -> s111 [label="length_req:1.0"]; -s110 -> s114 [label="length_rsp:1.0"]; -s110 -> s113 [label="feature_req:1.0"]; -s110 -> s126 [label="feature_rsp:1.0"]; +s110 -> s112 [label="length_req:1.0"]; +s110 -> s111 [label="length_rsp:1.0"]; +s110 -> s114 [label="feature_req:1.0"]; +s110 -> s127 [label="feature_rsp:1.0"]; s110 -> s110 [label="version_req:1.0"]; s110 -> s110 [label="mtu_req:1.0"]; s110 -> s110 [label="pairing_req:1.0"]; -s111 -> s111 [label="length_req:1.0"]; -s111 -> s114 [label="length_rsp:1.0"]; -s111 -> s113 [label="feature_req:1.0"]; -s111 -> s126 [label="feature_rsp:1.0"]; +s111 -> s112 [label="length_req:1.0"]; +s111 -> s111 [label="length_rsp:1.0"]; +s111 -> s114 [label="feature_req:1.0"]; +s111 -> s127 [label="feature_rsp:1.0"]; s111 -> s110 [label="version_req:1.0"]; s111 -> s110 [label="mtu_req:1.0"]; s111 -> s110 [label="pairing_req:1.0"]; -s112 -> s111 [label="length_req:1.0"]; -s112 -> s114 [label="length_rsp:1.0"]; -s112 -> s113 [label="feature_req:1.0"]; -s112 -> s126 [label="feature_rsp:1.0"]; +s112 -> s112 [label="length_req:1.0"]; +s112 -> s111 [label="length_rsp:1.0"]; +s112 -> s114 [label="feature_req:1.0"]; +s112 -> s127 [label="feature_rsp:1.0"]; s112 -> s110 [label="version_req:1.0"]; s112 -> s110 [label="mtu_req:1.0"]; s112 -> s110 [label="pairing_req:1.0"]; -s113 -> s111 [label="length_req:1.0"]; -s113 -> s114 [label="length_rsp:1.0"]; -s113 -> s113 [label="feature_req:1.0"]; -s113 -> s126 [label="feature_rsp:1.0"]; +s113 -> s112 [label="length_req:1.0"]; +s113 -> s111 [label="length_rsp:1.0"]; +s113 -> s114 [label="feature_req:1.0"]; +s113 -> s127 [label="feature_rsp:1.0"]; s113 -> s110 [label="version_req:1.0"]; s113 -> s110 [label="mtu_req:1.0"]; s113 -> s110 [label="pairing_req:1.0"]; -s114 -> s111 [label="length_req:1.0"]; -s114 -> s114 [label="length_rsp:1.0"]; -s114 -> s113 [label="feature_req:1.0"]; -s114 -> s126 [label="feature_rsp:1.0"]; +s114 -> s112 [label="length_req:1.0"]; +s114 -> s111 [label="length_rsp:1.0"]; +s114 -> s114 [label="feature_req:1.0"]; +s114 -> s127 [label="feature_rsp:1.0"]; s114 -> s110 [label="version_req:1.0"]; s114 -> s110 [label="mtu_req:1.0"]; s114 -> s110 [label="pairing_req:1.0"]; -s120 -> s122 [label="length_req:0.2"]; -s120 -> s121 [label="length_req:0.8"]; -s120 -> s121 [label="length_req:1.0"]; -s120 -> s122 [label="length_rsp:0.2"]; +s120 -> s126 [label="length_req:0.2"]; +s120 -> s122 [label="length_req:0.8"]; +s120 -> s126 [label="length_rsp:0.2"]; s120 -> s150 [label="length_rsp:0.8"]; -s120 -> s150 [label="length_rsp:1.0"]; -s120 -> s122 [label="feature_req:0.2"]; -s120 -> s124 [label="feature_req:0.8"]; -s120 -> s124 [label="feature_req:1.0"]; -s120 -> s122 [label="feature_rsp:0.2"]; +s120 -> s126 [label="feature_req:0.2"]; +s120 -> s123 [label="feature_req:0.8"]; +s120 -> s126 [label="feature_rsp:0.2"]; s120 -> s120 [label="feature_rsp:0.8"]; -s120 -> s120 [label="feature_rsp:1.0"]; -s120 -> s122 [label="version_req:0.2"]; +s120 -> s126 [label="version_req:0.2"]; s120 -> s120 [label="version_req:0.8"]; -s120 -> s120 [label="version_req:1.0"]; -s120 -> s122 [label="mtu_req:0.2"]; +s120 -> s126 [label="mtu_req:0.2"]; s120 -> s125 [label="mtu_req:0.8"]; -s120 -> s125 [label="mtu_req:1.0"]; -s120 -> s122 [label="pairing_req:0.2"]; +s120 -> s126 [label="pairing_req:0.2"]; s120 -> s120 [label="pairing_req:0.8"]; -s120 -> s120 [label="pairing_req:1.0"]; -s121 -> s122 [label="length_req:0.2"]; -s121 -> s121 [label="length_req:0.8"]; -s121 -> s121 [label="length_req:1.0"]; -s121 -> s122 [label="length_rsp:0.2"]; +s121 -> s126 [label="length_req:0.2"]; +s121 -> s122 [label="length_req:0.8"]; +s121 -> s126 [label="length_rsp:0.2"]; s121 -> s150 [label="length_rsp:0.8"]; -s121 -> s150 [label="length_rsp:1.0"]; -s121 -> s122 [label="feature_req:0.2"]; -s121 -> s124 [label="feature_req:0.8"]; -s121 -> s124 [label="feature_req:1.0"]; -s121 -> s122 [label="feature_rsp:0.2"]; +s121 -> s126 [label="feature_req:0.2"]; +s121 -> s123 [label="feature_req:0.8"]; +s121 -> s126 [label="feature_rsp:0.2"]; s121 -> s120 [label="feature_rsp:0.8"]; -s121 -> s120 [label="feature_rsp:1.0"]; -s121 -> s122 [label="version_req:0.2"]; +s121 -> s126 [label="version_req:0.2"]; s121 -> s120 [label="version_req:0.8"]; -s121 -> s120 [label="version_req:1.0"]; -s121 -> s122 [label="mtu_req:0.2"]; +s121 -> s126 [label="mtu_req:0.2"]; s121 -> s125 [label="mtu_req:0.8"]; -s121 -> s125 [label="mtu_req:1.0"]; -s121 -> s122 [label="pairing_req:0.2"]; +s121 -> s126 [label="pairing_req:0.2"]; s121 -> s120 [label="pairing_req:0.8"]; -s121 -> s120 [label="pairing_req:1.0"]; -s122 -> s122 [label="length_req:0.2"]; -s122 -> s121 [label="length_req:0.8"]; -s122 -> s121 [label="length_req:1.0"]; -s122 -> s122 [label="length_rsp:0.2"]; +s122 -> s126 [label="length_req:0.2"]; +s122 -> s122 [label="length_req:0.8"]; +s122 -> s126 [label="length_rsp:0.2"]; s122 -> s150 [label="length_rsp:0.8"]; -s122 -> s150 [label="length_rsp:1.0"]; -s122 -> s122 [label="feature_req:0.2"]; -s122 -> s124 [label="feature_req:0.8"]; -s122 -> s124 [label="feature_req:1.0"]; -s122 -> s122 [label="feature_rsp:0.2"]; +s122 -> s126 [label="feature_req:0.2"]; +s122 -> s123 [label="feature_req:0.8"]; +s122 -> s126 [label="feature_rsp:0.2"]; s122 -> s120 [label="feature_rsp:0.8"]; -s122 -> s120 [label="feature_rsp:1.0"]; -s122 -> s122 [label="version_req:0.2"]; +s122 -> s126 [label="version_req:0.2"]; s122 -> s120 [label="version_req:0.8"]; -s122 -> s120 [label="version_req:1.0"]; -s122 -> s122 [label="mtu_req:0.2"]; +s122 -> s126 [label="mtu_req:0.2"]; s122 -> s125 [label="mtu_req:0.8"]; -s122 -> s125 [label="mtu_req:1.0"]; -s122 -> s122 [label="pairing_req:0.2"]; +s122 -> s126 [label="pairing_req:0.2"]; s122 -> s120 [label="pairing_req:0.8"]; -s122 -> s120 [label="pairing_req:1.0"]; -s123 -> s122 [label="length_req:0.2"]; -s123 -> s121 [label="length_req:0.8"]; -s123 -> s121 [label="length_req:1.0"]; -s123 -> s122 [label="length_rsp:0.2"]; +s123 -> s126 [label="length_req:0.2"]; +s123 -> s122 [label="length_req:0.8"]; +s123 -> s126 [label="length_rsp:0.2"]; s123 -> s150 [label="length_rsp:0.8"]; -s123 -> s150 [label="length_rsp:1.0"]; -s123 -> s122 [label="feature_req:0.2"]; -s123 -> s124 [label="feature_req:0.8"]; -s123 -> s124 [label="feature_req:1.0"]; -s123 -> s122 [label="feature_rsp:0.2"]; +s123 -> s126 [label="feature_req:0.2"]; +s123 -> s123 [label="feature_req:0.8"]; +s123 -> s126 [label="feature_rsp:0.2"]; s123 -> s120 [label="feature_rsp:0.8"]; -s123 -> s120 [label="feature_rsp:1.0"]; -s123 -> s122 [label="version_req:0.2"]; +s123 -> s126 [label="version_req:0.2"]; s123 -> s120 [label="version_req:0.8"]; -s123 -> s120 [label="version_req:1.0"]; -s123 -> s122 [label="mtu_req:0.2"]; +s123 -> s126 [label="mtu_req:0.2"]; s123 -> s125 [label="mtu_req:0.8"]; -s123 -> s125 [label="mtu_req:1.0"]; -s123 -> s122 [label="pairing_req:0.2"]; +s123 -> s126 [label="pairing_req:0.2"]; s123 -> s120 [label="pairing_req:0.8"]; -s123 -> s120 [label="pairing_req:1.0"]; -s124 -> s122 [label="length_req:0.2"]; -s124 -> s121 [label="length_req:0.8"]; -s124 -> s121 [label="length_req:1.0"]; -s124 -> s122 [label="length_rsp:0.2"]; +s124 -> s126 [label="length_req:0.2"]; +s124 -> s122 [label="length_req:0.8"]; +s124 -> s126 [label="length_rsp:0.2"]; s124 -> s150 [label="length_rsp:0.8"]; -s124 -> s150 [label="length_rsp:1.0"]; -s124 -> s122 [label="feature_req:0.2"]; -s124 -> s124 [label="feature_req:0.8"]; -s124 -> s124 [label="feature_req:1.0"]; -s124 -> s122 [label="feature_rsp:0.2"]; +s124 -> s126 [label="feature_req:0.2"]; +s124 -> s123 [label="feature_req:0.8"]; +s124 -> s126 [label="feature_rsp:0.2"]; s124 -> s120 [label="feature_rsp:0.8"]; -s124 -> s120 [label="feature_rsp:1.0"]; -s124 -> s122 [label="version_req:0.2"]; +s124 -> s126 [label="version_req:0.2"]; s124 -> s120 [label="version_req:0.8"]; -s124 -> s120 [label="version_req:1.0"]; -s124 -> s122 [label="mtu_req:0.2"]; +s124 -> s126 [label="mtu_req:0.2"]; s124 -> s125 [label="mtu_req:0.8"]; -s124 -> s125 [label="mtu_req:1.0"]; -s124 -> s122 [label="pairing_req:0.2"]; +s124 -> s126 [label="pairing_req:0.2"]; s124 -> s120 [label="pairing_req:0.8"]; -s124 -> s120 [label="pairing_req:1.0"]; -s125 -> s122 [label="length_req:0.2"]; -s125 -> s121 [label="length_req:0.8"]; -s125 -> s121 [label="length_req:1.0"]; -s125 -> s122 [label="length_rsp:0.2"]; +s125 -> s126 [label="length_req:0.2"]; +s125 -> s122 [label="length_req:0.8"]; +s125 -> s126 [label="length_rsp:0.2"]; s125 -> s150 [label="length_rsp:0.8"]; -s125 -> s150 [label="length_rsp:1.0"]; -s125 -> s122 [label="feature_req:0.2"]; -s125 -> s124 [label="feature_req:0.8"]; -s125 -> s124 [label="feature_req:1.0"]; -s125 -> s122 [label="feature_rsp:0.2"]; +s125 -> s126 [label="feature_req:0.2"]; +s125 -> s123 [label="feature_req:0.8"]; +s125 -> s126 [label="feature_rsp:0.2"]; s125 -> s120 [label="feature_rsp:0.8"]; -s125 -> s120 [label="feature_rsp:1.0"]; -s125 -> s122 [label="version_req:0.2"]; +s125 -> s126 [label="version_req:0.2"]; s125 -> s120 [label="version_req:0.8"]; -s125 -> s120 [label="version_req:1.0"]; -s125 -> s122 [label="mtu_req:0.2"]; +s125 -> s126 [label="mtu_req:0.2"]; s125 -> s125 [label="mtu_req:0.8"]; -s125 -> s125 [label="mtu_req:1.0"]; -s125 -> s122 [label="pairing_req:0.2"]; +s125 -> s126 [label="pairing_req:0.2"]; s125 -> s120 [label="pairing_req:0.8"]; -s125 -> s120 [label="pairing_req:1.0"]; -s126 -> s122 [label="length_req:0.2"]; -s126 -> s121 [label="length_req:0.8"]; -s126 -> s121 [label="length_req:1.0"]; -s126 -> s122 [label="length_rsp:0.2"]; +s126 -> s126 [label="length_req:0.2"]; +s126 -> s122 [label="length_req:0.8"]; +s126 -> s126 [label="length_rsp:0.2"]; s126 -> s150 [label="length_rsp:0.8"]; -s126 -> s150 [label="length_rsp:1.0"]; -s126 -> s122 [label="feature_req:0.2"]; -s126 -> s124 [label="feature_req:0.8"]; -s126 -> s124 [label="feature_req:1.0"]; -s126 -> s122 [label="feature_rsp:0.2"]; +s126 -> s126 [label="feature_req:0.2"]; +s126 -> s123 [label="feature_req:0.8"]; +s126 -> s126 [label="feature_rsp:0.2"]; s126 -> s120 [label="feature_rsp:0.8"]; -s126 -> s120 [label="feature_rsp:1.0"]; -s126 -> s122 [label="version_req:0.2"]; +s126 -> s126 [label="version_req:0.2"]; s126 -> s120 [label="version_req:0.8"]; -s126 -> s120 [label="version_req:1.0"]; -s126 -> s122 [label="mtu_req:0.2"]; +s126 -> s126 [label="mtu_req:0.2"]; s126 -> s125 [label="mtu_req:0.8"]; -s126 -> s125 [label="mtu_req:1.0"]; -s126 -> s122 [label="pairing_req:0.2"]; +s126 -> s126 [label="pairing_req:0.2"]; s126 -> s120 [label="pairing_req:0.8"]; -s126 -> s120 [label="pairing_req:1.0"]; -s127 -> s122 [label="length_req:0.2"]; -s127 -> s121 [label="length_req:0.8"]; -s127 -> s121 [label="length_req:1.0"]; -s127 -> s122 [label="length_rsp:0.2"]; +s127 -> s126 [label="length_req:0.2"]; +s127 -> s122 [label="length_req:0.8"]; +s127 -> s126 [label="length_rsp:0.2"]; s127 -> s150 [label="length_rsp:0.8"]; -s127 -> s150 [label="length_rsp:1.0"]; -s127 -> s122 [label="feature_req:0.2"]; -s127 -> s124 [label="feature_req:0.8"]; -s127 -> s124 [label="feature_req:1.0"]; -s127 -> s122 [label="feature_rsp:0.2"]; +s127 -> s126 [label="feature_req:0.2"]; +s127 -> s123 [label="feature_req:0.8"]; +s127 -> s126 [label="feature_rsp:0.2"]; s127 -> s120 [label="feature_rsp:0.8"]; -s127 -> s120 [label="feature_rsp:1.0"]; -s127 -> s122 [label="version_req:0.2"]; +s127 -> s126 [label="version_req:0.2"]; s127 -> s120 [label="version_req:0.8"]; -s127 -> s120 [label="version_req:1.0"]; -s127 -> s122 [label="mtu_req:0.2"]; +s127 -> s126 [label="mtu_req:0.2"]; s127 -> s125 [label="mtu_req:0.8"]; -s127 -> s125 [label="mtu_req:1.0"]; -s127 -> s122 [label="pairing_req:0.2"]; +s127 -> s126 [label="pairing_req:0.2"]; s127 -> s120 [label="pairing_req:0.8"]; -s127 -> s120 [label="pairing_req:1.0"]; -s130 -> s131 [label="length_req:1.0"]; -s130 -> s134 [label="length_rsp:1.0"]; -s130 -> s132 [label="feature_req:1.0"]; +s130 -> s133 [label="length_req:1.0"]; +s130 -> s131 [label="length_rsp:1.0"]; +s130 -> s135 [label="feature_req:1.0"]; s130 -> s130 [label="feature_rsp:1.0"]; -s130 -> s152 [label="version_req:1.0"]; -s130 -> s133 [label="mtu_req:1.0"]; +s130 -> s155 [label="version_req:1.0"]; +s130 -> s134 [label="mtu_req:1.0"]; s130 -> s130 [label="pairing_req:1.0"]; -s131 -> s131 [label="length_req:1.0"]; -s131 -> s134 [label="length_rsp:1.0"]; -s131 -> s132 [label="feature_req:1.0"]; +s131 -> s133 [label="length_req:1.0"]; +s131 -> s131 [label="length_rsp:1.0"]; +s131 -> s135 [label="feature_req:1.0"]; s131 -> s130 [label="feature_rsp:1.0"]; -s131 -> s152 [label="version_req:1.0"]; -s131 -> s133 [label="mtu_req:1.0"]; +s131 -> s155 [label="version_req:1.0"]; +s131 -> s134 [label="mtu_req:1.0"]; s131 -> s130 [label="pairing_req:1.0"]; -s132 -> s131 [label="length_req:1.0"]; -s132 -> s134 [label="length_rsp:1.0"]; -s132 -> s132 [label="feature_req:1.0"]; +s132 -> s133 [label="length_req:1.0"]; +s132 -> s131 [label="length_rsp:1.0"]; +s132 -> s135 [label="feature_req:1.0"]; s132 -> s130 [label="feature_rsp:1.0"]; -s132 -> s152 [label="version_req:1.0"]; -s132 -> s133 [label="mtu_req:1.0"]; +s132 -> s155 [label="version_req:1.0"]; +s132 -> s134 [label="mtu_req:1.0"]; s132 -> s130 [label="pairing_req:1.0"]; -s133 -> s131 [label="length_req:1.0"]; -s133 -> s134 [label="length_rsp:1.0"]; -s133 -> s132 [label="feature_req:1.0"]; +s133 -> s133 [label="length_req:1.0"]; +s133 -> s131 [label="length_rsp:1.0"]; +s133 -> s135 [label="feature_req:1.0"]; s133 -> s130 [label="feature_rsp:1.0"]; -s133 -> s152 [label="version_req:1.0"]; -s133 -> s133 [label="mtu_req:1.0"]; +s133 -> s155 [label="version_req:1.0"]; +s133 -> s134 [label="mtu_req:1.0"]; s133 -> s130 [label="pairing_req:1.0"]; -s134 -> s131 [label="length_req:1.0"]; -s134 -> s134 [label="length_rsp:1.0"]; -s134 -> s132 [label="feature_req:1.0"]; +s134 -> s133 [label="length_req:1.0"]; +s134 -> s131 [label="length_rsp:1.0"]; +s134 -> s135 [label="feature_req:1.0"]; s134 -> s130 [label="feature_rsp:1.0"]; -s134 -> s152 [label="version_req:1.0"]; -s134 -> s133 [label="mtu_req:1.0"]; +s134 -> s155 [label="version_req:1.0"]; +s134 -> s134 [label="mtu_req:1.0"]; s134 -> s130 [label="pairing_req:1.0"]; -s135 -> s131 [label="length_req:1.0"]; -s135 -> s134 [label="length_rsp:1.0"]; -s135 -> s132 [label="feature_req:1.0"]; +s135 -> s133 [label="length_req:1.0"]; +s135 -> s131 [label="length_rsp:1.0"]; +s135 -> s135 [label="feature_req:1.0"]; s135 -> s130 [label="feature_rsp:1.0"]; -s135 -> s152 [label="version_req:1.0"]; -s135 -> s133 [label="mtu_req:1.0"]; +s135 -> s155 [label="version_req:1.0"]; +s135 -> s134 [label="mtu_req:1.0"]; s135 -> s130 [label="pairing_req:1.0"]; -s140 -> s141 [label="length_req:1.0"]; -s140 -> s145 [label="length_rsp:1.0"]; -s140 -> s143 [label="feature_req:1.0"]; +s140 -> s142 [label="length_req:1.0"]; +s140 -> s141 [label="length_rsp:1.0"]; +s140 -> s145 [label="feature_req:1.0"]; s140 -> s140 [label="feature_rsp:1.0"]; s140 -> s140 [label="version_req:1.0"]; -s140 -> s144 [label="mtu_req:1.0"]; -s140 -> s156 [label="pairing_req:1.0"]; -s141 -> s141 [label="length_req:1.0"]; -s141 -> s145 [label="length_rsp:1.0"]; -s141 -> s143 [label="feature_req:1.0"]; +s140 -> s143 [label="mtu_req:1.0"]; +s140 -> s152 [label="pairing_req:1.0"]; +s141 -> s142 [label="length_req:1.0"]; +s141 -> s141 [label="length_rsp:1.0"]; +s141 -> s145 [label="feature_req:1.0"]; s141 -> s140 [label="feature_rsp:1.0"]; s141 -> s140 [label="version_req:1.0"]; -s141 -> s144 [label="mtu_req:1.0"]; -s141 -> s156 [label="pairing_req:1.0"]; -s142 -> s141 [label="length_req:1.0"]; -s142 -> s145 [label="length_rsp:1.0"]; -s142 -> s143 [label="feature_req:1.0"]; +s141 -> s143 [label="mtu_req:1.0"]; +s141 -> s152 [label="pairing_req:1.0"]; +s142 -> s142 [label="length_req:1.0"]; +s142 -> s141 [label="length_rsp:1.0"]; +s142 -> s145 [label="feature_req:1.0"]; s142 -> s140 [label="feature_rsp:1.0"]; s142 -> s140 [label="version_req:1.0"]; -s142 -> s144 [label="mtu_req:1.0"]; -s142 -> s156 [label="pairing_req:1.0"]; -s143 -> s141 [label="length_req:1.0"]; -s143 -> s145 [label="length_rsp:1.0"]; -s143 -> s143 [label="feature_req:1.0"]; +s142 -> s143 [label="mtu_req:1.0"]; +s142 -> s152 [label="pairing_req:1.0"]; +s143 -> s142 [label="length_req:1.0"]; +s143 -> s141 [label="length_rsp:1.0"]; +s143 -> s145 [label="feature_req:1.0"]; s143 -> s140 [label="feature_rsp:1.0"]; s143 -> s140 [label="version_req:1.0"]; -s143 -> s144 [label="mtu_req:1.0"]; -s143 -> s156 [label="pairing_req:1.0"]; -s144 -> s141 [label="length_req:1.0"]; -s144 -> s145 [label="length_rsp:1.0"]; -s144 -> s143 [label="feature_req:1.0"]; +s143 -> s143 [label="mtu_req:1.0"]; +s143 -> s152 [label="pairing_req:1.0"]; +s144 -> s142 [label="length_req:1.0"]; +s144 -> s141 [label="length_rsp:1.0"]; +s144 -> s145 [label="feature_req:1.0"]; s144 -> s140 [label="feature_rsp:1.0"]; s144 -> s140 [label="version_req:1.0"]; -s144 -> s144 [label="mtu_req:1.0"]; -s144 -> s156 [label="pairing_req:1.0"]; -s145 -> s141 [label="length_req:1.0"]; -s145 -> s145 [label="length_rsp:1.0"]; -s145 -> s143 [label="feature_req:1.0"]; +s144 -> s143 [label="mtu_req:1.0"]; +s144 -> s152 [label="pairing_req:1.0"]; +s145 -> s142 [label="length_req:1.0"]; +s145 -> s141 [label="length_rsp:1.0"]; +s145 -> s145 [label="feature_req:1.0"]; s145 -> s140 [label="feature_rsp:1.0"]; s145 -> s140 [label="version_req:1.0"]; -s145 -> s144 [label="mtu_req:1.0"]; -s145 -> s156 [label="pairing_req:1.0"]; -s150 -> s151 [label="length_req:1.0"]; -s150 -> s155 [label="length_rsp:1.0"]; -s150 -> s153 [label="feature_req:1.0"]; +s145 -> s143 [label="mtu_req:1.0"]; +s145 -> s152 [label="pairing_req:1.0"]; +s150 -> s153 [label="length_req:1.0"]; +s150 -> s151 [label="length_rsp:1.0"]; +s150 -> s156 [label="feature_req:1.0"]; s150 -> s150 [label="feature_rsp:1.0"]; s150 -> s150 [label="version_req:1.0"]; s150 -> s154 [label="mtu_req:1.0"]; s150 -> s150 [label="pairing_req:1.0"]; -s151 -> s151 [label="length_req:1.0"]; -s151 -> s155 [label="length_rsp:1.0"]; -s151 -> s153 [label="feature_req:1.0"]; +s151 -> s153 [label="length_req:1.0"]; +s151 -> s151 [label="length_rsp:1.0"]; +s151 -> s156 [label="feature_req:1.0"]; s151 -> s150 [label="feature_rsp:1.0"]; s151 -> s150 [label="version_req:1.0"]; s151 -> s154 [label="mtu_req:1.0"]; s151 -> s150 [label="pairing_req:1.0"]; -s152 -> s151 [label="length_req:1.0"]; -s152 -> s155 [label="length_rsp:1.0"]; -s152 -> s153 [label="feature_req:1.0"]; +s152 -> s153 [label="length_req:1.0"]; +s152 -> s151 [label="length_rsp:1.0"]; +s152 -> s156 [label="feature_req:1.0"]; s152 -> s150 [label="feature_rsp:1.0"]; s152 -> s150 [label="version_req:1.0"]; s152 -> s154 [label="mtu_req:1.0"]; s152 -> s150 [label="pairing_req:1.0"]; -s153 -> s151 [label="length_req:1.0"]; -s153 -> s155 [label="length_rsp:1.0"]; -s153 -> s153 [label="feature_req:1.0"]; +s153 -> s153 [label="length_req:1.0"]; +s153 -> s151 [label="length_rsp:1.0"]; +s153 -> s156 [label="feature_req:1.0"]; s153 -> s150 [label="feature_rsp:1.0"]; s153 -> s150 [label="version_req:1.0"]; s153 -> s154 [label="mtu_req:1.0"]; s153 -> s150 [label="pairing_req:1.0"]; -s154 -> s151 [label="length_req:1.0"]; -s154 -> s155 [label="length_rsp:1.0"]; -s154 -> s153 [label="feature_req:1.0"]; +s154 -> s153 [label="length_req:1.0"]; +s154 -> s151 [label="length_rsp:1.0"]; +s154 -> s156 [label="feature_req:1.0"]; s154 -> s150 [label="feature_rsp:1.0"]; s154 -> s150 [label="version_req:1.0"]; s154 -> s154 [label="mtu_req:1.0"]; s154 -> s150 [label="pairing_req:1.0"]; -s155 -> s151 [label="length_req:1.0"]; -s155 -> s155 [label="length_rsp:1.0"]; -s155 -> s153 [label="feature_req:1.0"]; +s155 -> s153 [label="length_req:1.0"]; +s155 -> s151 [label="length_rsp:1.0"]; +s155 -> s156 [label="feature_req:1.0"]; s155 -> s150 [label="feature_rsp:1.0"]; s155 -> s150 [label="version_req:1.0"]; s155 -> s154 [label="mtu_req:1.0"]; s155 -> s150 [label="pairing_req:1.0"]; -s156 -> s151 [label="length_req:1.0"]; -s156 -> s155 [label="length_rsp:1.0"]; -s156 -> s153 [label="feature_req:1.0"]; +s156 -> s153 [label="length_req:1.0"]; +s156 -> s151 [label="length_rsp:1.0"]; +s156 -> s156 [label="feature_req:1.0"]; s156 -> s150 [label="feature_rsp:1.0"]; s156 -> s150 [label="version_req:1.0"]; s156 -> s154 [label="mtu_req:1.0"]; diff --git a/aalpy/utils/ModelChecking.py b/aalpy/utils/ModelChecking.py index 8b1414e7..8d271816 100644 --- a/aalpy/utils/ModelChecking.py +++ b/aalpy/utils/ModelChecking.py @@ -23,7 +23,8 @@ def get_properties_file(exp_name): 'shared_coin': aalpy.paths.path_to_properties + 'shared_coin_eval.props', 'slot_machine': aalpy.paths.path_to_properties + 'slot_machine_eval.props', 'mqtt': aalpy.paths.path_to_properties + 'emqtt_two_client.props', - 'tcp': aalpy.paths.path_to_properties + 'tcp_eval.props' + 'tcp': aalpy.paths.path_to_properties + 'tcp_eval.props', + 'bluetooth': aalpy.paths.path_to_properties + 'bluetooth.props', } return property_files[exp_name] @@ -40,7 +41,12 @@ def get_correct_prop_values(exp_name): 'prob5': 0.28567, 'prob6': 0.2500000000000001, 'prob7': 0.025445087448668406}, 'mqtt': {'prob1': 0.9612, 'prob2': 0.34390000000000004, 'prob3': 0.6513215599000001, 'prob4': 0.814697981114816, 'prob5': 0.7290000000000001}, - 'tcp': {'prob1': 0.19, 'prob2': 0.5695327900000001, 'prob3': 0.7712320754503901, 'prob4': 0.8784233454094308} + 'tcp': {'prob1': 0.19, 'prob2': 0.5695327900000001, 'prob3': 0.7712320754503901, 'prob4': 0.8784233454094308}, + 'bluetooth': {'prop1': 0.16800000000000004, 'prop2': 0.3926480000000001, 'prop3': 0.5572338000000001, + 'prop4': 0.6772233874640001, 'prop5': 0.7646958490393682, 'prop6': 0.8284632739463244, + 'prop7': 0.36000000000000004, 'prop8': 0.5904, 'prop9': 0.7902848, + 'prop10': 0.8926258176000001, 'prop11': 0.9450244186112, 'prop12': 0.9718525023289344, + 'prop13': 0.9855884811924145} } return list(correct_model_properties[exp_name].values()) @@ -229,6 +235,7 @@ def stop_based_on_confidence(hypothesis, property_based_stopping, print_level=2) return True + def bisimilar(a1: DeterministicAutomaton, a2: DeterministicAutomaton): """ Checks whether the provided automata are bisimilar @@ -238,9 +245,10 @@ def bisimilar(a1: DeterministicAutomaton, a2: DeterministicAutomaton): raise ValueError("tried to check bisimilarity of distinct automaton types") supported_automaton_types = (Dfa, MooreMachine, MealyMachine) if not isinstance(a1, supported_automaton_types): - raise NotImplementedError(f"bisimilarity is not implemented for {a1.__class__.__name__}. Supported: {', '.join(t.__name__ for t in supported_automaton_types)}") + raise NotImplementedError( + f"bisimilarity is not implemented for {a1.__class__.__name__}. Supported: {', '.join(t.__name__ for t in supported_automaton_types)}") - to_check : Queue[Tuple[AutomatonState, AutomatonState]] = Queue() + to_check: Queue[Tuple[AutomatonState, AutomatonState]] = Queue() to_check.put((a1.initial_state, a2.initial_state)) requirements = dict() requirements[(a1.initial_state, a2.initial_state)] = [] @@ -248,8 +256,8 @@ def bisimilar(a1: DeterministicAutomaton, a2: DeterministicAutomaton): while not to_check.empty(): s1, s2 = to_check.get() if (isinstance(s1, DfaState)) and s1.is_accepting != s2.is_accepting or \ - (isinstance(s1, MooreState) and s1.output != s2.output) or \ - (isinstance(s1, MealyState) and s1.output_fun != s2.output_fun): + (isinstance(s1, MooreState) and s1.output != s2.output) or \ + (isinstance(s1, MealyState) and s1.output_fun != s2.output_fun): return requirements[(s1, s2)] t1, t2 = s1.transitions, s2.transitions @@ -265,6 +273,7 @@ def bisimilar(a1: DeterministicAutomaton, a2: DeterministicAutomaton): requirements[(c1, c2)] = requirements[(s1, s2)] + [t] to_check.put((c1, c2)) + def compare_automata(aut_1: DeterministicAutomaton, aut_2: DeterministicAutomaton, num_cex=10): """ Finds cases of non-conformance between first and second automaton. This is done by performing RandomW equivalence @@ -391,6 +400,7 @@ def statistical_model_checking(model, goals, max_num_steps, num_tests=105967): num of tests containing element of goals set / num_tests """ + def compute_output_sequence(model, seq): model.reset_to_initial() observed_outputs = {model.step(i) for i in seq} @@ -404,4 +414,4 @@ def compute_output_sequence(model, seq): if goals & outputs: goal_reached += 1 - return goal_reached / num_tests \ No newline at end of file + return goal_reached / num_tests