Not much. Still does not work very well.

6 files changed, 56 insertions, 59 deletions

diff --git a/abstract/abs_domain.ml b/abstract/abs_domain.ml
index 64eefc7..d6ff489 100644
--- a/abstract/abs_domain.ml
+++ b/abstract/abs_domain.ml
@@ -131,7 +131,7 @@ module D (ND : NUMERICAL_ENVIRONMENT_DOMAIN) : ENVIRONMENT_DOMAIN = struct
                   if i > 0 then Format.fprintf fmt ",@ ";
                   Format.fprintf fmt "%a" Formula_printer.print_id id)
                 ids;
-              Format.fprintf fmt " = %s@]" v)
+              Format.fprintf fmt " ≡ %s@]" v)
             sbl;
           Format.fprintf fmt " }@]"
 
@@ -171,16 +171,23 @@ module D (ND : NUMERICAL_ENVIRONMENT_DOMAIN) : ENVIRONMENT_DOMAIN = struct
     let strict value =
         VMap.filter (fun _ v -> not (ND.is_bot v)) value
 
-    let add_case x (enum, num) =
+    let add_case_w widen 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
+          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
+            try VMap.add enum
+              ((if widen then ND.widen else ND.join) (VMap.find enum value) num)
+              value
             with Not_found -> VMap.add enum num value
         in { x with value = v }
+    let add_case = add_case_w false
 
     let addvar x id ty = match ty with
         | TInt | TReal ->
@@ -252,18 +259,18 @@ module D (ND : NUMERICAL_ENVIRONMENT_DOMAIN) : ENVIRONMENT_DOMAIN = struct
     let join x y =
         VMap.fold
           (fun enum num value -> add_case value (enum, num))
-          x.value
-          y
+          y.value
+          x
     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 }
+        let value = VMap.merge
+          (fun _ a b -> match a, b with
+            | Some x, None -> Some x
+            | None, Some y -> Some y
+            | Some x, Some y -> Some (ND.widen x y)
+            | _ -> None)
+          x.value y.value
+        in { x with value = value }
 
     (* Some cases of subset/equality not detected *)
     let subset a b =
@@ -281,13 +288,9 @@ module D (ND : NUMERICAL_ENVIRONMENT_DOMAIN) : ENVIRONMENT_DOMAIN = struct
         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)
+              | i, EItem u ->
+                  begin try let v = VarMap.find i enum in
+                    if (if op = E_EQ then u = v else u <> v)
                       then add_case value (enum, num)
                       else value
                   with Not_found ->
@@ -300,11 +303,11 @@ module D (ND : NUMERICAL_ENVIRONMENT_DOMAIN) : ENVIRONMENT_DOMAIN = struct
                           value
                           (List.filter ((<>) u) (List.assoc i x.evars))
                   end
-              | EIdent i, EIdent j ->
+              | 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)
+                        if (if op = E_EQ then x = y else x <> y)
                           then add_case value (enum, num)
                           else value
                       with Not_found (* J not found *) ->
diff --git a/abstract/abs_interp.ml b/abstract/abs_interp.ml
index 383a69c..a610843 100644
--- a/abstract/abs_interp.ml
+++ b/abstract/abs_interp.ml
@@ -111,14 +111,14 @@ end = struct
       let rec iter n i =
         let i' =
           if n < st.widen_delay
-            then E.join i (fsharp st.cl_g i)
+            then E.join i (fsharp st.cl i)
             else E.widen i (fsharp st.cl_g i)
         in
         if E.eq i i' then i else iter (n+1) i'
       in
 
       let x = iter 0 acc0 in
-      let y = fix E.eq (fsharp st.cl_g) x in    (* decreasing iteration *)
+      let y = fix E.eq (fsharp st.cl) x in    (* decreasing iteration *)
       let z = E.apply_cl y st.cl in             (* no more guarantee *)
       y, z
 
diff --git a/abstract/formula.ml b/abstract/formula.ml
index 62acb28..cb7a4c4 100644
--- a/abstract/formula.ml
+++ b/abstract/formula.ml
@@ -34,7 +34,7 @@ type enum_expr =
 type enum_op =
   | E_EQ | E_NE
 
-type enum_cons = enum_op * enum_expr * enum_expr
+type enum_cons = enum_op * id * enum_expr
 
 type bool_expr =
   (* constants *)
@@ -62,10 +62,10 @@ let f_or a b = match a, b with
   | a, BConst false -> a
   | a, b -> BOr(a, b)
 
-let f_e_eq a b = match a, b with
-  | EItem u, EItem v -> BConst (u = v)
-  | _ -> BEnumCons(E_EQ, a, b)
-
+let f_e_op op a b = match a, b with
+  | EItem i, EItem j -> BConst (if op = E_EQ then i = j else i <> j)
+  | EIdent x, v | v, EIdent x -> BEnumCons(op, x, v)
+let f_e_eq = f_e_op E_EQ
 
 (* Write all formula without using the NOT operator *)
 
