sig
type ('vertex, 'hedge, 'abstract, 'arc) manager =
('vertex, 'hedge, 'abstract, 'arc) FixpointType.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 =
FixpointType.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 =
('vertex, 'hedge) FixpointType.strategy_vertex = {
mutable vertex : 'vertex;
mutable hedges : 'hedge list;
mutable widen : bool;
}
type ('vertex, 'hedge) strategy =
(Fixpoint.strategy_iteration,
('vertex, 'hedge) Fixpoint.strategy_vertex)
Ilist.t
type stat_iteration =
FixpointType.stat_iteration = {
mutable nb : int;
mutable stable : bool;
}
type stat =
FixpointType.stat = {
mutable time : float;
mutable ascending : (Fixpoint.stat_iteration, unit) Ilist.t;
mutable descending : (Fixpoint.stat_iteration, unit) Ilist.t;
}
type ('vertex, 'hedge, 'abstract, 'arc) output =
('vertex, 'hedge, 'abstract, 'arc, Fixpoint.stat) PSHGraph.t
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) Fixpoint.strategy
val analysis_std :
('vertex, 'hedge, 'abstract, 'arc) Fixpoint.manager ->
('vertex, 'hedge, 'e, 'f, 'g) PSHGraph.t ->
'vertex PSette.t ->
('vertex, 'hedge) Fixpoint.strategy ->
('vertex, 'hedge, 'abstract, 'arc) Fixpoint.output
val analysis_guided :
('vertex, 'hedge, 'attr, 'arc) Fixpoint.manager ->
('vertex, 'hedge, 'e, 'f, 'g) PSHGraph.t ->
'vertex PSette.t ->
(('hedge -> bool) -> ('vertex, 'hedge) Fixpoint.strategy) ->
('vertex, 'hedge, 'attr, 'arc) Fixpoint.output
val equation_of_graph :
?filter:('hedge -> bool) ->
('vertex, 'hedge, 'attr, 'arc, 'e) PSHGraph.t ->
('vertex, 'hedge) Fixpoint.equation
val graph_of_equation :
('vertex, 'hedge) PSHGraph.compare ->
?filter:('hedge -> bool) ->
make_attrvertex:('vertex -> 'attr) ->
make_attrhedge:('hedge -> 'arc) ->
info:'e ->
('vertex, 'hedge) Fixpoint.equation ->
'vertex PSette.t -> ('vertex, 'hedge, 'attr, 'arc, 'e) PSHGraph.t
val analysis_dyn :
('a, 'b) SHGraph.compare ->
guided:bool ->
('a, 'b, 'c, 'd) Fixpoint.manager ->
('a, 'b) Fixpoint.equation ->
'a PSette.t ->
(('a, 'b, 'c, 'd) FixpointType.graph -> ('a, 'b) Fixpoint.strategy) ->
('a, 'b, 'c, 'd) Fixpoint.output
val print_strategy_vertex :
('a, 'b, 'c, 'd) Fixpoint.manager ->
Format.formatter -> ('a, 'b) Fixpoint.strategy_vertex -> unit
val print_strategy :
('a, 'b, 'c, 'd) Fixpoint.manager ->
Format.formatter -> ('a, 'b) Fixpoint.strategy -> unit
val print_stat : Format.formatter -> Fixpoint.stat -> unit
val print_output :
('vertex, 'hedge, 'attr, 'arc) Fixpoint.manager ->
Format.formatter ->
('vertex, 'hedge, 'attr, 'arc) Fixpoint.output -> unit
end