clean code and comments

Author: reb-ddm

core/KaSa_rep/reachability_analysis/bdu_static_views.ml

@@ -585,7 +585,8 @@ let collect_site_to_renamed_site_list parameters error store_remanent_triple
           let rec aux error site list output =
             match list with
             | [] -> error, output
-            | Ckappa_sig.Guard_p _ :: _ -> error, output
+            | Ckappa_sig.Guard_p _ :: _ ->
+              (*only sites are converted to a new index*) error, output
             | Ckappa_sig.Site h :: t ->
               let h =
                 Ckappa_sig.mvbdu_var_of_site_or_guard_p (Ckappa_sig.Site h)

core/KaSa_rep/reachability_analysis/parallel_bonds.ml

@@ -43,12 +43,11 @@ module Domain = struct
   }
 
   (*--------------------------------------------------------------*)
-  (* One map: for each tuple: Yes mvbdu, No mvbdu
-     - Yes: for these values of the guards, when the sites x and y are bound with sites of
-      the good type, then they are bound to the same B.
-     - No: for these values of the guards, when the sites x and y are bound with sites of the good
-      type, then they are never bound to the same B.
-     - Otherwise: both cases may happen.*)
+  (* The map `store_value` maps each tuple of sites ((x,y),(a,b)) to a mvbdu whose variables are the guard parameters and an additional variable (the "first variable").
+     Given a valuation for the guard parameters:
+        - if the "first variable" must be true in order to satisfy the mvbdu: it means that when the sites x and y are bound with sites of the types a and b, then they are always bound to the same agent.
+        - if the "first variable" must be false in order to satisfy the mvbdu: it means that when when the sites x and y are bound with sites of the types a and b, then they are never bound to the same agent.
+        - if the first variable may be both true or false: both cases may happen.*)
 
   type local_dynamic_information = {
     dummy: unit;

core/KaSa_rep/reachability_analysis/parallel_bonds_static.ml

@@ -62,7 +62,7 @@ type local_static_information = {
   store_sites_to_tuple:
     Parallel_bonds_type.PairAgentSitesStates_map_and_set.Set.t
     Parallel_bonds_type.AgentSite_map_and_set.Map.t;
-      (*the same as the global restriction mvbdu, but it contains one additional variable at the end.*)
+      (*the same as the global restriction mvbdu, but it contains an additional "first variable" at the beginning.*)
   restriction_mvbdu: Ckappa_sig.Views_bdu.mvbdu;
 }
 

core/KaSa_rep/reachability_analysis/parallel_bonds_type.ml

@@ -593,7 +593,6 @@ let add_value_lattice parameters error x value store_result =
     error, store_result
   )
 
-(*TODO merge with above*)
 let add_value_mvbdu parameters error x bdu_handler store_result mvbdu
     restriction_mvbdu =
   let error, bdu_handler, mvbdu_false =
@@ -607,10 +606,6 @@ let add_value_mvbdu parameters error x bdu_handler store_result mvbdu
     | error, None -> error, mvbdu_false
     | error, Some old_mvbdu -> error, old_mvbdu
   in
-  (* let error, bdu_handler, mvbdu_refined =
-     add_first_variable_to_mvbdu parameters bdu_handler error bool
-        mvbdu
-     in *)
   let error, bdu_handler, new_mvbdu =
     Ckappa_sig.mvbdu_or_for_guards parameters bdu_handler error old_mvbdu mvbdu
       restriction_mvbdu

core/KaSa_rep/reachability_analysis/site_across_bonds_domain.ml

@@ -48,9 +48,9 @@ module Domain = struct
   }
 
   (*--------------------------------------------------------------*)
-  (* Maps each such tuples (A,x,y,B,z,t) to a mvbdu with (n + 2) variables.
+  (* The map `store_value` maps each tuples (A,x,y,B,z,t) to a mvbdu with (n + 2) variables.
      The last n variables describe the boolean value of the guard parameters.
-         Tha first two variables describe the relation between the state of y and the state of t,
+         The first two variables describe the relation between the state of y and the state of t,
          when both agents are connected via x and z.
   *)
   (*--------------------------------------------------------------*)
@@ -1823,7 +1823,7 @@ module Domain = struct
         let error, handler =
           Site_across_bonds_domain_type.PairAgentSitesState_map_and_set.Map.fold
             (fun (x, y) mvbdu (error, handler) ->
-              Site_across_bonds_domain_type.print_site_across_domain
+              Site_across_bonds_domain_type.print_site_across_bonds_domain
                 ~verbose:true ~sparse:true ~final_result:true ~dump_any:true
                 parameters error kappa_handler handler (x, y) mvbdu
                 restriction_bdu)

core/KaSa_rep/reachability_analysis/site_across_bonds_domain_type.ml

@@ -324,9 +324,9 @@ let print_guard_mvbdu parameters error handler kappa_handler mvbdu
     error, handler
   )
 