diff --git a/abstract/formula_printer.ml b/abstract/formula_printer.ml
index 0c7d65e..383500c 100644
--- a/abstract/formula_printer.ml
+++ b/abstract/formula_printer.ml
@@ -68,7 +68,7 @@ let str_of_enum_op = function
 
 let print_econs fmt (op, a, b) =
     Format.fprintf fmt "%a %s %a"
-      print_enum_expr a (str_of_enum_op op) print_enum_expr b
+      print_id a (str_of_enum_op op) print_enum_expr b
 
 (* Print boolean form of formula *)
 
diff --git a/abstract/nonrelational.ml b/abstract/nonrelational.ml
index bbdc875..6497760 100644
--- a/abstract/nonrelational.ml
+++ b/abstract/nonrelational.ml
@@ -104,11 +104,7 @@ module ND (V : VALUE_DOMAIN) : NUMERICAL_ENVIRONMENT_DOMAIN = struct
     let eq a b = match a, b with
         | Bot, Bot -> true
         | Env m, Env n ->
-            VarMap.for_all2o
-                (fun _ _ -> false)
-                (fun _ _ -> false)
-                (fun _ a b -> a = b)
-                m n
+            VarMap.equal (=) m n
         | _ -> false
 
     (* Apply some formula to the environment *)
diff --git a/abstract/transform.ml b/abstract/transform.ml
index 6fa1277..b6781a8 100644
--- a/abstract/transform.ml
+++ b/abstract/transform.ml
@@ -136,7 +136,7 @@ and f_of_bexpr td (node, prefix) where expr =
               | AST_EQ -> E_EQ
               | AST_NE -> E_NE
               | _ -> type_error "Invalid operator on enumerated values."
-            in BEnumCons(eop, x, y)
+            in f_e_op eop x y
           | _ -> invalid_arity "Binary operator")
         (AST_tuple [a; b], snd expr))
   (* Temporal *)
@@ -233,12 +233,18 @@ let rec f_of_scope active td (node, prefix, eqs) assume_guarantees =
           BConst true
       in
         f_and (expr_eq e) assume_eq
-    | AST_guarantee (_, e) ->
+    | AST_guarantee ((id, _), e) ->
+      let gn = node^"/g_"^id in
       let guarantee_eq =
         if active && assume_guarantees then
-          f_of_expr td (node, prefix) e
+          f_and (f_of_expr td (node, prefix) e)
+                (BEnumCons(E_EQ, gn, EItem bool_true))
         else
-          BConst true
+          f_or
+            (f_and (f_of_expr td (node, prefix) e)
+                (BEnumCons(E_EQ, gn, EItem bool_true)))
+            (f_and (BNot (f_of_expr td (node, prefix) e))
+                (BEnumCons(E_EQ, gn, EItem bool_false)))
       in
         f_and (expr_eq e) guarantee_eq
     | AST_activate (b, _) ->
@@ -265,8 +271,8 @@ let rec f_of_scope active td (node, prefix, eqs) assume_guarantees =
       in
         f_and (cond_eq b) (if active then do_tree_act b else do_tree_inact b)
     | AST_automaton (aid, states, _) ->
-      let stv = EIdent (node^"/"^aid^".state") in
-      let nstv = EIdent ("N"^node^"/"^aid^".state") in
+      let stv = node^"/"^aid^".state" in
+      let nstv = "N"^node^"/"^aid^".state" in
       let st_eq_inact (st, _) =
         f_and
           (f_of_scope false td
@@ -304,13 +310,9 @@ let rec f_of_scope active td (node, prefix, eqs) assume_guarantees =
           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))
+        (if List.mem (node^"/") td.rp.init_scope
+          then f_e_eq (EIdent("N"^node^"/"^prefix^"init")) (EItem bool_false)
+          else BConst true)
     else
       f_and
         (if not (List.mem (node^"/") td.rp.no_time_scope)
@@ -318,14 +320,10 @@ let rec f_of_scope active td (node, prefix, eqs) assume_guarantees =
               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))
+        (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
@@ -364,7 +362,7 @@ let rec init_f_of_scope rp (node, prefix, eqs) =
       cond_eq b
     | AST_automaton (aid, states, _) ->
       let (st, _) = List.find (fun (st, _) -> st.initial) states in
-      let init_eq = BEnumCons(E_EQ, EIdent(node^"/"^aid^".state"), EItem st.st_name) in
+      let init_eq = BEnumCons(E_EQ, node^"/"^aid^".state", EItem st.st_name) in
       let state_eq (st, _) =
         let sc_f =
           init_f_of_scope rp (node, aid^"."^st.st_name^".", st.body)
@@ -421,7 +419,7 @@ let rec g_of_scope td (node, prefix, eqs) cond =
     | AST_automaton (aid, states, _) ->
       let st_g (st, _) =
         g_of_scope td (node, aid^"."^st.st_name^".", st.body)
-          (f_and cond (BEnumCons(E_EQ, EIdent(node^"/"^aid^".state"), EItem st.st_name)))
+          (f_and cond (BEnumCons(E_EQ, node^"/"^aid^".state", EItem st.st_name)))
       in
       List.flatten (List.map st_g states)
   in