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

History | View | Annotate | Download (12.4 KB)

1 | 4fd28192 | Thorsten Wißmann | (** The "plug-in" functions for each individual logic. |
---|---|---|---|

2 | @author Florian Widmann |
||

3 | *) |
||

4 | |||

5 | |||

6 | open CoAlgMisc |
||

7 | e2dc68f7 | Thorsten Wißmann | open CoolUtils |

8 | 7369dd14 | Thorsten Wißmann | open CoAlgLogicUtils |

9 | 60671427 | Thorsten Wißmann | open Gmlmip |

10 | 4fd28192 | Thorsten Wißmann | |

11 | b7445f7e | Thorsten Wißmann | module S = MiscSolver |

12 | 4fd28192 | Thorsten Wißmann | |

13 | b7445f7e | Thorsten Wißmann | (** directly return a list of rules **) |

14 | let mkRuleList_MultiModalK sort bs sl = |
||

15 | 4fd28192 | Thorsten Wißmann | assert (List.length sl = 1); |

16 | e4cd869a | Thorsten Wißmann | let dep f bsl = (* dependencies for formula f (f is a diamond) *) |

17 | 559819d7 | Thorsten Wißmann | assert (List.length bsl = 1); (* -+ *) |

18 | let bs1 = List.hd bsl in (* -+-> [bs1] := bsl *) |
||

19 | 4fd28192 | Thorsten Wißmann | let res = bsetMake () in |

20 | bsetAdd res f; |
||

21 | 559819d7 | Thorsten Wißmann | let (role : int) = lfGetDest3 sort f in (* ♥R.? := f, ♥ ∈ {∃,∀} *) |

22 | 4fd28192 | Thorsten Wißmann | let filterFkt f1 = |

23 | if lfGetType sort f1 = AxF && lfGetDest3 sort f1 = role |
||

24 | && bsetMem bs1 (lfGetDest1 sort f1) |
||

25 | 559819d7 | Thorsten Wißmann | then |

26 | (* if f1 = ∀R.C and C ∈ bs1 then res = res ∪ {∀R.C} *) |
||

27 | bsetAdd res f1 |
||

28 | 4fd28192 | Thorsten Wißmann | else () |

29 | in |
||

30 | bsetIter filterFkt bs; |
||

31 | res |
||

32 | in |
||

33 | let getRules f acc = |
||

34 | e4cd869a | Thorsten Wißmann | if lfGetType sort f = ExF then (* f = ∃R.C,i.e. a diamond *) |

35 | 4fd28192 | Thorsten Wißmann | let bs1 = bsetMake () in |

36 | 559819d7 | Thorsten Wißmann | bsetAdd bs1 (lfGetDest1 sort f); (* bs1 := { C } *) |

37 | let (role : int) = lfGetDest3 sort f in (* role := R *) |
||

38 | 4fd28192 | Thorsten Wißmann | let filterFkt f1 = |

39 | if lfGetType sort f1 = AxF && lfGetDest3 sort f1 = role then |
||

40 | 559819d7 | Thorsten Wißmann | (* if f1 = ∀R.D then bs1 = bs1 ∪ { D } *) |

41 | 4fd28192 | Thorsten Wißmann | bsetAdd bs1 (lfGetDest1 sort f1) |

42 | else () |
||

43 | in |
||

44 | 559819d7 | Thorsten Wißmann | bsetIter filterFkt bs; (* bs1 := bs1 ∪ { D | some "∀R.D" ∈ bs } *) |

45 | let s1 = List.hd sl in (* [s1] := sl *) |
||

46 | 4fd28192 | Thorsten Wißmann | let rle = (dep f, [(s1, bs1)]) in |

47 | rle::acc |
||

48 | else acc |
||

49 | in |
||

