## 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 |