Project

General

Profile

Statistics
| Branch: | Revision:

cool / src / lib / coalgcompare.ml @ 7c4d2eb4

History | View | Annotate | Download (17.8 KB)

1
(** This module generates coalgebraic formulae and queries, and runs solvers on them.
2
    The generated formulae contain randomly generated formulae
3
    as well as instances of certain classes of formulae.
4
    @author Florian Widmann
5
 *)
6

    
7

    
8
module G = GenAndComp
9
module C = CoAlgFormula
10
module A = ALCFormula
11

    
12
open CoolUtils
13

    
14
type solvanswer = ASAT | AUNSAT | ATIMEOUT | AFAILED
15

    
16
exception UserInterupt
17

    
18
let string_of_solvanswer a =
19
    match a with
20
    | ASAT -> "sat"
21
    | AUNSAT -> "unsat"
22
    | ATIMEOUT -> "timeout"
23
    | AFAILED -> "failed"
24

    
25
type testresults =
26
   ((string list) (* solver names *)
27
    * ((string * ((solvanswer * int) list)) (*some test case with times for each reasoner*)
28
        list))
29

    
30
let debugMsg str =
31
    prerr_endline (":: " ^ str)
32

    
33
let ptimeout = ref (300) (* default timeout in seconds *)
34

    
35

    
36
(* generates the int range from i to j (including) *)
37
let (--) i j = 
38
    let rec aux n acc =
39
      if n < i then acc else aux (n-1) (n :: acc)
40
    in aux j []
41

    
42
let _ = Gc.set { (Gc.get()) with Gc.minor_heap_size = 4194304; major_heap_increment = 67108864; space_overhead = 120 }
43

    
44

    
45
(*
46
let seed =
47
  Random.self_init (); 
48
  Random.int ((1 lsl 30) - 1)
49
*)
50

    
51
let pseed = ref (209314489)
52

    
53
let sortK = Array.make 1 (CoAlgMisc.MultiModalK, [0])
54

    
55
let nomTable name =
56
  assert (CoAlgFormula.isNominal name);
57
  Some 0
58

    
59

    
60
(*
61
let maxCard = ref 100
62

    
63
let const_min r f =
64
  let card = (Random.int !maxCard) + 1 in
65
  C.const_min card r f
66

    
67
let const_max r f =
68
  let card = (Random.int (!maxCard+1)) in
69
  C.const_max card r f
70
 *)
71

    
72
let lFF = [(C.const_not, 1)]
73
let lFFF = [(C.const_or, 1); (C.const_and, 1)]
74
let lPFF = [(C.const_ex, 1); (C.const_ax, 1)]
75

    
76
let genFormula litFkt pFkt size =
77
  let nrLitsF = litFkt size in
78
  let lF =
79
    G.genLiterals ~litlst:[C.const_true; C.const_false] ~prio:10 C.const_ap "p" nrLitsF
80
  in
81
  let nrLitsP = pFkt size in
82
  let lP =
83
    if nrLitsP > 1 then G.genLiterals (fun x -> x) "a" nrLitsP
84
    else [("", 1)]
85
  in
86
  let genRF = fst (G.mk_generator lF lFF lFFF lPFF lP [] [] []) in
87
  genRF size
88

    
89
let genQuery litFkt pFkt tbcardFkt tbfsizeFkt size =
90
  let tbcard = tbcardFkt size in
91
  let tbfsize = tbfsizeFkt size in
92
  let tblitFkt n = litFkt size in
93
  let tbpFkt n = pFkt size in
94
  let tbox = ref [] in
95
  for i = 1 to tbcard do
96
    let tbf = genFormula tblitFkt tbpFkt tbfsize in
97
    tbox := (0, tbf)::!tbox
98
  done;
99
  let f = genFormula litFkt pFkt size in
100
  (!tbox, (0, f))
101

    
102

    
103
let rec exportALCFormula f =
104
  match f with
105
  | C.TRUE -> A.TRUE
106
  | C.FALSE -> A.FALSE
107
  | C.AP s when not (C.isNominal s) -> A.AP s
108
  | C.NOT f1 -> A.NOT (exportALCFormula f1)
109
  | C.OR (f1, f2) -> A.OR (exportALCFormula f1, exportALCFormula f2)
