Project

General

Profile

Download (2.16 KB) Statistics
| Branch: | Tag: | Revision:
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
  
(30-30/67)