Everything proved !!

4 files changed, 104 insertions, 42 deletions

diff --git a/abstract/abs_interp.ml b/abstract/abs_interp.ml
index e55f199..383a69c 100644
--- a/abstract/abs_interp.ml
+++ b/abstract/abs_interp.ml
@@ -29,29 +29,30 @@ end = struct
 
     (* init state *)
     let init_state widen_delay rp =
-      let f = Formula.eliminate_not (Transform.f_of_prog rp false) in
-      let f_g = Formula.eliminate_not (Transform.f_of_prog rp true) in
-
       let env = List.fold_left
         (fun env (_, id, ty) -> E.addvar env id ty)
         E.init
         rp.all_vars
       in
-      let init_f = Transform.init_f_of_prog rp in
-      let guarantees = Transform.guarantees_of_prog rp in
+      Format.printf "Vars: @[<hov>%a@]@.@."
+          (Ast_printer.print_list Ast_printer.print_typed_var ", ")
+          rp.all_vars;
 
+      let init_f = Transform.init_f_of_prog rp in
       Format.printf "Init formula: %a@.@." Formula_printer.print_expr init_f;
-      Format.printf "Cycle formula:@.%a@.@." Formula_printer.print_expr f;
-      Format.printf "Cycle formula with guarantees:@.%a@.@." Formula_printer.print_expr f_g;
-
-      Format.printf "Vars: @[<hov>%a@]@.@." (Ast_printer.print_list Ast_printer.print_typed_var ", ") rp.all_vars;
 
+      let guarantees = Transform.guarantees_of_prog rp in
       Format.printf "Guarantees:@.";
       List.iter (fun (id, f) ->
           Format.printf "  %s: %a@." id Formula_printer.print_expr f)
         guarantees;
       Format.printf "@.";
 
+      let f = Formula.eliminate_not (Transform.f_of_prog rp false) in
+      let f_g = Formula.eliminate_not (Transform.f_of_prog rp true) in
+      Format.printf "Cycle formula:@.%a@.@." Formula_printer.print_expr f;
+      Format.printf "Cycle formula with guarantees:@.%a@.@." Formula_printer.print_expr f_g;
+
       let env = E.set_disjunct env "/exit" DNever in
       let env = E.apply_f env init_f in
 
diff --git a/abstract/formula.ml b/abstract/formula.ml
index ce83935..62acb28 100644
--- a/abstract/formula.ml
+++ b/abstract/formula.ml
@@ -54,6 +54,8 @@ let f_and a b = match a, b with
   | a, BConst true -> a
   | a, b -> BAnd(a, b)
 
+let f_and_list = List.fold_left f_and (BConst true)
+
 let f_or a b = match a, b with
   | BConst true, _ | _, BConst true -> BConst true
   | BConst false, b -> b
diff --git a/abstract/transform.ml b/abstract/transform.ml
index 64fd8d8..6fa1277 100644
--- a/abstract/transform.ml
+++ b/abstract/transform.ml
@@ -166,24 +166,22 @@ and f_of_expr td (node, prefix) expr =
     Translate program into one big formula
 *)
 let rec f_of_scope active td (node, prefix, eqs) assume_guarantees =
-  let expr_eq e eq =
+  let expr_eq e =
     let instance_eq (_, id, eqs, args) =
       let eq = f_of_scope active td (node^"/"^id, "", eqs) assume_guarantees in
       if active then
