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
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
|
open Ast
open Util
open Ast_util
open Formula
open Interpret (* used for constant evaluation ! *)
(* Transform SCADE program to logical formula. *)
(* node * prefix * equations *)
type scope = id * id * eqn ext list
type transform_data = {
p : Ast.prog;
consts : I.value VarMap.t;
root_scope : scope;
(* future : the automata state *)
}
let f_and a b =
if a = BConst true then b
else if b = BConst true then a
else BAnd(a, b)
(* f_of_nexpr :
transform_data -> (string, string) -> (num_expr list -> 'a) -> expr -> 'a
*)
let rec f_of_nexpr td (node, prefix) where expr =
let sub = f_of_nexpr td (node, prefix) in
match fst expr with
(* ident *)
| AST_identifier(id, _) -> where [NIdent (node^"/"^id)]
| AST_idconst(id, _) ->
begin let x = VarMap.find ("cst/"^id) td.consts in
try where [NIntConst (I.as_int x)]
with _ -> try where [NRealConst (I.as_real x)]
with _ -> error "Invalid data for supposedly numerical constant."
end
(* numerical *)
| AST_int_const(i, _) -> where [NIntConst(int_of_string i)]
| AST_real_const(r, _) -> where [NRealConst(float_of_string r)]
| AST_unary(op, e) ->
sub (function
| [x] -> where [NUnary(op, x)]
| _ -> invalid_arity "Unary operator") e
| AST_binary(op, a, b) ->
sub (function
| [x] ->
sub (function
| [y] -> where [NBinary(op, x, y)]
| _ -> invalid_arity "binary_operator") b
| _ -> invalid_arity "binary operator") a
(* temporal *)
| AST_pre(_, id) -> where [NIdent id]
| AST_arrow(a, b) ->
BOr(
BAnd(BRel(AST_EQ, NIdent(node^"/"^prefix^"time"), NIntConst 0),
sub where a),
BAnd(BRel(AST_GE, NIdent(node^"/"^prefix^"time"), NIntConst 1),
sub where b))
(* other *)
| AST_if(c, a, b) ->
BOr(
BAnd(f_of_bexpr td (node, prefix) c, sub where a),
BAnd(BNot(f_of_bexpr td (node, prefix) c), sub where b))
| AST_instance ((f, _), args, nid) ->
let (n, _) = find_node_decl td.p f in
where (List.map (fun (_, id, _) -> NIdent (node^"/"^nid^"/"^id)) n.ret)
(* boolean values treated as integers *)
| _ ->
BOr(
BAnd ((f_of_bexpr td (node, prefix) expr), where [NIntConst 1]),
BAnd (BNot(f_of_bexpr td (node, prefix) expr), where [NIntConst 0])
)
(* f_of_expr :
transform_data -> (string, string) -> expr -> bool_expr
*)
and f_of_bexpr td (node, prefix) expr =
let sub = f_of_bexpr td (node, prefix) in
match fst expr with
| AST_bool_const b -> BConst b
| AST_binary_bool(AST_AND, a, b) -> BAnd(sub a, sub b)
| AST_binary_bool(AST_OR, a, b) -> BOr(sub a, sub b)
| AST_not(a) -> BNot(sub a)
| AST_binary_rel(rel, a, b) ->
f_of_nexpr td (node, prefix)
(function
| [x] -> f_of_nexpr td (node, prefix)
(function
| [y] -> BRel(rel, x, y)
| _ -> invalid_arity "boolean relation") b
| _ -> invalid_arity "boolean relation")
a
| _ -> loc_error (snd expr) error "Invalid type : expected boolean value"
and f_of_scope active td (node, prefix, eqs) =
let expr_eq e eq =
let instance_eq (_, id, eqs, args) =
let eq = f_of_scope active td (node^"/"^id, "", eqs) in
if active then
List.fold_left (fun eq ((_,argname,_), expr) ->
let eq_arg = f_of_nexpr td (node, prefix) (function
| [v] -> BRel(AST_EQ, NIdent(node^"/"^id^"/"^argname), v)
| _ -> invalid_arity "in argument")
expr
in f_and eq eq_arg)
eq args
else
eq
in
let eq = List.fold_left (fun x i -> f_and (instance_eq i) x)
eq (extract_instances td.p e)
in
let pre_expr (id, expr) =
if active then
f_of_nexpr td (node, prefix) (function
| [v] -> BRel(AST_EQ, NIdent("N"^id), v)
| _ -> invalid_arity "pre on complex data not supported")
expr
else
BRel(AST_EQ, NIdent("N"^id), NIdent id)
in
List.fold_left (fun x i -> f_and (pre_expr i) x)
eq (extract_pre e)
in
let do_eq eq = match fst eq with
| AST_assign(ids, e) ->
let assign_eq =
if active then
f_of_nexpr td (node, prefix)
(fun vs ->
let rels =
List.map2 (fun (id, _) v -> BRel(AST_EQ, NIdent (node^"/"^id), v))
ids vs
in
list_fold_op f_and rels)
e
else
BConst true
in
expr_eq e assign_eq
| AST_assume (_, e) ->
let assume_eq =
if active then
f_of_bexpr td (node, prefix) e
else
BConst true
in
expr_eq e assume_eq
| AST_guarantee (_, e) ->
expr_eq e (BConst true)
| AST_activate (b, _) ->
let rec cond_eq = function
| AST_activate_body b -> BConst true
| AST_activate_if(c, a, b) ->
f_and (expr_eq c (BConst true))
(f_and (cond_eq a) (cond_eq b))
in
let rec do_tree_act = function
| AST_activate_body b ->
f_of_scope true td (node, b.act_id^".", b.body)
| AST_activate_if(c, a, b) ->
BOr(
f_and (f_of_bexpr td (node, prefix) c)
(f_and (do_tree_act a) (do_tree_inact b)),
f_and (BNot(f_of_bexpr td (node, prefix) c))
(f_and (do_tree_act b) (do_tree_inact a))
)
and do_tree_inact = function
| AST_activate_body b ->
f_of_scope false td (node, b.act_id^".", b.body)
| 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 _ -> not_implemented "f_of_scope do_eq automaton"
in
let time_incr_eq =
if active then
BRel(AST_EQ, NIdent("N"^node^"/"^prefix^"time"),
NBinary(AST_PLUS, NIntConst 1, NIdent(node^"/"^prefix^"time")))
else
BRel(AST_EQ,
NIdent("N"^node^"/"^prefix^"time"),
NIdent(node^"/"^prefix^"time"))
in
List.fold_left f_and
time_incr_eq
(List.map do_eq eqs)
and f_of_prog p root =
let td = {
root_scope = get_root_scope p root;
p = p;
consts = I.consts p root;
} in
f_of_scope true td td.root_scope
let rec init_f_of_scope p (node, prefix, eqs) =
let expr_eq e =
let instance_eq (_, id, eqs, args) =
init_f_of_scope p (node^"/"^id, "", eqs)
in
List.fold_left (fun x i -> f_and (instance_eq i) x)
(BConst true) (extract_instances 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 ->
init_f_of_scope p (node, b.act_id^".", b.body)
| 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 _ -> not_implemented "f_of_scope do_eq automaton"
in
let time_eq =
BRel(AST_EQ,
NIdent(node^"/"^prefix^"time"),
NIntConst 0)
in
List.fold_left f_and time_eq (List.map do_eq eqs)
and init_f_of_prog p root =
init_f_of_scope p (get_root_scope p root)
|
