Project

General

Profile

Revision 4f3cc9f3

View differences:

ex3.smt2
54 54
  (and (= speed.__speed_2 (and speed.second (not speed.beacon)))
55 55
       (= speed.__speed_1 (and speed.beacon (not speed.second)))
56 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.__COUNTER_1_x)
57
       (COUNTER_init 0 speed.incr (or speed.beacon speed.second) false speed.diff speed.ni_4.COUNTER.__COUNTER_1_x)
58 58
       (= speed.__speed_7 speed.__speed_6_c)
59 59
       (= speed.__speed_8 (ite speed.__speed_7 (< speed.diff 0)
60 60
                             (<= speed.diff (- 10))))
61
       (= speed.late 0)
61
       (= speed.late false)
62 62
       (= speed.__speed_4 speed.__speed_3_c)
63 63
       (= speed.__speed_5 (ite speed.__speed_4 (> speed.diff 0)
64 64
                             (>= speed.diff 10)))
65
       (= speed.early 0)
65
       (= speed.early false)
66 66
       (= speed.__speed_6_x speed.late)
67 67
       (= speed.__speed_3_x speed.early)
68 68
  )
......
73 73
  (and (= speed.__speed_2 (and speed.second (not speed.beacon)))
74 74
       (= speed.__speed_1 (and speed.beacon (not speed.second)))
75 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.__COUNTER_1_c speed.__COUNTER_1_x)
76
       (COUNTER_step 0 speed.incr (or speed.beacon speed.second) false speed.diff speed.ni_4.COUNTER.__COUNTER_1_c speed.ni_4.COUNTER.__COUNTER_1_x)
77 77
       (= speed.__speed_7 speed.__speed_6_c)
78 78
       (= speed.__speed_8 (ite speed.__speed_7 (< speed.diff 0)
79 79
                             (<= speed.diff (- 10))))
......
95 95
(declare-var top.__top_1_c Bool)
96 96
(declare-var top.ni_1.speed.__speed_3_c Bool)
97 97
(declare-var top.ni_1.speed.__speed_6_c Bool)
98
(declare-var top.ni_1.ni_4.COUNTER.__COUNTER_1_c Int)
98
(declare-var top.ni_1.speed.ni_4.COUNTER.__COUNTER_1_c Int)
99 99
(declare-var top.__top_1_x Bool)
100 100
(declare-var top.ni_1.speed.__speed_3_x Bool)
101 101
(declare-var top.ni_1.speed.__speed_6_x Bool)
102
(declare-var top.ni_1.ni_4.COUNTER.__COUNTER_1_x Int)
102
(declare-var top.ni_1.speed.ni_4.COUNTER.__COUNTER_1_x Int)
103 103
(declare-var top.early Bool)
104 104
(declare-var top.late Bool)
105 105
(declare-rel top_init (Bool Bool Bool Bool Bool Bool Int))
106 106
(declare-rel top_step (Bool Bool Bool Bool Bool Bool Int Bool Bool Bool Int))
107 107

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

  
116 116
(rule (=> 
117
  (and (speed_step top.beacon top.second top.late top.early top.__speed_3_c top.__speed_6_c top.ni_1.ni_4.COUNTER.__COUNTER_1_c top.__speed_3_x top.__speed_6_x top.ni_1.ni_4.COUNTER.__COUNTER_1_x)
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.speed.ni_4.COUNTER.__COUNTER_1_c top.ni_1.speed.__speed_3_x top.ni_1.speed.__speed_6_x top.ni_1.speed.ni_4.COUNTER.__COUNTER_1_x)
118 118
       (= top.OK (or (not top.__top_1_c) (not top.late)))
119 119
       (= top.__top_1_x top.early)
120 120
  )
121
  (top_step top.beacon top.second top.OK 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_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)
121
  (top_step top.beacon top.second top.OK top.__top_1_c top.ni_1.speed.__speed_3_c top.ni_1.speed.__speed_6_c top.ni_1.speed.ni_4.COUNTER.__COUNTER_1_c top.__top_1_x top.ni_1.speed.__speed_3_x top.ni_1.speed.__speed_6_x top.ni_1.speed.ni_4.COUNTER.__COUNTER_1_x)
122 122
))
123 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_1_x top.ni_1.speed.__speed_3_x top.ni_1.speed.__speed_6_x top.ni_1.speed.ni_4.COUNTER.__COUNTER_1_x)
133
  )
