sig
val args : (Arg.key * Arg.spec * Arg.doc) list
type state_predecessor = string * Exp.Id.t list * Assertions.cprop
type protocol_state =
string * Exp.Id.t list * Tycheck.state_predecessor list * Exp.Id.t *
Assertions.cprop
type protocol_item = {
protocol_name : string;
protocol_states : Tycheck.protocol_state Misc.StringMap.t;
protocol_successors : Misc.StringSet.t Misc.StringMap.t;
}
type escrow_item = {
escrow_name : string;
escrow_params : Exp.Id.t list;
escrow_pre : Assertions.cprop;
escrow_post : Assertions.cprop;
}
val convert :
Parsetree.p_item list ->
(string list * Misc.StringSet.t * Exp.IdSet.t *
(string, Tycheck.protocol_item) Hashtbl.t *
(string, Tycheck.escrow_item) Hashtbl.t *
(string, Commands.fun_info) Hashtbl.t *
(Misc.component, Assertions.act list * Assertions.act list) Hashtbl.t *
(Misc.component * Commands.res_init) list *
(string * Commands.can_entailment) list)
option
end