Many things, sorry for the mess.

- Implement two new enumeration domains (they don't bring us much) :
    multi valuation for variables ;
    multi valuation for variables and pairs of variables (not really sure it works)
- Make it so that the number of init/time variables is reduced
      (do not create new init/time variables on node instanciation, only
      inside activate blocks and automaton states)
- Some work on EDD (it is currently broken and does not compile)

3 files changed, 579 insertions, 179 deletions

diff --git a/abstract/abs_interp_edd.ml b/abstract/abs_interp_edd.ml
index 3ff91a6..4f2ad81 100644
--- a/abstract/abs_interp_edd.ml
+++ b/abstract/abs_interp_edd.ml
@@ -11,8 +11,6 @@ module I (ND : NUMERICAL_ENVIRONMENT_DOMAIN) : sig
 
     val do_prog : cmdline_opt -> rooted_prog -> unit
 
-    val test : unit -> unit
-
 end = struct
 
 
@@ -31,10 +29,11 @@ end = struct
         ev_order      : (id, int) Hashtbl.t;
     }
 
-    type edd =
+    type edd_node =
         | DBot
         | DVal of int
         | DChoice of id * (item * edd) list
+    and edd = int * edd_node
 
     type edd_v = {
         ve            : varenv;
@@ -43,40 +42,66 @@ end = struct
         (* add here eventual annotations *)
     }
 
