fix bugs when printing: add -1 for thesold and check if mvbdu is true

Author: reb-ddm

core/KaSa_rep/reachability_analysis/translation_in_natural_language.ml

@@ -249,7 +249,7 @@ let try_partitioning parameters handler error
 
 let translate parameters handler error (rename_site_inverse : rename_sites)
     mvbdu nsites restriction_bdu =
-  let threshold = Ckappa_sig.int_of_site_name nsites in
+  let threshold = Ckappa_sig.int_of_site_name nsites - 1 in
   let error, handler, list =
     Ckappa_sig.Views_bdu.parametric_conditions_of_mvbdu parameters handler error
       ~threshold mvbdu
@@ -295,11 +295,10 @@ let translate parameters handler error (rename_site_inverse : rename_sites)
       List.fold_left
         (fun (error, list) elt ->
           let error, elt = rename_site_inverse parameters error elt in
-          error, elt :: list)
         (* keep only the sites and not the guards, because the guards are contained in the mvbdu and all mvbdus are true *)
-        (* match Ckappa_sig.site_or_guard_p_of_mvbdu_var elt nsites with
+        match Ckappa_sig.site_or_guard_p_of_mvbdu_var elt nsites with
            | Site _ -> error, elt :: list
-           | Guard_p _ -> error, list) *)
+           | Guard_p _ -> error, list)
         (error, [])
         (List.rev var_list)
     in
@@ -796,6 +795,16 @@ let rec print ?beginning_of_sentence:(beggining = true)
       in
       error, bdu_handler
     | Valuations_with_guards valuations ->
+      let error =
+        Site_graphs.KaSa_site_graph.print log parameters error t
+      in
+      let () = Loggers.fprintf log " => " in
+      let should_use_bracket =
+        match valuations with
+        | [] | [ _ ] -> false
+        | _ :: _ -> true
+      in
+      let () = if should_use_bracket then Loggers.fprintf log "[ " in
       let error, _bool, bdu_handler =
         List.fold_left
           (fun (error, bool, bdu_handler) (sites, mvbdu) ->
@@ -831,6 +840,7 @@ let rec print ?beginning_of_sentence:(beggining = true)
           (error, false, bdu_handler)
           valuations
       in
+      let () = if should_use_bracket then Loggers.fprintf log " ]" in
       let () = Loggers.print_newline log in
       error, bdu_handler
     | No_known_translation list ->

core/KaSa_rep/reachability_analysis/views_domain.ml

@@ -758,14 +758,14 @@ module Domain = struct
       (*this is a function to convert a bdu of diff into a list.
         return a pair: (bdu, and a pair of (site, state) list of list)*)
       let handler = get_mvbdu_handler dynamic in
-      let nsites = Ckappa_sig.int_of_site_name (get_nsites static) in
+      let threshold = Ckappa_sig.int_of_site_name (get_nsites static) - 1 in
       let error, handler, list =
         Ckappa_sig.Views_bdu.extensional_of_mvbdu parameters handler error
           bdu_diff
       in
       let error, handler, split_list =
         Ckappa_sig.Views_bdu.parametric_conditions_of_mvbdu parameters handler
-          error ~threshold:nsites bdu_diff
+          error ~threshold:threshold bdu_diff
       in
       let _ = split_list in
 
@@ -3190,6 +3190,10 @@ module Domain = struct
             (*-----------------------------------------------------------*)
             Wrapped_modules.LoggedIntMap.fold
               (fun _ mvbdu (error, (handler, list)) ->
+                let error, handler, is_true = Ckappa_sig.mvbdu_is_true_for_guards parameters handler error mvbdu restriction_bdu in
+                if is_true then
+                  (error, (handler, list))
+              else
                 let error, handler =
                   if local_trace || Remanent_parameters.get_trace parameters
                   then (