Project

General

Profile

Statistics
| Branch: | Revision:

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

History | View | Annotate | Download (12.4 KB)

1
(** The "plug-in" functions for each individual logic.
2
    @author Florian Widmann
3
 *)
4

    
5

    
6
open CoAlgMisc
7
open CoolUtils
8
open CoAlgLogicUtils
9
open Gmlmip
10

    
11
module S = MiscSolver
12

    
13
(** directly return a list of rules **)
14
let mkRuleList_MultiModalK sort bs sl =
15
  assert (List.length sl = 1);
16
  let dep f bsl =                 (* dependencies for formula f (f is a diamond) *)
17
    assert (List.length bsl = 1); (* -+                 *)
18
    let bs1 = List.hd bsl in      (* -+-> [bs1] := bsl  *)
19
    let res = bsetMake () in
20
    bsetAdd res f;
21
    let (role : int) = lfGetDest3 sort f in (* ♥R.? := f, ♥ ∈ {∃,∀} *)
22
    let filterFkt f1 =
23
      if lfGetType sort f1 = AxF && lfGetDest3 sort f1 = role
24
        && bsetMem bs1 (lfGetDest1 sort f1)
25
      then
26
        (* if f1 = ∀R.C and C ∈ bs1 then res = res ∪ {∀R.C} *)
27
        bsetAdd res f1
28
      else ()
29
    in
30
    bsetIter filterFkt bs;
31
    res
32
  in
33
  let getRules f acc =
34
    if lfGetType sort f = ExF then (* f = ∃R.C,i.e. a diamond *)
35
      let bs1 = bsetMake () in
36
      bsetAdd bs1 (lfGetDest1 sort f); (* bs1 := { C }          *)
37
      let (role : int) = lfGetDest3 sort f in (* role := R *)
38
      let filterFkt f1 =
39
        if lfGetType sort f1 = AxF && lfGetDest3 sort f1 = role then
40
          (* if f1 = ∀R.D then bs1 = bs1 ∪ { D } *)
41
          bsetAdd bs1 (lfGetDest1 sort f1)
42
        else ()
43
      in
44
      bsetIter filterFkt bs; (* bs1 := bs1 ∪ { D | some "∀R.D" ∈ bs } *)
45
      let s1 = List.hd sl in (* [s1] := sl *)
46
      let rle = (dep f, [(s1, bs1)]) in
47
      rle::acc
48
    else acc
49
  in
