project away the Boolean parameters for removed rules

Author: Jérôme FERET

core/KaSa_rep/export/export.ml

@@ -2545,39 +2545,39 @@ functor
       let state = set_errors errors state in
       state, id_opt
 
-    let permanently_disable_rule_c_id_list list state =
-      let state, l =
+    let permanently_disable_rule_c_id_list list state acc =
+      let state, l, l' =
         List.fold_left
-          (fun (state, l) index ->
+          (fun (state, l, l') index ->
             let state, id_opt = working_set_id_of_rule_id index state in
             match id_opt with
-            | None -> state, l
-            | Some i -> state, i :: l)
-          (state, []) (List.rev list)
+            | None -> state, l, l'
+            | Some i -> state, i :: l, i::l')
+          (state, acc, []) (List.rev list)
       in
       let error = get_errors state in
       let error, state, _ =
-        toggle_working_set_boolean_parameters_in_compilation error false state l
+        toggle_working_set_boolean_parameters_in_compilation error false state l'
           true
       in
-      set_errors error state
+      set_errors error state, l 
 
-    let permanently_disable_init_c_id_list list state =
-      let state, l =
+    let permanently_disable_init_c_id_list list state acc =
+      let state, l, l' =
         List.fold_left
-          (fun (state, l) index ->
+          (fun (state, l, l') index ->
             let state, id_opt = working_set_id_of_init_id index state in
             match id_opt with
-            | None -> state, l
-            | Some i -> state, i :: l)
-          (state, []) (List.rev list)
+            | None -> state, l, l'
+            | Some i -> state, i :: l, i::l')
+          (state, acc,[]) (List.rev list)
       in
       let error = get_errors state in
       let error, state, _ =
-        toggle_working_set_boolean_parameters_in_compilation error false state l
+        toggle_working_set_boolean_parameters_in_compilation error false state l'
           true
       in
-      set_errors error state
+      set_errors error state, l 
 
     (* Incremental analysis *)
     let summarize_from_ast state =
@@ -2622,6 +2622,118 @@ functor
           (Remanent_state.set_handler handler state),
         state' )
 
+
+        (*  let state, c_compil = get_c_compilation state in
+      let rec toggle_parameters = function
+        | [] ->
+          ( error,
+            compilation.Ast.working_set_values,
+            c_compil.Cckappa_sig.working_set_valuations,
+            false )
+        | working_set_index :: indexes ->
+          let error, working_set_values, working_set_valuations, changed =
+            toggle_parameters indexes
+          in
+          let guard_int =
+            Ckappa_sig.int_of_working_set_index working_set_index
+          in
+          (match Mods.IntMap.find_option guard_int working_set_values with
+          | None ->
+            if permanently_disable then
+              error, working_set_values, working_set_valuations, changed
+            else (
+              let error, () =
+                Exception.warn parameters error __POS__
+                  ~message:
+                    ("Index out of bounds: there is no rule with index "
+                    ^ Ckappa_sig.string_of_working_set_index working_set_index
+                    ^ " in the working set. Or it may already have been \
+                       permanently disabled.")
+                  Exit ()
+              in
+              error, working_set_values, working_set_valuations, false
+            )
+          | Some old_bool ->
+            if old_bool = bool && not permanently_disable then
+              error, working_set_values, working_set_valuations, changed
+            else (
+              let working_set_values =
+                if permanently_disable then
+                  Mods.IntMap.add guard_int None working_set_values
+                else
+                  Mods.IntMap.add guard_int bool working_set_values
+              in
+              let error, (guard_id, _) =
+                Ckappa_sig.Ws_index_map_and_set.Map.find_default parameters
+                  error
+                  (Ckappa_sig.guard_parameter_of_int (-1), Some false)
+                  working_set_index working_set_valuations
+              in
+              let error, working_set_valuations =
+                Ckappa_sig.Ws_index_map_and_set.Map.add_or_overwrite parameters
+                  error working_set_index (guard_id, bool)
+                  working_set_valuations
+              in
+              error, working_set_values, working_set_valuations, true
+            ))
+      in
+      *)
+    let permanently_remove l state = 
+      let state, c_compil = get_c_compilation state in
+      let errors = get_errors state in 
+      let parameters = get_parameters state in 
+      let state, kappa_handler = get_handler state in 
+      let map = c_compil.Cckappa_sig.working_set_valuations in 
+      let errors, l = List.fold_left 
+                (fun (errors, l) elt -> 
+                  let errors, (id,_) = Ckappa_sig.Ws_index_map_and_set.Map.find_default parameters
+                  errors
+                  (Ckappa_sig.guard_parameter_of_int (-1), Some false)
+                  elt map in 
+                  errors, (Ckappa_sig.mvbdu_var_of_guard  id (Handler.get_nsites kappa_handler))::l)
+                   (errors, []) l 
+                in 
+      let l = List.sort compare l in   
+      let state =set_errors errors state in 
+      let state = 
+        match Remanent_state.get_reachability_result state with 
+        | None -> state
+        | Some x -> 
+          let bdu_handler = Remanent_state.get_bdu_handler state in 
+          let errors = get_errors state in 
+          let errors, bdu_handler, l = Ckappa_sig.Views_bdu.build_variables_list parameters bdu_handler errors  l in 
+          let state = Remanent_state.set_bdu_handler bdu_handler state in 
+          let state = set_errors errors state in 
+          let errors, (a,b)  = Reachability.map_mvbdu 
+          (fun parameters errors bdu_handler mvbdu -> Ckappa_sig.Views_bdu.mvbdu_definitely_remove parameters bdu_handler errors mvbdu l ) errors (snd (fst x)) (snd x) in 
+          let state = Remanent_state.set_reachability_result ((fst (fst x),a),b) state in 
+          set_errors errors state in 
+      state  
+
+(*  contact_map_int: Contact_map.t option option;
+  init_state: initial_state option;
+  quark_map: quark_map option;
+  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;
+  dead_agents: dead_agents option;
+  conditionally_dead_agents: agent_deadness_conditions option;
+  ode_flow: Ode_fragmentation_type.ode_frag option;
+  ctmc_flow: flow option;
+  errors: Exception.exceptions_caught_and_uncaught;
+  internal_constraint_list: internal_constraint_list option;
+  constraint_list: constraint_list option;
+  symmetric_sites: symmetric_sites Public_data.AccuracyMap.t;
+  separating_transitions: separating_transitions option;
+  transition_system_length: int list option;
+  global_static_information: 'global_static option;
+  patch: Cckappa_sig.compil option;*)
+
+
+
     let patch ?debug ?do_not_restart_fixpoint_computation ?do_we_show_title
         ~called_from ?compil ?patch_file_name ~old_file_name ~summary state =
       let parameters = get_parameters state in
@@ -2689,15 +2801,16 @@ functor
       let state = set_errors errors state in
       let state = Remanent_state.set_handler kappa_handler state in
       let state = rename_pos (Diff.renaming_of_diff diff) state in
-      let state =
+      let state, acc  =
         permanently_disable_rule_c_id_list
           (List.rev_map Ckappa_sig.rule_id_of_int
              (List.rev diff.Diff.diff_rules.removed_elt))
-          state
+          state []
       in
-      let state =
-        permanently_disable_init_c_id_list diff.Diff.diff_init.removed_elt state
+      let state, acc =
+        permanently_disable_init_c_id_list diff.Diff.diff_init.removed_elt state acc
       in
+      let state = permanently_remove acc state in   
       let state, handler = get_handler state in
       let state, cc_compil = get_c_compilation state in
       let errors = get_errors state in

core/KaSa_rep/more_datastructures/map_wrapper.ml

@@ -356,6 +356,15 @@ module type Map_with_logs = sig
   val fold : (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
+  val map_with_logs: 
+    Remanent_parameters_sig.parameters -> Exception.exceptions_caught_and_uncaught -> 'rem
+    -> (
+      Remanent_parameters_sig.parameters ->
+    Exception.exceptions_caught_and_uncaught -> 'rem -> 
+    'a ->
+    Exception.exceptions_caught_and_uncaught * 'rem * 'b) -> 'a t -> 
+       Exception.exceptions_caught_and_uncaught * 'rem * 'b t
+
   val for_all : (elt -> 'a -> bool) -> 'a t -> bool
   val filter_one : (elt -> 'a -> bool) -> 'a t -> (elt * 'a) option
   val compare : ('a -> 'a -> int) -> 'a t -> 'a t -> int
@@ -454,7 +463,7 @@ module Make (S_both : SetMap.S) :
     let find_option_without_logs _a b c d = b, S_both.Map.find_option c d
     let find_default_without_logs _a b c d e = b, S_both.Map.find_default c d e
     let add a b c d = lift S_both.Map.add_with_logs a b c d
-
+    
     let overwrite parameter error c d e =
       let error, bool, map =
         lift S_both.Map.add_while_testing_freshness parameter error c d e
@@ -495,6 +504,16 @@ module Make (S_both : SetMap.S) :
            (fun a b c d e () -> h a b c d e, ())
            mapf mapg ())
 
+    let map_with_logs (parameter:Remanent_parameters_sig.parameters) 
+    (error:Exception_without_parameter.exceptions_caught_and_uncaught) handler f map 
+    = let ((error:Exception_without_parameter.exceptions_caught_and_uncaught),handler),map = 
+      S_both.Map.map_with_logs 
+      (fun (p:Remanent_parameters_sig.parameters) (a,b) s s_opt exn -> 
+          let a = Exception.wrap p a s s_opt exn in (a,b)) parameter (error,handler)  
+      (fun a (b,b') c -> 
+          let a,b,c = f a b b' c in (a,b),c)  map 
+    in  (error:Exception_without_parameter.exceptions_caught_and_uncaught), handler, map 
+
     let fold2_sparse a b c = lift S_both.Map.fold2_sparse_with_logs a b c
     let iter2_sparse a b c = lift S_both.Map.iter2_sparse_with_logs a b c
     let diff a b c = lift S_both.Map.diff_with_logs a b c

core/KaSa_rep/more_datastructures/map_wrapper.mli

@@ -356,6 +356,15 @@ module type Map_with_logs = sig
   val fold : (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
+  val map_with_logs: 
+    Remanent_parameters_sig.parameters -> Exception.exceptions_caught_and_uncaught -> 'rem -> 
+    (
+      Remanent_parameters_sig.parameters ->
+    Exception.exceptions_caught_and_uncaught -> 'rem -> 
+    'a ->
+    Exception.exceptions_caught_and_uncaught * 'rem * 'b) -> 'a t -> 
+       Exception.exceptions_caught_and_uncaught * 'rem * 'b t
+
   val for_all : (elt -> 'a -> bool) -> 'a t -> bool
   val filter_one : (elt -> 'a -> bool) -> 'a t -> (elt * 'a) option
   val compare : ('a -> 'a -> int) -> 'a t -> 'a t -> int

core/KaSa_rep/reachability_analysis/agents_domain.ml

@@ -984,4 +984,31 @@ module Domain = struct
       }
     in
     error, dynamic, static
-end
+
+  let map_store_value parameters error handler f store_value = 
+      let error, (handler, store_value) = 
+        Ckappa_sig.Agent_type_nearly_Inf_Int_storage_Imperatif.fold 
+          parameters error 
+          (fun p e k data (handler, store_value) -> 
+              let e, handler, data' = f p e handler data in 
+              let e, store_value = Ckappa_sig.Agent_type_nearly_Inf_Int_storage_Imperatif.set p e k data' store_value in 
+              e, (handler, store_value)) 
+          store_value  
+          (handler, store_value) 
+      in error, handler, store_value  
+
+  let map_mvbdu f errors static dynamic = 
+    let parameters = get_parameter static in 
+    let handler = get_mvbdu_handler dynamic in 
+    let local =  dynamic.local in 
+    let errors, handler, agents_liveness  = 
+        map_store_value parameters errors handler f local.agents_liveness in 
+    let local = {local with agents_liveness} in 
+    let dynamic = {dynamic with  local} in 
+    let dynamic= set_mvbdu_handler handler dynamic in 
+    errors, (static, dynamic)
+
+  end
+
+
+

core/KaSa_rep/reachability_analysis/analyzer.ml

@@ -86,6 +86,16 @@ module type Analyzer = sig
 
   val set_bdu_handler :
     Ckappa_sig.Views_bdu.handler -> dynamic_information -> dynamic_information
+
+     val map_mvbdu: 
+      (Remanent_parameters_sig.parameters 
+ -> Exception.exceptions_caught_and_uncaught -> Ckappa_sig.Views_bdu.handler -> Ckappa_sig.Views_bdu.mvbdu -> Exception.exceptions_caught_and_uncaught * Ckappa_sig.Views_bdu.handler * Ckappa_sig.Views_bdu.mvbdu) ->
+   Exception.exceptions_caught_and_uncaught 
+     ->
+   static_information -> 
+     dynamic_information 
+     -> Exception.exceptions_caught_and_uncaught * (static_information*
+    dynamic_information)
 end
 
 (***************************************************************************)
@@ -442,4 +452,10 @@ module Make (Domain : Composite_domain.Composite_domain) = struct
     let global = Domain.get_global_dynamic_information dynamic in
     let global = Analyzer_headers.set_mvbdu_handler h global in
     Domain.set_global_dynamic_information global dynamic
+
+
+  let map_mvbdu f errors static dynamic  = 
+    let error, (static, dynamic) = Domain.map_mvbdu f errors static dynamic in 
+    error, ((static), dynamic)
+
 end

core/KaSa_rep/reachability_analysis/analyzer.mli

@@ -86,6 +86,17 @@ module type Analyzer = sig
 
   val set_bdu_handler :
     Ckappa_sig.Views_bdu.handler -> dynamic_information -> dynamic_information
+
+  val map_mvbdu: 
+      (Remanent_parameters_sig.parameters 
+ -> Exception.exceptions_caught_and_uncaught -> Ckappa_sig.Views_bdu.handler -> Ckappa_sig.Views_bdu.mvbdu -> Exception.exceptions_caught_and_uncaught * Ckappa_sig.Views_bdu.handler * Ckappa_sig.Views_bdu.mvbdu) ->
+   Exception.exceptions_caught_and_uncaught 
+     ->
+   static_information -> 
+     dynamic_information 
+     -> Exception.exceptions_caught_and_uncaught * (static_information*
+    dynamic_information)
+
 end
 
 module Make : functor (Domain : Composite_domain.Composite_domain) -> Analyzer

core/KaSa_rep/reachability_analysis/analyzer_domain_sig.ml

@@ -158,4 +158,14 @@ module type Domain = sig
     Exception.exceptions_caught_and_uncaught * Ckappa_sig.side_effects option
 
   val enable_or_disable_rule : (Cckappa_sig.compil, static_information) unary
+
+ val map_mvbdu: 
+    (Remanent_parameters_sig.parameters 
+ -> Exception.exceptions_caught_and_uncaught -> Ckappa_sig.Views_bdu.handler -> Ckappa_sig.Views_bdu.mvbdu -> Exception.exceptions_caught_and_uncaught * Ckappa_sig.Views_bdu.handler * Ckappa_sig.Views_bdu.mvbdu) ->
+   Exception.exceptions_caught_and_uncaught 
+     ->
+   static_information -> 
+     dynamic_information 
+     -> Exception.exceptions_caught_and_uncaught * (static_information*
+    dynamic_information)
 end

core/KaSa_rep/reachability_analysis/analyzer_domain_sig.mli

@@ -159,4 +159,14 @@ module type Domain = sig
     Exception.exceptions_caught_and_uncaught * Ckappa_sig.side_effects option
 
   val enable_or_disable_rule : (Cckappa_sig.compil, static_information) unary
+
+  val map_mvbdu: 
+      (Remanent_parameters_sig.parameters 
+ -> Exception.exceptions_caught_and_uncaught -> Ckappa_sig.Views_bdu.handler -> Ckappa_sig.Views_bdu.mvbdu -> Exception.exceptions_caught_and_uncaught * Ckappa_sig.Views_bdu.handler * Ckappa_sig.Views_bdu.mvbdu) ->
+   Exception.exceptions_caught_and_uncaught 
+     ->
+   static_information -> 
+     dynamic_information 
+     -> Exception.exceptions_caught_and_uncaught * (static_information*
+    dynamic_information)
 end

core/KaSa_rep/reachability_analysis/composite_domain.ml

@@ -98,6 +98,16 @@ module type Composite_domain = sig
 
   val get_parameters : static_information -> Remanent_parameters_sig.parameters
   val enable_or_disable_rule : (Cckappa_sig.compil, static_information) unary
+
+   val map_mvbdu: 
+     (Remanent_parameters_sig.parameters 
+ -> Exception.exceptions_caught_and_uncaught -> Ckappa_sig.Views_bdu.handler -> Ckappa_sig.Views_bdu.mvbdu -> Exception.exceptions_caught_and_uncaught * Ckappa_sig.Views_bdu.handler * Ckappa_sig.Views_bdu.mvbdu) ->
+   Exception.exceptions_caught_and_uncaught 
+     ->
+   static_information -> 
+     dynamic_information 
+     -> Exception.exceptions_caught_and_uncaught * (static_information*
+    dynamic_information)
 end
 
 (****************************************************************************)
@@ -678,4 +688,16 @@ module Make (Domain : Analyzer_domain_sig.Domain) = struct
     error, dynamic, (static_global, static_domain)
 
   let get_parameters (_, static_domain) = Domain.get_parameter static_domain
+
+
+let map_mvbdu f errors static dynamic = 
+  let errors, (dstatic, domain) =
+     Domain.map_mvbdu f errors 
+        (get_domain_static_information static)  
+        (
+         dynamic.domain) 
+in 
+  errors, ((fst static, dstatic), 
+          ({dynamic with domain}))
+          
 end