format

Author: Jérôme FERET

core/KaSa_rep/abstract_domains/mvbdu/boolean_mvbdu.ml

@@ -112,8 +112,10 @@ type memo_tables = {
   boolean_mvbdu_extensional_description_of_range_list:
     (int * (int option * int option)) list Hash_1.t;
   boolean_mvbdu_variables_of_mvbdu: unit List_sig.list Hash_1.t;
-  boolean_mvbdu_extensional_description_of_mvbdu: (int * int) list list Hash_1.t;
-  boolean_mvbdu_extensional_description_of_mvbdu_with_threshold: ((int * int) list * bool Mvbdu_sig.mvbdu) list Hash_2.t;
+  boolean_mvbdu_extensional_description_of_mvbdu:
+    (int * int) list list Hash_1.t;
+  boolean_mvbdu_extensional_description_of_mvbdu_with_threshold:
+    ((int * int) list * bool Mvbdu_sig.mvbdu) list Hash_2.t;
 }
 
 type mvbdu_dic =
@@ -340,8 +342,8 @@ let init_data parameters error =
     Hash_1.create parameters error 0
   in
   let error, mvbdu_extensional_description_of_mvbdu_with_threshold =
-  Hash_2.create parameters error (0,0)
-in
+    Hash_2.create parameters error (0, 0)
+  in
   let error, mvbdu_rename = Hash_2.create parameters error (0, 0) in
   ( error,
     {
@@ -380,8 +382,8 @@ in
       boolean_mvbdu_variables_of_mvbdu = mvbdu_variables_of;
       boolean_mvbdu_extensional_description_of_mvbdu =
         mvbdu_extensional_description_of_mvbdu;
-      boolean_mvbdu_extensional_description_of_mvbdu_with_threshold = 
-        mvbdu_extensional_description_of_mvbdu_with_threshold 
+      boolean_mvbdu_extensional_description_of_mvbdu_with_threshold =
+        mvbdu_extensional_description_of_mvbdu_with_threshold;
     } )
 
 let init_remanent parameters error =
@@ -1399,80 +1401,90 @@ let rec extensional_description_of_mvbdu parameters handler error mvbdu =
         },
         output ) )
 
-
-  let extensional_description_of_mvbdu_with_threshold parameters handler error ~threshold mvbdu =
-    let error, (handler, bdd_true) = boolean_mvbdu_true parameters handler error parameters   in 
-    match bdd_true with 
-      Some bdd_true -> 
-        begin 
+let extensional_description_of_mvbdu_with_threshold parameters handler error
+    ~threshold mvbdu =
+  let error, (handler, bdd_true) =
+    boolean_mvbdu_true parameters handler error parameters
+  in
+  match bdd_true with
+  | Some bdd_true ->
     let rec aux1 parameters handler error ~threshold mvbdu =
