Merge branch 'e-last'

Conflicts:
	abstract/abs_interp.ml
	tests/source/counters.scade

4 files changed, 347 insertions, 268 deletions

diff --git a/abstract/abs_interp.ml b/abstract/abs_interp.ml
index f6ce0ab..cb5ae9c 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
@@ -170,6 +165,7 @@ end = struct
         rp          : rooted_prog;
         opt         : cmdline_opt;
 
+        all_vars    : (bool * id * typ) list;
         enum_vars   : (id * ED.item list) list;
         num_vars    : (id * bool) list;
 
@@ -181,7 +177,8 @@ end = struct
         (* abstract interpretation *)
         cycle       : (id * id * typ) list;     (* s'(x) = s(y) *)
         forget      : (id * typ) list;          (* s'(x) not specified *)
-        d_vars      : id list;                  (* disjunction variables *)
+        d_vars      : id list;                  (* disjunction variables when calculating *)
+        acc_d_vars  : id list;                  (* disjunction variables in accumulator *)
         top         : case_v;
         env         : (case, case_v) Hashtbl.t;
         mutable delta : case list;
@@ -191,7 +188,7 @@ end = struct
     (*
       print_st : Formatter.t -> st -> unit
     *)
-    let print_st fmt st = print_aux fmt st.d_vars st.env
+    let print_st fmt st = print_aux fmt st.acc_d_vars st.env
 
     (*
       add_case : st -> case_v -> unit
@@ -223,29 +220,70 @@ end = struct
               | [en] -> aux en (v::vals) q
               | _ -> assert false)
             (ED.project enum p)
-      in aux enum [] st.d_vars
+      in aux enum [] st.acc_d_vars
 
+  
+    (*
+      dd_apply_cl : dd_v -> conslist -> dd_v
+    *)
+    let rec apply_cl_get_all_cases (enum, num) (ec, nc, r) =
+        match r with
+        | CLTrue ->
+          let enums = List.fold_left
+            (fun enums ec -> List.flatten
+              (List.map (fun e -> ED.apply_cons e ec) enums))
+            [enum] ec in
+          let num = ND.apply_cl num nc in
+          List.map (fun ec -> ec, num) enums
+        | CLFalse -> []
+        | CLAnd(a, b) ->
+          let envs = apply_cl_get_all_cases (enum, num) (ec, nc, a) in
+          List.flatten
+            (List.map (fun e -> apply_cl_get_all_cases e (ec, nc, b)) envs)
+        | CLOr((eca, nca, ra), (ecb, ncb, rb)) ->
+          apply_cl_get_all_cases (enum, num) (ec@eca, nc@nca, ra) @
+          apply_cl_get_all_cases (enum, num) (ec@ecb, nc@ncb, rb)
+
+    (*
+      pass_cycle : st -> case_v -> case_v
+    *)
+    let pass_cycle st (enum, num) =
+        let assign_e, assign_n = List.fold_left
+          (fun (ae, an) (a, b, t) -> match t with
+            | TEnum _ -> (a, b)::ae, an
+            | TInt | TReal -> ae, (a, NIdent b)::an)
+          ([], []) st.cycle in
+
+        let enum = ED.assign enum assign_e in
+        let num = ND.assign num assign_n in
+
+        List.fold_left
+            (fun (enum, num) (var, t) ->
+              let e, n = match t with
+              | TEnum _ -> ED.forgetvar enum var, num
+              | TReal | TInt -> enum, ND.forgetvar num var
+              in e, n)
+            (enum, num) st.forget
 
+    let dd_pass_cycle st (v : dd_v) =
+      let vv = dd_bot st.acc_d_vars in
+      Hashtbl.iter (fun _ x -> dd_add_case vv (pass_cycle st x)) v.data;
+      vv
 
     (*
       init_state : int -> rooted_prog -> st
     *)
     let init_state opt rp =
-      Format.printf "Vars: @[<hov>%a@]@.@."
-          (print_list Ast_printer.print_typed_var ", ")
-          rp.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
+      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;
-      let init_cl = conslist_of_f init_f in
+      Format.printf "Cycle formula:@.%a@.@." Formula_printer.print_expr f;
 
+      let init_cl = conslist_of_f init_f in
+      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 guarantees = Transform.guarantees_of_prog rp in
       Format.printf "Guarantees:@.";
       List.iter (fun (id, f) ->
@@ -253,69 +291,58 @@ 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;
+      (* add variables from LASTs *)
+      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 ", ")
+          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)
+          ([], []) all_vars in
 
       (* 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)
+        [] all_vars
       in
+      let forget = List.map (fun (_, id, ty) -> (id, ty)) rp.all_vars in
 
       (* calculate disjunction variables *)
-      (* first approximation : use all enum variables appearing in init formula *)
-      let rec calculate_dvars (ec, _, r) =
-          let a = List.map (fun (_, id, _) -> id) ec in
-          let rec aux = function
-          | CLTrue | CLFalse -> []
-          | CLAnd(u, v) ->
-              aux u @ aux v
-          | CLOr(u, v) ->
-              calculate_dvars u @ calculate_dvars v
-          in a @ aux r
-      in
-      let d_vars_0 = calculate_dvars init_cl in
-      let d_vars_1 = List.filter
-          (fun id -> opt.disjunct id && not (List.mem id d_vars_0) && id.[0] <> 'N')
+      (* actually, don't calculate them, rely on user input *)
+      let d_vars = List.filter (fun k -> k <> "/init" && opt.disjunct k)
           (List.map (fun (id, _) -> id) enum_vars) in
-      let d_vars = d_vars_0 @ d_vars_1 in
+      let acc_d_vars = List.filter (fun i -> i.[0] = 'L') d_vars in 
 
       (* setup abstract data *)
       let top = ED.top enum_vars, ND.top num_vars in
       let delta = [] in
       let widen = Hashtbl.create 12 in
 
-      (* calculate initial state and environment *)
-      let init_s = dd_bot d_vars in
-
-      let init_ec, _, _ = init_cl in
-      let init_ed = List.fold_left
-          (fun ed cons ->
-            List.flatten (List.map (fun x -> ED.apply_cons x cons) ed))
-          [ED.top enum_vars] (init_ec) in
-      List.iter (fun ed -> dd_add_case init_s (ed, ND.top num_vars)) init_ed;
-      let env_dd = apply_cl init_s init_cl in
-      let env = env_dd.data in
-      
       let st = 
-      { rp; opt; enum_vars; num_vars;
+      { rp; opt; enum_vars; num_vars; all_vars;
          cl; cl_g; guarantees;
-        cycle; forget; d_vars; top;
-        env; delta; widen } in
+        cycle; forget; acc_d_vars; d_vars; top;
+        env = Hashtbl.create 12; delta; widen } in
+
+      (* calculate initial state and environment *)
+      List.iter (fun ed -> add_case st (pass_cycle st ed))
+        (apply_cl_get_all_cases top init_cl);
 
       Hashtbl.iter (fun case _ -> st.delta <- case::st.delta) st.env;
 
@@ -323,30 +350,6 @@ end = struct
 
 
     (*
-      pass_cycle : st -> case_v -> case_v
-    *)
-    let pass_cycle st (enum, num) =
-        let assign_e, assign_n = List.fold_left
-          (fun (ae, an) (a, b, t) -> match t with
-            | TEnum _ -> (a, b)::ae, an
-            | TInt | TReal -> ae, (a, NIdent b)::an)
-          ([], []) st.cycle in
-
-        let enum = ED.assign enum assign_e in
-        let num = ND.assign num assign_n in
-
-        List.fold_left
-            (fun (enum, num) (var, t) -> match t with
-              | TEnum _ -> ED.forgetvar enum var, num
-              | TReal | TInt -> enum, ND.forgetvar num var)
-            (enum, num) st.forget
-
-    let dd_pass_cycle st (v : dd_v) =
-      let vv = dd_bot v.d_vars in
-      Hashtbl.iter (fun _ x -> dd_add_case vv (pass_cycle st x)) v.data;
-      vv
-
-    (*
       cycle : st -> cl -> dd_v -> dd_v
     *)
     let cycle st cl env =
@@ -362,10 +365,10 @@ end = struct
     let set_target_case st env case =
       List.fold_left2
         (fun env id v ->
-          if List.exists (fun (id2, _) -> id2 = "N"^id) st.enum_vars then
-            dd_apply_econs env (E_EQ, "N"^id, EItem v)
+          if List.exists (fun (id2, _) -> id2 = "L"^id) st.enum_vars then
+            dd_apply_econs env (E_EQ, id, EItem v)
           else env)
-        env st.d_vars case
+        env st.acc_d_vars case
 
     (*
       do_prog : rooted_prog -> unit
@@ -387,7 +390,7 @@ end = struct
             (print_list Formula_printer.print_id ", ") case;
         
         let start = try Hashtbl.find st.env case with Not_found -> assert false in
-        let start_dd = dd_singleton st.d_vars start in
+        let start_dd = dd_singleton st.acc_d_vars start in
         let f i =
           let i = dd_singleton st.d_vars i in
           let i' = set_target_case st i case in
@@ -422,7 +425,6 @@ end = struct
               Hashtbl.iter (fun _ q -> add_case st q) j.data)
             !cases;
 
-
         if st.opt.verbose_ci then
           Format.printf "-> @[<hov>%a@]@." print_st st;
 
diff --git a/abstract/abs_interp_edd.ml b/abstract/abs_interp_edd.ml
index 6220a0a..8ea0012 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_cl       : conslist;
         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,15 @@ end = struct
       init_env : cmdline_opt -> rooted_prog -> env
     *)
     let init_env opt rp =
-        Format.printf "Vars: @[<hov>%a@]@.@."
-            (print_list Ast_printer.print_typed_var ", ")
-            rp.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, 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 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
+        let cl = Formula.conslist_of_f f in
+        let cl_g = Formula.conslist_of_f f_g in
+        let init_cl = Formula.conslist_of_f init_f in
+        Format.printf "Cycle conslist:@.%a@.@." Formula_printer.print_conslist cl;
 
         let guarantees = Transform.guarantees_of_prog rp in
         Format.printf "Guarantees:@.";
@@ -945,20 +942,32 @@ end = struct
             Format.printf "  %s: %a@." id Formula_printer.print_expr f)
           guarantees;
         Format.printf "@.";
