make parallel bond / site across bond domains preprocessig incremental

Author: Jérôme FERET

core/KaSa_rep/more_datastructures/map_wrapper.ml

@@ -78,7 +78,7 @@ module type Set_with_logs = sig
   val equal : t -> t -> bool
   val subset : t -> t -> bool
   val iter : (elt -> unit) -> t -> unit
-  val fold : (elt -> 'a -> 'a) -> t -> 'a -> 'a
+  val fold : ?start:elt -> (elt -> 'a -> 'a) -> t -> 'a -> 'a
   val fold_inv : (elt -> 'a -> 'a) -> t -> 'a -> 'a
   val elements : t -> elt list
   val choose : t -> elt option
@@ -354,7 +354,7 @@ module type Map_with_logs = sig
     'b t ->
     Exception.exceptions_caught_and_uncaught
 
-  val fold : (elt -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
+  val fold : ?start:elt -> (elt -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
   val mapi : (elt -> 'a -> 'b) -> 'a t -> 'b t
   val map : ('a -> 'b) -> 'a t -> 'b t
 

core/KaSa_rep/more_datastructures/map_wrapper.mli

@@ -78,7 +78,7 @@ module type Set_with_logs = sig
   val equal : t -> t -> bool
   val subset : t -> t -> bool
   val iter : (elt -> unit) -> t -> unit
-  val fold : (elt -> 'a -> 'a) -> t -> 'a -> 'a
+  val fold : ?start:elt -> (elt -> 'a -> 'a) -> t -> 'a -> 'a
   val fold_inv : (elt -> 'a -> 'a) -> t -> 'a -> 'a
   val elements : t -> elt list
   val choose : t -> elt option
@@ -354,7 +354,7 @@ module type Map_with_logs = sig
     'b t ->
     Exception.exceptions_caught_and_uncaught
 
-  val fold : (elt -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
+  val fold : ?start:elt -> (elt -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
   val mapi : (elt -> 'a -> 'b) -> 'a t -> 'b t
   val map : ('a -> 'b) -> 'a t -> 'b t
 

core/KaSa_rep/reachability_analysis/agents_domain.ml

@@ -415,9 +415,9 @@ module Domain = struct
     in
     error, static, dynamic, modified_agents, []
 
-  let complete_wake_up_relation ?patch _static error wake_up = 
-     let _ = patch in 
-      error, wake_up
+  let complete_wake_up_relation ?patch _static error wake_up =
+    let _ = patch in
+    error, wake_up
 
   (***************************************************************************)
   (*JF: Here, you should add in the event list, each rule that test for an

core/KaSa_rep/reachability_analysis/bdu_static_views.ml

@@ -53,14 +53,15 @@ type bdu_analysis_static = {
     (Ckappa_sig.Views_bdu.mvbdu * Ckappa_sig.Views_bdu.hconsed_association_list)
     Covering_classes_type.AgentSiteCV_setmap.Map.t
     Ckappa_sig.Rule_setmap.Map.t;
-  store_patch_proj_bdu_potential_restriction_map: 
-     (Ckappa_sig.Views_bdu.mvbdu * Ckappa_sig.Views_bdu.hconsed_association_list)
+  store_patch_proj_bdu_potential_restriction_map:
+    (Ckappa_sig.Views_bdu.mvbdu * Ckappa_sig.Views_bdu.hconsed_association_list)
     Covering_classes_type.AgentSiteCV_setmap.Map.t
     Ckappa_sig.Rule_setmap.Map.t;
   store_proj_bdu_test_restriction:
     Ckappa_sig.Views_bdu.mvbdu Covering_classes_type.AgentsCV_setmap.Map.t
     Ckappa_sig.Rule_setmap.Map.t;
-    store_patch_proj_bdu_test_restriction: Ckappa_sig.Views_bdu.mvbdu Covering_classes_type.AgentsCV_setmap.Map.t
+  store_patch_proj_bdu_test_restriction:
+    Ckappa_sig.Views_bdu.mvbdu Covering_classes_type.AgentsCV_setmap.Map.t
     Ckappa_sig.Rule_setmap.Map.t;
   site_to_renamed_site_list:
     (Covering_classes_type.cv_id * Ckappa_sig.c_mvbdu_var) list
@@ -92,7 +93,7 @@ let init_bdu_analysis_static parameters error =
       store_patch_proj_bdu_test_restriction = Ckappa_sig.Rule_setmap.Map.empty;
       store_patch_proj_bdu_potential_restriction_map =
         Ckappa_sig.Rule_setmap.Map.empty;
-  site_to_renamed_site_list = init_site_to_renamed_site_list;
+      site_to_renamed_site_list = init_site_to_renamed_site_list;
     }
   in
   error, init_bdu_analysis_static
@@ -670,9 +671,8 @@ let collect_site_to_renamed_site_list parameters error store_remanent_triple
 (**************************************************************************)
 (*projection with rule_id*)
 
-let collect_proj_bdu_potential_restriction_map 
-    ~patch_store_remanent_triple parameters bdu_handler error
-    store_potential_side_effects  guard_mvbdus =
+let collect_proj_bdu_potential_restriction_map ~patch_store_remanent_triple
+    parameters bdu_handler error store_potential_side_effects guard_mvbdus =
   let store_init_bdu_potential_restriction_map =
     Covering_classes_type.AgentSiteRuleCV_setmap.Map.empty
   in
@@ -871,8 +871,8 @@ let collect_bdu_test_restriction_map ?start_cv ~new_rule ~modified_agents
 
 let collect_proj_bdu_test_restriction ?start_cv ~new_rule ~modified_agents
     parameters handler_kappa error rule_id rule
-    (*store_new_index_pair_map*) store_remanent_triple (store_result, patch_store_result) 
-    store_guard_bdu =
+    (*store_new_index_pair_map*) store_remanent_triple
+    (store_result, patch_store_result) store_guard_bdu =
   let store_init_bdu_test_restriction_map =
     Covering_classes_type.AgentsRuleCV_setmap.Map.empty
   in
@@ -903,7 +903,7 @@ let collect_proj_bdu_test_restriction ?start_cv ~new_rule ~modified_agents
     Ckappa_sig.Rule_setmap.Map.fold Ckappa_sig.Rule_setmap.Map.add store_result'
       store_result
   in
-   let patch_store_result =
+  let patch_store_result =
     Ckappa_sig.Rule_setmap.Map.fold Ckappa_sig.Rule_setmap.Map.add store_result'
       patch_store_result
   in
@@ -939,12 +939,14 @@ let scan_rule_static ?start_cv ~new_rule ~modified_agents parameters log_info
         store_result.store_patch_modif_list_restriction_map )
   in
   (*------------------------------------------------------------------------*)
-  let (error, handler_bdu), (store_proj_bdu_test_restriction, store_patch_proj_bdu_test_restriction) =
+  let ( (error, handler_bdu),
+        (store_proj_bdu_test_restriction, store_patch_proj_bdu_test_restriction)
+      ) =
     collect_proj_bdu_test_restriction ?start_cv ~new_rule ~modified_agents
       parameters handler_bdu error rule_id rule store_remanent_triple
-      (store_result.store_proj_bdu_test_restriction, 
-       store_result.store_patch_proj_bdu_test_restriction)
-        guard_mvbdus
+      ( store_result.store_proj_bdu_test_restriction,
+        store_result.store_patch_proj_bdu_test_restriction )
+      guard_mvbdus
   in
   (*------------------------------------------------------------------------*)
   let error, log_info =
@@ -960,7 +962,7 @@ let scan_rule_static ?start_cv ~new_rule ~modified_agents parameters log_info
       store_proj_bdu_creation_restriction_map;
       store_modif_list_restriction_map;
       store_patch_modif_list_restriction_map;
-      store_patch_proj_bdu_test_restriction; 
+      store_patch_proj_bdu_test_restriction;
       store_proj_bdu_test_restriction;
     } )
 
@@ -978,14 +980,11 @@ let scan_rule_set ?start ?start_cv ~patch_store_remanent_triple ~modified_agents
     parameters log_info handler_bdu error handler_kappa compiled
     store_potential_side_effects store_remanent_triple guard_mvbdus init =
   let nsites = Handler.get_nsites handler_kappa in
-  let (error, handler_bdu), store_patch_proj_bdu_potential_restriction_map  =
-    collect_proj_bdu_potential_restriction_map 
-      ~patch_store_remanent_triple parameters handler_bdu error
-      store_potential_side_effects 
-      guard_mvbdus
+  let (error, handler_bdu), store_patch_proj_bdu_potential_restriction_map =
+    collect_proj_bdu_potential_restriction_map ~patch_store_remanent_triple
+      parameters handler_bdu error store_potential_side_effects guard_mvbdus
   in
-  let init = { init with 
-  store_patch_proj_bdu_potential_restriction_map} in
+  let init = { init with store_patch_proj_bdu_potential_restriction_map } in
 
   let error, (handler_bdu, log_info, store_results) =
     Ckappa_sig.Rule_nearly_Inf_Int_storage_Imperatif.fold_two_steps ?start

core/KaSa_rep/reachability_analysis/counters_domain.ml

@@ -195,16 +195,16 @@ functor
        these tuples, and apply the function Common_static.add_dependency_site_rule
        to update the wake_up relation *)
     let complete_wake_up_relation ?patch static error wake_up =
-      let start = 
-        match patch with 
-          | None -> Ckappa_sig.rule_id_of_int 0 
-          | Some a -> a.Diff.next_rule 
-      in 
+      let start =
+        match patch with
+        | None -> Ckappa_sig.rule_id_of_int 0
+        | Some a -> a.Diff.next_rule
+      in
       let parameters = get_parameter static in
       let rule_restriction = get_rule_restriction static in
       let packs = get_packs static in
-      Ckappa_sig.Rule_id_quick_nearly_Inf_Int_storage_Imperatif.fold ~start parameters
-        error
+      Ckappa_sig.Rule_id_quick_nearly_Inf_Int_storage_Imperatif.fold ~start
+        parameters error
         (fun parameters error rule_id agent_map wake_up ->
           let error, rule = get_rule parameters error static rule_id in
           match rule with

core/KaSa_rep/reachability_analysis/dynamic_contact_map_domain.ml

@@ -147,8 +147,9 @@ module Domain = struct
       modified_agents,
       [] )
 
-  let complete_wake_up_relation ?patch _static error wake_up =  let _ = patch in 
-  error, wake_up
+  let complete_wake_up_relation ?patch _static error wake_up =
+    let _ = patch in
+    error, wake_up
 
   (**************************************************************************)
 

core/KaSa_rep/reachability_analysis/parallel_bonds.ml

@@ -521,9 +521,9 @@ module Domain = struct
     in
     error, static, dynamic, modified_agents, []
 
-  let add_rules_tuples_into_wake_up_relation parameters error rule_tuples
+  let add_rules_tuples_into_wake_up_relation ?start parameters error rule_tuples
       wake_up =
-    Ckappa_sig.Rule_map_and_set.Map.fold
+    Ckappa_sig.Rule_map_and_set.Map.fold ?start
       (fun rule_id map (error, wake_up) ->
         Parallel_bonds_type.PairAgentsSiteState_map_and_set.Map.fold
           (fun _ list (error, wake_up) ->
@@ -552,9 +552,9 @@ module Domain = struct
           map (error, wake_up))
       rule_tuples (error, wake_up)
 
-  let add_rules_tuples_into_wake_up_relation' parameters error store_map wake_up
-      =
-    Ckappa_sig.Rule_map_and_set.Map.fold
+  let add_rules_tuples_into_wake_up_relation' ?start parameters error store_map
+      wake_up =
+    Ckappa_sig.Rule_map_and_set.Map.fold ?start
       (fun rule_id map (error, wake_up) ->
         Parallel_bonds_type.PairAgentsSitesStates_map_and_set.Map.fold
           (fun ( _,
@@ -585,7 +585,11 @@ module Domain = struct
      these tuples, and apply the function Common_static.add_dependency_site_rule
      to update the wake_up relation *)
   let complete_wake_up_relation ?patch static error wake_up =
-     let _ = patch in 
+    let start =
+      match patch with
+      | None -> None
+      | Some a -> Some a.Diff.next_rule
+    in
     let parameters = get_parameter static in
     (*fst site created a parallel bonds*)
     (* TO DO make this incremental *)
@@ -600,21 +604,21 @@ module Domain = struct
     in
     (*----------------------------------------------------*)
     let error, wake_up =
-      add_rules_tuples_into_wake_up_relation' parameters error
+      add_rules_tuples_into_wake_up_relation' ?start parameters error
         store_rule_double_bonds_rhs wake_up
     in
     let error, wake_up =
-      add_rules_tuples_into_wake_up_relation' parameters error
+      add_rules_tuples_into_wake_up_relation' ?start parameters error
         store_rule_double_bonds_lhs wake_up
     in
     (*----------------------------------------------------*)
     let error, wake_up =
-      add_rules_tuples_into_wake_up_relation parameters error
+      add_rules_tuples_into_wake_up_relation ?start parameters error
         store_fst_site_create_parallel_bonds_rhs wake_up
     in
     (*----------------------------------------------------*)
     let error, wake_up =
-      add_rules_tuples_into_wake_up_relation parameters error
+      add_rules_tuples_into_wake_up_relation ?start parameters error
         store_snd_site_create_parallel_bonds_rhs wake_up
     in
     error, wake_up

core/KaSa_rep/reachability_analysis/product.ml

@@ -102,8 +102,8 @@ module Product
 
   let complete_wake_up_relation ?patch static error wake_up =
     let error, wake_up =
-      Underlying_domain.complete_wake_up_relation ?patch static.underlying_domain error
-        wake_up
+      Underlying_domain.complete_wake_up_relation ?patch
+        static.underlying_domain error wake_up
     in
     New_domain.complete_wake_up_relation ?patch static.new_domain error wake_up
 

core/KaSa_rep/reachability_analysis/rules_domain.ml

@@ -248,9 +248,9 @@ module Domain = struct
       modified_agents,
       [] )
 
-  let complete_wake_up_relation ?patch _static error wake_up = 
-     let _ = patch in 
-      error, wake_up
+  let complete_wake_up_relation ?patch _static error wake_up =
+    let _ = patch in
+    error, wake_up
 
   let add_initial_state ~new_init ?patch ?modified_agents _static dynamic error
       _species =

core/KaSa_rep/reachability_analysis/side_effects_domain.ml

@@ -143,8 +143,9 @@ module Domain = struct
       modified_agents,
       [] )
 
-  let complete_wake_up_relation ?patch _static error wake_up = 
-    let _ = patch in error, wake_up
+  let complete_wake_up_relation ?patch _static error wake_up =
+    let _ = patch in
+    error, wake_up
 
   let add_initial_state ~new_init ?patch ?modified_agents _static dynamic error
       _species =