50 | 559819d7 | Thorsten Wißmann | (* 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 | b7445f7e | Thorsten Wißmann | bsetFold getRules bs [] |

61 | |||

62 | let mkRule_MultiModalK sort bs sl = |
||

63 | let rules = mkRuleList_MultiModalK sort bs sl in |
||

64 | 4fd28192 | Thorsten Wißmann | 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 | b7445f7e | Thorsten Wißmann | (* TODO: test it with: |

73 | make && ./coalg sat <<< $'<R> False \n [R] False \n [R] True' |
||

74 | *) |
||

75 | a87192e8 | Thorsten Wißmann | let mkRule_MultiModalKD sort bs sl = |

76 | b7445f7e | Thorsten Wißmann | assert (List.length sl = 1); (* TODO: Why? *) |

77 | 2a84977e | Thorsten Wißmann | let s1 = List.hd sl in (* [s1] = List.hd sl *) |

78 | b7445f7e | Thorsten Wißmann | let roles = S.makeBS () in |

79 | (* step 1: for each ∀R._ add R *) |
||

80 | let addRoleIfBox formula = |
||

81 | 2a84977e | Thorsten Wißmann | if lfGetType sort formula = AxF then |

82 | b7445f7e | Thorsten Wißmann | 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 | 2a84977e | Thorsten Wißmann | 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 | b7445f7e | Thorsten Wißmann | in |

116 | 2a84977e | Thorsten Wißmann | bsetIter f bs; |

117 | (dep r, [(s1, succs)])::acc |
||

118 | b7445f7e | Thorsten Wißmann | 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 | a87192e8 | Thorsten Wißmann | 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 | 4fd28192 | Thorsten Wißmann | |

140 | d9fa5123 | Thorsten Wißmann | |

141 | 9793e062 | Thorsten Wißmann | (* 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 | 812ddc5d | Thorsten Wißmann | 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 | b7c3a47e | Thorsten Wißmann | 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 | 812ddc5d | Thorsten Wißmann | |

179 | (* |
||

180 | d9fa5123 | Thorsten Wißmann | 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 | e4cd869a | Thorsten Wißmann | 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 | 45d554b0 | Thorsten Wißmann | let nCands = bsetMakeRealEmpty () in (* all N-diamonds *) |

206 | 5e185dd3 | Thorsten Wißmann | let hasFullAgentList formula = |

207 | let aglist = lfGetDestAg sort formula in |
||

208 | e2dc68f7 | Thorsten Wißmann | let value = TArray.all (fun x -> TArray.elem x aglist) (cl_get_agents ()) in |

209 | 5e185dd3 | Thorsten Wißmann | 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 | 56208143 | Thorsten Wißmann | 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 | 45d554b0 | Thorsten Wißmann | let children = bsetMakeRealEmpty () in |

235 | 56208143 | Thorsten Wißmann | 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 | 45d554b0 | Thorsten Wißmann | let a_i : bset = bsetMakeRealEmpty () in |

249 | 56208143 | Thorsten Wißmann | 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 | d9fa5123 | Thorsten Wißmann | (* |

254 | mkRule_CL sort bs [s1] |
||

255 | 5e185dd3 | Thorsten Wißmann | = { (λ[bs1]. bs, [(s1, { a_i | i∈I })]) |

256 | d9fa5123 | Thorsten Wißmann | | {[C_i]a_i | i∈I} ⊆ bs, |

257 | C_i pairwise disjoint and I maximal |
||

258 | } |
||

259 | *) |
||

260 | 56208143 | Thorsten Wißmann | (* 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 | d9fa5123 | Thorsten Wißmann | |

269 | 29b2e3f3 | Thorsten Wißmann | let mkRule_GML sort bs sl = |

270 | af276a36 | Thorsten Wißmann | assert (List.length sl = 1); |

271 | let s1 = List.hd sl in (* [s1] = List.hd sl *) |
||

272 | 32289e1a | Thorsten Wißmann | 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 | 4706decb | Thorsten Wißmann | 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 | 32289e1a | Thorsten Wißmann | (* 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 | 29b2e3f3 | Thorsten Wißmann | |

322 | 4fd28192 | Thorsten Wißmann | 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 | 2a84977e | Thorsten Wißmann | | MultiModalK -> mkRule_MultiModalK |

398 | b7445f7e | Thorsten Wißmann | | MultiModalKD -> mkRule_MultiModalKD |

399 | d9fa5123 | Thorsten Wißmann | | CoalitionLogic -> mkRule_CL |

400 | 29b2e3f3 | Thorsten Wißmann | | GML -> mkRule_GML |

401 | 4fd28192 | Thorsten Wißmann | | Choice -> mkRule_Choice |

402 | | Fusion -> mkRule_Fusion |