Use LAST instead of NEXT (only EDD implementation works at the moment)

4 files changed, 164 insertions, 154 deletions

diff --git a/abstract/abs_interp.ml b/abstract/abs_interp.ml
index c3db657..26b788b 100644
--- a/abstract/abs_interp.ml
+++ b/abstract/abs_interp.ml
@@ -2,17 +2,12 @@ open Ast
 open Ast_util
 open Formula
 open Typing
+open Cmdline
 
 open Util
 open Num_domain
 open Enum_domain
 
-type cmdline_opt = {
-    widen_delay       : int;
-    disjunct          : (id -> bool);
-    verbose_ci        : bool;
-    vverbose_ci       : bool;
-}
 
 
 module I (ED : ENUM_ENVIRONMENT_DOMAIN) (ND : NUMERICAL_ENVIRONMENT_DOMAIN) : sig
diff --git a/abstract/abs_interp_edd.ml b/abstract/abs_interp_edd.ml
index 6220a0a..c1fb905 100644
--- a/abstract/abs_interp_edd.ml
+++ b/abstract/abs_interp_edd.ml
@@ -2,10 +2,10 @@ open Ast
 open Ast_util
 open Formula
 open Typing
+open Cmdline
 
 open Util
 open Num_domain
-open Abs_interp
 
 
 
@@ -592,9 +592,12 @@ end = struct
         rp            : rooted_prog;
         opt           : cmdline_opt;
 
+        last_vars     : (bool * id * typ) list;
+        all_vars      : (bool * id * typ) list;
         ve            : varenv;
 
         (* program expressions *)
+        init_f        : bool_expr;
         cl            : conslist;
         cl_g          : conslist;
         guarantees    : (id * bool_expr) list;
@@ -602,7 +605,6 @@ end = struct
         (* abstract interpretation *)
         cycle         : (id * id * typ) list;     (* s'(x) = s(y) *)
         forget        : (id * typ) list;          (* s'(x) not specified *)
-        mutable data  : edd_v;
     }
 
 
@@ -924,20 +926,33 @@ end = struct
       init_env : cmdline_opt -> rooted_prog -> env
     *)
     let init_env opt rp =
+        let init_f, f = Transform.f_of_prog rp false in
+        let _, f_g = Transform.f_of_prog rp true in
+        Format.printf "Init formula:@.%a@.@." Formula_printer.print_expr init_f;
+        Format.printf "Cycle formula:@.%a@.@." Formula_printer.print_expr f;
+
+        let cl = Formula.conslist_of_f f in
+        let cl_g = Formula.conslist_of_f f_g in
+        Format.printf "Cycle conslist:@.%a@.@." Formula_printer.print_conslist cl;
+
+        let last_vars = uniq_sorted (List.sort compare (Transform.extract_last_vars f_g)) in
+        let last_vars = List.map
+          (fun id ->
+            let (_, _, ty) = List.find (fun (_, u, _) -> id = "L"^u) rp.all_vars
+              in false, id, ty)
+          last_vars in
+        let all_vars = last_vars @ rp.all_vars in
+
         Format.printf "Vars: @[<hov>%a@]@.@."
             (print_list Ast_printer.print_typed_var ", ")
-            rp.all_vars;
+            all_vars;
 
         let num_vars, enum_vars = List.fold_left
             (fun (nv, ev) (_, id, t) -> match t with
                 | TEnum ch -> nv, (id, ch)::ev
                 | TInt -> (id, false)::nv, ev
                 | TReal -> (id, true)::nv, ev)
-            ([], []) rp.all_vars in
-
-        let init_f = Transform.init_f_of_prog rp in
-        Format.printf "Init formula: %a@.@." Formula_printer.print_expr init_f;
-        let init_cl = conslist_of_f init_f in
+            ([], []) all_vars in
 
         let guarantees = Transform.guarantees_of_prog rp in
         Format.printf "Guarantees:@.";
