1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
|
open Ast
open Ast_util
open Formula
open Util
open Environment_domain
module I (E : ENVIRONMENT_DOMAIN) : sig
type st
val do_prog : prog -> id -> unit
end = struct
type st = {
p : prog;
root_scope : scope;
all_vars : var_def list;
env : E.t;
f : bool_expr;
cl : conslist;
}
let node_vars p f nid =
let (n, _) = find_node_decl p f in
List.map (fun (p, id, t) -> p, nid^"/"^id, t)
(n.args @ n.ret @ n.var)
(*
extract_all_vars : prog -> scope -> var_decl 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
*)
let rec extract_all_vars p (node, prefix, eqs) =
let vars_of_expr e =
List.flatten
(List.map
(fun (f, id, eqs, args) ->
node_vars p f (node^"/"^id) @
extract_all_vars p (node^"/"^id, "", eqs))
(extract_instances p e))
@
List.flatten
(List.map
(fun (id, _) -> [false, id, AST_TINT; false, "N"^id, AST_TINT])
(* TODO : type of pre value ? *)
(extract_pre e))
in
let vars_of_eq e = match fst e with
| AST_assign(_, e) | AST_assume(_, e) | AST_guarantee(_, e) -> vars_of_expr e
| AST_activate (b, _) ->
let rec do_branch = function
| AST_activate_body b ->
List.map (fun (p, id, t) -> p, node^"/"^id, t) b.act_locals
@
extract_all_vars p (node, b.act_id^".", b.body)
| 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"
in
(false, node^"/"^prefix^"time", AST_TINT)::
(false, "N"^node^"/"^prefix^"time", AST_TINT)::
(List.flatten (List.map vars_of_eq eqs))
(* init state *)
let init_state p root =
let root_scope = get_root_scope p root in
let f = Formula.eliminate_not (Transform.f_of_prog p root) in
let cl = Formula.conslist_of_f f in
let all_vars = node_vars p root "" @ extract_all_vars p root_scope in
let env = List.fold_left
(fun env (_, id, ty) ->
E.addvar env id (ty = AST_TREAL))
E.init
all_vars
in
let init_f = Transform.init_f_of_prog p root in
Format.printf "Init formula: %a@.@." Formula_printer.print_expr init_f;
Format.printf "Cycle formula: %a@.@." Formula_printer.print_expr f;
Format.printf "Vars: %a@.@." (Ast_printer.print_list Ast_printer.print_var_decl ", ") all_vars;
let env = E.apply_f env init_f in
{ p; root_scope; f; cl; all_vars; env }
(*
pass_cycle : var_def list -> E.t -> E.t
Does :
- x <- Nx, for all x
- ignore x for all x such that Nx does not exist
*)
let pass_cycle vars e =
let tr_assigns = List.fold_left
(fun q (_, id, _) ->
if id.[0] = 'N' then
(String.sub id 1 (String.length id - 1), NIdent id)::q
else
q)
[] vars
in
let e = E.assign e tr_assigns in
let forget_vars = List.map (fun (_, id, _) -> id)
(List.filter
(fun (_, id, _) ->
not (List.exists (fun (_, id2, _) -> id2 = "N"^id) vars))
vars) in
let e = List.fold_left E.forgetvar e forget_vars in
e
(* cycle : st -> cl -> env -> env *)
let cycle st cl i =
E.apply_cl (pass_cycle st.all_vars i) cl
(*
loop : st -> cl -> env -> env -> env
*)
let loop st cycle_cl pnew stay =
let pnew = E.apply_cl pnew cycle_cl in
Format.printf "Loop @[<hv>%a@]@.New @[<hv>%a@]@.Stay @[<hv>%a@]@."
Formula_printer.print_conslist cycle_cl
E.print_all pnew E.print_all stay;
let add_stay = cycle st cycle_cl pnew in
let acc0 = E.join stay add_stay in
let fsharp i =
Format.printf "Acc @[<hv>%a@]@." E.print_all i;
let j = cycle st cycle_cl i in
E.join acc0 j
in
let widen_delay = 10 in
let rec iter n i =
let i' =
if n < widen_delay
then E.join i (fsharp i)
else E.widen i (fsharp i)
in
if E.eq i i' then i else iter (n+1) i'
in
let x = iter 0 acc0 in
fix E.eq fsharp x (* decreasing iteration *)
(*
do_prog : prog -> id -> unit
*)
let do_prog p root =
let st = init_state p root in
let pnew = st.env in
let stay = loop st st.cl pnew (E.vbottom pnew) in
Format.printf "@[<hov>Final stay %a@]@."
E.print_all stay;
Format.printf "Probes:@[<hov>";
List.iter (fun (p, id, _) ->
if p then Format.printf "@ %a ∊ %a,"
Formula_printer.print_id id
E.print_itv (E.var_itv stay id))
st.all_vars;
Format.printf "@]@."
end
|
