Project

General

Profile

Revision 9f77bff7 src/backends/Horn/horn_backend_common.ml

View differences:

src/backends/Horn/horn_backend_common.ml
69 69

  
70 70
let local_memory_vars machines machine =
71 71
  rename_machine_list machine.mname.node_id machine.mmemory
72
    
72

  
73 73
let instances_memory_vars ?(without_arrow=false) machines machine =
74 74
  let rec aux fst prefix m =
75 75
    (
......
81 81
      List.fold_left (fun accu (id, (n, _)) ->
82 82
	let name = node_name n in
83 83
	if without_arrow && name = "_arrow" then
84
	  accu 
84
	  accu
85 85
	else
86 86
	  let machine_n = get_machine machines name in
87
	  ( aux false (concat prefix 
87
	  ( aux false (concat prefix
88 88
			 (if fst then id else concat m.mname.node_id id))
89 89
	      machine_n ) @ accu
90 90
      ) [] (m.minstances)
......
101 101

  
102 102
let step_vars machines m =
103 103
  (inout_vars machines m)
104
  @ (rename_current_list (full_memory_vars machines m)) 
104
  @ (rename_current_list (full_memory_vars machines m))
105 105
  @ (rename_next_list (full_memory_vars machines m))
106 106

  
107 107
let step_vars_m_x machines m =
108 108
  (inout_vars machines m)
109
  @ (rename_mid_list (full_memory_vars machines m)) 
109
  @ (rename_mid_list (full_memory_vars machines m))
110 110
  @ (rename_next_list (full_memory_vars machines m))
111 111

  
112 112
let reset_vars machines m =
113
  (rename_current_list (full_memory_vars machines m)) 
113
  (rename_current_list (full_memory_vars machines m))
114 114
  @ (rename_mid_list (full_memory_vars machines m))
115 115

  
116 116

  

Also available in: Unified diff