Very buggy disjunction domain !

5 files changed, 363 insertions, 49 deletions

diff --git a/abstract/abs_domain.ml b/abstract/abs_domain.ml
index a7f5455..a30713a 100644
--- a/abstract/abs_domain.ml
+++ b/abstract/abs_domain.ml
@@ -4,6 +4,11 @@ open Num_domain
 open Typing
 open Util
 
+type disjunct_policy =
+  | DAlways
+  | DNever
+  | DSometimes
+
 module type ENVIRONMENT_DOMAIN = sig
     type t
     type itv
@@ -21,6 +26,7 @@ module type ENVIRONMENT_DOMAIN = sig
 
     val forgetvar         : t -> id -> t
     val var_itv           : t -> id -> itv
+    val set_disjunct      : t -> id -> disjunct_policy -> t
 
     (* set_theoretic operations *)
     val join              : t -> t -> t   (* union *)
@@ -33,7 +39,7 @@ module type ENVIRONMENT_DOMAIN = sig
     (* abstract operations *)
     val apply_f           : t -> bool_expr -> t
     val apply_cl          : t -> conslist -> t
-    val assign            : t -> (id * num_expr) list -> t
+    val assign            : t -> (id * id) list -> t
 
     (* pretty-printing *)
     val print_vars  : Format.formatter -> t -> id list -> unit
@@ -42,19 +48,13 @@ module type ENVIRONMENT_DOMAIN = sig
 
 end
 
-module D (ND : NUMERICAL_ENVIRONMENT_DOMAIN) : ENVIRONMENT_DOMAIN = struct
-
-    type enum_valuation = (string * string) list
-
-    module VMapKey = struct
-      type t = enum_valuation VarMap.t
-      let compare = VarMap.compare (fun a b -> Pervasives.compare (List.sort Pervasives.compare a) (List.sort Pervasives.compare b))
-    end
-    module VMap = Mapext.Make(VMapKey)
 
+module D_ignore_enum (ND : NUMERICAL_ENVIRONMENT_DOMAIN) : ENVIRONMENT_DOMAIN =
+struct
     type t = ND.t
     type itv = ND.itv
 
+
     let init = ND.init
     let bottom = ND.bottom
     let vbottom = ND.vbottom
@@ -66,6 +66,7 @@ module D (ND : NUMERICAL_ENVIRONMENT_DOMAIN) : ENVIRONMENT_DOMAIN = struct
 
     let forgetvar = ND.forgetvar
     let var_itv = ND.var_itv
+    let set_disjunct x _ _ = x
 
     let join = ND.join
     let meet = ND.meet
@@ -88,10 +89,295 @@ module D (ND : NUMERICAL_ENVIRONMENT_DOMAIN) : ENVIRONMENT_DOMAIN = struct
 
     let apply_f x f = apply_cl x (conslist_of_f f)
 
-    let assign = ND.assign
+    let assign x v = ND.assign x (List.map (fun (id, id2) -> id, NIdent id2) v)
 
     let print_vars = ND.print_vars
     let print_all = ND.print_all
     let print_itv = ND.print_itv
