Project

General

Profile

Revision faa5e5c5

View differences:

ex3.smt2
1
; COUNTER
2
(declare_var COUNTER.init Int)
3
(declare_var COUNTER.incr Int)
4
(declare_var COUNTER.X Bool)
5
(declare_var COUNTER.reset Bool)
6
(declare_var COUNTER.C Int)
7
(declare_var COUNTER.COUNTER.__COUNTER_1_c Int)
8
(declare_var COUNTER.COUNTER.__COUNTER_1_x Int)
9
(declare_var COUNTER.PC Int)
10
(declare-rel COUNTER_reset (Int Int Bool Bool Int Int))
11
(declare-rel COUNTER_step (Int Int Bool Bool Int Int Int))
12

  
13
(rule (=> 
14
  (and (= COUNTER.PC COUNTER.init)
15
       (= COUNTER.C (ite COUNTER.reset COUNTER.init
16
                       (ite COUNTER.X (+ COUNTER.PC COUNTER.incr) COUNTER.PC)))
17
       (= COUNTER.__COUNTER_1_x COUNTER.C)
18
  )
19
  (COUNTER_init COUNTER.init COUNTER.incr COUNTER.X COUNTER.reset COUNTER.C COUNTER.COUNTER.__COUNTER_1_x)
20
))
21

  
22
(rule (=> 
23
  (and (= COUNTER.PC COUNTER.__COUNTER_1_c)
24
       (= COUNTER.C (ite COUNTER.reset COUNTER.init
25
                       (ite COUNTER.X (+ COUNTER.PC COUNTER.incr) COUNTER.PC)))
26
       (= COUNTER.__COUNTER_1_x COUNTER.C)
27
  )
28
  (COUNTER_step COUNTER.init COUNTER.incr COUNTER.X COUNTER.reset COUNTER.C COUNTER.COUNTER.__COUNTER_1_c COUNTER.COUNTER.__COUNTER_1_x)
29
))
30

  
31
; speed
32
(declare_var speed.beacon Bool)
33
(declare_var speed.second Bool)
34
(declare_var speed.late Bool)
35
(declare_var speed.early Bool)
36
(declare_var speed.speed.__speed_3_c Bool)
37
(declare_var speed.speed.__speed_6_c Bool)
38
(declare_var speed.ni_4.COUNTER.__COUNTER_1_c Int)
39
(declare_var speed.speed.__speed_3_x Bool)
40
(declare_var speed.speed.__speed_6_x Bool)
41
(declare_var speed.ni_4.COUNTER.__COUNTER_1_x Int)
42
(declare_var speed.__speed_1 Bool)
43
(declare_var speed.__speed_2 Bool)
44
(declare_var speed.__speed_4 Bool)
45
(declare_var speed.__speed_5 Bool)
46
(declare_var speed.__speed_7 Bool)
47
(declare_var speed.__speed_8 Bool)
48
(declare_var speed.diff Int)
49
(declare_var speed.incr Int)
50
(declare-rel speed_reset (Bool Bool Bool Bool Bool Bool Int))
51
(declare-rel speed_step (Bool Bool Bool Bool Bool Bool Int Bool Bool Int))
52

  
53
(rule (=> 
54
  (and (= speed.__speed_2 (and speed.second (not speed.beacon)))
55
       (= speed.__speed_1 (and speed.beacon (not speed.second)))
56
       (= speed.incr (ite speed.__speed_1 1 (ite speed.__speed_2 2 0)))
57
       (COUNTER_init 0 speed.incr ((or speed.beacon speed.second)) 0 speed.diff speed.ni_4.COUNTER.__COUNTER_1_x)
58
       (= speed.__speed_7 speed.__speed_6_c)
59
       (= speed.__speed_8 (ite speed.__speed_7 (< speed.diff 0)
60
                             (<= speed.diff (- 10))))
61
       (= speed.late 0)
62
       (= speed.__speed_4 speed.__speed_3_c)
63
       (= speed.__speed_5 (ite speed.__speed_4 (> speed.diff 0)
64
                             (>= speed.diff 10)))
65
       (= speed.early 0)
66
       (= speed.__speed_6_x speed.late)
67
       (= speed.__speed_3_x speed.early)
68
  )
69
  (speed_init speed.beacon speed.second speed.late speed.early speed.speed.__speed_3_x speed.speed.__speed_6_x speed.ni_4.COUNTER.__COUNTER_1_x)
70
))
71

  
72
(rule (=> 
73
  (and (= speed.__speed_2 (and speed.second (not speed.beacon)))
74
       (= speed.__speed_1 (and speed.beacon (not speed.second)))
75
       (= speed.incr (ite speed.__speed_1 1 (ite speed.__speed_2 2 0)))
76
       (COUNTER_step 0 speed.incr ((or speed.beacon speed.second)) 0 speed.diff speed.ni_4.COUNTER.__COUNTER_1_c speed.ni_4.COUNTER.__COUNTER_1_x)
77
       (= speed.__speed_7 speed.__speed_6_c)
78
       (= speed.__speed_8 (ite speed.__speed_7 (< speed.diff 0)
79
                             (<= speed.diff (- 10))))
80
       (= speed.late speed.__speed_8)
81
       (= speed.__speed_4 speed.__speed_3_c)
82
       (= speed.__speed_5 (ite speed.__speed_4 (> speed.diff 0)
83
                             (>= speed.diff 10)))
84
       (= speed.early speed.__speed_5)
85
       (= speed.__speed_6_x speed.late)
86
       (= speed.__speed_3_x speed.early)
87
  )
88
  (speed_step speed.beacon speed.second speed.late speed.early speed.speed.__speed_3_c speed.speed.__speed_6_c speed.ni_4.COUNTER.__COUNTER_1_c speed.speed.__speed_3_x speed.speed.__speed_6_x speed.ni_4.COUNTER.__COUNTER_1_x)
89
))
90

  
91
; top
92
(declare_var top.beacon Bool)
93
(declare_var top.second Bool)
94
(declare_var top.OK Bool)
95
(declare_var top.top.__top_1_c Bool)
96
(declare_var top.ni_1.speed.__speed_3_c Bool)
97
(declare_var top.ni_1.speed.__speed_6_c Bool)
98
(declare_var top.ni_1.ni_4.COUNTER.__COUNTER_1_c Int)
99
(declare_var top.top.__top_1_x Bool)
100
(declare_var top.ni_1.speed.__speed_3_x Bool)
101
(declare_var top.ni_1.speed.__speed_6_x Bool)
102
(declare_var top.ni_1.ni_4.COUNTER.__COUNTER_1_x Int)
103
(declare_var top.early Bool)
104
(declare_var top.late Bool)
105
(declare-rel top_reset (Bool Bool Bool Bool Bool Bool Int))
106
(declare-rel top_step (Bool Bool Bool Bool Bool Bool Int Bool Bool Bool Int))
107

  
108
(rule (=> 
109
  (and (speed_init top.beacon top.second top.late top.early top.ni_1.speed.__speed_3_x top.ni_1.speed.__speed_6_x top.ni_1.ni_4.COUNTER.__COUNTER_1_x)
110
       (= top.OK 1)
111
       (= top.__top_1_x top.early)
112
  )
113
  (top_init top.beacon top.second top.OK top.top.__top_1_x top.ni_1.speed.__speed_3_x top.ni_1.speed.__speed_6_x top.ni_1.ni_4.COUNTER.__COUNTER_1_x)
114
))
115

  
116
(rule (=> 
117
  (and (speed_step top.beacon top.second top.late top.early top.ni_1.speed.__speed_3_c top.ni_1.speed.__speed_6_c top.ni_1.ni_4.COUNTER.__COUNTER_1_c top.ni_1.speed.__speed_3_x top.ni_1.speed.__speed_6_x top.ni_1.ni_4.COUNTER.__COUNTER_1_x)
118
       (= top.OK (or (not top.__top_1_c) (not top.late)))
119
       (= top.__top_1_x top.early)
120
  )
121
  (top_step top.beacon top.second top.OK top.top.__top_1_c top.ni_1.speed.__speed_3_c top.ni_1.speed.__speed_6_c top.ni_1.ni_4.COUNTER.__COUNTER_1_c top.top.__top_1_x top.ni_1.speed.__speed_3_x top.ni_1.speed.__speed_6_x top.ni_1.ni_4.COUNTER.__COUNTER_1_x)
122
))
123

  
124
; Collecting semantics with main node top
125

  
126
(declare-rel MAIN (Bool Bool Bool Int Bool))
127
; Initial set
128
(declare-rel INIT_STATE ())
129
(rule INIT_STATE)
130
(rule (=> 
131
  (and INIT_STATE
132
       (top_init top.beacon top.second top.OK top.top.__top_1_x top.ni_1.speed.__speed_3_x top.ni_1.speed.__speed_6_x top.ni_1.ni_4.COUNTER.__COUNTER_1_x)
133
  )
134
  (MAIN top.top.__top_1_x top.ni_1.speed.__speed_3_x top.ni_1.speed.__speed_6_x top.ni_1.ni_4.COUNTER.__COUNTER_1_x top.OK)
135
))
136

  
137
; Inductive def
138
(declare-var dummy Bool)
139
(rule (=> 
140
  (and (MAIN top.top.__top_1_c top.ni_1.speed.__speed_3_c top.ni_1.speed.__speed_6_c top.ni_1.ni_4.COUNTER.__COUNTER_1_c dummy)
141
       (top_step top.beacon top.second top.OK top.top.__top_1_c top.ni_1.speed.__speed_3_c top.ni_1.speed.__speed_6_c top.ni_1.ni_4.COUNTER.__COUNTER_1_c top.top.__top_1_x top.ni_1.speed.__speed_3_x top.ni_1.speed.__speed_6_x top.ni_1.ni_4.COUNTER.__COUNTER_1_x)
142
  )
143
  (MAIN top.top.__top_1_x top.ni_1.speed.__speed_3_x top.ni_1.speed.__speed_6_x top.ni_1.ni_4.COUNTER.__COUNTER_1_x top.OK)
144
))
145

  
146
; Property def
147
(declare-rel ERR ())
148
(rule (=> 
149
  (and (not (= top.OK true))
150
       (MAIN top.top.__top_1_c top.ni_1.speed.__speed_3_c top.ni_1.speed.__speed_6_c top.ni_1.ni_4.COUNTER.__COUNTER_1_c))
151
  ERR))
