add guard also to bdu_creation

Kappa-Dev · Jan 21, 2025 · 82c124d · 82c124d
1 parent 03412de
commit 82c124d
Show file tree

Hide file tree

Showing 2 changed files with 37 additions and 33 deletions.
diff --git 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
@@ -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