add closure for the mvbdu_equal operation

Author: reb-ddm

core/KaSa_rep/frontend/ckappa_sig.ml

@@ -1463,6 +1463,18 @@ let mvbdu_is_false_for_guards parameters handler_bdu error mvbdu bdu_restriction
   in
   error, handler_bdu, Views_bdu.equal inter_mvbdu mvbdu_false
 
+let mvbdu_equal_for_guards parameters handler_bdu error mvbdu1 mvbdu2
+    bdu_restriction =
+  if Views_bdu.equal mvbdu1 mvbdu2 then
+    error, handler_bdu, true
+  else (
+    let error, handler_bdu, mvbdu_xor =
+      Views_bdu.mvbdu_xor parameters handler_bdu error mvbdu1 mvbdu2
+    in
+    mvbdu_is_false_for_guards parameters handler_bdu error mvbdu_xor
+      bdu_restriction
+  )
+
 (**Returns the bdu representation of the guard, and a bdu that maps each guard parameter of the guard to 1 or 0.
 This second bdu is used to restrict the bdus that are calculated by using "or" and "not"
 to valid bdus where the values of the guards can only be 0 and 1. *)

core/KaSa_rep/frontend/ckappa_sig.mli

@@ -745,6 +745,17 @@ val mvbdu_is_false_for_guards :
   * Views_bdu.handler
   * bool
 
+val mvbdu_equal_for_guards :
+  Remanent_parameters_sig.parameters ->
+  Views_bdu.handler ->
+  Exception_without_parameter.exceptions_caught_and_uncaught ->
+  Views_bdu.mvbdu ->
+  Views_bdu.mvbdu ->
+  Views_bdu.mvbdu ->
+  Exception_without_parameter.exceptions_caught_and_uncaught
+  * Views_bdu.handler
+  * bool
+
 val guard_to_bdu :
   Remanent_parameters_sig.parameters ->
   Exception_without_parameter.exceptions_caught_and_uncaught ->

core/KaSa_rep/reachability_analysis/agents_domain.ml

@@ -453,7 +453,12 @@ module Domain = struct
       let error, dynamic, new_mvbdu =
         or_mvbdu parameters error dynamic old_mvbdu bdu_guard restriction_bdu
       in
