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
|
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^"/"^b.act_id^"."^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
let env = E.apply_f env init_f in
Format.printf "Init formula: %a@.@." Formula_printer.print_expr init_f;
Format.printf "Cycle formula: %a@.@." Formula_printer.print_expr f;
{ 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 -> env -> env *)
let cycle st i =
let i' = E.apply_cl i st.cl in
i', pass_cycle st.all_vars i'
(*
do_prog : prog -> id -> st
*)
let do_prog p root =
let st = init_state p root in
let _, acc = cycle st st.env in
let rec step acc n =
if n < 10 then begin
Format.printf "Step %d: %a@." n E.print_all acc;
let i', j = cycle st acc in
Format.printf " -> %a@." E.print_all i';
Format.printf "Pass cycle: %a@.@." E.print_all j;
let acc' = (if n >= 7 then E.widen else E.join) acc j in
step acc' (n+1)
end
in
step acc 0
end
|
