renamed guards to the corrrect index in the mvbdu and printed the val…

…ue of the guard parameters

core/KaSa_rep/frontend/ckappa_sig.ml

@@ -186,6 +186,7 @@ let next_link_value (i : c_link_value) : c_link_value = i + 1
 let site_name_of_int (a : int) : c_site_name = a
 let int_of_site_name (a : c_site_name) : int = a
 let string_of_site_name (a : c_site_name) : string = string_of_int a
+let string_of_guard_p_then_site (a : c_guard_p_then_site) : string = string_of_int a
 
 let string_of_site_or_guard (a : c_site_or_guard_p) : string =
   match a with

core/KaSa_rep/frontend/ckappa_sig.mli

@@ -67,6 +67,7 @@ val site_name_of_int : int -> c_site_name
 val int_of_site_name : c_site_name -> int
 val string_of_site_name : c_site_name -> string
 val string_of_site_or_guard : c_site_or_guard_p -> string
+val string_of_guard_p_then_site : c_guard_p_then_site -> string
 val state_index_of_int : int -> c_state
 val int_of_state_index : c_state -> int
 val string_of_state_index : c_state -> string

core/KaSa_rep/frontend/handler.ml

@@ -587,8 +587,18 @@ let string_of_site parameter error handler_kappa ?state
   in
   error, print_site parameter ?state ~add_parentheses site_type
 
-let string_of_guard g guard_params error =
-  error, List.nth guard_params (Ckappa_sig.int_of_guard_parameter g)
+let string_of_guard g guard_params ?state error =
+  let guard_param_name =
+    List.nth guard_params (Ckappa_sig.int_of_guard_parameter g)
+  in
+  match state with
+  | None -> error, guard_param_name
+  | Some s ->
+    (match Ckappa_sig.int_of_state_index s with
+    | 0 -> error, guard_param_name ^ "{false}"
+    | 1 -> error, guard_param_name ^ "{true}"
+    | _ -> error, guard_param_name ^ "{undefined}")
+
 (*rTODO error handling*)
 
 let string_of_site_or_guard parameter error handler_kappa ?state
@@ -598,7 +608,7 @@ let string_of_site_or_guard parameter error handler_kappa ?state
     string_of_site parameter error handler_kappa ?state ~add_parentheses
       agent_type s
   | Ckappa_sig.Guard_p g ->
-    string_of_guard g handler_kappa.Cckappa_sig.guard_parameters error
+    string_of_guard g handler_kappa.Cckappa_sig.guard_parameters ?state error
 
 (*this function used in views_domain*)
 let string_of_site_update_views parameter error handler_kappa agent_type

core/KaSa_rep/reachability_analysis/bdu_static_views.ml

