reset current working set information when the result of the domains changes

Author: reb-ddm

core/KaSa_rep/reachability_analysis/agents_domain.ml

@@ -169,7 +169,11 @@ module Domain = struct
       error, dynamic, result
 
   let set_seen_agent seen_agent dynamic =
-    { dynamic with local = { dynamic.local with agents_liveness = seen_agent } }
+    {
+      dynamic with
+      local =
+        { agents_liveness = seen_agent; liveness_current_working_set = None };
+    }
 
   let is_false_mvbdu parameters error dynamic mvbdu =
     let bdu_handler = get_mvbdu_handler dynamic in

core/KaSa_rep/reachability_analysis/parallel_bonds.ml

@@ -53,7 +53,6 @@ module Domain = struct
     Parallel_bonds_type.PairAgentSitesStates_map_and_set.Map.t
 
   type local_dynamic_information = {
-    dummy: unit;
     store_value: store_value;
     store_value_current_working_set: store_value option;
   }
@@ -297,7 +296,7 @@ module Domain = struct
 
   let set_value value dynamic =
     set_local_dynamic_information
-      { (get_local_dynamic_information dynamic) with store_value = value }
+      { store_value = value; store_value_current_working_set = None }
       dynamic
 
   (*--------------------------------------------------------------*)
@@ -546,7 +545,6 @@ module Domain = struct
     in
     let init_local_dynamic_information =
       {
-        dummy = ();
         store_value =
           Parallel_bonds_type.PairAgentSitesStates_map_and_set.Map.empty;
         store_value_current_working_set = None;

core/KaSa_rep/reachability_analysis/rules_domain.ml

@@ -144,7 +144,10 @@ module Domain = struct
       error, dynamic, result
 
   let set_dead_rule dead_rule dynamic =
-    { dynamic with local = { dynamic.local with rule_liveness = dead_rule } }
+    {
+      dynamic with
+      local = { rule_liveness = dead_rule; liveness_current_working_set = None };
+    }
 
   let is_false_mvbdu parameters error dynamic mvbdu =
     let bdu_handler = get_mvbdu_handler dynamic in

core/KaSa_rep/reachability_analysis/site_across_bonds_domain.ml

@@ -39,7 +39,6 @@ module Domain = struct
   type local_static_information = {
     store_basic_static_information:
       Site_across_bonds_domain_static.basic_static_information;
-    dummy: unit;
   }
 
   type static_information = {
@@ -55,11 +54,13 @@ module Domain = struct
   *)
   (*--------------------------------------------------------------*)
 
+  type store_value =
+    Ckappa_sig.Views_bdu.mvbdu
+    Site_across_bonds_domain_type.PairAgentSitesState_map_and_set.Map.t
+
   type local_dynamic_information = {
-    dummy: unit;
-    store_value:
-      Ckappa_sig.Views_bdu.mvbdu
-      Site_across_bonds_domain_type.PairAgentSitesState_map_and_set.Map.t;
+    store_value: store_value;
+    store_value_current_working_set: store_value option;
   }
 
   type dynamic_information = {
@@ -118,10 +119,7 @@ module Domain = struct
 
   let set_basic_static_information domain static =
     set_local_static_information
-      {
-        (get_local_static_information static) with
-        store_basic_static_information = domain;
-      }
+      { store_basic_static_information = domain }
       static
 
   (***************************************************************************)
@@ -356,7 +354,7 @@ module Domain = struct
 
   let set_value value dynamic =
     set_local_dynamic_information
-      { (get_local_dynamic_information dynamic) with store_value = value }
+      { store_value = value; store_value_current_working_set = None }
       dynamic
 
   (** profiling *)
@@ -634,7 +632,6 @@ module Domain = struct
       {
         store_basic_static_information =
           Site_across_bonds_domain_static.init_basic_static_information;
-        dummy = ();
       }
     in
     let init_global_static_information =
@@ -645,10 +642,10 @@ module Domain = struct
     in
     let init_local_dynamic_information =
       {
-        dummy = ();
         store_value =
           Site_across_bonds_domain_type.PairAgentSitesState_map_and_set.Map
           .empty;
+        store_value_current_working_set = None;
       }
     in
     let init_global_dynamic_information =