-      let b = Ckappa_sig.Views_bdu.equal old_mvbdu new_mvbdu in
+      let bdu_handler = get_mvbdu_handler dynamic in
+      let error, bdu_handler, b =
+        Ckappa_sig.mvbdu_equal_for_guards parameters bdu_handler error old_mvbdu
+          new_mvbdu restriction_bdu
+      in
+      let dynamic = set_mvbdu_handler bdu_handler dynamic in
       if b then
         error, (dynamic, event_list)
       else (

core/KaSa_rep/reachability_analysis/parallel_bonds_type.ml

@@ -656,7 +656,11 @@ let add_value_and_event parameters error kappa_handler x value store_set
     Ckappa_sig.mvbdu_or_for_guards parameters bdu_handler error old_value
       value_mvbdu restriction_mvbdu
   in
-  if Ckappa_sig.Views_bdu.equal new_value old_value then
+  let error, bdu_handler, are_equal =
+    Ckappa_sig.mvbdu_equal_for_guards parameters bdu_handler error new_value
+      old_value restriction_mvbdu
+  in
+  if are_equal then
     error, (bdu_handler, store_set, store_result)
   else (
     (*check whether or not if this is a fresh value*)

core/KaSa_rep/reachability_analysis/site_across_bonds_domain.ml

@@ -934,7 +934,7 @@ module Domain = struct
     error, dynamic, new_mvbdu
 
   let common_scan parameters error bdu_false dynamic store_value list guard_bdu
-      =
+      restriction_bdu =
     let rec scan list dynamic error precondition_bdu =
       match list with
       | [] -> error, true, dynamic, precondition_bdu
@@ -956,7 +956,13 @@ module Domain = struct
           build_mvbdu_range_list parameters error dynamic tuple
             mvbdu_value_with_guard
         in
-        if Ckappa_sig.Views_bdu.equal new_mvbdu bdu_false then
+        let bdu_handler = get_mvbdu_handler dynamic in
+        let error, bdu_handler, are_equal =
+          Ckappa_sig.mvbdu_equal_for_guards parameters bdu_handler error
+            new_mvbdu bdu_false restriction_bdu
+        in
+        let dynamic = set_mvbdu_handler bdu_handler dynamic in
+        if are_equal then
           error, false, dynamic, bdu_false
         else (
           let bdu_handler = get_mvbdu_handler dynamic in
@@ -975,7 +981,7 @@ module Domain = struct
     scan list dynamic error guard_bdu
 
   let whether_or_not_it_has_precondition parameters error bdu_false tuple_set
-      static dynamic precondition guard_bdu current_ws =
+      static dynamic precondition guard_bdu current_ws restriction_bdu =
     let list =
       Site_across_bonds_domain_type.PairAgentSitesPStates_map_and_set.Set
       .elements tuple_set
@@ -989,6 +995,7 @@ module Domain = struct
     (*check if this pattern belong to the set of the patterns in the result*)
     let error, bool, dynamic, precondition_bdu =
       common_scan parameters error bdu_false dynamic store_value list guard_bdu
+        restriction_bdu
     in
     let error, dynamic, precondition =
       update_state_of_guard_parameters parameters error dynamic precondition
@@ -1004,6 +1011,7 @@ module Domain = struct
     let parameters = get_parameter static in
     let error, dynamic, bdu_false = get_mvbdu_false static dynamic error in
     let guard_bdus = get_guard_mvbdus static in
+    let restriction_bdu = get_restriction_mvbdu static in
     let error, dynamic, guard_bdu =
       get_bdu_guard parameters dynamic error guard_bdus rule_id
     in
@@ -1016,7 +1024,7 @@ module Domain = struct
         .empty store_potential_tuple_pair_lhs
     in
     whether_or_not_it_has_precondition parameters error bdu_false tuple_set
-      static dynamic precondition guard_bdu false
+      static dynamic precondition guard_bdu false restriction_bdu
 
   (***************************************************************************)
   (*MAY BE REACHABLE*)
@@ -1030,6 +1038,7 @@ module Domain = struct
     let kappa_handler = get_kappa_handler static in
     let error, dynamic, bdu_false = get_mvbdu_false static dynamic error in
     let error, dynamic, bdu_true = get_mvbdu_true static dynamic error in
+    let restriction_bdu = get_restriction_mvbdu static in
     let error, bonds_lhs =
       Common_static.collect_bonds_pattern parameters error
         pattern.Cckappa_sig.views pattern.Cckappa_sig.bonds
@@ -1053,7 +1062,7 @@ module Domain = struct
         tuple_set
     in
     whether_or_not_it_has_precondition parameters error bdu_false tuple_set
-      static dynamic precondition bdu_true true
+      static dynamic precondition bdu_true true restriction_bdu
 
   (****************************************************************)
 
@@ -1069,7 +1078,8 @@ module Domain = struct
   (*APPLY RULE*)
   (***************************************************************************)
 
-  let check_association_list parameters error bdu_false pair check dynamic =
+  let check_association_list parameters error bdu_false pair check dynamic
+      restriction_bdu =
     let store_result = get_value dynamic in
     let bdu_handler = get_mvbdu_handler dynamic in
     let check, bdu_list =
@@ -1091,7 +1101,7 @@ module Domain = struct
     in
     let error, bdu_handler, bool =
       Site_across_bonds_domain_type.check parameters error bdu_false bdu_handler
-        pair mvbdu store_result
+        pair mvbdu store_result restriction_bdu
     in
     let dynamic = set_mvbdu_handler bdu_handler dynamic in
     error, dynamic, bool
@@ -1564,7 +1574,7 @@ module Domain = struct
                   in
                   let error, dynamic, unmodified_sites_ok =
                     check_association_list parameters error bdu_false pair check
-                      dynamic
+                      dynamic restriction_bdu
                   in
                   if unmodified_sites_ok then (
                     let error, bool, dynamic, modified_sites =
@@ -1855,7 +1865,7 @@ module Domain = struct
                 (*at the final result needs to check the non_relational
                   condition*)
                 Translation_in_natural_language.non_relational parameters
-                  bdu_handler error mvbdu
+                  bdu_handler error mvbdu restriction_bdu
               else
                 (*other cases will by pass this test*)
                 error, bdu_handler, false
@@ -1999,26 +2009,30 @@ module Domain = struct
           parameters error handler f store_value 
       in error, handler, store_value  
 
- let _map_store_value_opt parameters error handler f store_value = 
-    match store_value with 
-      | None -> error, handler, store_value 
-      | Some store_value -> 
-          let error, handler, store_value = map_store_value parameters error handler f store_value in 
-          error, handler, Some store_value 
-
-  let map_mvbdu f errors static dynamic = 
-    let parameters = get_parameter static in 
-    let handler = get_mvbdu_handler dynamic in 
-    let local = get_local_dynamic_information dynamic in 
-    let errors, handler, store_value  = 
-        map_store_value parameters errors handler f local.store_value in 
-    (*let errors, handler, store_value_current_working_set = 
-        map_store_value_opt parameters errors handler f local.store_value_current_working_set
-    in*) (* should not be impacted by Boolean parameters *) 
-    let local = {local with store_value (*; store_value_current_working_set*)} in 
-    let dynamic = set_local_dynamic_information local dynamic in 
-    let dynamic= set_mvbdu_handler handler dynamic in 
-    errors, (static, dynamic)
-
+  let _map_store_value_opt parameters error handler f store_value =
+    match store_value with
+    | None -> error, handler, store_value
+    | Some store_value ->
+      let error, handler, store_value =
+        map_store_value parameters error handler f store_value
+      in
+      error, handler, Some store_value
 
+  let map_mvbdu f errors static dynamic =
+    let parameters = get_parameter static in
+    let handler = get_mvbdu_handler dynamic in
+    let local = get_local_dynamic_information dynamic in
+    let errors, handler, store_value =
+      map_store_value parameters errors handler f local.store_value
+    in
+    (*let errors, handler, store_value_current_working_set =
+          map_store_value_opt parameters errors handler f local.store_value_current_working_set
+      in*)
+    (* should not be impacted by Boolean parameters *)
+    let local =
+      { local with store_value (*; store_value_current_working_set*) }
+    in
+    let dynamic = set_local_dynamic_information local dynamic in
+    let dynamic = set_mvbdu_handler handler dynamic in
+    errors, (static, dynamic)
 end

core/KaSa_rep/reachability_analysis/site_across_bonds_domain_type.ml

@@ -493,7 +493,7 @@ let print_site_across_bonds_domain ?verbose:(_verbose = true) ?(sparse = false)
       if final_result then
         (*at the final result needs to check the non_relational condition*)
         Translation_in_natural_language.non_relational parameters bdu_handler
-          error mvbdu
+          error mvbdu restriction_bdu
       else
         (*other cases will by pass this test*)
         error, bdu_handler, false
@@ -595,14 +595,19 @@ let add_sites_from_tuples parameters error tuple modified_sites =
     (error, modified_sites)
     [ agent, site1; agent, site2; agent', site1'; agent', site2' ]
 
-let check parameters error bdu_false bdu_handler pair mvbdu store_result =
+let check parameters error bdu_false bdu_handler pair mvbdu store_result
+    restriction_bdu =
   let error, bdu_old =
     get_mvbdu_from_tuple_pair parameters error pair bdu_false store_result
   in
   let error, bdu_handler, new_bdu =
     Ckappa_sig.Views_bdu.mvbdu_and parameters bdu_handler error bdu_old mvbdu
   in
-  if Ckappa_sig.Views_bdu.equal new_bdu bdu_false then
+  let error, bdu_handler, is_false =
+    Ckappa_sig.mvbdu_is_false_for_guards parameters bdu_handler error new_bdu
+      restriction_bdu
+  in
+  if is_false then
     error, bdu_handler, false
   else
     error, bdu_handler, true
@@ -620,7 +625,11 @@ let add_link_and_check parameter error bdu_false bdu_handler kappa_handler bool
   (*-----------------------------------------------------------*)
   (*check the freshness of the pair*)
   (*compare mvbdu and old mvbdu*)
-  if Ckappa_sig.Views_bdu.equal new_bdu bdu_old then
+  let error, bdu_handler, are_equal =
+    Ckappa_sig.mvbdu_equal_for_guards parameter bdu_handler error new_bdu
+      bdu_old restriction_mvbdu
+  in
+  if are_equal then
     error, bool, bdu_handler, modified_sites, store_result
   else (
     (*-----------------------------------------------------------*)