Skip to content

Commit

Permalink
added guard mvbdus to global information
Browse files Browse the repository at this point in the history
  • Loading branch information
@reb-ddm
reb-ddm committed Jan 29, 2025
1 parent 5ad0dc3 commit 959839e
Show file tree
Hide file tree
Showing 4 changed files with 186 additions and 65 deletions.
38 changes: 34 additions & 4 deletions core/KaSa_rep/reachability_analysis/analyzer_headers.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -25,6 +25,8 @@ type global_static_information = {
global_parameter: Remanent_parameters_sig.parameters;
global_common_views: Common_static.common_views;
global_wake_up_relation: Common_static.site_to_rules;
global_guard_mvbdus: Ckappa_sig.Views_bdu.mvbdu Ckappa_sig.Rule_setmap.Map.t;
global_restriction_mvbdu: Ckappa_sig.Views_bdu.mvbdu;
}

let add_wake_up_relation static wake =
Expand Down Expand Up @@ -254,38 +256,66 @@ let compute_initial_state error static =
error, List.rev init

(*****************************************************************************)
(*RULE*)
(*MVBDU OF THE GUARDS*)
(*****************************************************************************)

let get_mvbdu_handler dynamic = dynamic.mvbdu_handler
let set_mvbdu_handler handler dynamic = { dynamic with mvbdu_handler = handler }

let set_guard_mvbdus guard_mvbdus static =
{ static with global_guard_mvbdus = guard_mvbdus }

let set_restriction_mvbdu restriction_mvbdu static =
{ static with global_restriction_mvbdu = restriction_mvbdu }

(*****************************************************************************)
(*RULE*)
(*****************************************************************************)

let get_log_info dynamic = dynamic.log_info
let set_log_info log_info dynamic = { dynamic with log_info }

let scan_rule static error =
let scan_rule static error mvbdu_handler =
let parameters = get_parameter static in
let kappa_handler = get_kappa_handler static in
let compilation = get_cc_code static in
let error, store_result =
Common_static.scan_rule_set parameters error kappa_handler compilation
in
let static = set_common_views store_result static in
error, static
let error, mvbdu_handler, restriction_mvbdu =
Common_static.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
in
let static = set_guard_mvbdus guard_mvbdus static in
error, mvbdu_handler, static

let initialize_global_information parameters log_info error mvbdu_handler
compilation kappa_handler =
let error, init_common = Common_static.init_common_views parameters error in
let error, wake_up = Common_static.empty_site_to_rules parameters error in
let error, mvbdu_handler, restriction_mvbdu =
Ckappa_sig.Views_bdu.mvbdu_true parameters mvbdu_handler error
in
let init_global_static =
{
global_compilation_result = { cc_code = compilation; kappa_handler };
global_parameter = parameters;
global_common_views = init_common;
global_wake_up_relation = wake_up;
global_guard_mvbdus = Ckappa_sig.Rule_setmap.Map.empty;
global_restriction_mvbdu = restriction_mvbdu;
}
in
let error, mvbdu_handler, static =
scan_rule init_global_static error mvbdu_handler
in
let init_dynamic = { dynamic_dummy = (); mvbdu_handler; log_info } in
let error, static = scan_rule init_global_static error in
error, static, init_dynamic

let dummy_dead_rules _ error _ = error, false
Expand Down
58 changes: 19 additions & 39 deletions core/KaSa_rep/reachability_analysis/bdu_static_views.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -88,31 +88,6 @@ let init_bdu_analysis_static parameters error =
in
error, init_bdu_analysis_static

(***************************************************************************)
(* bdu operations that restrict the values of the guards to 0 and 1*)
(** Returns the disjunction of the two mvbdus but the values of each variable are restricted to the values 0 and 1.
Used for the guard parameters, which model boolean values. *)

