CoAlgMisc.ml 58.2 KB
Newer Older
Thorsten Wißmann's avatar
Thorsten Wißmann committed
1
2
3
4
5
(** Common types, functions, and data structures for the CoAlgebraic reasoner.
    @author Florian Widmann
 *)


6
7
module S = 
MiscSolver
Thorsten Wißmann's avatar
Thorsten Wißmann committed
8
module L = List
Thorsten Wißmann's avatar
Thorsten Wißmann committed
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
module C = CoAlgFormula
module HC = HashConsing


(** An instantiation of a set (of the standard library) for bitsets.
 *)
module BsSet = Set.Make(
  struct
    type t = S.bitset
    let (compare : t -> t -> int) = S.compareBS
  end
 )

(** An instantiation of a hash table (of the standard library) for bitsets.
 *)
module GHt = Hashtbl.Make(
25
26
27
28
29
30
31
32
33
34
35
  struct
    type t = S.bitset * S.bitset
    let equal ((bs1l, bs1r) : t) (bs2l, bs2r) =
      (S.compareBS bs1l bs2l = 0) && (S.compareBS bs1r bs2r = 0)
    let hash ((bsl, bsr) : t) = (S.hashBS bsl) lxor (S.hashBS bsr)
  end
 )

(** An instantiation of a hash table (of the standard library) for bitsets.
 *)
module GHtS = Hashtbl.Make(
Thorsten Wißmann's avatar
Thorsten Wißmann committed
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
  struct
    type t = S.bitset
    let equal (bs1 : t) bs2 = S.compareBS bs1 bs2 = 0
    let hash (bs : t) = S.hashBS bs
  end
 )

(** An instantiation of a hash table (of the standard library) for literals.
 *)
module LHt = Hashtbl.Make(
  struct
    type t = Minisat.lit
    let equal (l1 : t) l2 = l1 = l2
    let hash (l : t) = (l :> int)
  end
 )

(** An instantiation of a hash table (of the standard library) for formulae.
 *)
module FHt = Hashtbl.Make(
  struct
    type t = int
    let equal (f1 : t) f2 = f1 = f2
    let hash (f : t) = f
  end
 )

(** An instantiation of a hash table (of the standard library) for nominals.
 *)
module NHt = Hashtbl.Make(
  struct
    type t = int * int
    let equal ((s1, f1) : t) (s2, f2) = (s1 = s2) && (f1 = f2)
    let hash ((s, f) : t) = (((s+f)*(s+f+1)) / 2) + f
  end
)


(*****************************************************************************)
(*     Types that can be modified rather easily                              *)
(*     (of course you then have to modify the implementations below too)     *)
(*****************************************************************************)

(* This type must be extended for additional logics. *)
type functors =
  | MultiModalK
Thorsten Wißmann's avatar
Temp    
Thorsten Wißmann committed
82
  | MultiModalKD
83
  | Monotone
Ludwig Dietel's avatar
Ludwig Dietel committed
84
  | MultiModalM
Thorsten Wißmann's avatar
Thorsten Wißmann committed
85
  | CoalitionLogic
Thorsten Wißmann's avatar
Thorsten Wißmann committed
86
  | GML
87
  | PML
88
  | Constant of string list
89
90
  | Identity
  | DefaultImplication
Thorsten Wißmann's avatar
Thorsten Wißmann committed
91
92
93
  | Choice
  | Fusion

94
95
96
97
98
99
100
101
102
103
104
105
(* functors whose constructor takes additional parameters *)
type parametricFunctorName =
  | NameConstant

(* this type should only be used in the following few helper functions *)
type functorName =
  | NPa of functors (* No Parameters = functor without parameters *)
  | Pa  of parametricFunctorName (* Parameters = functor with parameters *)

let unaryfunctor2name : (functorName*string) list =
  [ (NPa MultiModalK , "MultiModalK")
  ; (NPa MultiModalKD , "MultiModalKD")
106
  ; (NPa Monotone , "Monotone")
Ludwig Dietel's avatar
Ludwig Dietel committed
107
  ; (NPa MultiModalM , "MultiModalM")
108
109
110
111
112
  ; (NPa GML ,           "GML")
  ; (NPa PML ,           "PML")
  ; (NPa CoalitionLogic , "CoalitionLogic")
  ; (NPa MultiModalK , "K")
  ; (NPa MultiModalKD , "KD")
Ludwig Dietel's avatar
Ludwig Dietel committed
113
  ; (NPa MultiModalM , "M")
114
115
116
  ; (NPa CoalitionLogic , "CL")
  ; (Pa  NameConstant , "Const")
  ; (Pa  NameConstant , "Constant")
117
118
  ; (NPa Identity, "Id")
  ; (NPa Identity, "Identity")
119
120
  ]

121
let functor2name : (functorName*string) list =
122
  L.append unaryfunctor2name
123
124
  [ (NPa Choice , "Choice")
  ; (NPa Fusion , "Fusion")
125
126
  ]