@@ -53,7 +53,9 @@ type bdu_analysis_static = {
   store_proj_bdu_test_restriction:
     Ckappa_sig.Views_bdu.mvbdu Covering_classes_type.AgentsCV_setmap.Map.t
     Ckappa_sig.Rule_setmap.Map.t;
-  store_guard_bdu: Ckappa_sig.Views_bdu.mvbdu Ckappa_sig.Rule_setmap.Map.t;
+  store_guard_bdu:
+    Ckappa_sig.Views_bdu.mvbdu Covering_classes_type.AgentCV_setmap.Map.t
+    Ckappa_sig.Rule_setmap.Map.t;
   site_to_renamed_site_list:
     (Covering_classes_type.cv_id * Ckappa_sig.c_guard_p_then_site) list
     Ckappa_sig
@@ -160,38 +162,54 @@ let get_pair_cv_map_with_missing_association_creation parameters error agent
         to_site_or_guard_map parameters error agent.Cckappa_sig.agent_interface
       in
       (*----------------------------------------------------*)
-      let error', map_res =
+      let error', (map_res, renamed_guard_params_list) =
         try
           Ckappa_sig.SiteOrGuard_map_and_set.Map
           .fold_restriction_with_missing_associations parameters error
-            (fun site port m ->
+            (fun site port (error, (m, r_guardp_list)) ->
               match
                 ( port.Cckappa_sig.site_state.Cckappa_sig.min,
                   port.Cckappa_sig.site_state.Cckappa_sig.max )
               with
               | Some a, Some b when a = b ->
-                add_dependency_site parameters map_new_index_forward site a
-                  nr_guard_params m
+                let error, m =
+                  add_dependency_site parameters map_new_index_forward site a
+                    nr_guard_params (error, m)
+                in
+                error, (m, r_guardp_list)
               | Some _, Some _ | None, _ | _, None -> raise Exit)
-            (fun site ->
+            (fun site (error, (m, r_guardp_list)) ->
               match site with
               | Ckappa_sig.Site _ ->
-                add_dependency_site parameters map_new_index_forward site
-                  Ckappa_sig.dummy_state_index nr_guard_params
+                let error, m =
+                  add_dependency_site parameters map_new_index_forward site
+                    Ckappa_sig.dummy_state_index nr_guard_params (error, m)
+                in
+                error, (m, r_guardp_list)
               | Ckappa_sig.Guard_p _ ->
-                add_dependency_site parameters map_new_index_forward site
-                  Ckappa_sig.dummy_state_index_true nr_guard_params
-              (*rTODO does that mean that all parameters are true?*))
-            set agent_interface Ckappa_sig.GuardSite_map_and_set.Map.empty
+                let error, guard_p' =
+                  match
+                    Ckappa_sig.SiteOrGuard_map_and_set.Map.find_option
+                      parameters error site map_new_index_forward
+                  with
+                  | error, None ->
+                    Exception.warn parameters error __POS__ Exit
+                      (Ckappa_sig.guard_p_then_site_of_site
+                         Ckappa_sig.dummy_site_name nr_guard_params)
+                  | error, Some s -> error, s
+                in
+                error, (m, guard_p' :: r_guardp_list))
+            set agent_interface
+            (Ckappa_sig.GuardSite_map_and_set.Map.empty, [])
         with Exit ->
           Exception.warn parameters error __POS__ Exit
-            Ckappa_sig.GuardSite_map_and_set.Map.empty
+            (Ckappa_sig.GuardSite_map_and_set.Map.empty, [])
       in
       let error =
         Exception.check_point Exception.warn parameters error error' __POS__
           Exit
       in
-      error, (cv_id, map_res) :: current_list)
+      error, (cv_id, map_res, renamed_guard_params_list) :: current_list)
     (error, []) triple_list
 
 let collect_bdu_creation_restriction_map parameters handler error rule_id rule
@@ -225,7 +243,7 @@ let collect_bdu_creation_restriction_map parameters handler error rule_id rule
               (*fold a list and get a pair of site and state and rule_id*)
               let error, handler, store_result =
                 List.fold_left
-                  (fun (error, handler, store_result) (cv_id, map_res) ->
+                  (fun (error, handler, store_result) (cv_id, map_res, _) ->
                     let pair_list =
                       Ckappa_sig.GuardSite_map_and_set.Map.fold
                         (fun site' state current_list ->
@@ -808,55 +826,85 @@ let collect_proj_bdu_test_restriction parameters handler_kappa handler error
   (error, handler), store_result
 
 (***************************************************************************)
+let rename_guard_to_mvbdu_indexing parameters error guard map1 =
+  let guard = Ckappa_sig.guard_p_then_site_of_guard guard in
+  match
+    Ckappa_sig.GuardPOrSite_nearly_Inf_Int_storage_Imperatif.get parameters
+      error guard map1
+  with
+  | error, Some g -> error, g
+  | error, None ->
+    Exception.warn parameters error __POS__ Exit
+      (Ckappa_sig.guard_p_then_site_of_site Ckappa_sig.dummy_site_name 0)
 
-let rec guard_to_bdu parameters error handler_bdu guard =
+let rec guard_to_bdu parameters error handler_bdu guard map1 =
   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 =
+      let error, renamed_guard =
+        rename_guard_to_mvbdu_indexing parameters error a map1
+      in
       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 );
-        ]
+        [ renamed_guard, 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 =
-      guard_to_bdu parameters error handler_bdu g1
+      guard_to_bdu parameters error handler_bdu g1 map1
     in
     Ckappa_sig.Views_bdu.mvbdu_not parameters handler_bdu error mvbdu1
   | Kappa_terms.LKappa.And (g1, g2) ->
     let error, handler_bdu, mvbdu1 =
-      guard_to_bdu parameters error handler_bdu g1
+      guard_to_bdu parameters error handler_bdu g1 map1
     in
     let error, handler_bdu, mvbdu2 =
-      guard_to_bdu parameters error handler_bdu g2
+      guard_to_bdu parameters error handler_bdu g2 map1
     in
     Ckappa_sig.Views_bdu.mvbdu_and parameters handler_bdu error mvbdu1 mvbdu2
   | Kappa_terms.LKappa.Or (g1, g2) ->
     let error, handler_bdu, mvbdu1 =
-      guard_to_bdu parameters error handler_bdu g1
+      guard_to_bdu parameters error handler_bdu g1 map1
     in
     let error, handler_bdu, mvbdu2 =
-      guard_to_bdu parameters error handler_bdu g2
+      guard_to_bdu parameters error handler_bdu g2 map1
     in
     Ckappa_sig.Views_bdu.mvbdu_or parameters handler_bdu error mvbdu1 mvbdu2
 
 let collect_guard_bdu parameters handler_bdu error rule_id rule store_guard_bdu
-    =
+    site_correspondence =
   match rule.Cckappa_sig.guard with
   | None -> (error, handler_bdu), store_guard_bdu
   | Some guard ->
-    let error, handler_bdu, bdu =
-      guard_to_bdu parameters error handler_bdu guard
+    let error, (handler_bdu, map_guard_bdu) =
+      Ckappa_sig.Agent_type_quick_nearly_Inf_Int_storage_Imperatif.fold
+        parameters error
+        (fun parameters error agent site_correspondence
+             (handler_bdu, map_guard_bdu) ->
+          let error, (handler_bdu, map_guard_bdu) =
+            Covering_classes_type.Cv_id_nearly_Inf_Int_storage_Imperatif.fold
+              parameters error
+              (fun parameters error cv_id (map1, _) (handler_bdu, map_guard_bdu) ->
+                let error, handler_bdu, bdu =
+                  guard_to_bdu parameters error handler_bdu guard map1
+                in
+                ( error,
+                  ( handler_bdu,
+                    Covering_classes_type.AgentCV_setmap.Map.add (agent, cv_id)
+                      bdu map_guard_bdu ) ))
+              site_correspondence
+              (handler_bdu, map_guard_bdu)
+          in
+          error, (handler_bdu, map_guard_bdu))
+        site_correspondence
+        (handler_bdu, Covering_classes_type.AgentCV_setmap.Map.empty)
     in
     ( (error, handler_bdu),
-      Ckappa_sig.Rule_setmap.Map.add rule_id bdu store_guard_bdu )
+      Ckappa_sig.Rule_setmap.Map.add rule_id map_guard_bdu store_guard_bdu )
 
 (***************************************************************************)
 
@@ -903,7 +951,8 @@ let collect_proj_bdu_test_restriction_pattern parameters error
 let scan_rule_static parameters log_info error handler_kappa handler_bdu
     (rule_id : Ckappa_sig.c_rule_id) rule
     (*store_new_index_pair_map*)
-      store_remanent_triple store_potential_side_effects _compil store_result =
+      store_remanent_triple store_potential_side_effects _compil store_result
+    site_correspondence =
   (*-----------------------------------------------------------------------*)
   (*pre_static*)
   let error, log_info =
@@ -944,7 +993,7 @@ let scan_rule_static parameters log_info error handler_kappa handler_bdu
   (*------------------------------------------------------------------------*)
   let (error, handler_bdu), store_guard_bdu =
     collect_guard_bdu parameters handler_bdu error rule_id rule
-      store_result.store_guard_bdu
+      store_result.store_guard_bdu site_correspondence
   in
   (*------------------------------------------------------------------------*)
   let error, log_info =
@@ -967,7 +1016,7 @@ let scan_rule_static parameters log_info error handler_kappa handler_bdu
 (***************************************************************************)
 
 let scan_rule_set parameters log_info handler_bdu error handler_kappa compiled
-    store_potential_side_effects store_remanent_triple =
+    store_potential_side_effects store_remanent_triple site_correspondence =
   let error, init = init_bdu_analysis_static parameters error in
   let nr_guard_params =
     Covering_classes_main.get_nr_guard_parameters handler_kappa
@@ -979,6 +1028,7 @@ let scan_rule_set parameters log_info handler_bdu error handler_kappa compiled
           scan_rule_static parameters log_info error handler_kappa handler_bdu
             rule_id rule.Cckappa_sig.e_rule_c_rule store_remanent_triple
             store_potential_side_effects compiled store_result
+            site_correspondence
         in
         error, (handler_bdu, log_info, store_result))
       compiled.Cckappa_sig.rules

core/KaSa_rep/reachability_analysis/translation_in_natural_language.ml

@@ -18,6 +18,9 @@ let _ = trace
 let get_nr_guard_parameters kappa_handler =
   kappa_handler.Cckappa_sig.nguard_params
 
+let get_guard_parameters kappa_handler =
+  kappa_handler.Cckappa_sig.guard_parameters
+
 type token =
   (*rTODO maybe change this*)
   | Range of Ckappa_sig.c_guard_p_then_site * Ckappa_sig.c_state list
@@ -444,14 +447,34 @@ let rec print ?beginning_of_sentence:(beggining = true)
   in
   let log = Remanent_parameters.get_logger parameters in
   let nr_guard_params = get_nr_guard_parameters handler_kappa in
+  let guard_parameters = get_guard_parameters handler_kappa in
   let error, () =
     match translation with
     | Range (site_type, state_list) ->
       (match
          Ckappa_sig.site_or_guard_p_of_guard_p_then_site site_type
            nr_guard_params
        with
-      | Guard_p _ -> error, () (*rTODO print guards*)
+      | Guard_p guard_param ->
+        let guard_p_string =
+          List.nth guard_parameters
+            (Ckappa_sig.int_of_guard_parameter guard_param)
+          (*rTODO error handling*)
+        in
+        let state_list_string =
+          List.map
+            (fun s ->
+              match Ckappa_sig.int_of_state_index s with
+              | 0 -> "false"
+              | 1 -> "true"
+              | _ -> "(error: guard_state > 1)")
+            state_list
+        in
+        Loggers.fprintf log "DDM%s{%s}" guard_p_string
+          (List.fold_left
+             (fun string state -> string ^ ", " ^ state)
+             "" state_list_string);
+        error, () (*rTODO print guards*)
       | Site site_type ->
         if dim_min <= 1 then (
           match Remanent_parameters.get_backend_mode parameters with