110
  | C.AND (f1, f2) -> A.AND (exportALCFormula f1, exportALCFormula f2)
111
  | C.EQU (f1, f2) -> A.EQU (exportALCFormula f1, exportALCFormula f2)
112
  | C.IMP (f1, f2) -> A.IMP (exportALCFormula f1, exportALCFormula f2)
113
  | C.EX (s, f1) -> A.EX (s, false, exportALCFormula f1)
114
  | C.AX (s, f1) -> A.AX (s, false, exportALCFormula f1)
115
  | C.MIN (n, s, f1) -> A.MIN (n, s, false, exportALCFormula f1)
116
  | C.MAX (n, s, f1) -> A.MAX (n, s, false, exportALCFormula f1)
117
  | C.MORETHAN (n, s, f1) -> A.MIN (n+1, s, false, exportALCFormula f1)
118
  | C.MAXEXCEPT (n, s, f1) -> A.MAX (n, s, false, exportALCFormula (C.NOT f1))
119
  | _ -> raise (C.CoAlgException "Formula is not expressible in ALC.")
120

    
121
let exportALCQuery tbox (_, f) =
122
  let tboxND = List.map (fun (_, f) -> exportALCFormula f) tbox in
123
  ([exportALCFormula f], tboxND, [])
124

    
125

    
126
let solvCoalg sortTable args =
127
  G.evaluateFkt (fun (tbox, sf) -> CoAlgReasoner.isSat sortTable nomTable tbox sf) args
128

    
129
let solvALC (tbox, sf) =
130
  let args = exportALCQuery tbox sf in
131
  G.evaluateFkt (fun (fl, tboxND, tboxD) -> ALCGraph.isSat fl tboxND tboxD) args
132

    
133
let solvFact (tbox, sf) timeout =
134
  let (fl, tboxND, tboxD) = exportALCQuery tbox sf in
135
  A.createFactTBox "fact.tbox" fl tboxND tboxD;
136
  let fact = "./FaCT++" in
137
  let reg = "is satisfiable" in
138
  let call () = G.callExt None fact ["fact.conf"] (Str.regexp_string reg) timeout in
139
  let ignore_exception = false in
140
  if ignore_exception then try call () with _ -> (G.FAILED, -1.0, 0)
141
                      else call ()
142

    
143
let solvTatl agents (tbox,(_,sf)) timeout = (* ignore the TBox... *)
144
  let tatl = "./tatl" in
145
  let tboxlist = List.map (fun (_,f) -> CoAlgFormula.exportTatlFormula f) tbox in
146
  let agstr = String.concat "," (List.map string_of_int agents) in
147
  let tboxstr = "~<<"^agstr^">>F~ ("^(String.concat " /\\ " tboxlist) ^ ") /\\ " in
148
  let inp = CoAlgFormula.exportTatlFormula sf in
149
  let inp = if TList.empty tbox then inp else (tboxstr ^ "(" ^ inp ^ ")") in
150
  G.callExt (Some ("1\n"^inp^"\n4")) tatl [] (Str.regexp_string "The formula is satisfiable") timeout
151

    
152
let solvCool functorname (tbox,sf) timeout =
153
  let inp = CoAlgFormula.exportQueryParsable tbox sf in
154
  G.callExt (Some inp) "./coalg" ["sat"; functorname] (Str.regexp_string "1: satisfiable") timeout
155

    
156
let solvCoolCL = solvCool "CL"
157

    
158
let solvers =
159
  let _ = [(solvCoalg sortK, "CoAlg"); (solvALC, "alc"); (solvFact, "fact")] in
160
  [(solvFact, "fact"); (solvCoalg sortK, "CoAlg")]
161

    
162
let printUsage () =
163
  print_endline "Usage: \"coalgcompare [<flags>] <logic> <logicargs>\" does tests where";
164
  print_endline "       <flags> in { --seed INITIALSEED }";
165
  print_endline "       <logic> in {";
166
  print_endline "                     K <formula counts in tbox> <list of sizes>";
167
  print_endline "                     (e.g. »K 0,5,10 10000,15000,20000«)";
168
  print_endline "                     genCL <agents> <list of sizes>";
169
  print_endline "                     (e.g. »genCL 1,2,3 4000,42«)";
170
  print_endline "                  }";
171
  exit 1