+        
+        (* add variables from LASTs *)
+        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
 
-        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;
+        Format.printf "Vars: @[<hov>%a@]@.@."
+            (print_list Ast_printer.print_typed_var ", ")
+            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)
+            ([], []) all_vars in
 
-        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
 
@@ -969,6 +978,9 @@ end = struct
           (List.filter (fun n -> is_suffix n "init") evars)) in
         let lv_f = lv_f @ (List.map (fun v -> (3.0, ["#BEGIN"; v]))
           (List.filter (fun n -> is_suffix n "state") evars)) in
+        let lv_f = lv_f @
+          (List.map (fun v -> (0.7, [v; "L"^v]))
+            (List.filter (fun n -> List.mem ("L"^n) evars) evars)) in
         let evars_ord =
           if true then
             time "FORCE" (fun () -> force_ordering evars lv_f)
@@ -995,25 +1007,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_cl; cl; cl_g; guarantees;
+          cycle; forget }
 
           
 
@@ -1094,7 +1098,9 @@ end = struct
             end
         in
 
-        let init_acc = edd_star_new (edd_bot e.data.ve) e.data in
+        Format.printf "Calculating initial state...@.";
+        let init_acc = edd_star_new (edd_bot e.ve)
+            (pass_cycle e (edd_apply_cl (edd_top e.ve) e.init_cl)) in
         
         (* Dump final state *)
         let acc = ch_it 0 init_acc in