152
(query ERR)
src/horn_backend.ml
27 27

  
28 28
let pp_var fmt id = Format.pp_print_string fmt id.var_id
29 29

  
30
let pp_instr machine_name fmt i =
31
  Format.fprintf fmt "(xxx)"
32 30

  
33 31
let rename f = (fun v -> {v with var_id = f v.var_id } )
34
let rename_current machine_name =  rename (fun n -> machine_name ^ "." ^ n ^ "_c")
35
let rename_current_list machine_name = List.map (rename_current machine_name)
36
let rename_next machine_name = rename (fun n -> machine_name ^ "." ^ n ^ "_x")
37
let rename_next_list machine_name = List.map (rename_next machine_name)
38
let rename_machine machine_name = rename (fun n -> machine_name ^ "." ^ n)
39
let rename_machine_list machine_name = List.map (rename_machine machine_name)
40

  
41
let full_memory_vars machine instance =
42
  (rename_current_list machine.mname.node_id machine.mmemory) @
43
    (rename_next_list machine.mname.node_id machine.mmemory)
44

  
45
let machine_vars m = 
32
let rename_current prefix =  rename (fun n -> prefix ^ "." ^ n ^ "_c")
33
let rename_current_list prefix = List.map (rename_current prefix)
34
let rename_next prefix = rename (fun n -> prefix ^ "." ^ n ^ "_x")
35
let rename_next_list prefix = List.map (rename_next prefix)
36
let rename_machine prefix = rename (fun n -> prefix ^ "." ^ n)
37
let rename_machine_list prefix = List.map (rename_machine prefix)
38

  
39
let get_machine machines node_name = 
40
  List.find (fun m  -> m.mname.node_id = node_name) machines 