172

    
173
let runTests solvs formulas timeout : testresults =
174
  let reasonerNames = List.map (fun (_,s) -> s) solvs in
175
  let fillCell (fn,formula) (solver,sn) =
176
    debugMsg ("running " ^ sn ^ " on " ^ fn);
177
    let (res, time, _) = solver formula timeout in
178
    let answer = match res with
179
                 | G.FINISHED (v) -> if (v) then ASAT else AUNSAT
180
                 | G.TIMED_OUT -> ATIMEOUT
181
                 | G.FAILED -> AFAILED
182
    in
183
    (answer, int_of_float time)
184
  in
185
  let interrupted = ref (false) in
186
  let do_line (str,f) = if not !interrupted then
187
                            try (str,List.map (fun s -> fillCell (str,f) s) solvs)
188
                            with UserInterupt -> (interrupted := true; ("",[]))
189
                        else ("",[])
190
  in
191
  let results = List.filter (fun (_,cols) -> match cols with
192
                                             | (_::_) -> true
193
                                             | [] -> false)
194
                            (List.map do_line formulas)
195
  in
196
  (reasonerNames,results)
197

    
198

    
199
let doTestK (tboxsizes:int list) (szlist:int list) : testresults =
200
  let solvs = [(solvFact, "fact"); (solvCool "K", "cool")] in
201
  (*
202
    lF A list of pairs (f, n), e.g. (p, 1).
203
    The list must not be empty.
204
    lFF A list of pairs (f->f, n), e.g. (~., 1).
205
    The list must not be empty.
206
    lFFF A list of pairs (f->f->f, n), e.g. (.&., 1).
207
    lPFF A list of pairs (p->f->f, n), e.g. (<.>., 1).
208
    lP A list of pairs (p, n), e.g. (a, 1).
209
    The list must not be empty unless lPFF is also empty.
210
    lPP A list of pairs (p->p, n), e.g. ( *., 1).
211
    lFP A list of pairs (f->p, n), e.g. (?., 1).
212
    lPPP A list of pairs (p->p->p, n), e.g. (.+., 1).
213
  *)
214
  let timeout = !ptimeout in (* 5 minutes *)
215
  let lF = List.map (fun p -> C.AP ("p"^(string_of_int p))) (1--3) in
216
  let lF = List.append lF (List.map (C.const_not) lF) in
217
  let lF = C.TRUE :: C.FALSE :: lF in
218
  let lF = List.map (fun v -> (v,1)) lF in
219
  let roles : string list = List.map (fun p -> "R"^(string_of_int p)) (1--3) in
220
  let exs : (C.formula -> C.formula) list = List.map C.const_ex roles in
221
  let axs : (C.formula -> C.formula) list = List.map C.const_ax roles in
222
  let lFF = List.map (fun v -> (v,1)) (List.append exs axs) in
223
  let lFFF : (C.formula -> C.formula -> C.formula) list = List.append
224
                (List.map (fun x y z -> x (C.const_and y z)) exs)
225
                (List.map (fun x y z -> x (C.const_or y z))  axs)
226
  in
227
  let lFFF = List.map (fun v -> (v,1)) lFFF in
228
  let (genF,_) = G.mk_generator lF lFF lFFF [] [] [] [] [] in
229
  let reasonerNames = List.map (fun (_,s) -> s) solvs in
230
  let s1 = 0 in (* probably the correct formula... *)
231
  let formulas = List.map (fun (sz,cnt) ->
232
                            let tbox = List.map (fun _ -> (s1,genF sz)) (1 -- cnt) in
233
                            ("sz"^(string_of_int sz)^"tb"^(string_of_int cnt),(tbox,(s1,genF sz)))
234
                          ) (TList.prod szlist tboxsizes) in
235
  runTests solvs formulas timeout
236

    
237
let doTestGenericGML () : testresults =
238
  let solvs = [(solvFact, "fact"); (solvCool "GML", "cool")] in
239
  let timeout = !ptimeout in (* 5 minutes *)
240
  let formulas = ref [] in
241
  let counter = ref 0 in
242
  let s1 = 0 in
243
  (try
244
    while true do
245
      let input = read_line () in
246
      if not (GenAndComp.isEmptyString input) then
247
        let (tbox, f) = CoAlgFormula.importQuery input in
248
        incr counter;
249
        let test = ("line" ^ (string_of_int !counter), (tbox,f)) in
250
        formulas := test::(!formulas)
251
      else ()
252
    done
253
  with End_of_file -> ());