let mvbdu_or_for_guards parameters handler_bdu error mvbdu1 mvbdu2
bdu_restriction =
let error, handler_bdu, or_bdu =
Ckappa_sig.Views_bdu.mvbdu_or parameters handler_bdu error mvbdu1 mvbdu2
in
(*all guard parameters must have value 0 or 1*)
Ckappa_sig.Views_bdu.mvbdu_and parameters handler_bdu error or_bdu
bdu_restriction

let mvbdu_and_for_guards parameters handler_bdu error mvbdu1 mvbdu2 =
Ckappa_sig.Views_bdu.mvbdu_and parameters handler_bdu error mvbdu1 mvbdu2

let mvbdu_not_for_guards parameters handler_bdu error mvbdu bdu_restriction =
let error, handler_bdu, not_bdu =
Ckappa_sig.Views_bdu.mvbdu_not parameters handler_bdu error mvbdu
in
(*all guard parameters must have value 0 or 1*)
Ckappa_sig.Views_bdu.mvbdu_and parameters handler_bdu error not_bdu
bdu_restriction

let get_bdu_guard store_guard_bdu rule_id agent_type cv_id bdu_true =
match Ckappa_sig.Rule_setmap.Map.find_option rule_id store_guard_bdu with
| None -> bdu_true, bdu_true
Expand Down Expand Up @@ -146,7 +121,7 @@ let add_dependency_triple_bdu parameters handler error
(agent_type, rule_id, cv_id) bdu store_result guard_bdu restriction_bdu =
(*add guard information*)
let error, handler, bdu =
mvbdu_and_for_guards parameters handler error bdu guard_bdu
Common_static.mvbdu_and_for_guards parameters handler error bdu guard_bdu
in
let error, handler, bdu_false =
Ckappa_sig.Views_bdu.mvbdu_false parameters handler error
Expand All @@ -158,7 +133,8 @@ let add_dependency_triple_bdu parameters handler error
in
(* In the case when the agent is created twice, we take the union *)
let error, handler, bdu_new =
mvbdu_or_for_guards parameters handler error old_bdu bdu restriction_bdu
Common_static.mvbdu_or_for_guards parameters handler error old_bdu bdu
restriction_bdu
in
let store_result =
Covering_classes_type.AgentRuleCV_setmap.Map.add
Expand Down Expand Up @@ -328,7 +304,8 @@ let collect_proj_bdu_creation_restriction_map parameters handler_bdu error
bdu_true
(fun parameters (error, handler_bdu) bdu bdu' ->
let error, handler_bdu, bdu_union =
mvbdu_and_for_guards parameters handler_bdu error bdu bdu'
Common_static.mvbdu_and_for_guards parameters handler_bdu error bdu
bdu'
in
(error, handler_bdu), bdu_union)
store_bdu_creation_restriction_map
Expand Down Expand Up @@ -569,13 +546,14 @@ let store_bdu_potential_restriction_map_aux parameters handler error
bdu_true
in
let error, handler, bdu_potential_effect_with_guards =
mvbdu_and_for_guards parameters handler error
guard_bdu bdu_potential_effect
Common_static.mvbdu_and_for_guards parameters handler
error guard_bdu bdu_potential_effect
in
(*union of bdu and bdu effect*)
let error, handler, bdu =
mvbdu_or_for_guards parameters handler error bdu
bdu_potential_effect_with_guards restriction_bdu
Common_static.mvbdu_or_for_guards parameters handler
error bdu bdu_potential_effect_with_guards
restriction_bdu
in
error, handler, bdu)
(error, handler, bdu_false)
Expand Down Expand Up @@ -816,8 +794,8 @@ let collect_bdu_test_restriction_map parameters handler error rule_id rule
bdu_true
in
let error, handler, bdu_test_with_guards =
mvbdu_and_for_guards parameters handler error guard_bdu
bdu_test
Common_static.mvbdu_and_for_guards parameters handler error
guard_bdu bdu_test
in
let error, store_result =
( error,
Expand Down Expand Up @@ -859,7 +837,7 @@ let collect_proj_bdu_test_restriction parameters handler_kappa error rule_id
bdu_true
(fun parameters (error, handler) bdu bdu' ->
let error, handler, bdu_union =
mvbdu_and_for_guards parameters handler error bdu bdu'
Common_static.mvbdu_and_for_guards parameters handler error bdu bdu'
in
(error, handler), bdu_union)
store_bdu_test_restriction_map
Expand Down Expand Up @@ -923,11 +901,13 @@ let guard_to_bdu parameters error handler_bdu guard map1 n_guard_p =
association_list
| Kappa_terms.LKappa.Not g1 ->
let error, handler_bdu, mvbdu1 = aux error handler_bdu g1 in
mvbdu_not_for_guards parameters handler_bdu error mvbdu1 bdu_restriction
Common_static.mvbdu_not_for_guards parameters handler_bdu error mvbdu1
bdu_restriction
| Kappa_terms.LKappa.And (g1, g2) ->
let error, handler_bdu, mvbdu1 = aux error handler_bdu g1 in
let error, handler_bdu, mvbdu2 = aux error handler_bdu g2 in
mvbdu_and_for_guards parameters handler_bdu error mvbdu1 mvbdu2
Common_static.mvbdu_and_for_guards parameters handler_bdu error mvbdu1
mvbdu2
| Kappa_terms.LKappa.Or (g1, g2) ->
let error, handler_bdu, mvbdu1 = aux error handler_bdu g1 in
let () =
Expand All @@ -940,8 +920,8 @@ let guard_to_bdu parameters error handler_bdu guard map1 n_guard_p =
in
let () = Ckappa_sig.Views_bdu.print parameters mvbdu2 in
let error, handler, result =
mvbdu_or_for_guards parameters handler_bdu error mvbdu1 mvbdu2
bdu_restriction
Common_static.mvbdu_or_for_guards parameters handler_bdu error mvbdu1
mvbdu2 bdu_restriction
in
let () =
Loggers.fprintf (Remanent_parameters.get_logger parameters) "result\n"
Expand Down
111 changes: 111 additions & 0 deletions core/KaSa_rep/reachability_analysis/common_static.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1094,6 +1094,117 @@ let scan_rule_set parameter error kappa_handler compil =
store_potential_side_effects_per_rule = potential_side_effects_per_rule;
} )