+    (*
+      Utility functions for memoization
+
+      memo : (((int * 'a) -> (int * 'b)) -> 'a -> 'b) -> (int * 'a) -> (int * 'b)
+      memo2 : (((int * 'a) -> (int * 'b) -> (int * 'c)) -> 'a -> 'b -> 'c) -> (int * 'a) -> (int * 'b) -> (int * 'c)
+    *)
+    let memo f =
+        let n = ref 0 in
+        let memo = Hashtbl.create 12 in
+        let rec ff (id, v) =
+          try Hashtbl.find memo id
+          with Not_found ->
+            let r = f ff v in
+            incr n;
+            Hashtbl.add memo id (n, r);
+            n, r
+        in ff
           
+    let memo2 f =
+        let n = ref 0 in
+        let memo = Hashtbl.create 12 in
+        let rec ff (id1, v1) (id2, v2) =
+          try Hashtbl.find memo (id1, id2)
+          with Not_found ->
+            let r = f ff v1 v2 in
+            incr n;
+            Hashtbl.add memo (id1, id2) (n, r);
+            n, r
+        in ff
 
     (*
       edd_print : Format.formatter -> edd_v -> unit
     *)
     let edd_print fmt v =
-        let ids = Hashtbl.create 12 in
-        let n = ref 0 in
-        let rec mkid = function
-            | DChoice(_, l) as x ->
-              if not (Hashtbl.mem ids x) then begin
-                incr n; Hashtbl.add ids x !n;
-                List.iter (fun (_, x) -> mkid x) l
+        let c_nodes = Hashtbl.create 12 in
+        let rec add = function
+            | n, (DChoice(_, l) as x) ->
+              if not (Hashtbl.mem c_nodes n) then begin
+                Hashtbl.add c_nodes n x;
+                List.iter (fun (_, y) -> add y) l
               end
             | _ -> ()
-        in mkid v.root;
+        in add v.root;
+
         let print_n fmt = function
-          | DBot -> Format.fprintf fmt "⊥";
-          | DVal i -> Format.fprintf fmt "v%d" i;
-          | DChoice _ as x -> Format.fprintf fmt "n%d" (Hashtbl.find ids x)
+          | (_, DBot) -> Format.fprintf fmt "⊥";
+          | (_, DVal i) -> Format.fprintf fmt "v%d" i;
+          | (n, DChoice _) -> Format.fprintf fmt "n%d" n
         in
         Format.fprintf fmt "Root: %a@." print_n v.root;
-        for id = 1 to !n do
-          let c = ref None in
-          Hashtbl.iter (fun u i -> if i = id then c := Some u) ids;
-          let x = match !c with | Some x -> x | None -> assert false in
-          match x with
+
+        Hashtbl.iter
+          (fun id x -> match x with
               | DChoice (var, l) ->
                 let p fmt (c, l) = Format.fprintf fmt "%s → %a" c print_n l in
                 Format.fprintf fmt "n%d: %a ? @[<hov>%a@]@."
                     id Formula_printer.print_id var
                     (print_list p ", ") l
-              | _ -> assert false
-        done;
+              | _ -> assert false)
+          c_nodes;
         Hashtbl.iter
             (fun id v -> Format.fprintf fmt "v%d: %a@." id ND.print v)
             v.leaves
@@ -86,7 +111,7 @@ end = struct
     (*
       edd_bot : varenv -> edd_v
     *)
-    let edd_bot ve = { ve; root = DBot; leaves = Hashtbl.create 1 }
+    let edd_bot ve = { ve; root = (0, DBot); leaves = Hashtbl.create 1 }
 
     (*
       edd_top : evar list -> nvar list -> edd_v
@@ -94,7 +119,7 @@ end = struct
     let edd_top ve =
         let leaves = Hashtbl.create 1 in
         Hashtbl.add leaves 0 (ND.top ve.nvars);
-        { ve; root = DVal 0; leaves }
+        { ve; root = (1, DVal 0); leaves }
 
     (*
       edd_of_cons : varenv -> enum_cons -> edd_v
@@ -105,23 +130,27 @@ end = struct
         let leaves = Hashtbl.create 1 in
         Hashtbl.add leaves 0 (ND.top ve.nvars);
 
+        let bot, top = (0, DBot), (1, DVal 0) in
+
         let root = match r with
         | EItem x ->
-          DChoice(vid,
-            List.map (fun v -> if op v x then v, DVal 0 else v, DBot)
-              (List.assoc vid ve.evars))      
+          2, DChoice(vid,
+              List.map (fun v -> if op v x then v, bot else v, top)
+                (List.assoc vid ve.evars))      
         | EIdent vid2 ->
             let a, b =
                 if Hashtbl.find ve.ev_order vid < Hashtbl.find ve.ev_order vid2
                   then vid, vid2
                   else vid2, vid
             in
+            let n = ref 2 in
             let nb x =
-              DChoice(b,
-                List.map (fun v -> if op v x then v, DVal 0 else v, DBot)
-                  (List.assoc b ve.evars))
+              incr n;
+              !n, DChoice(b,
+                    List.map (fun v -> if op v x then v, top else v, bot)
+                      (List.assoc b ve.evars))
             in
-            DChoice(a, List.map (fun x -> x, nb x) (List.assoc a ve.evars))
+            2, DChoice(a, List.map (fun x -> x, nb x) (List.assoc a ve.evars))
         in
         { ve; root; leaves }
 
@@ -131,10 +160,9 @@ end = struct
     let edd_join a b =
         let ve = a.ve in
 
-        let leaves = Hashtbl.copy a.leaves in
-        let n = ref 0 in
-        Hashtbl.iter (fun i _ -> if i > !n then n := i) leaves;
+        let leaves = Hashtbl.create 12 in
 
+        let n = ref 0 in
         let get_leaf x = 
           let id = ref None in
           Hashtbl.iter (fun i v -> if ND.eq v x then id := Some i) leaves;
@@ -147,61 +175,47 @@ end = struct
           end
         in
 
-        let memo_bcopy = Hashtbl.create 12 in
-        let rec bcopy nb =
-          try Hashtbl.find memo_bcopy nb
-          with Not_found -> let r =
-            match nb with
-            | DBot -> DBot
-            | DVal i -> get_leaf (Hashtbl.find b.leaves i)
-            | DChoice (v, x) ->
-              DChoice(v, List.map (fun (c, n) -> c, bcopy n) x)
-          in Hashtbl.add memo_bcopy nb r; r
-        in
 
-        let memo = Hashtbl.create 12 in
-        let rec f (na, nb) =
-          try Hashtbl.find memo (na, nb)
-          with Not_found -> let r =
-            let dq v l =
-              let _, x0 = List.hd l in
-              if List.exists (fun (_, x) -> x <> x0) l
-                then DChoice(v, l)
-                else x0
+        let f f_rec na nb =
+          let dq v l =
+            let _, (i, x0) = List.hd l in
+            if List.exists (fun (_, (j, x)) -> j <> i || x <> x0) l
+              then DChoice(v, l)
+              else x0
+          in
+          match na, nb with
+          | DBot, DBot -> DBot
+          | DBot, DVal i -> get_leaf (Hashtbl.find b.leaves i)
+          | x, DBot -> x
+
+          | DChoice(va, la), DChoice(vb, lb) when va = vb ->
+            let kl = List.map2
+                (fun (ta, ba) (tb, bb) -> assert (ta = tb);
+                  ta, f (ba, bb))
+                la lb
             in
-            match na, nb with
-            | DBot, x -> bcopy x
-            | x, DBot -> x
-
-            | DChoice(va, la), DChoice(vb, lb) when va = vb ->
-              let kl = List.map2
-                  (fun (ta, ba) (tb, bb) -> assert (ta = tb);
-                    ta, f (ba, bb))
-                  la lb
-              in
-              dq va kl
-            | DChoice(va, la), DChoice(vb, lb) ->
-              let v, kl =
-                if Hashtbl.find ve.ev_order va < Hashtbl.find ve.ev_order vb then
-                  va, List.map (fun (k, ca) -> k, f (ca, nb)) la
-                else
-                  vb, List.map (fun (k, cb) -> k, f (na, cb)) lb
-              in
-              dq v kl
-
-            | DChoice(va, la), _ ->
-              let kl = List.map (fun (k, ca) -> k, f (ca, nb)) la in
-              dq va kl
-            | _, DChoice(vb, lb) ->
-              let kl = List.map (fun (k, cb) -> k, f (na, cb)) lb in
-              dq vb kl
-
-            | DVal u, DVal v ->
-              let x = ND.join (Hashtbl.find a.leaves u) (Hashtbl.find b.leaves v) in
-              get_leaf x
-          in Hashtbl.add memo (na, nb) r; r
+            dq va kl
+          | DChoice(va, la), DChoice(vb, lb) ->
+            let v, kl =
+              if Hashtbl.find ve.ev_order va < Hashtbl.find ve.ev_order vb then
+                va, List.map (fun (k, ca) -> k, f (ca, nb)) la
+              else
+                vb, List.map (fun (k, cb) -> k, f (na, cb)) lb
+            in
+            dq v kl
+
+          | DChoice(va, la), _ ->
+            let kl = List.map (fun (k, ca) -> k, f (ca, nb)) la in
+            dq va kl
+          | _, DChoice(vb, lb) ->
+            let kl = List.map (fun (k, cb) -> k, f (na, cb)) lb in
+            dq vb kl
+
+          | DVal u, DVal v ->
+            let x = ND.join (Hashtbl.find a.leaves u) (Hashtbl.find b.leaves v) in
+            get_leaf x
         in
-        { leaves; ve; root = f (a.root, b.root) }
+        { leaves; ve; root = memo2 f a.root b.root }
 
     (*
       edd_meet : edd_v -> edd_v -> edd_v
@@ -342,6 +356,7 @@ end = struct
         in f (a.root, b.root)
 
 
+    (*
     let test () =
         let ve = {
             evars = ["x", ["tt"; "ff"]; "y", ["tt"; "ff"]; "z", ["tt"; "ff"]];
@@ -358,6 +373,7 @@ end = struct
         Format.printf "x = y && y != z : @[%a@]@." edd_print w;
         let t = edd_join u v in
         Format.printf "x = y || y != z : @[%a@]@." edd_print t
+    *)
 
 
     (* ******************************
diff --git a/abstract/enum_domain.ml b/abstract/enum_domain.ml
index c8b4ec5..2353049 100644
--- a/abstract/enum_domain.ml
+++ b/abstract/enum_domain.ml
@@ -34,6 +34,9 @@ module type ENUM_ENVIRONMENT_DOMAIN = sig
 end
 
 
+(*
+    Simple domain : one valuation for each variable, or T
+*)
 
 module Valuation : ENUM_ENVIRONMENT_DOMAIN = struct
     type item = string
@@ -142,3 +145,343 @@ module Valuation : ENUM_ENVIRONMENT_DOMAIN = struct
         Format.fprintf fmt " }@]"
 
 end
+
+
+(*
+    Less simple domain : a set of possible values for each variable, or T
+*)
+
+module MultiValuation : ENUM_ENVIRONMENT_DOMAIN = struct
+    type item = string
+
+    type t = {
+        vars      : (id * item list) list;
+        value     : item list VarMap.t;
+    }
+
+    let sort = List.sort Pervasives.compare
+    let uniq x = uniq_sorted (sort x)
+
+    let top vars = { vars; value = VarMap.empty }
+
+    let vars x = x.vars
+
+    let forgetvar x id =
+        { x with value = VarMap.remove id x.value }
+    let project x id =
+        try VarMap.find id x.value
+        with Not_found -> List.assoc id x.vars
+
+    let join x1 x2 =
+        let v = VarMap.merge
+          (fun _ a b -> match a, b with
+            | Some a, Some b -> Some (uniq (a@b))
+            | _ -> None)
+          x1.value x2.value in
+        { x1 with value = v }
+    let meet x1 x2 =
+        let v = VarMap.merge
+          (fun _ a b -> match a, b with
+            | Some a, None | None, Some a -> Some a
+            | Some a, Some b ->
+              begin match List.filter (fun x -> List.mem x b) a with
+              | [] -> raise Bot | l -> Some l end
+            | _ -> None)
+          x1.value x2.value in
+        { x1 with value = v }
+
+    let subset a b =
+        VarMap.for_all
+          (fun id v ->
+              try let v2 = VarMap.find id b.value in
+                  List.for_all (fun x -> List.mem x v2) v
+              with Not_found -> true)
+          a.value
+    let eq a b = subset a b && subset b a
+
+    let apply_cons x (op, id, e) =
+        let op = match op with | E_EQ -> (=) | E_NE -> (<>) in
+
+        match e with
+        | EItem s ->
+          let pv = project x id in
+          begin match List.filter (op s) pv with
+          | [] -> []
+          | vals -> [{ x with value = VarMap.add id vals x.value }]
+          end
+        | EIdent id2 ->
+          let v1 = project x id in
+          let v2 = project x id2 in
+          List.fold_left
+            (fun l v1 ->
+                let v2 = List.filter (op v1) v2 in
+                let x = { x with value = VarMap.add id [v1] x.value } in
+                match v2 with
+                | [] -> l
+                | _ -> { x with value = VarMap.add id2 v2 x.value }::l)
+            [] v1
+    
+    let assign x idl =
+        let v = List.fold_left
+            (fun v (id, id2) ->
+                try VarMap.add id (VarMap.find id2 x.value) v
+                with Not_found -> VarMap.remove id v )
+            x.value idl
+        in { x with value = v }
+
+
+    let print fmt x =
+        let b = List.map (fun (x, y) -> y, x) (VarMap.bindings x.value) in
+        let s = List.sort Pervasives.compare b in
+        let rec bl = function
+          | [] -> []
+          | (v, id)::q ->
+            let v = sort v in
+            if v <> sort (List.assoc id x.vars) then
+              match bl q with
+              | (vv, ids)::q when vv = v -> (v, id::ids)::q
+              | r -> (v, [id])::r
+            else
+              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 "@ ";
+            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;
+            match v with
+            | [v0] -> Format.fprintf fmt " ≡ %s@]" v0
+            | l -> Format.fprintf fmt " ∊ @[<hov>{ %a }@]@]" (print_list Format.pp_print_string ", ") l)
+          sbl;
+        Format.fprintf fmt " }@]"
+
+end
+
+
+(*
+    Complicated domain : a set of values for each variables, plus some
+    constraints on couples of variables
+      (eg. (x, y) in [ tt, tt ; ff, ff ]
+*)
+
+module MultiValuationCCons : ENUM_ENVIRONMENT_DOMAIN = struct
+
+    module VarC = struct
+        type t = id * id
+        let compare = Pervasives.compare
+    end
+    module VarCMap = Mapext.Make(VarC)
+
+    type item = string
+
+    type t = {
+        vars      : (id * item list) list;
+        value     : item list VarMap.t;
+
+        (* in ccond (x, y) -> l, must have x < y (textual order on identifiers) -> unicity *)
+        ccons     : (item * item) list VarCMap.t;
+    }
+
+    let sort = List.sort Pervasives.compare
+    let uniq x = uniq_sorted (sort x)
+    let list_inter x y = List.filter (fun k -> List.mem k y) x
+
+    let all_couples l1 l2 =
+        List.flatten
+          (List.map (fun x -> List.map (fun y -> x, y) l2) l1)
+
+    let top vars = { vars; value = VarMap.empty; ccons = VarCMap.empty }
+
+    let vars x = x.vars
+
+    let forgetvar x id =
+        (* TODO : try to find a substitution variable so that some contraints can be propagated.
+                  this is important so that cycle passing can be done correctly ! *)
+        { x with
+          value = VarMap.remove id x.value;
+          ccons = VarCMap.filter (fun (a, b) _ -> a <> id && b <> id) x.ccons }
+
+    let project x id =
+        try VarMap.find id x.value
+        with Not_found -> List.assoc id x.vars
+
+    let project2 x id1 id2 =
+        try
+          let id1', id2' = ord_couple (id1, id2) in
+          if id1' = id1 then
+            VarCMap.find (id1, id2) x.ccons
+          else
+            List.map (fun (a, b) -> b, a) (VarCMap.find (id1', id2') x.ccons)
+        with _ ->
+          let v1, v2 = project x id1, project x id2 in
+          all_couples v1 v2
+
+    let strict x =
+        let rec f x =
+          (*
+              - if (x, y) in [ a, b1 ; a, b2 ; ... ; a, bn ],
+                  replace this by x = a and y in { b1, ..., bn }
+              - filter (x, y) in [ ... ] with x in specified itv, y in specified itv
+          *)
+          let usefull, vv, cc =
+            VarCMap.fold
+              (fun (x, y) l (usefull, vv, cc) ->
+                  let p1, p2 = uniq (List.map fst l), uniq (List.map snd l) in
+                  let p1 = try list_inter p1 (VarMap.find x vv) with _ -> p1 in
+                  let p2 = try list_inter p2 (VarMap.find y vv) with _ -> p2 in
+
+                  if p1 = [] || p2 = [] then raise Bot;
+                  let vv = VarMap.add x p1 (VarMap.add y p2 vv) in
+
+                  if List.length p1 = 1 || List.length p2 = 1
+                  then
+                    true, vv, cc
+                  else
+                    match List.filter (fun (u, v) -> List.mem u p1 && List.mem v p2) l with
+                    | [] -> raise Bot
+                    | l2 -> List.length l2 < List.length l, vv, VarCMap.add (x, y) l2 cc)
+              x.ccons (false, x.value, VarCMap.empty) in
+
+          let x = { x with value = vv; ccons = cc } in
+          if usefull then f x else x
+        in
+        f x
+
+    let join x1 x2 =
+        let v = VarMap.merge
+          (fun _ a b -> match a, b with
+            | Some a, Some b -> Some (uniq (a@b))
+            | _ -> None)
+          x1.value x2.value in
+        let x = { x1 with value = v } in
+
+        let cc = VarCMap.merge
+          (fun (id1, id2) l1 l2 ->
+              let v1, v2 = project x1 id1, project x id2 in
+              let ac = all_couples v1 v2 in
+              let c = List.filter
+                  (fun q ->
+                    (match l1 with Some l -> List.mem q l | _ -> true) ||
+                    (match l2 with Some l -> List.mem q l | _ -> true))
+                  ac in 
+              if List.length c < List.length ac then Some c else None)
+          x1.ccons x2.ccons in
+
+        strict { x with ccons = cc }
+
+    let meet x1 x2 =
+        let v = VarMap.merge
+          (fun _ a b -> match a, b with
+            | Some a, None | None, Some a -> Some a
+            | Some a, Some b ->
+              begin match list_inter a b with
+              | [] -> raise Bot | l -> Some l end
+            | _ -> None)
+          x1.value x2.value in
+        let x = { x1 with value = v } in 
+
+        let cc = VarCMap.merge
+          (fun (id1, id2) l1 l2 ->
+              let v1, v2 = project x id1, project x id2 in
+              let ac = all_couples v1 v2 in
+              let c1 = match l1 with Some l -> list_inter l ac | None -> ac in
+              let c2 = match l2 with Some l -> list_inter l ac | None -> ac in
+              match list_inter c1 c2 with
+              | [] -> raise Bot
+              | l -> if List.length l < List.length ac then Some l else None)
+          x1.ccons x2.ccons in
+
+        strict { x with ccons = cc }
+
+    let subset a b =
+        VarMap.for_all
+          (fun id v ->
+              let vs = project a id in
+              List.for_all (fun c -> List.mem c vs) v)
+          b.value
+        &&
+        VarCMap.for_all
+          (fun (id1, id2) l ->
+              let l2 = project2 a id1 id2 in
+              List.for_all (fun c -> List.mem c l) l2)
+          b.ccons
+    let eq a b =
+      subset a b && subset b a
+
+    let apply_cons x (op, id, e) =
+        let op = match op with | E_EQ -> (=) | E_NE -> (<>) in
+        
+        match e with
+        | EItem s ->
+          let pv = project x id in
+          begin match List.filter (op s) pv with
+          | [] -> []
+          | vals -> try [strict { x with value = VarMap.add id vals x.value }] with Bot -> []
+          end
+        | EIdent id2 ->
+          let id, id2 = ord_couple (id, id2) in
+          let c = project2 x id id2 in
+          let ok_c = List.filter (fun (a, b) -> op a b) c in
+          try
+            [match uniq (List.map fst ok_c), uniq (List.map snd ok_c) with
+              | [], _ | _, [] -> raise Bot
+              | [a], q -> strict { x with value = VarMap.add id [a] (VarMap.add id2 q x.value) }
+              | q, [b] -> strict { x with value = VarMap.add id q (VarMap.add id2 [b] x.value) }
+              | _ -> strict { x with ccons = VarCMap.add (id, id2) ok_c x.ccons}
+            ]
+          with Bot -> []
+    
+    let assign x idl =
+        let x2 = List.fold_left (fun x (v, _) -> forgetvar x v) x idl in
+        let v = List.fold_left
+            (fun v (id, id2) ->
+                try VarMap.add id (VarMap.find id2 x.value) v
+                with Not_found -> v)
+            x2.value idl in
+        let c = VarCMap.fold
+            (fun (v1, v2) l c ->
+                let v1' = try List.assoc v1 idl with _ -> v1 in
+                let v2' = try List.assoc v2 idl with _ -> v2 in
+                VarCMap.add (v1', v2') l c)
+            x.ccons x2.ccons in
+        strict { x with value = v; ccons = c }
+
+
+    let print fmt x =
+        let b = List.map (fun (x, y) -> y, x) (VarMap.bindings x.value) in
+        let s = List.sort Pervasives.compare b in
+        let rec bl = function
+          | [] -> []
+          | (v, id)::q ->
+            let v = sort v in
+            if v <> sort (List.assoc id x.vars) then
+              match bl q with
+              | (vv, ids)::q when vv = v -> (v, id::ids)::q
+              | r -> (v, [id])::r
+            else
+              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 "@ ";
+            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;
+            match v with
+            | [v0] -> Format.fprintf fmt " ≡ %s@]" v0
+            | l -> Format.fprintf fmt " ∊ @[<hov>{ %a }@]@]" (print_list Format.pp_print_string ", ") l)
+          sbl;
+        Format.fprintf fmt " }@]"
+
+end
diff --git a/abstract/transform.ml b/abstract/transform.ml
index b9c173d..4a13e18 100644
--- a/abstract/transform.ml
+++ b/abstract/transform.ml
@@ -26,8 +26,8 @@ type ne_expr =
 (* f_of_neexpr :
     transform_data -> (string, string) -> (ne_expr list -> bool_expr) -> expr -> bool_expr
 *)
-let rec f_of_neexpr td (node, prefix) where expr =
-  let sub = f_of_neexpr td (node, prefix) in
+let rec f_of_neexpr td (node, prefix, clock_scope) where expr =
+  let sub = f_of_neexpr td (node, prefix, clock_scope) in
   let le = loc_error (snd expr) in
   match fst expr with
   (* ident *)
@@ -71,24 +71,27 @@ let rec f_of_neexpr td (node, prefix) where expr =
               | TEnum _ -> EE(EIdent x))
           typ)
   | AST_arrow(a, b) ->
-    if td.rp.init_scope (node^"/")
+    if td.rp.init_scope clock_scope
     then
       f_or
-        (f_and (f_e_eq (EIdent (node^"/"^prefix^"init")) (EItem bool_true))
+        (f_and (f_e_eq (EIdent (clock_scope^"init")) (EItem bool_true))
           (sub where a))
-        (f_and (f_e_eq (EIdent (node^"/"^prefix^"init")) (EItem bool_false))
+        (f_and (f_e_eq (EIdent (clock_scope^"init")) (EItem bool_false))
           (sub where b))
-    else
+    else if not (td.rp.no_time_scope clock_scope)
+    then
       f_or
-        (f_and (BRel(AST_EQ, NIdent(node^"/"^prefix^"time"), NIntConst 0))
+        (f_and (BRel(AST_EQ, NIdent(clock_scope^"time"), NIntConst 0))
           (sub where a))
-        (f_and (BRel(AST_GE, NIdent(node^"/"^prefix^"time"), NIntConst 1))
+        (f_and (BRel(AST_GE, NIdent(clock_scope^"time"), NIntConst 1))
           (sub where b))
+    else
+      f_or (sub where a) (sub where b)
   (* other *)
   | AST_if(c, a, b) ->
     f_or
-      (f_and (f_of_expr td (node, prefix) c) (sub where a))
-      (f_and (BNot(f_of_expr td (node, prefix) c)) (sub where b))
+      (f_and (f_of_expr td (node, prefix, clock_scope) c) (sub where a))
+      (f_and (BNot(f_of_expr td (node, prefix, clock_scope) c)) (sub where b))
   | AST_instance ((f, _), args, nid) ->
     let (n, _) = find_node_decl td.rp.p f in
     where
@@ -107,8 +110,9 @@ let rec f_of_neexpr td (node, prefix) where expr =
   (* boolean values treated as enumerated types *)
   | _ when type_expr td.rp node expr = [bool_type] ->
     f_or
-      (f_and (f_of_expr td (node, prefix) expr) (where [EE (EItem bool_true)]))
-      (f_and (f_of_expr td (node, prefix) (AST_not(expr), snd expr))
+      (f_and (f_of_expr td (node, prefix, clock_scope) expr)
+          (where [EE (EItem bool_true)]))
+      (f_and (f_of_expr td (node, prefix, clock_scope) (AST_not(expr), snd expr))
         (where [EE (EItem bool_false)]))
   | _ -> le type_error "Expected numerical/enumerated value"
 
@@ -120,8 +124,8 @@ let rec f_of_neexpr td (node, prefix) where expr =
   f_of_bexpr :
     transform_data -> (string, string) -> (bool_expr -> bool_expr) -> expr -> bool_expr
 *)
-and f_of_bexpr td (node, prefix) where expr =
-  let sub = f_of_bexpr td (node, prefix) in
+and f_of_bexpr td (node, prefix, clock_scope) where expr =
+  let sub = f_of_bexpr td (node, prefix, clock_scope) in
   match fst expr with
   | AST_bool_const b -> where (BConst b)
   | AST_binary_bool(AST_AND, a, b) -> f_and (sub where a) (sub where b)
@@ -129,7 +133,7 @@ and f_of_bexpr td (node, prefix) where expr =
   | AST_not(a) -> BNot(sub where a)
   | AST_binary_rel(rel, a, b) ->
     where
-      (f_of_neexpr td (node, prefix)
+      (f_of_neexpr td (node, prefix, clock_scope)
         (function
           | [NE x; NE y] -> BRel(rel, x, y)
           | [EE x; EE y] ->
@@ -142,11 +146,22 @@ and f_of_bexpr td (node, prefix) where expr =
         (AST_tuple [a; b], snd expr))
   (* Temporal *)
   | AST_arrow(a, b) ->
+    if td.rp.init_scope clock_scope
+    then
       f_or
-        (f_and (BRel(AST_EQ, NIdent(node^"/"^prefix^"time"), NIntConst 0))
+        (f_and (f_e_eq (EIdent (clock_scope^"init")) (EItem bool_true))
           (sub where a))
-        (f_and (BRel(AST_GE, NIdent(node^"/"^prefix^"time"), NIntConst 1))
+        (f_and (f_e_eq (EIdent (clock_scope^"init")) (EItem bool_false))
           (sub where b))
+    else if not (td.rp.no_time_scope clock_scope)
+    then
+      f_or
+        (f_and (BRel(AST_EQ, NIdent(clock_scope^"time"), NIntConst 0))
+          (sub where a))
+        (f_and (BRel(AST_GE, NIdent(clock_scope^"time"), NIntConst 1))
+          (sub where b))
+    else
+      f_or (sub where a) (sub where b)
   (* Enumerations... *)
   | _ when type_expr td.rp node expr = [bool_type] ->
     let ff = function
@@ -156,23 +171,53 @@ and f_of_bexpr td (node, prefix) where expr =
           (f_and (f_e_eq x (EItem bool_false)) (where (BConst false)))
       | _ -> assert false
     in
-    f_of_neexpr td (node, prefix) ff expr
+    f_of_neexpr td (node, prefix, clock_scope) ff expr
   | _ -> type_error "Expected boolean value."
 
-and f_of_expr td (node, prefix) expr =
-    f_of_bexpr td (node, prefix) (fun x -> x) expr
+and f_of_expr td (node, prefix, clock_scope) expr =
+    f_of_bexpr td (node, prefix, clock_scope) (fun x -> x) expr
   
 
 (*
     Translate program into one big formula
 *)
-let rec f_of_scope active td (node, prefix, eqs) assume_guarantees =
+
+let clock_scope_here (node, prefix, _) =
+  node^"/"^prefix
+
+let gen_clock td (node, prefix, _) active =
+  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")))
+          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"))
+          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)
+  in
+  clock_scope, clock_eq
+
+let rec f_of_scope active td (node, prefix, eqs) clock_scope assume_guarantees =
   let expr_eq e =
     let instance_eq (_, id, eqs, args) =
-      let eq = f_of_scope active td (node^"/"^id, "", eqs) assume_guarantees in
+      let eq = f_of_scope active td (node^"/"^id, "", eqs) clock_scope assume_guarantees in
       if active then
         let arg_eq ((_,argname,_), expr) =
-            f_of_neexpr td (node, prefix) (function
+            f_of_neexpr td (node, prefix, clock_scope) (function
                 | [NE v] -> BRel(AST_EQ, NIdent(node^"/"^id^"/"^argname), v)
                 | [EE v] -> f_e_eq (EIdent(node^"/"^id^"/"^argname)) v
                 | _ -> invalid_arity "in argument")
@@ -186,7 +231,7 @@ let rec f_of_scope active td (node, prefix, eqs) assume_guarantees =
     let pre_expr (id, expr) =
       let id = node^"/"^id in
       if active then
-        f_of_neexpr td (node, prefix) (fun elist ->
+        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
@@ -222,7 +267,7 @@ let rec f_of_scope active td (node, prefix, eqs) assume_guarantees =
               in
                 f_and_list rels
             in
-            f_of_neexpr td (node, prefix) apply_f e
+            f_of_neexpr td (node, prefix, clock_scope) apply_f e
         else
           BConst true
       in
@@ -230,7 +275,7 @@ let rec f_of_scope active td (node, prefix, eqs) assume_guarantees =
     | AST_assume (_, e) ->
       let assume_eq = 
         if active then
-          f_of_expr td (node, prefix) e
+          f_of_expr td (node, prefix, clock_scope) e
         else
           BConst true
       in
@@ -239,13 +284,13 @@ let rec f_of_scope active td (node, prefix, eqs) assume_guarantees =
       let gn = node^"/g_"^id in
       let guarantee_eq =
         if active && assume_guarantees then
-          f_and (f_of_expr td (node, prefix) e)
+          f_and (f_of_expr td (node, prefix, clock_scope) e)
                 (BEnumCons(E_EQ, gn, EItem bool_true))
         else
           f_or
-            (f_and (f_of_expr td (node, prefix) e)
+            (f_and (f_of_expr td (node, prefix, clock_scope) e)
                 (BEnumCons(E_EQ, gn, EItem bool_true)))
-            (f_and (BNot (f_of_expr td (node, prefix) e))
+            (f_and (BNot (f_of_expr td (node, prefix, clock_scope) e))
                 (BEnumCons(E_EQ, gn, EItem bool_false)))
       in
         f_and (expr_eq e) guarantee_eq
@@ -258,16 +303,20 @@ let rec f_of_scope active td (node, prefix, eqs) assume_guarantees =
       in
       let rec do_tree_act = function
         | AST_activate_body b ->
-            f_of_scope true td (node, b.act_id^".", b.body) assume_guarantees
+            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)
         | AST_activate_if(c, a, b) ->
           f_or
-            (f_and (f_of_expr td (node, prefix) c)
+            (f_and (f_of_expr td (node, prefix, clock_scope) c)
               (f_and (do_tree_act a) (do_tree_inact b)))
-            (f_and (BNot(f_of_expr td (node, prefix) c))
+            (f_and (BNot(f_of_expr td (node, prefix, clock_scope) c))
               (f_and (do_tree_act b) (do_tree_inact a)))
       and do_tree_inact = function
         | AST_activate_body b ->
-          f_of_scope false td (node, b.act_id^".", b.body) assume_guarantees
+            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)
         | AST_activate_if(_, a, b) ->
           f_and (do_tree_inact a) (do_tree_inact b)
       in
@@ -276,24 +325,27 @@ let rec f_of_scope active td (node, prefix, eqs) assume_guarantees =
       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
-              (node, aid^"."^st.st_name^".", st.body) assume_guarantees)
-          (f_and_list (List.map (fun (c, _, _) -> expr_eq c) st.until))
+        let st_scope = node, aid^"."^st.st_name^".", st.body in
+        let clock_scope, clock_eq = gen_clock td st_scope false in
+        f_and clock_eq
+          (f_and
+            (f_of_scope false td st_scope clock_scope 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_eq = f_of_scope true td
-              (node, aid^"."^st.st_name^".", st.body) assume_guarantees in
+            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 rec aux = function
               | [] -> 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) c)
+                  (f_and (f_of_expr td (node, prefix, clock_scope) c)
                         (BEnumCons(E_EQ, nstv, EItem target)))
-                  (f_and (BNot (f_of_expr td (node, prefix) c)) (aux q))
+                  (f_and (BNot (f_of_expr td (node, prefix, clock_scope) c)) (aux q))
             in f_and st_eq (aux st.until) 
           in
           f_or
@@ -305,31 +357,7 @@ let rec f_of_scope active td (node, prefix, eqs) assume_guarantees =
       else
         f_and_list (List.map st_eq_inact states)
   in
-  let time_incr_eq =
-    if active then
-      f_and
-        (if not (td.rp.no_time_scope (node^"/"))
-          then BRel(AST_EQ, NIdent("N"^node^"/"^prefix^"time"),
-              NBinary(AST_PLUS, NIntConst 1, NIdent(node^"/"^prefix^"time")))
-          else BConst true)
-        (if td.rp.init_scope (node^"/")
-          then f_e_eq (EIdent("N"^node^"/"^prefix^"init")) (EItem bool_false)
-          else BConst true)
-    else
-      f_and
-        (if not (td.rp.no_time_scope (node^"/"))
-          then BRel(AST_EQ,
-              NIdent("N"^node^"/"^prefix^"time"),
-              NIdent(node^"/"^prefix^"time"))
-          else BConst true)
-        (if td.rp.init_scope (node^"/")
-          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
-    (List.map do_eq eqs)
+  f_and_list (List.map do_eq eqs)
 
 and f_of_prog rp assume_guarantees =
     let td = {
@@ -337,15 +365,34 @@ and f_of_prog rp assume_guarantees =
       consts = I.consts rp;
     } in
 
-    f_of_scope true td td.rp.root_scope assume_guarantees
+    let clock_scope, clock_eq = gen_clock td rp.root_scope true in
+
+    f_and clock_eq (f_of_scope true td td.rp.root_scope clock_scope assume_guarantees)
 
 (*
     Translate init state into a formula
 *)
-let rec init_f_of_scope rp (node, prefix, eqs) =
+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)
+        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 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)
+     init_f_of_scope rp (node^"/"^id, "", eqs) clock_scope
     in
     List.fold_left (fun x i -> f_and (instance_eq i) x)
       (BConst true) (extract_instances rp.p e)
@@ -356,7 +403,9 @@ let rec init_f_of_scope rp (node, prefix, eqs) =
     | AST_activate (b, _) ->
       let rec cond_eq = function
         | AST_activate_body b ->
-          init_f_of_scope rp (node, b.act_id^".", b.body)
+          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))
@@ -367,37 +416,27 @@ let rec init_f_of_scope rp (node, prefix, eqs) =
       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)
+          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
-  let time_eq =
-    f_and
-      (if not (rp.no_time_scope (node^"/"))
-        then
-          BRel(AST_EQ,
-            NIdent(node^"/"^prefix^"time"),
-            NIntConst 0)
-        else BConst true)
-      (if rp.init_scope (node^"/")
-        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)
+  f_and_list (List.map do_eq eqs)
 
 and init_f_of_prog rp =
-    init_f_of_scope rp rp.root_scope
+    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
 *)
-let rec g_of_scope td (node, prefix, eqs) cond =
+let rec g_of_scope td (node, prefix, eqs) clock_scope cond =
   let expr_g e =
     let instance_g (_, id, eqs, args) =
-        g_of_scope td (node^"/"^id, "", eqs) cond
+        g_of_scope td (node^"/"^id, "", eqs) clock_scope cond
     in
     List.fold_left (fun x i -> (instance_g i) @ x)
       [] (extract_instances td.rp.p e)
@@ -406,21 +445,23 @@ let rec g_of_scope td (node, prefix, eqs) cond =
     | AST_assign(_, e) | AST_assume(_, e) ->
         expr_g e
     | AST_guarantee((id, _), e) ->
-        (id, f_and cond (f_of_expr td (node, prefix) (AST_not(e), snd e)))
+        (id, f_and cond (f_of_expr td (node, prefix, clock_scope) (AST_not(e), snd e)))
           :: (expr_g e)
     | AST_activate (b, _) ->
       let rec cond_g cond = function
         | AST_activate_body b ->
-          g_of_scope td (node, b.act_id^".", b.body) cond
+          let bscope = node, b.act_id^".", b.body in
+          g_of_scope td bscope (clock_scope_here bscope) cond
         | AST_activate_if(c, a, b) ->
-          (cond_g (f_and cond (f_of_expr td (node, prefix) c)) a) @
-          (cond_g (f_and cond (f_of_expr td (node, prefix) (AST_not(c), snd c))) b) @
+          (cond_g (f_and cond (f_of_expr td (node, prefix, clock_scope) c)) a) @
+          (cond_g (f_and cond (f_of_expr td (node, prefix, clock_scope) (AST_not(c), snd c))) b) @
           (expr_g c)
       in
       cond_g cond b
     | AST_automaton (aid, states, _) ->
       let st_g (st, _) =
-        g_of_scope td (node, aid^"."^st.st_name^".", st.body)
+        let stscope = (node, aid^"."^st.st_name^".", st.body) in
+        g_of_scope td stscope (clock_scope_here stscope)
           (f_and cond (BEnumCons(E_EQ, node^"/"^aid^".state", EItem st.st_name)))
       in
       List.flatten (List.map st_g states)
@@ -433,4 +474,4 @@ and guarantees_of_prog rp =
       consts = I.consts rp;
     } in
 
-    g_of_scope td rp.root_scope (BConst true)
+    g_of_scope td rp.root_scope "" (BConst true)