@@ -1124,13 +1130,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 +1152,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..0045489 100644
--- a/abstract/formula.ml
+++ b/abstract/formula.ml
@@ -50,19 +50,26 @@ type bool_expr =
   | BOr of bool_expr * bool_expr
   | BNot of bool_expr
 
-let f_and a b = match a, b with
-  | BConst false, _ | _, BConst false -> BConst false
-  | BConst true, b -> b
-  | a, BConst true -> a
-  | a, b -> BAnd(a, b)
+let is_false = function
+  | BConst false | BNot(BConst true) -> true
+  | _ -> false
+let is_true = function
+  | BConst true | BNot(BConst false) -> true
+  | _ -> false
+
+let f_and a b =
+  if is_false a || is_false b then BConst false
+  else if is_true a then b
+  else if is_true b then a
+  else BAnd(a, b)
 
 let f_and_list = List.fold_left f_and (BConst true)
 
-let f_or a b = match a, b with
-  | BConst true, _ | _, BConst true -> BConst true
-  | BConst false, b -> b
-  | a, BConst false -> a
-  | a, b -> BOr(a, b)
+let f_or a b =
+  if is_true a || is_true b then BConst true
+  else if is_false a then b
+  else if is_false b then a
+  else BOr(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)
diff --git a/abstract/transform.ml b/abstract/transform.ml
index dcb4049..480705f 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)
@@ -136,6 +143,7 @@ let rec f_of_neexpr td (node, prefix, clock_scope) where expr =
 and f_of_bexpr td (node, prefix, clock_scope) where expr =
   let sub = f_of_bexpr td (node, prefix, clock_scope) in
   let sub_id = sub (fun x -> x) in