(*****************************************************************************)
(*MVBDU OF THE GUARDS*)
(*****************************************************************************)

(* bdu operations that restrict the values of the guards to 0 and 1*)
(** Returns the disjunction of the two mvbdus but the values of each variable are restricted to the values 0 and 1.
Used for the guard parameters, which model boolean values. *)

let mvbdu_or_for_guards parameters handler_bdu error mvbdu1 mvbdu2
bdu_restriction =
let error, handler_bdu, or_bdu =
Ckappa_sig.Views_bdu.mvbdu_or parameters handler_bdu error mvbdu1 mvbdu2
in
(*all guard parameters must have value 0 or 1*)
Ckappa_sig.Views_bdu.mvbdu_and parameters handler_bdu error or_bdu
bdu_restriction

let mvbdu_and_for_guards parameters handler_bdu error mvbdu1 mvbdu2 =
Ckappa_sig.Views_bdu.mvbdu_and parameters handler_bdu error mvbdu1 mvbdu2

let mvbdu_not_for_guards parameters handler_bdu error mvbdu bdu_restriction =
let error, handler_bdu, not_bdu =
Ckappa_sig.Views_bdu.mvbdu_not parameters handler_bdu error mvbdu
in
(*all guard parameters must have value 0 or 1*)
Ckappa_sig.Views_bdu.mvbdu_and parameters handler_bdu error not_bdu
bdu_restriction

