Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / tools / zustre / zustre_cex.ml @ 7d77632f

History | View | Annotate | Download (7.82 KB)

1
(* Rebuilding Cex *)
2
(* In order to properly rebuild the Cex, one needsthe unsliced model. Otherwise
3
   some input or state variables are removed.
4

    
5
*)
6

    
7

    
8
open Lustre_types
9
open Machine_code_types
10
(* open Machine_code_common *)
11
open Zustre_common
12

    
13
open Zustre_data
14

    
15
let get_conjuncts e =
16
  assert (Z3.Boolean.is_bool e);
17
  if Z3.Boolean.is_and e then
18
    Z3.Expr.get_args e
19
  else
20
    [e]
21

    
22
let build_cex machine machines decl_err =
23
  (* Recovering associated top machine (to build full traces) and property *) 
24
  (* TODO: for example extract top node and ok prop. We may have multiple
25
     MAIN/ERR loaded at the same time. Each of them should be assocaited with a
26
     CEX/Inv/Timeout.*)
27
  
28
  let node_id = machine.mname.node_id in
29

    
30
  let cex = match Z3.Fixedpoint.get_answer !fp with Some e -> e | None -> raise Not_found in
31
  (* Original code used the function Z3.Fixedpoint.get_ground_sat_answer !fp *)
32

    
33
  let stats = Z3.Fixedpoint.get_statistics !fp in
34
  
35
  let conjuncts = List.rev (get_conjuncts cex) in
36

    
37
  Format.eprintf "cex: %s@.%i conjuncts: @[<v 0>%a@]@."
38
    (Z3.Expr.to_string cex)
39
    (List.length conjuncts)
40
    (Utils.fprintf_list ~sep:"@ " (fun fmt e -> Format.fprintf fmt "%s" (Z3.Expr.to_string e))) conjuncts;
41

    
42
  (* Checking size *)
43
  let inputs = machine.mstep.step_inputs in
44
  let nb_inputs = List.length inputs in
45
  let outputs = machine.mstep.step_outputs in
46
  let nb_outputs = List.length inputs in
47
  let nb_mems = List.length (full_memory_vars machines machine) in
48
  
49
  let main, funs =
50
    List.fold_left (fun (main, funs) conj ->
51
    (* Filtering out non MAIN decls *)
52
    let func_decl = Z3.Expr.get_func_decl conj in
53
    let node_name = Z3.Symbol.get_string (Z3.FuncDecl.get_name func_decl) in
54
    (* Focusing only on MAIN_nodeid predicates *)
55
    if node_name = "MAIN_" ^ node_id then
56
      (* Extracting info *)
57
      (* Recall that MAIN args are in@mems@out *)
58
      let args = Z3.Expr.get_args conj in
59
      if List.length args = 1 + nb_inputs + nb_mems + nb_outputs then
60
	let id = Z3.Arithmetic.Integer.get_int (List.hd args) in
61
	let input_values = Utils.List.extract args 1 (1 + nb_inputs) in
62
	let output_values = Utils.List.extract args (1+nb_inputs+nb_mems) (1 + nb_inputs + nb_mems + nb_outputs) in
63
	(id, (input_values, output_values))::main, funs
64
      else
65
	assert false
66
    else
67
      let reg = Str.regexp_string "[a-z]*_step" in
68
      if Str.string_match reg node_name 0 then (
69
	let actual_name = Str.matched_group 0 node_name in
70
	Format.eprintf "Name %s@." actual_name;
71
	main, funs
72
      )
73
      else (
74
	Format.eprintf "pas matché %s@." node_name;
75
	main, funs
76
      )
77
    ) ((* main*) [],(* other functions *) []) conjuncts
78
  in
79
  let main = List.sort (fun (id1, _) (id2, _) -> compare id1 id2) main in
80
  List.iter (
81
    fun (id, expr) ->
82
      Format.eprintf "Id %i: %a@."
83
	(id)
84
	(Utils.fprintf_list ~sep:", "
85
	   (fun fmt e -> Format.fprintf fmt "%s" (Z3.Expr.to_string e)))
86
	(fst expr)
87
  ) main;		    
88
   (* let ground_val = List.map (fun e -> Z3.Expr.to_string e) (Z3.Expr.get_args conj) in *)
89

    
90
   (* We recover the Zustre XML format, projecting each cex on each input/output
91
      signal *)
92
  let in_signals, out_signals =
93
    List.fold_right (
94
      fun (id, (sigs_in, sigs_out)) (res_sigs_in, res_sigs_out) ->
95
	let add l1 l2 = List.map2 (fun e1 e2 -> fst e2, ((id, e1)::(snd e2))) l1 l2 in
96
	let sigs_in_id = add sigs_in res_sigs_in in
97
	let sigs_out_id = add sigs_out res_sigs_out in
98
	sigs_in_id, sigs_out_id
99
    ) main (List.map (fun v -> v, []) inputs, List.map (fun v -> v, []) outputs)
100
  in