134
  (MAIN top.__top_1_x top.ni_1.speed.__speed_3_x top.ni_1.speed.__speed_6_x top.ni_1.speed.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_1_c top.ni_1.speed.__speed_3_c top.ni_1.speed.__speed_6_c top.ni_1.speed.ni_4.COUNTER.__COUNTER_1_c dummy)
141
       (top_step top.beacon top.second top.OK top.__top_1_c top.ni_1.speed.__speed_3_c top.ni_1.speed.__speed_6_c top.ni_1.speed.ni_4.COUNTER.__COUNTER_1_c top.__top_1_x top.ni_1.speed.__speed_3_x top.ni_1.speed.__speed_6_x top.ni_1.speed.ni_4.COUNTER.__COUNTER_1_x)
142
  )
143
  (MAIN top.__top_1_x top.ni_1.speed.__speed_3_x top.ni_1.speed.__speed_6_x top.ni_1.speed.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_1_c top.ni_1.speed.__speed_3_c top.ni_1.speed.__speed_6_c top.ni_1.speed.ni_4.COUNTER.__COUNTER_1_c))
151
  ERR))
152
(query ERR)
ex3_correct.smt2
4 4
(declare-var COUNTER.X Bool)
5 5
(declare-var COUNTER.reset Bool)
6 6
(declare-var COUNTER.C Int)
7
(declare-var COUNTER.COUNTER.__COUNTER_1_c Int)
8
(declare-var COUNTER.COUNTER.__COUNTER_1_x Int)
7
(declare-var COUNTER.__COUNTER_1_c Int)
8
(declare-var COUNTER.__COUNTER_1_x Int)
9 9
(declare-var COUNTER.PC Int)
10 10
(declare-rel COUNTER_init (Int Int Bool Bool Int Int))
11 11
(declare-rel COUNTER_step (Int Int Bool Bool Int Int Int))
......
14 14
  (and (= COUNTER.PC COUNTER.init)
15 15
       (= COUNTER.C (ite COUNTER.reset COUNTER.init
16 16
                       (ite COUNTER.X (+ COUNTER.PC COUNTER.incr) COUNTER.PC)))
17
       (= COUNTER.COUNTER.__COUNTER_1_x COUNTER.C)
17
       (= COUNTER.__COUNTER_1_x COUNTER.C)
18 18
  )
19
  (COUNTER_init COUNTER.init COUNTER.incr COUNTER.X COUNTER.reset COUNTER.C COUNTER.COUNTER.__COUNTER_1_x)
19
  (COUNTER_init COUNTER.init COUNTER.incr COUNTER.X COUNTER.reset COUNTER.C COUNTER.__COUNTER_1_x)
20 20
))
21 21

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

  
31 31
; speed
......
33 33
(declare-var speed.second Bool)
34 34
(declare-var speed.late Bool)
35 35
(declare-var speed.early Bool)
36
(declare-var speed.speed.__speed_3_c Bool)
37
(declare-var speed.speed.__speed_6_c Bool)
36
(declare-var speed.__speed_3_c Bool)
37
(declare-var speed.__speed_6_c Bool)
38 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)
39
(declare-var speed.__speed_3_x Bool)
40
(declare-var speed.__speed_6_x Bool)
41 41
(declare-var speed.ni_4.COUNTER.__COUNTER_1_x Int)
42 42
(declare-var speed.__speed_1 Bool)
43 43
(declare-var speed.__speed_2 Bool)
......
55 55
       (= speed.__speed_1 (and speed.beacon (not speed.second)))
56 56
       (= speed.incr (ite speed.__speed_1 1 (ite speed.__speed_2 2 0)))
57 57
       (COUNTER_init 0 speed.incr (or speed.beacon speed.second) false speed.diff speed.ni_4.COUNTER.__COUNTER_1_x)
