sig
  val isCrossable :
    (Promelaast.typed_condition * Promelaast.action) Promelaast.trans ->
    Cil_types.kernel_function -> Promelaast.funcStatus -> bool
  val isCrossableAtInit :
    (Promelaast.typed_condition * Promelaast.action) Promelaast.trans ->
    Cil_types.kernel_function -> bool
  val crosscond_to_pred :
    Promelaast.typed_condition ->
    Cil_types.kernel_function -> Promelaast.funcStatus -> Cil_types.predicate
  val initFile : Cil_types.file -> unit
  val initGlobals : Cil_types.kernel_function -> bool -> unit
  val host_state_term : unit -> Cil_types.term_lval
  val is_state_pred : Promelaast.state -> Cil_types.predicate
  val is_state_stmt :
    Promelaast.state * Cil_types.varinfo ->
    Cil_types.location -> Cil_types.stmt
  val is_state_exp : Promelaast.state -> Cil_types.location -> Cil_types.exp
  val is_out_of_state_pred : Promelaast.state -> Cil_types.predicate
  val is_out_of_state_stmt :
    Promelaast.state * Cil_types.varinfo ->
    Cil_types.location -> Cil_types.stmt
  val is_out_of_state_exp :
    Promelaast.state -> Cil_types.location -> Cil_types.exp
  val aorai_assigns :
    Data_for_aorai.state ->
    Cil_types.location -> Cil_types.identified_term Cil_types.assigns
  val force_transition :
    Cil_types.location ->
    Cil_types.kernel_function ->
    Promelaast.funcStatus ->
    Data_for_aorai.state -> Cil_types.identified_predicate list
  val auto_func_preconditions :
    Cil_types.location ->
    Cil_types.kernel_function ->
    Promelaast.funcStatus ->
    Data_for_aorai.state -> Cil_types.identified_predicate list
  val auto_func_behaviors :
    Cil_types.location ->
    Cil_types.kernel_function ->
    Promelaast.funcStatus ->
    Data_for_aorai.state -> Cil_types.funbehavior list
  val auto_func_block :
    Cil_types.location ->
    Cil_types.kernel_function ->
    Promelaast.funcStatus ->
    Data_for_aorai.state ->
    Cil_types.varinfo option -> Cil_types.block * Cil_types.varinfo list
  val get_preds_pre_wrt_params :
    Cil_types.kernel_function -> Cil_types.predicate
  val get_preds_post_bc_wrt_params :
    Cil_types.kernel_function -> Cil_types.predicate
  val possible_states_preds :
    Data_for_aorai.state -> Cil_types.predicate list
  val update_to_pred :
    start:Cil_types.logic_label ->
    pre_state:Promelaast.state ->
    post_state:Promelaast.state ->
    Cil_types.term -> Data_for_aorai.Intervals.t -> Cil_types.predicate
  val action_to_pred :
    start:Cil_types.logic_label ->
    pre_state:Promelaast.state ->
    post_state:Promelaast.state ->
    Data_for_aorai.Vals.t -> Cil_types.predicate list
  val all_actions_preds :
    Cil_types.logic_label -> Data_for_aorai.state -> Cil_types.predicate list
  val zero_term : unit -> Cil_types.term
  val mk_offseted_array : Cil_types.term_lval -> int -> Cil_types.term
  val mk_offseted_array_states_as_enum :
    Cil_types.term_lval -> int -> Cil_types.term
  val mk_term_from_vi : Cil_types.varinfo -> Cil_types.term
  val make_enum_states : unit -> unit
end