|
1
|
open Lustre_types
|
|
2
|
|
|
3
|
(* Create a node that checks whether two other nodes have the same output *)
|
|
4
|
|
|
5
|
let check_eq nd1 nd2 =
|
|
6
|
let check_nd = Corelang.copy_node nd1 in (* to keep the type info *)
|
|
7
|
let loc = Location.dummy_loc in
|
|
8
|
let ok_var =
|
|
9
|
Corelang.mkvar_decl loc ~orig:false
|
|
10
|
("__OK",
|
|
11
|
Corelang.mktyp loc Tydec_bool,
|
|
12
|
Corelang.mkclock loc Ckdec_any,
|
|
13
|
false,
|
|
14
|
None,
|
|
15
|
None)
|
|
16
|
in
|
|
17
|
let check_nd = { check_nd with
|
|
18
|
node_id = "check_eq_" ^ nd1.node_id ^ "_" ^ nd2.node_id;
|
|
19
|
node_outputs = [ok_var];
|
|
20
|
}
|
|
21
|
in
|
|
22
|
check_nd
|
|
23
|
|
|
24
|
(*
|
|
25
|
|
|
26
|
TODO:
|
|
27
|
|
|
28
|
construire
|
|
29
|
|
|
30
|
les variables temporaires pour les outputs de l'un et de l'autre
|
|
31
|
les statements d'appels de nodes
|
|
32
|
ok = and (o1 = o2)
|
|
33
|
|
|
34
|
et on ajoute le contrat guarantee ok
|
|
35
|
in
|
|
36
|
check_nd
|
|
37
|
|
|
38
|
*)
|
|
39
|
|
|
40
|
(* (\* Build the contract: guarentee output = orig_node(input) *\)
|
|
41
|
* let expr_of_vars vl =
|
|
42
|
* Corelang.expr_of_expr_list loc
|
|
43
|
* (List.map Corelang.expr_of_vdecl vl)
|
|
44
|
* in
|
|
45
|
* let local_outputs = List.map (fun v -> { (Corelang.copy_var_decl v) with var_id = v.var_id ^ "_local" } ) copy_nd.node_outputs in
|
|
46
|
* let input_e = expr_of_vars copy_nd.node_inputs in
|
|
47
|
* let call_orig_e =
|
|
48
|
* Corelang.mkexpr loc (Expr_appl (orig_nd.node_id, input_e , None)) in
|
|
49
|
* let build_orig_outputs =
|
|
50
|
* Eq (
|
|
51
|
* Corelang.mkeq loc
|
|
52
|
* (List.map (fun v -> v.var_id) local_outputs, call_orig_e)) in
|
|
53
|
* let eq_expr = Corelang.expr_of_expr_list loc (
|
|
54
|
* List.map2 (fun v1 v2 ->
|
|
55
|
* let args = expr_of_vars [v1;v2] in
|
|
56
|
* Corelang.mkexpr loc (Expr_appl ("=", args, None)))
|
|
57
|
* copy_nd.node_outputs local_outputs
|
|
58
|
* )
|
|
59
|
* in
|
|
60
|
* let contract = {
|
|
61
|
* consts = [];
|
|
62
|
* locals = local_outputs;
|
|
63
|
* stmts = [build_orig_outputs];
|
|
64
|
* assume = [];
|
|
65
|
* guarantees = [Corelang.mkeexpr loc eq_expr];
|
|
66
|
* modes = [];
|
|
67
|
* imports = [];
|
|
68
|
* spec_loc = loc;
|
|
69
|
*
|
|
70
|
* }
|
|
71
|
* in *)
|
|
72
|
|