Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / tools / zustre / zustre_analyze.ml @ 5778dd5e

History | View | Annotate | Download (5.09 KB)

1
(* This module takes a main node (reset and step) and a property. It assumes
2
   that the system is properly defined and check that the property is valid. 
3

    
4
   When valid, it returns a set of local invariants. Otherwise, it returns a cex
5
   expressed as a sequence of input values.
6

    
7
*)
8
open Lustre_types
9
open Machine_code_types
10
open Machine_code_common
11
open Zustre_common
12
open Zustre_data
13

    
14
let check machines node =
15

    
16
  let machine = get_machine machines node in
17

    
18
  (* Declaring collecting semantics *)
19
  
20
  let main_output =
21
    rename_machine_list machine.mname.node_id machine.mstep.step_outputs
22
  in
23
  let main_output_dummy =
24
    rename_machine_list ("dummy" ^ machine.mname.node_id) machine.mstep.step_outputs
25
  in
26
  let main_memory_next =
27
    (rename_next_list (* machine.mname.node_id *) (full_memory_vars machines machine)) @
28
      main_output
29
  in
30
  let main_memory_current =
31
    (rename_current_list (* machine.mname.node_id *) (full_memory_vars machines machine)) @
32
      main_output_dummy
33
  in
34

    
35
  (* TODO: push/pop? donner un nom different par instance pour les garder dans le buffer ?
36
     Faut-il declarer les "rel" dans la hashtbl ?
37
  *)
38
  let decl_main = decl_rel "MAIN" main_memory_next in
39

    
40
  
41
  
42
  (* Init case *)
43
  let decl_init = decl_rel "INIT_STATE" [] in
44

    
45
  (* rule INIT_STATE *)
46
  let _ = add_rule [] (Z3.Expr.mk_app
47
			 !ctx
48
			 decl_init
49
			 []
50
  )  in
51
  
52
  let horn_head = 
53
    Z3.Expr.mk_app
54
      !ctx
55
      decl_main
56
      (List.map horn_var_to_expr main_memory_next)
57
  in
58
  (* Special case when the main node is stateless *)
59
  let _ =
60
    if Machine_code_common.is_stateless machine then
61
      begin
62
	
63
	(* Initial set: One Step(m,x)  -- Stateless node  *)	
64
     	(* rule => (INIT_STATE and step(mid, next)) MAIN(next) *)
65

    
66
	(* Note that vars here contains main_memory_next *)
67
	let vars = step_vars_m_x machines machine in
68
	
69
	let horn_body =
70
	  Z3.Boolean.mk_and !ctx
71
	    [
72
	      Z3.Expr.mk_app !ctx decl_init [];
73
	      Z3.Expr.mk_app !ctx
74
		(get_fdecl (machine_stateless_name node))
75
		(List.map horn_var_to_expr vars) 
76
	    ]
77
	in
78
	add_rule vars (Z3.Boolean.mk_implies !ctx horn_body horn_head)
79
	  
80
	  
81
      end
82
    else
83
      begin
84
	(* Initial set: Reset(c,m) + One Step(m,x) @. *)
85
	(* rule => (INIT_STATE and reset(mid) and step(mid, next)) MAIN(next) *)
86
	let horn_body =
87
	  Z3.Boolean.mk_and !ctx
88
	    [
89
	      Z3.Expr.mk_app !ctx decl_init [];
90
	      Z3.Expr.mk_app !ctx
91
		(get_fdecl (machine_reset_name node))
92
		(List.map horn_var_to_expr (reset_vars machines machine));
93
	      Z3.Expr.mk_app !ctx
94
		(get_fdecl (machine_step_name node))
95
		(List.map horn_var_to_expr (step_vars_m_x machines machine))
96
	    ]
97
	in
98

    
99
	(* Vars contains all vars: in_out, current, mid, neXt memories *)
100
	let vars = step_vars_c_m_x machines machine in
101
	add_rule vars (Z3.Boolean.mk_implies !ctx horn_body horn_head)
102
	  
103
	  
104
      end
105
  in
106
  
107
  let step_name = 
108
    if Machine_code_common.is_stateless machine then 
109
      machine_stateless_name
110
    else
111
      machine_step_name
112
  in
113
  
114
  (* ; Inductive def@. *)
115

    
116
  List.iter (fun x -> ignore (decl_var x)) main_output_dummy;
117
  
118
  (* (Utils.fprintf_list ~sep:" " (fun fmt v -> fprintf fmt "%a@." pp_decl_var v)) fmt main_output_dummy; *)
119

    
120
  (* fprintf fmt *)
121
  (*   "@[<v 2>(rule (=> @ (and @[<v 0>(MAIN %a)@ (@[<v 0>%a %a@])@]@ )@ (MAIN %a)@]@.))@.@." *)
122
  (*   (Utils.fprintf_list ~sep:" " (pp_horn_var machine)) main_memory_current *)
123
  (*   step_name node *)
124
  (*   (Utils.fprintf_list ~sep:" " (pp_horn_var machine)) (step_vars machines machine) *)
125
  
126
  
127
  let horn_head = 
128
    Z3.Expr.mk_app
129
      !ctx
130
      decl_main
131
      (List.map horn_var_to_expr main_memory_next)
132
  in
133
  let horn_body =
134
    Z3.Boolean.mk_and !ctx
135
      [
136
	Z3.Expr.mk_app !ctx decl_main (List.map horn_var_to_expr main_memory_current);
137
	Z3.Expr.mk_app !ctx (get_fdecl (step_name node)) (List.map horn_var_to_expr (step_vars machines machine))
138
      ]
139
  in
140
  let _ =
141
    add_rule []  (Z3.Boolean.mk_implies !ctx horn_body horn_head)
142
      
143
  in
144

    
145

    
146
  (* Property def *)
147
  let decl_err = decl_rel "ERR" [] in
148

    
149
  let prop =
150
    Z3.Boolean.mk_and !ctx (List.map horn_var_to_expr main_output)
151
  in
152
  let not_prop =
153
    Z3.Boolean.mk_not !ctx prop
154
  in
155
  add_rule main_memory_next (Z3.Boolean.mk_implies !ctx
156
	      (
157
		Z3.Boolean.mk_and !ctx
158
		  [not_prop;
159
		   Z3.Expr.mk_app !ctx decl_main (List.map horn_var_to_expr main_memory_next);
160
		  ]
161
	      )
162
	      (Z3.Expr.mk_app !ctx decl_err []))
163
  ;
164
  
165
      (* fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>(not %a)@ (MAIN %a)@])@ ERR))@." *)
166
      (*   (pp_conj (pp_horn_var machine)) main_output *)
167
      (*   (Utils.fprintf_list ~sep:" " (pp_horn_var machine)) main_memory_next *)
168
      (*   ; *)
169
      (*  if !Options.horn_query then fprintf fmt "(query ERR)@." *)
170

    
171
      (* Debug instructions *)
172
  let rules_expr = Z3.Fixedpoint.get_rules !fp in
173
  Format.eprintf "@[<v 2>Registered rules:@ %a@ @]@."
174
    (Utils.fprintf_list ~sep:"@ "
175
       (fun fmt e -> Format.pp_print_string fmt (Z3.Expr.to_string e)) )
176
    rules_expr;
177

    
178
  
179
  let res_status = Z3.Fixedpoint.query_r !fp [decl_err] in
180

    
181
  Format.eprintf "Status: %s@." (Z3.Solver.string_of_status res_status)
182
  
183
(* Local Variables: *)
184
(* compile-command:"make -C ../.." *)
185
(* End: *)