1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
type status = Unknown of string
| Uncoverable of string
| Covered of string
type node_elt = {
labels: int list;
sequences : int list;
condition : (string * string * string) list
}
type node = {
mutable id: int;
ls: node_elt list;
mutable status: status
}
let annotateHLabel i e s = {id=i; ls=e.ls; status=s; }
let is_unknown hl =
match hl.status with
| Unknown _ -> true
| _ -> false
let string_of_intlist st il =
let l = List.fold_right (fun i s -> st ^ (string_of_int i) ^ "." ^ s) il "" in
String.sub l 0 (max 0 ((String.length l) - 1))
let string_of_tuple (va,t,vb) =
match va,t,vb with
| (va,"=",vb) -> va ^ "==" ^ vb
| (va,"!",vb) -> va ^ "!=" ^ vb
| _ -> raise (Invalid_argument "")
let combine_cond l r = if (String.length r = 0) then l else (l ^ " && " ^ r)
let string_of_cond c = if c = [] then "" else List.fold_right combine_cond (List.map string_of_tuple c) ""
let string_of_env env =
if env = "" then "[ ]" else env
let string_of_status status =
match status with
| Unknown env -> " - UNKNOWN - " ^ (string_of_env env)
| Uncoverable env -> " - UNCOVERABLE - " ^ (string_of_env env)
| Covered env -> " - COVERED - " ^ (string_of_env env)
let string_of_node n =
(if n.id >=0 then (string_of_int n.id) ^ ") " else "") ^
(let st =
(List.fold_right (fun nel s ->
"<"
^ (string_of_intlist "l" nel.labels)
^ (if (((List.length nel.labels) > 0) && ((List.length nel.sequences) > 0)) then "." else "")
^ (string_of_intlist "s" nel.sequences)
^ "|;"
^ (string_of_cond nel.condition)
^ ";> + "
^ s) n.ls "")
in
(String.sub st 0 ((String.length st) - 3)))
^ (string_of_status n.status)
^ ","
exception SyntaxError of string
let combine elle elri = {labels = elle.labels @ elri.labels;
sequences = elle.sequences @ elri.sequences;
condition = elle.condition @ elri.condition}
let createDnfFromLabel l = {id = -1;
ls = [{labels = [l]; sequences = []; condition = []}];
status = Unknown ""}
let createDnfFromSequence s = {id = -1;
ls = [{labels = []; sequences = [s]; condition = []}];
status = Unknown ""}
let createDnfFromGuard h c = {id = -1;
ls = List.map (fun el -> {
labels = el.labels;
sequences = el.sequences;
condition = el.condition @ c
}) h.ls;
status = Unknown ""}
let createDnfFromConjunction le ri =
{id = -1;
ls = List.concat (List.map (fun elle ->
List.map (fun elri -> combine elle elri) ri.ls
) le.ls);
status = Unknown ""}
let createDnfFromDisjunction le ri = {id = -1;
ls = le.ls @ ri.ls;
status = Unknown ""}