@@ -946,19 +961,10 @@ end = struct
           guarantees;
         Format.printf "@.";
 
-        let f = Formula.eliminate_not (Transform.f_of_prog rp false) in
-        let f_g = Formula.eliminate_not (Transform.f_of_prog rp true) in
-        Format.printf "Cycle formula:@.%a@.@." Formula_printer.print_expr f;
-
-        let cl = Formula.conslist_of_f f in
-        let cl_g = Formula.conslist_of_f f_g in
-        Format.printf "Cycle conslist:@.%a@.@." Formula_printer.print_conslist cl;
-
         (* calculate order for enumerated variables *)
         let evars = List.map fst enum_vars in
 
-        let lv = extract_linked_evars_root init_cl
-            @ extract_linked_evars_root cl_g in
+        let lv = extract_linked_evars_root cl_g in
         let lv = uniq_sorted
              (List.sort Pervasives.compare (List.map ord_couple lv)) in
 
@@ -995,25 +1001,17 @@ end = struct
         (* calculate cycle variables and forget variables *)
         let cycle = List.fold_left
           (fun q (_, id, ty) ->
-              if id.[0] = 'N' then
-                (String.sub id 1 (String.length id - 1), id, ty)::q
+              if id.[0] = 'L' then
+                (id, String.sub id 1 (String.length id - 1), ty)::q
               else q)
-          [] rp.all_vars
-        in
-        let forget = List.map (fun (_, id, ty) -> (id, ty))
-            (List.filter
-              (fun (_, id, _) ->
-                not (List.exists (fun (_, id2, _) -> id2 = "N"^id) rp.all_vars))
-              rp.all_vars)
+          [] last_vars
         in
+        let forget = List.map (fun (_, id, ty) -> (id, ty)) rp.all_vars in
 
-        (* calculate initial environment *)
-        let data = edd_apply_cl (edd_top ve) init_cl in
-        Format.printf "Init: @[<hov>%a@]@." edd_print data;
 
-        { rp; opt; ve;
-          cl; cl_g; guarantees;
-          cycle; forget; data }
+        { rp; opt; ve; last_vars; all_vars;
+          init_f; cl; cl_g; guarantees;
+          cycle; forget }
 
           
 
@@ -1094,7 +1092,8 @@ end = struct
             end
         in
 
-        let init_acc = edd_star_new (edd_bot e.data.ve) e.data in
+        let init_acc = edd_star_new (edd_bot e.ve)
+            (pass_cycle e (edd_apply_cl (edd_top e.ve) (conslist_of_f e.init_f))) in
         
         (* Dump final state *)
         let acc = ch_it 0 init_acc in
@@ -1124,13 +1123,13 @@ end = struct
         end;
 
         (* Examine probes *)
-        if List.exists (fun (p, _, _) -> p) e.rp.all_vars then begin
+        if List.exists (fun (p, _, _) -> p) e.all_vars then begin
           let final_flat = edd_forget_vars final
             (List.fold_left
               (fun l (_, id, ty) -> match ty with
                 | TInt | TReal -> l
                 | TEnum _ -> id::l)
-              [] e.rp.all_vars) in
+              [] e.all_vars) in
           let final_flat = match final_flat.root with
             | DTop -> ND.top e.ve.nvars
             | DBot -> ND.bottom e.ve.nvars
@@ -1146,7 +1145,7 @@ end = struct
                 ND.print_itv (ND.project final_flat id)
             | TEnum _ -> Format.printf "%a : enum variable@."
                 Formula_printer.print_id id)
-            e.rp.all_vars;
+            e.all_vars;
           Format.printf "@]@."
         end
 
diff --git a/abstract/formula.ml b/abstract/formula.ml
index 01f6655..9c0ff71 100644
--- a/abstract/formula.ml
+++ b/abstract/formula.ml
@@ -51,7 +51,8 @@ type bool_expr =
   | BNot of bool_expr
 
 let f_and a b = match a, b with
