reuse the contact map or the separating transitions if already computed

Author: Jérôme FERET

core/KaSa_rep/export/export.ml

@@ -659,7 +659,12 @@ functor
 
     let get_reachability_analysis =
       get_gen ~log_title:"Reachability analysis"
-        Remanent_state.get_reachability_result compute_reachability_result
+        (fun state ->
+          if Remanent_state.is_reachability_result_available state then
+            Remanent_state.get_reachability_result state
+          else
+            None)
+        compute_reachability_result
 
     let output_reachability_result state =
       let error = Remanent_state.get_errors state in
@@ -1373,8 +1378,7 @@ functor
         (Remanent_state.get_internal_contact_map Public_data.Low)
         compute_raw_internal_contact_map
 
-    let compute_intermediary_internal_contact_map show_title state =
-      let state, _ = compute_reachability_result show_title state in
+    let compute_intermediary_internal_contact_map _show_title state =
       let state, _ = get_reachability_analysis state in
       match
         Remanent_state.get_internal_contact_map Public_data.Medium state
@@ -2057,7 +2061,6 @@ functor
         Remanent_parameters.set_compute_separating_transitions parameters true
       in
       let state' = set_parameters parameters' state in
-      let state', _ = compute_reachability_result _show_title state' in
       let state', _ = get_reachability_analysis state' in
       let state = set_parameters parameters state' in
       match Remanent_state.get_separating_transitions state with

core/KaSa_rep/remanent_state/remanent_state.ml

@@ -218,6 +218,7 @@ type ('global_static, 'static, 'dynamic) state = {
   bdu_handler: Mvbdu_wrapper.Mvbdu.handler;
   reachability_state:
     ('global_static, 'static, 'dynamic) reachability_result option;
+  is_reachability_result_available: bool;
   subviews_info: subviews_info option;
   dead_rules: dead_rules option;
   conditionally_dead_rules: rule_deadness_conditions option;
@@ -300,6 +301,7 @@ let create_state ?errors ?env ?init_state ?reset parameters init =
     transition_system_length = None;
     patch = None;
     global_static_information = None;
+    is_reachability_result_available = false;
   }
 
 (**************)
@@ -661,7 +663,11 @@ let get_scc_decomposition accuracy accuracy' state =
 let get_reachability_result state = state.reachability_state
 
 let set_reachability_result reachability_state state =
-  { state with reachability_state = Some reachability_state }
+  {
+    state with
+    reachability_state = Some reachability_state;
+    is_reachability_result_available = true;
+  }
 
 let get_dead_rules state = state.dead_rules
 
@@ -784,8 +790,12 @@ let reset_reachability_memoized_values state =
     scc_decomposition = Public_data.AccuracyMap.empty;
     signature = None;
     constraint_list = None;
+    is_reachability_result_available = false;
   }
 
+let is_reachability_result_available state =
+  state.is_reachability_result_available
+
 let set_handler_opt h_opt state =
   match h_opt with
   | None -> state

core/KaSa_rep/remanent_state/remanent_state.mli

@@ -495,6 +495,9 @@ val get_working_set_elements :
 val reset_reachability_memoized_values :
   ('global, 'static, 'compile) state -> ('global, 'static, 'compile) state
 
+val is_reachability_result_available :
+  ('global, 'static, 'compile) state -> bool
+
 val rename_pos :
   ( Remanent_parameters_sig.parameters,
     Exception.exceptions_caught_and_uncaught,