-          match
-            Hash_2.unsafe_get parameters error (threshold,mvbdu.Mvbdu_sig.id)
-              handler.Memo_sig.data.boolean_mvbdu_extensional_description_of_mvbdu_with_threshold
-          with
-          | error, Some output -> error, (handler, output)
-          | error, None ->
-            let rec aux2 mvbdu remanent handler error output =
-              match mvbdu.Mvbdu_sig.value with
-              | Mvbdu_sig.Leaf true -> error, (handler, ([],bdd_true) :: output)
-              | Mvbdu_sig.Leaf false -> error, (handler, output)
-              | Mvbdu_sig.Node a ->
-                let id = a.Mvbdu_sig.variable in 
-                if id <= threshold 
-                then (* Recursion *)
-                let error, (handler, branch_true) =
-                  aux1 parameters handler error ~threshold a.Mvbdu_sig.branch_true
-                in
-                let upper_bound = a.Mvbdu_sig.upper_bound in
-                let error, (handler, output) =
-                  match remanent, branch_true with
-                  | _, [] -> error, (handler, output)
-                  | None, _ -> Exception.warn parameters error __POS__ Exit (handler, [])
-                  | Some (var, lower_bound), list ->
-                    let head_list =
-                      let rec aux3 k res =
-                        if k <= lower_bound then
-                          res
-                        else
-                          aux3 (k - 1) (k :: res)
-                      in
-                      aux3 upper_bound []
-                    in
-                    let output =
-                      List.fold_left
-                        (fun output head ->
-                          List.fold_left
-                            (fun output (tail,b) -> ((var, head) :: tail,b) :: output)
-                            output list)
-                        output head_list
+      match
+        Hash_2.unsafe_get parameters error
+          (threshold, mvbdu.Mvbdu_sig.id)
+          handler.Memo_sig.data
+            .boolean_mvbdu_extensional_description_of_mvbdu_with_threshold
+      with
+      | error, Some output -> error, (handler, output)
+      | error, None ->
+        let rec aux2 mvbdu remanent handler error output =
+          match mvbdu.Mvbdu_sig.value with
+          | Mvbdu_sig.Leaf true -> error, (handler, ([], bdd_true) :: output)
+          | Mvbdu_sig.Leaf false -> error, (handler, output)
+          | Mvbdu_sig.Node a ->
+            let id = a.Mvbdu_sig.variable in
+            if id <= threshold then (
+              (* Recursion *)
+              let error, (handler, branch_true) =
+                aux1 parameters handler error ~threshold a.Mvbdu_sig.branch_true
+              in
+              let upper_bound = a.Mvbdu_sig.upper_bound in
+              let error, (handler, output) =
+                match remanent, branch_true with
+                | _, [] -> error, (handler, output)
+                | None, _ ->
+                  Exception.warn parameters error __POS__ Exit (handler, [])
+                | Some (var, lower_bound), list ->
+                  let head_list =
+                    let rec aux3 k res =
+                      if k <= lower_bound then
+                        res
+                      else
+                        aux3 (k - 1) (k :: res)
                     in
-                    error, (handler, output)
-                in
-                aux2 a.Mvbdu_sig.branch_false
-                  (Some (a.Mvbdu_sig.variable, upper_bound))
-                  handler error output
-              else (* threshold crossed, convert in bdd *)
-             (* let error, (handler, bdd) = memo_identity parameters handler error parameters a in*)
-                error, (handler, ([],mvbdu) :: output)
-            in
-            let error, (handler, output) = aux2 mvbdu None handler error [] in
-            let error, memo =
-              Hash_2.set parameters error (threshold,mvbdu.Mvbdu_sig.id) output
-                handler.Memo_sig.data.boolean_mvbdu_extensional_description_of_mvbdu_with_threshold
-            in
-            ( error,
-              ( {
-                  handler with
-                  Memo_sig.data =
-                    {
-                      handler.Memo_sig.data with
-                      boolean_mvbdu_extensional_description_of_mvbdu_with_threshold = memo;
-                    };
-                },
-                output ) )   
-    in aux1 parameters handler error ~threshold mvbdu     
-  end 
-  | None -> error, (handler,[])
+                    aux3 upper_bound []
+                  in
+                  let output =
+                    List.fold_left
+                      (fun output head ->
+                        List.fold_left
+                          (fun output (tail, b) ->
+                            ((var, head) :: tail, b) :: output)
+                          output list)
+                      output head_list
+                  in
+                  error, (handler, output)
+              in
+              aux2 a.Mvbdu_sig.branch_false
+                (Some (a.Mvbdu_sig.variable, upper_bound))
+                handler error output
+            ) else
+              (* threshold crossed, convert in bdd *)
+              (* let error, (handler, bdd) = memo_identity parameters handler error parameters a in*)
+              error, (handler, ([], mvbdu) :: output)
+        in
+        let error, (handler, output) = aux2 mvbdu None handler error [] in
+        let error, memo =
+          Hash_2.set parameters error
+            (threshold, mvbdu.Mvbdu_sig.id)
+            output
+            handler.Memo_sig.data
+              .boolean_mvbdu_extensional_description_of_mvbdu_with_threshold
+        in
+        ( error,
+          ( {
+              handler with
+              Memo_sig.data =
+                {
+                  handler.Memo_sig.data with
+                  boolean_mvbdu_extensional_description_of_mvbdu_with_threshold =
+                    memo;
+                };
+            },
+            output ) )
+    in
+    aux1 parameters handler error ~threshold mvbdu
+  | None -> error, (handler, [])
 
 let print_boolean_mvbdu parameters
     (error : Exception.exceptions_caught_and_uncaught) =