58
       (= speed.__speed_7 speed.speed.__speed_6_c)
58
       (= speed.__speed_7 speed.__speed_6_c)
59 59
       (= speed.__speed_8 (ite speed.__speed_7 (< speed.diff 0)
60 60
                             (<= speed.diff (- 10))))
61 61
       (= speed.late false)
62
       (= speed.__speed_4 speed.speed.__speed_3_c)
62
       (= speed.__speed_4 speed.__speed_3_c)
63 63
       (= speed.__speed_5 (ite speed.__speed_4 (> speed.diff 0)
64 64
                             (>= speed.diff 10)))
65 65
       (= speed.early false)
66
       (= speed.speed.__speed_6_x speed.late)
67
       (= speed.speed.__speed_3_x speed.early)
66
       (= speed.__speed_6_x speed.late)
67
       (= speed.__speed_3_x speed.early)
68 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)
69
  (speed_init speed.beacon speed.second speed.late speed.early speed.__speed_3_x speed.__speed_6_x speed.ni_4.COUNTER.__COUNTER_1_x)
70 70
))
71 71

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

  
91 91
; top
92 92
(declare-var top.beacon Bool)
93 93
(declare-var top.second Bool)
94 94
(declare-var top.OK Bool)
95
(declare-var top.top.__top_1_c Bool)
95
(declare-var top.__top_1_c Bool)
96 96
(declare-var top.ni_1.speed.__speed_3_c Bool)
97 97
(declare-var top.ni_1.speed.__speed_6_c Bool)
98 98
(declare-var top.ni_1.ni_4.COUNTER.__COUNTER_1_c Int)
99
(declare-var top.top.__top_1_x Bool)
99
(declare-var top.__top_1_x Bool)
100 100
(declare-var top.ni_1.speed.__speed_3_x Bool)
101 101
(declare-var top.ni_1.speed.__speed_6_x Bool)
102 102
(declare-var top.ni_1.ni_4.COUNTER.__COUNTER_1_x Int)
......
108 108
(rule (=> 
109 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 110
       (= top.OK true)
111
       (= top.top.__top_1_x top.early)
111
       (= top.__top_1_x top.early)
112 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)
113
  (top_init top.beacon top.second top.OK 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 114
))
115 115

  
116 116
(rule (=> 
117 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.__top_1_c) (not top.late)))
119
       (= top.top.__top_1_x top.early)
118
       (= top.OK (or (not top.__top_1_c) (not top.late)))
119
       (= top.__top_1_x top.early)