-let print_site_across_domain_raw parameters error kappa_handler handler log
-    final_result pair_list nsites agent_id1 site_type1' agent_id2 site_type2'
-    pattern restriction_bdu =
+let print_site_across_bonds_domain_raw parameters error kappa_handler handler
+    log final_result pair_list nsites agent_id1 site_type1' agent_id2
+    site_type2' pattern restriction_bdu =
   let error =
     (*do not print the precondition if it is not the final result*)
     if final_result then (
@@ -414,9 +414,10 @@ let print_site_across_domain_raw parameters error kappa_handler handler log
     in
     error, handler
 
-let print_site_across_domain_natural_language parameters error kappa_handler
-    handler log pair_list nsites prefix site1 site2 site1' agent1 site2' agent2
-    agent_type1 site_type1 agent_type2 site_type2 restriction_bdu =
+let print_site_across_bonds_domain_natural_language parameters error
+    kappa_handler handler log pair_list nsites prefix site1 site2 site1' agent1
+    site2' agent2 agent_type1 site_type1 agent_type2 site_type2 restriction_bdu
+    =
   let () =
     Loggers.fprintf log
       "%sWhenever the site %s of %s and the site %s of %s are bound together, \
@@ -468,7 +469,7 @@ let print_site_across_domain_natural_language parameters error kappa_handler
       error, handler)
     (error, handler) pair_list
 
-let print_site_across_domain ?verbose:(_verbose = true) ?(sparse = false)
+let print_site_across_bonds_domain ?verbose:(_verbose = true) ?(sparse = false)
     ?(final_result = false) ?dump_any:(_dump_any = false) parameters error
     kappa_handler handler tuple mvbdu restriction_bdu =
   let prefix = Remanent_parameters.get_prefix parameters in
@@ -528,11 +529,11 @@ let print_site_across_domain ?verbose:(_verbose = true) ?(sparse = false)
             Site_graphs.KaSa_site_graph.add_bond parameters error kappa_handler
               agent_id1 site_type1 agent_id2 site_type2 pattern
           in
-          print_site_across_domain_raw parameters error kappa_handler handler
-            log final_result pair_list nsites agent_id1 site_type1' agent_id2
-            site_type2' pattern restriction_bdu
+          print_site_across_bonds_domain_raw parameters error kappa_handler
+            handler log final_result pair_list nsites agent_id1 site_type1'
+            agent_id2 site_type2' pattern restriction_bdu
         | Remanent_parameters_sig.Natural_language ->
-          print_site_across_domain_natural_language parameters error
+          print_site_across_bonds_domain_natural_language parameters error
             kappa_handler handler log pair_list nsites prefix site1 site2 site1'
             agent1 site2' agent2 agent_type1 site_type1 agent_type2 site_type2
             restriction_bdu
@@ -570,8 +571,8 @@ let add_link parameter error bdu_false handler kappa_handler pair mvbdu
       let parameter =
         Remanent_parameters.update_prefix parameter "                "
       in
-      print_site_across_domain ~verbose:false ~dump_any:true parameter error
-        kappa_handler handler pair mvbdu restriction_mvbdu
+      print_site_across_bonds_domain ~verbose:false ~dump_any:true parameter
+        error kappa_handler handler pair mvbdu restriction_mvbdu
     ) else
       error, handler
   in
@@ -628,8 +629,8 @@ let add_link_and_check parameter error bdu_false handler kappa_handler bool
           else
             dump_title ()
         in
-        print_site_across_domain ~verbose:false ~dump_any:true parameter error
-          kappa_handler handler x mvbdu restriction_mvbdu
+        print_site_across_bonds_domain ~verbose:false ~dump_any:true parameter
+          error kappa_handler handler x mvbdu restriction_mvbdu
       ) else
         error, handler
     in

core/KaSa_rep/type_interface/public_data.ml

@@ -32,7 +32,7 @@ let hyp = "site graph"
 let refinement = "site graph list"
 let domain_name = "domain name"
 let refinements_list = "refinements list"
-let refinement_lemmas = "lemmas"
+let refinement_lemmas = "refinement lemmas"
 let rule_id = "id"
 let agent_id = "id"
 let label = "label"

examples/boolean_predicates/example_double_bonds_all_cases.ka

@@ -26,5 +26,3 @@ A(x[.],y[.]), A(x[.],y[.]) -> A(x[1],y[.]), A(x[1],y[.]) @ 1
 
 // Measure amount of A double bonds
 %obs: 'Trimer' |A(x[1],y[2]),A(x[1],y[2])|
-
-// Static analysis must show that P => no double bonds