Implement automata and activate blocks in interpret.

4 files changed, 232 insertions, 126 deletions

diff --git a/interpret/interpret2.ml b/interpret/interpret2.ml
index 33439e6..d6f7731 100644
--- a/interpret/interpret2.ml
+++ b/interpret/interpret2.ml
@@ -16,7 +16,7 @@ module I : INTERPRET = struct
     | VState of id
     | VPrevious of value list
     | VBusy   (* intermediate value : calculating ! *)
-    | VCalc of (unit -> value)
+    | VCalc of (unit -> unit)
 
   let int_value i = VInt i
   let bool_value b = VBool b
@@ -78,12 +78,13 @@ module I : INTERPRET = struct
 
     Gets the value of a variable relative to a node path.
   *)
-  let get_var env node id =
+  let rec get_var env node id =
     let p = node^"/"^id in
     try match Hashtbl.find env.vars p with
       | VCalc f ->
         Hashtbl.replace env.vars p VBusy;
-        f ()
+        f ();
+        get_var env node id
       | VBusy -> combinatorial_cycle p
       | x -> x
     with
@@ -182,6 +183,8 @@ module I : INTERPRET = struct
 
     Sets all the init variables to true, and all the state variables
     to initial state. Does this recursively.
+    The state reset done by this on the environment is only applied on the
+    next iteration, when the state info has been extracted by extract_st.
   *)
   let rec reset_scope env (node, prefix, eqs) =
     Hashtbl.replace env.vars (node^"/"^prefix^"init") (VBool true);
@@ -226,7 +229,7 @@ module I : INTERPRET = struct
             let apath = node^"/"^id^"/"^name in
             let calc () =
               match eval_expr env (node, prefix) expr with
-              | [v] -> Hashtbl.replace env.vars apath v; v
+              | [v] -> Hashtbl.replace env.vars apath v
               | _ -> loc_error (snd expr) error "Unsupported arity for argument."
             in
             Hashtbl.replace env.vars apath (VCalc calc)
@@ -237,18 +240,43 @@ module I : INTERPRET = struct
     let do_eq (e, _) = match e with
       | AST_assign(vars, e) ->
         do_expr e;
-        let calc i () =
+        let calc () =
           let vals = eval_expr env (node, prefix) e in
           List.iter2 (fun (id, _) v ->
-            Hashtbl.replace env.vars (node^"/"^id) v) vars vals;
-          List.nth vals i
+            Hashtbl.replace env.vars (node^"/"^id) v) vars vals
         in
-        List.iteri
-          (fun i (id, _) ->
-              Hashtbl.replace env.vars (node^"/"^id) (VCalc (calc i)))
+        List.iter
+          (fun (id, _) ->
+              Hashtbl.replace env.vars (node^"/"^id) (VCalc (calc)))
           vars
       | AST_assume(_,e) | AST_guarantee(_,e) -> do_expr e
-      | _ -> not_implemented "activate_scope"
+      | AST_activate(t, vars) ->
+        let rec do_tree = function
+          | AST_activate_body _ -> ()
+          | AST_activate_if(c, a, b) ->
+            do_expr c; do_tree a; do_tree b
+        in do_tree t;
+        let rec needed x () = match x with
+          | AST_activate_body b ->
+            activate_scope env (node, b.act_id^".", b.body)
+          | AST_activate_if (c, t, f) ->
+            begin match eval_expr env (node, prefix) c with
+            | [VBool true] -> needed t ()
+            | [VBool false] -> needed f ()
+            | _ -> error "Invalid value in activate if condition."
+            end
+        in
+        List.iter (fun id ->
+            Hashtbl.replace env.vars (node^"/"^id) (VCalc (needed t)))
+          vars
+      | AST_automaton(aid, states, vars) ->
+        let asn = match VarMap.find (node^"/"^aid^".state") env.st.save with
+          | VState s -> s
+          | _ -> assert false
+        in
+        let (st, _) = List.find (fun (st, _) -> st.st_name = asn) states in
+        activate_scope env (node, aid^"."^st.st_name^".", st.body);
+        List.iter (fun (c, _, _) -> do_expr c) st.until
     in
     List.iter do_eq eqs
 