127
128
129
130
131
132
133
134
let functor_apply_parameters (func : parametricFunctorName) (params: string list) : functors option =
    (* apply parameter list to the constructor, denoted by the functor name func *)
    (* return None, if the parameters somehow don't match the required parameters *)
    match func with
    | NameConstant -> Some (Constant params)


let functor_of_string str params : functors option =
135
136
    let fst (a,b) = a in
    try
137
138
139
140
        let functorName = fst (List.find (fun (f,name) -> name = str) functor2name) in
        match functorName with
        | NPa x -> Some x
        | Pa f -> functor_apply_parameters f params
141
142
    with Not_found -> None

143
144
let unaryfunctor_of_string str params =
    match (functor_of_string str params) with
145
146
147
148
149
    | Some Choice -> None
    | Some Fusion -> None
    | x -> x

let string_of_functor (f: functors) : string =
150
151
152
153
154
155
    (* replace f orrectly with possibly some Pa wrapper *)
    (* also put the parameters into some suffix which will be appended later *)
    let f,suffix = match f with
            | Constant params -> Pa NameConstant, " "^(String.concat " " params)
            | _ -> NPa f, ""
    in
156
157
    let snd (a,b) = b in
    try
158
159
        let name = snd (List.find (fun (f2,name) -> f = f2) functor2name) in
        name ^ suffix
160
161
    with Not_found -> assert false

Thorsten Wißmann's avatar
Thorsten Wißmann committed
162
163
164
(* This type may be extended for additional logics. *)
type formulaType =
  | Other
dirk's avatar
dirk committed
165
  | TrueFalseF (* constant true or false *)
Thorsten Wißmann's avatar
Thorsten Wißmann committed
166
167
168
169
  | AndF
  | OrF
  | AtF
  | NomF
170
171
  | ExF  (* Existential / diamond *)
  | AxF  (* Universal / box *)
Thorsten Wißmann's avatar
Thorsten Wißmann committed
172
173
  | EnforcesF (* diamond of CL *)
  | AllowsF   (* box of CL *)
174
175
  | MoreThanF (* more than n successors = diamond in gml *)
  | MaxExceptF(* at most n exceptions = box in gml *)
176
  | AtLeastProbF (* for PML *)
177
  | LessProbFailF (* box for PML *)
178
179
  | ConstF (* constant functor *)
  | ConstnF (* constant functor *)
180
181
182
  | IdF (* Identity functor *)
  | NormF (* Default Implication *)
  | NormnF (* negation normal form of default implication *)
183
184
  | ChcF (* Choice *)
  | FusF (* Fusion *)
185
186
  | MuF
  | NuF
Thorsten Wißmann's avatar
Thorsten Wißmann committed
187
188
189
190
191
192
193
194
195
196
197
198

type localFormula = int
type bset = S.bitset

type atFormula = int
type cset = S.bitset
type csetSet = BsSet.t

type lht = localFormula LHt.t
type fht = Minisat.lit FHt.t
type nht = bset NHt.t

199
200
201
202
203
type state = { sortS : sort;
               mutable bsS : bset; (* a set of formulas who are either literals or
                                      modalities (TODO: also @-formulas?).
                                      the state is satisfiable if /\bsS is satisfiable.
                                    *)
204
               mutable deferralS : bset; (* which formulas still have deferrals *)
205
               mutable statusS : nodeStatus;
Thorsten Wißmann's avatar
Thorsten Wißmann committed
206
               mutable parentsS : core list; mutable childrenS : (dependencies * core list) list;
207
208
               mutable constraintsS : csetSet; expandFkt : stateExpander;
               idx: int }
Thorsten Wißmann's avatar
Thorsten Wißmann committed
209

210
211
212
213
and core = { (* for details, see documentation of newCore *)
             sortC : sort;
             mutable bsC : bset; (* a set of arbitrary formulas.
                                    the present core is satisfiable if /\ bsC is satisfiable *)
214
             mutable deferralC : bset; (* which formulas still have deferrals *)
215
216
217
218
             mutable statusC : nodeStatus;
             mutable parentsC : (state * int) list;
             mutable childrenC : state list;
             mutable constraintsC : csetSet;
219
             mutable solver : Minisat.solver option; (* a solver to find satisfying assignemnts for bsC.
220
221
222
223
224
225
226
227
                                         the solver returns "satisfiable" iff
                                         there is a satisfying assignment of
                                         bsC which is not represented by some state from the
                                         childrenC yet.
                                       *)
             fht : fht; (* mapping of boolean subformulas of bsC to their corresponding literals
                           of the Minisat solver
                         *)
228
229
             mutable constraintParents : cset list;
             idx : int }
Thorsten Wißmann's avatar
Thorsten Wißmann committed
230

231
and setState = state GHt.t array
Thorsten Wißmann's avatar
Thorsten Wißmann committed
232

233
and setCore = core GHt.t array
Thorsten Wißmann's avatar
Thorsten Wißmann committed
234

235
and setCnstr = unit GHtS.t
Thorsten Wißmann's avatar
Thorsten Wißmann committed
236
237
238
239
240
241


(*****************************************************************************)
(*                Types that are hard coded into the algorithm               *)
(*****************************************************************************)

242
243
244
and 'a junction = | Disjunctive of 'a (*specifies that any of the 'a needs to be satifsfied *)
                  | Conjunctive of 'a (*specifies that all of the 'a need  to be satifsfied *)

245
and stateExpander = rule lazylist
Thorsten Wißmann's avatar
Thorsten Wißmann committed
246
247
248
249
250
251
252
253
254

and sort = C.sort

and nodeStatus =
  | Expandable
  | Open
  | Sat
  | Unsat

255
256
257
258
259
260
261
(* In K, given the singleton list [bs] returns the list of all Ax'es
   responsible for the individual members of bs being part of the core
   as well as the Ex.

   So given the state { <>φ , []ψ , []η } and the core { φ , ψ , η },
   dependency would map { η } to { <>φ , []η } and { ψ } to { <>φ , []ψ }
*)
Thorsten Wißmann's avatar
Thorsten Wißmann committed
262
and dependencies = bset list -> bset
263

264
(* Note: sort * bset * bset is to be read as sort * formulas_in_core * deferrals_in_core *)
265
and rule = (dependencies * (sort * bset * bset) lazylist)
266

267
and 'a lazyliststep =
268
269
270
271
  | MultipleElements of 'a list
  | SingleElement    of 'a
  | NoMoreElements

272
273
274
275
and 'a lazylist = unit -> 'a lazyliststep

and ruleEnumeration = rule lazyliststep

276
277
278
279
280
281
let nodeStatusToString : nodeStatus -> string = function
  | Expandable -> "Expandable"
  | Open -> "Open"
  | Sat -> "Sat"
  | Unsat -> "Unsat"

282
283
284
285
286
287
288
289
290
let lazylistFromList a_list =
    let list_state = ref (Some a_list) in
    fun () -> begin match !list_state with
              | Some (a_list) -> begin
                    list_state := None;
                    MultipleElements a_list
                end
              | None -> NoMoreElements
              end
Thorsten Wißmann's avatar
Thorsten Wißmann committed
291

292
293
294
295
296
297
298
let rec listFromLazylist evalfunc =
    let step = evalfunc () in
    match step with
    | NoMoreElements -> []
    | SingleElement x -> x::(listFromLazylist evalfunc)
    | MultipleElements xs -> List.append xs (listFromLazylist evalfunc)

Thorsten Wißmann's avatar
Thorsten Wißmann committed
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
type nominal = sort * localFormula

type node =
  | State of state
  | Core of core

type constrnt =
  | UnsatC
  | SatC
  | OpenC of node list
  | UnexpandedC of node list

type propagateElement =
  | UState of state * int option
  | UCore of core * bool
  | UCnstr of cset

type queueElement =
  | QState of state
  | QCore of core
  | QCnstr of cset
  | QEmpty

type sortTable = (functors * int list) array

exception CoAlg_finished of bool


let sortTable = ref (Array.make 0 (MultiModalK, [1]))

329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
let junctionEvalBool : (bool list junction) -> bool = function
    | Disjunctive l -> List.fold_right (||) l false
    | Conjunctive l -> List.fold_right (&&) l true

let junctionEval (f: 'a -> bool) : 'a list junction -> bool = function
    | Disjunctive l -> List.fold_right (fun x y -> (f x) || y) l false
    | Conjunctive l -> List.fold_right (fun x y -> (f x) && y) l true

let optionalizeOperator (f: 'a -> 'b -> 'c) (x: 'a option) (y: 'b option) : 'c option =
    match x with
    | None -> None
    | Some x -> (match y with
                 | None -> None
                 | Some y -> Some (f x y))

let junctionEvalBoolOption : bool option list junction -> bool option =
    let f extreme op x y = (* ensure that: (Some True) || None = Some True *)
        if x = extreme || y = extreme
        then extreme
        else optionalizeOperator op x y
    in function
    | Disjunctive l ->
        List.fold_right (f (Some true)  (||)) l (Some false)
    | Conjunctive l ->
        List.fold_right (f (Some false) (&&)) l (Some true)

let junctionExtract : 'a junction -> ('a * ('b -> 'b junction)) = function
    | Disjunctive l -> (l, fun x -> Disjunctive x)
    | Conjunctive l -> (l, fun x -> Conjunctive x)
Thorsten Wißmann's avatar
Thorsten Wißmann committed
358
359
360
361
362
363
364
365
366
367

(*****************************************************************************)
(*      "Module type" and a specific implementation of the main queue        *)
(*****************************************************************************)

let queueStates = ref ([] : state list)
let queueCores1 = ref ([] : core list)
let queueCores2 = ref ([] : core list)
let queueCnstrs = ref ([] : cset list)
let doPropagation = ref false
368
let doPropagationCounter = ref 0
Thorsten Wißmann's avatar
Thorsten Wißmann committed
369
370
371
372
373
374
375
376
377
378
379
380
381

let queueInit () =
  queueStates := [];
  queueCores1 := [];
  queueCores2 := [];
  queueCnstrs := [];
  doPropagation := false

let queueIsEmpty () =
  !queueStates = [] && !queueCores1 = [] && !queueCores2 = [] && !queueCnstrs = []

let queueInsertState state = queueStates := state::!queueStates

382
(* original version: breadth-first *)
Thorsten Wißmann's avatar
Thorsten Wißmann committed
383
384
let queueInsertCore core = queueCores2 := core::!queueCores2

Christoph Egger's avatar
Christoph Egger committed
385
(* experiment: depth first
386
387
388
let queueInsertCore core = queueCores1 := core::!queueCores1
*)

Thorsten Wißmann's avatar
Thorsten Wißmann committed
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
let queueInsertCnstr cset = queueCnstrs := cset::!queueCnstrs

let queueGetElement () =
  if !queueCnstrs <> [] then
    let res = List.hd !queueCnstrs in
    queueCnstrs := List.tl !queueCnstrs;
    QCnstr res
  else if !queueStates <> [] then
    let res = List.hd !queueStates in
    queueStates := List.tl !queueStates;
    QState res
  else if !queueCores1 <> [] then
    let res = List.hd !queueCores1 in
    queueCores1 := List.tl !queueCores1;
    QCore res
  else if !queueCores2 = [] then QEmpty
  else
    let res = List.hd !queueCores2 in
    doPropagation := true;
    queueCores1 := List.tl !queueCores2;
    queueCores2 := [];
    QCore res

let doNominalPropagation () = !doPropagation

414
415
416
let setPropagationCounter count =
  doPropagationCounter := count

Thorsten Wißmann's avatar
Thorsten Wißmann committed
417
let doSatPropagation () =
418
  if !doPropagationCounter == 0
419
  then true
420
421
422
423
424
425
426
  else begin
      doPropagationCounter := !doPropagationCounter - 1;
      false
    end
  (* let res = !doPropagation in *)
  (* doPropagation := false; *)
  (* res *)
Thorsten Wißmann's avatar
Thorsten Wißmann committed
427
428
429
430
431
432
433

(*****************************************************************************)
(*        "Module type" and a specific implementation of the graph           *)
(*****************************************************************************)

let graphStates = ref (Array.make 0 (GHt.create 0 : state GHt.t))
let graphCores = ref (Array.make 0 (GHt.create 0 : core GHt.t))
434
let graphCnstrs = ref (GHtS.create 0 : constrnt GHtS.t)
Thorsten Wißmann's avatar
Thorsten Wißmann committed
435
436
437
438
439
440
let graphRoot = ref (None : core option)

let graphInit () =
  let size = Array.length !sortTable in
  graphStates := Array.init size (fun _ -> GHt.create 128);
  graphCores := Array.init size (fun _ -> GHt.create 128);
441
  graphCnstrs := GHtS.create 128;
Thorsten Wißmann's avatar
Thorsten Wißmann committed
442
443
444
445
446
447
448
449
  graphRoot := None

let graphIterStates fkt =
  Array.iter (fun ht -> GHt.iter (fun _ x -> fkt x) ht) !graphStates

let graphIterCores fkt =
  Array.iter (fun ht -> GHt.iter (fun _ x -> fkt x) ht) !graphCores

450
let graphIterCnstrs fkt = GHtS.iter fkt !graphCnstrs
Thorsten Wißmann's avatar
Thorsten Wißmann committed
451
452

let graphClearCnstr () =
453
  let newGraph = GHtS.create (GHtS.length !graphCnstrs) in
Thorsten Wißmann's avatar
Thorsten Wißmann committed
454
455
456
  let copyCnstr cset cnstr =
    match cnstr with
    | UnsatC
457
458
459
    | SatC -> GHtS.add newGraph cset cnstr
    | OpenC _ -> GHtS.add newGraph cset (OpenC [])
    | UnexpandedC _ -> GHtS.add newGraph cset (UnexpandedC [])
Thorsten Wißmann's avatar
Thorsten Wißmann committed
460
  in
461
  GHtS.iter copyCnstr !graphCnstrs;
Thorsten Wißmann's avatar
Thorsten Wißmann committed
462
463
464
465
466
467
468
469
470
471
472
473
474
475
  graphCnstrs := newGraph

let graphFindState sort bs =
  try
    Some (GHt.find !graphStates.(sort) bs)
  with Not_found -> None

let graphFindCore sort bs =
  try
    Some (GHt.find !graphCores.(sort) bs)
  with Not_found -> None

let graphFindCnstr cset =
  try
476
    Some (GHtS.find !graphCnstrs cset)
Thorsten Wißmann's avatar
Thorsten Wißmann committed
477
478
479
480
481
482
  with Not_found -> None

let graphInsertState sort bs state =
  assert (not (GHt.mem !graphStates.(sort) bs));
  GHt.add !graphStates.(sort) bs state

483
484
485
let graphDeleteState sort state =
  GHt.remove !graphStates.(sort) state

Thorsten Wißmann's avatar
Thorsten Wißmann committed
486
487
488
489
let graphInsertCore sort bs core =
  assert (not (GHt.mem !graphCores.(sort) bs));
  GHt.add !graphCores.(sort) bs core

490
491
492
let graphDeleteCore sort core =
  GHt.remove !graphCores.(sort) core

Thorsten Wißmann's avatar
Thorsten Wißmann committed
493
let graphInsertCnstr cset cnstr =
494
495
  assert (not (GHtS.mem !graphCnstrs cset));
  GHtS.add !graphCnstrs cset cnstr
Thorsten Wißmann's avatar
Thorsten Wißmann committed
496
497

let graphReplaceCnstr cset cnstr =
498
  GHtS.replace !graphCnstrs cset cnstr
Thorsten Wißmann's avatar
Thorsten Wißmann committed
499
500
501
502
503

let graphSizeState () =
  Array.fold_left (fun acc ht -> acc + GHt.length ht) 0 !graphStates
let graphSizeCore () =
  Array.fold_left (fun acc ht -> acc + GHt.length ht) 0 !graphCores
504
let graphSizeCnstr () = GHtS.length !graphCnstrs
Thorsten Wißmann's avatar
Thorsten Wißmann committed
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527

let graphAddRoot core =
  if !graphRoot = None then graphRoot := Some core
  else raise (C.CoAlgException "Root of graph is already set.")

let graphGetRoot () =
  match !graphRoot with
  | None -> raise (C.CoAlgException "Root of graph is not set.")
  | Some core -> core


(*****************************************************************************)
(*     "Module type" and a specific implementation of sets of constraints    *)
(*****************************************************************************)

let cssEmpty = BsSet.empty
let cssExists fkt css = BsSet.exists fkt css
let cssForall fkt css = BsSet.for_all fkt css
let cssUnion css1 css2 = BsSet.union css1 css2
let cssAdd cset css = BsSet.add cset css
let cssFold fkt css init = BsSet.fold fkt css init
let cssSingleton cset = BsSet.singleton cset
let cssEqual css1 css2 = BsSet.equal css1 css2
528
529
let cssIter (action: cset -> unit) css =
    BsSet.iter action css
Thorsten Wißmann's avatar
Thorsten Wißmann committed
530
531
532
533
534


(*****************************************************************************)
(*      "Module type" and a specific implementation of state nodes           *)
(*****************************************************************************)
535
536
537
538
539
540
let nodeCounter = ref 0
let nextNodeIdx () : int =
    let oldVal = !nodeCounter in
    nodeCounter := oldVal + 1;
    oldVal

541
542
let stateMake sort bs defer exp =
  { sortS = sort; bsS = bs; deferralS = defer; statusS = Expandable; parentsS = []; childrenS = [];
543
    constraintsS = cssEmpty; expandFkt = exp;
544
    idx = nextNodeIdx ()
545
  }
Thorsten Wißmann's avatar
Thorsten Wißmann committed
546
547
548
let stateGetSort state = state.sortS
let stateGetBs state = state.bsS
let stateSetBs state bs = state.bsS <- bs
549
550
let stateGetDeferral state = state.deferralS
let stateSetDeferral state bs = state.deferralS <- bs
Thorsten Wißmann's avatar
Thorsten Wißmann committed
551
552
553
554
555
556
557
558
559
560
561
562
let stateGetStatus state = state.statusS
let stateSetStatus state status = state.statusS <- status
let stateGetParents state = state.parentsS
let stateAddParent state parent = state.parentsS <- parent::state.parentsS
let stateGetRule state idx = List.nth state.childrenS (List.length state.childrenS - idx)
let stateGetRules state = state.childrenS
let stateAddRule state dep children =
  state.childrenS <- (dep, children)::state.childrenS;
  List.length state.childrenS
let stateGetConstraints state = state.constraintsS
let stateSetConstraints state csets = state.constraintsS <- csets
let stateNextRule state = state.expandFkt ()
563
let stateGetIdx (state:state) = state.idx
Thorsten Wißmann's avatar
Thorsten Wißmann committed
564
565
566
567
568
569


(*****************************************************************************)
(*      "Module type" and a specific implementation of core nodes            *)
(*****************************************************************************)

570
571
let coreMake sort bs defer solver fht =
  { sortC = sort; bsC = bs; deferralC = defer; statusC = Expandable; parentsC = []; childrenC = [];
572
    constraintsC = cssEmpty; solver = solver; fht = fht; constraintParents = [];
573
    idx = nextNodeIdx ()
574
  }
Thorsten Wißmann's avatar
Thorsten Wißmann committed
575
576
577
let coreGetSort core = core.sortC
let coreGetBs core = core.bsC
let coreSetBs core bs = core.bsC <- bs
578
579
let coreGetDeferral core = core.deferralC
let coreSetDeferral core bs = core.deferralC <- bs
Thorsten Wißmann's avatar
Thorsten Wißmann committed
580
581
582
583
let coreGetStatus core = core.statusC
let coreSetStatus core status = core.statusC <- status
let coreGetParents core = core.parentsC
let coreAddParent core parent idx = core.parentsC <- (parent, idx)::core.parentsC
584
let coreSetParent core parent idx = core.parentsC <- [(parent, idx)]
Thorsten Wißmann's avatar
Thorsten Wißmann committed
585
586
587
588
589
let coreGetChildren core = core.childrenC
let coreAddChild core child = core.childrenC <- child::core.childrenC
let coreGetConstraints core = core.constraintsC
let coreSetConstraints core csets = core.constraintsC <- csets
let coreGetSolver core = core.solver
590
let coreDeallocateSolver core = core.solver <- None; FHt.reset core.fht
Thorsten Wißmann's avatar
Thorsten Wißmann committed
591
let coreGetFht core = core.fht
592
let coreGetIdx (core:core) = core.idx
Thorsten Wißmann's avatar
Thorsten Wißmann committed
593
594
595
596
597
598
599
600
601
602
let coreGetConstraintParents core = core.constraintParents
let coreAddConstraintParent core cset =
  core.constraintParents <- cset::core.constraintParents


(*****************************************************************************)
(*      "Module type" and a specific implementation of sets of               *)
(*      states, cores, and constraints for the sat propagation               *)
(*****************************************************************************)

603
604
let setEmptyState () = Array.init (Array.length !sortTable) (fun _ -> GHt.create 128)
let setEmptyCore () = Array.init (Array.length !sortTable) (fun _ -> GHt.create 128)
605
606
let setCopyState set = Array.init (Array.length !sortTable) (fun idx -> GHt.copy set.(idx))
let setCopyCore set = Array.init (Array.length !sortTable) (fun idx -> GHt.copy set.(idx))
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
let setEmptyCnstr () = GHtS.create 128
let setAddState set state =
  GHt.add set.(stateGetSort state) ((stateGetBs state), (stateGetDeferral state)) state
let setAddCore set core =
  GHt.add set.(coreGetSort core) ((coreGetBs core), (coreGetDeferral core)) core
let setAddCnstr set cset = GHtS.add set cset ()
let setMemState set state =
  GHt.mem set.(stateGetSort state) ((stateGetBs state), (stateGetDeferral state))
let setMemCore set core =
  GHt.mem set.(coreGetSort core) ((coreGetBs core), (coreGetDeferral core))
let setMemCnstr set cset = GHtS.mem set cset
let setRemoveState set state =
  GHt.remove set.(stateGetSort state) ((stateGetBs state), (stateGetDeferral state))
let setRemoveCore set core =
  GHt.remove set.(coreGetSort core) ((coreGetBs core), (coreGetDeferral core))
let setRemoveCnstr set cset = GHtS.remove set cset
623
624
let setIterState fkt set = Array.iter (fun ht -> GHt.iter (fun _ x -> fkt x) ht) set
let setIterCore fkt set = Array.iter (fun ht -> GHt.iter (fun _ x -> fkt x) ht) set
625
let setIterCnstr fkt set = GHtS.iter (fun cset () -> fkt cset) set
626
627
let setLengthState seta = Array.fold_left (fun acc set -> acc + GHt.length set) 0 seta
let setLengthCore seta = Array.fold_left (fun acc set -> acc + GHt.length set) 0 seta
Thorsten Wißmann's avatar
Thorsten Wißmann committed
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663


(*****************************************************************************)
(*        "Module type" and a specific implementation of the mapping         *)
(*        between (local) formulae and literals of the sat solver,           *)
(*        and of a mapping of nominals to sets of formulae                   *)
(*****************************************************************************)

let lhtInit () = LHt.create 16
let lhtAdd lht lit f = LHt.add lht lit f
let lhtFind lht lit =
  try
    Some (LHt.find lht lit)
  with Not_found -> None

let fhtInit () = FHt.create 16
let fhtAdd fht f lit = FHt.add fht f lit
let fhtFind fht f =
  try
    Some (FHt.find fht f)
  with Not_found -> None

let nhtInit () = NHt.create 8
let nhtAdd nht nom bs = NHt.add nht nom bs
let nhtFind nht nom =
  try
    Some (NHt.find nht nom)
  with Not_found -> None
let nhtFold fkt nht init = NHt.fold fkt nht init

(*****************************************************************************)
(*         "Module type" and a specific implementation of sets of            *)
(*         local formulae and @-formulae                                     *)
(*****************************************************************************)

let tboxTable = ref (Array.make 0 S.dummyBS)
664
665
let negativeFormulas = ref (Array.make 0 S.dummyBS) (* negative Formulas *)
let tboxDefs  = ref (Array.make 0 (Hashtbl.create 0))  (* Definitions *)
666
let tboxExtensions  = ref (Array.make 0 (Hashtbl.create 0))	(* Extensions *)
Thorsten Wißmann's avatar
Thorsten Wißmann committed
667
668

let bsetMake () = S.makeBS ()
Ludwig Dietel's avatar
Ludwig Dietel committed
669
let bsetDummy () = S.dummyBS
Thorsten Wißmann's avatar
Thorsten Wißmann committed
670
671
let bsetAdd bs lf = S.addBSNoChk bs lf
let bsetMem bs lf = S.memBS bs lf
672
let bsetRem bs lf = S.remBS bs lf
673
let bsetCompare bs1 bs2 = S.compareBS bs1 bs2
674
let bsetUnion bs1 bs2 = S.unionBSNoChk bs1 bs2
675
676
677
678
let bsetMakeRealEmpty () =
    let res = bsetMake () in
    bsetRem res !S.bstrue; (* remove bstrue which is initially in an empty bset *)
    res
Thorsten Wißmann's avatar
Thorsten Wißmann committed
679
let bsetCopy bs = S.copyBS bs
Thorsten Wißmann's avatar
Thorsten Wißmann committed
680
let bsetFold fkt bs init = S.foldBS fkt bs init
681
let bsetReplace fkt bs init = S.foldBS fkt bs init
Thorsten Wißmann's avatar
Thorsten Wißmann committed
682
let bsetIter fkt bset = S.iterBS fkt bset
Thorsten Wißmann's avatar
Thorsten Wißmann committed
683
let bsetFilter (a: bset) (f: localFormula -> bool) : bset =
684
    let res = bsetMakeRealEmpty () in
Thorsten Wißmann's avatar
Thorsten Wißmann committed
685
686
    bsetIter (fun form -> if (f form) then bsetAdd res form else ()) a;
    res
687
688
689
690
691
let bsetPartition (f: localFormula -> bool) (a: bset) : (bset * bset) =
    let left = bsetMakeRealEmpty () in
    let right = bsetMakeRealEmpty () in
    bsetIter (fun form -> if (f form) then bsetAdd left form else bsetAdd right form) a;
    (left, right)
Thorsten Wißmann's avatar
Thorsten Wißmann committed
692

Thorsten Wißmann's avatar
Thorsten Wißmann committed
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
let bsetAddTBox sort bs = S.unionBSNoChk bs !tboxTable.(sort)

let csetCompare cs1 cs2 = S.compareBS cs1 cs2
let csetMake () = S.makeBS ()
let csetAdd cs lf = S.addBSNoChk cs lf
let csetCopy cs = S.copyBS cs
let csetUnion cs1 cs2 = S.unionBSNoChk cs1 cs2
let csetHasDot cs = S.memBS cs !S.bsfalse
let csetAddDot cs = S.addBSNoChk cs !S.bsfalse
let csetRemDot cs = S.remBS cs !S.bsfalse
let csetAddTBox sort cs = S.unionBSNoChk cs !tboxTable.(sort)
let csetIter cs fkt =
  let fkt2 f = if not (f = !S.bstrue || f = !S.bsfalse) then fkt f else () in
  S.iterBS fkt2 cs


(*****************************************************************************)
(*            "Module type" and a specific implementation of                 *)
(*            local formulae and @-formulae                                  *)
(*****************************************************************************)

(** This table maps integers (representing formulae) to their corresponding formulae.
 *)
let arrayFormula = ref (Array.make 0 (Array.make 0 C.TRUE))

(** This table maps integers (representing formulae) to their corresponding type.
 *)
let arrayType = ref (Array.make 0 (Array.make 0 Other))

(** This lookup table maps formulae (represented as integers)
    to their negation (in negation normal form).
 *)
let arrayNeg = ref (Array.make 0 (Array.make 0 (-1)))

(** These lookup tables map formulae (represented as integers)
    to their decompositions (represented as integers).
    This is done according to the rules of the tableau procedure
    and depends on the type of the formulae.
 *)
732
733
 (*
    for PML: arrayDest1 = the subformula
734
735
             arrayNum  = the nominator of the probability
             arrayNum2 = the denominator of the probability
736
 *)
Thorsten Wißmann's avatar
Thorsten Wißmann committed
737
738
739
let arrayDest1 = ref (Array.make 0 (Array.make 0 (-1)))  (* first subformula *)
let arrayDest2 = ref (Array.make 0 (Array.make 0 (-1)))  (* second subformula *)
let arrayDest3 = ref (Array.make 0 (Array.make 0 (-1)))  (* a role *)
740
let arrayDeferral = ref (Array.make 0 (Array.make 0 (-1)))  (* deferral at point *)
Thorsten Wißmann's avatar
Thorsten Wißmann committed
741
let arrayDestNum = ref (Array.make 0 (Array.make 0 (-1)))  (* an integer *)
742
let arrayDestNum2 = ref (Array.make 0 (Array.make 0 (-1)))  (* another integer *)
Thorsten Wißmann's avatar
Thorsten Wißmann committed
743
let arrayDestAg = ref (Array.make 0 (Array.make 0 [|0|])) (* arrays of agents *)
Thorsten Wißmann's avatar
Thorsten Wißmann committed
744
745
746
747
748
749
750
751
752
753

(** This lookup table maps formulae (represented as integers)
    to their @-wrapper.
 *)
let arrayAt = ref (Array.make 0 (Array.make 0 (FHt.create 64)))

let lfGetType sort f = !arrayType.(sort).(f)
let lfGetDest1 sort f = !arrayDest1.(sort).(f)
let lfGetDest2 sort f = !arrayDest2.(sort).(f)
let lfGetDest3 sort f = !arrayDest3.(sort).(f)
754
let lfGetDeferral sort f = !arrayDeferral.(sort).(f)
Thorsten Wißmann's avatar
Thorsten Wißmann committed
755
let lfGetDestNum sort f = !arrayDestNum.(sort).(f)
756
let lfGetDestNum2 sort f = !arrayDestNum2.(sort).(f)
Thorsten Wißmann's avatar
Thorsten Wißmann committed
757
let lfGetDestAg sort f = !arrayDestAg.(sort).(f)
Thorsten Wißmann's avatar
Thorsten Wißmann committed
758
759
760
761
762
let lfGetNeg sort f =
  let nf = !arrayNeg.(sort).(f) in
  if nf >= 0 then Some nf else None
let lfGetAt (sort, nom) f =
  FHt.find !arrayAt.(sort).(f) nom
763
764
let lfToInt lf = lf
let lfFromInt num = num
765
766
let lfGetFormula sort f = !arrayFormula.(sort).(f)

767
768
769
770
771
let escapeHtml (input : string) : string =
  List.fold_right (fun (x, y) (str : string) -> Str.global_replace (Str.regexp x) y str)
    [("<", "&lt;") ; (">", "&gt;") ; ("&", "&amp;")]
    input

772
773
774
775
776
777
778
779
780
781
let bsetToString sort bset : string =
    let toFormula (lf:localFormula) (lst: string list) : string list =
        let formula: C.formula = lfGetFormula sort lf in
        (C.string_of_formula formula) :: lst
    in
    let formulaList = bsetFold toFormula bset [] in
    "{ "^(String.concat ", " formulaList)^" }"

let csetToString sort cset = bsetToString sort cset

782
let coreToString (core:core): string =
783
784
785
786
    let helper cset lst : string list =
        (csetToString core.sortC cset):: lst
    in
    let constraints = cssFold helper core.constraintsC [] in
Thorsten Wißmann's avatar
Thorsten Wißmann committed
787
788
789
    let children =
        List.map (fun (st:state) -> string_of_int st.idx) core.childrenC
    in
790
791
792
    let parents =
        List.map (fun (st,_:state*int) -> string_of_int st.idx) core.parentsC
    in
793
    "Core "^(string_of_int core.idx)^" {\n"^
794
795
    "  Status: " ^ (nodeStatusToString core.statusC) ^ "\n"^
    "  " ^ bsetToString core.sortC core.bsC ^ "\n" ^
796
797
    "  Deferrals: \n" ^
    "    " ^ bsetToString core.sortC core.deferralC ^ "\n" ^
798
799
    "  Constraints: { "^(String.concat
                         "\n                 " constraints)^" }\n"^
Thorsten Wißmann's avatar
Thorsten Wißmann committed
800
801
    "  Children: { "^(String.concat
                         ", " children)^" }\n"^
802
    "  Parents: { "^(String.concat ", " parents)^" }\n"^
803
    "}"
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819

let stateToString (state:state): string =
    let helper cset lst : string list =
        (csetToString state.sortS cset):: lst
    in
    let constraints = cssFold helper state.constraintsS [] in
    let core2idx core = core.idx in
    let fst (a,b) = a in
    let conclusionList =
        List.map (fun (_,lst) ->
                  List.map (fun (core:core) -> string_of_int core.idx) lst
        ) state.childrenS
    in
    let conclusionList =
        List.map (fun x -> "{"^String.concat ", " x^"}") conclusionList
    in
820
821
822
    let parents =
        List.map (fun (co:core) -> string_of_int co.idx) state.parentsS
    in
823
824
825
    "State "^(string_of_int state.idx)^" {\n"^
    "  Status: " ^ (nodeStatusToString state.statusS) ^ "\n"^
    "  " ^ bsetToString state.sortS state.bsS ^ "\n" ^
826
827
    "  Deferrals: \n" ^
    "    " ^ bsetToString state.sortS state.deferralS ^ "\n" ^
828
829
830
831
    "  Constraints: { "^(String.concat
                         "\n                 " constraints)^" }\n"^
    "  Children: { "^(String.concat
                         "\n              " conclusionList)^" }\n"^
832
    "  Parents: { "^(String.concat ", " parents)^" }\n"^
833
834
    "}"

835
let stateToDot (state:state): string =
836
837
838
839
840
841
  let color = match state.statusS with
    | Sat -> "green"
    | Unsat -> "red"
    | Open -> "yellow"
    | Expandable -> "white"
  in
842
843
844
845
846
847
848
  let toFormula (lf:localFormula) (lst: string list) : string list =
    let formula: C.formula = lfGetFormula state.sortS lf in
    if (bsetMem state.deferralS lf)
    then ("<B>"^(escapeHtml (C.string_of_formula formula))^"</B>") :: lst
    else (escapeHtml (C.string_of_formula formula)) :: lst
  in
  let formulaList = bsetFold toFormula state.bsS [] in
849
850
  let ownidx = (string_of_int state.idx) in
  let parents =
851
852
    List.map (fun (co:core) ->
              "Node"^string_of_int co.idx^" -> Node"^ownidx^";")
853
854
             state.parentsS
  in
855
  "Node" ^ ownidx ^ " [shape=ellipse,style=filled,fillcolor=" ^ color
856
857
858
  ^ ",label=<State "  ^ ownidx
  ^ "<BR/>" ^ (String.concat "<BR/>" formulaList)
  ^ ">];\n"
859
860
861
862
  ^ (String.concat "\n" parents)


let coreToDot (core:core): string =
863
864
865
866
867
868
  let color = match core.statusC with
    | Sat -> "green"
    | Unsat -> "red"
    | Open -> "yellow"
    | Expandable -> "white"
  in
869
870
871
872
873
874
875
  let toFormula (lf:localFormula) (lst: string list) : string list =
    let formula: C.formula = lfGetFormula core.sortC lf in
    if (bsetMem core.deferralC lf)
    then ("<B>"^(escapeHtml (C.string_of_formula formula))^"</B>") :: lst
    else (escapeHtml (C.string_of_formula formula)) :: lst
  in
  let formulaList = bsetFold toFormula core.bsC [] in
876
877
  let ownidx = (string_of_int core.idx) in
  let parents =
878
879
    List.map (fun (st,_:state*int) ->
              "Node"^string_of_int st.idx^" -> Node"^ownidx^";")
880
881
             core.parentsC
  in
882
  "Node" ^ ownidx ^ " [shape=ellipse,style=filled,fillcolor=" ^ color
883
884
885
  ^ ",label=<Core "  ^ ownidx
  ^ "<BR/>" ^ (String.concat "<BR/>" formulaList)
  ^ ">];\n"
886
887
888
  ^ (String.concat "\n" parents)


Thorsten Wißmann's avatar
Thorsten Wißmann committed
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
let queuePrettyStatus () =
  let printList (sl : int list) : string =
    String.concat ", " (List.map string_of_int sl)
  in
  (* TODO: are atFormulas always look-up-able for sort 0? *)
  (Printf.sprintf "%d Constraints: " (List.length !queueCnstrs))
  ^(String.concat ", " (List.map (csetToString 0) !queueCnstrs))
  ^(Printf.sprintf "\n%d States: " (List.length !queueStates))
  ^(printList (List.map (fun (st:state) -> st.idx) !queueStates))
  ^(Printf.sprintf "\n%d Cores1: " (List.length !queueCores1))
  ^(printList (List.map (fun (co:core) -> co.idx) !queueCores1))
  ^(Printf.sprintf "\n%d Cores2: " (List.length !queueCores2))
  ^(printList (List.map (fun (co:core) -> co.idx) !queueCores2))
  ^"\n"

904
905


Thorsten Wißmann's avatar
Thorsten Wißmann committed
906
907
908
909
910
911
912
913
914

let atFormulaGetSubformula f = !arrayDest1.(0).(f)
let atFormulaGetNominal f =
  let s = !arrayDest3.(0).(f) in
  let n = !arrayDest2.(0).(f) in
  (s, n)

let lfToAt _ lf = lf

915
916
(* Calculate all possible formulae. This includes all subformulae and
   in the case of μ-Calculus the Fischer-Ladner closure.
Thorsten Wißmann's avatar
Thorsten Wißmann committed
917

918
919
   TODO: variable sort needs to match epected sort
 *)
920
921
922
923
924
925
let rec detClosure vars nomTbl hcF fset vset atset nomset s f =
  let newvars = List.filter (fun (x) -> C.hc_freeIn x f) vars in
  let detClosure_ = detClosure newvars in
  let deferral = if List.length newvars > 0
                 then (List.hd newvars)
                 else "ε" in
Thorsten Wißmann's avatar
Thorsten Wißmann committed
926
927
928
929
  if s < 0 || s >= Array.length fset then
    let sstr = string_of_int s in
    raise (C.CoAlgException ("Invalid sort (i.e. sort out of range): " ^ sstr))
  else ();
930
  if C.HcFHt.mem vset.(s) f &&
931
932
    (compare (C.HcFHt.find vset.(s) f) deferral = 0 ||
        compare deferral "ε" = 0)
933
  then ()
Thorsten Wißmann's avatar
Thorsten Wißmann committed
934
  else
935
    let () = C.HcFHt.add vset.(s) f deferral in
Thorsten Wißmann's avatar
Thorsten Wißmann committed
936
937
938
939
    let () = C.HcFHt.add fset.(s) f () in
    let (func, sortlst) = !sortTable.(s) in
    match f.HC.node with
    | C.HCTRUE
940
941
    | C.HCFALSE
    | C.HCVAR _ -> ()
Thorsten Wißmann's avatar
Thorsten Wißmann committed
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
    | C.HCAP name ->
        if C.isNominal name then begin
          Hashtbl.replace nomset name s;
          match nomTbl name with
          | None -> raise (C.CoAlgException ("Unknown nominal: " ^ name))
          | Some sort ->
              if sort <> s then
                let str1 = "Nominal: " ^ name ^ " of sort " ^ (string_of_int sort) in
                let str2 = " is used in sort " ^ (string_of_int s) ^ "." in
                raise (C.CoAlgException (str1 ^ str2))
              else ()
        end else ()
    | C.HCNOT _ -> ()
    | C.HCAT (name, f1) ->
        C.HcFHt.replace atset f ();
        let s1 =
          match nomTbl name with
          | None -> raise (C.CoAlgException ("Unknown nominal: " ^ name))
          | Some sort -> sort
        in
        let hcnom = C.HcFormula.hashcons hcF (C.HCAP name) in
963
964
        detClosure_ nomTbl hcF fset vset atset nomset s1 hcnom;
        detClosure_ nomTbl hcF fset vset atset nomset s1 f1
Thorsten Wißmann's avatar
Thorsten Wißmann committed
965
966
    | C.HCOR (f1, f2)
    | C.HCAND (f1, f2) ->
967
968
        detClosure_ nomTbl hcF fset vset atset nomset s f1;
        detClosure_ nomTbl hcF fset vset atset nomset s f2
Thorsten Wißmann's avatar
Thorsten Wißmann committed
969
970
    | C.HCEX (_, f1)
    | C.HCAX (_, f1) ->
Ludwig Dietel's avatar
Ludwig Dietel committed
971
        if (func <> MultiModalK && func <> MultiModalKD && func <> Monotone && func <> MultiModalM)
Thorsten Wißmann's avatar
Thorsten Wißmann committed
972
973
            || List.length sortlst <> 1
        then raise (C.CoAlgException "Ex/Ax-formula is used in wrong sort.")
Thorsten Wißmann's avatar
Thorsten Wißmann committed
974
        else ();
975
        detClosure_ nomTbl hcF fset vset atset nomset (List.hd sortlst) f1
Thorsten Wißmann's avatar
Thorsten Wißmann committed
976
977
978
979
980
    | C.HCENFORCES (_, f1)
    | C.HCALLOWS (_, f1) ->
        if func <> CoalitionLogic || List.length sortlst <> 1
        then raise (C.CoAlgException "[{Agents}]-formula is used in wrong sort.")
        else ();
981
        detClosure_ nomTbl hcF fset vset atset nomset (List.hd sortlst) f1
982
983
    | C.HCMORETHAN (_,_,f1)
    | C.HCMAXEXCEPT (_,_,f1) ->
Thorsten Wißmann's avatar
Thorsten Wißmann committed
984
985
986
        if func <> GML || List.length sortlst <> 1
        then raise (C.CoAlgException "[{>=,<=}]-formula is used in wrong sort.")
        else ();
987
        detClosure_ nomTbl hcF fset vset atset nomset (List.hd sortlst) f1
988
    | C.HCATLEASTPROB (_,f1)
989
    | C.HCLESSPROBFAIL (_,f1) ->
990
        if func <> PML || List.length sortlst <> 1
991
        then raise (C.CoAlgException "[{>=,<}]-formula with probability is used in wrong sort.")
992
        else ();
993
        detClosure_ nomTbl hcF fset vset atset nomset (List.hd sortlst) f1;
994
995
996
997
        (*
            TODO: add ¬ f1 to the closure!
        detClosure nomTbl hcF fset atset nomset (List.hd sortlst) (f1.HC.node.negNde)
        *)
998
999
1000
    | C.HCCONST color
    | C.HCCONSTN color ->
      begin match func with
For faster browsing, not all history is shown. View entire blame