sig
  type expression =
      PVar of string
    | PPrm of string * string
    | PCst of Logic_ptree.constant
    | PBinop of Logic_ptree.binop * Promelaast.expression *
        Promelaast.expression
    | PUnop of Logic_ptree.unop * Promelaast.expression
    | PArrget of Promelaast.expression * Promelaast.expression
    | PField of Promelaast.expression * string
    | PArrow of Promelaast.expression * string
  type condition =
      PRel of Logic_ptree.relation * Promelaast.expression *
        Promelaast.expression
    | PTrue
    | PFalse
    | POr of Promelaast.condition * Promelaast.condition
    | PAnd of Promelaast.condition * Promelaast.condition
    | PNot of Promelaast.condition
    | PCall of string * string option
    | PReturn of string
  and seq_elt = {
    condition : Promelaast.condition option;
    nested : Promelaast.sequence;
    min_rep : Promelaast.expression option;
    max_rep : Promelaast.expression option;
  }
  and sequence = Promelaast.seq_elt list
  type parsed_condition = Seq of Promelaast.sequence | Otherwise
  type typed_condition =
      TOr of Promelaast.typed_condition * Promelaast.typed_condition
    | TAnd of Promelaast.typed_condition * Promelaast.typed_condition
    | TNot of Promelaast.typed_condition
    | TCall of Cil_types.kernel_function * Cil_types.funbehavior option
    | TReturn of Cil_types.kernel_function
    | TTrue
    | TFalse
    | TRel of Cil_types.relation * Cil_types.term * Cil_types.term
  type single_action =
      Counter_init of Cil_types.term_lval
    | Counter_incr of Cil_types.term_lval
    | Pebble_init of Cil_types.logic_info * Cil_types.logic_var *
        Cil_types.logic_var
    | Pebble_move of Cil_types.logic_info * Cil_types.logic_var *
        Cil_types.logic_info * Cil_types.logic_var
    | Copy_value of Cil_types.term_lval * Cil_types.term
  type action = Promelaast.single_action list
  type state = {
    name : string;
    mutable acceptation : Bool3.t;
    mutable init : Bool3.t;
    mutable nums : int;
    mutable multi_state : (Cil_types.logic_info * Cil_types.logic_var) option;
  }
  type 'condition trans = {
    start : Promelaast.state;
    stop : Promelaast.state;
    mutable cross : 'condition;
    mutable numt : int;
  }
  type 'condition automaton =
      Promelaast.state list * 'condition Promelaast.trans list
  type parsed_automaton = Promelaast.parsed_condition Promelaast.automaton
  type typed_automaton =
      (Promelaast.typed_condition * Promelaast.action) Promelaast.automaton
  type funcStatus = Call | Return
end