@@ -262,8 +290,50 @@ module I : INTERPRET = struct
   (*
     do_weak_transitions : env -> scope -> unit
   *)
-  let do_weak_transitions env (node, prefix, eqs) =
-    not_implemented "do_weak_transitions"
+  let rec do_weak_transitions env (node, prefix, eqs) =
+    let do_expr e =
+      List.iter
+        (fun (id, eqs, args) ->
+          do_weak_transitions env (node^"/"^id, "", eqs))
+        (extract_instances env.st.p e)
+    in
+    let do_eq (e, _) = match e with
+      | AST_assign(_, e) -> do_expr e
+      | AST_assume (_, e) | AST_guarantee (_, e) -> do_expr e
+      | AST_activate(t, _) ->
+        let rec do_tree = function
+          | AST_activate_body b -> do_weak_transitions env (node, b.act_id^".", b.body)
+          | AST_activate_if(c, a, b) ->
+            do_expr c; do_tree a; do_tree b
+        in do_tree t
+      | AST_automaton(aid, states, vars) ->
+        let svn = node^"/"^aid^".state" in
+        let stv = VarMap.find svn env.st.save in
+        let new_st =
+          if is_scope_active env (node, prefix, eqs) then begin
+            let asn = match stv with
+              | VState s -> s
+              | _ -> assert false
+            in
+            let (st, _) = List.find (fun (st, _) -> st.st_name = asn) states in
+            try
+              let (_, (next_st,_), rst) = List.find
+                (fun (c, _, _) -> eval_expr env (node, aid^"."^st.st_name^".") c = [VBool true])
+                st.until
+              in
+                if rst then begin
+                  let (st, _) = List.find (fun (st, _) -> st.st_name = next_st) states in
+                  reset_scope env (node, aid^"."^next_st^".", st.body)
+                end;
+                VState(next_st)
+            with
+              | _ -> stv
+          end else
+            stv
+        in
+            Hashtbl.replace env.vars svn new_st
+    in
+    List.iter do_eq eqs
 
   (*
     extract_st : env -> state
@@ -282,10 +352,18 @@ module I : INTERPRET = struct
       let save_expr save e =
         let save = List.fold_left
           (fun save (id, expr) ->
-            VarMap.add
-              (node^"/"^prefix^id)
-              (VPrevious (eval_expr env (node, prefix) expr))
-              save)
+            let n = node^"/"^prefix^id in
+            if is_scope_active env (node, prefix, eqs) then
+              VarMap.add
+                n
+                (VPrevious (eval_expr env (node, prefix) expr))
+                save
+            else
+              try VarMap.add n
+                (VarMap.find n env.st.save)
+                save
+              with Not_found -> save
+          )
           save (extract_pre e) in
         let save = List.fold_left
           (fun save (n, eqs, _) ->
@@ -296,8 +374,25 @@ module I : INTERPRET = struct
       let save_eq save eq = match fst eq with
         | AST_assign(_, e) | AST_assume(_, e) | AST_guarantee(_, e) ->
             save_expr save e
-        | AST_automaton(aid, states, _) -> not_implemented "save_eq automaton"
-        | AST_activate(r, _) -> not_implemented "save_eq activate"
+        | AST_automaton(aid, states, _) ->
+          let svn = node^"/"^aid^".state" in
+          let st = Hashtbl.find env.vars svn in
+          let save = VarMap.add (node^"/"^aid^".state") st save in
+          List.fold_left (fun save (st, _) ->
+              let save = 
+                List.fold_left (fun save (c, _, _) -> save_expr save c) save st.until in
+              aux (node, aid^"."^st.st_name^".", st.body) save)
+            save states
+        | AST_activate(r, _) ->
+          let rec do_t save = function
+            | AST_activate_if(c, t, f) ->
+              let save = save_expr save c in
+              let save = do_t save t in
+              do_t save f
+            | AST_activate_body b ->
+              aux (node, b.act_id^".", b.body) save
+          in
+          do_t save r
       in
       List.fold_left save_eq save eqs
 
@@ -327,7 +422,7 @@ module I : INTERPRET = struct
           let cpath = "cst/" ^ d.c_name in
           Hashtbl.replace env.vars cpath (VCalc (fun () ->
             match eval_expr env ("cst", "") d.value with
-            | [v] -> Hashtbl.replace env.vars cpath v; v
+            | [v] -> Hashtbl.replace env.vars cpath v
             | _ -> loc_error l error "Arity error in constant expression."))
         | _ -> ())
       p;