let compute_restriction_mvbdu parameters error mvbdu_handler kappa_handler =
let n_guard_p = Handler.get_nr_guard_parameters kappa_handler in
let guard_p_list = Ckappa_sig.get_list_of_guard_parameters n_guard_p in
let pair_list =
List.map
(fun guard ->
( Ckappa_sig.guard_p_then_site_of_guard guard,
( Some Ckappa_sig.dummy_state_index_false,
Some Ckappa_sig.dummy_state_index_true ) ))
guard_p_list
in
Ckappa_sig.Views_bdu.mvbdu_of_range_list parameters mvbdu_handler error
pair_list

(**Returns the bdu representation of the guard, and a bdu that maps each guard to 1 or 0.
This second bdu is used to restrict the bdus that are calculated by using "or" and "not"
to valid bdus where the values of the guards can only be 0 and 1. *)
let guard_to_bdu parameters error handler_bdu guard bdu_restriction =
let rec aux error handler_bdu guard =
match guard with
| Kappa_terms.LKappa.True ->
Ckappa_sig.Views_bdu.mvbdu_true parameters handler_bdu error
| Kappa_terms.LKappa.False ->
Ckappa_sig.Views_bdu.mvbdu_false parameters handler_bdu error
| Kappa_terms.LKappa.Param a ->
let error, handler_bdu, association_list =
Ckappa_sig.Views_bdu.build_association_list parameters handler_bdu error
[
( Ckappa_sig.guard_p_then_site_of_guard a,
Ckappa_sig.dummy_state_index_true );
]
in
Ckappa_sig.Views_bdu.mvbdu_of_hconsed_asso parameters handler_bdu error
association_list
| Kappa_terms.LKappa.Not g1 ->
let error, handler_bdu, mvbdu1 = aux error handler_bdu g1 in
mvbdu_not_for_guards parameters handler_bdu error mvbdu1 bdu_restriction
| Kappa_terms.LKappa.And (g1, g2) ->
let error, handler_bdu, mvbdu1 = aux error handler_bdu g1 in
let error, handler_bdu, mvbdu2 = aux error handler_bdu g2 in
mvbdu_and_for_guards parameters handler_bdu error mvbdu1 mvbdu2
| Kappa_terms.LKappa.Or (g1, g2) ->
let error, handler_bdu, mvbdu1 = aux error handler_bdu g1 in
let () =
Loggers.fprintf (Remanent_parameters.get_logger parameters) "mvbdu1\n"
in
let () = Ckappa_sig.Views_bdu.print parameters mvbdu1 in
let error, handler_bdu, mvbdu2 = aux error handler_bdu g2 in
let () =
Loggers.fprintf (Remanent_parameters.get_logger parameters) "mvbdu2\n"
in
let () = Ckappa_sig.Views_bdu.print parameters mvbdu2 in
let error, handler, result =
mvbdu_or_for_guards parameters handler_bdu error mvbdu1 mvbdu2
bdu_restriction
in
let () =
Loggers.fprintf (Remanent_parameters.get_logger parameters) "result\n"
in
let () = Ckappa_sig.Views_bdu.print parameters result in
error, handler, result
in
aux error handler_bdu guard

let collect_guard_mvbdus parameters error mvbdu_handler compilation
bdu_restriction =
let error, (mvbdu_handler, guard_mvbdus) =
Ckappa_sig.Rule_nearly_Inf_Int_storage_Imperatif.fold parameters error
(fun parameters error rule_id rule (mvbdu_handler, guard_mvbdus) ->
match rule.Cckappa_sig.e_rule_c_rule.Cckappa_sig.guard with
| None -> error, (mvbdu_handler, guard_mvbdus)
| Some guard ->
let error, mvbdu_handler, bdu =
guard_to_bdu parameters error mvbdu_handler guard bdu_restriction
in
( error,
( mvbdu_handler,
Ckappa_sig.Rule_setmap.Map.add rule_id bdu guard_mvbdus ) ))
compilation.Cckappa_sig.rules
(mvbdu_handler, Ckappa_sig.Rule_setmap.Map.empty)
in
error, mvbdu_handler, guard_mvbdus

(******************************************************************)
(******************************************************************)

Expand Down
Loading

0 comments on commit 959839e

Please sign in to comment.