core/KaSa_rep/abstract_domains/mvbdu/boolean_mvbdu.mli

@@ -66,8 +66,10 @@ type memo_tables = {
   boolean_mvbdu_extensional_description_of_range_list:
     (int * (int option * int option)) list Hash_1.t;
   boolean_mvbdu_variables_of_mvbdu: unit List_sig.list Hash_1.t;
-  boolean_mvbdu_extensional_description_of_mvbdu: (int * int) list list Hash_1.t;
-  boolean_mvbdu_extensional_description_of_mvbdu_with_threshold: ((int * int) list * bool Mvbdu_sig.mvbdu) list Hash_2.t;
+  boolean_mvbdu_extensional_description_of_mvbdu:
+    (int * int) list list Hash_1.t;
+  boolean_mvbdu_extensional_description_of_mvbdu_with_threshold:
+    ((int * int) list * bool Mvbdu_sig.mvbdu) list Hash_2.t;
 }
 
 type unary_memoized_fun
@@ -118,14 +120,14 @@ val extensional_description_of_mvbdu :
   Exception_without_parameter.exceptions_caught_and_uncaught
   * (handler * (int * int) list list)
 
-  val extensional_description_of_mvbdu_with_threshold :
+val extensional_description_of_mvbdu_with_threshold :
   Remanent_parameters_sig.parameters ->
   handler ->
   Exception_without_parameter.exceptions_caught_and_uncaught ->
-  threshold:int -> 
+  threshold:int ->
   bool Mvbdu_sig.mvbdu ->
   Exception_without_parameter.exceptions_caught_and_uncaught
-  * (handler * ((int * int) list * bool Mvbdu_sig.mvbdu) list)  
+  * (handler * ((int * int) list * bool Mvbdu_sig.mvbdu) list)
 
 val extensional_description_of_range_list :
   'g ->

core/KaSa_rep/abstract_domains/mvbdu/mvbdu_wrapper.ml

@@ -44,12 +44,12 @@ module type Mvbdu = sig
     Exception.exceptions_caught_and_uncaught ->
     'input ->
     Exception.exceptions_caught_and_uncaught * handler * 'output
-    
+
   type ('input, 'output) unary_with_threshold =
     Remanent_parameters_sig.parameters ->
     handler ->
-    Exception.exceptions_caught_and_uncaught -> 
-    threshold:int -> 
+    Exception.exceptions_caught_and_uncaught ->
+    threshold:int ->
     'input ->
     Exception.exceptions_caught_and_uncaught * handler * 'output
 
@@ -204,7 +204,9 @@ module type Mvbdu = sig
     (hconsed_range_list, (key * (value option * value option)) list) unary
 
   val extensional_of_mvbdu : (mvbdu, (key * value) list list) unary
-  val parametric_conditions_of_mvbdu:   (mvbdu, ((key * value) list * mvbdu) list) unary_with_threshold
+
+  val parametric_conditions_of_mvbdu :
+    (mvbdu, ((key * value) list * mvbdu) list) unary_with_threshold
 
   val variables_list_of_mvbdu : (mvbdu, hconsed_variables_list) unary
   val print : Remanent_parameters_sig.parameters -> mvbdu -> unit
@@ -426,15 +428,14 @@ module Make (_ : Nul) : Mvbdu with type key = int and type value = int = struct
     'input ->
     Exception.exceptions_caught_and_uncaught * handler * 'output
 
-    type ('input, 'output) unary_with_threshold =
+  type ('input, 'output) unary_with_threshold =
     Remanent_parameters_sig.parameters ->
     handler ->
     Exception.exceptions_caught_and_uncaught ->
