ctl/ctl_engine.mli

   1 open Ast_ctl
   2
   3 module type SUBST =
   4   sig
   5     type value
   6     type mvar
   7     val eq_mvar : mvar -> mvar -> bool
   8     val eq_val : value -> value -> bool
   9     val merge_val : value -> value -> value
  10     val print_mvar : mvar -> unit
  11     val print_value : value -> unit
  12   end
  13
  14 module type GRAPH =
  15   sig
  16     type node
  17     type cfg
  18     val predecessors:     cfg -> node -> node list
  19     val successors:       cfg -> node -> node list
  20     val extract_is_loop : cfg -> node -> bool
  21     val print_node :      node -> unit
  22     val size :            cfg -> int
  23     val print_graph :     cfg -> string option ->
  24       (node * string) list -> (node * string) list -> string -> unit
  25   end
  26
  27 module OGRAPHEXT_GRAPH :
  28   sig
  29     type node = int
  30     type cfg = (string, unit) Ograph_extended.ograph_mutable
  31     val predecessors :
  32       < predecessors : 'a -> < tolist : ('b * 'c) list; .. >; .. > ->
  33       'a -> 'b list
  34     val print_node : node -> unit
  35   end
  36
  37 module type PREDICATE =
  38 sig
  39   type t
  40   val print_predicate : t -> unit
  41 end
  42
  43 module CTL_ENGINE :
  44   functor (SUB : SUBST) ->
  45     functor (G : GRAPH) ->
  46       functor (P : PREDICATE) ->
  47       sig
  48
  49         type substitution = (SUB.mvar, SUB.value) Ast_ctl.generic_subst list
  50
  51         type ('pred,'anno) witness =
  52             (G.node, substitution,
  53              ('pred, SUB.mvar, 'anno) Ast_ctl.generic_ctl list)
  54               Ast_ctl.generic_witnesstree
  55
  56         type ('pred,'anno) triples =
  57             (G.node * substitution * ('pred,'anno) witness list) list
  58
  59         val sat :
  60           G.cfg * (P.t -> (P.t,'anno) triples) * G.node list ->
  61             (P.t, SUB.mvar, 'c) Ast_ctl.generic_ctl ->
  62               (P.t list list (* optional and required things *)) ->
  63                 (P.t,'anno) triples
  64
  65         val print_bench : unit -> unit
  66       end
  67
  68 val get_graph_files : unit -> string list
  69 val get_graph_comp_files : string -> string list
  70