41

  
42
let full_memory_vars machines prefix machine =
43
  let rec aux prefix m =
44
    let pref x = if prefix = "" then x else prefix ^ "." ^ x in 
45
    (rename_machine_list (pref m.mname.node_id) m.mmemory) @
46
      List.fold_left (fun accu (id, (n, _)) -> 
47
	let name = node_name n in 
48
	if name = "_arrow" then accu else
49
	  let machine_n = get_machine machines name in
50
	( aux (pref id) machine_n ) @ accu
51
      ) [] (m.minstances) 
52
  in
53
  aux prefix machine
54

  
55
let machine_vars machines m = 
56
    (rename_machine_list m.mname.node_id m.mstep.step_inputs)@
57
    (rename_machine_list m.mname.node_id m.mstep.step_outputs)@
58
    (rename_current_list m.mname.node_id (full_memory_vars machines "" m)) @ 
59
    (rename_next_list m.mname.node_id (full_memory_vars machines "" m)) 
60

  
61
let step_vars machines m = 
62
    (rename_machine_list m.mname.node_id m.mstep.step_inputs)@
63
    (rename_machine_list m.mname.node_id m.mstep.step_outputs)@
64
    (rename_current_list m.mname.node_id (full_memory_vars machines "" m)) @ 
65
    (rename_next_list m.mname.node_id (full_memory_vars machines "" m)) 
