diff --git a/src/Bdd.ml b/src/Bdd.ml
new file mode 100644
index 0000000..ed9fbd7
--- /dev/null
+++ b/src/Bdd.ml
@@ -0,0 +1,100 @@
+(** Implementation of BDDs with hashconsing *)
+
+type t = {id: int; l: t; r: t; value: int}
+
+
+(* type tree = One | Zero | Tree of tree * tree * int *)
+(* and t = int * tree *)
+
+let rec null = {id = -1; l = null; r = null; value = -1}
+
+let one = {id = 0; l = null; r = null; value = -1}
+let zero = {id = 1; l = null; r = null; value = -1}
+
+type bdd = t
+
+module S = struct
+  type t = bdd
+
+  let equal b1 b2 =
+    b1.l == b2.l && b1.r == b2.r
+
+  let hash b =
+    29 * (b.l.id + (29 * b.r.id))
+
+end
+
+module HashedBdd = S
+
+module HBdd = Hashtbl.Make(S)
+
+let create =
+  let htbl = HBdd.create 53 in
+  let id = ref 2 in
+  fun v l r ->
+    let i = !id in
+    let b = {id = i; l; r; value = v} in
+    try
+      HBdd.find htbl b
+    with
+      Not_found ->
+        HBdd.add htbl b b;
+        incr id;
+        b
+
+module HPair = Hashtbl.Make(
+  struct
+    type t = bdd * bdd
+
+    let equal (b1, b2) (b1', b2') =
+      S.equal b1 b1' && S.equal b2 b2'
+
+    let hash (b1, b2) =
+      S.hash b1 + 29 * S.hash b2
+  end)
+
+let is_leaf b = b == one || b == zero
+
+let boolean_equiv b =
+  (* if b <> from one and zero, assert false will be evaluated *)
+  b == one || (b <> zero && assert false)
+
+let apply op =
+  let htbl = HPair.create 53 in
+  let apply_op op b1 b2 =
+    let b1 = boolean_equiv b1 in
+    let b2 = boolean_equiv b2 in
+    let res = op b1 b2 in
+    if res then one else zero
+  in
+  let rec apply b1 b2 =
+    try HPair.find htbl (b1, b2)
+    with Not_found ->
+      let res =
+        if is_leaf b1 && is_leaf b2 then
+          apply_op op b1 b2
+        else if b1.value = b2.value then
+          create b1.value (apply b1.l b2.l) (apply b1.r b2.r)
+        else if b1.value < b2.value then
+          create b1.value (apply b1.l b2) (apply b1.r b2)
+        else create b2.value (apply b1 b2.l) (apply b1 b2.r)
+      in
+      HPair.add htbl (b1, b2) res; res
+  in
+  apply
+
+let rec restrict bool value b =
+  if is_leaf b then b
+  else
+    if b.value < value then
+      let l = restrict bool value b.l in
+      let r = restrict bool value b.r in
+      create b.value l r
+    else if b.value = value then
+      if bool then b.r else b.l
+    else b
+
+let exists value b =
+  let l = restrict false value b in
+  let r = restrict true value b in
+  apply ( or ) l r
diff --git a/src/Check.ml b/src/Check.ml
new file mode 100644
index 0000000..14d0bbe
--- /dev/null
+++ b/src/Check.ml
@@ -0,0 +1,498 @@
+open Formula
+open Global
+open Semop
+open Bdd
+open Utils
+
+(** Local model checker *)
+
+(** takes a normalized processor *)
+let compute_derivation s =
+  if s = Weak then
+    Semop.weak_transitions false global_definition_map
+  else
+    Semop.derivatives global_definition_map
+
+exception Impossible_transition
+
+(* Computes derivations for named actions *)
+let get_matching_derivations_named act tr acc =
+  TSet.fold
+    (fun t acc ->
+      let _, pre, _ = t in
+      match act, pre with
+      | FIn s, T_In n | FOut s, T_Out n ->
+        if s = n then TSet.add t acc else acc
+      | FTau, T_Tau -> TSet.add t acc
+      | _, _ -> acc)
+    tr
+    acc
+
+(* Computes derivation for "polymorphic" actions *)
+let get_matching_derivations io tr =
+  TSet.fold
+    (fun t acc ->
+      let _, pre, _ = t in
+      match io, pre with
+      | In, T_In _ | Out, T_Out _ | _, T_Tau | Any, _ -> TSet.add t acc
+      | _, _ -> acc)
+    tr
+    TSet.empty
+
+
+(* Returns the transitions that matches the actions in the modality *)
+let compute_modality modl tr =
+  match modl with
+  | _, _, Prefix acts ->
+    List.fold_left
+      (fun acc a ->
+        get_matching_derivations_named a tr acc)
+      TSet.empty
+      acts
+  | _, _, (_ as io) ->
+    get_matching_derivations io tr
+
+(** Main function for the local checker *)
+let handle_check_local form proc =
+  let proc = Normalize.normalize proc in
+
+  let rec step proc trace = function
+    | FTrue -> true, trace
+
+    | FFalse -> false, trace
+
+    | FVar v -> failwith (Format.sprintf "This variable is unbound: %s@." v)
+
+    | FPar f -> step proc trace f
+
+    | FNot f -> let r, t = step proc trace f in
+                (not r, t)
+
+    | FAnd (f, g) -> let r1, t1 = step proc trace f in
+                     let r2, t2 = step proc trace g in
+                     if r1 && r2 then true, t1
+                     else if r1 then false, t2
+                     else false, t1
+
+    | FOr (f, g) -> let r1, t1 = step proc trace f in
+                    let r2, _ = step proc trace g in
+                    if r1 || r2 then true, t1
+                    else false, t1 (* both can be considered as an incorrect
+                                      trace *)
+
+    | FImplies (f, g) ->
+      let r1, t1 = step proc trace f in
+      let r2, _t2 = step proc trace g in
+      not r1 || r2, t1
+
+    | FModal (m, f) ->
+      let s,_,_ = m in
+      let d = compute_derivation s proc in
+      let res = compute_modality m d in (* gets the transitions corresponding to
+                                           the modal *)
+      if TSet.is_empty res then (not @@ diamond m, trace)
+      else if diamond m then
+        (* We could have used TSet.exists, but we only can get the boolean
+           results, not the trace *)
+        TSet.fold
+          (fun ((_, m, p') as _tr) (r, t) ->
+            if r then r,t (* no need to test the transition if one is
+                             true *)
+            else step p' (m::t) f)
+          res
+          (false, trace)
+      else
+        TSet.fold
+          (fun (_, m, p') (r, t) ->
+            if not r then r,t (* no need to test the transition if one is
+                                 false *)
+            else step p' (m::t) f)
+          res
+          (true, trace)
+
+    | FInvModal(m, f) ->
+      let r, t = step proc trace @@ FModal (m,f) in
+      (not r, t)
+
+    | FNu (x, s, f) ->
+      if PSet.mem proc s then true, trace
+      else
+        let s = PSet.add proc s in
+        let f = reduce f x @@ FNu(x, s, f) in
+        step proc trace f
+
+    | FMu (x, s, f) ->
+      (* We use the duality of the least fixed point *)
+      let f = FNot (reduce f x @@ FNot (FVar x)) in
+      let f = FNot (FNu (x, s, f))  in
+      step proc trace f
+
+        (* In case that happen, we substitute the prop by its corresponding
+           formula, that shouldn't however *)
+    | FProp (s, il) ->
+      let f = if Hashtbl.mem props s then
+        let (vars, formula) = Hashtbl.find props s in
+        substitute formula @@ List.combine vars il
+      else
+        raise (Unbound_prop s) in
+      step proc trace f
+
+  in
+  let (res, trace) = step proc [] form in
+  if res then
+    Format.printf "The processor given matches the model@."
+  else
+    begin
+      let t = List.rev trace |>
+          List.fold_left (fun acc t ->
+            Format.sprintf "%s --> %s" acc @@ string_of_label t) ""
+      in
+      let t = Format.sprintf "%s --> <stuck>"  t in
+      Format.printf "Doesn't match, here is why: @.%s@." t
+    end
+
+(** Global model checking *)
+
+(** This is not working, those functions are only draft to show the work done to
+    understand and implement the global model checking algorithm *)
+
+let associate_vars f =
+  let rec step f acc =
+    match f with
+    | FTrue | FFalse -> acc
+    | FVar x -> x :: acc
+    | FPar f | FNot f -> step f acc
+    | FAnd (f1, f2) | FImplies (f1, f2) | FOr (f1, f2) ->
+      let acc = step f1 acc in
+      step f2 acc
+    | FModal (_, f) | FInvModal (_, f) -> step f acc
+    | FProp (_,_) -> assert false (* assuming there is no prop at this state *)
+    | FMu (_, _, f) | FNu (_, _, f) -> step f acc
+  in
+  step f []
+
+
+
+let (bdds : (string, Bdd.bdd) Hashtbl.t)= Hashtbl.create 19
+
+
+let rec fix f env name =
+  let rec step f env =
+    let old = SMap.find name env in
+    let env = SMap.add name old env in
+    let res = compute_obdd f env in
+    if HashedBdd.equal res old then res
+    else step f env
+  in
+  step f env
+
+
+and compute_obdd f env =
+
+  let implies b1 b2 = (not b1) || b2 in
+  let xor b1 b2  = ((not b1) && b2) || (b1 && (not b2)) in
+  let rec step f env  =
+    match f with
+    | FTrue -> one
+    | FFalse -> zero
+    | FVar x -> SMap.find x env
+    | FPar f -> step f env
+    | FNot f -> apply xor (step f env) one
+    | FAnd (f1, f2) ->
+      let b1 = step f1 env in
+      let b2 = step f2 env in
+      apply ( && ) b1 b2
+    | FOr (f1, f2) ->
+      let b1 = step f1 env in
+      let b2 = step f2 env in
+      apply ( || ) b1 b2
+    | FImplies (f1, f2) ->
+      let b1 = step f1 env in
+      let b2 = step f2 env in
+      apply implies b1 b2
+    | FModal (m, f) ->
+      if not @@ diamond m then step (FInvModal(m, FNot f)) env
+      else assert false
+    | FInvModal (_m, _f) -> assert false
+    | FProp (name,_) -> Hashtbl.find bdds name
+    | FMu (name, _, f) -> fix f (SMap.add name zero env) name
+    | FNu (name, _, f) -> fix f (SMap.add name one env) name
+
+  in
+  step f env
+
+let bdd_of_formula f name =
+  (* let vars = associate vars f in *)
+  if Hashtbl.mem bdds name then Hashtbl.find bdds name
+  else
+    let bdd = compute_obdd f @@ SMap.empty in
+    (Hashtbl.add bdds name bdd;
+     bdd)
+
+let count_fixpoint f =
+  let rec step f acc count =
+    match f with
+    | FTrue | FFalse -> acc, count
+    | FVar _ -> step f acc count
+    | FPar f | FNot f -> step f acc count
+    | FAnd (f1, f2) | FImplies (f1, f2) | FOr (f1, f2) ->
+      let acc, count = step f1 acc count in
+      step f2 acc count
+    | FModal (_, f) | FInvModal (_, f) -> step f acc count
+    | FProp (_,_) -> assert false
+    | FMu (_, _, f) -> step f ((count, true) :: acc) (count+1)
+    | FNu (_, _, f) -> step f ((count, false) :: acc) (count+1)
+  in
+  step f [] 0
+
+type ens =
+  Top | Bot
+| Trans of io * ens
+| EForAll of ens list
+| Exists of ens list
+
+let rec string_of_ens = function
+  | Top -> "Top"
+  | Bot -> "Bot"
+  | Trans (io, ens) -> "Trans: " ^ (string_of_io io) ^ "->" ^
+    (string_of_ens ens)
+  | EForAll l ->
+    (List.fold_left
+      (fun acc e -> acc ^ "; " ^ (string_of_ens e)) "EForAll:[" l) ^ "]"
+  | Exists l ->
+    (List.fold_left
+      (fun acc e -> acc ^ "; " ^ (string_of_ens e)) "Exists:[" l) ^ "]"
+
+let trans_equiv a b =
+  match a, b with
+  | Any, _ | _, Any -> true
+  | In, In | Out, Out -> true
+  | In, Prefix pl | Prefix pl, In ->
+    List.fold_left
+      (fun acc fp ->
+        match fp with
+        | FTau | FIn _ | FInVar _ -> acc
+        | _ -> false)
+      true
+      pl
+  | Out, Prefix pl | Prefix pl, Out ->
+    List.fold_left
+      (fun acc fp ->
+        match fp with
+        | FTau | FOut _ | FOutVar _ -> acc
+        | _ -> false)
+      true
+      pl
+  | _, _ -> a = b
+
+
+let rec union ens1 ens2 =
+  Format.printf "Union between: %s && %s@." (string_of_ens ens1) (string_of_ens ens2);
+  match ens1, ens2 with
+  | Top, _ | _, Top-> Top
+  | e, Bot | Bot, e -> e
+
+  | Trans (a1, e1), Trans (a2, e2) ->
+    if a1 = a2 then Trans (a1, union e1 e2)
+    else Exists ([ens1; ens2])
+
+  | (Trans (a, e) as t), Exists l
+  | Exists l, (Trans (a, e) as t) ->
+    let added = ref false in
+    let l = List.fold_left
+      (fun acc el ->
+        match el with
+        | Trans (a2, e2) ->
+          if a2 = a then (added := true; Trans (a, union e e2) :: acc)
+          else el :: acc
+        | _ -> el :: acc)
+      []
+      l
+    in
+    let l = if !added then l else t :: l in
+    Exists l
+
+  | (Trans (a, e) as t), (EForAll l) | (EForAll l), (Trans (a, e) as t) ->
+    let added = ref false in
+    let l = List.fold_left
+      (fun acc el ->
+        match el with
+          Trans (a2, e2) ->
+            if a2 = a then (added := true;Trans (a, union e e2) :: acc)
+            else el :: acc
+        | _ -> el :: acc)
+      []
+      l
+    in
+    let l = if !added then l else t :: l in
+    EForAll l
+
+  | EForAll l1, EForAll l2 ->
+    let l = List.fold_left
+      (fun acc e -> union e acc) (EForAll l2) l1 in
+    l
+
+  | Exists l1, Exists l2 ->
+    let l = List.fold_left
+      (fun acc e -> union acc e) (Exists l2) l1 in
+    l
+
+  | (Exists _ as c), (EForAll _ as a) | (EForAll _ as a), (Exists _ as c) ->
+    Exists [c; a]
+
+
+let rec inter ens1 ens2 =
+  Format.printf "Inter between: %s && %s@." (string_of_ens ens1) (string_of_ens ens2);
+  match ens1, ens2 with
+  | _, _ when ens1 = ens2 -> ens1
+  | Top, e | e, Top -> e
+  | _, Bot | Bot, _ -> Bot
+
+  | Trans (a, e1), Trans (b, e2) ->
+    if trans_equiv a b then
+      Trans (a, inter e1 e2)
+    else Bot
+
+  | (Trans (a, e) as t), Exists l | Exists l, (Trans (a, e) as t) ->
+    let added = ref false in
+    let l = List.fold_left
+      (fun acc el ->
+        match el with
+        | Trans (a2, e2) ->
+          if a2 = a then (added := true; Trans (a, inter e e2) :: acc)
+          else el :: acc
+        | _ -> el :: acc)
+      []
+      l
+    in
+    let l = if !added then l else t :: l in
+    Exists l
+
+  | (Trans (a, e) as t), EForAll l | EForAll l, (Trans (a, e) as t) ->
+    let added = ref false in
+    let l = List.fold_left
+      (fun acc el ->
+        match el with
+          Trans (a2, e2) ->
+            if a2 = a then (added := true;Trans (a, inter e e2) :: acc)
+            else el :: acc
+        | _ -> el :: acc)
+      []
+      l
+    in
+    let l = if !added then l else t :: l in
+    EForAll l
+
+  | EForAll l1, EForAll l2 ->
+    let l = List.fold_left
+      (fun acc e -> inter e acc) (EForAll l2) l1 in
+    l
+
+  | Exists l1, Exists l2 ->
+    let l = List.fold_left
+      (fun acc e -> inter acc e) (Exists l2) l1 in
+    l
+
+
+  | (Exists _ as c), (EForAll _ as a) | (EForAll _ as a), (Exists _ as c) ->
+    Exists [c; a]
+
+type fp = Nu | Mu
+
+
+let rec evalrec a f env i =
+  match f with
+  | FTrue -> Top
+  | FFalse -> Bot
+  | FVar v -> SMap.find v env
+  | FPar f -> evalrec a f env i
+
+  | FAnd (f1, f2) ->
+    let e1 = evalrec a f1 env i in
+    let e2 = evalrec a f2 env i in
+    inter e1 e2
+
+  | FOr (f1, f2) ->
+    let e1 = evalrec a f1 env i in
+    let e2 = evalrec a f2 env i in
+    union e1 e2
+
+  | FModal (m, f) | FInvModal (m, f) ->
+    let _, m, io = m in
+    let f = evalrec a f env i in
+    (match m with
+    | Possibly -> Exists([Trans(io, f)])
+    | _ -> EForAll([Trans(io, f)]))
+
+  | FMu (v, _, f) -> fixpoint a Mu v f i env
+  | FNu (v, _, f) -> fixpoint a Nu v f i env
+  | FProp (_, _) -> assert false
+  | FNot _ -> assert false
+  | FImplies (_, _) -> assert false
+
+and fixpoint a fp var f i env =
+  let ens = match fp with Mu -> Top | Nu -> Bot in
+  for j=0 to i-1 do
+    let (ty, _) = a.(j) in
+    if ty = fp then a.(j) <- ty, ens
+  done;
+  let r_old = ref a.(i) in
+  let first = ref true in
+  while !r_old <> a.(i) || !first do
+    first := false;
+    let ty, ens = a.(i) in
+    r_old := ty, ens;
+    let env = SMap.add var ens env in
+    a.(i) <- ty, evalrec a f env (i+1);
+  done;
+  let _, ens = a.(i) in
+  ens
+
+let check_ens ens proc =
+
+  (* let get_matching_deriv s p a = *)
+  (*   let deriv = compute_derivation s p in *)
+  (*   TSet.fold *)
+  (*     (fun ((_, m, p') as _tr) acc -> *)
+  (*       step p' (m::t) f) *)
+  (*     deriv *)
+  (*     [] *)
+  (* in *)
+
+  let _proc = Normalize.normalize proc in
+  let res = match ens with
+    | Bot -> false
+    | Top -> true
+    | Trans(_a, _e) -> assert false
+      (* let m = Strong, Possibly, a in (\* The first two are just to match the *)
+      (*                                   modality scheme *\) *)
+      (* let d = compute_derivation Strong proc in *)
+      (* let res = compute_modality m d in *)
+      (* if TSet.is_empty res then false *)
+      (* else if diamond m then *)
+      (*   TSet.fold *)
+      (*     (fun ((_, m, p') as _tr) (r, t) -> *)
+      (*       (\* Format.printf "t: %s@." @@ string_of_transition tr; *\) *)
+      (*       if r then r,t (\* no need to test the transition if one is *)
+      (*                        true *\) *)
+      (*       else step p' (m::t) f) *)
+      (*     res *)
+      (*     false *)
+    | Exists _l -> assert false
+    | EForAll _l -> assert false
+  in
+  res
+
+let check_global f _ =
+  let acc, n = count_fixpoint f in
+  let a = Array.make n (Mu, Top) in
+  let rec make acc =
+    match acc with
+    | [] -> ()
+    | (i, b)::l ->
+      a.(i) <- if b then Mu, Top else Nu, Bot;
+      make l
+  in
+  make acc;
+  let ens = evalrec a f SMap.empty 0 in
+  Format.printf "Ens: %s@." @@ string_of_ens ens
diff --git a/src/Control.ml b/src/Control.ml
index 405bd6a..761949e 100644
--- a/src/Control.ml
+++ b/src/Control.ml
@@ -1,5 +1,5 @@
 open Printf
-
+open Global
 open Utils
 open Syntax
 open Normalize
@@ -39,11 +39,11 @@ let script_mode = ref false ;;
 exception Constdef_Exception of string ;;
 exception Typedef_Exception of string ;;
 
-let handle_help () = 
+let handle_help () =
   printf "%s\n> %!" help_me
 
 let handle_quit () =
-  printf "bye bye !\n%!" ; 
+  printf "bye bye !\n%!" ;
   exit 0
 
 let timing operation =
@@ -51,13 +51,13 @@ let timing operation =
   in let result = operation()
      in let end_time = Sys.time()
         in
-        (result, end_time -. start_time) 
+        (result, end_time -. start_time)
 
 let handle_constdef (const_name:string) (const_val:int) =
   (* printf "(handle_constdef %s %d)\n%!" const_name const_val ; *)
   if not (SMap.mem const_name !Presyntax.env_const) then
     Presyntax.env_const := SMap.add const_name const_val !Presyntax.env_const
-  else 
+  else
     raise (Constdef_Exception const_name)
 ;;
 
@@ -65,10 +65,10 @@ let handle_typedef_range (type_name:string) (min_val:string) (max_val:string) =
   (* printf "(handle_typedef_range %s %s %s)\n%!" type_name min_val max_val ; *)
   if not (SMap.mem type_name !Presyntax.env_type) then
     let find_val v =
-      try 
-	SMap.find v !Presyntax.env_const 
+      try
+	SMap.find v !Presyntax.env_const
       with
-	Not_found -> 
+	Not_found ->
 	  try
 	    int_of_string v
 	  with
@@ -76,14 +76,14 @@ let handle_typedef_range (type_name:string) (min_val:string) (max_val:string) =
     in
     let min = find_val min_val
     and max = find_val max_val in
-    
-    Presyntax.add_to_env_type type_name 
-      ( if min < max then 
+
+    Presyntax.add_to_env_type type_name
+      ( if min < max then
 	  Presyntax.PTDefRange (type_name, min, max)
 	else
 	  Presyntax.PTDefRange (type_name, max, min)
-      ) 
-  else 
+      )
+  else
     raise (Typedef_Exception type_name)
 ;;
 
@@ -96,7 +96,7 @@ let handle_typedef_enum (type_name:string) (names:string list) =
   in
   if not (SMap.mem type_name !Presyntax.env_type) then
     Presyntax.add_to_env_type type_name ( Presyntax.PTDefEnum (type_name, list2set names) )
-  else 
+  else
     raise (Typedef_Exception type_name)
 ;;
 
@@ -122,7 +122,7 @@ let handle_normalization proc =
   let proc',time = timing (fun () -> normalize proc)
   in
   printf "%s\n%!" (string_of_nprocess proc') ;
-  printf "(elapsed time=%fs)\n%!" time 
+  printf "(elapsed time=%fs)\n%!" time
 
 let handle_struct_congr p q =
   if !script_mode then
@@ -133,9 +133,7 @@ let handle_struct_congr p q =
   (if ok
    then printf "the processes *are* structurally congruent\n%!"
    else printf "the processes are *not* structurally congruent\n%!") ;
-  printf "(elapsed time=%fs)\n%!" time 
-
-let global_definition_map = Hashtbl.create 64
+  printf "(elapsed time=%fs)\n%!" time
 
 let common_deriv f_deriv f_print str str2 p =
   if !script_mode then
@@ -143,12 +141,12 @@ let common_deriv f_deriv f_print str str2 p =
   printf "Compute %s...\n%!" str2;
   let op = fun () ->
     let np = normalize p in
-    f_deriv global_definition_map np 
+    f_deriv global_definition_map np
   in
   let derivs, time = timing op
   in
   f_print derivs;
-  printf "(elapsed time=%fs)\n%!" time 
+  printf "(elapsed time=%fs)\n%!" time
 
 let fetch_definition key =
   Hashtbl.find global_definition_map key
@@ -166,7 +164,7 @@ let dot_style_format (p, l, p') =
   sprintf "\"%s\" -> \"%s\" [ label = \"%s\", fontcolor=red ]"
     (string_of_nprocess p) (string_of_nprocess p') (string_of_label l)
 
-let dot_style_format' (pl, l, pl') = 
+let dot_style_format' (pl, l, pl') =
   sprintf "\"%s\" -> \"%s\" [ label = \"%s\", fontcolor=red ]"
     (string_of_list string_of_nprocess pl)
     (string_of_list string_of_nprocess pl')
@@ -175,7 +173,7 @@ let dot_style_format' (pl, l, pl') =
 let common_lts f str p =
   if !script_mode then
     printf "> %s %s\n%!" str (string_of_process p) ;
-  let transs, time = timing (fun () -> f global_definition_map (normalize p)) 
+  let transs, time = timing (fun () -> f global_definition_map (normalize p))
   in
   List.iter (fun t -> printf "%s\n" (string_of_transition t)) transs;
   printf "\nGenerating %s.dot... %!" str;
@@ -194,23 +192,23 @@ let common_lts f str p =
   fprintf oc "}\n";
   close_out oc;
   printf "done\n(elapsed time=%fs)\n%!" time
- 
+
 let common_minimization f_deriv str proc =
   if !script_mode then
     printf "> %s %s\n%!" str (string_of_process proc) ;
   printf "Minimize process...\n%!";
   let transs, time = timing (fun () ->
     let p = normalize proc in
-    minimize f_deriv global_definition_map p) 
+    minimize f_deriv global_definition_map p)
   in
   List.iter (fun t -> printf "%s\n" (string_of_transitions t)) transs;
   printf "\nGenerating lts_mini.dot... %!";
-  let nprocs = 
+  let nprocs =
     List.fold_left (fun acc (x, _, y) -> x::(y::acc)) [] transs
   in
   let oc = open_out "lts_mini.dot" in
   fprintf oc "digraph LTSMINI {\n";
-  List.iter 
+  List.iter
     (fun x -> fprintf oc "\"%s\" [ fontcolor=blue ]\n"
       (string_of_list string_of_nprocess x))
     nprocs;
@@ -221,7 +219,7 @@ let common_minimization f_deriv str proc =
   printf "done\n(elapsed time=%fs)\n%!" time
 
 
-let common_bisim f_bisim str str2 str3 p1 p2 = 
+let common_bisim f_bisim str str2 str3 p1 p2 =
   if !script_mode then
     printf "> %s %s ~ %s\n%!" str (string_of_process p1) (string_of_process p2) ;
   printf "Calculate %s...\n%!" str2;
@@ -230,7 +228,7 @@ let common_bisim f_bisim str str2 str3 p1 p2 =
   let np1 = normalize p1 in
   let np2 = normalize p2 in
   try
-    let bsm = f_bisim global_definition_map np1 np2 
+    let bsm = f_bisim global_definition_map np1 np2
     in
     let end_time = Sys.time()
     in
@@ -252,10 +250,10 @@ let common_is_bisim f_bisim str str2 p1 p2 =
     let np2 = normalize p2 in
     f_bisim global_definition_map np1 np2)
   in
-  if ok 
+  if ok
   then printf "the processes *are* %s\n(elapsed time=%fs)\n%!" str2 time
   else printf "the processes are *not* %s\n(elapsed time=%fs)\n%!" str2 time
-    
+
 let common_is_fbisim f_deriv str1 str2 p1 p2 =
 if !script_mode then
     printf "> %s ? %s ~ %s\n%!" str1 (string_of_process p1) (string_of_process p2) ;
@@ -300,14 +298,14 @@ let handle_wderiv p = common_deriv (weak_derivatives false) printPfixMap "wderiv
 let handle_tderiv p = common_deriv (weak_derivatives true) printPfixMap "tderiv" "tau derivatives" p
 
 
+(*** Mu-Calculus part *)
 
-let handle_prop _ _ _ = failwith "TODO"
-
-let handle_check_local _ _ = failwith "TODO"
-
-let handle_check_global _ _ = failwith "TODO"
-
-
+let handle_prop name idents formula =
 
+  Formula.add_prop name idents formula(* ; *)
+  (* ignore (Check.bdd_of_formula formula name) *)
 
+let handle_check_local =
+  Check.handle_check_local
 
+let handle_check_global = Check.check_global
diff --git a/src/Formula.ml b/src/Formula.ml
index 3fddb71..757d774 100644
--- a/src/Formula.ml
+++ b/src/Formula.ml
@@ -1,75 +1,460 @@
 (*** Representation of mu-calculus formulae ***)
 
 open Printf
-
+open Semop
 open Presyntax
 open Utils
 
-(* mu-calculus formulae *)
-
-type modality =
-  | FPossibly of preprefix list
-  | FOutPossibly
-  | FInPossibly
-  | FAnyPossibly
-  | FWPossibly of preprefix list
-  | FWOutPossibly
-  | FWInPossibly
-  | FWAnyPossibly
-  | FNecessity of preprefix list
-  | FOutNecessity
-  | FInNecessity
-  | FAnyNecessity
-  | FWNecessity of preprefix list
-  | FWOutNecessity
-  | FWInNecessity
-  | FWAnyNecessity
-
-let string_of_modality : modality -> string = function
-  | FPossibly(acts) -> string_of_collection "<" ">" ","  string_of_preprefix acts
-  | FOutPossibly -> "<!>"
-  | FInPossibly -> "<?>"
-  | FAnyPossibly -> "<.>"
-  | FWPossibly(acts) -> string_of_collection "<<" ">>" ","  string_of_preprefix acts
-  | FWOutPossibly -> "<<!>>"
-  | FWInPossibly -> "<<?>>"
-  | FWAnyPossibly -> "<<.>>"
-  | FNecessity(acts) -> string_of_collection "[" "]" ","  string_of_preprefix acts
-  | FOutNecessity -> "[!]"
-  | FInNecessity -> "[?]"
-  | FAnyNecessity -> "[.]"
-  | FWNecessity(acts) -> string_of_collection "[[" "]]" ","  string_of_preprefix acts
-  | FWOutNecessity -> "[[!]]"
-  | FWInNecessity -> "[[?]]"
-  | FWAnyNecessity -> "[[.]]"
-
-type formula = 
+(** Type of "named" prefix *)
+type fprefix =
+| FIn of string
+| FInVar of string
+| FOut of string
+| FOutVar of string
+| FTau
+
+(** Takes a preprefix and gives its corresponding fprefix to be used correctly in
+   the formula *)
+let fprefix_of_preprefix = function
+  | PIn (PName n) -> FIn n
+  | POut (PName n) -> FOut n
+  | PIn (PVar n) -> FInVar n (* (String.sub n 1 (String.length n - 1)) *)
+  | POut (PVar n) -> FOutVar n (* (String.sub n 1 (String.length n - 1)) *)
+  | PTau -> FTau
+  | _ as pr -> failwith (Format.sprintf "Received : %s@." @@ string_of_preprefix pr)
+
+let string_of_fprefix = function
+  | FIn n -> n ^ "?"
+  | FInVar n -> "var:" ^ n ^ "?"
+  | FOut n -> n ^ "!"
+  | FOutVar n -> "var:" ^ n ^ "!"
+  | FTau -> "tau"
+
+(** Transform a preprefix list into a fprefix list *)
+let parse_preprefix_list =
+  List.map fprefix_of_preprefix
+
+(** Types used to represent modalities *)
+type strongness = Strong | Weak
+type modal = Possibly | Necessity
+type io =
+  In | Out | Any | Prefix of fprefix list
+
+type modality = strongness * modal * io
+
+let string_of_io = function
+  | In -> "?"
+  | Out -> "!"
+  | Any -> "."
+  | Prefix pl -> List.fold_left
+    (fun acc p -> acc ^ "," ^ (string_of_fprefix p))
+    (string_of_fprefix (List.hd pl))
+    (List.tl pl)
+
+
+let string_of_modality (s, m, io) =
+  let io = string_of_io io  in
+  match s, m with
+    | Strong, Possibly -> Format.sprintf "<%s>" io
+    | Strong, Necessity -> Format.sprintf "[%s]" io
+    | Weak, Possibly -> Format.sprintf "<<%s>>" io
+    | Weak, Necessity -> Format.sprintf "[[%s]]" io
+
+let diamond = function
+  | _, Possibly, _ -> true
+  | _, _, _ -> false
+
+(** Type to represent preformula, particularely the ForAll and Exists terms *)
+type preformula =
+  | PFTrue
+  | PFFalse
+  | PFPar of preformula
+  | PFAnd of preformula * preformula
+  | PFOr of preformula * preformula
+  | PFImplies of preformula * preformula
+  | PFModal of modality * preformula
+  | PFInvModal of modality * preformula
+  | PFProp of string * (preformula list)
+  | PFVar of string
+  | PFMu of string * preformula
+  | PFNu of string * preformula
+  | PFForall of preparam * preexpr * preformula
+  | PFExists of preparam * preexpr * preformula
+
+let rec string_of_preformula : preformula -> string = function
+  | PFTrue -> "True"
+  | PFFalse -> "False"
+  | PFPar f -> sprintf "(%s)" @@ string_of_preformula f
+  | PFAnd(f,g) -> sprintf "(%s and %s)" (string_of_preformula f) (string_of_preformula g)
+  | PFOr(f,g) -> sprintf "(%s or %s)" (string_of_preformula f) (string_of_preformula g)
+  | PFImplies(f,g) -> sprintf "(%s ==> %s)" (string_of_preformula f) (string_of_preformula g)
+  | PFModal(m,f) -> (string_of_modality m) ^ (string_of_preformula f)
+  | PFInvModal(m,f) ->  "~" ^ (string_of_modality m) ^ (string_of_preformula f)
+  | PFProp(prop,params) -> prop ^
+    (string_of_collection "(" ")" ","
+       (fun s ->
+         string_of_preformula s)
+       params)
+  | PFVar(var) -> var
+  | PFMu(x,f) -> sprintf "Mu(%s).%s" x (string_of_preformula f)
+  | PFNu(x,f) -> sprintf "Nu(%s).%s" x (string_of_preformula f)
+  | PFForall (par, pe, f) ->
+    sprintf "(forall %s, %s in %s)"
+      (string_of_preparam par) (string_of_preexpr pe) (string_of_preformula f)
+  | PFExists (par, pe, f) ->
+    sprintf "(exists %s, %s in %s)"
+      (string_of_preparam par) (string_of_preexpr pe) (string_of_preformula f)
+
+(** Similar to preformula, without the quantifying clauses *)
+type formula =
   | FTrue
   | FFalse
+  | FPar of formula
   | FAnd of formula * formula
   | FOr of formula * formula
   | FImplies of formula * formula
   | FModal of modality * formula
   | FInvModal of modality * formula
-  | FProp of string * (string list)
+  | FProp of string * (formula list)
   | FVar of string
-  | FMu of string * formula
-  | FNu of string * formula
- 
+  | FMu of string * PSet.t * formula
+  | FNu of string * PSet.t * formula
+  | FNot of formula (* considered only internaly *)
+
 let rec string_of_formula : formula -> string = function
   | FTrue -> "True"
   | FFalse -> "False"
+  | FPar f -> sprintf "(%s)" @@ string_of_formula f
   | FAnd(f,g) -> sprintf "(%s and %s)" (string_of_formula f) (string_of_formula g)
   | FOr(f,g) -> sprintf "(%s or %s)" (string_of_formula f) (string_of_formula g)
   | FImplies(f,g) -> sprintf "(%s ==> %s)" (string_of_formula f) (string_of_formula g)
   | FModal(m,f) -> (string_of_modality m) ^ (string_of_formula f)
   | FInvModal(m,f) ->  "~" ^ (string_of_modality m) ^ (string_of_formula f)
-  | FProp(prop,params) -> prop ^ (string_of_collection "(" ")" "," (fun s -> s) params)
+  | FProp(prop,params) ->
+    prop ^ (string_of_collection "(" ")" ","
+              (fun s ->
+                string_of_formula s)
+              params)
   | FVar(var) -> var
-  | FMu(x,f) -> sprintf "Mu(%s).%s" x (string_of_formula f)
-  | FNu(x,f) -> sprintf "Nu(%s).%s" x (string_of_formula f)
-  
+  | FMu(x, _, f) -> sprintf "Mu(%s).%s" x (string_of_formula f)
+  | FNu(x, _, f) -> sprintf "Nu(%s).%s" x (string_of_formula f)
+  | FNot f -> sprintf "~%s" @@ string_of_formula f
+
+(** A prop is a list of bound variables and its formulas *)
+type prop = string list * formula
+
+let props : (string, prop) Hashtbl.t = Hashtbl.create 53
+
+exception Formdef_exception of string
+exception Unbound_variable of string
+exception Unbound_prop of string
+
+(** Will verify if every variable is bound in the prop *)
+let rec verify_vars f idents =
+  match f with
+  | FVar v -> if not (List.mem v idents) then raise (Unbound_variable v)
+  | FAnd (f,g) | FOr (f,g) | FImplies (f,g) ->
+    verify_vars f idents; verify_vars g idents
+  | FModal (_, f) | FInvModal (_, f) -> verify_vars f idents
+  | FMu (x,_,f) | FNu (x,_,f) -> verify_vars f (x :: idents)
+  (* | FProp (_, l) -> List.iter (fun v -> verify_vars (FVar v) idents) l *)
+  | _ -> ()
+
+(** val add_prop : string -> string list -> formula -> unit *)
+let add_prop name idents formula =
+  if Hashtbl.mem props name then
+    raise (Formdef_exception name)
+  else
+    begin
+      verify_vars formula idents;
+      Hashtbl.add props name (idents, formula)
+    end
+
+module IMap = Map.Make(
+  struct
+    type t = int
+    let compare = compare
+ end)
+
+(** Converts a variable name to avoid multiple definitions. Never used however,
+    since the fixed points variables are always in tail position *)
+let alpha_convert f =
+  let i = ref 0 in
+  let rec step f env =
+    match f with
+    | FVar v ->
+      if SMap.mem v env then FVar (SMap.find v env)
+      else FVar v
+
+    | FTrue | FFalse as f -> f
+    | FPar f -> FPar (step f env)
+    | FNot f -> FNot (step f env)
+    | FAnd (f, g) -> FAnd (step f env, step g env)
+    | FOr (f, g) -> FOr (step f env, step g env)
+    | FImplies (f, g) -> FImplies (step f env, step g env)
+    | FModal(m, f) -> FModal (m, step f env)
+    | FInvModal (m, f) -> FInvModal (m, step f env)
+    | FMu (x, s, f) ->
+      let nx = x ^ "_" ^ (string_of_int !i) in
+      let env = SMap.add x nx env in
+      incr i;
+      FMu (nx, s, step f env)
+    | FNu (x, s, f) ->
+      let nx = x ^ "_" ^ (string_of_int !i) in
+      let env = SMap.add x nx env in
+      incr i;
+      FNu (x, s, step f env)
+    | FProp (_,_) -> f
+  in
+  step f SMap.empty
+
+(** Replaces a var in f by the formula given *)
+let reduce f var value =
+  let rec step = function
+  | FVar v -> if v = var then value else FVar v
+  | FTrue | FFalse as f -> f
+  | FPar f -> FPar (step f)
+  | FNot f -> FNot (step f)
+  | FAnd (f, g) -> FAnd (step f, step g)
+  | FOr (f, g) -> FOr (step f, step g)
+  | FImplies (f, g) -> FImplies (step f, step g)
+  | FModal(m, f) -> FModal (m, step f)
+  | FInvModal (m, f) -> FInvModal (m, step f)
+  | FMu (x, s, f) -> FMu (x, s, step f)
+  | FNu (x, s, f) -> FNu (x, s, step f)
+  | _ -> failwith (string_of_formula f)
+  in
+  step f
+
+(** Replaces each Var by its correspondance. Works as a reduce for multiple
+    vars. Assumes each variable is correctly bound *)
+let substitute f sub_list =
+  let rec step sl = function
+  | FVar v -> List.assoc v sl
+  | FTrue | FFalse as f -> f
+  | FPar f -> FPar (step sl f)
+  | FAnd (f, g) -> FAnd (step sl f, step sl g)
+  | FOr (f, g) -> FOr (step sl f, step sl g)
+  | FImplies (f, g) -> FImplies (step sl f, step sl g)
+  | FModal(m, f) -> FModal (m, step sl f)
+  | FInvModal (m, f) -> FInvModal (m, step sl f)
+  | FMu (x, s, f) -> FMu (x, s, step ((x, FVar x)::sl) f)
+  | FNu (x, s, f) -> FNu (x, s, step ((x, FVar x)::sl) f)
+  | _ -> assert false (* Technically, no Prop should remain ? *)
+  in
+  step sub_list f
+
+(** Inlines a prop call *)
+let substitute_prop f =
+  let rec step = function
+    | FTrue | FFalse as f -> f
+    | FPar f -> FPar (step f)
+    | FAnd (f, g) -> FAnd (step f, step g)
+    | FOr (f, g) -> FOr (step f, step g)
+    | FImplies (f, g) -> FImplies (step f, step g)
+    | FModal(m, f) -> FModal (m, step f)
+    | FInvModal (m, f) -> FInvModal (m, step f)
+    | FVar v -> FVar v
+    | FMu (x, s, f) -> FMu (x, s, step f)
+    | FNu (x, s, f) -> FNu (x, s, step f)
+    | FNot f -> FNot (step f)
+    | FProp (s, fl) ->
+      if Hashtbl.mem props s then
+        let (vars, formula) = Hashtbl.find props s in
+        substitute formula @@ List.combine vars fl
+      else
+        raise (Unbound_prop s)
+  in
+  step f
+
+(** Renames a modality *)
+let substitute_modality m vars =
+  let rename_modal (s,mo,io) =
+    match io with
+    | In | Out | Any -> m
+    | Prefix l ->
+      s, mo, Prefix (List.map
+        (fun fpref ->
+          match fpref with
+          | FTau -> FTau
+          | FOut _ | FIn _ -> fpref
+          | FInVar s ->
+            if SMap.mem s vars then
+              let n = String.sub s 1 @@ String.length s - 1 in
+              FIn (n ^ "_" ^ (string_of_int @@ int_of_value @@ (SMap.find s vars)))
+            else fpref
+          | FOutVar s -> if SMap.mem s vars then
+              let n = String.sub s 1 @@ String.length s - 1 in
+              FOut (n ^ "_" ^ (string_of_int @@ int_of_value @@ (SMap.find s vars)))
+            else fpref)
+        l)
+  in
+  rename_modal m
+
+(** Computes a preformula quantified into a correct formula *)
+let formula_of_preformula pf =
+  let open Syntax in
+  let compute_param p =
+    match p with
+    | PParamVar (n, t) ->
+      if not @@ SMap.mem t !env_type then failwith "Not found" else
+      n, value_list (SMap.find t !env_type)
+    | _ -> failwith
+      (Format.sprintf "Unusable param for mu-calculus:%s@." @@ string_of_preparam p)
+  in
+
+  (* From Presyntax, modified not to used a global hashtbl, but a local map
+     instead *)
+  let rec test_expr vars = function
+    | PTrue -> Bool true
+    | PFalse -> Bool false
+    | PInt i -> Int i
+    | PName str -> Name str
+    | PConst name -> Int (SMap.find name !env_const)
+    | PVar name -> if not @@ SMap.mem name vars then
+        failwith "Var not found"
+      else
+        (SMap.find name vars)
+    | PNot pexpr -> let b = bool_of_value (test_expr vars pexpr) in Bool (not b)
+    | PAnd (preexpr1, preexpr2) ->
+      let b1 = bool_of_value (test_expr vars preexpr1)
+      and b2 = bool_of_value (test_expr vars preexpr2) in
+      Bool ( b1 && b2 )
+    | POr (preexpr1, preexpr2) ->
+      let b1 = bool_of_value (test_expr vars preexpr1)
+      and b2 = bool_of_value (test_expr vars preexpr2) in
+      Bool ( b1 || b2 )
+
+    | PAdd (preexpr1, preexpr2) ->
+      let i1 = int_of_value (test_expr vars preexpr1 )
+      and i2 = int_of_value ( test_expr vars preexpr2 ) in
+      Int ( i1 + i2 )
+
+    | PSub (preexpr1, preexpr2) ->
+      let i1 = int_of_value (test_expr vars preexpr1 )
+      and i2 = int_of_value ( test_expr vars preexpr2 ) in
+      Int ( i1 - i2 )
+
+    | PMul (preexpr1, preexpr2) ->
+      let i1 = int_of_value (test_expr vars preexpr1 )
+      and i2 = int_of_value ( test_expr vars preexpr2 ) in
+      Int ( i1 * i2 )
+
+    | PDiv (preexpr1, preexpr2) ->
+      let i1 = int_of_value (test_expr vars preexpr1 )
+      and i2 = int_of_value ( test_expr vars preexpr2 ) in
+      Int ( i1 / i2 )
+
+    | PMod (preexpr1, preexpr2) ->
+      let i1 = int_of_value (test_expr vars preexpr1 )
+      and i2 = int_of_value ( test_expr vars preexpr2 ) in
+      Int ( i1 mod i2 )
+
+    | PInf (preexpr1, preexpr2) ->
+      let i1 = int_of_value (test_expr vars preexpr1 )
+      and i2 = int_of_value ( test_expr vars preexpr2 ) in
+      Bool ( i1 < i2 )
+
+    | PSup (preexpr1, preexpr2) ->
+      let i1 = int_of_value (test_expr vars preexpr1 )
+      and i2 = int_of_value ( test_expr vars preexpr2 ) in
+      Bool ( i1 > i2 )
+
+    | PEq (preexpr1, preexpr2) ->
+      let p1 = test_expr vars preexpr1
+      and p2 = test_expr vars preexpr2 in
+      (match (p1, p2) with
+      | (Bool b1, Bool b2) -> Bool ( b1 = b2 )
+      | (Int i1, Int i2) -> Bool ( i1 = i2 )
+      | (Name n1, Name n2) -> Bool ( n1 = n2 )
+      | (_, _) -> Bool ( false ))
+
+    | PNeq (preexpr1, preexpr2) ->
+      let p1 = test_expr vars preexpr1
+      and p2 = test_expr vars preexpr2 in
+      (match (p1, p2) with
+      | (Bool b1, Bool b2) -> Bool ( b1 <> b2 )
+      | (Int i1, Int i2) -> Bool ( i1 <> i2 )
+      | (Name n1, Name n2) -> Bool ( n1 <> n2 )
+      | (_, _) -> Bool ( true ))
+
+    | PInfEq (preexpr1, preexpr2) ->
+      let i1 = int_of_value (test_expr vars preexpr1 )
+      and i2 = int_of_value ( test_expr vars preexpr2 ) in
+      Bool ( i1 <= i2 )
+
+    | PSupEq (preexpr1, preexpr2) ->
+      let i1 = int_of_value (test_expr vars preexpr1 )
+      and i2 = int_of_value ( test_expr vars preexpr2 ) in
+      Bool ( i1 >= i2 )
+
+    | PIf (cond, preexpr1, preexpr2) ->
+      let b = bool_of_value (test_expr vars cond) in
+      if b then
+        test_expr vars preexpr1
+      else
+        test_expr vars preexpr2
+  in
+
+  let res_of_expr e vars =
+    match test_expr vars e with
+    | Bool b -> b
+    | _ -> failwith "The result of the expression wasn't a boolean expression"
+  in
+
+  let rec step vars = function
+    | PFTrue -> FTrue
+    | PFFalse -> FFalse
+    | PFPar f -> FPar (step vars f)
+    | PFAnd (f, g) -> FAnd (step vars f, step vars g)
+    | PFOr (f, g) -> FOr (step vars f, step vars g)
+    | PFImplies (f, g) -> FImplies (step vars f, step vars g)
+    | PFModal(m, f) -> FModal (substitute_modality m vars, step vars f)
+    | PFInvModal (m, f) -> FInvModal (substitute_modality m vars, step vars f)
+    | PFVar v -> FVar v
+    | PFMu (x, f) -> FMu (x, PSet.empty, step vars f)
+    | PFNu (x, f) -> FNu (x, PSet.empty, step vars f)
+
+    | PFProp (s, pfl) -> (* inlining *)
+      if Hashtbl.mem props s then
+        let (vars', formula) = Hashtbl.find props s in
+        let fl = List.map (step vars) pfl in
+        substitute formula @@ List.combine vars' fl
+      else
+        raise (Unbound_prop s)
+
+(* The next two cases compute the qunatification, modifying the modalities to
+   the value given by the quantification *)
+    | PFForall (param, expr, f) ->
+      let n, val_list = compute_param param in
+      List.fold_left
+        (fun acc_f i ->
+          let vars = SMap.add n i vars in
+          let b = res_of_expr expr vars in
+          if b then
+            let f = step vars f in
+            if acc_f = FTrue then f
+            else FAnd (f, acc_f)
+          else acc_f)
+        FTrue
+        val_list
 
-let formula_of_preformula : formula -> formula =
-  failwith "TODO" 
+    | PFExists (param, expr, f) ->
+      let n, val_list = compute_param param in
+      List.fold_left
+        (fun acc_f i ->
+          let vars = SMap.add n i vars in
+          let b = res_of_expr expr vars in
+          if b then
+            let f = step vars f in
+            if acc_f = FFalse then f
+            else FOr (f, acc_f)
+          else acc_f)
+        FFalse
+        val_list
 
+  in
+  Format.printf "Preformula received :\n%s@." @@ string_of_preformula pf;
+  let res = step SMap.empty pf in
+  Format.printf "Result :\n%s@." @@ string_of_formula res;
+  res
diff --git a/src/Global.ml b/src/Global.ml
new file mode 100644
index 0000000..4cb4a59
--- /dev/null
+++ b/src/Global.ml
@@ -0,0 +1,5 @@
+(** Contains global definitiions that can be used by multiple modules. Avoid
+    circular dependencies *)
+
+
+let global_definition_map : (string, Syntax.definition) Hashtbl.t = Hashtbl.create 64
diff --git a/src/Lexer.mll b/src/Lexer.mll
index 7decd26..432d00b 100644
--- a/src/Lexer.mll
+++ b/src/Lexer.mll
@@ -1,5 +1,5 @@
 
-{ 
+{
   open Parser
   let line=ref 1
 
@@ -11,7 +11,7 @@ let digit = ['0'-'9']
 let int = (['1'-'9'] digit*)
 
 let cmt = ('#' [^'\n']*)
-  
+
 let r_def = "def"
 let r_true = "true"
 let r_false = "false"
@@ -63,6 +63,7 @@ let tild = "~"
 let semicol = ";"
 let ws = (['\t' ' ']*)
 let colon = ':'
+let whereas = "|"
 
 let implies_1 = "==>"
 let implies_2 = "=>"
@@ -92,6 +93,9 @@ let cmd_check = "check"
 let cmd_check_local = "checklocal"
 let cmd_check_global = "checkglobal"
 
+let forall = "forall"
+let exists = "exists"
+
 let sat_1 = "|-"
 let sat_2 = "satisfies"
 
@@ -105,7 +109,7 @@ let nu_3 = "NU"
   rule token = parse
     | ws
 	{token lexbuf}
-    | eol                                
+    | eol
 	{ incr line;
 	  token lexbuf }
     | cmt
@@ -134,8 +138,8 @@ let nu_3 = "NU"
     | r_const { CONSTDEF }
     | r_type { TYPEDEF }
     | dotdot { DOTDOT }
-    | op_dot { DOT } 
-    | op_plus { PLUS } 
+    | op_dot { DOT }
+    | op_plus { PLUS }
     | op_minus { MINUS }
     | op_par { PAR }
     | op_out { OUT }
@@ -169,7 +173,8 @@ let nu_3 = "NU"
     | cmd_free { FREE }
     | cmd_bound { BOUND }
     | cmd_names { NAMES }
-	
+    | whereas { WHEREAS }
+
     | implies_1 { IMPLIES }
     | implies_2 { IMPLIES }
 
@@ -180,6 +185,9 @@ let nu_3 = "NU"
     | cmd_wmini { WMINI }
     | cmd_wfbisim { WFBISIM }
 
+    | forall { FORALL }
+    | exists { EXISTS }
+
     | mu_1 { MU }
     | mu_2 { MU }
     | mu_3 { MU }
@@ -195,14 +203,14 @@ let nu_3 = "NU"
 
     | sat_1 { SATISFY }
     | sat_2 { SATISFY }
-  
+
     | cmd_help { HELP }
     | cmd_quit { QUIT }
-    | ident as id                   
+    | ident as id
 	{ IDENT (id) }
     | eof { EOF }
-    | _ { failwith((Lexing.lexeme lexbuf) ^ 
+    | _ { failwith((Lexing.lexeme lexbuf) ^
 		      ": mistake at line " ^ string_of_int !line)}
-	
+
 	{
 	}
diff --git a/src/Minim.ml b/src/Minim.ml
index 8b59e81..2f545bc 100755
--- a/src/Minim.ml
+++ b/src/Minim.ml
@@ -52,7 +52,7 @@ let string_of_graph g =
   in
     GMap.fold folder g ""
 
-let string_of_partition parts = 
+let string_of_partition parts =
   (List.fold_left
     (fun s part -> s ^ "\n" ^ (string_of_gset string_of_gstate part)) "" parts)
     ^ "\n"
@@ -109,12 +109,12 @@ let build_graph f_deriv init_graph init_partition defs ps =
     | _ -> (init_graph, init_partition)
 
 let rec refine (graph, part) =
-  let prevs = 
+  let prevs =
     List.map (fun x ->
       GSet.fold (fun x' acc -> GSet.union acc (GMap.find x' graph))
 	x GSet.empty) part
   in
-  let split part prev = 
+  let split part prev =
     let p1 = GSet.inter part prev in
     let p2 = GSet.diff part prev in
     (p1, p2)
@@ -123,7 +123,7 @@ let rec refine (graph, part) =
     match pt with
       | [] -> []
       | h1::t1 -> (f2 h1 pr)@(f1 t1 pr)
-  and f2 pt pr = 
+  and f2 pt pr =
     match pr with
       | [] -> [pt]
       | h2::t2 -> let (spl1, spl2) = split pt h2 in
@@ -137,7 +137,7 @@ let rec refine (graph, part) =
   then part' else refine (graph, part')
 
 let build_lts partition =
-  let (ps, ls) = 
+  let (ps, ls) =
     List.partition (fun x -> match GSet.choose x with
 		    | LState _ -> false
 		    | PState _ -> true)
@@ -163,15 +163,15 @@ let build_lts partition =
       | cp::t ->
 	  begin
 	    let p = List.hd cp in
-	    let labs = 
+	    let labs =
 	      List.fold_left
-		(fun acc x -> 
+		(fun acc x ->
 		   match List.filter (fun (src,_,_) -> src = p) x with
 		     | [] -> acc
 		     | t::_ -> t::acc
 		)
 		[] lstates
-	    in let transs' = 
+	    in let transs' =
 		List.fold_left
 		  (fun acc (_,lbl,dst) ->
 		     let cdl = List.filter
@@ -216,5 +216,3 @@ let is_fbisimilar f_deriv defs p1 p2 =
   let l = List.filter (fun x ->
     (GSet.mem pst1 x) || (GSet.mem pst2 x)) partition' in
   (List.length l) = 1
-
-
diff --git a/src/Parser.mly b/src/Parser.mly
index 94e1a5d..bc54593 100644
--- a/src/Parser.mly
+++ b/src/Parser.mly
@@ -10,12 +10,12 @@
     | [] -> p
     | n::ns' -> PRes(n,(mkRes ns' p))
 
-  let mkRename ns p = 
+  let mkRename ns p =
     let rec ren = function
     | [] -> p
     | (old,value) :: ns' -> PRename(old,value,(ren ns'))
     in
-    ren (List.rev ns)  
+    ren (List.rev ns)
 
 
 (*
@@ -71,9 +71,12 @@
 /* inturals */
 %token <int> INT
 
+/* quantifiers */
+%token FORALL EXISTS
+
 /* punctuation */
 %token LPAREN RPAREN LBRACKET RBRACKET COMMA EQUAL EQEQ TILD COLON
-%token IF THEN ELSE INF SUP INFEQ SUPEQ DIFF DOTDOT LACCOL RACCOL
+%token IF THEN ELSE INF SUP INFEQ SUPEQ DIFF DOTDOT LACCOL RACCOL WHEREAS
 
 /* operators */
 %token PAR PLUS DOT OUT IN MINUS DIV MULT MOD AND OR NOT IMPLIES
@@ -87,6 +90,7 @@
 %left MULT , DIV , MOD
 %right COMMA
 %left OUT IN
+%right WHEREAS
 
 %nonassoc UNARY
 
@@ -101,7 +105,7 @@
 %type <preprefix> prefix
 %type <preexpr> expr
 %type <modality> modality
-%type <formula> formula
+%type <preformula> formula
 
   /* grammar */
 %%
@@ -115,65 +119,65 @@
   | INT { (string_of_int $1) }
 
       statement:
-  | definition                     
+  | definition
       { let defs = definitions_of_predefinition $1
         in
-          List.iter Control.handle_definition defs 
+          List.iter Control.handle_definition defs
       }
-  | CONSTDEF CONST EQUAL INT 
+  | CONSTDEF CONST EQUAL INT
       { Control.handle_constdef $2 $4 }
   | TYPEDEF IDENT EQUAL LBRACKET minmax DOTDOT minmax RBRACKET
       { Control.handle_typedef_range $2 $5 $7 }
   | TYPEDEF IDENT EQUAL LACCOL list_of_names RACCOL
       { Control.handle_typedef_enum $2 $5 }
-  | NORM process                   
+  | NORM process
       { Control.handle_normalization (process_of_preprocess $2) }
-  | NORM error     
+  | NORM error
       { raise (Fatal_Parse_Error "missing process to normalize") }
   | STRUCT process EQEQ process
-      { Control.handle_struct_congr 
+      { Control.handle_struct_congr
         (process_of_preprocess $2)
         (process_of_preprocess $4) }
   | STRUCT process error
       { raise (Fatal_Parse_Error "missing '==' for structural congruence") }
   | STRUCT process EQEQ error
       { raise (Fatal_Parse_Error "missing process after '==' for structural congruence") }
-  | STRUCT error 
+  | STRUCT error
       {raise (Fatal_Parse_Error "missing process before '==' for structural congruence") }
-  | BISIM IN process TILD process 
-      { Control.handle_is_bisim 
-        (process_of_preprocess $3) 
+  | BISIM IN process TILD process
+      { Control.handle_is_bisim
+        (process_of_preprocess $3)
         (process_of_preprocess $5) }
   | BISIM IN process error
       { raise (Fatal_Parse_Error "missing '~' for strong bisimilarity") }
   | BISIM IN process TILD error
       { raise (Fatal_Parse_Error "missing process after '~' for strong bisimilarity") }
   | BISIM process TILD process
-      { Control.handle_bisim 
+      { Control.handle_bisim
         (process_of_preprocess $2)
         (process_of_preprocess $4) }
   | BISIM process error
       { raise (Fatal_Parse_Error "missing '~' for strong bisimilarity") }
   | BISIM process TILD error
       { raise (Fatal_Parse_Error "missing process after '~' for strong bisimilarity") }
-  | BISIM error 
+  | BISIM error
       { raise (Fatal_Parse_Error "missing '?' or process before '~' for strong bisimilarity") }
-  | FBISIM IN process TILD process 
-      { Control.handle_is_fbisim 
+  | FBISIM IN process TILD process
+      { Control.handle_is_fbisim
         (process_of_preprocess $3)
         (process_of_preprocess $5) }
   | FBISIM IN process error
       { raise (Fatal_Parse_Error "missing '~' for strong bisimilarity") }
   | FBISIM IN process TILD error
       { raise (Fatal_Parse_Error "missing process after '~' for strong bisimilarity") }
-  | FBISIM error 
+  | FBISIM error
       { raise (Fatal_Parse_Error "missing '?' or process before '~' for strong bisimilarity") }
 
 
 
-  | WBISIM IN process TILD TILD process 
-      { Control.handle_is_wbisim 
-        (process_of_preprocess $3) 
+  | WBISIM IN process TILD TILD process
+      { Control.handle_is_wbisim
+        (process_of_preprocess $3)
         (process_of_preprocess $6) }
   | WBISIM IN process error
       { raise (Fatal_Parse_Error "missing '~~' for weak bisimilarity") }
@@ -182,9 +186,9 @@
   | WBISIM IN process TILD TILD error
       { raise (Fatal_Parse_Error "missing process after '~~' for weak bisimilarity") }
 
-  | WBISIM process TILD TILD process 
-      { Control.handle_wbisim 
-        (process_of_preprocess $2) 
+  | WBISIM process TILD TILD process
+      { Control.handle_wbisim
+        (process_of_preprocess $2)
         (process_of_preprocess $5) }
   | WBISIM process error
       { raise (Fatal_Parse_Error "missing '~~' for weak bisimilarity") }
@@ -192,13 +196,13 @@
       { raise (Fatal_Parse_Error "missing '~' for weak bisimilarity") }
   | WBISIM process TILD TILD error
       { raise (Fatal_Parse_Error "missing process after '~~' for weak bisimilarity") }
-      
-  | WBISIM error 
+
+  | WBISIM error
       { raise (Fatal_Parse_Error "missing '?' or process before '~~' for weak bisimilarity") }
 
-  | WFBISIM IN process TILD TILD process 
-      { Control.handle_is_fwbisim 
-        (process_of_preprocess $3) 
+  | WFBISIM IN process TILD TILD process
+      { Control.handle_is_fwbisim
+        (process_of_preprocess $3)
         (process_of_preprocess $6) }
   | WFBISIM IN process error
       { raise (Fatal_Parse_Error "missing '~~' for weak bisimilarity") }
@@ -210,46 +214,49 @@
   | WDERIV process
       { Control.handle_wderiv (process_of_preprocess $2) }
   | WDERIV error
-      { raise (Fatal_Parse_Error "missing process to derivate") } 
+      { raise (Fatal_Parse_Error "missing process to derivate") }
 
   | TDERIV process
       { Control.handle_tderiv (process_of_preprocess $2) }
   | TDERIV error
-      { raise (Fatal_Parse_Error "missing process to derivate") } 
+      { raise (Fatal_Parse_Error "missing process to derivate") }
 
   | WLTS process
       { Control.handle_wlts (process_of_preprocess $2) }
   | WLTS error
-      { raise (Fatal_Parse_Error "missing process for LTS") } 
+      { raise (Fatal_Parse_Error "missing process for LTS") }
   | WMINI process
       { Control.handle_wminimization (process_of_preprocess $2) }
   | WMINI error
-      {raise (Fatal_Parse_Error "missing process for minimization") } 
-      
+      {raise (Fatal_Parse_Error "missing process for minimization") }
+
   | DERIV process
       { Control.handle_deriv (process_of_preprocess $2) }
   | DERIV error
-      { raise (Fatal_Parse_Error "missing process to derivate") } 
+      { raise (Fatal_Parse_Error "missing process to derivate") }
   | LTS process
       { Control.handle_lts (process_of_preprocess $2) }
   | LTS error
-      { raise (Fatal_Parse_Error "missing process for LTS") } 
+      { raise (Fatal_Parse_Error "missing process for LTS") }
   | MINI process
       { Control.handle_minimization (process_of_preprocess $2) }
   | MINI error
-      {raise (Fatal_Parse_Error "missing process for minimization") } 
+      {raise (Fatal_Parse_Error "missing process for minimization") }
   | FREE process
       { Control.handle_free (process_of_preprocess $2) }
   | FREE error
-      { raise (Fatal_Parse_Error "missing process for free names") } 
+      { raise (Fatal_Parse_Error "missing process for free names") }
   | BOUND process
       { Control.handle_bound (process_of_preprocess $2) }
   | BOUND error
-      { raise (Fatal_Parse_Error "missing process for bound names") } 
+      { raise (Fatal_Parse_Error "missing process for bound names") }
   | NAMES process
       { Control.handle_names (process_of_preprocess $2) }
   | NAMES error
-      { raise (Fatal_Parse_Error "missing process for names") } 
+      { raise (Fatal_Parse_Error "missing process for names") }
+
+  | PROP IDENT LPAREN RPAREN EQUAL formula
+      { Control.handle_prop $2 [] (formula_of_preformula $6) }
 
   | PROP IDENT LPAREN list_of_names RPAREN EQUAL formula
       { Control.handle_prop $2 $4 (formula_of_preformula $7) }
@@ -266,20 +273,20 @@
       { Control.handle_quit () }
 
       process:
-  | INT 
-      { if $1 = 0 then PSilent 
+  | INT
+      { if $1 = 0 then PSilent
         else raise (Fatal_Parse_Error "Only 0 can be used as Silent process") }
-  | END 
+  | END
       { PSilent }
   | prefix { PPrefix($1,PSilent) }
   | prefix COMMA process { PPrefix($1,$3) }
   | prefix COMMA error
       { raise (Fatal_Parse_Error "right-hand process missing after prefix") }
   | prefix error
-      { raise (Fatal_Parse_Error "missing ',' after prefix") }      
+      { raise (Fatal_Parse_Error "missing ',' after prefix") }
   | process PAR process {  PPar($1,$3) }
   | process PAR error
-      { raise (Fatal_Parse_Error "right-hand process missing in parallel") }      
+      { raise (Fatal_Parse_Error "right-hand process missing in parallel") }
   | process PLUS process { PSum($1,$3) }
   | process PLUS error
       { raise (Fatal_Parse_Error "right-hand process missing in sum") }
@@ -302,7 +309,7 @@
 
       list_of_prefixes:
   | prefix { [$1] }
-  | prefix COMMA list_of_prefixes { $1::$3 }  
+  | prefix COMMA list_of_prefixes { $1::$3 }
 
       rename :
   | LBRACKET list_of_renames RBRACKET { $2 }
@@ -357,39 +364,52 @@
   | /* empty */ { [] }
   | expr list_of_exprs { $1::$2 }
 
+      list_of_formulas:
+  | formula { [$1] }
+  | formula COMMA list_of_formulas { $1::$3 }
+
       formula:
-  | TRUE { FTrue }
-  | FALSE { FFalse }
-  | formula AND formula { FAnd ($1,$3) }
-  | formula OR formula { FOr ($1,$3) }
-  | formula IMPLIES formula { FImplies ($1,$3) }
-  | modality formula { FModal($1,$2) }
-  | TILD modality formula { FInvModal($2,$3) }
-  | MU LPAREN IDENT RPAREN DOT formula { FMu ($3,$6) }
-  | NU LPAREN IDENT RPAREN DOT formula { FNu ($3,$6) }
-  | IDENT LPAREN list_of_names RPAREN { FProp($1,$3) }
-  | IDENT { FVar($1) }
+  | TRUE { PFTrue }
+  | FALSE { PFFalse }
+  | LPAREN formula RPAREN { PFPar $2 }
+  | formula AND formula { PFAnd ($1,$3) }
+  | formula OR formula { PFOr ($1,$3) }
+  | formula IMPLIES formula { PFImplies ($1,$3) }
+  | modality LPAREN formula RPAREN { PFModal($1, $3) }
+  | modality formula { PFModal($1,$2) }
+  | TILD modality formula { PFInvModal($2,$3) }
+  | MU LPAREN IDENT RPAREN DOT formula { PFMu ($3,$6) }
+  | NU LPAREN IDENT RPAREN DOT formula { PFNu ($3,$6) }
+  | IDENT LPAREN RPAREN { PFProp($1, []) }
+  | IDENT LPAREN list_of_formulas RPAREN { PFProp($1,$3) }
+  | IDENT { PFVar($1) }
+  | FORALL param COMMA expr WHEREAS formula { PFForall($2, $4, $6) }
+  | EXISTS param COMMA expr WHEREAS formula { PFExists($2, $4, $6) }
 
       modality:
-  | INF list_of_prefixes SUP { FPossibly $2 }
-  | INF OUT SUP { FOutPossibly }
-  | INF IN SUP { FInPossibly }
-  | INF DOT SUP { FAnyPossibly }
-
-  | INF INF list_of_prefixes SUP SUP { FWPossibly $3 }
-  | INF INF OUT SUP SUP { FWOutPossibly }
-  | INF INF IN SUP SUP { FWInPossibly }
-  | INF INF DOT SUP SUP { FWAnyPossibly }
-
-  | LBRACKET list_of_prefixes RBRACKET { FNecessity $2 }
-  | LBRACKET OUT RBRACKET { FOutNecessity }
-  | LBRACKET IN RBRACKET { FInNecessity }
-  | LBRACKET DOT RBRACKET { FAnyNecessity }
-
-  | LBRACKET LBRACKET list_of_prefixes RBRACKET RBRACKET { FWNecessity $3 }
-  | LBRACKET LBRACKET OUT RBRACKET RBRACKET { FWOutNecessity }
-  | LBRACKET LBRACKET IN RBRACKET RBRACKET { FWInNecessity }
-  | LBRACKET LBRACKET DOT RBRACKET RBRACKET { FWAnyNecessity }
+  | INF list_of_prefixes SUP
+      { Strong, Possibly, Prefix (Formula.parse_preprefix_list $2) }
+  | INF OUT SUP { Strong, Possibly, Out }
+  | INF IN SUP { Strong, Possibly, In }
+  | INF DOT SUP { Strong, Possibly, Any }
+
+  | INF INF list_of_prefixes SUP SUP
+      { Weak, Possibly, Prefix (Formula.parse_preprefix_list $3) }
+  | INF INF OUT SUP SUP { Weak, Possibly, Out }
+  | INF INF IN SUP SUP { Weak, Possibly, In }
+  | INF INF DOT SUP SUP { Weak, Possibly, Any }
+
+  | LBRACKET list_of_prefixes RBRACKET
+      { Strong, Necessity, Prefix (Formula.parse_preprefix_list $2) }
+  | LBRACKET OUT RBRACKET { Strong, Necessity, Out }
+  | LBRACKET IN RBRACKET { Strong, Necessity, In }
+  | LBRACKET DOT RBRACKET { Strong, Necessity, Any }
+
+  | LBRACKET LBRACKET list_of_prefixes RBRACKET RBRACKET
+      { Weak, Necessity, Prefix (Formula.parse_preprefix_list $3) }
+  | LBRACKET LBRACKET OUT RBRACKET RBRACKET { Weak, Necessity, Out }
+  | LBRACKET LBRACKET IN RBRACKET RBRACKET { Weak, Necessity, In }
+  | LBRACKET LBRACKET DOT RBRACKET RBRACKET { Weak, Necessity, Any }
 
 
 %%
diff --git a/src/Pave.ml b/src/Pave.ml
index 8d0583e..741d307 100644
--- a/src/Pave.ml
+++ b/src/Pave.ml
@@ -4,7 +4,7 @@ open Utils
 
 let version_str = "Pave' v.1 r20130910"
 let usage = "Usage: pave <opt>"
-let banner = 
+let banner =
 "\n"^
 "===============\n"^
 "   .+------+                                         +------+.\n"^
@@ -44,40 +44,41 @@ let parse_error_msg lexbuf =
   in
     printf "Parser error at line %d char %d: ~%s~\n%!" l c tok ;;
 
-match !load_file with
+let _ =
+  match !load_file with
   | None ->
-      printf "Interactive mode... \n%!";
+    printf "Interactive mode... \n%!";
     Control.script_mode := false ;
     while true do
-	printf "> %!";
+      printf "> %!";
       let lexbuf = Lexing.from_channel stdin in
-	try
-	  ignore (Parser.script Lexer.token lexbuf)
-	with 
-	| Failure msg -> printf "Failure: %s\n%!" msg
-        | Fatal_Parse_Error(msg) ->
-          parse_error_msg lexbuf ;
-          printf " ==> %s\n%!" msg
-	| Parsing.Parse_error -> 
-          parse_error_msg lexbuf
+      try
+	ignore (Parser.script Lexer.token lexbuf)
+      with
+      | Failure msg -> printf "Failure: %s\n%!" msg
+      | Fatal_Parse_Error(msg) ->
+        parse_error_msg lexbuf ;
+        printf " ==> %s\n%!" msg
+      | Parsing.Parse_error ->
+        parse_error_msg lexbuf
     done
   | Some file ->
-      printf "Loading file %s... \n%!" file;
+    printf "Loading file %s... \n%!" file;
     Control.script_mode := true ;
-      let lexbuf = Lexing.from_channel (open_in file) in
-      let rec loop () =
-	let continue = 
-	  try
-	    Parser.script Lexer.token lexbuf
-	  with 
-	    | Failure msg -> printf "Failure: %s\n%!" msg ; true
-            | Fatal_Parse_Error(msg) ->
-              parse_error_msg lexbuf ;
-              printf " ==> %s\n%!" msg ; true
-	    | Parsing.Parse_error -> 
-              parse_error_msg lexbuf ; true
-	in
-	  if continue then loop ();
+    let lexbuf = Lexing.from_channel (open_in file) in
+    let rec loop () =
+      let continue =
+	try
+	  Parser.script Lexer.token lexbuf
+	with
+	| Failure msg -> printf "Failure: %s\n%!" msg ; true
+        | Fatal_Parse_Error(msg) ->
+          parse_error_msg lexbuf ;
+          printf " ==> %s\n%!" msg ; true
+	| Parsing.Parse_error ->
+          parse_error_msg lexbuf ; true
       in
-	loop ()
+      if continue then loop ();
+    in
+    loop ()
 ;;
diff --git a/src/Presyntax.ml b/src/Presyntax.ml
index f2c6fc3..6ec05d6 100644
--- a/src/Presyntax.ml
+++ b/src/Presyntax.ml
@@ -14,7 +14,7 @@ type preconstdef =
 
 let string_of_preconstdef = function
   | PConstDef (name,value) -> sprintf "const %%%s = %d" name value
-  
+
 type pretypedef =
 | PTDefRange of string * int * int
 | PTDefEnum of string * SSet.t
@@ -22,7 +22,7 @@ type pretypedef =
 
 
 
-let env_type = 
+let env_type =
   let bool_type = PTDefEnum( "Bool", (SSet.add "True" (SSet.add "False" SSet.empty)))
   in ref (SMap.add "Bool" bool_type SMap.empty) ;;
 
@@ -34,7 +34,7 @@ let add_to_env_type k v =
 let string_of_pretypedef = function
   | PTDefRange (name,min,max) -> sprintf "type %s = [%d..%d]" name min max
   | PTDefEnum (name,names) -> "type " ^ name ^ " = " ^ (string_of_set (fun x -> x) names)
-  
+
 type preexpr =
 | PTrue
 | PFalse
@@ -60,7 +60,7 @@ type preexpr =
 
 exception Type_Exception of string
 
-let bool_of_value = function 
+let bool_of_value = function
   | Bool b -> b
   | Name n -> raise (Type_Exception (sprintf "Name %s was received where Bool was expected !!!" n))
   | Int i -> raise (Type_Exception (sprintf "Int %d was received where Bool was expected !!!" i))
@@ -74,7 +74,7 @@ let int_of_value = function
   | Bool b -> raise (Type_Exception (sprintf "Bool %s was received where Int was expected !!!" (if b then "true" else "false")))
   | Name n -> raise (Type_Exception (sprintf "Name %s was received where Int was expected !!!" n))
   | Int i -> i
-    
+
 let rec interprete_preexpr : preexpr -> value = function
   | PTrue -> Bool true
   | PFalse -> Bool false
@@ -83,14 +83,14 @@ let rec interprete_preexpr : preexpr -> value = function
   | PConst name -> Int (SMap.find name !env_const)
   | PVar name -> (SMap.find name !env_var)
   | PNot pexpr -> let b = bool_of_value (interprete_preexpr pexpr) in Bool (not b)
-  | PAnd (preexpr1, preexpr2) -> 
+  | PAnd (preexpr1, preexpr2) ->
     let b1 = bool_of_value (interprete_preexpr preexpr1)
     and b2 = bool_of_value (interprete_preexpr preexpr2) in
-    Bool ( b1 && b2 ) 
+    Bool ( b1 && b2 )
   | POr (preexpr1, preexpr2) ->
     let b1 = bool_of_value (interprete_preexpr preexpr1)
     and b2 = bool_of_value (interprete_preexpr preexpr2) in
-    Bool ( b1 || b2 ) 
+    Bool ( b1 || b2 )
 
   | PAdd (preexpr1, preexpr2) ->
     let i1 = int_of_value (interprete_preexpr preexpr1 )
@@ -135,7 +135,7 @@ let rec interprete_preexpr : preexpr -> value = function
     | (Int i1, Int i2) -> Bool ( i1 = i2 )
     | (Name n1, Name n2) -> Bool ( n1 = n2 )
     | (_, _) -> Bool ( false ))
-      
+
   | PNeq (preexpr1, preexpr2) ->
     let p1 = interprete_preexpr preexpr1
     and p2 = interprete_preexpr preexpr2 in
@@ -149,12 +149,12 @@ let rec interprete_preexpr : preexpr -> value = function
     let i1 = int_of_value (interprete_preexpr preexpr1 )
     and i2 = int_of_value ( interprete_preexpr preexpr2 ) in
     Bool ( i1 <= i2 )
-      
+
   | PSupEq (preexpr1, preexpr2) ->
     let i1 = int_of_value (interprete_preexpr preexpr1 )
     and i2 = int_of_value ( interprete_preexpr preexpr2 ) in
     Bool ( i1 >= i2 )
-      
+
   | PIf (cond, preexpr1, preexpr2) ->
     let b = bool_of_value (interprete_preexpr cond) in
     if b then
@@ -181,7 +181,7 @@ let rec string_of_preexpr = function
   | PInf (e1,e2) -> sprintf "(%s) < (%s)" (string_of_preexpr e1) (string_of_preexpr e2)
   | PSup (e1,e2) -> sprintf "(%s) > (%s)" (string_of_preexpr e1) (string_of_preexpr e2)
   | PEq (e1,e2) -> sprintf "(%s) = (%s)" (string_of_preexpr e1) (string_of_preexpr e2)
-  | PNeq (e1,e2) -> sprintf "(%s) <> (%s)" (string_of_preexpr e1) (string_of_preexpr e2)  
+  | PNeq (e1,e2) -> sprintf "(%s) <> (%s)" (string_of_preexpr e1) (string_of_preexpr e2)
   | PInfEq (e1,e2) -> sprintf "(%s) <= (%s)" (string_of_preexpr e1) (string_of_preexpr e2)
   | PSupEq (e1,e2) -> sprintf "(%s) >= (%s)" (string_of_preexpr e1) (string_of_preexpr e2)
   | PIf (c,e1,e2) -> sprintf "if (%s) then (%s) else (%s)" (string_of_preexpr c) (string_of_preexpr e1) (string_of_preexpr e2)
@@ -236,17 +236,17 @@ let value_list : pretypedef -> (value list) = function
   | PTDefRange (_, min,max) ->(make_int_list min max)
   | PTDefEnum ("Bool" , _) -> [Bool true; Bool false]
   | PTDefEnum (_ , enum) -> (List.map (fun a -> Name a) (SSet.elements enum))
-    
+
 let rec process_of_receive : string -> string -> pretypedef -> preprocess -> process =
   fun canal nomVar theType pproc ->
     let val_list = value_list theType  in
     let rec process_of_receive_aux v_list=
       match v_list with
-      | [] -> failwith "Empty list" 
+      | [] -> failwith "Empty list"
       | hd::[] -> (env_var := (SMap.add nomVar hd !env_var);
 		   Prefix( In( sprintf "%s_%s" canal
 				 (string_of_value hd)), (process_of_preprocess pproc) ))
-      | hd::tl -> 
+      | hd::tl ->
 	env_var:=(SMap.add nomVar hd !env_var);
 	let pref = Prefix( In( sprintf "%s_%s" canal
 				 (string_of_value hd)), (process_of_preprocess pproc) ) in
@@ -257,37 +257,37 @@ let rec process_of_receive : string -> string -> pretypedef -> preprocess -> pro
 and process_of_prefix : preprefix -> preprocess -> process =
   fun pfix pproc ->
     match pfix with
-    | PTau -> Prefix(Tau, (process_of_preprocess pproc) ) 
+    | PTau -> Prefix(Tau, (process_of_preprocess pproc) )
     | PIn (pexpr) -> Prefix( In ( string_of_value (interprete_preexpr pexpr)),
-			     (process_of_preprocess pproc) ) 
+			     (process_of_preprocess pproc) )
     | POut(pexpr) -> Prefix( Out ( string_of_value (interprete_preexpr pexpr)),
-			     (process_of_preprocess pproc) ) 
-      
-    | PSend(pexprCanal, pexprVal) -> Prefix( Out ( sprintf "%s_%s" 
+			     (process_of_preprocess pproc) )
+
+    | PSend(pexprCanal, pexprVal) -> Prefix( Out ( sprintf "%s_%s"
 						     (string_of_value (interprete_preexpr pexprCanal))
 						     (string_of_value (interprete_preexpr pexprVal)) ),
 					     (process_of_preprocess pproc))
-    | PReceive(pexprCanal, nomVar, nomType) -> 
+    | PReceive(pexprCanal, nomVar, nomType) ->
       (if SMap.mem nomVar !env_var then
 	  raise (Vardef_Exception nomVar));
-      let canal = string_of_value (interprete_preexpr pexprCanal) 
+      let canal = string_of_value (interprete_preexpr pexprCanal)
       and theType = SMap.find nomType !env_type in
       let prc = process_of_receive canal nomVar theType pproc in
       (env_var := SMap.remove nomVar !env_var;
        prc)
-and process_of_preprocess : preprocess -> process = 
-  fun preproc -> 
+and process_of_preprocess : preprocess -> process =
+  fun preproc ->
     printf "Transforming process:\n%s\n%!" (string_of_preprocess preproc) ;
     match preproc with
     | PSilent -> Silent
     | PPrefix (pfix, pproc) -> process_of_prefix pfix pproc
-      
-    | PSum (pproc1, pproc2) -> 
-      Sum( (process_of_preprocess pproc1), 
+
+    | PSum (pproc1, pproc2) ->
+      Sum( (process_of_preprocess pproc1),
 	   (process_of_preprocess pproc2) )
 
-    | PPar (pproc1, pproc2) -> 
-      Par( (process_of_preprocess pproc1), 
+    | PPar (pproc1, pproc2) ->
+      Par( (process_of_preprocess pproc1),
 	   (process_of_preprocess pproc2) )
 
     | PRes (nvar, pproc) ->
@@ -298,13 +298,13 @@ and process_of_preprocess : preprocess -> process =
     | PRename( oldName, newName , pproc) ->
       Rename( oldName, newName, (process_of_preprocess pproc) )
 
-    | PGuard( pexpr, ppro) -> 
+    | PGuard( pexpr, ppro) ->
       let b = bool_of_value (interprete_preexpr pexpr) in
       if b then
 	process_of_preprocess ppro
       else
 	Silent
-      
+
 type preparam =
 | PParamVar of string * string
 | PParamBool of bool
@@ -319,7 +319,7 @@ let string_of_preparam = function
 
 type predefinition = PDefinition of string * preparam list * preprocess
 
-let string_of_predef_header (PDefinition (name,params,_)) = 
+let string_of_predef_header (PDefinition (name,params,_)) =
   name ^ (string_of_args string_of_preparam params)
 
 let string_of_predefinition = function
@@ -332,16 +332,16 @@ let definitions_of_predefinition : predefinition -> definition list =
     (* let rec def_of_predef_aux : string -> value list -> preparam list -> preprocess -> definition list= *)
     (*   function name computed_params preparams preproc -> *)
     let rec def_of_predef_aux  name computed_params preparams preproc =
-	match preparams with 
+	match preparams with
 	| [] -> [ Definition (name, computed_params, process_of_preprocess preproc) ]
 	| (PParamBool b)::tl  -> def_of_predef_aux name (computed_params@[Bool b]) tl preproc
 	| (PParamName n)::tl -> def_of_predef_aux name (computed_params@[Name n]) tl preproc
 	| (PParamInt i)::tl -> def_of_predef_aux name (computed_params@[Int i]) tl preproc
-	| (PParamVar (nomVar, theType))::tl -> 
+	| (PParamVar (nomVar, theType))::tl ->
 	  (if SMap.mem nomVar !env_var then
 	      raise (Vardef_Exception nomVar));
 	  let val_list = value_list (SMap.find theType !env_type) in
-	  let def_list = List.map (function v -> 
+	  let def_list = List.map (function v ->
 	    env_var := (SMap.add nomVar v !env_var);
 	    (def_of_predef_aux name (computed_params@[v]) tl preproc) )
 	    val_list
@@ -351,5 +351,3 @@ let definitions_of_predefinition : predefinition -> definition list =
     in
     printf "Transforming definition:\n%s\n%!" (string_of_predefinition predef) ;
     def_of_predef_aux name [] preparams preproc
-
-    
diff --git a/src/Semop.ml b/src/Semop.ml
index 046c268..3c64cd9 100644
--- a/src/Semop.ml
+++ b/src/Semop.ml
@@ -52,9 +52,9 @@ module BSet = Set.Make (
   end
 )
 
-let label_of_prefix =function 
+let label_of_prefix =function
   | Tau -> T_Tau | In n -> T_In n | Out n -> T_Out n
-  
+
 
 let derivatives defs ((orig_res, orig_np) as orig_nproc) =
   let restrict res derivs =
@@ -90,7 +90,7 @@ let derivatives defs ((orig_res, orig_np) as orig_nproc) =
 	restrict body_res derivs
     | NPrefix (pref, np) ->
       TSet.singleton (orig_nproc, label_of_prefix pref, renormalize(res,np))
-    | NRename (var,name,np) -> 
+    | NRename (var,name,np) ->
       let derivs = f res np
       in
         renames var name derivs
@@ -127,9 +127,9 @@ let derivatives defs ((orig_res, orig_np) as orig_nproc) =
 	      in
 	      let (_, new_in, new_in_res) =
 		SSet.fold folder_in in_forbid (0, dst, in_res)
-		 (*We rename all the names (at depth 1) 
+		 (*We rename all the names (at depth 1)
 		   of dst in folder_in by the new name
-		 *) 
+		 *)
 	      in
 	      let folder_oths name (cnt, acc_oths, acc_oths_res) =
 		let rec gen_name n =
@@ -264,8 +264,8 @@ let name_of_pfix = function
   | Tau -> ""
   | In n -> n
   | Out n -> n
-    
-let rename_pfix oldp n = 
+
+let rename_pfix oldp n =
   match oldp with
   | Tau -> Tau
   | In _ -> In n
@@ -292,14 +292,14 @@ and pmap_add_val map key v =
 let is_restricted rest pf =
   SSet.mem (name_of_pfix pf) rest
 
-let prefix_of_label = function 
+let prefix_of_label = function
   | T_Tau -> Tau | T_In n -> In n | T_Out n -> Out n
-	
+
 
 let weak_derivatives tau_only defs (orig_restrict, p) : PSet.t PrefixMap.t =
   let rec weak_deriv_aux pfix_key entry_map (restrict, p) =
     let get_set key =
-      try 
+      try
 	PrefixMap.find key entry_map
       with
 	Not_found -> PSet.empty
@@ -314,7 +314,7 @@ let weak_derivatives tau_only defs (orig_restrict, p) : PSet.t PrefixMap.t =
     | NSilent -> add_val pfix_key NSilent
     | NPrefix (pfix, p') ->
       (match pfix with
-      | Tau -> 
+      | Tau ->
 	if in_map pfix_key p' then
 	  entry_map
 	else
@@ -332,14 +332,14 @@ let weak_derivatives tau_only defs (orig_restrict, p) : PSet.t PrefixMap.t =
       )
     | NSum p_list ->
       List.fold_left (fun m p -> weak_deriv_aux pfix_key m (restrict, p)) entry_map p_list
-	
-    | NPar _ -> 
+
+    | NPar _ ->
       let a_suivre = ref [] in
       let rmap = ref entry_map in
       let follow = function (_, lbl, pr') ->
 	let a = prefix_of_label lbl in
 	match (pfix_key, a) with
-	| Tau, pfix | pfix, Tau -> 
+	| Tau, pfix | pfix, Tau ->
       	  if not (pmap_in_map !rmap pfix pr') then
 	    (a_suivre:= (pr', pfix) ::!a_suivre;
 	     rmap:= pmap_add_val !rmap pfix pr')
@@ -349,12 +349,12 @@ let weak_derivatives tau_only defs (orig_restrict, p) : PSet.t PrefixMap.t =
 	  (a_suivre:= (pr', Tau) ::!a_suivre;
 	   rmap:= pmap_add_val !rmap Tau pr')
       in
-      let pl = TSet.elements (derivatives defs (restrict, p)) in 
-      (* Nous avions commencé par écrire notre fonction dans l'optique de ne 
-	 pas utiliser derivatives. Cependant à la fin on s'est retrouvé face au problème 
+      let pl = TSet.elements (derivatives defs (restrict, p)) in
+      (* Nous avions commencé par écrire notre fonction dans l'optique de ne
+	 pas utiliser derivatives. Cependant à la fin on s'est retrouvé face au problème
 	 de l'extraction des restrictions dans le cas parallèle.
 	 Par manque de temps, nous avons du nous résoudre à utiliser derivatives.
-	 
+
 	 Vous pourrez trouvez nos essais dans Semop_abandon.ml
 	 Notament notre version de derivatives, réservée au cas parallele: par_derivatives
       *)
@@ -363,8 +363,8 @@ let weak_derivatives tau_only defs (orig_restrict, p) : PSet.t PrefixMap.t =
        else
 	  List.iter follow pl);
       List.fold_left (fun m (p,a) -> weak_deriv_aux a m p) !rmap !a_suivre
-	
-    | NCall (name, args) -> 
+
+    | NCall (name, args) ->
       let def_sign = string_of_def_header (Definition(name,args,Silent)) in
       let Definition (_, _, body) =
       	try Hashtbl.find defs def_sign
@@ -378,7 +378,7 @@ let weak_derivatives tau_only defs (orig_restrict, p) : PSet.t PrefixMap.t =
     | NRename (old, newn, p') ->
       (*ici on fait un appel réccursif avec une map vide et on trie à la sortie*)
       let m = weak_deriv_aux pfix_key PrefixMap.empty (restrict, p')
-      and merger _ s1 s2 = 
+      and merger _ s1 s2 =
 	match s1,s2 with
 	  None, Some s -> Some s
 	| Some s, None -> Some s
@@ -390,17 +390,17 @@ let weak_derivatives tau_only defs (orig_restrict, p) : PSet.t PrefixMap.t =
       and find_rename f m =
 	try
 	  let s = PrefixMap.find (f old) m in
-	  let s' = 
-	    try 
+	  let s' =
+	    try
 	      PrefixMap.find (f newn) m
 	    with
 	      Not_found -> PSet.empty
-	  in 
+	  in
 	  PrefixMap.add (f newn) (PSet.union s s') (PrefixMap.remove (f old) m)
-	with 
+	with
 	  Not_found -> m
       in
-      let m'= PrefixMap.map package_set (find_rename (fun x -> Out x) 
+      let m'= PrefixMap.map package_set (find_rename (fun x -> Out x)
 					   (find_rename (fun x -> In x) m)) in
       PrefixMap.merge merger m' entry_map
   in
@@ -408,16 +408,16 @@ let weak_derivatives tau_only defs (orig_restrict, p) : PSet.t PrefixMap.t =
   let derivs = PrefixMap.filter (fun k _ -> not (is_restricted orig_restrict k)) derivs in
   pmap_add_val derivs Tau (orig_restrict, p)
 
-  
+
 
 let printPfixMap map =
   let b = PrefixMap.bindings map in
-  let print_b (k, s) = 
+  let print_b (k, s) =
     let l = PSet.elements s in
     let arrow = Printf.sprintf "==%s==>" (string_of_prefix k) in
     List.iter (fun p -> print_string arrow; print_endline (string_of_nprocess p)) l
   in
-  List.iter print_b b  
+  List.iter print_b b
 
 
 let construct_weak_bisimilarity defs nproc1 nproc2 =
@@ -429,9 +429,9 @@ let construct_weak_bisimilarity defs nproc1 nproc2 =
 
     let d1s = derivatives defs np1 in
     let d2s = derivatives defs np2 in
-    
+
     let folder wds inv (_, lab, dstx) acc_bsm =
-      let dys = 
+      let dys =
 	try PrefixMap.find (prefix_of_label lab) wds
 	with Not_found -> failwith "Bad path"
       in
@@ -450,7 +450,7 @@ let construct_weak_bisimilarity defs nproc1 nproc2 =
       in
       search dys
     in
-    TSet.fold (folder wd2s false) d1s 
+    TSet.fold (folder wd2s false) d1s
       (TSet.fold (folder wd1s true) d2s bsm)
   in
   try construct (BSet.singleton (nproc1, nproc2)) nproc1 nproc2
@@ -467,7 +467,7 @@ let is_weakly_bisimilar defs nproc1 nproc2 =
 *)
 let pmap_to_trans map orig =
   let bds = PrefixMap.bindings map in
-  List.fold_left (fun acc (pfix, dst_set) -> 
+  List.fold_left (fun acc (pfix, dst_set) ->
     let lbl= label_of_prefix pfix in
     PSet.fold (fun dst acc' -> TSet.add (orig, lbl, dst) acc') dst_set acc) TSet.empty bds
 
diff --git a/src/Utils.ml b/src/Utils.ml
index fd5cd6b..6b14ee0 100644
--- a/src/Utils.ml
+++ b/src/Utils.ml
@@ -29,7 +29,7 @@ let string_of_args tostr lst = string_of_collection "(" ")" "," tostr lst
 let string_of_set tostr set =
   string_of_collection "{" "}" "," tostr (SSet.elements set)
 
-let string_of_map map = 
+let string_of_map map =
   string_of_collection "{" "}" "," (fun (old,value) -> sprintf "%s/%s" value old) (SMap.bindings map)
 
 
@@ -51,7 +51,7 @@ let forget _ = ()
 
 (* permutations:: 'a list -> 'a list list *)
 let rec permutations =
-  let rec inject_all e n l llen = 
+  let rec inject_all e n l llen =
     if n > llen then []
     else (inject e n l)::(inject_all e (n+1) l llen)
   and inject e n l =
diff --git a/src/examples/mucalculus.ccs b/src/examples/mucalculus.ccs
new file mode 100644
index 0000000..c66bf60
--- /dev/null
+++ b/src/examples/mucalculus.ccs
@@ -0,0 +1,85 @@
+
+# Some definitions, as proof of concept
+# prop p1() = true;
+# prop p2(A) = A;
+# prop p3() = <a!>true;
+
+# Check if, after every action, there is no out
+prop noIn() = Nu(X). ([?]false) and [.]X;
+
+def proc1 = a!, b!, proc1;
+
+# Returns OK
+checklocal noIn() |- proc1;
+
+# After the first action, there is a out
+def proc2 = a!, b?, proc2;
+
+# Returns false
+checklocal noIn() |- proc2;
+
+
+# Exercise 1 of TD5
+prop A() = <tau>((<a!>true) or (<b?>true));
+prop B() = [tau]((<a!>true) or (<b?>true));
+prop C() = ([a!]false) and ([b?] false);
+
+def pA = tau, a!, 0 + tau, c!, 0 + a!, 0;
+
+# Should returns OK
+checklocal A() |- pA;
+
+# Should returns False
+checklocal B() |- pA;
+
+# Should returns False
+checklocal C() |- pA;
+
+# Exercice 5 of TD5
+prop possibly(A) = Mu(X).A or <.> X;
+prop always(A) = Nu(X). A and [.] X;
+prop eventually(A) = Mu(X). A or ((<.>true) and [.] X);
+
+prop deadlock() = [.] false;
+prop cont() = <.> true;
+
+# Will never end
+def Loop = a!, Loop;
+
+# Returns false
+checklocal possibly(deadlock()) |- Loop;
+
+# OK
+checklocal always(cont()) |- Loop;
+
+# Should returns False
+checklocal always(deadlock()) |- Loop;
+
+# OK, since it's a loop
+checklocal eventually(cont()) |- Loop;
+
+# Should return False
+checklocal eventually(deadlock()) |- Loop;
+
+# This example was given in the Exercise 5
+prop correct() = ([start!]true) => eventually((<stop!>true) or ([.]false));
+def s = start!, p;
+def p = a!, b!, p2;
+def p2 = c?, p + stop!, 0;
+checklocal correct() |- s;
+
+#####
+# Some more examples
+
+# The process first matches A, and after some time B
+prop until(A,B) = Nu(X).(B or (A and [.]X));
+
+#####
+# Some examples of the mucalulus by value
+
+type Range = [0..3];
+# The process that does in_0?, in_1? and in_2?
+prop fa() = forall $in:Range, $in < 3 | (<<$in?>>true);
+
+# The processes that does at least out_0!, out_1! or out_2!
+prop fa() = exists $out:Range, $out < 3 | (<<$out!>>true);