diff --git a/core/KaSa_rep/reachability_analysis/translation_in_natural_language.ml b/core/KaSa_rep/reachability_analysis/translation_in_natural_language.ml
index 9aa214b17..488c898d7 100644
--- a/core/KaSa_rep/reachability_analysis/translation_in_natural_language.ml
+++ b/core/KaSa_rep/reachability_analysis/translation_in_natural_language.ml
@@ -100,8 +100,6 @@ let try_partitioning parameters handler error
Ckappa_sig.Views_bdu.extensional_of_mvbdu parameters handler error
proj_in
in
- print_string "LENGTH: ";
- print_int (List.length list_asso);
let error =
Exception.check_point Exception.warn parameters error error_4 __POS__
Exit
diff --git a/core/KaSa_rep/reachability_analysis/views_domain.ml b/core/KaSa_rep/reachability_analysis/views_domain.ml
index d14c34b34..46fa36f1a 100644
--- a/core/KaSa_rep/reachability_analysis/views_domain.ml
+++ b/core/KaSa_rep/reachability_analysis/views_domain.ml
@@ -239,6 +239,18 @@ module Domain = struct
let get_site_to_renamed_site_list static error =
let error, result_static = get_bdu_analysis_static static error in
error, result_static.Bdu_static_views.site_to_renamed_site_list
+
+ let get_bdu_guard error static rule_id agent_type cv_id bdu_true =
+ let error, store_guard_bdu = get_store_guard_bdu static error in
+ match Ckappa_sig.Rule_setmap.Map.find_option rule_id store_guard_bdu with
+ | None -> error, bdu_true
+ | Some map_guard_bdu ->
+ (match
+ Covering_classes_type.AgentCV_setmap.Map.find_option
+ (agent_type, cv_id) map_guard_bdu
+ with
+ | None -> error, bdu_true
+ | Some guard_bdu -> error, guard_bdu)
(*--------------------------------------------------------------------*)
type 'a zeroary =
@@ -847,7 +859,10 @@ module Domain = struct
(*build bdu restriction for initial state *)
let bdu_build static dynamic error
- (pair_list : (Ckappa_sig.c_guard_p_then_site * (Ckappa_sig.c_state option * Ckappa_sig.c_state option)) list) =
+ (pair_list :
+ (Ckappa_sig.c_guard_p_then_site
+ * (Ckappa_sig.c_state option * Ckappa_sig.c_state option))
+ list) =
let parameters = get_parameter static in
let handler = get_mvbdu_handler dynamic in
let error, handler, bdu_result =
@@ -895,7 +910,9 @@ module Domain = struct
let error, pair_list =
Ckappa_sig.GuardSite_map_and_set.Map.fold
(fun site' state (error, current_list) ->
- let pair_list = (site', (Some state, Some state)) :: current_list in
+ let pair_list =
+ (site', (Some state, Some state)) :: current_list
+ in
error, pair_list)
map_res (error, [])
in
@@ -904,7 +921,9 @@ module Domain = struct
pair_list
@ List.map
(fun guard ->
- guard, (Some Ckappa_sig.dummy_state_index_false, Some Ckappa_sig.dummy_state_index_true))
+ ( guard,
+ ( Some Ckappa_sig.dummy_state_index_false,
+ Some Ckappa_sig.dummy_state_index_true ) ))
guard_p_list
in
let error, dynamic, bdu_init =
@@ -2548,7 +2567,7 @@ module Domain = struct
(***************************************************************)
let compute_bdu_update_side_effects static dynamic error bdu_test list_a bdu_X
- =
+ bdu_guard =
let parameters = get_parameter static in
let parameter_views =
Remanent_parameters.update_prefix parameters "\t\t\t"
@@ -2563,9 +2582,14 @@ module Domain = struct
Ckappa_sig.Views_bdu.mvbdu_redefine parameter_views handler error
bdu_inter list_a
in
+ (*conjunction with the guard*)
+ let error, handler, bdu_with_guard =
+ Ckappa_sig.Views_bdu.mvbdu_and parameter_views handler error bdu_guard
+ bdu_redefine
+ in
(*do the union of bdu_redefine and bdu_X*)
let error, handler, bdu_result =
- Ckappa_sig.Views_bdu.mvbdu_or parameter_views handler error bdu_redefine
+ Ckappa_sig.Views_bdu.mvbdu_or parameter_views handler error bdu_with_guard
bdu_X
in
let dynamic = set_mvbdu_handler handler dynamic in
@@ -2578,7 +2602,6 @@ module Domain = struct
let error, store_proj_bdu_test_restriction =
get_store_proj_bdu_test_restriction static error
in
- let error, store_guard_bdu = get_store_guard_bdu static error in
let error, proj_bdu_test_restriction =
match
Ckappa_sig.Rule_setmap.Map.find_option rule_id
@@ -2628,17 +2651,7 @@ module Domain = struct
| Some bdu -> error, bdu
in
let error, bdu_guard =
- match
- Ckappa_sig.Rule_setmap.Map.find_option rule_id store_guard_bdu
- with
- | None -> error, bdu_true
- | Some map_guard_bdu ->
- (match
- Covering_classes_type.AgentCV_setmap.Map.find_option
- (agent_type, cv_id) map_guard_bdu
- with
- | None -> error, bdu_true
- | Some guard_bdu -> error, guard_bdu)
+ get_bdu_guard error static rule_id agent_type cv_id bdu_true
in
let error, dynamic, bdu_update =
match
@@ -2680,7 +2693,6 @@ module Domain = struct
| None -> error, Covering_classes_type.AgentCV_setmap.Map.empty
| Some map -> error, map
in
- let error, store_guard_bdu = get_store_guard_bdu static error in
(*-----------------------------------------------------------------------*)
let error, dynamic, event_list =
Covering_classes_type.AgentCV_setmap.Map.fold
@@ -2700,17 +2712,7 @@ module Domain = struct
| error, Some bdu -> error, bdu
in
let error, bdu_guard =
- match
- Ckappa_sig.Rule_setmap.Map.find_option rule_id store_guard_bdu
- with
- | None -> error, bdu_true
- | Some map_guard_bdu ->
- (match
- Covering_classes_type.AgentCV_setmap.Map.find_option
- (agent_type, cv_id) map_guard_bdu
- with
- | None -> error, bdu_true
- | Some guard_bdu -> error, guard_bdu)
+ get_bdu_guard error static rule_id agent_type cv_id bdu_true
in
let error, dynamic, bdu_update =
compute_bdu_update_creation static dynamic error bdu_creation bdu_X
@@ -2770,7 +2772,7 @@ module Domain = struct
in
error, dynamic, (precondition, event_list)
- let apply_one_side_effect static dynamic error _rule_id
+ let apply_one_side_effect static dynamic error rule_id
(_, (agent_name, site, state)) precondition =
let parameters = get_parameter static in
let nr_guard_params =
@@ -2804,6 +2806,7 @@ module Domain = struct
in
let dynamic = set_mvbdu_handler handler dynamic in
let fixpoint_result = get_fixpoint_result dynamic in
+ let error, dynamic, bdu_true = get_mvbdu_true static dynamic error in
let error, dynamic, bdu_false =
get_mvbdu_false static dynamic error
in
@@ -2816,10 +2819,13 @@ module Domain = struct
| error, None -> error, bdu_false
| error, Some bdu -> error, bdu
in
+ let error, bdu_guard =
+ get_bdu_guard error static rule_id agent_name cv_id bdu_true
+ in
let error, dynamic, bdu_update =
(*rTODO add guard bdu*)
compute_bdu_update_side_effects static dynamic error bdu_test
- list_modif bdu_X
+ list_modif bdu_X bdu_guard
in
let error, dynamic, event_list =
add_link ~title:"Dealing with side effects" error static dynamic