Project

General

Profile

Revision 587cdc0d

View differences:

src/horn_backend.ml
244 244

  
245 245

  
246 246
(**************************************************************)
247
    
247
   
248
let is_stateless m = m.minstances = [] && m.mmemory = [] 
249

  
248 250
(* Print the machine m: 
249 251
   two functions: m_init and m_step
250 252
   - m_init is a predicate over m memories
......
266 268
	 (rename_machine_list m.mname.node_id m.mstep.step_locals));
267 269
   Format.pp_print_newline fmt ();
268 270

  
269
   let stateless = m.minstances = [] && m.mmemory = [] in
270 271
   
271
   if stateless then
272
   
273
   if is_stateless m then
272 274
     begin
273 275
       (* Declaring single predicate *)
274 276
       Format.fprintf fmt "(declare-rel %a (%a))@."
......
348 350
      (rename_current_list (* machine.mname.node_id *) (full_memory_vars machines machine)) @
349 351
      main_output_dummy
350 352
    in
353

  
354
    (* Special case when the main node is stateless *)
355
    let init_name, step_name = 
356
      if is_stateless machine then
357
	pp_machine_stateless_name, pp_machine_stateless_name
358
      else
359
	pp_machine_init_name, pp_machine_step_name
360
    in
361
    
351 362
    Format.fprintf fmt "(declare-rel MAIN (%a))@."
352 363
      (Utils.fprintf_list ~sep:" " pp_type) 
353 364
      (List.map (fun v -> v.var_type) main_memory_next);
......
356 367
    Format.fprintf fmt "(declare-rel INIT_STATE ())@.";
357 368
    Format.fprintf fmt "(rule INIT_STATE)@.";
358 369
    Format.fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>INIT_STATE@ (@[<v 0>%a %a@])@]@ )@ (MAIN %a)@]@.))@.@."
359
      pp_machine_init_name node
370
      init_name node
360 371
      (Utils.fprintf_list ~sep:" " pp_var) (init_vars machines machine)
361 372
      (Utils.fprintf_list ~sep:" " pp_var) main_memory_next ;
362 373

  
......
365 376
    Format.fprintf fmt 
366 377
      "@[<v 2>(rule (=> @ (and @[<v 0>(MAIN %a)@ (@[<v 0>%a %a@])@]@ )@ (MAIN %a)@]@.))@.@."
367 378
      (Utils.fprintf_list ~sep:" " pp_var) main_memory_current
368
      pp_machine_step_name node
379
      step_name node
369 380
      (Utils.fprintf_list ~sep:" " pp_var) (step_vars machines machine)
370 381
      (Utils.fprintf_list ~sep:" " pp_var) main_memory_next ;
371 382

  

Also available in: Unified diff