Project

General

Profile

« Previous | Next » 

Revision d0f26f04

Added by LĂ©lio Brun 7 months ago

corrections for stateless nodes

View differences:

src/machine_code.ml
236 236
  | None ->
237 237
    None, []
238 238

  
239
let translate_eq env ctx id inputs locals outputs i eq =
239
let translate_eq env ctx nd inputs locals outputs i eq =
240
  let id = nd.node_id in
240 241
  let translate_expr = translate_expr env in
241 242
  let translate_act = translate_act env in
242 243
  let locals_pi = Lustre_live.inter_live_i_with id (i - 1) locals in
......
268 269
        {
269 270
          inst with
270 271
          instr_spec =
271
            [
272
              mk_memory_pack ~i id;
273
              mk_transition ~i id (vdecls_to_vals inputs)
274
                (vdecls_to_vals locals_i) (vdecls_to_vals outputs_i);
275
            ];
272
            (if fst (get_stateless_status_node nd) then []
273
            else [ mk_memory_pack ~i id ])
274
            @ [
275
                mk_transition ~i id (vdecls_to_vals inputs)
276
                  (vdecls_to_vals locals_i) (vdecls_to_vals outputs_i);
277
              ];
276 278
        }
277 279
        :: ctx.s;
278 280
      mp = pred_mp ctx spec_mp;
......
388 390
      else eqs)
389 391
    [] locals
390 392

  
391
let translate_eqs env ctx id inputs locals outputs eqs =
393
let translate_eqs env ctx nd inputs locals outputs eqs =
392 394
  List.fold_left
393 395
    (fun (ctx, i) eq ->
394
      let ctx = translate_eq env ctx id inputs locals outputs i eq in
396
      let ctx = translate_eq env ctx nd inputs locals outputs i eq in
395 397
      ctx, i + 1)
396 398
    (ctx, 1) eqs
397 399
  |> fst
......
434 436
    in
435 437
    vars, eql, assertl
436 438

  
437
let translate_core env nid sorted_eqs inputs locals outputs =
439
let translate_core env nd sorted_eqs inputs locals outputs =
438 440
  let constant_eqs = constant_equations locals in
439 441

  
440 442
  (* Compute constants' instructions *)
441
  let ctx0 =
442
    translate_eqs env ctx_init nid inputs locals outputs constant_eqs
443
  in
443
  let ctx0 = translate_eqs env ctx_init nd inputs locals outputs constant_eqs in
444 444
  assert (ctx0.si = []);
445 445
  assert (IMap.is_empty ctx0.j);
446 446

  
447 447
  (* Compute ctx for all eqs *)
448
  let ctx = translate_eqs env ctx_init nid inputs locals outputs sorted_eqs in
448
  let ctx = translate_eqs env ctx_init nd inputs locals outputs sorted_eqs in
449 449

  
450 450
  ctx, ctx0.s
451 451

  
......
480 480
  }
481 481

  
482 482
let transition_toplevel nd i =
483
  let tr =
484
    mk_transition nd.node_id ~i
485
      (vdecls_to_vals nd.node_inputs)
486
      []
487
      (vdecls_to_vals nd.node_outputs)
488
  in
483 489
  {
484 490
    tname = nd;
485 491
    tindex = None;
......
487 493
    tlocals = [];
488 494
    toutputs = nd.node_outputs;
489 495
    tformula =
490
      ExistsMem
491
        ( nd.node_id,
492
          Predicate (ResetCleared nd.node_id),
493
          mk_transition nd.node_id ~i
494
            (vdecls_to_vals nd.node_inputs)
495
            []
496
            (vdecls_to_vals nd.node_outputs) );
496
      (if fst (get_stateless_status_node nd) then tr
497
      else ExistsMem (nd.node_id, Predicate (ResetCleared nd.node_id), tr));
497 498
    tfootprint = ISet.empty;
498 499
  }
499 500

  
......
542 543

  
543 544
  (* Translate equations *)
544 545
  let ctx, ctx0_s =
545
    translate_core env nd.node_id equations nd.node_inputs locals
546
      nd.node_outputs
546
    translate_core env nd equations nd.node_inputs locals nd.node_outputs
547 547
  in
548 548

  
549 549
  (* Format.eprintf "ok4@.@?"; *)
......
578 578
  let clear_reset =
579 579
    mkinstr
580 580
      ~instr_spec:
581
        [
582
          mk_memory_pack ~i:0 nd.node_id;
583
          mk_transition ~i:0 nd.node_id (vdecls_to_vals nd.node_inputs) [] [];
584
        ]
581
        ((if fst (get_stateless_status_node nd) then []
582
         else [ mk_memory_pack ~i:0 nd.node_id ])
583
        @ [
584
            mk_transition ~i:0 nd.node_id (vdecls_to_vals nd.node_inputs) [] [];
585
          ])
585 586
      MClearReset
586 587
  in
587 588
  {

Also available in: Unified diff