254
  let formulas = List.rev !formulas in
255
  runTests solvs formulas timeout
256

    
257

    
258
let doTestGenericK () : testresults =
259
  let solvs = [(solvFact, "fact"); (solvCool "K", "cool")] in
260
  let timeout = !ptimeout in (* 5 minutes *)
261
  let formulas = ref [] in
262
  let counter = ref 0 in
263
  let s1 = 0 in
264
  (try
265
    while true do
266
      let input = read_line () in
267
      if not (GenAndComp.isEmptyString input) then
268
        let (tbox, f) = CoAlgFormula.importQuery input in
269
        incr counter;
270
        let test = ("line" ^ (string_of_int !counter), (tbox,f)) in
271
        formulas := test::(!formulas)
272
      else ()
273
    done
274
  with End_of_file -> ());
275
  let formulas = List.rev !formulas in
276
  runTests solvs formulas timeout
277

    
278

    
279

    
280
let doTestGenericCL () : testresults =
281
  let agents = [1;2;3;4;5] in
282
  let solvs = [(solvTatl agents, "tatl"); (solvCoolCL, "cool")] in
283
  let timeout = !ptimeout in (* 5 minutes *)
284
  let formulas = ref [] in
285
  let counter = ref 0 in
286
  let s1 = 0 in
287
  (try
288
    while true do
289
      let input = read_line () in
290
      if not (GenAndComp.isEmptyString input) then
291
        let (tbox, f) = CoAlgFormula.importQuery input in
292
        incr counter;
293
        let test = ("line" ^ (string_of_int !counter), (tbox,f)) in
294
        formulas := test::(!formulas)
295
      else ()
296
    done
297
  with End_of_file -> ());
298
  let formulas = List.rev !formulas in
299
  runTests solvs formulas timeout
300

    
301

    
302

    
303
let printRawData ((rn,results):testresults) : unit =
304
    let doubler l = List.fold_right (fun a b -> (a ^ "_state")::(a^"_time")::b) l [] in
305
    print_endline (String.concat ";" ("formula"::doubler rn)) ;
306
    let format_cell (stat,time) = (string_of_solvanswer stat) ^ ";" ^ (string_of_int time) in
307
    let format_line (fn,res) = fn ^ ";" ^ (String.concat ";" (List.map format_cell res)) in
308
    let lines = List.map format_line results in
309
    print_endline (String.concat "\n" lines)
310

    
311
let doTestCL agents formulas : testresults =
312
  let solvs = [(solvTatl agents, "tatl"); (solvCoolCL, "cool")] in
313
  runTests solvs formulas !ptimeout
314

    
315
let doGenCL aglist sizelist : CoAlgFormula.formula list =
316
  (*
317
    lF A list of pairs (f, n), e.g. (p, 1).
318
    The list must not be empty.
319
    lFF A list of pairs (f->f, n), e.g. (~., 1).
320
    The list must not be empty.
321
    lFFF A list of pairs (f->f->f, n), e.g. (.&., 1).
322
    lPFF A list of pairs (p->f->f, n), e.g. (<.>., 1).
323
    lP A list of pairs (p, n), e.g. (a, 1).
324
    The list must not be empty unless lPFF is also empty.
325
    lPP A list of pairs (p->p, n), e.g. ( *., 1).
326
    lFP A list of pairs (f->p, n), e.g. (?., 1).
327
    lPPP A list of pairs (p->p->p, n), e.g. (.+., 1).
328
  *)
329
  let lF = List.map (fun p -> (C.AP ("p"^(string_of_int p)), 1)) (1--3) in
330
  let lFF = [(C.const_not,1)] in
331
  let lFFF = [(C.const_and,1)] in (* Warning: This forbids disjunctions! *)
332
  let lPFF = [(C.const_enforces,1); (C.const_allows, 1)] in
333
  (* role names *)
334
  let lP = List.map (fun p -> (p, 1)) (TList.powerset aglist) in
335
  let lPP : ((int list -> int list) * int) list= [] in
336
  let lFP = [] in
337
  let lPPP = [] in
338
  let (genF,_) = G.mk_generator lF lFF lFFF lPFF lP lPP lFP lPPP in
