summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--abstract/abs_interp.ml194
-rw-r--r--abstract/abs_interp_edd.ml90
-rw-r--r--abstract/formula.ml27
-rw-r--r--abstract/transform.ml304
-rw-r--r--cmdline.ml8
-rw-r--r--frontend/ast.ml4
-rw-r--r--frontend/lexer.mll6
-rw-r--r--frontend/parser.mly1
-rw-r--r--frontend/typing.ml38
-rw-r--r--libs/util.ml2
-rw-r--r--main.ml18
-rw-r--r--tests/source/NestedControl.scade8
-rwxr-xr-xtests/source/counters.scade11
-rw-r--r--tests/source/test5.scade4
14 files changed, 405 insertions, 310 deletions
diff --git a/abstract/abs_interp.ml b/abstract/abs_interp.ml
index f6ce0ab..cb5ae9c 100644
--- a/abstract/abs_interp.ml
+++ b/abstract/abs_interp.ml
@@ -2,17 +2,12 @@ open Ast
open Ast_util
open Formula
open Typing
+open Cmdline
open Util
open Num_domain
open Enum_domain
-type cmdline_opt = {
- widen_delay : int;
- disjunct : (id -> bool);
- verbose_ci : bool;
- vverbose_ci : bool;
-}
module I (ED : ENUM_ENVIRONMENT_DOMAIN) (ND : NUMERICAL_ENVIRONMENT_DOMAIN) : sig
@@ -170,6 +165,7 @@ end = struct
rp : rooted_prog;
opt : cmdline_opt;
+ all_vars : (bool * id * typ) list;
enum_vars : (id * ED.item list) list;
num_vars : (id * bool) list;
@@ -181,7 +177,8 @@ end = struct
(* abstract interpretation *)
cycle : (id * id * typ) list; (* s'(x) = s(y) *)
forget : (id * typ) list; (* s'(x) not specified *)
- d_vars : id list; (* disjunction variables *)
+ d_vars : id list; (* disjunction variables when calculating *)
+ acc_d_vars : id list; (* disjunction variables in accumulator *)
top : case_v;
env : (case, case_v) Hashtbl.t;
mutable delta : case list;
@@ -191,7 +188,7 @@ end = struct
(*
print_st : Formatter.t -> st -> unit
*)
- let print_st fmt st = print_aux fmt st.d_vars st.env
+ let print_st fmt st = print_aux fmt st.acc_d_vars st.env
(*
add_case : st -> case_v -> unit
@@ -223,29 +220,70 @@ end = struct
| [en] -> aux en (v::vals) q
| _ -> assert false)
(ED.project enum p)
- in aux enum [] st.d_vars
+ in aux enum [] st.acc_d_vars
+
+ (*
+ dd_apply_cl : dd_v -> conslist -> dd_v
+ *)
+ let rec apply_cl_get_all_cases (enum, num) (ec, nc, r) =
+ match r with
+ | CLTrue ->
+ let enums = List.fold_left
+ (fun enums ec -> List.flatten
+ (List.map (fun e -> ED.apply_cons e ec) enums))
+ [enum] ec in
+ let num = ND.apply_cl num nc in
+ List.map (fun ec -> ec, num) enums
+ | CLFalse -> []
+ | CLAnd(a, b) ->
+ let envs = apply_cl_get_all_cases (enum, num) (ec, nc, a) in
+ List.flatten
+ (List.map (fun e -> apply_cl_get_all_cases e (ec, nc, b)) envs)
+ | CLOr((eca, nca, ra), (ecb, ncb, rb)) ->
+ apply_cl_get_all_cases (enum, num) (ec@eca, nc@nca, ra) @
+ apply_cl_get_all_cases (enum, num) (ec@ecb, nc@ncb, rb)
+
+ (*
+ pass_cycle : st -> case_v -> case_v
+ *)
+ let pass_cycle st (enum, num) =
+ let assign_e, assign_n = List.fold_left
+ (fun (ae, an) (a, b, t) -> match t with
+ | TEnum _ -> (a, b)::ae, an
+ | TInt | TReal -> ae, (a, NIdent b)::an)
+ ([], []) st.cycle in
+
+ let enum = ED.assign enum assign_e in
+ let num = ND.assign num assign_n in
+
+ List.fold_left
+ (fun (enum, num) (var, t) ->
+ let e, n = match t with
+ | TEnum _ -> ED.forgetvar enum var, num
+ | TReal | TInt -> enum, ND.forgetvar num var
+ in e, n)
+ (enum, num) st.forget
+ let dd_pass_cycle st (v : dd_v) =
+ let vv = dd_bot st.acc_d_vars in
+ Hashtbl.iter (fun _ x -> dd_add_case vv (pass_cycle st x)) v.data;
+ vv
(*
init_state : int -> rooted_prog -> st
*)
let init_state opt rp =
- Format.printf "Vars: @[<hov>%a@]@.@."
- (print_list Ast_printer.print_typed_var ", ")
- rp.all_vars;
-
- let num_vars, enum_vars = List.fold_left
- (fun (nv, ev) (_, id, t) -> match t with
- | TEnum ch -> nv, (id, ch)::ev
- | TInt -> (id, false)::nv, ev
- | TReal -> (id, true)::nv, ev)
- ([], []) rp.all_vars in
-
- let init_f = Transform.init_f_of_prog rp in
+ let init_f, f = Transform.f_of_prog rp false in
+ let _, f_g = Transform.f_of_prog rp true in
Format.printf "Init formula: %a@.@." Formula_printer.print_expr init_f;
- let init_cl = conslist_of_f init_f in
+ Format.printf "Cycle formula:@.%a@.@." Formula_printer.print_expr f;
+ let init_cl = conslist_of_f init_f in
+ let cl = Formula.conslist_of_f f in
+ let cl_g = Formula.conslist_of_f f_g in
+ Format.printf "Cycle conslist:@.%a@.@." Formula_printer.print_conslist cl;
+
let guarantees = Transform.guarantees_of_prog rp in
Format.printf "Guarantees:@.";
List.iter (fun (id, f) ->
@@ -253,69 +291,58 @@ end = struct
guarantees;
Format.printf "@.";
- let f = Formula.eliminate_not (Transform.f_of_prog rp false) in
- let f_g = Formula.eliminate_not (Transform.f_of_prog rp true) in
- Format.printf "Cycle formula:@.%a@.@." Formula_printer.print_expr f;
- let cl = Formula.conslist_of_f f in
- let cl_g = Formula.conslist_of_f f_g in
- Format.printf "Cycle conslist:@.%a@.@." Formula_printer.print_conslist cl;
+ (* add variables from LASTs *)
+ let last_vars = uniq_sorted
+ (List.sort compare (Transform.extract_last_vars f_g)) in
+ let last_vars = List.map
+ (fun id ->
+ let (_, _, ty) = List.find (fun (_, u, _) -> id = "L"^u) rp.all_vars
+ in false, id, ty)
+ last_vars in
+ let all_vars = last_vars @ rp.all_vars in
+
+ Format.printf "Vars: @[<hov>%a@]@.@."
+ (print_list Ast_printer.print_typed_var ", ")
+ all_vars;
+
+ let num_vars, enum_vars = List.fold_left
+ (fun (nv, ev) (_, id, t) -> match t with
+ | TEnum ch -> nv, (id, ch)::ev
+ | TInt -> (id, false)::nv, ev
+ | TReal -> (id, true)::nv, ev)
+ ([], []) all_vars in
(* calculate cycle variables and forget variables *)
let cycle = List.fold_left
(fun q (_, id, ty) ->
- if id.[0] = 'N' then
- (String.sub id 1 (String.length id - 1), id, ty)::q
+ if id.[0] = 'L' then
+ (id, String.sub id 1 (String.length id - 1), ty)::q
else q)
- [] rp.all_vars
- in
- let forget = List.map (fun (_, id, ty) -> (id, ty))
- (List.filter
- (fun (_, id, _) ->
- not (List.exists (fun (_, id2, _) -> id2 = "N"^id) rp.all_vars))
- rp.all_vars)
+ [] all_vars
in
+ let forget = List.map (fun (_, id, ty) -> (id, ty)) rp.all_vars in
(* calculate disjunction variables *)
- (* first approximation : use all enum variables appearing in init formula *)
- let rec calculate_dvars (ec, _, r) =
- let a = List.map (fun (_, id, _) -> id) ec in
- let rec aux = function
- | CLTrue | CLFalse -> []
- | CLAnd(u, v) ->
- aux u @ aux v
- | CLOr(u, v) ->
- calculate_dvars u @ calculate_dvars v
- in a @ aux r
- in
- let d_vars_0 = calculate_dvars init_cl in
- let d_vars_1 = List.filter
- (fun id -> opt.disjunct id && not (List.mem id d_vars_0) && id.[0] <> 'N')
+ (* actually, don't calculate them, rely on user input *)
+ let d_vars = List.filter (fun k -> k <> "/init" && opt.disjunct k)
(List.map (fun (id, _) -> id) enum_vars) in
- let d_vars = d_vars_0 @ d_vars_1 in
+ let acc_d_vars = List.filter (fun i -> i.[0] = 'L') d_vars in
(* setup abstract data *)
let top = ED.top enum_vars, ND.top num_vars in
let delta = [] in
let widen = Hashtbl.create 12 in
- (* calculate initial state and environment *)
- let init_s = dd_bot d_vars in
-
- let init_ec, _, _ = init_cl in
- let init_ed = List.fold_left
- (fun ed cons ->
- List.flatten (List.map (fun x -> ED.apply_cons x cons) ed))
- [ED.top enum_vars] (init_ec) in
- List.iter (fun ed -> dd_add_case init_s (ed, ND.top num_vars)) init_ed;
- let env_dd = apply_cl init_s init_cl in
- let env = env_dd.data in
-
let st =
- { rp; opt; enum_vars; num_vars;
+ { rp; opt; enum_vars; num_vars; all_vars;
cl; cl_g; guarantees;
- cycle; forget; d_vars; top;
- env; delta; widen } in
+ cycle; forget; acc_d_vars; d_vars; top;
+ env = Hashtbl.create 12; delta; widen } in
+
+ (* calculate initial state and environment *)
+ List.iter (fun ed -> add_case st (pass_cycle st ed))
+ (apply_cl_get_all_cases top init_cl);
Hashtbl.iter (fun case _ -> st.delta <- case::st.delta) st.env;
@@ -323,30 +350,6 @@ end = struct
(*
- pass_cycle : st -> case_v -> case_v
- *)
- let pass_cycle st (enum, num) =
- let assign_e, assign_n = List.fold_left
- (fun (ae, an) (a, b, t) -> match t with
- | TEnum _ -> (a, b)::ae, an
- | TInt | TReal -> ae, (a, NIdent b)::an)
- ([], []) st.cycle in
-
- let enum = ED.assign enum assign_e in
- let num = ND.assign num assign_n in
-
- List.fold_left
- (fun (enum, num) (var, t) -> match t with
- | TEnum _ -> ED.forgetvar enum var, num
- | TReal | TInt -> enum, ND.forgetvar num var)
- (enum, num) st.forget
-
- let dd_pass_cycle st (v : dd_v) =
- let vv = dd_bot v.d_vars in
- Hashtbl.iter (fun _ x -> dd_add_case vv (pass_cycle st x)) v.data;
- vv
-
- (*
cycle : st -> cl -> dd_v -> dd_v
*)
let cycle st cl env =
@@ -362,10 +365,10 @@ end = struct
let set_target_case st env case =
List.fold_left2
(fun env id v ->
- if List.exists (fun (id2, _) -> id2 = "N"^id) st.enum_vars then
- dd_apply_econs env (E_EQ, "N"^id, EItem v)
+ if List.exists (fun (id2, _) -> id2 = "L"^id) st.enum_vars then
+ dd_apply_econs env (E_EQ, id, EItem v)
else env)
- env st.d_vars case
+ env st.acc_d_vars case
(*
do_prog : rooted_prog -> unit
@@ -387,7 +390,7 @@ end = struct
(print_list Formula_printer.print_id ", ") case;
let start = try Hashtbl.find st.env case with Not_found -> assert false in
- let start_dd = dd_singleton st.d_vars start in
+ let start_dd = dd_singleton st.acc_d_vars start in
let f i =
let i = dd_singleton st.d_vars i in
let i' = set_target_case st i case in
@@ -422,7 +425,6 @@ end = struct
Hashtbl.iter (fun _ q -> add_case st q) j.data)
!cases;
-
if st.opt.verbose_ci then
Format.printf "-> @[<hov>%a@]@." print_st st;
diff --git a/abstract/abs_interp_edd.ml b/abstract/abs_interp_edd.ml
index 6220a0a..8ea0012 100644
--- a/abstract/abs_interp_edd.ml
+++ b/abstract/abs_interp_edd.ml
@@ -2,10 +2,10 @@ open Ast
open Ast_util
open Formula
open Typing
+open Cmdline
open Util
open Num_domain
-open Abs_interp
@@ -592,9 +592,12 @@ end = struct
rp : rooted_prog;
opt : cmdline_opt;
+ last_vars : (bool * id * typ) list;
+ all_vars : (bool * id * typ) list;
ve : varenv;
(* program expressions *)
+ init_cl : conslist;
cl : conslist;
cl_g : conslist;
guarantees : (id * bool_expr) list;
@@ -602,7 +605,6 @@ end = struct
(* abstract interpretation *)
cycle : (id * id * typ) list; (* s'(x) = s(y) *)
forget : (id * typ) list; (* s'(x) not specified *)
- mutable data : edd_v;
}
@@ -924,20 +926,15 @@ end = struct
init_env : cmdline_opt -> rooted_prog -> env
*)
let init_env opt rp =
- Format.printf "Vars: @[<hov>%a@]@.@."
- (print_list Ast_printer.print_typed_var ", ")
- rp.all_vars;
-
- let num_vars, enum_vars = List.fold_left
- (fun (nv, ev) (_, id, t) -> match t with
- | TEnum ch -> nv, (id, ch)::ev
- | TInt -> (id, false)::nv, ev
- | TReal -> (id, true)::nv, ev)
- ([], []) rp.all_vars in
+ let init_f, f = Transform.f_of_prog rp false in
+ let _, f_g = Transform.f_of_prog rp true in
+ Format.printf "Init formula:@.%a@.@." Formula_printer.print_expr init_f;
+ Format.printf "Cycle formula:@.%a@.@." Formula_printer.print_expr f;
- let init_f = Transform.init_f_of_prog rp in
- Format.printf "Init formula: %a@.@." Formula_printer.print_expr init_f;
- let init_cl = conslist_of_f init_f in
+ let cl = Formula.conslist_of_f f in
+ let cl_g = Formula.conslist_of_f f_g in
+ let init_cl = Formula.conslist_of_f init_f in
+ Format.printf "Cycle conslist:@.%a@.@." Formula_printer.print_conslist cl;
let guarantees = Transform.guarantees_of_prog rp in
Format.printf "Guarantees:@.";
@@ -945,20 +942,32 @@ end = struct
Format.printf " %s: %a@." id Formula_printer.print_expr f)
guarantees;
Format.printf "@.";
+
+ (* add variables from LASTs *)
+ let last_vars = uniq_sorted (List.sort compare (Transform.extract_last_vars f_g)) in
+ let last_vars = List.map
+ (fun id ->
+ let (_, _, ty) = List.find (fun (_, u, _) -> id = "L"^u) rp.all_vars
+ in false, id, ty)
+ last_vars in
+ let all_vars = last_vars @ rp.all_vars in
- let f = Formula.eliminate_not (Transform.f_of_prog rp false) in
- let f_g = Formula.eliminate_not (Transform.f_of_prog rp true) in
- Format.printf "Cycle formula:@.%a@.@." Formula_printer.print_expr f;
+ Format.printf "Vars: @[<hov>%a@]@.@."
+ (print_list Ast_printer.print_typed_var ", ")
+ all_vars;
+
+ let num_vars, enum_vars = List.fold_left
+ (fun (nv, ev) (_, id, t) -> match t with
+ | TEnum ch -> nv, (id, ch)::ev
+ | TInt -> (id, false)::nv, ev
+ | TReal -> (id, true)::nv, ev)
+ ([], []) all_vars in
- let cl = Formula.conslist_of_f f in
- let cl_g = Formula.conslist_of_f f_g in
- Format.printf "Cycle conslist:@.%a@.@." Formula_printer.print_conslist cl;
(* calculate order for enumerated variables *)
let evars = List.map fst enum_vars in
- let lv = extract_linked_evars_root init_cl
- @ extract_linked_evars_root cl_g in
+ let lv = extract_linked_evars_root cl_g in
let lv = uniq_sorted
(List.sort Pervasives.compare (List.map ord_couple lv)) in
@@ -969,6 +978,9 @@ end = struct
(List.filter (fun n -> is_suffix n "init") evars)) in
let lv_f = lv_f @ (List.map (fun v -> (3.0, ["#BEGIN"; v]))
(List.filter (fun n -> is_suffix n "state") evars)) in
+ let lv_f = lv_f @
+ (List.map (fun v -> (0.7, [v; "L"^v]))
+ (List.filter (fun n -> List.mem ("L"^n) evars) evars)) in
let evars_ord =
if true then
time "FORCE" (fun () -> force_ordering evars lv_f)
@@ -995,25 +1007,17 @@ end = struct
(* calculate cycle variables and forget variables *)
let cycle = List.fold_left
(fun q (_, id, ty) ->
- if id.[0] = 'N' then
- (String.sub id 1 (String.length id - 1), id, ty)::q
+ if id.[0] = 'L' then
+ (id, String.sub id 1 (String.length id - 1), ty)::q
else q)
- [] rp.all_vars
- in
- let forget = List.map (fun (_, id, ty) -> (id, ty))
- (List.filter
- (fun (_, id, _) ->
- not (List.exists (fun (_, id2, _) -> id2 = "N"^id) rp.all_vars))
- rp.all_vars)
+ [] last_vars
in
+ let forget = List.map (fun (_, id, ty) -> (id, ty)) rp.all_vars in
- (* calculate initial environment *)
- let data = edd_apply_cl (edd_top ve) init_cl in
- Format.printf "Init: @[<hov>%a@]@." edd_print data;
- { rp; opt; ve;
- cl; cl_g; guarantees;
- cycle; forget; data }
+ { rp; opt; ve; last_vars; all_vars;
+ init_cl; cl; cl_g; guarantees;
+ cycle; forget }
@@ -1094,7 +1098,9 @@ end = struct
end
in
- let init_acc = edd_star_new (edd_bot e.data.ve) e.data in
+ Format.printf "Calculating initial state...@.";
+ let init_acc = edd_star_new (edd_bot e.ve)
+ (pass_cycle e (edd_apply_cl (edd_top e.ve) e.init_cl)) in
(* Dump final state *)
let acc = ch_it 0 init_acc in
@@ -1124,13 +1130,13 @@ end = struct
end;
(* Examine probes *)
- if List.exists (fun (p, _, _) -> p) e.rp.all_vars then begin
+ if List.exists (fun (p, _, _) -> p) e.all_vars then begin
let final_flat = edd_forget_vars final
(List.fold_left
(fun l (_, id, ty) -> match ty with
| TInt | TReal -> l
| TEnum _ -> id::l)
- [] e.rp.all_vars) in
+ [] e.all_vars) in
let final_flat = match final_flat.root with
| DTop -> ND.top e.ve.nvars
| DBot -> ND.bottom e.ve.nvars
@@ -1146,7 +1152,7 @@ end = struct
ND.print_itv (ND.project final_flat id)
| TEnum _ -> Format.printf "%a : enum variable@."
Formula_printer.print_id id)
- e.rp.all_vars;
+ e.all_vars;
Format.printf "@]@."
end
diff --git a/abstract/formula.ml b/abstract/formula.ml
index 01f6655..0045489 100644
--- a/abstract/formula.ml
+++ b/abstract/formula.ml
@@ -50,19 +50,26 @@ type bool_expr =
| BOr of bool_expr * bool_expr
| BNot of bool_expr
-let f_and a b = match a, b with
- | BConst false, _ | _, BConst false -> BConst false
- | BConst true, b -> b
- | a, BConst true -> a
- | a, b -> BAnd(a, b)
+let is_false = function
+ | BConst false | BNot(BConst true) -> true
+ | _ -> false
+let is_true = function
+ | BConst true | BNot(BConst false) -> true
+ | _ -> false
+
+let f_and a b =
+ if is_false a || is_false b then BConst false
+ else if is_true a then b
+ else if is_true b then a
+ else BAnd(a, b)
let f_and_list = List.fold_left f_and (BConst true)
-let f_or a b = match a, b with
- | BConst true, _ | _, BConst true -> BConst true
- | BConst false, b -> b
- | a, BConst false -> a
- | a, b -> BOr(a, b)
+let f_or a b =
+ if is_true a || is_true b then BConst true
+ else if is_false a then b
+ else if is_false b then a
+ else BOr(a, b)
let f_e_op op a b = match a, b with
| EItem i, EItem j -> BConst (if op = E_EQ then i = j else i <> j)
diff --git a/abstract/transform.ml b/abstract/transform.ml
index dcb4049..480705f 100644
--- a/abstract/transform.ml
+++ b/abstract/transform.ml
@@ -7,7 +7,14 @@ open Typing
open Interpret (* used for constant evaluation ! *)
-(* Transform SCADE program to logical formula. *)
+(* Transform SCADE program to logical formula.
+
+ Convention : to access the last value of a variable,
+ access the variable with the same name prefixed by "L".
+ A pre-processing pass will extract the variables that are
+ referenced in such a way so that they are taken into
+ account when calculating the memory.
+*)
(* node * prefix * equations *)
type scope = id * id * eqn ext list
@@ -72,7 +79,7 @@ let rec f_of_neexpr td (node, prefix, clock_scope) where expr =
let typ = type_expr td.rp node expr in
where
(List.mapi
- (fun i t -> let x = id^"."^(string_of_int i) in
+ (fun i t -> let x = "L"^id^"."^(string_of_int i) in
match t with
| TInt -> NE(NIdent x, false)
| TReal -> NE(NIdent x, true)
@@ -136,6 +143,7 @@ let rec f_of_neexpr td (node, prefix, clock_scope) where expr =
and f_of_bexpr td (node, prefix, clock_scope) where expr =
let sub = f_of_bexpr td (node, prefix, clock_scope) in
let sub_id = sub (fun x -> x) in
+ let le = loc_error (snd expr) in
match fst expr with
| AST_bool_const b -> where (BConst b)
| AST_binary_bool(AST_AND, a, b) -> where (f_and (sub_id a) (sub_id b))
@@ -152,7 +160,8 @@ and f_of_bexpr td (node, prefix, clock_scope) where expr =
| AST_NE -> E_NE
| _ -> type_error "Invalid operator on enumerated values."
in f_e_op eop x y
- | _ -> invalid_arity "Binary operator")
+ | [NE _; EE _] | [EE _; NE _] -> le type_error "Invalid arguments for binary operator."
+ | _ -> le invalid_arity "Binary operator")
(AST_tuple [a; b], snd expr))
(* Temporal *)
| AST_arrow(a, b) ->
@@ -180,7 +189,7 @@ and f_of_bexpr td (node, prefix, clock_scope) where expr =
| _ -> assert false
in
f_of_neexpr td (node, prefix, clock_scope) ff expr
- | _ -> type_error "Expected boolean value."
+ | _ -> le type_error "Expected boolean value."
and f_of_expr td (node, prefix, clock_scope) expr =
f_of_bexpr td (node, prefix, clock_scope) (fun x -> x) expr
@@ -190,40 +199,63 @@ and f_of_expr td (node, prefix, clock_scope) expr =
Translate program into one big formula
*)
+let reset_cond rst_exprs =
+ List.fold_left f_or (BConst false) rst_exprs
+let no_reset_cond rst_exprs =
+ List.fold_left (fun ff c -> f_and ff (BNot c)) (BConst true) rst_exprs
+
let clock_scope_here (node, prefix, _) =
node^"/"^prefix
-let gen_clock td (node, prefix, _) active =
+let gen_clock td (node, prefix, _) active rst_exprs =
let clock_scope = node^"/"^prefix in
let clock_eq =
- if active then
- f_and
- (if not (td.rp.no_time_scope clock_scope)
- then BRel(AST_EQ, NIdent("N"^clock_scope^"time"),
- NBinary(AST_PLUS, NIntConst 1, NIdent(clock_scope^"time"), false),
- false)
- else BConst true)
- (if td.rp.init_scope clock_scope
- then f_e_eq (EIdent("N"^clock_scope^"init")) (EItem bool_false)
- else BConst true)
- else
- f_and
- (if not (td.rp.no_time_scope clock_scope)
- then BRel(AST_EQ,
- NIdent("N"^clock_scope^"time"),
- NIdent(clock_scope^"time"), false)
- else BConst true)
- (if td.rp.init_scope clock_scope
- then f_e_eq (EIdent("N"^clock_scope^"init"))
- (EIdent (clock_scope^"init"))
- else BConst true)
+ let rst_code =
+ f_and
+ (if not (td.rp.no_time_scope clock_scope)
+ then BRel(AST_EQ, NIdent(clock_scope^"time"), NIntConst 0, false)
+ else BConst true)
+ (if td.rp.init_scope clock_scope
+ then f_e_eq (EIdent(clock_scope^"init")) (EItem bool_true)
+ else BConst true)
+ in
+ let no_rst_code =
+ if active then
+ f_and
+ (if not (td.rp.no_time_scope clock_scope)
+ then BRel(AST_EQ, NIdent(clock_scope^"time"),
+ NBinary(AST_PLUS, NIntConst 1, NIdent("L"^clock_scope^"time"), false),
+ false)
+ else BConst true)
+ (if td.rp.init_scope clock_scope
+ then f_e_eq (EIdent(clock_scope^"init")) (EItem bool_false)
+ else BConst true)
+ else
+ f_and
+ (if not (td.rp.no_time_scope clock_scope)
+ then BRel(AST_EQ,
+ NIdent(clock_scope^"time"),
+ NIdent("L"^clock_scope^"time"), false)
+ else BConst true)
+ (if td.rp.init_scope clock_scope
+ then f_e_eq (EIdent(clock_scope^"init"))
+ (EIdent ("L"^clock_scope^"init"))
+ else BConst true)
+ in
+ if rst_code = BConst true && no_rst_code = BConst true
+ then BConst true
+ else
+ f_or
+ (f_and (reset_cond rst_exprs) rst_code)
+ (f_and (no_reset_cond rst_exprs) no_rst_code)
in
- clock_scope, clock_eq
+ (clock_scope, rst_exprs), clock_eq
-let rec f_of_scope active td (node, prefix, eqs) clock_scope assume_guarantees =
+let rec f_of_scope active td (node, prefix, eqs) (clock_scope, rst_exprs as cs) assume_guarantees =
let expr_eq e =
let instance_eq (_, id, eqs, args) =
- let eq = f_of_scope active td (node^"/"^id, "", eqs) clock_scope assume_guarantees in
+ let eq = f_of_scope active td (node^"/"^id, "", eqs)
+ cs assume_guarantees in
if active then
let arg_eq ((_,argname,ty), expr) =
f_of_neexpr td (node, prefix, clock_scope) (function
@@ -247,7 +279,7 @@ let rec f_of_scope active td (node, prefix, eqs) clock_scope assume_guarantees =
f_of_neexpr td (node, prefix, clock_scope) (fun elist ->
list_fold_op f_and
(List.mapi
- (fun i v -> let x = ("N"^id^"."^(string_of_int i)) in
+ (fun i v -> let x = (id^"."^(string_of_int i)) in
match v with
| NE (v, r) -> BRel(AST_EQ, NIdent x, v, r)
| EE v -> f_e_eq (EIdent x) v)
@@ -257,11 +289,11 @@ let rec f_of_scope active td (node, prefix, eqs) clock_scope assume_guarantees =
let typ = type_expr td.rp node expr in
list_fold_op f_and
(List.mapi
- (fun i t -> let x = string_of_int i in
+ (fun i t -> let id_x = id ^ "." ^ string_of_int i in
match t with
- | TInt -> BRel(AST_EQ, NIdent("N"^id^"."^x), NIdent (id^"."^x), false)
- | TReal -> BRel(AST_EQ, NIdent("N"^id^"."^x), NIdent (id^"."^x), true)
- | TEnum _ -> f_e_eq (EIdent("N"^id^"."^x)) (EIdent (id^"."^x)))
+ | TInt -> BRel(AST_EQ, NIdent(id_x), NIdent ("L"^id_x), false)
+ | TReal -> BRel(AST_EQ, NIdent(id_x), NIdent ("L"^id_x), true)
+ | TEnum _ -> f_e_eq (EIdent(id_x)) (EIdent ("L"^id_x)))
typ)
in
let eq_p = f_and_list (List.map pre_expr (extract_pre e)) in
@@ -323,8 +355,8 @@ let rec f_of_scope active td (node, prefix, eqs) clock_scope assume_guarantees =
let rec do_tree_act = function
| AST_activate_body b ->
let b_scope = node, b.act_id^".", b.body in
- let clock_scope, clock_eq = gen_clock td b_scope true in
- f_and clock_eq (f_of_scope true td b_scope clock_scope assume_guarantees)
+ let cs2, clock_eq = gen_clock td b_scope true rst_exprs in
+ f_and clock_eq (f_of_scope true td b_scope cs2 assume_guarantees)
| AST_activate_if(c, a, b) ->
f_or
(f_and (f_of_expr td (node, prefix, clock_scope) c)
@@ -334,47 +366,97 @@ let rec f_of_scope active td (node, prefix, eqs) clock_scope assume_guarantees =
and do_tree_inact = function
| AST_activate_body b ->
let b_scope = node, b.act_id^".", b.body in
- let clock_scope, clock_eq = gen_clock td b_scope false in
- f_and clock_eq (f_of_scope false td b_scope clock_scope assume_guarantees)
+ let cs2, clock_eq = gen_clock td b_scope false rst_exprs in
+ f_and clock_eq (f_of_scope false td b_scope cs2 assume_guarantees)
| AST_activate_if(_, a, b) ->
f_and (do_tree_inact a) (do_tree_inact b)
in
f_and (cond_eq b) (if active then do_tree_act b else do_tree_inact b)
| AST_automaton (aid, states, _) ->
+ let (init_st, _) = List.find (fun (st, _) -> st.initial) states in
+ let lnstv = "L"^node^"/"^aid^".next_state" in
+ let nstv = node^"/"^aid^".next_state" in
let stv = node^"/"^aid^".state" in
- let nstv = "N"^node^"/"^aid^".state" in
+ let st_choice_eq =
+ f_or
+ (f_and (reset_cond rst_exprs) (f_e_eq (EIdent stv) (EItem init_st.st_name)))
+ (f_and (no_reset_cond rst_exprs) (f_e_eq (EIdent stv) (EIdent lnstv)))
+ in
+
+ let rst_states = uniq_sorted @@ List.sort compare @@ List.flatten
+ (List.map (fun (st, _) ->
+ List.map (fun (_, (id, _), _) -> id)
+ (List.filter (fun (_, _, rst) -> rst) st.until))
+ states)
+ in
+
let st_eq_inact (st, _) =
let st_scope = node, aid^"."^st.st_name^".", st.body in
- let clock_scope, clock_eq = gen_clock td st_scope false in
+ let clock_scope, clock_eq = gen_clock td st_scope false rst_exprs in
f_and clock_eq
(f_and
- (f_of_scope false td st_scope clock_scope assume_guarantees)
+ (f_of_scope false td st_scope cs assume_guarantees)
(f_and_list (List.map (fun (c, _, _) -> expr_eq c) st.until)))
in
if active then
let st_eq_act (st, l) =
let act_eq =
let st_scope = node, aid^"."^st.st_name^".", st.body in
- let clock_scope, clock_eq = gen_clock td st_scope true in
- let st_eq = f_and clock_eq (f_of_scope true td st_scope clock_scope assume_guarantees) in
+ let rst_exprs =
+ if List.mem st.st_name rst_states then
+ (f_e_eq (EIdent("L"^node^"/"^aid^"."^st.st_name^".must_reset"))
+ (EItem bool_true))::rst_exprs
+ else rst_exprs
+ in
+ let cs2, clock_eq = gen_clock td st_scope true rst_exprs in
+ let st_eq = f_and clock_eq (f_of_scope true td st_scope cs2 assume_guarantees) in
+
+ let cr, cnr = List.partition
+ (fun i -> List.exists (fun (_, (v, _), x) -> x && v = i) st.until)
+ rst_states in
+ let must_reset_c l f =
+ f_and_list
+ (List.map
+ (fun i -> f_e_eq (EIdent (node^"/"^aid^"."^i^".must_reset"))
+ (EItem (if f i then bool_true else bool_false)))
+ l)
+ in
let rec aux = function
- | [] -> BEnumCons(E_EQ, nstv, EItem st.st_name)
+ | [] ->
+ f_and
+ (must_reset_c cr (fun _ -> false))
+ (BEnumCons(E_EQ, nstv, EItem st.st_name))
| (c, (target, l), rst)::q ->
- if rst then loc_error l error "Resetting transitions not supported.";
f_or
(f_and (f_of_expr td (node, prefix, clock_scope) c)
- (BEnumCons(E_EQ, nstv, EItem target)))
+ (f_and
+ (BEnumCons(E_EQ, nstv, EItem target))
+ (must_reset_c cr (fun i -> rst && i = target))))
(f_and (BNot (f_of_expr td (node, prefix, clock_scope) c)) (aux q))
- in f_and st_eq (aux st.until)
+ in
+ let trans_code = must_reset_c cnr (fun _ -> false) in
+ let trans_code = f_and trans_code (aux st.until) in
+ f_and st_eq trans_code
in
- f_or
- (f_and (BEnumCons(E_EQ, stv, EItem st.st_name)) act_eq)
- (f_and (BEnumCons(E_NE, stv, EItem st.st_name))
- (st_eq_inact (st, l)))
+ if List.length states = 1 then
+ act_eq
+ else
+ f_or
+ (f_and (BEnumCons(E_EQ, stv, EItem st.st_name)) act_eq)
+ (f_and (BEnumCons(E_NE, stv, EItem st.st_name))
+ (st_eq_inact (st, l)))
in
- f_and_list (List.map st_eq_act states)
+ f_and st_choice_eq
+ (f_and_list (List.map st_eq_act states))
else
- f_and_list (List.map st_eq_inact states)
+ f_and st_choice_eq
+ (f_and
+ (f_and_list
+ (List.map
+ (fun s -> let n = node^"/"^aid^"."^s^".must_reset" in
+ f_e_eq (EIdent n) (EIdent ("L"^n)))
+ rst_states))
+ (f_and_list (List.map st_eq_inact states)))
in
f_and_list (List.map do_eq eqs)
@@ -384,77 +466,32 @@ and f_of_prog rp assume_guarantees =
consts = I.consts rp;
} in
- let clock_scope, clock_eq = gen_clock td rp.root_scope true in
-
- let scope_f =
- f_of_scope
- true
- td td.rp.root_scope
- clock_scope
- assume_guarantees in
- f_and clock_eq scope_f
-
+ let prog_normal =
+ let clock_scope, clock_eq = gen_clock td rp.root_scope true [] in
-(*
- Translate init state into a formula
-*)
-let gen_clock_init rp (node, prefix, _) =
- let clock_scope = node^"/"^prefix in
- let time_eq =
- f_and
- (if not (rp.no_time_scope clock_scope)
- then
- BRel(AST_EQ,
- NIdent(clock_scope^"time"),
- NIntConst 0, false)
- else BConst true)
- (if rp.init_scope clock_scope
- then
- f_e_eq (EIdent(clock_scope^"init")) (EItem bool_true)
- else BConst true)
- in
- clock_scope, time_eq
+ let scope_f =
+ f_of_scope
+ true
+ td td.rp.root_scope
+ clock_scope
+ assume_guarantees in
+ f_and clock_eq scope_f
+ in
+ let prog_init =
+ let clock_scope, clock_eq =
+ gen_clock td rp.root_scope true [BConst true] in
-let rec init_f_of_scope rp (node, prefix, eqs) clock_scope =
- let expr_eq e =
- let instance_eq (_, id, eqs, args) =
- init_f_of_scope rp (node^"/"^id, "", eqs) clock_scope
+ let scope_f =
+ f_of_scope
+ true
+ td td.rp.root_scope
+ clock_scope
+ assume_guarantees in
+ f_and clock_eq scope_f
in
- List.fold_left (fun x i -> f_and (instance_eq i) x)
- (BConst true) (extract_instances rp.p e)
- in
- let do_eq eq = match fst eq with
- | AST_assign(_, e) | AST_assume(_, e) | AST_guarantee(_, e) ->
- expr_eq e
- | AST_activate (b, _) ->
- let rec cond_eq = function
- | AST_activate_body b ->
- let bscope = (node, b.act_id^".", b.body) in
- let clock_scope, clock_eq = gen_clock_init rp bscope in
- f_and clock_eq (init_f_of_scope rp bscope clock_scope)
- | AST_activate_if(c, a, b) ->
- f_and (expr_eq c)
- (f_and (cond_eq a) (cond_eq b))
- in
- cond_eq b
- | AST_automaton (aid, states, _) ->
- let (st, _) = List.find (fun (st, _) -> st.initial) states in
- let init_eq = BEnumCons(E_EQ, node^"/"^aid^".state", EItem st.st_name) in
- let state_eq (st, _) =
- let sc_f =
- let st_scope = (node, aid^"."^st.st_name^".", st.body) in
- let clock_scope, clock_eq = gen_clock_init rp st_scope in
- f_and clock_eq (init_f_of_scope rp st_scope clock_scope)
- in List.fold_left (fun f (c, _, _) -> f_and f (expr_eq c)) sc_f st.until
- in
- List.fold_left f_and init_eq
- (List.map state_eq states)
- in
- f_and_list (List.map do_eq eqs)
+ prog_init, prog_normal
+
-and init_f_of_prog rp =
- let clock_scope, clock_eq = gen_clock_init rp rp.root_scope in
- f_and clock_eq (init_f_of_scope rp rp.root_scope clock_scope)
(*
Get expressions for guarantee violation
@@ -502,3 +539,30 @@ and guarantees_of_prog rp =
g_of_scope td rp.root_scope (clock_scope_here rp.root_scope) (BConst true)
+
+
+(*
+ Extract variables accessed by a LAST
+*)
+
+let rec extract_last_vars = function
+ | BRel(_, a, b, _) ->
+ elv_ne a @ elv_ne b
+ | BEnumCons c ->
+ elv_ec c
+ | BAnd(a, b) | BOr (a, b) ->
+ extract_last_vars a @ extract_last_vars b
+ | BNot(e) -> extract_last_vars e
+ | _ -> []
+
+and elv_ne = function
+ | NIdent i when i.[0] = 'L' -> [i]
+ | NBinary(_, a, b, _) -> elv_ne a @ elv_ne b
+ | NUnary (_, a, _) -> elv_ne a
+ | _ -> []
+
+and elv_ec (_, v, q) =
+ (if v.[0] = 'L' then [v] else []) @
+ (match q with
+ | EIdent i when i.[0] = 'L' -> [i]
+ | _ -> [])
diff --git a/cmdline.ml b/cmdline.ml
new file mode 100644
index 0000000..b8f8ea8
--- /dev/null
+++ b/cmdline.ml
@@ -0,0 +1,8 @@
+open Ast
+
+type cmdline_opt = {
+ widen_delay : int;
+ disjunct : (id -> bool);
+ verbose_ci : bool;
+ vverbose_ci : bool;
+}
diff --git a/frontend/ast.ml b/frontend/ast.ml
index c561cef..d55626d 100644
--- a/frontend/ast.ml
+++ b/frontend/ast.ml
@@ -69,10 +69,6 @@ and state = {
st_locals : var_def list;
body : eqn ext list;
until : transition list;
- (* these two rst info are determined after parsing, in typing.ml when
- the variable list is extracted *)
- mutable i_rst : bool; (* resettable by S -> S transition *)
- mutable o_rst : bool; (* resettable by S' -> S transition *)
}
and transition = (expr ext) * (id ext) * bool (* bool : does it reset ? *)
diff --git a/frontend/lexer.mll b/frontend/lexer.mll
index ef40aa7..837ee75 100644
--- a/frontend/lexer.mll
+++ b/frontend/lexer.mll
@@ -88,6 +88,7 @@ rule token = parse
| const_real as c { REALVAL c }
(* spaces, comments *)
| "(*" { comment lexbuf; token lexbuf }
+ | "/*" { cppcomment lexbuf; token lexbuf }
| "--" [^ '\n' '\r']* { token lexbuf }
| newline { new_line lexbuf; token lexbuf }
| space { token lexbuf }
@@ -98,3 +99,8 @@ and comment = parse
| "*)" { () }
| [^ '\n' '\r'] { comment lexbuf }
| newline { new_line lexbuf; comment lexbuf }
+
+and cppcomment = parse
+ | "*/" { () }
+ | [^ '\n' '\r'] { cppcomment lexbuf }
+ | newline { new_line lexbuf; cppcomment lexbuf }
diff --git a/frontend/parser.mly b/frontend/parser.mly
index 672bb9a..e8a6ecf 100644
--- a/frontend/parser.mly
+++ b/frontend/parser.mly
@@ -126,7 +126,6 @@ state:
st_locals = v;
body = b;
until = until;
- i_rst = false; o_rst = false; (* calculated later *)
} }
trans(TT):
diff --git a/frontend/typing.ml b/frontend/typing.ml
index 2859230..883e8e0 100644
--- a/frontend/typing.ml
+++ b/frontend/typing.ml
@@ -129,15 +129,12 @@ let clock_vars rp (node, prefix, _) =
let v =
if not (rp.no_time_scope (node^"/"^prefix))
then
- [
- false, node^"/"^prefix^"time", TInt;
- false, "N"^node^"/"^prefix^"time", TInt]
+ [false, node^"/"^prefix^"time", TInt]
else [] in
let v =
if rp.init_scope (node^"/"^prefix)
then
- (false, node^"/"^prefix^"init", bool_type)::
- (false, "N"^node^"/"^prefix^"init", bool_type)::v
+ (false, node^"/"^prefix^"init", bool_type)::v
else v in
v
@@ -145,9 +142,7 @@ let clock_vars rp (node, prefix, _) =
extract_all_vars : rooted_prog -> scope -> var list
Extracts all variables with names given according to
- naming convention used here and in transform.ml :
- - pre variables are not prefixed by scope
- - next values for variables are prefixed by capital N
+ naming convention used here and in transform.ml
*)
let rec extract_all_vars rp (node, prefix, eqs) n_vars =
let vars_of_expr e =
@@ -162,12 +157,9 @@ let rec extract_all_vars rp (node, prefix, eqs) n_vars =
(List.map
(fun (id, expr) ->
let id = node^"/"^id in
- let vd =
- List.mapi
- (fun i t -> false, id^"."^(string_of_int i), t)
- (type_expr_vl rp.p n_vars rp.const_vars node expr)
- in
- vd @ (List.map (fun (a, x, c) -> (a, "N"^x, c)) vd))
+ List.mapi
+ (fun i t -> false, id^"."^(string_of_int i), t)
+ (type_expr_vl rp.p n_vars rp.const_vars node expr))
(extract_pre e))
in
let vars_of_eq e = match fst e with
@@ -186,17 +178,12 @@ let rec extract_all_vars rp (node, prefix, eqs) n_vars =
vars_of_expr c @ do_branch a @ do_branch b
in do_branch b
| AST_automaton (aid, states, ret) ->
- (* Determine which states can be reset *)
- let rst_trans = List.flatten
+ let rst_states = List.flatten
(List.map (fun (st, _) ->
- List.map (fun (_, (id, _), _) -> (st.st_name, id))
+ List.map (fun (_, (id, _), _) -> id)
(List.filter (fun (_, _, rst) -> rst) st.until))
states)
in
- List.iter (fun (st, _) ->
- st.i_rst <- List.mem (st.st_name, st.st_name) rst_trans;
- st.o_rst <- List.exists (fun (a, b) -> b = st.st_name && a <> b) rst_trans)
- states;
let do_state (st, _) =
let tvars =
@@ -205,15 +192,15 @@ let rec extract_all_vars rp (node, prefix, eqs) n_vars =
in
let st_scope = (node, aid^"."^st.st_name^".", st.body) in
let svars = vars_in_node node st.st_locals in
- (if st.i_rst || st.o_rst then
- [false, node^"/"^aid^"."^st.st_name^".next_reset", bool_type]
+ (if List.mem st.st_name rst_states then
+ [false, node^"/"^aid^"."^st.st_name^".must_reset", bool_type]
else [])
@ svars @ tvars @ clock_vars rp st_scope @
extract_all_vars rp st_scope (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)::
+ (false, node^"/"^aid^".next_state", TEnum st_ids)::
(List.flatten (List.map do_state states))
in
let v = List.flatten (List.map vars_of_eq eqs) in
@@ -247,6 +234,7 @@ let root_prog p root no_time_scope init_scope =
let root_vars = vars_in_node "" (decls_of_node root_node) in
let root_clock_vars = clock_vars rp root_scope in
- { rp with all_vars = root_clock_vars @ root_vars @ extract_all_vars rp root_scope root_vars }
+ { rp with all_vars = root_clock_vars @
+ root_vars @ extract_all_vars rp root_scope root_vars }
diff --git a/libs/util.ml b/libs/util.ml
index 940fe3e..6e8dc59 100644
--- a/libs/util.ml
+++ b/libs/util.ml
@@ -13,7 +13,7 @@ let rec uniq_sorted = function
(* list_fold_op : ('a -> 'a -> 'a) -> 'a list -> 'a *)
let rec list_fold_op op = function
- | [] -> invalid_arg "list_fold_opt on empty list"
+ | [] -> invalid_arg "list_fold_op on empty list"
| [a] -> a
| x::q -> op x (list_fold_op op q)
diff --git a/main.ml b/main.ml
index 5e9f087..2995e24 100644
--- a/main.ml
+++ b/main.ml
@@ -1,9 +1,10 @@
+open Cmdline
+
open Ast
open Num_domain
open Nonrelational
open Apron_domain
-open Abs_interp
module Interpret = Interpret.I
@@ -26,7 +27,7 @@ let ai_rel = ref false
let ai_itv_edd = ref false
let ai_rel_edd = ref false
let ai_root = ref "test"
-let ai_widen_delay = ref 3
+let ai_widen_delay = ref 5
let ai_no_time_scopes = ref ""
let ai_init_scopes = ref ""
let ai_disj_v = ref ""
@@ -106,9 +107,16 @@ let () =
if !ai_itv || !ai_rel || !ai_itv_edd || !ai_rel_edd then begin
let comma_split = Str.split (Str.regexp ",") in
let select_f x =
- if x = "all"
- then (fun _ -> true)
- else (fun i -> List.mem i (comma_split x))
+ if x = "all" then
+ (fun _ -> true)
+ else if x = "last" then
+ (fun i -> i.[0] = 'L')
+ else if String.length x > 5 && String.sub x 0 5 = "last+" then
+ let psl = comma_split
+ (String.sub x 5 (String.length x - 5)) in
+ (fun i -> i.[0] = 'L' || List.mem i psl)
+ else
+ (fun i -> List.mem i (comma_split x))
in
let rp = Typing.root_prog prog !ai_root
(select_f !ai_no_time_scopes)
diff --git a/tests/source/NestedControl.scade b/tests/source/NestedControl.scade
index 2551eb6..af4fdab 100644
--- a/tests/source/NestedControl.scade
+++ b/tests/source/NestedControl.scade
@@ -1,13 +1,13 @@
node root(In : int; C : bool) returns (Out, Out1 : int)
var last_Out, last_Out1: int;
- isp, isn: bool;
+ disj, disj2: bool;
let
last_Out = 0 -> pre Out;
last_Out1 = 0 -> pre Out1;
- isp = In > 0;
- isn = In < 0;
- assume C_in_not_null: (not C) or isp or isn;
+ disj = In > 0;
+ disj2 = In < 0;
+ assume C_in_not_null: (not C) or disj or disj2;
automaton SM1
initial state State1
diff --git a/tests/source/counters.scade b/tests/source/counters.scade
index 3266ec9..334bca1 100755
--- a/tests/source/counters.scade
+++ b/tests/source/counters.scade
@@ -1,4 +1,15 @@
+/*
+ x = 10 | 9 | 8 | 7 | 6 | 5 | ... | 0 | 1 | 2 | ... | 10 | ...
+ y = 0 | 1 | 2 | 3 | 4 | 5 | ... | 10 | 9 | 8 | ... | 0 | ...
+ b1 = t | f | f | f | f | f | ... | f | f | f | ... | t | ...
+ b2 = t | f | f | f | f | f | ... | f | f | f | ... | t | ...
+
+ eq* = t | t | t | t | t | t | ... | t | t | t | ... | t | ...
+*/
+
+
+-- type t2 = subrange [0,10] of int;
const bound: int = 1000;
diff --git a/tests/source/test5.scade b/tests/source/test5.scade
index 1de390d..566acf0 100644
--- a/tests/source/test5.scade
+++ b/tests/source/test5.scade
@@ -1,8 +1,8 @@
-node test(i: int) returns(probe a, b, c: int; exit: bool)
+node test(i: int) returns(probe a, probe b, probe c: int; exit: bool)
let
b = 0 -> pre a;
a = if b > 4 then 0 else b + 1;
- c = 0;
+ c = i;
exit = i >= 10;
tel