CristalCaveGem » LustreC

let rec translate_act env (y, expr) =

  let translate_act = translate_act env in

  let translate_guard = translate_guard env in

  let translate_expr = translate_expr env in

  let lustre_eq = Corelang.mkeq Location.dummy_loc ([ y.var_id ], expr) in

  match expr.expr_desc with

    * var_decl list

    (* outputs *)

    * ISet.t (* memory footprint *)

    * mc_formula_t)

    (* formula *)

    list;

      locals_i,

      outputs_i,

      ctx.m,

      Exists

        ( Lustre_live.existential_vars id i eq (locals @ outputs),

          And

        (MStep ([ var_x ], inst, [ c1; c2 ]))

        (mk_memory_pack ~inst (node_name td))

        (mk_transition ~inst (node_name td) [] [] [ vdecl_to_val var_x ])

    in

  | [ x ], Expr_pre e when env.is_local x ->

    let var_x = env.get_var x in

    let e = translate_expr e in

        (MStep (var_p, inst, vl))

        (mk_memory_pack ~inst (node_name node_f))

        (mk_transition ?r ~inst (node_name node_f) vl [] (vdecls_to_vals var_p))

    in

    (*Clocks.new_var true in Clock_calculus.unify_imported_clock (Some call_ck)

      eq.eq_rhs.expr_clock eq.eq_rhs.expr_loc; Format.eprintf "call %a: %a:

      si =

        (if Stateless.check_node node_f then ctx.si

        else mkinstr (MSetReset inst) :: ctx.si);

    }

  | [ x ], _ ->

    let var_x = env.get_var x in

    tlocals = [];

    toutputs = [];

    tformula = True;

  }

let transition_toplevel nd i =

    tformula =

      (if fst (get_stateless_status_node nd) then tr

      else ExistsMem (nd.node_id, Predicate (ResetCleared nd.node_id), tr));

  }

let translate_decl nd sch =

    transition_0 nd

    ::

    List.mapi

        {

          tname = nd;

          tindex = Some (i + 1);

          tlocals;

          toutputs;

          tformula = red f;

        })

      (List.rev ctx.t)

    @ [ transition_toplevel nd (List.length ctx.t) ]