339
  List.map (fun sz -> (genF sz)) sizelist
340

    
341
let _ =
342
    let argidx = ref (1) in
343
    let fail str = (prerr_endline str ; printUsage ()) in
344
    let getarg () =
345
        if !argidx >= Array.length Sys.argv then (fail "Error: Missing argument ") else ();
346
        let str = Sys.argv.(!argidx) in
347
        argidx := 1 + !argidx;
348
        str
349
    in
350
    let pcmd = ref (getarg ()) in
351
    let rec parseflags () =
352
        match !pcmd with
353
        | "--seed" -> (pseed := (int_of_string (getarg ()));
354
                       pcmd := getarg ();
355
                       parseflags ())
356
        | "--timeout" -> (ptimeout := (int_of_string (getarg ()));
357
                       pcmd := getarg ();
358
                       parseflags ())
359
        | _ -> ()
360
    in
361
    parseflags ();
362
    Random.init !pseed;
363
    let alarmHandler (n : int) = raise G.Timeout in
364
    let sigintHandler (n : int) = prerr_endline "" ; raise UserInterupt in
365
    let oldHandler = Sys.signal Sys.sigalrm (Sys.Signal_handle alarmHandler) in
366
    let oldSigint = Sys.signal Sys.sigint (Sys.Signal_handle sigintHandler) in
367
    debugMsg ("seed is " ^ (string_of_int (!pseed)));
368
    let cmd = !pcmd in
369
    (
370
    match cmd with
371
    | "K" ->
372
             let tboxsizes = intlist_of_string (getarg ()) in
373
             let szlist = intlist_of_string (getarg()) in
374
             printRawData (doTestK tboxsizes szlist)
375
    | "genericK" ->
376
            printRawData (doTestGenericK ())
377
    | "genericGML" ->
378
            printRawData (doTestGenericGML ())
379
    | "genericCL" ->
380
            printRawData (doTestGenericCL ())
381
    | "CL1" -> let sz = (5000 -- 5080) in
382
               let agents = [1;2;3;4;5] in
383
               let ats (str,f) = (str, ([], (0, f))) in (* add tbox and sort *)
384
               printRawData (doTestCL agents (List.map ats (TList.zip (List.map string_of_int sz) (doGenCL agents sz))))
385
    | "genCL" -> let p1 = getarg () in
386
                 let p2 = getarg () in
387
                 let forms = doGenCL (intlist_of_string p1) (intlist_of_string p2) in
388
                 List.iter (fun f -> print_endline (CoAlgFormula.exportFormula f)) forms
389
    | _ -> raise (CoAlgFormula.CoAlgException ("Unknown Logic name »" ^ (Sys.argv.(1)) ^ "«"))
390
    );
391
    Sys.set_signal Sys.sigalrm oldHandler;
392
    Sys.set_signal Sys.sigint oldSigint
