Skip to content

Commit

Permalink
formating
Browse files Browse the repository at this point in the history
  • Loading branch information
reb-ddm committed Feb 10, 2025
1 parent af58808 commit eb5cf27
Show file tree
Hide file tree
Showing 5 changed files with 29 additions and 44 deletions.
4 changes: 1 addition & 3 deletions core/KaSa_rep/reachability_analysis/bdu_static_views.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
4 changes: 3 additions & 1 deletion core/KaSa_rep/reachability_analysis/covering_classes_main.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
20 changes: 10 additions & 10 deletions core/KaSa_rep/reachability_analysis/rules_domain.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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 =
Expand Down
44 changes: 15 additions & 29 deletions core/KaSa_rep/reachability_analysis/views_domain.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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 *)
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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 =
Expand Down Expand Up @@ -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) =
Expand Down

0 comments on commit eb5cf27

Please sign in to comment.