+end
+
+module D (ND : NUMERICAL_ENVIRONMENT_DOMAIN) : ENVIRONMENT_DOMAIN = struct
+
+    module Valuation = struct
+      type t = string VarMap.t
+      let compare = VarMap.compare Pervasives.compare
+
+      let subset a b =
+          VarMap.for_all
+            (fun id v ->
+                try v = VarMap.find id b
+                with Not_found -> true)
+            a
+
+      let print fmt x =
+          let b = List.map (fun (x, y) -> y, x) (VarMap.bindings x) in
+          let s = List.sort Pervasives.compare b in
+          let rec bl = function
+            | [] -> []
+            | (v, id)::q ->
+              begin match bl q with
+              | (vv, ids)::q when vv = v -> (v, id::ids)::q
+              | r -> (v, [id])::r
+              end
+          in
+          let sbl = bl s in
+          Format.fprintf fmt "@[<v 2>{ ";
+          List.iteri
+            (fun j (v, ids) ->
+              if j > 0 then Format.fprintf fmt "@ ";
+              Format.fprintf fmt "@[<hov 4>";
+              List.iteri
+                (fun i id ->
+                  if i > 0 then Format.fprintf fmt ",@ ";
+                  Format.fprintf fmt "%a" Formula_printer.print_id id)
+                ids;
+              Format.fprintf fmt " = %s@]" v)
+            sbl;
+          Format.fprintf fmt " }@]"
+
+    end
+    module VMap = Mapext.Make(Valuation)
+
+    type t = {
+        nvars     : (id * bool) list;
+        evars     : (id * string list) list;
+        nd_init   : ND.t;
+        nd_bottom : ND.t;
+        value     : ND.t VMap.t;
+        disj_v    : id list;
+        nodisj_v  : id list;
+    }
+    type itv =
+      | IN of ND.itv VMap.t
+      | IE of SSet.t
+
+
+    let init = {
+        nvars = []; evars = []; disj_v = []; nodisj_v = [];
+        nd_init = ND.init;
+        nd_bottom = ND.bottom;
+        value = VMap.singleton VarMap.empty ND.init;
+      }
+    let bottom = {
+        nvars = []; evars = []; disj_v = []; nodisj_v = [];
+        nd_init = ND.init;
+        nd_bottom = ND.bottom;
+        value = VMap.empty;
+      }
+    let vbottom x = { x with value = VMap.empty }
+    
+    let is_bot x = VMap.is_empty x.value || VMap.for_all (fun _ v -> ND.is_bot v) x.value
+
+    let strict value =
+        VMap.filter (fun _ v -> not (ND.is_bot v)) value
+
+    let add_case x (enum, num) =
+        let value = x.value in
+        let enum = VarMap.filter (fun k v -> not (List.mem k x.nodisj_v)) enum in
+        let v = 
+          if VMap.exists (fun e0 n0 -> Valuation.subset enum e0 && ND.subset num n0) value || ND.is_bot num then
+            value
+          else
+            try VMap.add enum (ND.join num (VMap.find enum value)) value
+            with Not_found -> VMap.add enum num value
+        in { x with value = v }
+
+    let addvar x id ty = match ty with
+        | TInt | TReal ->
+          let is_real = (ty = TReal) in
+          { x with
+            nvars     = (id, is_real)::(x.nvars);
+            nd_init   = ND.addvar x.nd_init id is_real;
+            nd_bottom = ND.addvar x.nd_bottom id is_real;
+            value     = VMap.map (fun v -> ND.addvar v id is_real) x.value
+          }
+        | TEnum options ->
+          { x with
+            evars     = (id, options)::x.evars
+          }
+
+    let vars x =
+        List.map (fun (id, r) -> id, if r then TReal else TInt) x.nvars @
+        List.map (fun (id, o) -> id, TEnum o) x.evars
+
+    let forgetvar x id =
+        if List.mem_assoc id x.evars then
+          VMap.fold
+              (fun enum num value ->
+                let enum' = VarMap.remove id enum in
+                add_case value (enum', num))
+              x.value
+              { x with value = VMap.empty }
+        else
+          { x with value = strict @@ VMap.map (fun v -> ND.forgetvar v id) x.value }
+
+    let rmvar x id =
+        if List.mem_assoc id x.evars then
+          let y = forgetvar x id in
+          { y with
+            evars = List.remove_assoc id x.evars }
+        else
+          { x with
+            nvars = List.remove_assoc id x.nvars;
+            value = strict @@ VMap.map (fun v -> ND.rmvar v id) x.value }
+
+    let var_itv x id =
+        if List.mem_assoc id x.nvars
+          then IN (VMap.map (fun v -> ND.var_itv v id) x.value)
+          else not_implemented "var_itv for enum variable"
+
+    let set_disjunct x id p =
+        { x with
+          disj_v = (if p = DAlways then id::x.disj_v
+                      else List.filter ((<>) id) x.disj_v);
+          nodisj_v = (if p = DNever then id::x.nodisj_v
+                      else List.filter ((<>) id) x.nodisj_v);
+        }
+
+    let join x y =
+        VMap.fold
+          (fun enum num value -> add_case value (enum, num))
+          x.value
+          y
+    let meet x y = not_implemented "meet for enum+num domain"
+    let widen x y =
+        { x with
+          value = VMap.merge
+            (fun _ a b -> match a, b with
+              | None, Some a -> Some a
+              | Some a, None -> Some a
+              | Some a, Some b -> Some (ND.widen a b)
+              | _ -> assert false)
+            x.value y.value }
+
+    (* Some cases of subset/equality not detected *)
+    let subset a b =
+        VMap.for_all
+          (fun enum num ->
+              VMap.exists
+                (fun enum_b num_b ->
+                  Valuation.subset enum enum_b && ND.subset num num_b)
+                b.value)
+          a.value
+    let eq a b = subset a b && subset b a
+
+    (* Constraints ! *)
+    let apply_ec x (op, a, b) =
+        VMap.fold
+            (fun enum num value ->
+              match a, b with
+              | EItem x, EItem y ->
+                  if (x = y && op = E_EQ) || (x <> y && op = E_NE)
+                    then add_case value (enum, num)
+                    else value
+              | EItem u, EIdent i | EIdent i, EItem u ->
+                  begin try let y = VarMap.find i enum in
+                    if (u = y && op = E_EQ) || (u <> y && op = E_NE)
+                      then add_case value (enum, num)
+                      else value
+                  with Not_found ->
+                    if op = E_EQ
+                      then add_case value (VarMap.add i u enum, num)
+                      else (* MAKE A DISJUNCTION *)
+                        List.fold_left
+                          (fun value item ->
+                              add_case value (VarMap.add i item enum, num))
+                          value
+                          (List.filter ((<>) u) (List.assoc i x.evars))
+                  end
+              | EIdent i, EIdent j ->
+                  begin
+                    try let x = VarMap.find i enum in
+                      try let y = VarMap.find j enum in
+                        if (x = y && op = E_EQ) || (x <> y && op = E_NE)
+                          then add_case value (enum, num)
+                          else value
+                      with Not_found (* J not found *) ->
+                        add_case value (VarMap.add j x enum, num)
+                    with Not_found (* I not found *) ->
+                      try let y = VarMap.find j enum in
+                        add_case value (VarMap.add i y enum, num)
+                      with Not_found (* J not found *) ->
+                        if op = E_EQ
+                        then (* MAKE A DISJUNCTION ! *)
+                            List.fold_left
+                              (fun value item ->
+                                let enum = VarMap.add i item enum in
+                                let enum = VarMap.add j item enum in
+                                add_case value (enum, num))
+                              value
+                              (List.assoc i x.evars)
+                        else
+                          add_case value (enum, num)
+                  end)
+            x.value
+            { x with value = VMap.empty }
+
+    let apply_ecl x cons =
+        let f x = List.fold_left apply_ec x cons in
+        fix eq f x
+            
+
+    let apply_ncl x econs =
+        { x with value = strict @@ VMap.map (fun x -> ND.apply_ncl x econs) x.value }
+
+    let rec apply_cl x (econs, ncons, rest) = match rest with
+        | CLTrue ->
+          let y = apply_ecl x econs in
+          let z = apply_ncl y ncons in
+          z
+        | CLFalse -> vbottom x
+        | CLAnd(a, b) ->
+          let y = apply_cl x (econs, ncons, a) in
+          apply_cl y (econs, ncons, b)
+        | CLOr((eca, ca, ra), (ecb, cb, rb)) ->
+          let y = apply_cl x (econs@eca, ncons@ca, ra) in
+          let z = apply_cl x (econs@ecb, ncons@cb, rb) in
+          join y z
+
+    let apply_f x f = apply_cl x (conslist_of_f f)
+
+    let assign x e =
+      let ee, ne = List.partition (fun (id, id2) -> List.mem_assoc id x.evars) e in
+      let ne_e = List.map (fun (id, id2) -> id, NIdent id2) ne in
+
+      VMap.fold
+          (fun enum0 num value ->
+              let enum = List.fold_left
+                  (fun enum (id, id2) ->
+                      try let y = VarMap.find id2 enum0 in
+                        VarMap.add id y enum
+                      with Not_found ->
+                        VarMap.remove id enum)
+                  enum0 ee
+              in
+              add_case value (enum, ND.assign num ne_e))
+          x.value
+          { x with value = VMap.empty }
+
+    let print_all fmt x =
+        Format.fprintf fmt "@[<v 0>";
+        VMap.iter
+          (fun enum num ->
+            Format.fprintf fmt "@[<hv 2>{ %a ∧@ %a }@]@ "
+              Valuation.print enum ND.print_all num)
+          x.value;
+        Format.fprintf fmt "@]"
+
+    let print_vars fmt x idl = print_all fmt x (* TODO *)
+
+    let print_itv fmt = function
+        | IN x ->
+          Format.fprintf fmt "@[<v 0>";
+          VMap.iter
+            (fun enum i ->
+              Format.fprintf fmt "%a when %a@ "
+                ND.print_itv i Valuation.print enum)
+            x;
+          Format.fprintf fmt "@]"
+        | IE x ->
+          Format.fprintf fmt "@[<hov 2>{ ";
+          SSet.iter (fun x -> Format.fprintf fmt "%s@ " x) x;
+          Format.fprintf fmt "}@]"
 
 end
diff --git a/abstract/abs_interp.ml b/abstract/abs_interp.ml
index 7950144..7a53134 100644
--- a/abstract/abs_interp.ml
+++ b/abstract/abs_interp.ml
@@ -52,6 +52,7 @@ end = struct
         guarantees;
       Format.printf "@.";
 
+      let env = E.set_disjunct env "/exit" DNever in
       let env = E.apply_f env init_f in
 
       let cl = Formula.conslist_of_f f in
@@ -72,7 +73,7 @@ end = struct
       let tr_assigns = List.fold_left
         (fun q (_, id, _) ->
             if id.[0] = 'N' then
-              (String.sub id 1 (String.length id - 1), NIdent id)::q
+              (String.sub id 1 (String.length id - 1), id)::q
             else
               q)
         [] vars
@@ -95,14 +96,10 @@ end = struct
     (*
       loop : st -> env -> env -> env
     *)
-    let loop st pnew stay =
+    let loop st acc0 =
 
-      Format.printf "Loop @[<hv>%a@]@.New @[<hv>%a@]@.Stay @[<hv>%a@]@."
-        Formula_printer.print_conslist st.cl
-        E.print_all pnew E.print_all stay;
-
-      let add_stay = cycle st st.cl pnew in
-      let acc0 = E.join stay add_stay in
+      Format.printf "Loop @[<hv>%a@]@.@."
+        Formula_printer.print_conslist st.cl;
 
       let fsharp cl i = 
         Format.printf "Acc @[<hv>%a@]@." E.print_all i;
@@ -121,7 +118,7 @@ end = struct
 
       let x = iter 0 acc0 in
       let y = fix E.eq (fsharp st.cl_g) x in    (* decreasing iteration *)
-      let z = E.apply_cl y st.cl in
+      let z = E.apply_cl y st.cl in             (* no more guarantee *)
       y, z
 
     (*
@@ -130,20 +127,14 @@ end = struct
     let do_prog widen_delay rp =
       let st = init_state widen_delay rp in
 
-      let pnew = st.env in
-      let pnew_c = E.apply_cl pnew st.cl in
-
-      let stay, stay_c = loop st pnew (E.vbottom pnew) in
-
-      Format.printf "@.@[<hov>New %a@]@.@."
-        E.print_all pnew_c;
-      Format.printf "@[<hov>Stay %a@]@.@."
-        E.print_all stay_c;
-
-      let final = E.join pnew_c stay_c in
+      let final, final_c = loop st st.env in
 
-      Format.printf "@[<hov>Final %a@]@.@."
+      Format.printf "@[<hov>F %a@]@.@."
         E.print_all final;
+      (*
+      Format.printf "@[<hov>F' %a@]@.@."
+        E.print_all final_c;
+      *)
 
       let check_guarantee (id, f) =
         let cl = Formula.conslist_of_f f in
@@ -162,9 +153,9 @@ end = struct
       end;
 
       if List.exists (fun (p, _, _) -> p) st.rp.all_vars then begin
-        Format.printf "Probes:@[<v>";
+        Format.printf "Probes: @[<v 0>";
         List.iter (fun (p, id, _) ->
-          if p then Format.printf " %a ∊ %a@ "
+          if p then Format.printf "%a ∊ %a@ "
                 Formula_printer.print_id id
                 E.print_itv (E.var_itv final id))
           st.rp.all_vars;
diff --git a/abstract/formula_printer.ml b/abstract/formula_printer.ml
index 44f2d39..0c7d65e 100644
--- a/abstract/formula_printer.ml
+++ b/abstract/formula_printer.ml
@@ -59,7 +59,7 @@ let rec print_num_expr fmt e = match e with
 
 (* Enumeated expressions *)
 let print_enum_expr fmt = function
-  | EIdent id -> Format.fprintf fmt "%s" id
+  | EIdent id -> print_id fmt id
   | EItem x -> Format.fprintf fmt "%s" x
 
 let str_of_enum_op = function
diff --git a/abstract/nonrelational.ml b/abstract/nonrelational.ml
index 492b547..bbdc875 100644
--- a/abstract/nonrelational.ml
+++ b/abstract/nonrelational.ml
@@ -188,7 +188,6 @@ module ND (V : VALUE_DOMAIN) : NUMERICAL_ENVIRONMENT_DOMAIN = struct
         match env with
         | Bot -> Format.fprintf fmt "⊥"
         | Env env ->
-            Format.fprintf fmt "@[<v 2>{ ";
             let l = List.map (fun id -> (get_var env id, id)) ids in
             let s = List.sort Pervasives.compare l in
             let rec bl = function
@@ -201,6 +200,7 @@ module ND (V : VALUE_DOMAIN) : NUMERICAL_ENVIRONMENT_DOMAIN = struct
               | _::q -> bl q
             in
             let sbl = bl s in
+            Format.fprintf fmt "@[<v 2>{ ";
             List.iteri
               (fun j (v, ids) ->
                 if j > 0 then Format.fprintf fmt "@ ";
diff --git a/abstract/transform.ml b/abstract/transform.ml
index 708456e..64fd8d8 100644
--- a/abstract/transform.ml
+++ b/abstract/transform.ml
@@ -70,11 +70,19 @@ let rec f_of_neexpr td (node, prefix) where expr =
               | TEnum _ -> EE(EIdent x))
           typ)
   | AST_arrow(a, b) ->
-    f_or
-      (f_and (BRel(AST_EQ, NIdent(node^"/"^prefix^"time"), NIntConst 0))
-        (sub where a))
-      (f_and (BRel(AST_GE, NIdent(node^"/"^prefix^"time"), NIntConst 1))
-        (sub where b))
+    if List.mem (node^"/") td.rp.init_scope
+    then
+      f_or
+        (f_and (f_e_eq (EIdent (node^"/"^prefix^"init")) (EItem bool_true))
+          (sub where a))
+        (f_and (f_e_eq (EIdent (node^"/"^prefix^"init")) (EItem bool_false))
+          (sub where b))
+    else
+      f_or
+        (f_and (BRel(AST_EQ, NIdent(node^"/"^prefix^"time"), NIntConst 0))
+          (sub where a))
+        (f_and (BRel(AST_GE, NIdent(node^"/"^prefix^"time"), NIntConst 1))
+          (sub where b))
   (* other *)
   | AST_if(c, a, b) ->
     f_or
@@ -261,12 +269,33 @@ let rec f_of_scope active td (node, prefix, eqs) assume_guarantees =
   in
   let time_incr_eq =
     if active then
-      BRel(AST_EQ, NIdent("N"^node^"/"^prefix^"time"),
-          NBinary(AST_PLUS, NIntConst 1, NIdent(node^"/"^prefix^"time")))
+      f_and
+        (if not (List.mem (node^"/") td.rp.no_time_scope)
+          then BRel(AST_EQ, NIdent("N"^node^"/"^prefix^"time"),
+              NBinary(AST_PLUS, NIntConst 1, NIdent(node^"/"^prefix^"time")))
+          else BConst true)
+        (f_and
+          (if List.mem (node^"/") td.rp.act_scope
+            then f_e_eq (EIdent(node^"/"^prefix^"act")) (EItem bool_true)
+            else BConst true)
+          (if List.mem (node^"/") td.rp.init_scope
+            then f_e_eq (EIdent("N"^node^"/"^prefix^"init")) (EItem bool_false)
+            else BConst true))
     else
-      BRel(AST_EQ,
-          NIdent("N"^node^"/"^prefix^"time"),
-          NIdent(node^"/"^prefix^"time"))
+      f_and
+        (if not (List.mem (node^"/") td.rp.no_time_scope)
+          then BRel(AST_EQ,
+              NIdent("N"^node^"/"^prefix^"time"),
+              NIdent(node^"/"^prefix^"time"))
+          else BConst true)
+        (f_and
+          (if List.mem (node^"/") td.rp.act_scope
+            then f_e_eq (EIdent(node^"/"^prefix^"act")) (EItem bool_false)
+            else BConst true)
+          (if List.mem (node^"/") td.rp.init_scope
+            then f_e_eq (EIdent("N"^node^"/"^prefix^"init"))
+                  (EIdent (node^"/"^prefix^"init"))
+            else BConst true))
   in
   List.fold_left f_and
     time_incr_eq
@@ -306,9 +335,17 @@ let rec init_f_of_scope rp (node, prefix, eqs) =
     | AST_automaton _ -> not_implemented "f_of_scope do_eq automaton"
   in
   let time_eq =
-    BRel(AST_EQ,
-        NIdent(node^"/"^prefix^"time"),
-        NIntConst 0)
+    f_and
+      (if not (List.mem (node^"/") rp.no_time_scope)
+        then
+          BRel(AST_EQ,
+            NIdent(node^"/"^prefix^"time"),
+            NIntConst 0)
+        else BConst true)
+      (if List.mem (node^"/") rp.init_scope
+        then
+          f_e_eq (EIdent(node^"/"^prefix^"init")) (EItem bool_true)
+        else BConst true)
   in
   List.fold_left f_and time_eq (List.map do_eq eqs)