@@ -348,11 +443,10 @@ module I : INTERPRET = struct
     let env = { st = st; vars = vars } in
     
     activate_scope env st.root_scope; 
-    (*
+    if false then
       Hashtbl.iter (fun k v -> Format.printf "%s : %s@." k (str_repr_of_val v)) env.vars;
-    *)
     let out = List.map (fun id -> id, get_var env "" id) st.outputs in
-    (* do_weak_transitions env st.root_scope; *)
+    do_weak_transitions env st.root_scope;
     extract_st env, out
 
 
diff --git a/tests/result/train.out b/tests/result/train.out
index 4af78b5..061ff7a 100644
--- a/tests/result/train.out
+++ b/tests/result/train.out
@@ -1,101 +1,101 @@
-0. 0 0 0
+0. -1 0 0
 1. 0 0 0
 2. 0 0 0
 3. 0 0 0
 4. 0 0 0
-5. 0 0 0
+5. 1 0 0
 6. 0 0 0
-7. 0 0 0
-8. 0 0 0
-9. 0 0 0
-10. 0 0 0
-11. 0 0 0
-12. 0 0 0
-13. 0 0 0
-14. 0 0 0
-15. 0 0 0
-16. 0 0 0
-17. 0 0 0
-18. 0 0 0
-19. 0 0 0
-20. 0 0 0
-21. 0 0 0
-22. 0 0 0
-23. 0 0 0
-24. 0 0 0
-25. 0 0 0
-26. 0 0 0
-27. 0 0 0
-28. 0 0 0
-29. 0 0 0
-30. 0 0 0
-31. 0 0 0
-32. 0 0 0
-33. 0 0 0
-34. 0 0 0
-35. 0 0 0
-36. 0 0 0
-37. 0 0 0
-38. 0 0 0
-39. 0 0 0
-40. 0 0 0
-41. 0 0 0
-42. 0 0 0
-43. 0 0 0
-44. 0 0 0
-45. 0 0 0
-46. 0 0 0
-47. 0 0 0
-48. 0 0 0
-49. 0 0 0
-50. 0 0 0
-51. 0 0 0
-52. 0 0 0
-53. 0 0 0
-54. 0 0 0
-55. 0 0 0
-56. 0 0 0
-57. 0 0 0
-58. 0 0 0
-59. 0 0 0
-60. 1 0 0
-61. 1 0 0
-62. 1 0 0
-63. 1 0 0
-64. 1 0 0
-65. 1 0 0
-66. 1 0 0
-67. 1 0 0
-68. 1 0 0
-69. 1 0 0
-70. 1 0 0
-71. 1 0 0
-72. 1 0 0
-73. 1 0 0
-74. 1 0 0
-75. 1 0 0
-76. 1 0 0
-77. 1 0 0
-78. 1 0 0
-79. 1 0 0
-80. 1 0 0
-81. 1 0 0
-82. 1 0 0
-83. 1 0 0
-84. 1 0 0
-85. 1 0 0
-86. 1 0 0
-87. 1 0 0
-88. 1 0 0
-89. 1 0 0
-90. 1 0 0
-91. 1 0 0
-92. 1 0 0
-93. 1 0 0
-94. 1 0 0
-95. 1 0 0
-96. 1 0 0
-97. 1 0 0
-98. 1 0 0
-99. 1 0 0
-100. 1 0 0
+7. 1 0 0
+8. 1 0 0
+9. 1 0 0
+10. 1 0 0
+11. 2 0 0
+12. 1 0 0
+13. 2 0 0
+14. 2 0 0
+15. 2 0 0
+16. 2 0 0
+17. 3 0 0
+18. 2 0 0
+19. 3 0 0
+20. 3 0 0
+21. 3 0 0
+22. 3 0 0
+23. 4 0 0
+24. 3 0 0
+25. 4 0 0
+26. 4 0 0
+27. 4 0 0
+28. 4 0 0
+29. 5 0 0
+30. 4 0 0
+31. 5 0 0
+32. 5 0 0
+33. 5 0 0
+34. 5 0 0
+35. 6 0 0
+36. 5 0 0
+37. 6 0 0
+38. 6 0 0
+39. 6 0 0
+40. 6 0 0
+41. 7 0 0
+42. 6 0 0
+43. 7 0 0
+44. 7 0 0
+45. 7 0 0
+46. 7 0 0
+47. 8 0 0
+48. 7 0 0
+49. 8 0 0
+50. 8 0 0
+51. 8 0 0
+52. 8 0 0
+53. 9 0 0
+54. 8 0 0
+55. 9 0 0
+56. 9 0 0
+57. 9 0 0
+58. 9 0 0
+59. 10 0 0
+60. 9 1 0
+61. 10 1 0
+62. 10 1 0
+63. 10 1 0
+64. 10 1 0
+65. 11 1 0
+66. 10 1 0
+67. 11 1 0
+68. 11 1 0
+69. 11 1 0
+70. 11 1 0
+71. 12 1 0
+72. 11 1 0
+73. 12 1 0
+74. 12 1 0
+75. 12 1 0
+76. 12 1 0
+77. 13 1 0
+78. 12 1 0
+79. 13 1 0
+80. 13 1 0
+81. 13 1 0
+82. 13 1 0
+83. 14 1 0
+84. 13 1 0
+85. 14 1 0
+86. 14 1 0
+87. 14 1 0
+88. 14 1 0
+89. 15 1 0
+90. 14 1 0
+91. 15 1 0
+92. 15 1 0
+93. 15 1 0
+94. 15 1 0
+95. 16 1 0
+96. 15 1 0
+97. 16 1 0
+98. 16 1 0
+99. 16 1 0
+100. 16 1 0
diff --git a/tests/source/train.scade b/tests/source/train.scade
index c51971e..0b93b2f 100644
--- a/tests/source/train.scade
+++ b/tests/source/train.scade
@@ -9,8 +9,7 @@ let
         else 0);
 tel
 