66

  
67
let init_vars machines m = 
46 68
    (rename_machine_list m.mname.node_id m.mstep.step_inputs)@
47 69
    (rename_machine_list m.mname.node_id m.mstep.step_outputs)@
48
  full_memory_vars m ()
70
    (rename_next_list m.mname.node_id (full_memory_vars machines "" m)) 
49 71

  
50 72
  
51 73
(********************************************************************************************)
......
130 152
      | name, _, _ ->  
131 153
	begin
132 154
	  let target_machine = List.find (fun m  -> m.mname.node_id = name) machines in
133
	  Format.fprintf fmt "(%s_%s %a%t%a%t%a)"
155
	  if init then
156
	  Format.fprintf fmt "(%s_init %a%t%a%t%a)"
134 157
	    (node_name n) 
135
	    (if init then "init" else "step")
136 158
	    (Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m))) inputs
137 159
	    (Utils.pp_final_char_if_non_empty " " inputs) 
138 160
	    (Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m))) (List.map (fun v -> LocalVar v) outputs)
139
	       (Utils.pp_final_char_if_non_empty " " outputs)
140
	    (Utils.fprintf_list ~sep:" " pp_var) (full_memory_vars target_machine i)
161
	    (Utils.pp_final_char_if_non_empty " " outputs)
162
	    (Utils.fprintf_list ~sep:" " pp_var) (
163
  	      (rename_next_list m.mname.node_id (full_memory_vars machines i target_machine)) 
164
	     )
165
	  else
166
	    Format.fprintf fmt "(%s_step %a%t%a%t%a)"
167
	    (node_name n) 
168
	      (Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m))) inputs
169
	      (Utils.pp_final_char_if_non_empty " " inputs) 
170
	      (Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m))) (List.map (fun v -> LocalVar v) outputs)
171
	      (Utils.pp_final_char_if_non_empty " " outputs)
172
	      (Utils.fprintf_list ~sep:" " pp_var) (
173

  
174
	      (rename_current_list m.mname.node_id (full_memory_vars machines i target_machine)) @ 
175
	      (rename_next_list m.mname.node_id (full_memory_vars machines i target_machine)) 
176
	       )
141 177
	    
142 178
	     end
143 179
    end
......
209 245
   Format.fprintf fmt "; %s@." m.mname.node_id;
210 246
   (* Printing variables *)
211 247
   Utils.fprintf_list ~sep:"@." pp_decl_var fmt 
212
     ((machine_vars m)@(rename_machine_list m.mname.node_id m.mstep.step_locals));
248
     ((machine_vars machines m)@(rename_machine_list m.mname.node_id m.mstep.step_locals));
213 249
   Format.pp_print_newline fmt ();
214 250
   (* Declaring predicate *)
215 251
   Format.fprintf fmt "(declare-rel %a (%a))@."
216 252
     pp_machine_reset_name m.mname.node_id
217
     (Utils.fprintf_list ~sep:" " pp_type) (List.map (fun v -> v.var_type) m.mmemory);
253
     (Utils.fprintf_list ~sep:" " pp_type) (List.map (fun v -> v.var_type) (init_vars machines m));
218 254
   
219 255
   Format.fprintf fmt "(declare-rel %a (%a))@."
