diff --git a/core/KaSa_rep/reachability_analysis/bdu_static_views.ml b/core/KaSa_rep/reachability_analysis/bdu_static_views.ml index 0f65d5d1b..09b5446cf 100644 --- a/core/KaSa_rep/reachability_analysis/bdu_static_views.ml +++ b/core/KaSa_rep/reachability_analysis/bdu_static_views.ml @@ -1041,9 +1041,7 @@ let scan_rule_set parameters log_info handler_bdu error handler_kappa compiled store_potential_side_effects store_remanent_triple site_correspondence guard_mvbdus restriction_bdu = let error, init = init_bdu_analysis_static parameters error in - let nr_guard_params = - Handler.get_nr_guard_parameters handler_kappa - in + let nr_guard_params = Handler.get_nr_guard_parameters handler_kappa in let error, (handler_bdu, store_guard_restriction_bdu) = collect_guard_restriction_bdu parameters handler_bdu error site_correspondence nr_guard_params restriction_bdu diff --git a/core/KaSa_rep/reachability_analysis/covering_classes_main.ml b/core/KaSa_rep/reachability_analysis/covering_classes_main.ml index cbe10923d..2879c30cb 100644 --- a/core/KaSa_rep/reachability_analysis/covering_classes_main.ml +++ b/core/KaSa_rep/reachability_analysis/covering_classes_main.ml @@ -714,7 +714,9 @@ let scan_predicate_covering_classes parameters error handler_kappa compil = let error, last_site = Handler.last_site_of_agent parameters error handler_kappa ag in - let nr_guard_parameters = Handler.get_nr_guard_parameters handler_kappa in + let nr_guard_parameters = + Handler.get_nr_guard_parameters handler_kappa + in let size_map1 = 1 + Ckappa_sig.int_of_site_name last_site diff --git a/core/KaSa_rep/reachability_analysis/rules_domain.ml b/core/KaSa_rep/reachability_analysis/rules_domain.ml index 08a930e8f..3cb4981f9 100644 --- a/core/KaSa_rep/reachability_analysis/rules_domain.ml +++ b/core/KaSa_rep/reachability_analysis/rules_domain.ml @@ -207,16 +207,16 @@ module Domain = struct let error, dynamic, is_false = is_false_mvbdu parameters error dynamic mvbdu in - let guard_mvbdus = get_guard_mvbdus static in - let error, dynamic, guard_bdu = - get_bdu_guard parameters dynamic error guard_mvbdus rule_id - in - let bdu_handler = get_mvbdu_handler dynamic in - let error, bdu_handler, precondition = - Communication.update_state_of_guard_parameters parameters error - bdu_handler precondition guard_bdu - in - let dynamic = set_mvbdu_handler bdu_handler dynamic in + let guard_mvbdus = get_guard_mvbdus static in + let error, dynamic, guard_bdu = + get_bdu_guard parameters dynamic error guard_mvbdus rule_id + in + let bdu_handler = get_mvbdu_handler dynamic in + let error, bdu_handler, precondition = + Communication.update_state_of_guard_parameters parameters error + bdu_handler precondition guard_bdu + in + let dynamic = set_mvbdu_handler bdu_handler dynamic in if is_false then ( let error, precondition = Communication.the_rule_is_applied_for_the_first_time diff --git a/core/KaSa_rep/reachability_analysis/site_across_bonds_domain.ml b/core/KaSa_rep/reachability_analysis/site_across_bonds_domain.ml index 3e575644f..46af7a170 100644 --- a/core/KaSa_rep/reachability_analysis/site_across_bonds_domain.ml +++ b/core/KaSa_rep/reachability_analysis/site_across_bonds_domain.ml @@ -78,7 +78,6 @@ module Domain = struct let lift f x = f (get_global_static_information x) let get_parameter static = lift Analyzer_headers.get_parameter static let get_kappa_handler static = lift Analyzer_headers.get_kappa_handler static - let get_guard_mvbdus static = lift Analyzer_headers.get_guard_mvbdus static let get_potential_side_effects static = diff --git a/core/KaSa_rep/reachability_analysis/views_domain.ml b/core/KaSa_rep/reachability_analysis/views_domain.ml index 25b68bdce..19b39cd97 100644 --- a/core/KaSa_rep/reachability_analysis/views_domain.ml +++ b/core/KaSa_rep/reachability_analysis/views_domain.ml @@ -1023,9 +1023,7 @@ module Domain = struct let collect_bdu_enabled parameters error static dynamic bdu_false fixpoint_result proj_bdu_test_restriction precondition handler_kappa = - let nr_guard_parameters = - Handler.get_nr_guard_parameters handler_kappa - in + let nr_guard_parameters = Handler.get_nr_guard_parameters handler_kappa in let bdu_handler = get_mvbdu_handler dynamic in let error, bdu_handler, state_guard_parameters = Communication.get_state_of_guard_parameters parameters bdu_handler error @@ -1089,7 +1087,8 @@ module Domain = struct in let bdu_handler = get_mvbdu_handler dynamic in let error, bdu_handler, precondition = - Communication.update_state_of_guard_parameters parameters error bdu_handler precondition bdu_guard + Communication.update_state_of_guard_parameters parameters error + bdu_handler precondition bdu_guard in let dynamic = set_mvbdu_handler bdu_handler dynamic in error, dynamic, precondition @@ -1221,9 +1220,7 @@ module Domain = struct let precondition_empty_step_list kappa_handler parameters error dynamic rule_id path store_agent_name bdu_false bdu_true store_covering_classes_id site_correspondence fixpoint_result proj_bdu_test_restriction = - let nr_guard_params = - Handler.get_nr_guard_parameters kappa_handler - in + let nr_guard_params = Handler.get_nr_guard_parameters kappa_handler in let error, agent_type = match Ckappa_sig.RuleAgent_map_and_set.Map.find_option_without_logs parameters @@ -1417,9 +1414,7 @@ module Domain = struct where (agent_type_in, site_in) is the information of the last agent, and (agent_type', site_in) is the information of the agent of the pattern *) - let nr_guard_params = - Handler.get_nr_guard_parameters kappa_handler - in + let nr_guard_params = Handler.get_nr_guard_parameters kappa_handler in let to_guard_or_site s = Ckappa_sig.guard_p_then_site_of_site s nr_guard_params in @@ -2210,9 +2205,7 @@ module Domain = struct let precondition_empty_aux parameters error path pattern kappa_handler dynamic bdu_false bdu_true site_correspondence site_correspondence_map fixpoint_result cv_list = - let nr_guard_params = - Handler.get_nr_guard_parameters kappa_handler - in + let nr_guard_params = Handler.get_nr_guard_parameters kappa_handler in let to_guard_or_site s = Ckappa_sig.guard_p_then_site_of_site s nr_guard_params in @@ -2356,9 +2349,7 @@ module Domain = struct let site_correspondence = get_remanent_triple static in let site_correspondence_map = get_site_correspondence_array static in let store_covering_classes_id = get_covering_classes_id static in - let nr_guard_parameters = - Handler.get_nr_guard_parameters kappa_handler - in + let nr_guard_parameters = Handler.get_nr_guard_parameters kappa_handler in (*---------------------------------------------------------*) (* Why an arbitrary patterns would be stored in that map *) (* For each view, you have to collect the set of sites *) @@ -2474,10 +2465,11 @@ module Domain = struct pattern.Cckappa_sig.views (dynamic, bdu_true) in let bdu_handler = get_mvbdu_handler dynamic in - let error, bdu_handler, precondition = - Communication.update_state_of_guard_parameters parameters error bdu_handler precondition result_bdu_guard - in - let dynamic = set_mvbdu_handler bdu_handler dynamic in + let error, bdu_handler, precondition = + Communication.update_state_of_guard_parameters parameters error + bdu_handler precondition result_bdu_guard + in + let dynamic = set_mvbdu_handler bdu_handler dynamic in let precondition = Communication.refine_information_about_state_of_sites_in_precondition precondition @@ -3061,9 +3053,7 @@ module Domain = struct parameters handler error handler_kappa (*store_new_index_pair_map*) site_correspondence result = - let nr_guard_params = - Handler.get_nr_guard_parameters handler_kappa - in + let nr_guard_params = Handler.get_nr_guard_parameters handler_kappa in let error', handler, mvbdu_true = Ckappa_sig.Views_bdu.mvbdu_true parameters handler error in @@ -3159,9 +3149,7 @@ module Domain = struct let stabilise_bdu_update_map_gen_decomposition decomposition ~smash ~show_dep_with_dimmension_higher_than:dim_min parameters handler error handler_kappa site_correspondence result = - let nr_guard_parameters = - Handler.get_nr_guard_parameters handler_kappa - in + let nr_guard_parameters = Handler.get_nr_guard_parameters handler_kappa in let log = Remanent_parameters.get_logger parameters in if smash then ( let error', handler, output = @@ -3600,9 +3588,7 @@ module Domain = struct let kappa_handler = get_kappa_handler static in let handler = get_mvbdu_handler dynamic in let parameters = get_parameter static in - let nr_guard_params = - Handler.get_nr_guard_parameters kappa_handler - in + let nr_guard_params = Handler.get_nr_guard_parameters kappa_handler in let contact_map = Preprocess.init_contact_map in (*-----------------------------------------------*) let error, (handler, contact_map) =