Commit | Line | Data |
---|---|---|
34e49164 C |
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 | |
485bce71 C |
23 | val print_graph : cfg -> string option -> |
24 | (node * string) list -> (node * string) list -> string -> unit | |
34e49164 C |
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 | |
485bce71 C |
67 | |
68 | val get_graph_files : unit -> string list | |
69 | val get_graph_comp_files : string -> string list | |
70 |