120 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)
121
  (top_step top.beacon top.second top.OK 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_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 122
))
123 123

  
124 124
; Collecting semantics with main node top
......
129 129
(rule INIT_STATE)
130 130
(rule (=> 
131 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)
132
       (top_init top.beacon top.second top.OK 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 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)
134
  (MAIN 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 135
))
136 136

  
137 137
; Inductive def
138 138
(declare-var dummy Bool)
139 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)
140
  (and (MAIN 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_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_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 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)
143
  (MAIN 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 144
))
145 145

  
146 146
; Property def
147 147
(declare-rel ERR ())
148 148
(rule (=> 
149 149
  (and (not (= top.OK true))
150
       (MAIN top.top.__top_1_c top.ni_1.speed.__speed_3_c
150
       (MAIN top.__top_1_c top.ni_1.speed.__speed_3_c
151 151
       top.ni_1.speed.__speed_6_c top.ni_1.ni_4.COUNTER.__COUNTER_1_c top.OK))
152 152
  ERR))
153 153
(query ERR)
src/horn_backend.ml
28 28
let pp_var fmt id = Format.pp_print_string fmt id.var_id
29 29

  
30 30

  
31
let prefix prefix x = if prefix = "" then x else prefix ^ "." ^ x 
32
let rename_machine p = rename (fun n -> prefix p n)
31
let concat prefix x = if prefix = "" then x else prefix ^ "." ^ x 
32
let rename f = (fun v -> {v with var_id = f v.var_id } )
33
let rename_machine p = rename (fun n -> concat p n)
33 34
let rename_machine_list p = List.map (rename_machine p)
34 35
    
35
let rename f = (fun v -> {v with var_id = f v.var_id } )
36 36
let rename_current =  rename (fun n -> n ^ "_c")
37 37
let rename_current_list = List.map rename_current
38 38
let rename_next = rename (fun n -> n ^ "_x")
......
43 43
  List.find (fun m  -> m.mname.node_id = node_name) machines 
44 44

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

  
86 86
(* Used to print boolean constants *)
87 87
let pp_horn_tag fmt t =
88
  pp_print_string fmt (if t = tag_true then "1" else if t = tag_false then "0" else t)
88
  pp_print_string fmt (if t = tag_true then "true" else if t = tag_false then "false" else t)
89 89

  
90 90
(* Prints a constant value *)
91 91
let rec pp_horn_const fmt c =
......
110 110
    | StateVar v    ->
111 111
      if Types.is_array_type v.var_type
112 112
      then assert false 
113
      else pp_var fmt ((if is_lhs then rename_next else rename_current) self v)
113
      else pp_var fmt (rename_machine self ((if is_lhs then rename_next else rename_current) (* self *) v))
114 114
    | Fun (n, vl)   -> Format.fprintf fmt "%a" (Basic_library.pp_horn n (pp_horn_val self pp_var)) vl
115 115

  
116 116
(* Prints a [value] indexed by the suffix list [loop_vars] *)
......
161 161
	    (Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m))) (List.map (fun v -> LocalVar v) outputs)
162 162
	    (Utils.pp_final_char_if_non_empty " " outputs)
163 163
	    (Utils.fprintf_list ~sep:" " pp_var) (
164
  	      (rename_next_list m.mname.node_id (full_memory_vars machines i target_machine)) 
164
  	      rename_machine_list (concat m.mname.node_id i) (rename_next_list (* concat m.mname.node_id i *) (full_memory_vars machines target_machine)) 
165 165
	     )
166 166
	  else
167 167
	    Format.fprintf fmt "(%s_step %a%t%a%t%a)"
......
172 172
	      (Utils.pp_final_char_if_non_empty " " outputs)
173 173
	      (Utils.fprintf_list ~sep:" " pp_var) (
174 174

  
175
	      (rename_current_list m.mname.node_id (full_memory_vars machines i target_machine)) @ 
176
	      (rename_next_list m.mname.node_id (full_memory_vars machines i target_machine)) 
175
	      (rename_machine_list (concat m.mname.node_id i) (rename_current_list (* concat m.mname.node_id i *) (full_memory_vars machines target_machine))) @ 
176
		(rename_machine_list (concat m.mname.node_id i) (rename_next_list (* concat m.mname.node_id i *) (full_memory_vars machines target_machine))) 
177 177
	       )
178 178
	    
179 179
	     end
......
280 280
    Format.fprintf fmt "; Collecting semantics with main node %s@.@." node;
281 281
    (* We print the types of the main node "memory tree" TODO: add the output *)
282 282
    let main_memory_next = 
283
      (rename_next_list machine.mname.node_id (full_memory_vars machines "" machine)) 
283
      (rename_next_list (* machine.mname.node_id *) (full_memory_vars machines machine)) 
284 284
    in
285 285
    let main_memory_current = 
286
      (rename_current_list machine.mname.node_id (full_memory_vars machines "" machine)) 
286
      (rename_current_list (* machine.mname.node_id *) (full_memory_vars machines machine)) 
287 287
    in
288 288
    Format.fprintf fmt "(declare-rel MAIN (%a Bool))@."
289 289
      (Utils.fprintf_list ~sep:" " pp_type) 
src/main_lustre_compiler.ml
258 258
      let fmt = Format.std_formatter in
259 259
      Horn_backend.translate fmt basename normalized_prog machine_code
260 260
    end
261
    | _ -> assert false
261 262
  in
262 263
  report ~level:1 (fun fmt -> fprintf fmt ".. done !@ @]@.");
263 264
  (* We stop the process here *)

Also available in: Unified diff