101

    
102
  (* let _ = List.mapi (fun k conj -> *)
103
  (*   (\* k-iterate *\) *)
104
  (*   let ground_val = List.map (fun e -> Z3.Expr.to_string e) (Z3.Expr.get_args conj) in *)
105
  (*   let func_decl = Z3.Expr.get_func_decl conj in *)
106
  (*   if !debug then Format.eprintf "FuncDecl %s@." (Z3.FuncDecl.to_string func_decl); *)
107
  (*   let node_name = Z3.Symbol.get_string (Z3.FuncDecl.get_name func_decl) in *)
108

    
109
   
110
  (*   if !debug then Format.eprintf "Node %s, args %a@." node_name  (Utils.fprintf_list ~sep:", " (Format.pp_print_string)) ground_val; *)
111
    
112
  (*   () *)
113
  (*   (\*  ground_pair = [] *)
114
  (*           try: *)
115
  (*               ground_vars = pred_dict[node_name] *)
116
  (*               ground_pair = zip(ground_vars,ground_val) *)
117
  (*               if "_reset" in node_name: *)
118
  (*                   # this condition is to remove the node nodename_reset added by lustrec *)
119
  (*                   continue *)
120
  (*                   # node = node_name.split("_reset")[0] *)
121
  (*                   # cex_dict.update({node:{k:ground_pair}}) *)
122
  (*               elif "_step" in node_name: *)
123
  (*                   node = node_name.split("_step")[0] *)
124
  (*                   try: *)
125
  (*                       # case in which we already have the node in dict *)
126
  (*                       d = cex_dict[node] *)
127
  (*                       max_key = max(k for k, v in d.iteritems() if v != 0) #get the maximum key value and add 1 *)
128
  (*                       d.update({(max_key+1):ground_pair}) *)
129
  (*                   except Exception as e: *)
130
  (*                       self._log.warning("Adding a new node cex " + str(e)) *)
131
  (*                       cex_dict.update({node:{k:ground_pair}}) *)
132
  (*               else: *)
133
  (*                   node = node_name *)
134
  (*                   try: *)
135
  (*                       d = cex_dict[node] *)
136
  (*                       max_key = max(k for k, v in d.iteritems() if v != 0) #get the maximum key value and add 1 *)
137
  (*                       d.update({(max_key+1):ground_pair}) *)
138
  (*                   except Exception as e: *)
139
  (*                       if node not in ["MAIN", "ERR"]: *)
140
  (*                           self._log.warning("Adding a new node cex " + str(e)) *)
141
  (*                           cex_dict.update({node:{k:ground_pair}}) *)
142
  (*           except Exception as e: *)
143
  (*               self._log.warning("Problem with getting a node name: " + str(e)) *)
144
  (*   *\) *)
145
  (* ) conjuncts in *)
146
  (*   let rules_expr = Z3.Fixedpoint.get_rules !fp in *)
147
  (*   if !debug then *)
148
  (*     Format.eprintf "@[<v 2>Registered rules:@ %a@ @]@." *)
149
  (* 	(Utils.fprintf_list ~sep:"@ " *)
150
  (*   	   (fun fmt e -> Format.pp_print_string fmt (Z3.Expr.to_string e)) ) *)
151
  (* 	rules_expr; *)
152
  (*   if !debug then *)
153
  (*     Format.eprintf "FP help: %s@." (Z3.Fixedpoint.get_help !fp); *)
154

    
155
  let stats_entries =   Z3.Statistics.get_entries stats in
156
  (* List.iter (fun e -> Format.eprintf "%s@.@?" *)
157
  (*   (Z3.Statistics.Entry.to_string e) *)
158
    
159
  (* ) stats_entries; *)
160
  let json : Yojson.json =
161
    `Assoc [
162
      "Results",
163
      `Assoc [
164
	"Property",
165
	`Assoc [
166
	  "name", `String node_id;
167
	  "date", `String (Utils.get_date ());
168
	  "query", `Assoc ["unit", `String "sec";
169
			   "value", `Float (
170
			     let time_opt = Z3.Statistics.get stats "time.spacer.solve" in
171
			     match time_opt with None -> -1.
172
			     | Some f -> Z3.Statistics.Entry.get_float f)
173
			  ];
174
	  "answer", `String "CEX";
175
	  "counterexample",
176
	  `Assoc [
177
	    node_id, `Assoc
178
	      (
179
		List.map (fun (vardecl, values) ->
180
		  vardecl.var_id,
181
		  `Assoc [
182
		    "type", (let _ = Format.fprintf Format.str_formatter "%a" Printers.pp_var_type vardecl in
183
			    let s = Format.flush_str_formatter () in
184
			    `String s);
185
		    "values", `Assoc (List.map (fun (id, v) ->
186
		      string_of_int id, `String (Z3.Expr.to_string v))
187
					values)
188
		  ]   
189
		) in_signals
190
	      )
191
	  ]
192
	]
193
      ]
194
     ]
195
  in
196
  Format.eprintf "JSON: %s@."
197
    (Yojson.to_string json);
198
  ()
199
  (* Results *)
200
  (*   Property *)
201
  (*   Date *)
202
  (*   Query time *)
203
  (*   Answer CEX *)
204
  (*   Counterexample *)
205
  (*     Node name="nodeid" *)
206
  (*       Stream name="opt.x" type="unk" *)
207
  (* 	  Value instant="0">xxx</Value>		       *)
208
  (* () *)
209
	(* ordered_by_signal = self.reorder(cex_dict) *)
210
        (* return self.mk_cex_xml(ordered_by_signal) *)
211

    
212
(* Local Variables: *)
213
(* compile-command:"make -C ../.. lustrev" *)
214
(* End: *)
215

    
216