diff options
| -rw-r--r-- | abstract/abs_interp.ml | 4 | ||||
| -rw-r--r-- | abstract/abs_interp_edd.ml | 12 | ||||
| -rw-r--r-- | abstract/transform.ml | 2 | ||||
| -rw-r--r-- | main.ml | 5 | ||||
| -rw-r--r-- | tests/source/rfollow.scade | 6 |
5 files changed, 23 insertions, 6 deletions
diff --git a/abstract/abs_interp.ml b/abstract/abs_interp.ml index a401f60..c3b2d79 100644 --- a/abstract/abs_interp.ml +++ b/abstract/abs_interp.ml @@ -11,6 +11,7 @@ type cmdline_opt = { widen_delay : int; disjunct : (id -> bool); verbose_ci : bool; + vverbose_ci : bool; } @@ -354,7 +355,8 @@ end = struct *) let cycle st cl env = let env_f = apply_cl env cl in - (*Format.printf "{{ %a ->@.%a }}@." print_dd env print_dd env_f;*) + if st.opt.vverbose_ci then + Format.printf "{{ %a ->@.%a }}@." print_dd env print_dd env_f; dd_pass_cycle st env_f diff --git a/abstract/abs_interp_edd.ml b/abstract/abs_interp_edd.ml index 510bf93..6e45240 100644 --- a/abstract/abs_interp_edd.ml +++ b/abstract/abs_interp_edd.ml @@ -929,6 +929,10 @@ end = struct let dc = pass_cycle e d2 in let y = edd_join_star_widen e x dc in + if e.opt.vverbose_ci then + Format.printf "d2 %a@. dc %a@. y %a@." + edd_print d2 edd_print dc edd_print y; + if e.opt.verbose_ci then Format.printf " -> %a@." edd_print y; @@ -945,7 +949,13 @@ end = struct let f i = let i = edd_meet path i in let i' = edd_meet i path_target in - let q = edd_join start (pass_cycle e (edd_apply_cl i' e.cl)) in + let j = edd_apply_cl i' e.cl in + + if e.opt.vverbose_ci then + Format.printf "i %a@.i' %a@.j %a@." + edd_print i edd_print i' edd_print j; + + let q = edd_join start (pass_cycle e j) in edd_meet path q in diff --git a/abstract/transform.ml b/abstract/transform.ml index ff2374e..7ae54ad 100644 --- a/abstract/transform.ml +++ b/abstract/transform.ml @@ -494,5 +494,5 @@ and guarantees_of_prog rp = consts = I.consts rp; } in - g_of_scope td rp.root_scope "" (BConst true) + g_of_scope td rp.root_scope (clock_scope_here rp.root_scope) (BConst true) @@ -31,6 +31,7 @@ let ai_no_time_scopes = ref "" let ai_init_scopes = ref "" let ai_disj_v = ref "" let ai_vci = ref false +let ai_vvci = ref false let ifile = ref "" let usage = "usage: analyzer [options] file.scade" @@ -46,6 +47,7 @@ let options = [ "--ai-itv-edd", Arg.Set ai_itv_edd, "Do abstract analysis using intervals and EDD disjunction domain."; "--ai-rel-edd", Arg.Set ai_rel_edd, "Do abstract analysis using Apron and EDD disjunction domain."; "--ai-vci", Arg.Set ai_vci, "Verbose chaotic iterations (show state at each iteration)"; + "--ai-vvci", Arg.Set ai_vvci, "Very verbose chaotic iterations (show everything all the time)"; "--wd", Arg.Set_int ai_widen_delay, "Widening delay in abstract analysis of loops (default: 3)."; "--root", Arg.Set_string ai_root, "Root node for abstract analysis (default: test)."; "--no-time", Arg.Set_string ai_no_time_scopes, "Scopes for which not to introduce a 'time' variable in analysis."; @@ -117,7 +119,8 @@ let () = let opt = { widen_delay = !ai_widen_delay; disjunct = disj; - verbose_ci = !ai_vci + verbose_ci = !ai_vci; + vverbose_ci = !ai_vvci; } in if !ai_itv then AI_Itv.do_prog opt rp; diff --git a/tests/source/rfollow.scade b/tests/source/rfollow.scade index 6ee1558..c62c90d 100644 --- a/tests/source/rfollow.scade +++ b/tests/source/rfollow.scade @@ -1,14 +1,16 @@ node follow(a: real) returns (probe f: real) var probe pf: real; + prop: bool; let assume h1: a >= 0. and a <= 1.; - guarantee g1: f >= 0. and f <= 1.; - guarantee g2: pf >= 0. and pf <= 1.; pf = 0. -> pre f; f = (pf + a) / 2.0; + prop = (f >= 0 and f <= 1.); + + guarantee g1: (true -> pre prop) and prop; tel |