Module States.Agreement

module Recovery_tactic = Gillian.General.Recovery_tactic
val to_yojson : t -> Yojson.Safe.t
val of_yojson : Yojson.Safe.t -> t Ppx_deriving_yojson_runtime.error_or
type err_t =
  1. | MissingState
val pp_err_t : Ppx_deriving_runtime.Format.formatter -> err_t -> Ppx_deriving_runtime.unit
val show_err_t : err_t -> Ppx_deriving_runtime.string
val err_t_to_yojson : err_t -> Yojson.Safe.t
val err_t_of_yojson : Yojson.Safe.t -> err_t Ppx_deriving_yojson_runtime.error_or
val _ : Yojson.Safe.t -> err_t Ppx_deriving_yojson_runtime.error_or
type action =
  1. | Load
type pred =
  1. | Ag
val pp : Gillian.Gil_syntax.Expr.t option Fmt.t
val action_from_str : string -> action option
val action_to_str : action -> string
val list_actions : unit -> (action * 'a list * string list) list
val pred_from_str : string -> pred option
val pred_to_str : pred -> string
val list_preds : unit -> (pred * 'a list * string list) list
val empty : unit -> t
val execute_action : action -> 'a option -> 'b list -> ('a option * 'a list, err_t) Stdlib.result Monadic.Delayed.t
val consume : pred -> 'a option -> 'b list -> ('a option * 'a list, err_t) Stdlib.result Monadic.Delayed.t
val is_exclusively_owned : 'a -> 'b -> bool Gillian.Monadic.Delayed.t
val is_empty : 'a option -> bool
val is_concrete : Gillian.Gil_syntax.Expr.t option -> bool
val instantiate : Gillian.Gil_syntax.Expr.t list -> Gillian.Gil_syntax.Expr.t option * 'a list
val assertions : 'a option -> (pred * 'b list * 'a list) list
val assertions_others : 'a -> 'b list
val can_fix : err_t -> bool
val get_fixes : err_t -> pred MyAsrt.t list list