sig
type ('vertex, 'hedge, 'abstract, 'arc) manager = {
mutable bottom : 'vertex -> 'abstract;
mutable canonical : 'vertex -> 'abstract -> unit;
mutable is_bottom : 'vertex -> 'abstract -> bool;
mutable is_leq : 'vertex -> 'abstract -> 'abstract -> bool;
mutable join : 'vertex -> 'abstract -> 'abstract -> 'abstract;
mutable join_list : 'vertex -> 'abstract list -> 'abstract;
mutable widening : 'vertex -> 'abstract -> 'abstract -> 'abstract;
mutable odiff : ('vertex -> 'abstract -> 'abstract -> 'abstract) option;
mutable abstract_init : 'vertex -> 'abstract;
mutable arc_init : 'hedge -> 'arc;
mutable apply : 'hedge -> 'abstract array -> 'arc * 'abstract;
mutable print_vertex : Format.formatter -> 'vertex -> unit;
mutable print_hedge : Format.formatter -> 'hedge -> unit;
mutable print_abstract : Format.formatter -> 'abstract -> unit;
mutable print_arc : Format.formatter -> 'arc -> unit;
mutable accumulate : bool;
mutable print_fmt : Format.formatter;
mutable print_analysis : bool;
mutable print_component : bool;
mutable print_step : bool;
mutable print_state : bool;
mutable print_postpre : bool;
mutable print_workingsets : bool;
mutable dot_fmt : Format.formatter option;
mutable dot_vertex : Format.formatter -> 'vertex -> unit;
mutable dot_hedge : Format.formatter -> 'hedge -> unit;
mutable dot_attrvertex : Format.formatter -> 'vertex -> unit;
mutable dot_attrhedge : Format.formatter -> 'hedge -> unit;
}
type ('vertex, 'hedge) equation =
'vertex -> ('hedge, 'vertex array * 'vertex) PMappe.t
type strategy_iteration = {
mutable widening_start : int;
mutable widening_descend : int;
mutable ascending_nb : int;
mutable descending_nb : int;
mutable descending_stable : bool;
}
type ('vertex, 'hedge) strategy_vertex = {
mutable vertex : 'vertex;
mutable hedges : 'hedge list;
mutable widen : bool;
}
type ('vertex, 'hedge) strategy =
(FixpointType.strategy_iteration,
('vertex, 'hedge) FixpointType.strategy_vertex)
Ilist.t
val print_strategy_iteration :
Format.formatter -> FixpointType.strategy_iteration -> unit
val print_strategy_vertex :
('a, 'b, 'c, 'd) FixpointType.manager ->
Format.formatter -> ('a, 'b) FixpointType.strategy_vertex -> unit
val print_strategy :
('a, 'b, 'c, 'd) FixpointType.manager ->
Format.formatter -> ('a, 'b) FixpointType.strategy -> unit
val make_strategy_iteration :
?widening_start:int ->
?widening_descend:int -> unit -> FixpointType.strategy_iteration
val make_strategy_default :
?depth:int ->
?widening_start:int ->
?widening_descend:int ->
?priority:'hedge PSHGraph.priority ->
vertex_dummy:'vertex ->
hedge_dummy:'hedge ->
('vertex, 'hedge, 'e, 'f, 'g) PSHGraph.t ->
'vertex PSette.t -> ('vertex, 'hedge) FixpointType.strategy
type stat_iteration = { mutable nb : int; mutable stable : bool; }
type stat = {
mutable time : float;
mutable ascending : (FixpointType.stat_iteration, unit) Ilist.t;
mutable descending : (FixpointType.stat_iteration, unit) Ilist.t;
}
type ('vertex, 'hedge, 'abstract, 'arc) output =
('vertex, 'hedge, 'abstract, 'arc, FixpointType.stat) PSHGraph.t
val ilist_map_condense : ('a -> 'c) -> ('a, 'b) Ilist.t -> ('c, 'd) Ilist.t
val stat_iteration_merge :
(FixpointType.stat_iteration, unit) Ilist.t ->
FixpointType.stat_iteration
val print_stat_iteration :
Format.formatter -> FixpointType.stat_iteration -> unit
val print_stat_iteration_ilist :
Format.formatter -> (FixpointType.stat_iteration, 'a) Ilist.t -> unit
val print_stat : Format.formatter -> FixpointType.stat -> unit
val print_output :
('vertex, 'hedge, 'attr, 'arc) FixpointType.manager ->
Format.formatter ->
('vertex, 'hedge, 'attr, 'arc) FixpointType.output -> unit
type 'abstract attr = {
mutable reach : 'abstract;
mutable diff : 'abstract;
mutable empty : bool;
}
type 'arc arc = { mutable arc : 'arc; mutable aempty : bool; }
type ('vertex, 'hedge) infodyn = {
mutable iaddhedge : ('hedge, 'vertex array * 'vertex) PHashhe.t;
iequation : ('vertex, 'hedge) FixpointType.equation;
}
type ('vertex, 'hedge) info = {
iinit : 'vertex PSette.t;
itime : float Pervasives.ref;
mutable iascending : (FixpointType.stat_iteration, unit) Ilist.t;
mutable idescending : (FixpointType.stat_iteration, unit) Ilist.t;
mutable iworkvertex : ('vertex, unit) PHashhe.t;
mutable iworkhedge : ('hedge, unit) PHashhe.t;
iinfodyn : ('vertex, 'hedge) FixpointType.infodyn option;
}
type ('vertex, 'hedge, 'abstract, 'arc) graph =
('vertex, 'hedge, 'abstract FixpointType.attr, 'arc FixpointType.arc,
('vertex, 'hedge) FixpointType.info)
PSHGraph.t
val print_attr :
('a, 'b, 'c, 'd) FixpointType.manager ->
Format.formatter -> 'c FixpointType.attr -> unit
val print_arc :
('a, 'b, 'c, 'd) FixpointType.manager ->
Format.formatter -> 'd FixpointType.arc -> unit
val print_info :
('a, 'b, 'c, 'd) FixpointType.manager ->
Format.formatter -> ('a, 'b) FixpointType.info -> unit
val print_workingsets :
('a, 'b, 'c, 'd) FixpointType.manager ->
Format.formatter -> ('a, 'b, 'c, 'd) FixpointType.graph -> unit
val print_graph :
('vertex, 'hedge, 'attr, 'arc) FixpointType.manager ->
Format.formatter ->
('vertex, 'hedge, 'attr, 'arc) FixpointType.graph -> unit
val dot_graph :
?style:string ->
?titlestyle:string ->
?vertexstyle:string ->
?hedgestyle:string ->
?strategy:('a, 'b) FixpointType.strategy ->
?vertex:'a ->
('a, 'b, 'c, 'd) FixpointType.manager ->
('a, 'b, 'c, 'd) FixpointType.graph -> title:string -> unit
end