-node train(beacon, second: bool) returns (early, late: bool)
-var probe advance: int;
+node train(beacon, second: bool) returns (early, late: bool; probe advance: int)
 let
     advance = diff(beacon, second);
 
@@ -50,9 +49,9 @@ let
     returns alarm;
 tel
 
-node train_check(beacon, second: bool) returns (early, late, alarm: bool)
+node train_check(beacon, second: bool) returns (early, late, alarm: bool; adv: int)
 let
-    early, late = train(beacon, second);
+    early, late, adv = train(beacon, second);
     alarm = observer(early, late);
     guarantee ok : not alarm;
 tel
@@ -61,9 +60,8 @@ node test(i: int) returns(a, b, c: int; exit: bool)
 var early, late, alarm: bool;
 let
     exit = i >= 100;
-    early, late, alarm = train_check((i+1) mod 2 = 0, i mod 3 = 0);
+    early, late, alarm, a = train_check((i+1) mod 2 = 0, i mod 3 = 0);
     c = if alarm then 1 else 0;
-    a = if early then 1 else 0;
-    b = if late then 1 else 0;
+    b = if early then 1 else if late then 2 else 0;
 tel
 
diff --git a/tests/testanalyze.sh b/tests/testanalyze.sh
new file mode 100755
index 0000000..8b1add2
--- /dev/null
+++ b/tests/testanalyze.sh
@@ -0,0 +1,14 @@
+#!/bin/sh
+
+for a in source/*.scade; do
+  if ../analyze --test $a > /tmp/analyze_out.txt;
+  then
+    if diff -B /tmp/analyze_out.txt result/`basename $a .scade`.out >/dev/null; then
+      echo "OK    $a"
+    else
+      echo "FAIL  $a"
+    fi
+  else
+    echo "TODO  $a"
+  fi
+done