-  | BConst false, _ | _, BConst false -> BConst false
+  | BConst false, _ | _, BConst false
+  | BNot (BConst true), _ | _, BNot (BConst true) -> BConst false
   | BConst true, b -> b
   | a, BConst true -> a
   | a, b -> BAnd(a, b)
diff --git a/abstract/transform.ml b/abstract/transform.ml
index dcb4049..1cbc27d 100644
--- a/abstract/transform.ml
+++ b/abstract/transform.ml
@@ -7,7 +7,14 @@ open Typing
 open Interpret  (* used for constant evaluation ! *)
 
 
-(* Transform SCADE program to logical formula. *)
+(* Transform SCADE program to logical formula.
+
+    Convention : to access the last value of a variable,
+    access the variable with the same name prefixed by "L".
+    A pre-processing pass will extract the variables that are
+    referenced in such a way so that they are taken into
+    account when calculating the memory.
+*)
 
 (* node * prefix * equations *)
 type scope = id * id * eqn ext list
@@ -72,7 +79,7 @@ let rec f_of_neexpr td (node, prefix, clock_scope) where expr =
     let typ = type_expr td.rp node expr in
       where
         (List.mapi
-          (fun i t -> let x = id^"."^(string_of_int i) in
+          (fun i t -> let x = "L"^id^"."^(string_of_int i) in
               match t with
               | TInt -> NE(NIdent x, false)
               | TReal -> NE(NIdent x, true)
@@ -190,40 +197,56 @@ and f_of_expr td (node, prefix, clock_scope) expr =
     Translate program into one big formula
 *)
 
+let reset_cond rst_exprs =
+  List.fold_left f_or (BConst false) rst_exprs
+let no_reset_cond rst_exprs =
+  List.fold_left (fun ff c -> f_and ff (BNot c)) (BConst true) rst_exprs
+
 let clock_scope_here (node, prefix, _) =
   node^"/"^prefix
 
-let gen_clock td (node, prefix, _) active =
+let gen_clock td (node, prefix, _) active rst_exprs =
   let clock_scope = node^"/"^prefix in
   let clock_eq =
-    if active then
-      f_and
-        (if not (td.rp.no_time_scope clock_scope)
-          then BRel(AST_EQ, NIdent("N"^clock_scope^"time"),
-              NBinary(AST_PLUS, NIntConst 1, NIdent(clock_scope^"time"), false),
-              false)
-          else BConst true)
-        (if td.rp.init_scope clock_scope
-          then f_e_eq (EIdent("N"^clock_scope^"init")) (EItem bool_false)
-          else BConst true)
-    else
-      f_and
-        (if not (td.rp.no_time_scope clock_scope)
-          then BRel(AST_EQ,
-              NIdent("N"^clock_scope^"time"),
-              NIdent(clock_scope^"time"), false)
-          else BConst true)
-        (if td.rp.init_scope clock_scope
-          then f_e_eq (EIdent("N"^clock_scope^"init"))
-                (EIdent (clock_scope^"init"))
-          else BConst true)
+    f_or
+      (f_and (reset_cond rst_exprs)
+        (f_and
+          (if not (td.rp.no_time_scope clock_scope)
+            then BRel(AST_EQ, NIdent(clock_scope^"time"), NIntConst 0, false)
+            else BConst true)
+          (if td.rp.init_scope clock_scope
+            then f_e_eq (EIdent(clock_scope^"init")) (EItem bool_true)
+            else BConst true)))
+      (f_and (no_reset_cond rst_exprs)
+        (if active then
+          f_and
+            (if not (td.rp.no_time_scope clock_scope)
+              then BRel(AST_EQ, NIdent(clock_scope^"time"),
+                  NBinary(AST_PLUS, NIntConst 1, NIdent("L"^clock_scope^"time"), false),
+                  false)
+              else BConst true)
+            (if td.rp.init_scope clock_scope
+              then f_e_eq (EIdent(clock_scope^"init")) (EItem bool_false)
+              else BConst true)
+        else
+          f_and
+            (if not (td.rp.no_time_scope clock_scope)
+              then BRel(AST_EQ,
+                  NIdent(clock_scope^"time"),
+                  NIdent("L"^clock_scope^"time"), false)
+              else BConst true)
+            (if td.rp.init_scope clock_scope
+              then f_e_eq (EIdent(clock_scope^"init"))
+                    (EIdent ("L"^clock_scope^"init"))
+              else BConst true)))
   in
-  clock_scope, clock_eq
+  (clock_scope, rst_exprs), clock_eq
 
-let rec f_of_scope active td (node, prefix, eqs) clock_scope assume_guarantees =
+let rec f_of_scope active td (node, prefix, eqs) (clock_scope, rst_exprs as cs) assume_guarantees =
   let expr_eq e =
     let instance_eq (_, id, eqs, args) =
-      let eq = f_of_scope active td (node^"/"^id, "", eqs) clock_scope assume_guarantees in
+      let eq = f_of_scope active td (node^"/"^id, "", eqs)
+          cs assume_guarantees in
       if active then
         let arg_eq ((_,argname,ty), expr) =
             f_of_neexpr td (node, prefix, clock_scope) (function
@@ -247,7 +270,7 @@ let rec f_of_scope active td (node, prefix, eqs) clock_scope assume_guarantees =
         f_of_neexpr td (node, prefix, clock_scope) (fun elist ->
             list_fold_op f_and
               (List.mapi
-                (fun i v -> let x = ("N"^id^"."^(string_of_int i)) in
+                (fun i v -> let x = (id^"."^(string_of_int i)) in
                   match v with
                   | NE (v, r) -> BRel(AST_EQ, NIdent x, v, r)
                   | EE v -> f_e_eq (EIdent x) v)
@@ -257,11 +280,11 @@ let rec f_of_scope active td (node, prefix, eqs) clock_scope assume_guarantees =
         let typ = type_expr td.rp node expr in
         list_fold_op f_and
           (List.mapi
-            (fun i t -> let x = string_of_int i in
+            (fun i t -> let id_x = id ^ "." ^ string_of_int i in
               match t with
-              | TInt -> BRel(AST_EQ, NIdent("N"^id^"."^x), NIdent (id^"."^x), false)
-              | TReal -> BRel(AST_EQ, NIdent("N"^id^"."^x), NIdent (id^"."^x), true)
-              | TEnum _ -> f_e_eq (EIdent("N"^id^"."^x)) (EIdent (id^"."^x)))
+              | TInt -> BRel(AST_EQ, NIdent(id_x), NIdent ("L"^id_x), false)
+              | TReal -> BRel(AST_EQ, NIdent(id_x), NIdent ("L"^id_x), true)
+              | TEnum _ -> f_e_eq (EIdent(id_x)) (EIdent ("L"^id_x)))
             typ)
     in
     let eq_p = f_and_list (List.map pre_expr (extract_pre e)) in
@@ -323,8 +346,8 @@ let rec f_of_scope active td (node, prefix, eqs) clock_scope assume_guarantees =
       let rec do_tree_act = function
         | AST_activate_body b ->
             let b_scope = node, b.act_id^".", b.body in
-            let clock_scope, clock_eq = gen_clock td b_scope true in
-            f_and clock_eq (f_of_scope true td b_scope clock_scope assume_guarantees)
+            let cs2, clock_eq = gen_clock td b_scope true rst_exprs in
+            f_and clock_eq (f_of_scope true td b_scope cs2 assume_guarantees)
         | AST_activate_if(c, a, b) ->
           f_or
             (f_and (f_of_expr td (node, prefix, clock_scope) c)
@@ -334,29 +357,37 @@ let rec f_of_scope active td (node, prefix, eqs) clock_scope assume_guarantees =
       and do_tree_inact = function
         | AST_activate_body b ->
             let b_scope = node, b.act_id^".", b.body in
-            let clock_scope, clock_eq = gen_clock td b_scope false in
-            f_and clock_eq (f_of_scope false td b_scope clock_scope assume_guarantees)
+            let cs2, clock_eq = gen_clock td b_scope false rst_exprs in
+            f_and clock_eq (f_of_scope false td b_scope cs2 assume_guarantees)
         | AST_activate_if(_, a, b) ->
           f_and (do_tree_inact a) (do_tree_inact b)
       in
         f_and (cond_eq b) (if active then do_tree_act b else do_tree_inact b)
     | AST_automaton (aid, states, _) ->
+      let (init_st, _) = List.find (fun (st, _) -> st.initial) states in
+      let lnstv = "L"^node^"/"^aid^".next_state" in
+      let nstv = node^"/"^aid^".next_state" in
       let stv = node^"/"^aid^".state" in
-      let nstv = "N"^node^"/"^aid^".state" in
+      let st_choice_eq =
+        f_or
+          (f_and (reset_cond rst_exprs) (f_e_eq (EIdent stv) (EItem init_st.st_name)))
+          (f_and (no_reset_cond rst_exprs) (f_e_eq (EIdent stv) (EIdent lnstv)))
+      in
+
       let st_eq_inact (st, _) =
         let st_scope = node, aid^"."^st.st_name^".", st.body in
-        let clock_scope, clock_eq = gen_clock td st_scope false in
+        let clock_scope, clock_eq = gen_clock td st_scope false rst_exprs in
         f_and clock_eq
           (f_and
-            (f_of_scope false td st_scope clock_scope assume_guarantees)
+            (f_of_scope false td st_scope cs assume_guarantees)
             (f_and_list (List.map (fun (c, _, _) -> expr_eq c) st.until)))
       in
       if active then
         let st_eq_act (st, l) =
           let act_eq =
             let st_scope = node, aid^"."^st.st_name^".", st.body in
-            let clock_scope, clock_eq = gen_clock td st_scope true in
-            let st_eq = f_and clock_eq (f_of_scope true td st_scope clock_scope assume_guarantees) in
+            let cs2, clock_eq = gen_clock td st_scope true rst_exprs in
+            let st_eq = f_and clock_eq (f_of_scope true td st_scope cs2 assume_guarantees) in
             let rec aux = function
               | [] -> BEnumCons(E_EQ, nstv, EItem st.st_name)
               | (c, (target, l), rst)::q ->
@@ -372,9 +403,11 @@ let rec f_of_scope active td (node, prefix, eqs) clock_scope assume_guarantees =
             (f_and (BEnumCons(E_NE, stv, EItem st.st_name))
               (st_eq_inact (st, l)))
         in
-        f_and_list (List.map st_eq_act states)
+        f_and st_choice_eq
+          (f_and_list (List.map st_eq_act states))
       else
-        f_and_list (List.map st_eq_inact states)
+        f_and st_choice_eq
+          (f_and_list (List.map st_eq_inact states))
   in
   f_and_list (List.map do_eq eqs)
 
@@ -384,77 +417,32 @@ and f_of_prog rp assume_guarantees =
       consts = I.consts rp;
     } in
 
-    let clock_scope, clock_eq = gen_clock td rp.root_scope true in
-
-    let scope_f = 
-      f_of_scope
-        true
-        td td.rp.root_scope
-        clock_scope
-        assume_guarantees in
-    f_and clock_eq scope_f
-      
+    let prog_normal =
+      let clock_scope, clock_eq = gen_clock td rp.root_scope true [] in
 
-(*
-    Translate init state into a formula
-*)
-let gen_clock_init rp (node, prefix, _) =
-  let clock_scope = node^"/"^prefix in
-  let time_eq =
-    f_and
-      (if not (rp.no_time_scope clock_scope)
-        then
-          BRel(AST_EQ,
-            NIdent(clock_scope^"time"),
-            NIntConst 0, false)
-        else BConst true)
-      (if rp.init_scope clock_scope
-        then
-          f_e_eq (EIdent(clock_scope^"init")) (EItem bool_true)
-        else BConst true)
-  in
-  clock_scope, time_eq
+      let scope_f = 
+        f_of_scope
+          true
+          td td.rp.root_scope
+          clock_scope
+          assume_guarantees in
+      f_and clock_eq scope_f
+    in
+    let prog_init =
+      let clock_scope, clock_eq =
+        gen_clock td rp.root_scope true [BConst true] in
 
-let rec init_f_of_scope rp (node, prefix, eqs) clock_scope =
-  let expr_eq e =
-    let instance_eq (_, id, eqs, args) =
-     init_f_of_scope rp (node^"/"^id, "", eqs) clock_scope
+      let scope_f = 
+        f_of_scope
+          true
+          td td.rp.root_scope
+          clock_scope
+          assume_guarantees in
+      f_and clock_eq scope_f
     in
-    List.fold_left (fun x i -> f_and (instance_eq i) x)
-      (BConst true) (extract_instances rp.p e)
-  in
-  let do_eq eq = match fst eq with
-    | AST_assign(_, e) | AST_assume(_, e) | AST_guarantee(_, e) ->
-        expr_eq e
-    | AST_activate (b, _) ->
-      let rec cond_eq = function
-        | AST_activate_body b ->
-          let bscope = (node, b.act_id^".", b.body) in
-          let clock_scope, clock_eq = gen_clock_init rp bscope in
-          f_and clock_eq (init_f_of_scope rp bscope clock_scope)
-        | AST_activate_if(c, a, b) ->
-          f_and (expr_eq c)
-            (f_and (cond_eq a) (cond_eq b))
-      in
-      cond_eq b
-    | AST_automaton (aid, states, _) ->
-      let (st, _) = List.find (fun (st, _) -> st.initial) states in
-      let init_eq = BEnumCons(E_EQ, node^"/"^aid^".state", EItem st.st_name) in
-      let state_eq (st, _) =
-        let sc_f =
-          let st_scope = (node, aid^"."^st.st_name^".", st.body) in
-          let clock_scope, clock_eq = gen_clock_init rp st_scope in
-          f_and clock_eq (init_f_of_scope rp st_scope clock_scope)
-        in List.fold_left (fun f (c, _, _) -> f_and f (expr_eq c)) sc_f st.until
-      in
-      List.fold_left f_and init_eq
-        (List.map state_eq states)
-  in
-  f_and_list (List.map do_eq eqs)
+      prog_init, prog_normal
+      
 
-and init_f_of_prog rp =
-    let clock_scope, clock_eq = gen_clock_init rp rp.root_scope in
-    f_and clock_eq (init_f_of_scope rp rp.root_scope clock_scope)
 
 (*
     Get expressions for guarantee violation
@@ -502,3 +490,30 @@ and guarantees_of_prog rp =
 
     g_of_scope td rp.root_scope (clock_scope_here rp.root_scope) (BConst true)
 
+
+
+(*
+    Extract variables accessed by a LAST
+*)
+
+let rec extract_last_vars = function
+  | BRel(_, a, b, _) ->
+      elv_ne a @ elv_ne b
+  | BEnumCons c ->
+      elv_ec c
+  | BAnd(a, b) | BOr (a, b) ->
+    extract_last_vars a @ extract_last_vars b
+  | BNot(e) -> extract_last_vars e
+  | _ -> []
+
+and elv_ne = function
+  | NIdent i when i.[0] = 'L' -> [i]
+  | NBinary(_, a, b, _) -> elv_ne a @ elv_ne b
+  | NUnary (_, a, _) -> elv_ne a
+  | _ -> []
+
+and elv_ec (_, v, q) =
+  (if v.[0] = 'L' then [v] else []) @
+  (match q with
+    | EIdent i when i.[0] = 'L' -> [i]
+    | _ -> [])