-    threshold:int -> 
+    threshold:int ->
     'input ->
     Exception.exceptions_caught_and_uncaught * handler * 'output
 
-
   type ('input1, 'input2, 'output) binary =
     Remanent_parameters_sig.parameters ->
     handler ->
@@ -584,9 +585,8 @@ module Make (_ : Nul) : Mvbdu with type key = int and type value = int = struct
     | error, (handler, a) -> error, handler, a
 
   let lift1__with_threshold ~threshold _string f parameters handler error a =
-      match f parameters handler error ~threshold a with
-      | error, (handler, a) -> error, handler, a
-  
+    match f parameters handler error ~threshold a with
+    | error, (handler, a) -> error, handler, a
 
   let lift1four buildlist pos f parameters handler error a =
     match f parameters error handler a with
@@ -776,10 +776,11 @@ module Make (_ : Nul) : Mvbdu with type key = int and type value = int = struct
     lift1__ __POS__ Boolean_mvbdu.extensional_description_of_mvbdu parameters
       handler error mvbdu
 
-  let parametric_conditions_of_mvbdu parameters handler error ~threshold mvbdu = 
-    lift1__with_threshold ~threshold __POS__ Boolean_mvbdu.extensional_description_of_mvbdu_with_threshold parameters
-          handler error mvbdu
-    
+  let parametric_conditions_of_mvbdu parameters handler error ~threshold mvbdu =
+    lift1__with_threshold ~threshold __POS__
+      Boolean_mvbdu.extensional_description_of_mvbdu_with_threshold parameters
+      handler error mvbdu
+
   let print = Boolean_mvbdu.print_mvbdu
   let print_association_list = List_algebra.print_association_list
   let print_variables_list = List_algebra.print_variables_list

core/KaSa_rep/abstract_domains/mvbdu/mvbdu_wrapper.mli

@@ -47,11 +47,11 @@ module type Mvbdu = sig
     'input ->
     Exception.exceptions_caught_and_uncaught * handler * 'output
 
-    type ('input, 'output) unary_with_threshold =
+  type ('input, 'output) unary_with_threshold =
     Remanent_parameters_sig.parameters ->
     handler ->
-    Exception.exceptions_caught_and_uncaught -> 
-    threshold:int -> 
+    Exception.exceptions_caught_and_uncaught ->
+    threshold:int ->
     'input ->
     Exception.exceptions_caught_and_uncaught * handler * 'output
 
@@ -207,7 +207,8 @@ module type Mvbdu = sig
 
   val extensional_of_mvbdu : (mvbdu, (key * value) list list) unary
 
-  val parametric_conditions_of_mvbdu:   (mvbdu, ((key * value) list*mvbdu) list) unary_with_threshold
+  val parametric_conditions_of_mvbdu :
+    (mvbdu, ((key * value) list * mvbdu) list) unary_with_threshold
 
   val variables_list_of_mvbdu : (mvbdu, hconsed_variables_list) unary
   val print : Remanent_parameters_sig.parameters -> mvbdu -> unit

core/KaSa_rep/reachability_analysis/views_domain.ml

@@ -763,18 +763,18 @@ module Domain = struct
           bdu_diff
       in
       let error, handler, split_list =
-        Ckappa_sig.Views_bdu.parametric_conditions_of_mvbdu parameters handler error
-          ~threshold:3 (* TO DO *)
-           bdu_diff
+        Ckappa_sig.Views_bdu.parametric_conditions_of_mvbdu parameters handler
+          error ~threshold:3 (* TO DO *)
+          bdu_diff
       in
-      let _ = split_list in 
-      
+      let _ = split_list in
+
       let dynamic = set_mvbdu_handler handler dynamic in
       (*----------------------------------------------------*)
       (*print function for extentional description*)
       let error =
         List.fold_left
-          (fun error l (* (l,bdd) *)->
+          (fun error l (* (l,bdd) *) ->
             let error, bool =
               List.fold_left
                 (fun (error, bool) (site_type, state) ->