-        List.fold_left (fun eq ((_,argname,_), expr) ->
-            let eq_arg = f_of_neexpr td (node, prefix) (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")
-                expr
-            in f_and eq eq_arg)
-        eq args
+        let arg_eq ((_,argname,_), expr) =
+            f_of_neexpr td (node, prefix) (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")
+              expr
+        in f_and eq (f_and_list (List.map arg_eq args))
       else
         eq
     in
-    let eq = List.fold_left (fun x i -> f_and (instance_eq i) x)
-      eq (extract_instances td.rp.p e)
-    in
+    let eq_i = f_and_list (List.map instance_eq (extract_instances td.rp.p e)) in
+
     let pre_expr (id, expr) =
       if active then
         f_of_neexpr td (node, prefix) (fun elist ->
@@ -205,27 +203,28 @@ let rec f_of_scope active td (node, prefix, eqs) assume_guarantees =
               | TEnum _ -> f_e_eq (EIdent("N"^id^"."^x)) (EIdent (id^"."^x)))
             typ)
     in
-    List.fold_left (fun x i -> f_and (pre_expr i) x)
-      eq (extract_pre e)
+    let eq_p = f_and_list (List.map pre_expr (extract_pre e)) in
+
+    f_and eq_i eq_p
   in
   let do_eq eq = match fst eq with
     | AST_assign(ids, e) ->
       let assign_eq = 
         if active then
-            f_of_neexpr td (node, prefix)
-              (fun vs ->
-                let rels = 
-                  List.map2 (fun (id, _) -> function
-                    | NE v -> BRel(AST_EQ, NIdent (node^"/"^id), v)
-                    | EE v -> f_e_eq (EIdent (node^"/"^id)) v)
-                  ids vs
-                in
-                  list_fold_op f_and rels)
-              e
+            let apply_f vs =
+              let rels = 
+                List.map2 (fun (id, _) -> function
+                  | NE v -> BRel(AST_EQ, NIdent (node^"/"^id), v)
+                  | EE v -> f_e_eq (EIdent (node^"/"^id)) v)
+                ids vs
+              in
+                f_and_list rels
+            in
+            f_of_neexpr td (node, prefix) apply_f e
         else
           BConst true
       in
-        expr_eq e assign_eq
+        f_and (expr_eq e) assign_eq
     | AST_assume (_, e) ->
       let assume_eq = 
         if active then
@@ -233,7 +232,7 @@ let rec f_of_scope active td (node, prefix, eqs) assume_guarantees =
         else
           BConst true
       in
-        expr_eq e assume_eq
+        f_and (expr_eq e) assume_eq
     | AST_guarantee (_, e) ->
       let guarantee_eq =
         if active && assume_guarantees then
@@ -241,12 +240,12 @@ let rec f_of_scope active td (node, prefix, eqs) assume_guarantees =
         else
           BConst true
       in
-        expr_eq e guarantee_eq
+        f_and (expr_eq e) guarantee_eq
     | AST_activate (b, _) ->
       let rec cond_eq = function
         | AST_activate_body b -> BConst true
         | AST_activate_if(c, a, b) ->
-          f_and (expr_eq c (BConst true))
+          f_and (expr_eq c)
             (f_and (cond_eq a) (cond_eq b))
       in
       let rec do_tree_act = function
@@ -265,7 +264,38 @@ let rec f_of_scope active td (node, prefix, eqs) assume_guarantees =
           f_and (do_tree_inact a) (do_tree_inact b)
       in
         f_and (cond_eq b) (if active then do_tree_act b else do_tree_inact b)
-    | AST_automaton _ -> not_implemented "f_of_scope do_eq automaton"
+    | AST_automaton (aid, states, _) ->
+      let stv = EIdent (node^"/"^aid^".state") in
+      let nstv = EIdent ("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))
+      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 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)
+                        (BEnumCons(E_EQ, nstv, EItem target)))
+                  (f_and (BNot (f_of_expr td (node, prefix) c)) (aux q))
+            in f_and st_eq (aux st.until) 
+          in
+          f_or
+            (f_and (BEnumCons(E_EQ, stv, EItem st.st_name)) act_eq)
+            (f_and (BEnumCons(E_NE, stv, EItem st.st_name))
+              (st_eq_inact (st, l)))
+        in
+        f_and_list (List.map st_eq_act states)
+      else
+        f_and_list (List.map st_eq_inact states)
   in
   let time_incr_eq =
     if active then
@@ -332,7 +362,16 @@ let rec init_f_of_scope rp (node, prefix, eqs) =
             (f_and (cond_eq a) (cond_eq b))
       in
       cond_eq b
-    | AST_automaton _ -> not_implemented "f_of_scope do_eq automaton"
+    | AST_automaton (aid, states, _) ->
+      let (st, _) = List.find (fun (st, _) -> st.initial) states in
+      let init_eq = BEnumCons(E_EQ, EIdent(node^"/"^aid^".state"), EItem st.st_name) in
+      let state_eq (st, _) =
+        let sc_f =
+          init_f_of_scope rp (node, aid^"."^st.st_name^".", st.body)
+        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
@@ -379,9 +418,14 @@ let rec g_of_scope td (node, prefix, eqs) cond =
           (expr_g c)
       in
       cond_g cond b
-    | AST_automaton _ -> not_implemented "g_of_scope automaton"
+    | AST_automaton (aid, states, _) ->
+      let st_g (st, _) =
+        g_of_scope td (node, aid^"."^st.st_name^".", st.body)
+          (f_and cond (BEnumCons(E_EQ, EIdent(node^"/"^aid^".state"), EItem st.st_name)))
+      in
+      List.flatten (List.map st_g states)
   in
-  List.fold_left (@) [] (List.map do_eq eqs)
+  List.flatten (List.map do_eq eqs)
 
 and guarantees_of_prog rp =
     let td = {
diff --git a/frontend/typing.ml b/frontend/typing.ml
index a4abfe0..564d91e 100644
--- a/frontend/typing.ml
+++ b/frontend/typing.ml
@@ -158,7 +158,22 @@ let rec extract_all_vars rp (node, prefix, eqs) n_vars =
           | AST_activate_if(c, a, b) ->
             vars_of_expr c @ do_branch a @ do_branch b
         in do_branch b
-      | AST_automaton _ -> not_implemented "extract_all vars automaton"
+      | AST_automaton (aid, states, ret) ->
+        let do_state (st, _) =
+          let tvars =
+            List.flatten
+              (List.map (fun (e, _, _) -> vars_of_expr e) st.until)
+          in
+          let svars = vars_in_node node st.st_locals in
+          svars @ tvars @
+            extract_all_vars rp
+              (node, aid^"."^st.st_name^".", st.body)
+              (tvars@n_vars)
+        in
+        let st_ids = List.map (fun (st, _) -> st.st_name) states in
+        (false, node^"/"^aid^".state", TEnum st_ids)::
+        (false, "N"^node^"/"^aid^".state", TEnum st_ids)::
+        (List.flatten (List.map do_state states))
     in
     let v = List.flatten (List.map vars_of_eq eqs) in
     let v =