From 44e4e0b849645c401d638cbccd0402090b9ff793 Mon Sep 17 00:00:00 2001 From: Rebecca Ghidini Date: Wed, 12 Feb 2025 15:18:59 +0100 Subject: [PATCH] first decompose before printing (for agent_domain, rule_domain and parallel-bonds domain) --- core/KaSa_rep/frontend/handler.ml | 37 ++++++++++++------- core/KaSa_rep/frontend/handler.mli | 4 +- .../reachability_analysis/agents_domain.ml | 15 ++++---- .../reachability_analysis/analyzer_headers.ml | 6 +-- .../parallel_bonds_type.ml | 36 ++++++++++-------- .../reachability_analysis/rules_domain.ml | 7 ++-- 6 files changed, 62 insertions(+), 43 deletions(-) diff --git a/core/KaSa_rep/frontend/handler.ml b/core/KaSa_rep/frontend/handler.ml index 93d3d7c58..f98267a2a 100644 --- a/core/KaSa_rep/frontend/handler.ml +++ b/core/KaSa_rep/frontend/handler.ml @@ -694,9 +694,9 @@ let print_guard_mvbdu parameters error kappa_handler bdu_handler Ckappa_sig.Views_bdu.mvbdu_true parameters bdu_handler error in if Ckappa_sig.Views_bdu.equal mvbdu mvbdu_true then - error + error, bdu_handler else ( - let error, _, mvbdu_extensional = + let error, bdu_handler, mvbdu_extensional = Ckappa_sig.Views_bdu.extensional_of_mvbdu parameters bdu_handler error mvbdu in @@ -736,7 +736,7 @@ let print_guard_mvbdu parameters error kappa_handler bdu_handler (false, error) mvbdu_extensional in (* let () = Loggers.fprintf loggers ")" in *) - error + error, bdu_handler ) (*****************************************************************************) @@ -836,33 +836,44 @@ let guard_to_bdu parameters error handler_bdu guard bdu_restriction = let print_guard_mvbdu_decompose parameters error kappa_handler bdu_handler ?(with_comma = false) mvbdu restriction_bdu = let error, bdu_handler, mvbdu_list = - Ckappa_sig.Views_bdu.mvbdu_cartesian_abstraction parameters bdu_handler - error mvbdu + Ckappa_sig.Views_bdu.mvbdu_full_cartesian_decomposition parameters + bdu_handler error mvbdu in let error, _, _ = List.fold_left (fun (error, bdu_handler, with_comma) mvbdu -> - let () = - if with_comma then - Loggers.fprintf (Remanent_parameters.get_logger parameters) "," - in let error, bdu_handler = let error, bdu_handler, is_true = mvbdu_is_true_for_guards parameters bdu_handler error mvbdu restriction_bdu in + let error, bdu_handler, variables = + Ckappa_sig.Views_bdu.variables_list_of_mvbdu parameters bdu_handler + error mvbdu + in + let error, bdu_handler, nr_variables = + Ckappa_sig.Views_bdu.nbr_variables parameters bdu_handler error + variables + in if is_true then error, bdu_handler else ( let () = - Loggers.fprintf (Remanent_parameters.get_logger parameters) "(" + if with_comma then + Loggers.fprintf (Remanent_parameters.get_logger parameters) "," in - let error = + + let () = + if nr_variables > 1 then + Loggers.fprintf (Remanent_parameters.get_logger parameters) "(" + in + let error, bdu_handler = print_guard_mvbdu parameters error kappa_handler bdu_handler ~with_comma:false mvbdu in let () = - Loggers.fprintf (Remanent_parameters.get_logger parameters) ")" + if nr_variables > 1 then + Loggers.fprintf (Remanent_parameters.get_logger parameters) ")" in error, bdu_handler ) @@ -871,7 +882,7 @@ let print_guard_mvbdu_decompose parameters error kappa_handler bdu_handler (error, bdu_handler, with_comma) mvbdu_list in - error + error, bdu_handler let collect_guard_mvbdus parameters error mvbdu_handler compilation bdu_restriction = diff --git a/core/KaSa_rep/frontend/handler.mli b/core/KaSa_rep/frontend/handler.mli index a11391b26..3e7659641 100644 --- a/core/KaSa_rep/frontend/handler.mli +++ b/core/KaSa_rep/frontend/handler.mli @@ -287,14 +287,16 @@ val collect_guard_mvbdus : * Ckappa_sig.Views_bdu.mvbdu Ckappa_sig.Rule_setmap.Map.t (*************************************************************) -val print_guard_mvbdu : +val print_guard_mvbdu_decompose : Remanent_parameters_sig.parameters -> Exception_without_parameter.exceptions_caught_and_uncaught -> Cckappa_sig.kappa_handler -> Ckappa_sig.Views_bdu.handler -> ?with_comma:bool -> Ckappa_sig.Views_bdu.mvbdu -> + Ckappa_sig.Views_bdu.mvbdu -> Exception_without_parameter.exceptions_caught_and_uncaught + * Ckappa_sig.Views_bdu.handler val print_labels : Remanent_parameters_sig.parameters -> diff --git a/core/KaSa_rep/reachability_analysis/agents_domain.ml b/core/KaSa_rep/reachability_analysis/agents_domain.ml index 69848e053..c52850748 100644 --- a/core/KaSa_rep/reachability_analysis/agents_domain.ml +++ b/core/KaSa_rep/reachability_analysis/agents_domain.ml @@ -677,7 +677,6 @@ module Domain = struct let parameters = get_parameter static in let result = get_seen_agent dynamic in let handler = get_kappa_handler static in - let bdu_handler = get_mvbdu_handler dynamic in if Remanent_parameters.get_dump_reachability_analysis_result parameters then ( let error, bool = Ckappa_sig.Agent_type_nearly_Inf_Int_storage_Imperatif.fold parameters @@ -739,24 +738,26 @@ module Domain = struct let error, dynamic, is_false = is_false_mvbdu parameters error dynamic mvbdu in - let error = + let error, dynamic = if is_false then ( let () = Loggers.fprintf loggers "%s cannot occur in the model" agent_string in - error + error, dynamic ) else ( let () = Loggers.fprintf loggers "%s can occur in the model if " agent_string in - let error = - Handler.print_guard_mvbdu parameters error handler - bdu_handler mvbdu + let bdu_handler = get_mvbdu_handler dynamic in + let error, bdu_handler = + Handler.print_guard_mvbdu_decompose parameters error + handler bdu_handler mvbdu restriction_bdu in + let dynamic = set_mvbdu_handler bdu_handler dynamic in let () = Loggers.fprintf loggers "." in - error + error, dynamic ) in let () = Loggers.print_newline loggers in diff --git a/core/KaSa_rep/reachability_analysis/analyzer_headers.ml b/core/KaSa_rep/reachability_analysis/analyzer_headers.ml index 64fdde7cd..44d59daa3 100644 --- a/core/KaSa_rep/reachability_analysis/analyzer_headers.ml +++ b/core/KaSa_rep/reachability_analysis/analyzer_headers.ml @@ -290,13 +290,13 @@ let scan_rule static error mvbdu_handler = in let static = set_common_views store_result static in let error, mvbdu_handler, restriction_mvbdu = - Common_static.compute_restriction_mvbdu parameters error mvbdu_handler + Handler.compute_restriction_mvbdu parameters error mvbdu_handler kappa_handler in let static = set_restriction_mvbdu restriction_mvbdu static in let error, mvbdu_handler, guard_mvbdus = - Common_static.collect_guard_mvbdus parameters error mvbdu_handler - compilation restriction_mvbdu + Handler.collect_guard_mvbdus parameters error mvbdu_handler compilation + restriction_mvbdu in let static = set_guard_mvbdus guard_mvbdus static in error, mvbdu_handler, static diff --git a/core/KaSa_rep/reachability_analysis/parallel_bonds_type.ml b/core/KaSa_rep/reachability_analysis/parallel_bonds_type.ml index d88e42f75..5b557bcad 100644 --- a/core/KaSa_rep/reachability_analysis/parallel_bonds_type.ml +++ b/core/KaSa_rep/reachability_analysis/parallel_bonds_type.ml @@ -264,24 +264,25 @@ let compute_mvbdus_for_parallel_vs_non_parallel_bounds parameters bdu_handler bdu_undefined_bonds ) let print_guard_parameters_natural_language parameters prefix error - kappa_handler bdu_handler is_true mvbdu = + kappa_handler bdu_handler is_true mvbdu restriction_bdu = if not is_true then ( let () = Loggers.fprintf (Remanent_parameters.get_logger parameters) "%sFor the following values of the guard parameters: \n" prefix in - let error = - Handler.print_guard_mvbdu parameters error kappa_handler bdu_handler mvbdu + let error, bdu_handler = + Handler.print_guard_mvbdu_decompose parameters error kappa_handler + bdu_handler mvbdu restriction_bdu in let () = Loggers.fprintf (Remanent_parameters.get_logger parameters) "\nIt holds that: " in - error + error, bdu_handler ) else - error + error, bdu_handler let print_parallel_constraint ?(verbose = true) ?(sparse = false) ?final_resul:(final_result = false) ?(dump_any = false) parameters error @@ -415,9 +416,10 @@ let print_parallel_constraint ?(verbose = true) ?(sparse = false) (Remanent_parameters.get_logger parameters) parameters error t_precondition in - let error = - Handler.print_guard_mvbdu parameters error kappa_handler - bdu_handler ~with_comma:true parallel_bond_mvbdu + let error, bdu_handler = + Handler.print_guard_mvbdu_decompose parameters error + kappa_handler bdu_handler ~with_comma:true parallel_bond_mvbdu + restriction_bdu in let () = Loggers.fprintf @@ -447,9 +449,10 @@ let print_parallel_constraint ?(verbose = true) ?(sparse = false) | Remanent_parameters_sig.Natural_language -> if verbose then if not parallel_is_false then ( - let error = + let error, bdu_handler = print_guard_parameters_natural_language parameters prefix error kappa_handler bdu_handler parallel_is_true parallel_bond_mvbdu + restriction_bdu in let () = Loggers.fprintf @@ -504,9 +507,10 @@ let print_parallel_constraint ?(verbose = true) ?(sparse = false) (Remanent_parameters.get_logger parameters) parameters error t_precondition in - let error = - Handler.print_guard_mvbdu parameters error kappa_handler - bdu_handler ~with_comma:true non_parallel_bond_mvbdu + let error, bdu_handler = + Handler.print_guard_mvbdu_decompose parameters error + kappa_handler bdu_handler ~with_comma:true + non_parallel_bond_mvbdu restriction_bdu in let () = Loggers.fprintf @@ -537,10 +541,10 @@ let print_parallel_constraint ?(verbose = true) ?(sparse = false) let error, bdu_handler = if verbose then if not non_parallel_is_false then ( - let error = + let error, bdu_handler = print_guard_parameters_natural_language parameters prefix error kappa_handler bdu_handler non_parallel_is_true - non_parallel_bond_mvbdu + non_parallel_bond_mvbdu restriction_bdu in let () = Loggers.fprintf @@ -589,10 +593,10 @@ let print_parallel_constraint ?(verbose = true) ?(sparse = false) error, bdu_handler | Remanent_parameters_sig.Natural_language -> if not any_bond_is_false then ( - let error = + let error, bdu_handler = print_guard_parameters_natural_language parameters prefix error kappa_handler bdu_handler any_bond_is_true - any_bond_mvbdu + any_bond_mvbdu restriction_bdu in let () = Loggers.fprintf diff --git a/core/KaSa_rep/reachability_analysis/rules_domain.ml b/core/KaSa_rep/reachability_analysis/rules_domain.ml index 61081699d..ed04cf027 100644 --- a/core/KaSa_rep/reachability_analysis/rules_domain.ml +++ b/core/KaSa_rep/reachability_analysis/rules_domain.ml @@ -361,6 +361,7 @@ module Domain = struct let compiled = get_compil static in let kappa_handler = get_kappa_handler static in let bdu_handler = get_mvbdu_handler dynamic in + let restriction_bdu = get_restriction_mvbdu static in if Remanent_parameters.get_dump_reachability_analysis_result parameters then ( let error, bool = Ckappa_sig.Rule_nearly_Inf_Int_storage_Imperatif.fold parameters error @@ -442,9 +443,9 @@ module Domain = struct (Remanent_parameters.get_logger parameters) "%s could be applied if " rule_string in - let error = - Handler.print_guard_mvbdu parameters error kappa_handler - bdu_handler mvbdu + let error, _ = + Handler.print_guard_mvbdu_decompose parameters error + kappa_handler bdu_handler mvbdu restriction_bdu in let () = Loggers.fprintf