50
  (* effectively:
51
        mkRule_MultiModalK sort bs [s1]
52
            = { ( λ[bs1]. { ∃R.C } ∪ { ∀R.D
53
                                     | ∀R.D ∈ bs, D ∈ bs1
54
                                     }
55
                , [(s1, {C}∪{D | "∀R.D" ∈ bs)]
56
                )
57
              | "∃R.C" ∈ bs
58
              }
59
  *)
60
  bsetFold getRules bs []
61

    
62
let mkRule_MultiModalK sort bs sl =
63
  let rules = mkRuleList_MultiModalK sort bs sl in
64
  let res = ref (Some rules) in
65
  fun () ->
66
    match !res with
67
    | None -> NoMoreRules
68
    | Some rules ->
69
        res := None;
70
        AllInOne rules
71

    
72
(* TODO: test it with:
73
     make && ./coalg sat <<< $'<R> False \n [R] False \n [R] True'
74
*)
75
let mkRule_MultiModalKD sort bs sl =
76
  assert (List.length sl = 1); (* TODO: Why? *)
77
  let s1 = List.hd sl in (* [s1] = List.hd sl *)
78
  let roles = S.makeBS () in
79
  (* step 1: for each ∀R._ add R *)
80
  let addRoleIfBox formula =
81
    if lfGetType sort formula = AxF then
82
      ignore (S.addBS roles (lfGetDest3 sort formula))
83
    else ()
84
  in
85
  bsetIter (addRoleIfBox) bs;
86
  (* step 2: for each ∃R._ remove R again from roles (optimization) *)
87
  let rmRoleIfDiamond formula =
88
    if lfGetType sort formula = ExF then
89
      S.remBS roles (lfGetDest3 sort formula)
90
    else ()
91
  in
92
  bsetIter (rmRoleIfDiamond) bs;
93
  (* step 3: for each R in roles enforce one successor *)
94
  let getRules r acc = (* add the rule for a concrete R *)
95
    let dep r bsl =
96
      assert (List.length bsl = 1); (* -+                 *)
97
      let bs1 = List.hd bsl in      (* -+-> [bs1] := bsl  *)
98
      let res = bsetMake () in (* res := { ∀R.D ∈ bs | D ∈ bs1} *)
99
      let f formula =
100
        if lfGetType sort formula = AxF
101
           && lfGetDest3 sort formula = r
102
           && bsetMem bs1 (lfGetDest1 sort formula)
103
        then ignore (bsetAdd res formula)
104
        else ()
105
      in
106
      bsetIter f bs; (* fill res *)
107
      res
108
    in
109
    let succs = bsetMake () in (* succs := {D | ∀r.D ∈ bs *)
110
    let f formula =
111
      if lfGetType sort formula = AxF
112
         && lfGetDest3 sort formula = r
113
      then ignore (bsetAdd succs (lfGetDest1 sort formula))
114
      else ()
115
    in
116
    bsetIter f bs;
117
    (dep r, [(s1, succs)])::acc
118
  in
119
  (*
120
    mkRule_MultiModalKD sort bs [s1]
121
        = { (λ[bs1]. { ∀R.D ∈ bs | D ∈ bs1}
122
            , [(s1, {D | "∀R.D" ∈ bs)]
123
            )
124
          | R ∈ signature(bs) (or R ∈ roles)
125
          }
126
          ∪ mkRule_MultiModalK sort bs [s1]
127
  *)
128
  let rules = mkRuleList_MultiModalK sort bs sl in
129
  (* extend rules from K with enforcing of successors *)
130
  let rules = S.foldBS getRules roles rules in
131
  (* TODO: replace cannonical wrapper by helper function *)
132
  let res = ref (Some rules) in
133
  fun () ->
134
    match !res with
135
    | None -> NoMoreRules
136
    | Some rules ->
137
        res := None;
138
        AllInOne rules
139

    
140

    
141
(* CoalitionLogic: helper functions *)
142
(*val subset : bitset -> bitset -> bool*)
143
let bsetlen (a: bset) : int =
144
    let res = ref (0) in
145
    bsetIter (fun _ -> res := !res + 1) a;
146
    !res
147

    
148
let subset (a: bset) (b: bset) : bool =
149
    let res = ref (true) in
150
    let f formula =
151
        if bsetMem b formula
152
        then ()
153
        else res := false
154
    in
155
    bsetIter f a;
156
    !res && (bsetlen a < bsetlen b)
157

    
158
let bsetForall (a: bset) (f: CoAlgMisc.localFormula -> bool) : bool =
159
    let res = ref (true) in
160
    let helper formula =
161
        if (f formula) then () else res := false
162
    in
163
    bsetIter helper a;
164
    !res
165

    
166
let bsetExists (a: bset) (f: CoAlgMisc.localFormula -> bool) : bool =
167
    not (bsetForall a (fun x -> not (f x)))
168

    
169
let compatible sort (a: bset) formula1 =
170
    let res = ref (true) in
171
    let f formula2 =
172
        if not (disjointAgents sort formula1 formula2)
173
        then res := false
174
        else ()
175
    in
176
    bsetIter f a;
177
    !res
178

    
179
(*
180
    CoalitionLogic: tableau rules for satisfiability
181

    
182
    Rule 1:
183

    
184
     /\  n
185
    /  \i=1 [C_i] a_i       n ≥ 0,
186
  ——————————————————————    C_i pairwise disjoint
187
     /\  n
188
    /  \i=1  a_i
189

    
190
    Rule 2:
191

    
192
     /\ n                         /\ m
193
    /  \i=1 [C_i] a_i  /\ <D> b  /  \j=1 <N> c_j    n,m ≥ 0
194
  ————————————————————————————————————————————————  C_i pairwise disjoint
195
     /\ n                         /\ m              all C_i ⊆ D
196
    /  \i=1 a_i        /\    b   /  \j=1 c_j
197
*)
198

    
199
let mkRule_CL sort bs sl =
200
  assert (List.length sl = 1); (* TODO: Why? *)
201
  let s1 = List.hd sl in (* [s1] = List.hd sl *)
202
  let boxes = bsetFilter bs (fun f -> lfGetType sort f = EnforcesF) in
203
  let diamonds = bsetFilter bs (fun f -> lfGetType sort f = AllowsF) in
204
  let disjoints = maxDisjoints sort boxes in
205
  let nCands = bsetMakeRealEmpty () in (* all N-diamonds *)
206
  let hasFullAgentList formula =
207
    let aglist = lfGetDestAg sort formula in
208
    let value = TArray.all (fun x -> TArray.elem x aglist) (cl_get_agents ()) in
209
    if (value) then bsetAdd nCands formula else () ;
210
    value
211
  in
212
  (* Candidates for D in Rule 2 *)
213
  let dCands = bsetFilter diamonds (fun f -> not (hasFullAgentList f)) in
214
  let c_j : localFormula list =
215
    bsetFold (fun f a -> (lfGetDest1 sort f)::a) nCands []
216
  in
217
  let getRule2 diamDb acc = (* diamDb = <D> b *)
218
    let d = lfGetDestAg sort diamDb in (* the agent list *)
219
    let b = lfGetDest1 sort diamDb in
220
    let hasAppropriateAglist f =
221
        let aglist = lfGetDestAg sort f in
222
        TArray.included aglist d
223
    in
224
    let maxdisj = maxDisjoints sort (bsetFilter boxes hasAppropriateAglist) in
225
    let createSingleRule acc coalitions =
226
        let a_i : localFormula list =
227
            bsetFold (fun f a -> (lfGetDest1 sort f)::a) coalitions []
228
        in
229
        (* now do rule 2:
230
            coalitions  /\ <d> b /\ nCands
231
           ————————————————————————————————
232
              a_i       /\     b /\ c_j
233
        *)
234
        let children = bsetMakeRealEmpty () in
235
        List.iter (bsetAdd children) (b::c_j) ;
236
        List.iter (bsetAdd children) (a_i) ;
237
        ((fun bs1 -> bs), [(s1, children)])::acc
238
    in
239
    List.fold_left createSingleRule acc maxdisj
240
  in
241
  let rules = bsetFold getRule2 dCands [] in
242
  let getRule1 acc coalitions =
243
    (* do rule 1:
244
        coalitions
245
       ————————————
246
           a_i
247
    *)
248
    let a_i : bset = bsetMakeRealEmpty () in
249
    bsetIter (fun f -> bsetAdd a_i (lfGetDest1 sort f)) coalitions ;
250
    ((fun bs1 -> bs), [(s1, a_i)])::acc
251
  in
252
  let rules = List.fold_left getRule1 rules disjoints in
253
  (*
254
    mkRule_CL sort bs [s1]
255
    = { (λ[bs1]. bs, [(s1, { a_i | i∈I })])
256
        | {[C_i]a_i | i∈I} ⊆ bs,
257
          C_i pairwise disjoint and I maximal
258
        }
259
  *)
260
  (* standard return procedure *)
261
  let res = ref (Some rules) in
262
  fun () ->
263
    match !res with
264
    | None -> NoMoreRules
265
    | Some rules ->
266
        res := None;
267
        AllInOne rules
268

    
269
let mkRule_GML sort bs sl =
270
  assert (List.length sl = 1);
271
  let s1 = List.hd sl in (* [s1] = List.hd sl *)
272
  let diamonds = bsetFilter bs (fun f -> lfGetType sort f = MoreThanF) in
273
  let boxes = bsetFilter bs (fun f -> lfGetType sort f = MaxExceptF) in
274
  let roles = S.makeBS () in
275
  (* step 1: for each diamond/box add R *)
276
  let addRole formula =
277
      ignore (S.addBS roles (lfGetDest3 sort formula))
278
  in
279
  bsetIter addRole boxes;
280
  bsetIter addRole diamonds;
281
  let addRule role acc =
282
      let premise: (bool*int*int) list =
283
        let modality isDiamond m acc =
284
            if lfGetDest3 sort m = role
285
            then (isDiamond,lfGetDestNum sort m,lfToInt (lfGetDest1 sort m))::acc
286
            else acc
287
        in
288
        List.append
289
            (bsetFold (modality true) diamonds [])
290
            (bsetFold (modality false) boxes [])
291
      in
292
      let conclusion = gml_rules premise in
293
      (* conclusion is a set of rules, each of the forman \/ /\ lit *)
294
      let handleRuleConcl rc acc =
295
        let handleConjunction conj =
296
            let res = bsetMake () in
297
            List.iter (fun (f,positive) ->
298
                        let f = lfFromInt f in
299
                        let f = if positive then f else
300
                                    match lfGetNeg sort f with
301
                                    | Some nf -> nf
302
                                    | None -> raise (CoAlgFormula.CoAlgException ("Negation of formula missing"))
303
                                    in
304
                        bsetAdd res f)
305
                      conj;
306
            (s1,res)
307
        in
308
        let rc = List.map handleConjunction rc in
309
        ((fun bs1 -> bs),rc)::acc
310
      in List.fold_right handleRuleConcl conclusion acc
311
  in
312
  let rules = S.foldBS addRule roles [] in
313
  (* standard return procedure *)
314
  let res = ref (Some rules) in
315
  fun () ->
316
    match !res with
317
    | None -> NoMoreRules
318
    | Some rules ->
319
        res := None;
320
        AllInOne rules
321

    
322
let mkRule_Choice sort bs sl =
323
  assert (List.length sl = 2);
324
  let dep bsl =
325
    assert (List.length bsl = 2);
326
    let bs1 = List.nth bsl 0 in
327
    let bs2 = List.nth bsl 1 in
328
    let res = bsetMake () in
329
    let filterFkt f =
330
      if lfGetType sort f = ChcF &&
331
        (bsetMem bs1 (lfGetDest1 sort f) || bsetMem bs2 (lfGetDest2 sort f))
332
      then bsetAdd res f
333
      else ()
334
    in
335
    bsetIter filterFkt bs;
336
    res
337
  in
338
  let bs1 = bsetMake () in
339
  let bs2 = bsetMake () in
340
  let getRule f =
341
    if lfGetType sort f = ChcF then begin
342
      bsetAdd bs1 (lfGetDest1 sort f);
343
      bsetAdd bs2 (lfGetDest2 sort f)
344
    end else ()
345
  in
346
  bsetIter getRule bs;
347
  let s1 = List.nth sl 0 in
348
  let s2 = List.nth sl 1 in
349
  let res = ref (Some [(dep, [(s1, bs1); (s2, bs2)])]) in
350
  fun () ->
351
    match !res with
352
    | None -> NoMoreRules
353
    | Some rules ->
354
        res := None;
355
        AllInOne rules
356

    
357

    
358
let mkRule_Fusion sort bs sl =
359
  assert (List.length sl = 2);
360
  let dep proj bsl =
361
    assert (List.length bsl = 1);
362
    let bs1 = List.hd bsl in
363
    let res = bsetMake () in
364
    let filterFkt f =
365
      if lfGetType sort f = FusF && lfGetDest3 sort f = proj &&
366
        bsetMem bs1 (lfGetDest1 sort f)
367
      then bsetAdd res f
368
      else ()
369
    in
370
    bsetIter filterFkt bs;
371
    res
372
  in
373
  let bs1 = bsetMake () in
374
  let bs2 = bsetMake () in
375
  let getRule f =
376
    if lfGetType sort f = FusF then
377
      if lfGetDest3 sort f = 0 then bsetAdd bs1 (lfGetDest1 sort f)
378
      else bsetAdd bs2 (lfGetDest1 sort f)
379
    else ()
380
  in
381
  bsetIter getRule bs;
382
  let s1 = List.nth sl 0 in
383
  let s2 = List.nth sl 1 in
384
  let res = ref (Some [(dep 0, [(s1, bs1)]); (dep 1, [(s2, bs2)])]) in
385
  fun () ->
386
    match !res with
387
    | None -> NoMoreRules
388
    | Some rules ->
389
        res := None;
390
        AllInOne rules
391

    
392

    
393
(* Maps a logic represented by the type "functors" to the corresponding
394
   "plug-in" function.
395
 *)
396
let getExpandingFunctionProducer = function
397
  | MultiModalK -> mkRule_MultiModalK
398
  | MultiModalKD -> mkRule_MultiModalKD
399
  | CoalitionLogic -> mkRule_CL
400
  | GML -> mkRule_GML
401
  | Choice -> mkRule_Choice
402
  | Fusion -> mkRule_Fusion