Skip to content

Commit

Permalink
first decompose before printing (for agent_domain, rule_domain and pa…
Browse files Browse the repository at this point in the history 
…rallel-bonds domain)
  • Loading branch information
@reb-ddm
reb-ddm committed Feb 12, 2025
1 parent c003b21 commit 44e4e0b
Show file tree
Hide file tree
Showing 6 changed files with 62 additions and 43 deletions.
37 changes: 24 additions & 13 deletions core/KaSa_rep/frontend/handler.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
)

(*****************************************************************************)
Expand Down Expand Up @@ -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
)
Expand All @@ -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 =
Expand Down
4 changes: 3 additions & 1 deletion core/KaSa_rep/frontend/handler.mli
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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 ->
Expand Down
15 changes: 8 additions & 7 deletions core/KaSa_rep/reachability_analysis/agents_domain.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down
6 changes: 3 additions & 3 deletions core/KaSa_rep/reachability_analysis/analyzer_headers.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
36 changes: 20 additions & 16 deletions core/KaSa_rep/reachability_analysis/parallel_bonds_type.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down
7 changes: 4 additions & 3 deletions core/KaSa_rep/reachability_analysis/rules_domain.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down

0 comments on commit 44e4e0b

Please sign in to comment.