393

    
394

    
395
(*
396
let expQ (tbox, sf) = C.exportQuery tbox sf
397

    
398
let rateF = int_of_string Sys.argv.(1)
399
let rateP = int_of_string Sys.argv.(2)
400
let nr = int_of_string Sys.argv.(3)
401
let start = int_of_string Sys.argv.(4)
402
let stop = int_of_string Sys.argv.(5)
403
let step = int_of_string Sys.argv.(6)
404

    
405
let litFkt n = n / rateF
406
let pFkt n = n / rateP
407
let tbcardFkt n = 0
408
let tbfsizeFkt n = max 1 (n / 10)
409

    
410
let genQ = genQuery litFkt pFkt tbcardFkt tbfsizeFkt
411

    
412
let _ = G.toGnuPlot ~dots:10 ~timeout:10 ~fail:true expQ genQ solvers nr start stop ((+) step)
413

    
414
*)
415

    
416
(*
417
let files = [ ("benchmarks/DL98/DL98_alc_branch_sat.txt", "branch\\_n");
418
              ("benchmarks/DL98/DL98_alc_branch_unsat.txt", "branch\\_p");
419
              ("benchmarks/DL98/DL98_alc_d4_sat.txt", "d4\\_n");
420
              ("benchmarks/DL98/DL98_alc_d4_unsat.txt", "d4\\_p");
421
              ("benchmarks/DL98/DL98_alc_dum_sat.txt", "dum\\_n");
422
              ("benchmarks/DL98/DL98_alc_dum_unsat.txt", "dum\\_p");
423
              ("benchmarks/DL98/DL98_alc_grz_sat.txt", "grz\\_n");
424
              ("benchmarks/DL98/DL98_alc_grz_unsat.txt", "grz\\_p");
425
              ("benchmarks/DL98/DL98_alc_lin_sat.txt", "lin\\_n");
426
              ("benchmarks/DL98/DL98_alc_lin_unsat.txt", "lin\\_p");
427
              ("benchmarks/DL98/DL98_alc_path_sat.txt", "path\\_n");
428
              ("benchmarks/DL98/DL98_alc_path_unsat.txt", "path\\_p");
429
              ("benchmarks/DL98/DL98_alc_ph_sat.txt", "ph\\_n");
430
              ("benchmarks/DL98/DL98_alc_ph_unsat.txt", "ph\\_p");
431
              ("benchmarks/DL98/DL98_alc_poly_sat.txt", "poly\\_n");
432
              ("benchmarks/DL98/DL98_alc_poly_unsat.txt", "poly\\_p");
433
              ("benchmarks/DL98/DL98_alc_t4p_sat.txt", "t4p\\_n");
434
              ("benchmarks/DL98/DL98_alc_t4p_unsat.txt", "t4p\\_p") ]
435

    
436
let prebenchmarks =
437
  let mapB (filename, lab) =
438
    let file = open_in filename in
439
    let res = ref [] in
440
    let _ =
441
      try
442
        while true do
443
          let input = input_line file in
444
          if not (G.isEmptyString input) then
445
            let q = C.importQuery input in
446
            res := q::!res
447
          else ()
448
        done
449
      with End_of_file -> ()
450
    in
451
    (List.rev !res, lab)
452
  in
453
  List.map mapB files
454

    
455
let benchmarks =
456
  List.map (fun f -> fun () -> f) (List.flatten (List.map (fun (fl, _) -> fl) prebenchmarks))
457

    
458
let labels = List.map (fun (fl, lab) -> (List.length fl, lab)) prebenchmarks
459

    
460
let timeouts = [ 1; 2; 4; 8; 15; 30; 60 ]
461

    
462
let _ = G.outputBenchmarks ~fail:true expQ solvers timeouts benchmarks labels
463
 *)
464

    
465
let logicFkts = {
466
  G.l_tt = C.TRUE;
467
  G.l_ff = C.FALSE;
468
  G.l_ap = (fun s i -> C.AP (s ^ (string_of_int i)));
469
  G.l_not = C.const_not;
470
  G.l_and = C.const_and;
471
  G.l_or = C.const_or;
472
  G.l_imp = C.const_imp;
473
  G.l_aa = (fun s i -> s ^ (string_of_int i));
474
  G.l_box = C.const_ax;
475
  G.l_dia = C.const_ex;
476
  G.l_aw = (fun _ _ -> raise (C.CoAlgException "not implemented"));
477
  G.l_ev = (fun _ _ -> raise (C.CoAlgException "not implemented"));
478
  G.l_until = (fun _ _ -> raise (C.CoAlgException "not implemented"))
479
}
480

    
481
(*
482
let m = int_of_string Sys.argv.(1)
483
let k = int_of_string Sys.argv.(2)
484

    
485
let wrapSorts (f, tbox) =
486
  let tbox1 = List.map (fun f -> (0, f)) tbox in
487
  (tbox1, (0, f))
488

    
489
let (tbox, sf) =
490
  let (concl, tbox) = G.mk_wisemen_tbox logicFkts m k in
491
  wrapSorts (C.NOT concl, tbox)
492

    
493
let (tbox, sf) =
494
  let (concl, tbox) = G.mk_muddychildren_tbox logicFkts m k in
495
  wrapSorts (C.NOT concl, tbox)
496

    
497
let (tbox, sf) = wrapSorts (G.mk_exptime_tbox logicFkts m false)
498

    
499
let _ = CoAlgReasoner.isSat ~verbose:true sorts nomTable tbox sf
500
let _ =
501
  let (fl, tboxND, tboxD) = exportALCQuery tbox sf in
502
  ALCGraph.isSat ~verbose:true fl tboxND tboxD
503
 *)