220 256
     pp_machine_step_name m.mname.node_id
221
     (Utils.fprintf_list ~sep:" " pp_type) (List.map (fun v -> v.var_type) (machine_vars m));
257
     (Utils.fprintf_list ~sep:" " pp_type) (List.map (fun v -> v.var_type) (step_vars machines m));
222 258
   Format.pp_print_newline fmt ();
223 259

  
224 260
   Format.fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>%a@]@ )@ (%s_init %a)@]@.))@.@."
225 261
     (Utils.fprintf_list ~sep:"@ " (pp_instr true m.mname.node_id)) m.mstep.step_instrs
226 262
     m.mname.node_id
227
     (Utils.fprintf_list ~sep:" " pp_var) (rename_next_list m.mname.node_id m.mmemory);
263
     (Utils.fprintf_list ~sep:" " pp_var) (init_vars machines m);
264

  
228 265

  
229 266
   Format.fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>%a@]@ )@ (%s_step %a)@]@.))@.@."
230 267
     (Utils.fprintf_list ~sep:"@ " (pp_instr false m.mname.node_id)) m.mstep.step_instrs
231 268
     m.mname.node_id
232
     (Utils.fprintf_list ~sep:" " pp_var) (machine_vars m);
269
     (Utils.fprintf_list ~sep:" " pp_var) (step_vars machines m);
233 270
   
234 271
()
235 272
  )
236 273

  
237
let main_print fmt = ()
274
let main_print machines fmt = 
275
if !Options.main_node <> "" then 
276
  begin
277
    let node = !Options.main_node in
278
    let machine = get_machine machines node in
279
    Format.fprintf fmt "; Collecting semantics with main node %s@.@." node;
280
    (* We print the types of the main node "memory tree" TODO: add the output *)
281
    let main_memory_next = 
282
      (rename_next_list machine.mname.node_id (full_memory_vars machines "" machine)) 
283
    in
284
    let main_memory_current = 
285
      (rename_current_list machine.mname.node_id (full_memory_vars machines "" machine)) 
286
    in
287
    Format.fprintf fmt "(declare-rel MAIN (%a Bool))@."
288
      (Utils.fprintf_list ~sep:" " pp_type) 
289
      (List.map (fun v -> v.var_type) main_memory_next);
290
    
291
    Format.fprintf fmt "; Initial set@.";
292
    Format.fprintf fmt "(declare-rel INIT_STATE ())@.";
293
    Format.fprintf fmt "(rule INIT_STATE)@.";
294
    Format.fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>INIT_STATE@ (@[<v 0>%s_init %a@])@]@ )@ (MAIN %a top.OK)@]@.))@.@."
295
      node
296
      (Utils.fprintf_list ~sep:" " pp_var) (init_vars machines machine)
297
      (Utils.fprintf_list ~sep:" " pp_var) main_memory_next;
298

  
299
    Format.fprintf fmt "; Inductive def@.";
300
    Format.fprintf fmt "(declare-var dummy Bool)@.";
301
    Format.fprintf fmt 
302
      "@[<v 2>(rule (=> @ (and @[<v 0>(MAIN %a dummy)@ (@[<v 0>%s_step %a@])@]@ )@ (MAIN %a top.OK)@]@.))@.@."
303
      (Utils.fprintf_list ~sep:" " pp_var) main_memory_current
304
      node
305
      (Utils.fprintf_list ~sep:" " pp_var) (step_vars machines machine)
306
      (Utils.fprintf_list ~sep:" " pp_var) main_memory_next;
307

  
308
    Format.fprintf fmt "; Property def@.";
309
    Format.fprintf fmt "(declare-rel ERR ())@.";
310
    Format.fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>(not (= top.OK true))@ (MAIN %a)@])@ ERR))@."
311
      (Utils.fprintf_list ~sep:" " pp_var) main_memory_current;
312
    Format.fprintf fmt "(query ERR)@.";
313

  
314
    ()
315
end
316

  
238 317

  
239 318
let translate fmt basename prog machines =
240 319
  List.iter (print_machine machines fmt) (List.rev machines);
241
  main_print fmt 
320
  main_print machines fmt 
242 321

  
243 322

  
244 323
(* Local Variables: *)

Also available in: Unified diff