+  let le = loc_error (snd expr) in
   match fst expr with
   | AST_bool_const b -> where (BConst b)
   | AST_binary_bool(AST_AND, a, b) -> where (f_and (sub_id a) (sub_id b))
@@ -152,7 +160,8 @@ and f_of_bexpr td (node, prefix, clock_scope) where expr =
               | AST_NE -> E_NE
               | _ -> type_error "Invalid operator on enumerated values."
             in f_e_op eop x y
-          | _ -> invalid_arity "Binary operator")
+          | [NE _; EE _] | [EE _; NE _] -> le type_error "Invalid arguments for binary operator."
+          | _ -> le invalid_arity "Binary operator")
         (AST_tuple [a; b], snd expr))
   (* Temporal *)
   | AST_arrow(a, b) ->
@@ -180,7 +189,7 @@ and f_of_bexpr td (node, prefix, clock_scope) where expr =
       | _ -> assert false
     in
     f_of_neexpr td (node, prefix, clock_scope) ff expr
-  | _ -> type_error "Expected boolean value."
+  | _ -> le type_error "Expected boolean value."
 
 and f_of_expr td (node, prefix, clock_scope) expr =
     f_of_bexpr td (node, prefix, clock_scope) (fun x -> x) expr
@@ -190,40 +199,63 @@ 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)
+    let rst_code =
+        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)
+    in
+    let no_rst_code =
+        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
+    if rst_code = BConst true && no_rst_code = BConst true
+      then BConst true
+      else
+        f_or
+          (f_and (reset_cond rst_exprs) rst_code)
+          (f_and (no_reset_cond rst_exprs) no_rst_code)
   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 +279,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 +289,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 +355,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,47 +366,97 @@ 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 rst_states = uniq_sorted @@ List.sort compare @@ List.flatten
+          (List.map (fun (st, _) ->
+              List.map (fun (_, (id, _), _) -> id)
+              (List.filter (fun (_, _, rst) -> rst) st.until))
+            states)
+      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 rst_exprs =
+              if List.mem st.st_name rst_states then
+                  (f_e_eq (EIdent("L"^node^"/"^aid^"."^st.st_name^".must_reset"))
+                    (EItem bool_true))::rst_exprs
+              else rst_exprs
+            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 cr, cnr = List.partition
+              (fun i -> List.exists (fun (_, (v, _), x) -> x && v = i) st.until)
+              rst_states in
+            let must_reset_c l f =
+              f_and_list
+                (List.map
+                  (fun i -> f_e_eq (EIdent (node^"/"^aid^"."^i^".must_reset"))
+                      (EItem (if f i then bool_true else bool_false)))
+                  l)
+            in
             let rec aux = function
-              | [] -> BEnumCons(E_EQ, nstv, EItem st.st_name)
+              | [] ->
+                f_and
+                  (must_reset_c cr (fun _ -> false))
+                  (BEnumCons(E_EQ, nstv, EItem st.st_name))
               | (c, (target, l), rst)::q ->
-                if rst then loc_error l error "Resetting transitions not supported.";
                 f_or
                   (f_and (f_of_expr td (node, prefix, clock_scope) c)
-                        (BEnumCons(E_EQ, nstv, EItem target)))
+                        (f_and
+                          (BEnumCons(E_EQ, nstv, EItem target))
+                          (must_reset_c cr (fun i -> rst && i = target))))
                   (f_and (BNot (f_of_expr td (node, prefix, clock_scope) c)) (aux q))
-            in f_and st_eq (aux st.until) 
+            in
+            let trans_code = must_reset_c cnr (fun _ -> false) in
+            let trans_code = f_and trans_code (aux st.until) in
+            f_and st_eq trans_code 
           in
-          f_or
-            (f_and (BEnumCons(E_EQ, stv, EItem st.st_name)) act_eq)
-            (f_and (BEnumCons(E_NE, stv, EItem st.st_name))
-              (st_eq_inact (st, l)))
+          if List.length states = 1 then
+            act_eq
+          else
+            f_or
+              (f_and (BEnumCons(E_EQ, stv, EItem st.st_name)) act_eq)
+              (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
+            (f_and_list
+              (List.map
+                (fun s -> let n = node^"/"^aid^"."^s^".must_reset" in
+                  f_e_eq (EIdent n) (EIdent ("L"^n)))
+                rst_states))
+            (f_and_list (List.map st_eq_inact states)))
   in
   f_and_list (List.map do_eq eqs)
 
@@ -384,77 +466,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 +539,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]
+    | _ -> [])