## cool / src / lib / CoAlgFormula.ml @ de84f40d

History | View | Annotate | Download (66.9 KB)

1 |
(** This module implements coalgebraic formulae |
---|---|

2 |
(e.g. parsing, printing, (de-)constructing, ...). |

3 |
@author Florian Widmann |

4 |
*) |

5 | |

6 | |

7 |
module HC = HashConsing |

8 |
module A = AltGenlex |

9 |
module L = List |

10 |
module Str = String |

11 | |

12 | |

13 |
(** A general exception for all kinds of errors |

14 |
that can happen in the tableau procedure. |

15 |
More specific information is given in the argument. |

16 |
*) |

17 |
exception CoAlgException of string |

18 | |

19 |
(** Indicates the sort of a sorted formula |

20 |
*) |

21 |
type sort = int |

22 | |

23 |
type rational = { nominator: int; denominator: int } |

24 | |

25 |
let string_of_rational r = |

26 |
(string_of_int r.nominator)^"/"^(string_of_int r.denominator) |

27 | |

28 |
let rational_of_int n d = { nominator = n; denominator = d } |

29 | |

30 |
(** Defines (unsorted) coalgebraic formulae. |

31 |
*) |

32 |
type formula = |

33 |
| TRUE |

34 |
| FALSE |

35 |
| AP of string (* atomic proposition *) |

36 |
| NOT of formula |

37 |
| AT of string * formula |

38 |
| OR of formula * formula |

39 |
| AND of formula * formula |

40 |
| EQU of formula * formula |

41 |
| IMP of formula * formula |

42 |
| EX of string * formula |

43 |
| AX of string * formula |

44 |
| ENFORCES of int list * formula |

45 |
| ALLOWS of int list * formula |

46 |
| MIN of int * string * formula |

47 |
| MAX of int * string * formula |

48 |
| MORETHAN of int * string * formula (* diamond of GML *) |

49 |
| MAXEXCEPT of int * string * formula (* box of GML *) |

50 |
| ATLEASTPROB of rational * formula (* = {>= 0.5} C ---> C occurs with *) |

51 |
(* probability of at least 50% *) |

52 |
| LESSPROBFAIL of rational * formula (* = [1/2] C = {< 1/2} ¬ C ---> C fails with *) |

53 |
(* probability of less than 50% *) |

54 |
| CONST of string (* constant functor with value string *) |

55 |
| CONSTN of string (* constant functor with value other than string *) |

56 |
| ID of formula (* modality of the identity functor *) |

57 |
| NORM of formula * formula (* default implication *) |

58 |
| NORMN of formula * formula (* \neg NORM (\neg A, \neg B) *) |

59 |
| CHC of formula * formula (* Choice is self-dual *) |

60 |
| FUS of bool * formula |

61 |
| MU of string * formula |

62 |
| NU of string * formula |

63 |
| VAR of string |

64 |
| AF of formula |

65 |
| EF of formula |

66 |
| AG of formula |

67 |
| EG of formula |

68 |
| AU of formula * formula |

69 |
| EU of formula * formula |

70 | |

71 |
exception ConversionException of formula |

72 | |

73 | |

74 |
(** Defines sorted coalgebraic formulae. |

75 |
*) |

76 |
type sortedFormula = sort * formula |

77 | |

78 | |

79 |
(** Determines whether a name indicates a nominal. |

80 |
@param A string s. |

81 |
@return True iff s contains a prime character. |

82 |
*) |

83 |
let isNominal s = String.contains s '\'' |

84 | |

85 | |

86 |
(** Determines the size of a formula. |

87 |
@param f A formula. |

88 |
@return The size of f. |

89 |
*) |

90 |
let rec sizeFormula f = |

91 |
match f with |

92 |
| TRUE |

93 |
| FALSE |

94 |
| AP _ -> 1 |

95 |
| NOT f1 |

96 |
| AT (_, f1) -> succ (sizeFormula f1) |

97 |
| OR (f1, f2) |

98 |
| AND (f1, f2) |

99 |
| EQU (f1, f2) |

100 |
| IMP (f1, f2) -> succ (sizeFormula f1 + sizeFormula f2) |

101 |
| EX (_, f1) |

102 |
| AX (_, f1) |

103 |
| ENFORCES (_, f1) |

104 |
| ALLOWS (_, f1) -> succ (sizeFormula f1) |

105 |
| MIN (_, _, f1) |

106 |
| MAX (_, _, f1) |

107 |
| ATLEASTPROB (_, f1) |

108 |
| LESSPROBFAIL (_, f1) |

109 |
| MORETHAN (_, _, f1) |

110 |
| MAXEXCEPT (_, _, f1) -> succ (sizeFormula f1) |

111 |
| ID (f1) -> succ (sizeFormula f1) |

112 |
| NORM(f1, f2) |

113 |
| NORMN(f1, f2) -> succ (sizeFormula f1 + sizeFormula f2) |

114 |
| CONST _ |

115 |
| CONSTN _ -> 1 |

116 |
| CHC (f1, f2) -> succ (sizeFormula f1 + sizeFormula f2) |

117 |
| FUS (_, f1) -> succ (sizeFormula f1) |

118 |
| MU (_, f1) |

119 |
| NU (_, f1) -> succ (succ (sizeFormula f1)) |

120 |
| VAR _ -> 1 |

121 |
| AF _ | EF _ |

122 |
| AG _ | EG _ |

123 |
| AU _ | EU _ -> |

124 |
raise (CoAlgException ("sizeFormula: CTL should have been removed at this point")) |

125 | |

126 |
(** Determines the size of a sorted formula. |

127 |
@param f A sorted formula. |

128 |
@return The size of f. |

129 |
*) |

130 |
let sizeSortedFormula f = sizeFormula (snd f) |

131 | |

132 | |

133 |
(* think of func: (formula -> unit) -> formula -> unit as identity. |

134 |
iterate over all subformulae and collect side effects. *) |

135 |
let rec iter func formula = |

136 |
func formula; |

137 |
let proc = iter func in (* proc = "process" *) |

138 |
match formula with |

139 |
| TRUE | FALSE | AP _ | VAR _ -> () |

140 |
| CONST _ |

141 |
| CONSTN _ -> () |

142 |
| NOT a | AT (_,a) |

143 |
| EX (_,a) | AX (_,a) -> proc a |

144 |
| OR (a,b) | AND (a,b) |

145 |
| EQU (a,b) | IMP (a,b) -> (proc a ; proc b) |

146 |
| ENFORCES (_,a) | ALLOWS (_,a) |

147 |
| MIN (_,_,a) | MAX (_,_,a) |

148 |
| ATLEASTPROB (_, a) | LESSPROBFAIL (_, a) |

149 |
| MORETHAN (_,_,a) | MAXEXCEPT (_,_,a) -> proc a |

150 |
| ID(a) -> proc a |

151 |
| NORM(a, b) | NORMN(a, b) -> (proc a; proc b) |

152 |
| CHC (a,b) -> (proc a ; proc b) |

153 |
| FUS (_,a) -> proc a |

154 |
| MU (_, f) | NU (_, f) -> proc f |

155 |
| AF f | EF f | AG f | EG f -> proc f |

156 |
| AU (f1, f2) | EU (f1, f2) -> (proc f1; proc f2) |

157 | |

158 |
let rec convert_post func formula = (* run over all subformulas in post order *) |

159 |
let c = convert_post func in (* some shorthand *) |

160 |
(* replace parts of the formula *) |

161 |
let formula = (match formula with |

162 |
(* 0-ary constructors *) |

163 |
| TRUE | FALSE | AP _ | VAR _ -> formula |

164 |
| CONST _ |

165 |
| CONSTN _ -> formula |

166 |
(* unary *) |

167 |
| NOT a -> NOT (c a) |

168 |
| AT (s,a) -> AT (s,c a) |

169 |
(* binary *) |

170 |
| OR (a,b) -> OR (c a, c b) |

171 |
| AND (a,b) -> AND (c a, c b) |

172 |
| EQU (a,b) -> EQU (c a, c b) |

173 |
| IMP (a,b) -> IMP (c a, c b) |

174 |
| EX (s,a) -> EX (s,c a) |

175 |
| AX (s,a) -> AX (s,c a) |

176 |
| ENFORCES (s,a) -> ENFORCES (s,c a) |

177 |
| ALLOWS (s,a) -> ALLOWS (s,c a) |

178 |
| MIN (n,s,a) -> MIN (n,s,c a) |

179 |
| MAX (n,s,a) -> MAX (n,s,c a) |

180 |
| ATLEASTPROB (p,a) -> ATLEASTPROB (p, c a) |

181 |
| LESSPROBFAIL (p,a) -> LESSPROBFAIL (p, c a) |

182 |
| MORETHAN (n,s,a) -> MORETHAN (n,s,c a) |

183 |
| MAXEXCEPT (n,s,a) -> MAXEXCEPT (n,s,c a) |

184 |
| ID(a) -> ID (c a) |

185 |
| NORM(a, b) -> NORM(c a, c b) |

186 |
| NORMN(a, b) -> NORMN(c a, c b) |

187 |
| CHC (a,b) -> CHC (c a, c b) |

188 |
| FUS (s,a) -> FUS (s, c a) |

189 |
| MU (n, f1) -> MU (n, c f1) |

190 |
| NU (n, f1) -> NU (n, c f1) |

191 |
| AF f1 -> AF (c f1) |

192 |
| EF f1 -> EF (c f1) |

193 |
| AG f1 -> AG (c f1) |

194 |
| EG f1 -> EG (c f1) |

195 |
| AU (f1, f2) -> AU (c f1, c f2) |

196 |
| EU (f1, f2) -> AU (c f1, c f2))in |

197 |
func formula |

198 | |

199 |
let convertToK formula = (* tries to convert a formula to a pure K formula *) |

200 |
let helper formula = match formula with |

201 |
| ENFORCES _ | ALLOWS _ -> raise (ConversionException formula) |

202 |
| MORETHAN (0,s,a) | MIN (1,s,a) -> EX (s,a) |

203 |
| MAX (0,s,a) -> AX (s, NOT a) |

204 |
| MAXEXCEPT (0,s,a) -> AX (s, a) |

205 |
| TRUE | FALSE |

206 |
| EQU _ | IMP _ |

207 |
| AND _ | OR _ |

208 |
| AP _ | NOT _ |

209 |
| AX _ | EX _ |

210 |
| CHC _ | FUS _ -> formula |

211 |
| _ -> raise (ConversionException formula) |

212 |
in |

213 |
convert_post helper formula |

214 | |

215 |
let convertToGML formula = (* tries to convert a formula to a pure GML formula *) |

216 |
let helper formula = match formula with |

217 |
| ENFORCES _ | ALLOWS _ -> raise (ConversionException formula) |

218 |
| MORETHAN _ | MIN _ | MAX _ | MAXEXCEPT _ -> formula |

219 |
| TRUE | FALSE |

220 |
| EQU _ | IMP _ |

221 |
| AND _ | OR _ |

222 |
| AP _ | NOT _ |

223 |
| CHC _ | FUS _ -> formula |

224 |
| AX (r,a) -> MAXEXCEPT (0,r,a) |

225 |
| EX (r,a) -> MORETHAN (0,r,a) |

226 |
| _ -> raise (ConversionException formula) |

227 |
in |

228 |
convert_post helper formula |

229 | |

230 |
let gensym = Stream.from (fun i -> Some (Printf.sprintf "#gensym%x#" i)) |

231 | |

232 |
let convertToMu formula = |

233 |
let helper formula = |

234 |
match formula with |

235 |
| AF f1 -> |

236 |
MU ("#AF#", (OR (f1, (AX ("", (VAR "#AF#")))))) |

237 |
| EF f1 -> |

238 |
MU ("#EF#", (OR (f1, (EX ("", (VAR "#EF#")))))) |

239 |
| AG f1 -> |

240 |
NU ("#AG#", (AND (f1, (AX ("", (VAR "#AG#")))))) |

241 |
| EG f1 -> |

242 |
NU ("#EG#", (AND (f1, (EX ("", (VAR "#EG#")))))) |

243 |
| AU (f1, f2) -> |

244 |
MU ("#AU#", (OR (f2, (AND (f1, (AX ("", (VAR "#AU#")))))))) |

245 |
| EU (f1, f2) -> |

246 |
MU ("#EU#", (OR (f2, (AND (f1, (EX ("", (VAR "#EU#")))))))) |

247 |
| _ -> formula |

248 |
in |

249 |
convert_post helper formula |

250 | |

251 |
(** Appends a string representation of a formula to a string buffer. |

252 |
Parentheses are ommited where possible |

253 |
where the preference rules are defined as usual. |

254 |
@param sb A string buffer. |

255 |
@param f A formula. |

256 |
*) |

257 |
let rec exportFormula_buffer sb f = |

258 |
let negate = function |

259 |
| NOT f -> f |

260 |
| f -> NOT f |

261 |
in |

262 |
let prio n lf = |

263 |
let prionr = function |

264 |
| EQU _ -> 0 |

265 |
| IMP _ -> 1 |

266 |
| OR _ -> 2 |

267 |
| AND _ -> 3 |

268 |
| _ -> 4 |

269 |
in |

270 |
if prionr lf < n then begin |

271 |
Buffer.add_char sb '('; |

272 |
exportFormula_buffer sb lf; |

273 |
Buffer.add_char sb ')' |

274 |
end |

275 |
else exportFormula_buffer sb lf |

276 |
in |

277 |
match f with |

278 |
| TRUE -> Buffer.add_string sb "True" |

279 |
| FALSE -> Buffer.add_string sb "False" |

280 |
| AP s -> Buffer.add_string sb s |

281 |
| NOT f1 -> |

282 |
Buffer.add_string sb "~"; |

283 |
prio 4 f1 |

284 |
| AT (s, f1) -> |

285 |
Buffer.add_string sb "@ "; |

286 |
Buffer.add_string sb s; |

287 |
Buffer.add_string sb " "; |

288 |
prio 4 f1 |

289 |
| OR (f1, f2) -> |

290 |
prio 2 f1; |

291 |
Buffer.add_string sb " | "; |

292 |
prio 2 f2 |

293 |
| AND (f1, f2) -> |

294 |
prio 3 f1; |

295 |
Buffer.add_string sb " & "; |

296 |
prio 3 f2 |

297 |
| EQU (f1, f2) -> |

298 |
prio 0 f1; |

299 |
Buffer.add_string sb " <=> "; |

300 |
prio 0 f2 |

301 |
| IMP (f1, f2) -> |

302 |
prio 2 f1; |

303 |
Buffer.add_string sb " => "; |

304 |
prio 2 f2 |

305 |
| EX (s, f1) -> |

306 |
Buffer.add_string sb "<"; |

307 |
Buffer.add_string sb s; |

308 |
Buffer.add_string sb ">"; |

309 |
prio 4 f1 |

310 |
| AX (s, f1) -> |

311 |
Buffer.add_string sb "["; |

312 |
Buffer.add_string sb s; |

313 |
Buffer.add_string sb "]"; |

314 |
prio 4 f1 |

315 |
| ALLOWS (s, f1) -> |

316 |
Buffer.add_string sb "<{"; |

317 |
Buffer.add_string sb ( |

318 |
match s with |

319 |
| [] -> " " |

320 |
| _ ->(Str.concat " " (L.map string_of_int s)) |

321 |
); |

322 |
Buffer.add_string sb "}>"; |

323 |
prio 4 f1 |

324 |
| ENFORCES (s, f1) -> |

325 |
Buffer.add_string sb "[{"; |

326 |
Buffer.add_string sb ( |

327 |
match s with |

328 |
| [] -> " " |

329 |
| _ ->(Str.concat " " (L.map string_of_int s)) |

330 |
); |

331 |
Buffer.add_string sb "}]"; |

332 |
prio 4 f1 |

333 |
| ATLEASTPROB (p, f1) -> |

334 |
Buffer.add_string sb "{>="; |

335 |
Buffer.add_string sb (string_of_rational p); |

336 |
Buffer.add_string sb "}"; |

337 |
prio 4 f1 |

338 |
| LESSPROBFAIL (p, f1) -> |

339 |
Buffer.add_string sb "{<"; |

340 |
Buffer.add_string sb (string_of_rational p); |

341 |
Buffer.add_string sb "} ~ "; |

342 |
prio 4 f1 |

343 |
| MIN (n, s, f1) -> |

344 |
Buffer.add_string sb "{>="; |

345 |
Buffer.add_string sb (string_of_int n); |

346 |
Buffer.add_string sb " "; |

347 |
Buffer.add_string sb s; |

348 |
Buffer.add_string sb "}"; |

349 |
prio 4 f1 |

350 |
| MAX (n, s, f1) -> |

351 |
Buffer.add_string sb "{<="; |

352 |
Buffer.add_string sb (string_of_int n); |

353 |
Buffer.add_string sb " "; |

354 |
Buffer.add_string sb s; |

355 |
Buffer.add_string sb "}"; |

356 |
prio 4 f1 |

357 |
| MORETHAN (n, s, f1) -> |

358 |
Buffer.add_string sb "{>"; |

359 |
Buffer.add_string sb (string_of_int n); |

360 |
Buffer.add_string sb " "; |

361 |
Buffer.add_string sb s; |

362 |
Buffer.add_string sb "}"; |

363 |
prio 4 f1 |

364 |
| MAXEXCEPT (n, s, f1) -> |

365 |
Buffer.add_string sb "{<="; |

366 |
Buffer.add_string sb (string_of_int n); |

367 |
Buffer.add_string sb " ~ "; |

368 |
Buffer.add_string sb s; |

369 |
Buffer.add_string sb "}"; |

370 |
prio 4 f1 (* actually is prio of ~ and not of <= *) |

371 |
| ID (f1) -> |

372 |
Buffer.add_string sb "O"; |

373 |
prio 4 f1 |

374 |
| NORM(f1, f2) -> |

375 |
Buffer.add_string sb "("; |

376 |
exportFormula_buffer sb f1; |

377 |
Buffer.add_string sb " =o "; |

378 |
exportFormula_buffer sb f2; |

379 |
Buffer.add_string sb ")" |

380 |
| NORMN(f1, f2) -> |

381 |
Buffer.add_string sb "~("; |

382 |
exportFormula_buffer sb (negate f1); |

383 |
Buffer.add_string sb " =o "; |

384 |
exportFormula_buffer sb (negate f2); |

385 |
Buffer.add_string sb ")" |

386 |
| CHC (f1, f2) -> |

387 |
Buffer.add_string sb "("; |

388 |
exportFormula_buffer sb f1; |

389 |
Buffer.add_string sb " + "; |

390 |
exportFormula_buffer sb f2; |

391 |
Buffer.add_string sb ")" |

392 |
| CONST s -> Buffer.add_string sb "="; |

393 |
Buffer.add_string sb s |

394 |
| CONSTN s -> Buffer.add_string sb "~="; |

395 |
Buffer.add_string sb s |

396 |
| FUS (first, f1) -> |

397 |
Buffer.add_string sb (if first then "[pi1]" else "[pi2]"); |

398 |
prio 4 f1 |

399 |
| MU (s, f1) -> |

400 |
Buffer.add_string sb "μ"; |

401 |
Buffer.add_string sb s; |

402 |
Buffer.add_string sb "."; |

403 |
prio 4 f1 |

404 |
| NU (s, f1) -> |

405 |
Buffer.add_string sb "ν"; |

406 |
Buffer.add_string sb s; |

407 |
Buffer.add_string sb "."; |

408 |
prio 4 f1 |

409 |
| VAR s -> |

410 |
Buffer.add_string sb s |

411 |
| AF f1 -> |

412 |
Buffer.add_string sb "AF "; |

413 |
prio 4 f1 |

414 |
| EF f1 -> |

415 |
Buffer.add_string sb "EF "; |

416 |
prio 4 f1 |

417 |
| AG f1 -> |

418 |
Buffer.add_string sb "AG "; |

419 |
prio 4 f1 |

420 |
| EG f1 -> |

421 |
Buffer.add_string sb "EG "; |

422 |
prio 4 f1 |

423 |
| AU (f1, f2) -> |

424 |
Buffer.add_string sb "A ("; |

425 |
prio 4 f1; |

426 |
Buffer.add_string sb " U "; |

427 |
prio 4 f2; |

428 |
Buffer.add_string sb ")" |

429 |
| EU (f1, f2) -> |

430 |
Buffer.add_string sb "E ("; |

431 |
prio 4 f1; |

432 |
Buffer.add_string sb " U "; |

433 |
prio 4 f2; |

434 |
Buffer.add_string sb ")" |

435 | |

436 |
(** Converts a formula into a string representation. |

437 |
Parentheses are ommited where possible |

438 |
where the preference rules are defined as usual. |

439 |
@param f A formula. |

440 |
@return A string representing f. |

441 |
*) |

442 |
let exportFormula f = |

443 |
let sb = Buffer.create 128 in |

444 |
exportFormula_buffer sb f; |

445 |
Buffer.contents sb |

446 | |

447 |
let string_of_formula = exportFormula |

448 | |

449 |
(** export (CL)-formula suitable for tatl-inputs *) |

450 |
let rec exportTatlFormula_buffer sb f = |

451 |
let prio n lf = |

452 |
let prionr = function |

453 |
| EQU _ -> 0 |

454 |
| IMP _ -> 1 |

455 |
| OR _ -> 2 |

456 |
| AND _ -> 3 |

457 |
| _ -> 4 |

458 |
in |

459 |
if prionr lf < n then begin |

460 |
Buffer.add_char sb '('; |

461 |
exportTatlFormula_buffer sb lf; |

462 |
Buffer.add_char sb ')' |

463 |
end |

464 |
else exportTatlFormula_buffer sb lf |

465 |
in |

466 |
match f with |

467 |
| TRUE -> Buffer.add_string sb "(p \\/ ~p)" |

468 |
| FALSE -> Buffer.add_string sb "(p /\\ ~p)" |

469 |
| AP s -> Buffer.add_string sb s |

470 |
| NOT f1 -> |

471 |
Buffer.add_string sb "~"; |

472 |
prio 4 f1 |

473 |
| OR (f1, f2) -> |

474 |
prio 2 f1; |

475 |
Buffer.add_string sb " \\/ "; |

476 |
prio 2 f2 |

477 |
| AND (f1, f2) -> |

478 |
prio 3 f1; |

479 |
Buffer.add_string sb " /\\ "; |

480 |
prio 3 f2 |

481 |
| EQU (f1, f2) -> |

482 |
prio 0 (AND (IMP (f1,f2), IMP (f2,f1))) |

483 |
| IMP (f1, f2) -> |

484 |
prio 2 f1; |

485 |
Buffer.add_string sb " -> "; |

486 |
prio 2 f2 |

487 |
| ALLOWS (s, f1) -> |

488 |
Buffer.add_string sb "<<"; |

489 |
Buffer.add_string sb ( |

490 |
match s with |

491 |
| [] -> " " |

492 |
| _ ->(Str.concat "," (L.map string_of_int s)) |

493 |
); |

494 |
Buffer.add_string sb ">>X "; |

495 |
prio 4 f1 |

496 |
| ENFORCES (s, f1) -> |

497 |
Buffer.add_string sb "~<<"; |

498 |
Buffer.add_string sb ( |

499 |
match s with |

500 |
| [] -> " " |

501 |
| _ ->(Str.concat "," (L.map string_of_int s)) |

502 |
); |

503 |
Buffer.add_string sb ">>X ~ "; |

504 |
prio 4 f1 |

505 |
| EX _ |

506 |
| AX _ |

507 |
| MIN _ |

508 |
| MAX _ |

509 |
| MORETHAN _ |

510 |
| MAXEXCEPT _ |

511 |
| AT _ |

512 |
| CONST _ |

513 |
| CONSTN _ |

514 |
| CHC _ |

515 |
| ATLEASTPROB _ |

516 |
| LESSPROBFAIL _ |

517 |
| ID _ |

518 |
| NORM _ |

519 |
| NORMN _ |

520 |
| FUS _ |

521 |
| MU _ |

522 |
| NU _ |

523 |
| VAR _ |

524 |
| AF _ |

525 |
| EF _ |

526 |
| AG _ |

527 |
| EG _ |

528 |
| AU _ |

529 |
| EU _ -> raise (CoAlgException ("export to tatl: Not connectives of CL")) |

530 | |

531 |
let exportTatlFormula f = |

532 |
let sb = Buffer.create 128 in |

533 |
exportTatlFormula_buffer sb f; |

534 |
Buffer.contents sb |

535 | |

536 |
(** Appends a string representation of a sorted formula to a string buffer. |

537 |
Parentheses are ommited where possible |

538 |
where the preference rules are defined as usual. |

539 |
@param sb A string buffer. |

540 |
@param (s, f) A sorted formula. |

541 |
*) |

542 |
let rec exportSortedFormula_buffer sb (s, f) = |

543 |
Buffer.add_string sb (string_of_int s); |

544 |
Buffer.add_string sb ": "; |

545 |
exportFormula_buffer sb f |

546 | |

547 |
(** Converts a sorted formula into a string representation. |

548 |
Parentheses are ommited where possible |

549 |
where the preference rules are defined as usual. |

550 |
@param f A sorted formula. |

551 |
@return A string representing f. |

552 |
*) |

553 |
let exportSortedFormula f = |

554 |
let sb = Buffer.create 128 in |

555 |
exportSortedFormula_buffer sb f; |

556 |
Buffer.contents sb |

557 | |

558 |
(** Converts a (sorted) formula query into a string representation. |

559 |
@param tbox A list of sorted formulae representing a TBox. |

560 |
@param f A sorted formula. |

561 |
@return A string representing tbox |- f. |

562 |
*) |

563 |
let exportQuery tbox f = |

564 |
let sb = Buffer.create 1000 in |

565 |
let rec expFl = function |

566 |
| [] -> () |

567 |
| h::tl -> |

568 |
exportSortedFormula_buffer sb h; |

569 |
if tl <> [] then Buffer.add_string sb "; " else (); |

570 |
expFl tl |

571 |
in |

572 |
expFl tbox; |

573 |
Buffer.add_string sb " |- "; |

574 |
exportSortedFormula_buffer sb f; |

575 |
Buffer.contents sb |

576 | |

577 |
(** Converts a (sorted) formula query into a string representation. Such that |

578 |
coalg can read it again using importQuery |

579 |
@param tbox A list of sorted formulae representing a TBox. |

580 |
@param f A sorted formula. |

581 |
@return A string representing tbox |- f. |

582 |
*) |

583 |
let exportQueryParsable tbox (_,f) = |

584 |
let sb = Buffer.create 1000 in |

585 |
let rec expFl = function |

586 |
| [] -> () |

587 |
| (_,h)::tl -> |

588 |
exportFormula_buffer sb h; |

589 |
if tl <> [] then Buffer.add_string sb "; " else (); |

590 |
expFl tl |

591 |
in |

592 |
expFl tbox; |

593 |
Buffer.add_string sb " |- "; |

594 |
exportFormula_buffer sb f; |

595 |
Buffer.contents sb |

596 | |

597 | |

598 |
(* NB: True and False are the propositional constants. Lower case |

599 |
true/false are regardes as atomic propositions and we emit a warning |

600 |
*) |

601 |
let lexer = A.make_lexer |

602 |
[":";";";"|-";"(";")";"=>";"<=>";"|";"&";"~";"@";"True";"False";"true";"false";"<";">";"[";"]";"{<=";"{>=";"}";"+";"[pi1]";"[pi2]" |

603 |
;"[{";"}]";"<{";"}>";",";"/";"{<";"=";"=o";"O" |

604 |
;"μ";"ν";"." |

605 |
;"AX";"EX";"AF";"EF";"AG";"EG";"A";"E";"U" |

606 |
] |

607 | |

608 |
let mk_exn s = CoAlgException s |

609 | |

610 |
(** Process from inside out. cons all variables seen, remove them when |

611 |
binding fixpoint is found. Fixpoint type may only change if last |

612 |
(inner) fixpoint didn't include any free variables. |

613 |
*) |

614 |
let rec verifyMuAltFree formula = |

615 |
let proc = verifyMuAltFree in |

616 |
match formula with |

617 |
| TRUE | FALSE | AP _ -> ("none", []) |

618 |
| CONST _ |

619 |
| CONSTN _ -> ("none", []) |

620 |
| AT (_,a) | NOT a |

621 |
| EX (_,a) | AX (_,a) -> proc a |

622 |
| OR (a,b) | AND (a,b) |

623 |
| EQU (a,b) | IMP (a,b) -> |

624 |
let (atype, afree) = proc a |

625 |
and (btype, bfree) = proc b in |

626 |
if (compare atype "μ" == 0 && compare btype "ν" == 0) || |

627 |
(compare atype "ν" == 0 && compare btype "μ" == 0) then |

628 |
raise (CoAlgException ("formula not alternation-free")); |

629 |
if compare atype "none" == 0 then |

630 |
(btype, List.flatten [afree; bfree]) |

631 |
else |

632 |
(atype, List.flatten [afree; bfree]) |

633 |
| ENFORCES (_,a) | ALLOWS (_,a) |

634 |
| MIN (_,_,a) | MAX (_,_,a) |

635 |
| ATLEASTPROB (_, a) | LESSPROBFAIL (_, a) |

636 |
| MORETHAN (_,_,a) | MAXEXCEPT (_,_,a) -> proc a |

637 |
| ID(a) -> proc a |

638 |
| NORM(a, b) | NORMN(a, b) |

639 |
| CHC (a,b) -> |

640 |
let (atype, afree) = proc a |

641 |
and (btype, bfree) = proc b in |

642 |
if (compare atype "μ" == 0 && compare btype "ν" == 0) || |

643 |
(compare atype "ν" == 0 && compare btype "μ" == 0) then |

644 |
raise (CoAlgException ("formula not alternation-free")); |

645 |
if compare atype "none" == 0 then |

646 |
(btype, List.flatten [afree; bfree]) |

647 |
else |

648 |
(atype, List.flatten [afree; bfree]) |

649 |
| FUS (_,a) -> proc a |

650 |
| MU (s, f) -> |

651 |
let (fptype, free) = proc f in |

652 |
(if (compare fptype "ν" == 0) then |

653 |
raise (CoAlgException ("formula not alternation-free"))); |

654 |
let predicate x = compare x s != 0 in |

655 |
let newfree = List.filter predicate free in |

656 |
if newfree = [] then |

657 |
("none", []) |

658 |
else |

659 |
("μ", newfree) |

660 |
| NU (s, f) -> |

661 |
let (fptype, free) = proc f in |

662 |
(if (compare fptype "μ" == 0) then |

663 |
raise (CoAlgException ("formula not alternation-free"))); |

664 |
let predicate x = compare x s != 0 in |

665 |
let newfree = List.filter predicate free in |

666 |
if newfree = [] then |

667 |
("none", []) |

668 |
else |

669 |
("ν", newfree) |

670 |
| VAR s -> ("none", [s]) |

671 |
| AF _ | EF _ | AG _ | EG _ | AU _ | EU _ -> |

672 |
raise (CoAlgException ("verifyMuAltFree: CTL should have been removed at this point")) |

673 | |

674 | |

675 |
(** Process from outside in. For every variable bound keep the tuple |

676 |
(name, negations). For every negation crossed map a +1 over snd on |

677 |
that list. For every variable met check that the matching |

678 |
negations is even. |

679 |
*) |

680 |
let rec verifyMuMonotone negations formula = |

681 |
let proc = verifyMuMonotone negations in |

682 |
match formula with |

683 |
| TRUE | FALSE | AP _ -> () |

684 |
| CONST _ |

685 |
| CONSTN _ -> () |

686 |
| AT (_,a) |

687 |
| EX (_,a) | AX (_,a) -> proc a |

688 |
| OR (a,b) | AND (a,b) |

689 |
| EQU (a,b) | IMP (a,b) -> (proc a ; proc b) |

690 |
| ENFORCES (_,a) | ALLOWS (_,a) |

691 |
| MIN (_,_,a) | MAX (_,_,a) |

692 |
| ATLEASTPROB (_, a) | LESSPROBFAIL (_, a) |

693 |
| MORETHAN (_,_,a) | MAXEXCEPT (_,_,a) -> proc a |

694 |
| ID(a) -> proc a |

695 |
| NORM(a, b) | NORMN(a, b) -> (proc a; proc b) |

696 |
| CHC (a,b) -> (proc a ; proc b) |

697 |
| FUS (_,a) -> proc a |

698 |
| MU (s, f) |

699 |
| NU (s, f) -> |

700 |
let newNeg = (s, 0) :: negations in |

701 |
verifyMuMonotone newNeg f |

702 |
| VAR s -> |

703 |
let finder (x, _) = compare x s == 0 in |

704 |
let (_, neg) = List.find finder negations in |

705 |
if ((neg land 1) != 0) then raise (CoAlgException ("formula not monotone")) |

706 |
| NOT a -> |

707 |
let increment (s, n) = (s, n+1) in |

708 |
let newNeg = List.map increment negations in |

709 |
verifyMuMonotone newNeg a |

710 |
| AF _ | EF _ | AG _ | EG _ | AU _ | EU _ -> |

711 |
raise (CoAlgException ("verifyMuMonotone: CTL should have been removed at this point")) |

712 | |

713 |
let rec verifyMuGuarded unguarded formula = |

714 |
let proc = verifyMuGuarded unguarded in |

715 |
match formula with |

716 |
| TRUE | FALSE | AP _ -> () |

717 |
| CONST _ |

718 |
| CONSTN _ -> () |

719 |
| AT (_,a) | NOT a -> proc a |

720 |
| EX (_,a) | AX (_,a) -> verifyMuGuarded [] a |

721 |
| OR (a,b) | AND (a,b) |

722 |
| EQU (a,b) | IMP (a,b) -> (proc a ; proc b) |

723 |
| ENFORCES (_,a) | ALLOWS (_,a) |

724 |
| MIN (_,_,a) | MAX (_,_,a) |

725 |
| ATLEASTPROB (_, a) | LESSPROBFAIL (_, a) |

726 |
| MORETHAN (_,_,a) | MAXEXCEPT (_,_,a) -> proc a |

727 |
| ID(a) -> proc a |

728 |
| NORM(a, b) | NORMN(a, b) -> (proc a; proc b) |

729 |
| CHC (a,b) -> (proc a ; proc b) |

730 |
| FUS (_,a) -> proc a |

731 |
| MU (s, f) |

732 |
| NU (s, f) -> |

733 |
let newUnguard = s :: unguarded in |

734 |
verifyMuGuarded newUnguard f |

735 |
| VAR s -> |

736 |
let finder x = compare x s == 0 in |

737 |
if List.exists finder unguarded then |

738 |
raise (CoAlgException ("formula not guarded")) |

739 |
| AF _ | EF _ | AG _ | EG _ | AU _ | EU _ -> |

740 |
raise (CoAlgException ("verifyMuGuarded: CTL should have been removed at this point")) |

741 | |

742 |
let verifyFormula formula = |

743 |
verifyMuAltFree formula; |

744 |
verifyMuMonotone [] formula; |

745 |
verifyMuGuarded [] formula |

746 | |

747 |
(** These functions parse a token stream to obtain a formula. |

748 |
It is a standard recursive descent procedure. |

749 |
@param ts A token stream. |

750 |
@return The resulting (sub-)formula. |

751 |
@raise CoAlgException if ts does not represent a formula. |

752 |
*) |

753 |
let rec parse_formula (symtab: 'a list) ts = |

754 |
let formula = (parse_imp symtab ts) in |

755 |
let f1 = convertToMu formula in |

756 |
match Stream.peek ts with |

757 |
| None -> f1 |

758 |
| Some (A.Kwd "<=>") -> |

759 |
Stream.junk ts; |

760 |
let f2 = parse_formula symtab ts in |

761 |
EQU (f1, f2) |

762 |
| _ -> f1 |

763 | |

764 |
(** These functions parse a token stream to obtain a formula. |

765 |
It is a standard recursive descent procedure. |

766 |
@param ts A token stream. |

767 |
@return The resulting (sub-)formula. |

768 |
@raise CoAlgException if ts does not represent a formula. |

769 |
*) |

770 |
and parse_imp symtab ts= |

771 |
let f1 = parse_or symtab ts in |

772 |
match Stream.peek ts with |

773 |
| None -> f1 |

774 |
| Some (A.Kwd "=>") -> |

775 |
Stream.junk ts; |

776 |
let f2 = parse_imp symtab ts in |

777 |
IMP (f1, f2) |

778 |
| _ -> f1 |

779 | |

780 |
(** These functions parse a token stream to obtain a formula. |

781 |
It is a standard recursive descent procedure. |

782 |
@param ts A token stream. |

783 |
@return The resulting (sub-)formula. |

784 |
@raise CoAlgException if ts does not represent a formula. |

785 |
*) |

786 |
and parse_or symtab ts = |

787 |
let f1 = parse_and symtab ts in |

788 |
match Stream.peek ts with |

789 |
| None -> f1 |

790 |
| Some (A.Kwd "|") -> |

791 |
Stream.junk ts; |

792 |
let f2 = parse_or symtab ts in |

793 |
OR (f1, f2) |

794 |
| _ -> f1 |

795 | |

796 |
(** These functions parse a token stream to obtain a formula. |

797 |
It is a standard recursive descent procedure. |

798 |
@param ts A token stream. |

799 |
@return The resulting (sub-)formula. |

800 |
@raise CoAlgException if ts does not represent a formula. |

801 |
*) |

802 |
and parse_and symtab ts = |

803 |
let f1 = parse_cimp symtab ts in |

804 |
match Stream.peek ts with |

805 |
| None -> f1 |

806 |
| Some (A.Kwd "&") -> |

807 |
Stream.junk ts; |

808 |
let f2 = parse_and symtab ts in |

809 |
AND (f1, f2) |

810 |
| _ -> f1 |

811 | |

812 |
(** These functions parse a token stream to obtain a formula. |

813 |
It is a standard recursive descent procedure. |

814 |
@param ts A token stream. |

815 |
@return The resulting (sub-)formula. |

816 |
@raise CoAlgException if ts does not represent a formula. |

817 |
*) |

818 |
and parse_cimp symtab ts = |

819 |
let f1 = parse_rest symtab ts in |

820 |
match Stream.peek ts with |

821 |
| None -> f1 |

822 |
| Some (A.Kwd "=o") -> |

823 |
Stream.junk ts; |

824 |
let f2 = parse_cimp symtab ts in |

825 |
NORM (f1, f2) |

826 |
| _ -> f1 |

827 | |

828 |
(** These functions parse a token stream to obtain a formula. |

829 |
It is a standard recursive descent procedure. |

830 |
@param ts A token stream. |

831 |
@return The resulting (sub-)formula. |

832 |
@raise CoAlgException if ts does not represent a formula. |

833 |
*) |

834 |
and parse_rest symtab ts = |

835 |
let boxinternals noNo es = |

836 |
let n = |

837 |
if noNo then 0 |

838 |
else |

839 |
match Stream.next ts with |

840 |
| A.Int n when n >= 0 -> n |

841 |
| t -> A.printError mk_exn ~t ~ts "<non-negative number> expected: " |

842 |
in |

843 |
let (s,denominator) = |

844 |
match Stream.peek ts with |

845 |
| Some (A.Ident s1) -> Stream.junk ts; (s1,0) |

846 |
| Some (A.Kwd c) when c = es -> ("", 0) |

847 |
| Some (A.Kwd "/") -> begin |

848 |
Stream.junk ts; |

849 |
match Stream.next ts with |

850 |
| A.Int denom when denom > 0 -> ("", denom) |

851 |
| t -> A.printError mk_exn ~t ~ts "<positive number> (the denominator) expected: " |

852 |
end |

853 |
| _ -> A.printError mk_exn ~ts ("role name or \"" ^ es ^ "\" expected: ") |

854 |
in |

855 |
if (denominator < n) then begin |

856 |
let explanation = |

857 |
("nominator="^(string_of_int n)^" but denominator="^(string_of_int denominator)) |

858 |
in |

859 |
A.printError mk_exn ~ts ("Nominator must not be larger than the denominator " |

860 |
^"("^explanation^") at: " |

861 |
) |

862 |
end; |

863 |
let _ = |

864 |
match Stream.next ts with |

865 |
| A.Kwd c when c = es -> () |

866 |
| t -> A.printError mk_exn ~t ~ts ("\"" ^ es ^ "\" expected: ") |

867 |
in |

868 |
(n, denominator, s) |

869 |
in |

870 |
let rec agentlist es = |

871 |
let allAgents = CoolUtils.cl_get_agents () in |

872 |
match Stream.next ts with |

873 |
| A.Int n -> if CoolUtils.TArray.elem n allAgents |

874 |
then n::(agentlist es) |

875 |
else A.printError mk_exn ~ts ("agent name \"" ^ (string_of_int n) ^ "\" unknonwn, see --agents: ") |

876 |
| A.Kwd c when c = es -> [] |

877 |
| _ -> A.printError mk_exn ~ts ("agent name or " ^ es ^ "\" expected: ") |

878 |
in |

879 |
match Stream.next ts with |

880 |
| A.Kwd "true" -> |

881 |
print_endline "*** Warning: \"true\" used as propositional variable."; |

882 |
AP "true" |

883 |
| A.Kwd "false" -> |

884 |
print_endline "*** Warning: \"false\" used as propositional variable."; |

885 |
AP "false" |

886 |
| A.Kwd "True" -> TRUE |

887 |
| A.Kwd "False" -> FALSE |

888 |
| A.Ident s -> |

889 |
(try |

890 |
let finder (x, _) = compare x s == 0 in |

891 |
let (_, symbol) = List.find finder symtab in |

892 |
VAR symbol |

893 |
with Not_found -> AP s) |

894 |
| A.Kwd "~" -> |

895 |
let f = parse_rest symtab ts in |

896 |
NOT f |

897 |
| A.Kwd "@" -> |

898 |
let s = |

899 |
match Stream.next ts with |

900 |
| A.Ident s when isNominal s -> s |

901 |
| t -> A.printError mk_exn ~t ~ts ("nominal expected: ") |

902 |
in |

903 |
let f = parse_rest symtab ts in |

904 |
AT (s, f) |

905 |
| A.Kwd "<" -> |

906 |
let (_, _, s) = boxinternals true ">" in |

907 |
let f1 = parse_rest symtab ts in |

908 |
EX (s, f1) |

909 |
| A.Kwd "[" -> |

910 |
let (_, _, s) = boxinternals true "]" in |

911 |
let f1 = parse_rest symtab ts in |

912 |
AX (s, f1) |

913 |
| A.Kwd "[{" -> |

914 |
let ls = agentlist "}]" in |

915 |
let f1 = parse_rest symtab ts in |

916 |
ENFORCES (ls, f1) |

917 |
| A.Kwd "<{" -> |

918 |
let ls = agentlist "}>" in |

919 |
let f1 = parse_rest symtab ts in |

920 |
ALLOWS (ls, f1) |

921 |
| A.Kwd "{>=" -> |

922 |
let (n, denom, s) = boxinternals false "}" in |

923 |
let f1 = parse_rest symtab ts in |

924 |
if (denom <> 0) |

925 |
then ATLEASTPROB (rational_of_int n denom, f1) |

926 |
else MIN (n, s, f1) |

927 |
| A.Kwd "{<=" -> |

928 |
let (n, denom, s) = boxinternals false "}" in |

929 |
let f1 = parse_rest symtab ts in |

930 |
if (denom <> 0) |

931 |
then A.printError mk_exn ~ts "Can not express {<= probability}" |

932 |
else MAX (n, s, f1) |

933 |
| A.Kwd "{<" -> |

934 |
let (n, denom, s) = boxinternals false "}" in |

935 |
let f1 = parse_rest symtab ts in |

936 |
if (denom <> 0) |

937 |
then LESSPROBFAIL (rational_of_int n denom, NOT f1) |

938 |
else A.printError mk_exn ~ts "The \"Less than\" < is not implemented yet" |

939 |
| A.Kwd "=" -> begin |

940 |
match Stream.next ts with |

941 |
(* | A.Int s *) |

942 |
| A.Kwd s |

943 |
| A.Ident s -> CONST s |

944 |
| _ -> A.printError mk_exn ~ts "constant = expects an identifier afterwards" |

945 |
end |

946 |
| A.Kwd "(" -> begin |

947 |
let f = parse_formula symtab ts in |

948 |
match Stream.next ts with |

949 |
| A.Kwd ")" -> f |

950 |
| A.Kwd "+" -> begin |

951 |
let f2 = parse_formula symtab ts in |

952 |
match Stream.next ts with |

953 |
| A.Kwd ")" -> CHC (f, f2) |

954 |
| t -> A.printError mk_exn ~t ~ts "\")\" expected: " |

955 |
end |

956 |
| t -> A.printError mk_exn ~t ~ts "\")\" or \"+\" expected: " |

957 |
end |

958 |
| A.Kwd "O" -> |

959 |
let f = parse_rest symtab ts in |

960 |
ID f |

961 |
| A.Kwd "[pi1]" -> |

962 |
let f = parse_rest symtab ts in |

963 |
FUS (true, f) |

964 |
| A.Kwd "[pi2]" -> |

965 |
let f = parse_rest symtab ts in |

966 |
FUS (false, f) |

967 |
| A.Kwd "μ" -> |

968 |
let (_, _, s) = boxinternals true "." in |

969 |
let symbol = Stream.next gensym in |

970 |
let newtab = (s, symbol) :: symtab in |

971 |
let f1 = parse_rest newtab ts in |

972 |
MU (symbol, f1) |

973 |
| A.Kwd "ν" -> |

974 |
let (_, _, s) = boxinternals true "." in |

975 |
let symbol = Stream.next gensym in |

976 |
let newtab = (s, symbol) :: symtab in |

977 |
let f1 = parse_rest newtab ts in |

978 |
NU (symbol, f1) |

979 |
| A.Kwd "AF" -> |

980 |
let f = parse_rest symtab ts in |

981 |
AF f |

982 |
| A.Kwd "EF" -> |

983 |
let f = parse_rest symtab ts in |

984 |
EF f |

985 |
| A.Kwd "AG" -> |

986 |
let f = parse_rest symtab ts in |

987 |
AG f |

988 |
| A.Kwd "EG" -> |

989 |
let f = parse_rest symtab ts in |

990 |
EG f |

991 |
| A.Kwd "A" -> |

992 |
assert (Stream.next ts = A.Kwd "("); |

993 |
let f1 = parse_formula symtab ts in |

994 |
assert (Stream.next ts = A.Kwd "U"); |

995 |
let f2 = parse_formula symtab ts in |

996 |
assert (Stream.next ts = A.Kwd ")"); |

997 |
AU (f1, f2) |

998 |
| A.Kwd "E" -> |

999 |
assert (Stream.next ts = A.Kwd "("); |

1000 |
let f1 = parse_formula symtab ts in |

1001 |
assert (Stream.next ts = A.Kwd "U"); |

1002 |
let f2 = parse_formula symtab ts in |

1003 |
assert (Stream.next ts = A.Kwd ")"); |

1004 |
EU (f1, f2) |

1005 |
| A.Kwd "AX" -> |

1006 |
let f1 = parse_rest symtab ts in |

1007 |
AX ("", f1) |

1008 |
| A.Kwd "EX" -> |

1009 |
let f1 = parse_rest symtab ts in |

1010 |
EX ("", f1) |

1011 |
| t -> A.printError mk_exn ~t ~ts |

1012 |
"\"<\", \"[\", \"{>=\", \"{<=\", \"@\", \"~\", \"(\", |

1013 |
\"True\", \"False\", \"=\", \"=o\", \"O\" or <ident> expected: " |

1014 | |

1015 |
(** Parses a sorted formula. |

1016 |
@param ts A token stream. |

1017 |
@return A sorted formula. |

1018 |
@raise CoAlgException If ts does not represent a sorted formula. |

1019 |
*) |

1020 |
let parse_sortedFormula ts = |

1021 |
let nr = |

1022 |
match Stream.peek ts with |

1023 |
| Some (A.Int n) -> |

1024 |
if n >= 0 then begin |

1025 |
Stream.junk ts; |

1026 |
let () = |

1027 |
match Stream.next ts with |

1028 |
| A.Kwd ":" -> () |

1029 |
| t -> A.printError mk_exn ~t ~ts ("\":\" expected: ") |

1030 |
in |

1031 |
n |

1032 |
end else |

1033 |
A.printError mk_exn ~ts ("<non-negative number> expected: ") |

1034 |
| _ -> 0 |

1035 |
in |

1036 |
let f = parse_formula [] ts in |

1037 |
(nr, f) |

1038 | |

1039 |
(** Parses a list of sorted formulae separated by ";". |

1040 |
@param ts A token stream. |

1041 |
@param acc The list of sorted formulae parsed so far. |

1042 |
@return The resulting list of sorted formula. |

1043 |
@raise CoAlgException if ts does not represent a list of sorted formulae. |

1044 |
*) |

1045 |
let rec parse_sortedFormulaList ts acc = |

1046 |
let f1 = parse_sortedFormula ts in |

1047 |
match Stream.peek ts with |

1048 |
| Some (A.Kwd ";") -> |

1049 |
Stream.junk ts; |

1050 |
parse_sortedFormulaList ts (f1::acc) |

1051 |
| _ -> List.rev (f1::acc) |

1052 | |

1053 |
(** A common wrapper for import functions. |

1054 |
@param fkt An import function. |

1055 |
@param s A string. |

1056 |
@return The object imported from s using fkt. |

1057 |
@raise CoAlgException If ts is not empty. |

1058 |
*) |

1059 |
let importWrapper fkt s = |

1060 |
let ts = lexer s in |

1061 |
try |

1062 |
let res = fkt ts in |

1063 |
let _ = |

1064 |
match Stream.peek ts with |

1065 |
| None -> () |

1066 |
| Some _ -> A.printError mk_exn ~ts "EOS expected: " |

1067 |
in |

1068 |
res |

1069 |
with Stream.Failure -> A.printError mk_exn ~ts "unexpected EOS" |

1070 | |

1071 |
(** Parses a string to obtain a formula. |

1072 |
@param s A string representing a formula. |

1073 |
@return The resulting formula. |

1074 |
@raise CoAlgException if s does not represent a formula. |

1075 |
*) |

1076 |
let importFormula s = importWrapper (parse_formula []) s |

1077 | |

1078 |
(** Parses a string to obtain a sorted formula. |

1079 |
@param s A string representing a sorted formula. |

1080 |
@return The sorted formula. |

1081 |
@raise CoAlgException If s does not represent a sorted formula. |

1082 |
*) |

1083 |
let importSortedFormula s = importWrapper parse_sortedFormula s |

1084 | |

1085 |
(** Parses a string to obtain a (sorted) formula query. |

1086 |
@param s A string representing a formula query. |

1087 |
@return A pair (tbox, f) where |

1088 |
tbox is a list of sorted formulae representing the TBox; and |

1089 |
f is a sorted formula. |

1090 |
@raise CoAlgException if s does not represent a formula query. |

1091 |
*) |

1092 |
let importQuery s = |

1093 |
let fkt ts = |

1094 |
match Stream.peek ts with |

1095 |
| Some (A.Kwd "|-") -> |

1096 |
Stream.junk ts; |

1097 |
let f = parse_sortedFormula ts in |

1098 |
([], f) |

1099 |
| _ -> |

1100 |
let fl = parse_sortedFormulaList ts [] in |

1101 |
match Stream.peek ts with |

1102 |
| Some (A.Kwd "|-") -> |

1103 |
Stream.junk ts; |

1104 |
let f = parse_sortedFormula ts in |

1105 |
(fl, f) |

1106 |
| _ -> |

1107 |
if List.length fl = 1 then ([], List.hd fl) |

1108 |
else A.printError mk_exn ~ts "\"|-\" expected: " |

1109 |
in |

1110 |
importWrapper fkt s |

1111 | |

1112 | |

1113 |
(** Converts the negation of a formula to negation normal form |

1114 |
by "pushing in" the negations "~". |

1115 |
The symbols "<=>" and "=>" are substituted by their usual definitions. |

1116 |
@param f A formula. |

1117 |
@return A formula in negation normal form and not containing "<=>" or "=>" |

1118 |
that is equivalent to ~f. |

1119 |
*) |

1120 |
let rec nnfNeg f = |

1121 |
match f with |

1122 |
| TRUE -> FALSE |

1123 |
| FALSE -> TRUE |

1124 |
| AP _ -> NOT f |

1125 |
| VAR _ -> f |

1126 |
| NOT f1 -> nnf f1 |

1127 |
| AT (s, f1) -> AT (s, nnfNeg f1) |

1128 |
| OR (f1, f2) -> AND (nnfNeg f1, nnfNeg f2) |

1129 |
| AND (f1, f2) -> OR (nnfNeg f1, nnfNeg f2) |

1130 |
| EQU (f1, f2) -> OR (AND (nnf f1, nnfNeg f2), AND (nnf f2, nnfNeg f1)) |

1131 |
| IMP (f1, f2) -> AND (nnf f1, nnfNeg f2) |

1132 |
| EX (s, f1) -> AX (s, nnfNeg f1) |

1133 |
| AX (s, f1) -> EX (s, nnfNeg f1) |

1134 |
| ENFORCES (s, f1) -> ALLOWS (s, nnfNeg f1) |

1135 |
| ALLOWS (s, f1) -> ENFORCES (s, nnfNeg f1) |

1136 |
| MIN (n, s, f1) -> if n = 0 then FALSE else MAXEXCEPT (n-1, s, nnfNeg f1) |

1137 |
| MAX (n, s, f1) -> MORETHAN (n, s, nnf f1) |

1138 |
| MORETHAN (n, s, f1) -> MAXEXCEPT (n, s, nnfNeg f1) |

1139 |
| MAXEXCEPT (n, s, f1) -> MORETHAN (n, s, nnfNeg f1) |

1140 |
| ATLEASTPROB (p, f1) -> LESSPROBFAIL (p, nnfNeg f1) |

1141 |
| LESSPROBFAIL (p, f1) -> ATLEASTPROB (p, nnfNeg f1) |

1142 |
| CONST s -> CONSTN s |

1143 |
| CONSTN s -> CONST s |

1144 |
| ID (f1) -> ID (nnfNeg f1) |

1145 |
| NORM(f1, f2) -> NORMN(nnfNeg f1, nnfNeg f2) |

1146 |
| NORMN(f1, f2) -> NORM (nnfNeg f1, nnfNeg f2) |

1147 |
| CHC (f1, f2) -> CHC (nnfNeg f1, nnfNeg f2) |

1148 |
| FUS (first, f1) -> FUS (first, nnfNeg f1) |

1149 |
| MU (s, f1) -> NU(s, nnfNeg f1) |

1150 |
| NU (s, f1) -> MU(s, nnfNeg f1) |

1151 |
| AF _ |

1152 |
| EF _ |

1153 |
| AG _ |

1154 |
| EG _ |

1155 |
| AU _ |

1156 |
| EU _ -> raise (CoAlgException ("nnfNeg: CTL should have been removed at this point")) |

1157 | |

1158 |
(** Converts a formula to negation normal form |

1159 |
by "pushing in" the negations "~". |

1160 |
The symbols "<=>" and "=>" are substituted by their usual definitions. |

1161 |
@param f A formula. |

1162 |
@return A formula in negation normal form and not containing "<=>" or "=>" |

1163 |
that is equivalent to f. |

1164 |
*) |

1165 |
and nnf f = |

1166 |
match f with |

1167 |
| TRUE |

1168 |
| FALSE |

1169 |
| AP _ |

1170 |
| NOT (AP _) |

1171 |
| CONST _ |

1172 |
| CONSTN _ |

1173 |
| VAR _ -> f |

1174 |
| NOT f1 -> nnfNeg f1 |

1175 |
| AT (s, f1) -> |

1176 |
let ft1 = nnf f1 in |

1177 |
if ft1 == f1 then f else AT (s, ft1) |

1178 |
| OR (f1, f2) -> |

1179 |
let ft1 = nnf f1 in |

1180 |
let ft2 = nnf f2 in |

1181 |
if ft1 == f1 && ft2 == f2 then f else OR (ft1, ft2) |

1182 |
| AND (f1, f2) -> |

1183 |
let ft1 = nnf f1 in |

1184 |
let ft2 = nnf f2 in |

1185 |
if ft1 == f1 && ft2 == f2 then f else AND (ft1, ft2) |

1186 |
| EQU (f1, f2) -> AND (OR (nnfNeg f1, nnf f2), OR (nnfNeg f2, nnf f1)) |

1187 |
| IMP (f1, f2) -> OR (nnfNeg f1, nnf f2) |

1188 |
| EX (s, f1) -> |

1189 |
let ft = nnf f1 in |

1190 |
if ft == f1 then f else EX (s, ft) |

1191 |
| AX (s, f1) -> |

1192 |
let ft = nnf f1 in |

1193 |
if ft == f1 then f else AX (s, ft) |

1194 |
| ENFORCES (s, f1) -> |

1195 |
let ft = nnf f1 in |

1196 |
if ft == f1 then f else ENFORCES (s, ft) |

1197 |
| ALLOWS (s, f1) -> |

1198 |
let ft = nnf f1 in |

1199 |
if ft == f1 then f else ALLOWS (s, ft) |

1200 |
| MIN (n, s, f1) -> |

1201 |
if n = 0 then TRUE |

1202 |
else |

1203 |
let ft = nnf f1 in |

1204 |
MORETHAN (n-1,s,ft) |

1205 |
| MAX (n, s, f1) -> |

1206 |
let ft = nnfNeg f1 in |

1207 |
MAXEXCEPT (n,s, ft) |

1208 |
| MORETHAN (n,s,f1) -> |

1209 |
let ft = nnf f1 in |

1210 |
if ft = f1 then f else MORETHAN (n,s,ft) |

1211 |
| MAXEXCEPT (n,s,f1) -> |

1212 |
let ft = nnf f1 in |

1213 |
if ft = f1 then f else MAXEXCEPT (n,s,ft) |

1214 |
| ATLEASTPROB (p, f1) -> |

1215 |
let ft = nnf f1 in |

1216 |
if ft == f1 then f else ATLEASTPROB (p, ft) |

1217 |
| LESSPROBFAIL (p, f1) -> |

1218 |
let ft = nnf f1 in |

1219 |
if ft == f1 then f else LESSPROBFAIL (p, ft) |

1220 |
| ID (f1) -> |

1221 |
let ft = nnf f1 in |

1222 |
if ft == f1 then f else ID(ft) |

1223 |
| NORM (f1, f2) -> |

1224 |
let ft1 = nnf f1 in |

1225 |
let ft2 = nnf f2 in |

1226 |
if ft1 == f1 && ft2 == f2 then f else NORM (ft1, ft2) |

1227 |
| NORMN (f1, f2) -> |

1228 |
let ft1 = nnf f1 in |

1229 |
let ft2 = nnf f2 in |

1230 |
if ft1 == f1 && ft2 == f2 then f else NORMN (ft1, ft2) |

1231 |
| CHC (f1, f2) -> |

1232 |
let ft1 = nnf f1 in |

1233 |
let ft2 = nnf f2 in |

1234 |
if ft1 == f1 && ft2 == f2 then f else CHC (ft1, ft2) |

1235 |
| FUS (first, f1) -> |

1236 |
let ft = nnf f1 in |

1237 |
if ft == f1 then f else FUS (first, ft) |

1238 |
| MU (s, f1) -> |

1239 |
let ft = nnf f1 in |

1240 |
if ft == f1 then f else MU (s, ft) |

1241 |
| NU (s, f1) -> |

1242 |
let ft = nnf f1 in |

1243 |
if ft == f1 then f else NU (s, ft) |

1244 |
| AF _ |

1245 |
| EF _ |

1246 |
| AG _ |

1247 |
| EG _ |

1248 |
| AU _ |

1249 |
| EU _ -> raise (CoAlgException ("nnf: CTL should have been removed at this point")) |

1250 | |

1251 |
(** Simplifies a formula. |

1252 |
@param f A formula which must be in negation normal form. |

1253 |
@return A formula in negation normal form that is equivalent to f. |

1254 |
@raise CoAlgException if f is not in negation normal form. |

1255 |
*) |

1256 |
let rec simplify f = |

1257 |
match f with |

1258 |
| TRUE |

1259 |
| FALSE |

1260 |
| AP _ |

1261 |
| NOT (AP _) |

1262 |
| VAR _ |

1263 |
| NOT (VAR _) -> f |

1264 |
| AT (s, f1) -> |

1265 |
let ft = simplify f1 in |

1266 |
begin |

1267 |
match ft with |

1268 |
| FALSE -> FALSE |

1269 |
| TRUE -> TRUE |

1270 |
| AT _ -> ft |

1271 |
| AP s1 when s = s1 -> TRUE |

1272 |
| NOT (AP s1) when s = s1 -> FALSE |

1273 |
| _ -> if ft == f1 then f else AT (s, ft) |

1274 |
end |

1275 |
| OR (f1, f2) -> |

1276 |
let ft1 = simplify f1 in |

1277 |
let ft2 = simplify f2 in |

1278 |
begin |

1279 |
match ft1, ft2 with |

1280 |
| TRUE, _ -> TRUE |

1281 |
| FALSE, _ -> ft2 |

1282 |
| _, TRUE -> TRUE |

1283 |
| _, FALSE -> ft1 |

1284 |
| _, _ -> |

1285 |
if (f1 == ft1) && (f2 == ft2) then f |

1286 |
else OR (ft1, ft2) |

1287 |
end |

1288 |
| AND (f1, f2) -> |

1289 |
let ft1 = simplify f1 in |

1290 |
let ft2 = simplify f2 in |

1291 |
begin |

1292 |
match ft1, ft2 with |

1293 |
| TRUE, _ -> ft2 |

1294 |
| FALSE, _ -> FALSE |

1295 |
| _, TRUE -> ft1 |

1296 |
| _, FALSE -> FALSE |

1297 |
| _, _ -> |

1298 |
if (f1 == ft1) && (f2 == ft2) then f |

1299 |
else AND (ft1, ft2) |

1300 |
end |

1301 |
| NOT _ |

1302 |
| EQU _ |

1303 |
| IMP _ -> raise (CoAlgException "Formula is not in negation normal form.") |

1304 |
| EX (s, f1) -> |

1305 |
let ft = simplify f1 in |

1306 |
begin |

1307 |
match ft with |

1308 |
| FALSE -> FALSE |

1309 |
| _ -> if ft == f1 then f else EX (s, ft) |

1310 |
end |

1311 |
| AX (s, f1) -> |

1312 |
let ft = simplify f1 in |

1313 |
begin |

1314 |
match ft with |

1315 |
| TRUE -> TRUE |

1316 |
| _ -> if ft == f1 then f else AX (s, ft) |

1317 |
end |

1318 |
| ENFORCES (s, f1) -> |

1319 |
let ft = simplify f1 in |

1320 |
begin |

1321 |
match ft with |

1322 |
(* Simplification rules are checked with dirks Generic.hs |

1323 |
let enforce ls = M (C ls) |

1324 |
let allow ls = Neg . M (C ls) . Neg |

1325 |
provable $ F <-> enforce [1,2] F |

1326 |
*) |

1327 |
| TRUE -> TRUE |

1328 |
| FALSE -> FALSE |

1329 |
| _ -> if ft == f1 then f else ENFORCES (s, ft) |

1330 |
end |

1331 |
| ALLOWS (s, f1) -> |

1332 |
let ft = simplify f1 in |

1333 |
begin |

1334 |
match ft with |

1335 |
(* Simplification rules are checked with dirks Generic.hs |

1336 |
let enforce ls = M (C ls) |

1337 |
let allow ls = Neg . M (C ls) . Neg |

1338 |
provable $ F <-> enforce [1,2] F |

1339 |
*) |

1340 |
| TRUE -> TRUE |

1341 |
| FALSE -> FALSE |

1342 |
| _ -> if ft == f1 then f else ALLOWS (s, ft) |

1343 |
end |

1344 |
| MIN (n, s, f1) -> |

1345 |
if n = 0 then TRUE |

1346 |
else |

1347 |
let ft = simplify f1 in |

1348 |
begin |

1349 |
match ft with |

1350 |
| FALSE -> FALSE |

1351 |
| _ -> if ft == f1 then f else MIN (n, s, ft) |

1352 |
end |

1353 |
| MORETHAN (n,s,f1) -> |

1354 |
let ft = simplify f1 in |

1355 |
if ft == f1 then f else MORETHAN (n,s,ft) |

1356 |
| MAXEXCEPT (n,s,f1) -> |

1357 |
let ft = simplify f1 in |

1358 |
if ft == f1 then f else MAXEXCEPT (n,s,ft) |

1359 |
| MAX (n, s, f1) -> |

1360 |
let ft = simplify f1 in |

1361 |
begin |

1362 |
match ft with |

1363 |
| FALSE -> TRUE |

1364 |
| _ -> if ft == f1 then f else MAX (n, s, ft) |

1365 |
end |

1366 |
| LESSPROBFAIL (p,f1) -> |

1367 |
let ft1 = simplify f1 in |

1368 |
if (ft1 == f1) then f else LESSPROBFAIL (p,ft1) |

1369 |
| ATLEASTPROB (p,f1) -> |

1370 |
let ft1 = simplify f1 in |

1371 |
if (ft1 == f1) then f else ATLEASTPROB (p,ft1) |

1372 |
| CONST _ |

1373 |
| CONSTN _ -> f (* no simplifications possible *) |

1374 |
| ID (f1) -> |

1375 |
let ft1 = simplify f1 in |

1376 |
begin |

1377 |
match ft1 with |

1378 |
| TRUE -> TRUE |

1379 |
| FALSE -> FALSE |

1380 |
| _ -> if (ft1 == f1) then f else ID (ft1) |

1381 |
end |

1382 |
(* todo: more simplifications for KLM? *) |

1383 |
| NORM (f1, f2) -> |

1384 |
let ft1 = simplify f1 in |

1385 |
let ft2 = simplify f2 in |

1386 |
begin |

1387 |
match ft2 with |

1388 |
| TRUE -> TRUE |

1389 |
| _ -> |

1390 |
if (f1 == ft1) && (f2 == ft2) then f |

1391 |
else NORM (ft1, ft2) |

1392 |
end |

1393 |
| NORMN (f1, f2) -> |

1394 |
let ft1 = simplify f1 in |

1395 |
let ft2 = simplify f2 in |

1396 |
begin |

1397 |
match ft2 with |

1398 |
| FALSE -> FALSE |

1399 |
| _ -> |

1400 |
if (f1 == ft1) && (f2 == ft2) then f |

1401 |
else NORMN (ft1, ft2) |

1402 |
end |

1403 |
| CHC (f1, f2) -> |

1404 |
let ft1 = simplify f1 in |

1405 |
let ft2 = simplify f2 in |

1406 |
begin |

1407 |
match ft1, ft2 with |

1408 |
| TRUE, TRUE -> TRUE |

1409 |
| FALSE, FALSE -> FALSE |

1410 |
| _, _ -> |

1411 |
if (f1 == ft1) && (f2 == ft2) then f |

1412 |
else CHC (ft1, ft2) |

1413 |
end |

1414 |
| FUS (first, f1) -> |

1415 |
let ft = simplify f1 in |

1416 |
begin |

1417 |
match ft with |

1418 |
| FALSE -> FALSE |

1419 |
| TRUE -> TRUE |

1420 |
| _ -> if ft == f1 then f else FUS (first, ft) |

1421 |
end |

1422 |
| MU (s, f1) -> |

1423 |
let ft = simplify f1 in |

1424 |
begin |

1425 |
match ft with |

1426 |
| TRUE -> TRUE |

1427 |
| _ -> if ft == f1 then f else MU (s, ft) |

1428 |
end |

1429 |
| NU (s, f1) -> |

1430 |
let ft = simplify f1 in |

1431 |
begin |

1432 |
match ft with |

1433 |
| TRUE -> TRUE |

1434 |
| _ -> if ft == f1 then f else NU (s, ft) |

1435 |
end |

1436 |
| AF _ |

1437 |
| EF _ |

1438 |
| AG _ |

1439 |
| EG _ |

1440 |
| AU _ |

1441 |
| EU _ -> |

1442 |
raise (CoAlgException ("nnf: CTL should have been removed at this point")) |

1443 | |

1444 |
(** Destructs an atomic proposition. |

1445 |
@param f An atomic proposition. |

1446 |
@return The name of the atomic proposition. |

1447 |
@raise CoAlgException if f is not an atomic proposition. |

1448 |
*) |

1449 |
let dest_ap f = |

1450 |
match f with |

1451 |
| AP s when not (isNominal s) -> s |

1452 |
| _ -> raise (CoAlgException "Formula is not an atomic proposition.") |

1453 | |

1454 |
(** Destructs a nominal. |

1455 |
@param f A nominal. |

1456 |
@return The name of the nominal |

1457 |
@raise CoAlgException if f is not a nominal. |

1458 |
*) |

1459 |
let dest_nom f = |

1460 |
match f with |

1461 |
| AP s when isNominal s -> s |

1462 |
| _ -> raise (CoAlgException "Formula is not a nominal.") |

1463 | |

1464 |
(** Destructs a negation. |

1465 |
@param f A negation. |

1466 |
@return The immediate subformula of the negation. |

1467 |
@raise CoAlgException if f is not a negation. |

1468 |
*) |

1469 |
let dest_not f = |

1470 |
match f with |

1471 |
| NOT f1 -> f1 |

1472 |
| _ -> raise (CoAlgException "Formula is not a negation.") |

1473 | |

1474 |
(** Destructs an @-formula. |

1475 |
@param f An @-formula. |

1476 |
@return The name of the nominal and the immediate subformula of the @-formula. |

1477 |
@raise CoAlgException if f is not an @-formula. |

1478 |
*) |

1479 |
let dest_at f = |

1480 |
match f with |

1481 |
| AT (s, f1) -> (s, f1) |

1482 |
| _ -> raise (CoAlgException "Formula is not an @-formula.") |

1483 | |

1484 |
(** Destructs an or-formula. |

1485 |
@param f An or-formula. |

1486 |
@return The two immediate subformulae of the or-formula. |

1487 |
@raise CoAlgException if f is not an or-formula. |

1488 |
*) |

1489 |
let dest_or f = |

1490 |
match f with |

1491 |
| OR (f1, f2) -> (f1, f2) |

1492 |
| _ -> raise (CoAlgException "Formula is not an or-formula.") |

1493 | |

1494 |
(** Destructs an and-formula. |

1495 |
@param f An and-formula. |

1496 |
@return The two immediate subformulae of the and-formula. |

1497 |
@raise CoAlgException if f is not an and-formula. |

1498 |
*) |

1499 |
let dest_and f = |

1500 |
match f with |

1501 |
| AND (f1, f2) -> (f1, f2) |

1502 |
| _ -> raise (CoAlgException "Formula is not an and-formula.") |

1503 | |

1504 |
(** Destructs an equivalence. |

1505 |
@param f An equivalence. |

1506 |
@return The two immediate subformulae of the equivalence. |

1507 |
@raise CoAlgException if f is not an equivalence. |

1508 |
*) |

1509 |
let dest_equ f = |

1510 |
match f with |

1511 |
| EQU (f1, f2) -> (f1, f2) |

1512 |
| _ -> raise (CoAlgException "Formula is not an equivalence.") |

1513 | |

1514 |
(** Destructs an implication. |

1515 |
@param f An implication. |

1516 |
@return The two immediate subformulae of the implication. |

1517 |
@raise CoAlgException if f is not an implication. |

1518 |
*) |

1519 |
let dest_imp f = |

1520 |
match f with |

1521 |
| IMP (f1, f2) -> (f1, f2) |

1522 |
| _ -> raise (CoAlgException "Formula is not an implication.") |

1523 | |

1524 |
(** Destructs an EX-formula. |

1525 |
@param f An EX-formula. |

1526 |
@return The role name and the immediate subformula of the EX-formula. |

1527 |
@raise CoAlgException if f is not an EX-formula. |

1528 |
*) |

1529 |
let dest_ex f = |

1530 |
match f with |

1531 |
| EX (s, f1) -> (s, f1) |

1532 |
| _ -> raise (CoAlgException "Formula is not an EX-formula.") |

1533 | |

1534 |
(** Destructs an AX-formula. |

1535 |
@param f An AX-formula. |

1536 |
@return The role name and the immediate subformula of the AX-formula. |

1537 |
@raise CoAlgException if f is not an AX-formula. |

1538 |
*) |

1539 |
let dest_ax f = |

1540 |
match f with |

1541 |
| AX (s, f1) -> (s, f1) |

1542 |
| _ -> raise (CoAlgException "Formula is not an AX-formula.") |

1543 | |

1544 |
(** Destructs a MIN-formula. |

1545 |
@param f A MIN-formula. |

1546 |
@return The number restriction, role name, |

1547 |
and the immediate subformula of the MIN-formula. |

1548 |
@raise CoAlgException if f is not a MIN-formula. |

1549 |
*) |

1550 |
let dest_min f = |

1551 |
match f with |

1552 |
| MIN (n, s, f1) -> (n, s, f1) |

1553 |
| _ -> raise (CoAlgException "Formula is not a MIN-formula.") |

1554 | |

1555 |
(** Destructs a MAX-formula. |

1556 |
@param f A MAX-formula. |

1557 |
@return The number restriction, role name, |

1558 |
and the immediate subformula of the MAX-formula. |

1559 |
@raise CoAlgException if f is not a MAX-formula. |

1560 |
*) |

1561 |
let dest_max f = |

1562 |
match f with |

1563 |
| MAX (n, s, f1) -> (n, s, f1) |

1564 |
| _ -> raise (CoAlgException "Formula is not a MAX-formula.") |

1565 | |

1566 |
(** Destructs a choice formula. |

1567 |
@param f A choice formula. |

1568 |
@return The two immediate subformulae of the choice formula. |

1569 |
@raise CoAlgException if f is not a choice formula. |

1570 |
*) |

1571 |
let dest_choice f = |

1572 |
match f with |

1573 |
| CHC (f1, f2) -> (f1, f2) |

1574 |
| _ -> raise (CoAlgException "Formula is not a choice formula.") |

1575 | |

1576 |
(** Destructs a fusion formula. |

1577 |
@param f A fusion formula. |

1578 |
@return A pair (first, f1) where |

1579 |
first is true iff f is a first projection; and |

1580 |
f1 is the immediate subformulae of f. |

1581 |
@raise CoAlgException if f is not a fusion formula. |

1582 |
*) |

1583 |
let dest_fusion f = |

1584 |
match f with |

1585 |
| FUS (first, f1) -> (first, f1) |

1586 |
| _ -> raise (CoAlgException "Formula is not a fusion formula.") |

1587 | |

1588 | |

1589 |
(** Tests whether a formula is the constant True. |

1590 |
@param f A formula. |

1591 |
@return True iff f is the constant True. |

1592 |
*) |

1593 |
let is_true f = |

1594 |
match f with |

1595 |
| TRUE -> true |

1596 |
| _ -> false |

1597 | |

1598 |
(** Tests whether a formula is the constant False. |

1599 |
@param f A formula. |

1600 |
@return True iff f is the constant False. |

1601 |
*) |

1602 |
let is_false f = |

1603 |
match f with |

1604 |
| FALSE -> true |

1605 |
| _ -> false |

1606 | |

1607 |
(** Tests whether a formula is an atomic proposition. |

1608 |
@param f A formula. |

1609 |
@return True iff f is an atomic proposition. |

1610 |
*) |

1611 |
let is_ap f = |

1612 |
match f with |

1613 |
| AP s when not (isNominal s) -> true |

1614 |
| _ -> false |

1615 | |

1616 |
(** Tests whether a formula is a nominal. |

1617 |
@param f A formula. |

1618 |
@return True iff f is a nominal. |

1619 |
*) |

1620 |
let is_nom f = |

1621 |
match f with |

1622 |
| AP s when isNominal s -> true |

1623 |
| _ -> false |

1624 | |

1625 |
(** Tests whether a formula is a negation. |

1626 |
@param f A formula. |

1627 |
@return True iff f is a negation. |

1628 |
*) |

1629 |
let is_not f = |

1630 |
match f with |

1631 |
| NOT _ -> true |

1632 |
| _ -> false |

1633 | |

1634 |
(** Tests whether a formula is an @-formula. |

1635 |
@param f A formula. |

1636 |
@return True iff f is an @-formula. |

1637 |
*) |

1638 |
let is_at f = |

1639 |
match f with |

1640 |
| AT _ -> true |

1641 |
| _ -> false |

1642 | |

1643 |
(** Tests whether a formula is an or-formula. |

1644 |
@param f A formula. |

1645 |
@return True iff f is an or-formula. |

1646 |
*) |

1647 |
let is_or f = |

1648 |
match f with |

1649 |
| OR _ -> true |

1650 |
| _ -> false |

1651 | |

1652 |
(** Tests whether a formula is an and-formula. |

1653 |
@param f A formula. |

1654 |
@return True iff f is an and-formula. |

1655 |
*) |

1656 |
let is_and f = |

1657 |
match f with |

1658 |
| AND _ -> true |

1659 |
| _ -> false |

1660 | |

1661 |
(** Tests whether a formula is an equivalence. |

1662 |
@param f A formula. |

1663 |
@return True iff f is an equivalence. |

1664 |
*) |

1665 |
let is_equ f = |

1666 |
match f with |

1667 |
| EQU _ -> true |

1668 |
| _ -> false |

1669 | |

1670 |
(** Tests whether a formula is an implication. |

1671 |
@param f A formula. |

1672 |
@return True iff f is an implication. |

1673 |
*) |

1674 |
let is_imp f = |

1675 |
match f with |

1676 |
| IMP _ -> true |

1677 |
| _ -> false |

1678 | |

1679 |
(** Tests whether a formula is an EX-formula. |

1680 |
@param f A formula. |

1681 |
@return True iff f is an EX-formula. |

1682 |
*) |

1683 |
let is_ex f = |

1684 |
match f with |

1685 |
| EX _ -> true |

1686 |
| _ -> false |

1687 | |

1688 |
(** Tests whether a formula is an AX-formula. |

1689 |
@param f A formula. |

1690 |
@return True iff f is an AX-formula. |

1691 |
*) |

1692 |
let is_ax f = |

1693 |
match f with |

1694 |
| AX _ -> true |

1695 |
| _ -> false |

1696 | |

1697 |
(** Tests whether a formula is a MIN-formula. |

1698 |
@param f A formula. |

1699 |
@return True iff f is a MIN-formula. |

1700 |
*) |

1701 |
let is_min f = |

1702 |
match f with |

1703 |
| MIN _ -> true |

1704 |
| _ -> false |

1705 | |

1706 |
(** Tests whether a formula is a MAX-formula. |

1707 |
@param f A formula. |

1708 |
@return True iff f is a MAX-formula. |

1709 |
*) |

1710 |
let is_max f = |

1711 |
match f with |

1712 |
| MAX _ -> true |

1713 |
| _ -> false |

1714 | |

1715 |
(** Tests whether a formula is a choice formula. |

1716 |
@param f A formula. |

1717 |
@return True iff f is a choice formula. |

1718 |
*) |

1719 |
let is_choice f = |

1720 |
match f with |

1721 |
| CHC _ -> true |

1722 |
| _ -> false |

1723 | |

1724 |
(** Tests whether a formula is a fusion formula. |

1725 |
@param f A formula. |

1726 |
@return True iff f is a fusion formula. |

1727 |
*) |

1728 |
let is_fusion f = |

1729 |
match f with |

1730 |
| FUS _ -> true |

1731 |
| _ -> false |

1732 | |

1733 | |

1734 |
(** The constant True. |

1735 |
*) |

1736 |
let const_true = TRUE |

1737 | |

1738 |
(** The constant False. |

1739 |
*) |

1740 |
let const_false = FALSE |

1741 | |

1742 |
(** Constructs an atomic proposition. |

1743 |
@param s The name of the atomic proposition. |

1744 |
@return The atomic proposition with name s. |

1745 |
@raise CoAlgException if s is a nominal name. |

1746 |
*) |

1747 |
let const_ap s = |

1748 |
if isNominal s then raise (CoAlgException "The name indicates a nominal.") |

1749 |
else AP s |

1750 | |

1751 |
(** Constructs a nominal. |

1752 |
@param s The name of the nominal. |

1753 |
@return A nominal with name s. |

1754 |
@raise CoAlgException if s is not a nominal name. |

1755 |
*) |

1756 |
let const_nom s = |

1757 |
if isNominal s then AP s |

1758 |
else raise (CoAlgException "The name does not indicate a nominal.") |

1759 | |

1760 |
(** Negates a formula. |

1761 |
@param f A formula. |

1762 |
@return The negation of f. |

1763 |
*) |

1764 |
let const_not f = NOT f |

1765 | |

1766 |
(** Constructs an @-formula from a name and a formula. |

1767 |
@param s A nominal name. |

1768 |
@param f A formula. |

1769 |
@return The formula AT (s, f). |

1770 |
*) |

1771 |
let const_at s f = AT (s, f) |

1772 | |

1773 |
(** Constructs an or-formula from two formulae. |

1774 |
@param f1 The first formula (LHS). |

1775 |
@param f2 The second formula (LHS). |

1776 |
@return The formula f1 | f2. |

1777 |
*) |

1778 |
let const_or f1 f2 = OR (f1, f2) |

1779 | |

1780 |
(** Constructs an and-formula from two formulae. |

1781 |
@param f1 The first formula (LHS). |

1782 |
@param f2 The second formula (LHS). |

1783 |
@return The formula f1 & f2. |

1784 |
*) |

1785 |
let const_and f1 f2 = AND (f1, f2) |

1786 | |

1787 |
(** Constructs an equivalence from two formulae. |

1788 |
@param f1 The first formula (LHS). |

1789 |
@param f2 The second formula (LHS). |

1790 |
@return The equivalence f1 <=> f2. |

1791 |
*) |

1792 |
let const_equ f1 f2 = EQU (f1, f2) |

1793 | |

1794 |
(** Constructs an implication from two formulae. |

1795 |
@param f1 The first formula (LHS). |

1796 |
@param f2 The second formula (LHS). |

1797 |
@return The implication f1 => f2. |

1798 |
*) |

1799 |
let const_imp f1 f2 = IMP (f1, f2) |

1800 | |

1801 |
(** Constructs an EX-formula from a formula. |

1802 |
@param s A role name. |

1803 |
@param f A formula. |

1804 |
@return The formula EX (s, f). |

1805 |
*) |

1806 |
let const_ex s f = EX (s, f) |

1807 | |

1808 |
(** Constructs an AX-formula from a formula. |

1809 |
@param s A role name. |

1810 |
@param f A formula. |

1811 |
@return The formula AX (s, f). |

1812 |
*) |

1813 |
let const_ax s f = AX (s, f) |

1814 | |

1815 |
(** Constructs a MIN-formula from a formula. |

1816 |
@param n A non-negative integer. |

1817 |
@param s A role name. |

1818 |
@param f A formula. |

1819 |
@return The formula MIN f. |

1820 |
@raise CoAlgException Iff n is negative. |

1821 |
*) |

1822 |
let const_min n s f = |

1823 |
if n < 0 then raise (CoAlgException "Negative cardinality constraint.") |

1824 |
else MIN (n, s, f) |

1825 | |

1826 |
(** Constructs a MAX-formula from a formula. |

1827 |
@param n A non-negative integer. |

1828 |
@param s A role name. |

1829 |
@param f A formula. |

1830 |
@return The formula MAX f. |

1831 |
@raise CoAlgException Iff n is negative. |

1832 |
*) |

1833 |
let const_max n s f = |

1834 |
if n < 0 then raise (CoAlgException "Negative cardinality constraint.") |

1835 |
else MAX (n, s, f) |

1836 | |

1837 |
let const_enforces p f = |

1838 |
ENFORCES (p,f) |

1839 | |

1840 |
let const_allows p f = |

1841 |
ALLOWS (p,f) |

1842 | |

1843 |
(** Constructs a choice formula from two formulae. |

1844 |
@param f1 The first formula (LHS). |

1845 |
@param f2 The second formula (LHS). |

1846 |
@return The formula (f1 + f2). |

1847 |
*) |

1848 |
let const_choice f1 f2 = CHC (f1, f2) |

1849 | |

1850 |
(** Constructs a fusion formula. |

1851 |
@param first True iff the result is a first projection. |

1852 |
@param f1 A formula. |

1853 |
@return The formula [pi1] f1 or [pi2] f1 (depending on first). |

1854 |
*) |

1855 |
let const_fusion first f1 = FUS (first, f1) |

1856 | |

1857 | |

1858 |
(** Hash-consed formulae, which are in negation normal form, |

1859 |
such that structural and physical equality coincide. |

1860 | |

1861 |
Also CTL has been replaced by the equivalent μ-Calculus |

1862 |
constructs |

1863 |
*) |

1864 |
type hcFormula = (hcFormula_node, formula) HC.hash_consed |

1865 |
and hcFormula_node = |

1866 |
| HCTRUE |

1867 |
| HCFALSE |

1868 |
| HCAP of string |

1869 |
| HCNOT of string |

1870 |
| HCAT of string * hcFormula |

1871 |
| HCOR of hcFormula * hcFormula |

1872 |
| HCAND of hcFormula * hcFormula |

1873 |
| HCEX of string * hcFormula |

1874 |
| HCAX of string * hcFormula |

1875 |
| HCENFORCES of int list * hcFormula |

1876 |
| HCALLOWS of int list * hcFormula |

1877 |
| HCMORETHAN of int * string * hcFormula (* GML Diamond *) |

1878 |
| HCMAXEXCEPT of int * string * hcFormula (* GML Box *) |

1879 |
| HCATLEASTPROB of rational * hcFormula |

1880 |
| HCLESSPROBFAIL of rational * hcFormula |

1881 |
| HCCONST of string |

1882 |
| HCCONSTN of string |

1883 |
| HCID of hcFormula |

1884 |
| HCNORM of hcFormula * hcFormula |

1885 |
| HCNORMN of hcFormula * hcFormula |

1886 |
| HCCHC of hcFormula * hcFormula |

1887 |
| HCFUS of bool * hcFormula |

1888 |
| HCMU of string * hcFormula |

1889 |
| HCNU of string * hcFormula |

1890 |
| HCVAR of string |

1891 | |

1892 |
(** Determines whether two formula nodes are structurally equal. |

1893 |
@param f1 The first formula node. |

1894 |
@param f2 The second formula node. |

1895 |
@return True iff f1 and f2 are structurally equal. |

1896 |
*) |

1897 |
let equal_hcFormula_node f1 f2 = |

1898 |
match f1, f2 with |

1899 |
| HCTRUE, HCTRUE -> true |

1900 |
| HCFALSE, HCFALSE -> true |

1901 |
| HCCONST s1, HCCONST s2 |

1902 |
| HCCONSTN s1, HCCONSTN s2 |

1903 |
| HCAP s1, HCAP s2 |

1904 |
| HCNOT s1, HCNOT s2 -> compare s1 s2 = 0 |

1905 |
| HCAT (s1, f1), HCAT (s2, f2) -> compare s1 s2 = 0 && f1 == f2 |

1906 |
| HCOR (f1a, f1b), HCOR (f2a, f2b) |

1907 |
| HCAND (f1a, f1b), HCAND (f2a, f2b) -> f1a == f2a && f1b == f2b |

1908 |
| HCEX (s1, f1), HCEX (s2, f2) |

1909 |
| HCAX (s1, f1), HCAX (s2, f2) -> compare s1 s2 = 0 && f1 == f2 |

1910 |
| HCENFORCES (s1, f1), HCENFORCES (s2, f2) |

1911 |
| HCALLOWS (s1, f1), HCALLOWS (s2, f2) -> compare s1 s2 = 0 && f1 == f2 |

1912 |
| HCMORETHAN (n1, s1, f1), HCMORETHAN (n2, s2, f2) |

1913 |
| HCMAXEXCEPT (n1, s1, f1), HCMAXEXCEPT (n2, s2, f2) -> |

1914 |
n1 = n2 && compare s1 s2 = 0 && f1 == f2 |

1915 |
| HCATLEASTPROB (p1, f1), HCATLEASTPROB (p2,f2) -> |

1916 |
p1 = p2 && f1 == f2 |

1917 |
| HCLESSPROBFAIL (p1, f1), HCLESSPROBFAIL (p2,f2) -> |

1918 |
p1 = p2 && f1 == f2 |

1919 |
| HCID f1, HCID f2 -> f1 == f2 |

1920 |
| HCNORM (f1a, f1b), HCNORMN (f2a, f2b) -> f1a == f2a && f1b == f2b |

1921 |
| HCCHC (f1a, f1b), HCCHC (f2a, f2b) -> f1a == f2a && f1b == f2b |

1922 |
| HCFUS (first1, f1), HCFUS (first2, f2) -> first1 = first2 && f1 == f2 |

1923 |
| HCMU (name1, f1), HCMU(name2, f2) -> compare name1 name2 = 0 && f1 == f2 |

1924 |
| HCNU (name1, f1), HCNU(name2, f2) -> compare name1 name2 = 0 && f1 == f2 |

1925 |
| HCVAR name1, HCVAR name2 -> compare name1 name2 = 0 |

1926 |
(* The rest could be shortened to | _ -> false, |

1927 |
but then the compiler would not warn if the formula type is extended |

1928 |
and this function is not updated accordingly.*) |

1929 |
| HCTRUE, _ |

1930 |
| HCFALSE, _ |

1931 |
| HCAP _, _ |

1932 |
| HCNOT _, _ |

1933 |
| HCAT _, _ |

1934 |
| HCOR _, _ |

1935 |
| HCAND _, _ |

1936 |
| HCEX _, _ |

1937 |
| HCAX _, _ |

1938 |
| HCENFORCES _, _ |

1939 |
| HCALLOWS _, _ |

1940 |
| HCMORETHAN _, _ |

1941 |
| HCMAXEXCEPT _, _ |

1942 |
| HCATLEASTPROB _, _ |

1943 |
| HCLESSPROBFAIL _, _ |

1944 |
| HCCONST _, _ |

1945 |
| HCCONSTN _, _ |

1946 |
| HCID _, _ |

1947 |
| HCNORM _, _ |

1948 |
| HCNORMN _, _ |

1949 |
| HCCHC _, _ |

1950 |
| HCFUS _, _ |

1951 |
| HCMU _, _ |

1952 |
| HCNU _, _ |

1953 |
| HCVAR _, _ -> false |

1954 | |

1955 |
(** Computes the hash value of a formula node. |

1956 |
@param f A formula node. |

1957 |
@return The hash value of f. |

1958 |
*) |

1959 |
let hash_hcFormula_node f = |

1960 |
let base = 23 in (* should be larger than the no of constructors *) |

1961 |
match f with |

1962 |
| HCTRUE -> 0 |

1963 |
| HCFALSE -> 1 |

1964 |
| HCAP s |

1965 |
| HCNOT s |

1966 |
| HCVAR s -> base * Hashtbl.hash s + 1 |

1967 |
| HCAT (s, f1) -> base * (base * (Hashtbl.hash s) + f1.HC.hkey) + 2 |

1968 |
| HCOR (f1, f2) -> base * (base * f1.HC.hkey + f2.HC.hkey) + 5 |

1969 |
| HCAND (f1, f2) -> base * (base * f1.HC.hkey + f2.HC.hkey) + 6 |

1970 |
| HCEX (s, f1) -> base * (base * (Hashtbl.hash s) + f1.HC.hkey) + 3 |

1971 |
| HCAX (s, f1) -> base * (base * (Hashtbl.hash s) + f1.HC.hkey) + 4 |

1972 |
| HCMORETHAN (n, s, f1) -> base * (base * (base * (Hashtbl.hash s) + n) + f1.HC.hkey) + 7 |

1973 |
| HCMAXEXCEPT (n, s, f1) -> base * (base * (base * (Hashtbl.hash s) + n) + f1.HC.hkey) + 8 |

1974 |
| HCATLEASTPROB (p,f1) -> base * (base * (base * p.nominator + p.denominator) + f1.HC.hkey) + 9 |

1975 |
| HCLESSPROBFAIL (p,f1) -> base * (base * (base * p.nominator + p.denominator) + f1.HC.hkey) + 10 |

1976 |
| HCCHC (f1, f2) -> base * (base * f1.HC.hkey + f2.HC.hkey) + 11 |

1977 |
| HCFUS (first, f1) -> base * (base * (Hashtbl.hash first) + f1.HC.hkey) + 13 |

1978 |
| HCENFORCES (s, f1) -> base * (base * (Hashtbl.hash s) + f1.HC.hkey) + 14 |

1979 |
| HCALLOWS (s, f1) -> base * (base * (Hashtbl.hash s) + f1.HC.hkey) + 15 |

1980 |
| HCCONST s -> Hashtbl.hash s + 16 |

1981 |
| HCCONSTN s -> Hashtbl.hash s + 17 |

1982 |
| HCNORM (f1, f2) -> base * (base * f1.HC.hkey + f2.HC.hkey) + 18 |

1983 |
| HCNORMN (f1, f2) -> base * (base * f1.HC.hkey + f2.HC.hkey) + 19 |

1984 |
| HCID (f1) -> base * f1.HC.hkey + 20 |

1985 |
| HCMU (s, f1) -> base * (base * (Hashtbl.hash s) + f1.HC.hkey) + 21 |

1986 |
| HCNU (s, f1) -> base * (base * (Hashtbl.hash s) + f1.HC.hkey) + 22 |

1987 | |

1988 |
(** Determines the "real" formula of a formula node. |

1989 |
@param f A formula node. |

1990 |
@return The formula (in negation normal form) which corresponds to f. |

1991 |
*) |

1992 |
let toFml_hcFormula_node f = |

1993 |
match f with |

1994 |
| HCTRUE -> TRUE |

1995 |
| HCFALSE -> FALSE |

1996 |
| HCAP s -> AP s |

1997 |
| HCVAR s -> VAR s |

1998 |
| HCNOT s -> NOT (AP s) |

1999 |
| HCAT (s, f1) -> AT (s, f1.HC.fml) |

2000 |
| HCOR (f1, f2) -> OR (f1.HC.fml, f2.HC.fml) |

2001 |
| HCAND (f1, f2) -> AND (f1.HC.fml, f2.HC.fml) |

2002 |
| HCEX (s, f1) -> EX (s, f1.HC.fml) |

2003 |
| HCAX (s, f1) -> AX (s, f1.HC.fml) |

2004 |
| HCENFORCES (s, f1) -> ENFORCES (s, f1.HC.fml) |

2005 |
| HCALLOWS (s, f1) -> ALLOWS (s, f1.HC.fml) |

2006 |
| HCMORETHAN (n, s, f1) -> MORETHAN (n, s, f1.HC.fml) |

2007 |
| HCMAXEXCEPT (n, s, f1) -> MAXEXCEPT (n, s, f1.HC.fml) |

2008 |
| HCATLEASTPROB (p, f1) -> ATLEASTPROB (p, f1.HC.fml) |

2009 |
| HCLESSPROBFAIL (p, f1) -> LESSPROBFAIL (p, f1.HC.fml) |

2010 |
| HCCONST s -> CONST s |

2011 |
| HCCONSTN s -> CONSTN s |

2012 |
| HCID (f1) -> ID(f1.HC.fml) |

2013 |
| HCNORM (f1, f2) -> NORM(f1.HC.fml, f2.HC.fml) |

2014 |
| HCNORMN (f1, f2) -> NORMN(f1.HC.fml, f2.HC.fml) |

2015 |
| HCCHC (f1, f2) -> CHC (f1.HC.fml, f2.HC.fml) |

2016 |
| HCFUS (first, f1) -> FUS (first, f1.HC.fml) |

2017 |
| HCMU (var, f1) -> MU (var, f1.HC.fml) |

2018 |
| HCNU (var, f1) -> NU (var, f1.HC.fml) |

2019 | |

2020 |
(** Determines the negation (in negation normal form) of a formula node. |

2021 |
@param f A formula node. |

2022 |
@return The negation (in negation normal form) of f. |

2023 |
*) |

2024 |
let negNde_hcFormula_node f = |

2025 |
match f with |

2026 |
| HCTRUE -> HCFALSE |

2027 |
| HCFALSE -> HCTRUE |

2028 |
| HCAP s -> HCNOT s |

2029 |
| HCNOT s -> HCAP s |

2030 |
| HCVAR s -> f |

2031 |
| HCAT (s, f1) -> HCAT (s, f1.HC.neg) |

2032 |
| HCOR (f1, f2) -> HCAND (f1.HC.neg, f2.HC.neg) |

2033 |
| HCAND (f1, f2) -> HCOR (f1.HC.neg, f2.HC.neg) |

2034 |
| HCEX (s, f2) -> HCAX (s, f2.HC.neg) |

2035 |
| HCAX (s, f2) -> HCEX (s, f2.HC.neg) |

2036 |
| HCENFORCES (s, f2) -> HCALLOWS (s, f2.HC.neg) |

2037 |
| HCALLOWS (s, f2) -> HCENFORCES (s, f2.HC.neg) |

2038 |
| HCMORETHAN (n, s, f1) -> HCMAXEXCEPT (n, s, f1.HC.neg) |

2039 |
| HCMAXEXCEPT (n, s, f1) -> HCMORETHAN (n, s, f1.HC.neg) |

2040 |
| HCATLEASTPROB (p, f1) -> HCLESSPROBFAIL (p, f1.HC.neg) |

2041 |
| HCLESSPROBFAIL (p, f1) -> HCATLEASTPROB (p, f1.HC.neg) |

2042 |
| HCCONST s -> HCCONSTN s |

2043 |
| HCCONSTN s -> HCCONST s |

2044 |
| HCID (f1) -> HCID(f1.HC.neg) |

2045 |
| HCNORM (f1, f2) -> HCNORMN(f1.HC.neg, f2.HC.neg) |

2046 |
| HCNORMN (f1, f2) -> HCNORM(f1.HC.neg, f2.HC.neg) |

2047 |
| HCCHC (f1, f2) -> HCCHC (f1.HC.neg, f2.HC.neg) |

2048 |
| HCFUS (first, f1) -> HCFUS (first, f1.HC.neg) |

2049 |
| HCMU (name, f1) -> HCNU (name, f1.HC.neg) |

2050 |
| HCNU (name, f1) -> HCMU (name, f1.HC.neg) |

2051 | |

2052 |
(** An instantiation of hash-consing for formulae. |

2053 |
*) |

2054 |
module HcFormula = HC.Make( |

2055 |
struct |

2056 |
type nde = hcFormula_node |

2057 |
type fml = formula |

2058 |
let equal (n1 : nde) n2 = equal_hcFormula_node n1 n2 |

2059 |
let hash (n : nde) = hash_hcFormula_node n |

2060 |
let negNde (n : nde) = negNde_hcFormula_node n |

2061 |
let toFml (n : nde) = toFml_hcFormula_node n |

2062 |
end |

2063 |
) |

2064 | |

2065 |
(** Converts a formula into its hash-consed version. |

2066 |
@param hcF A hash-cons table for formulae. |

2067 |
@param f A formula in negation normal form. |

2068 |
@return The hash-consed version of f. |

2069 |
@raise CoAlgException if f is not in negation normal form. |

2070 |
*) |

2071 |
let rec hc_formula hcF f = |

2072 |
match f with |

2073 |
| TRUE -> HcFormula.hashcons hcF HCTRUE |

2074 |
| FALSE -> HcFormula.hashcons hcF HCFALSE |

2075 |
| AP s -> HcFormula.hashcons hcF (HCAP s) |

2076 |
| VAR s -> HcFormula.hashcons hcF (HCVAR s) |

2077 |
| NOT (AP s) -> HcFormula.hashcons hcF (HCNOT s) |

2078 |
| AT (s, f1) -> |

2079 |
let tf1 = hc_formula hcF f1 in |

2080 |
HcFormula.hashcons hcF (HCAT (s, tf1)) |

2081 |
| OR (f1, f2) -> |

2082 |
let tf1 = hc_formula hcF f1 in |

2083 |
let tf2 = hc_formula hcF f2 in |

2084 |
HcFormula.hashcons hcF (HCOR (tf1, tf2)) |

2085 |
| AND (f1, f2) -> |

2086 |
let tf1 = hc_formula hcF f1 in |

2087 |
let tf2 = hc_formula hcF f2 in |

2088 |
HcFormula.hashcons hcF (HCAND (tf1, tf2)) |

2089 |
| NOT _ |

2090 |
| EQU _ |

2091 |
| MIN _ |

2092 |
| MAX _ |

2093 |
| IMP _ -> raise (CoAlgException "Formula is not in negation normal form.") |

2094 |
| EX (s, f1) -> |

2095 |
let tf1 = hc_formula hcF f1 in |

2096 |
HcFormula.hashcons hcF (HCEX (s, tf1)) |

2097 |
| AX (s, f1) -> |

2098 |
let tf1 = hc_formula hcF f1 in |

2099 |
HcFormula.hashcons hcF (HCAX (s, tf1)) |

2100 |
| ENFORCES (s, f1) -> |

2101 |
let tf1 = hc_formula hcF f1 in |

2102 |
HcFormula.hashcons hcF (HCENFORCES (s, tf1)) |

2103 |
| ALLOWS (s, f1) -> |

2104 |
let tf1 = hc_formula hcF f1 in |

2105 |
HcFormula.hashcons hcF (HCALLOWS (s, tf1)) |

2106 |
| MORETHAN (n, s, f1) -> |

2107 |
let tf1 = hc_formula hcF f1 in |

2108 |
HcFormula.hashcons hcF (HCMORETHAN (n, s, tf1)) |

2109 |
| MAXEXCEPT (n, s, f1) -> |

2110 |
let tf1 = hc_formula hcF f1 in |

2111 |
HcFormula.hashcons hcF (HCMAXEXCEPT (n, s, tf1)) |

2112 |
| ATLEASTPROB (p, f1) -> |

2113 |
HcFormula.hashcons hcF (HCATLEASTPROB (p, hc_formula hcF f1)) |

2114 |
| LESSPROBFAIL (p, f1) -> |

2115 |
HcFormula.hashcons hcF (HCLESSPROBFAIL (p, hc_formula hcF f1)) |

2116 |
| CONST s -> |

2117 |
HcFormula.hashcons hcF (HCCONST s) |

2118 |
| CONSTN s -> |

2119 |
HcFormula.hashcons hcF (HCCONSTN s) |

2120 |
| ID f1 -> |

2121 |
let tf1 = hc_formula hcF f1 in |

2122 |
HcFormula.hashcons hcF (HCID tf1) |

2123 |
| NORM (f1, f2) -> |

2124 |
let tf1 = hc_formula hcF f1 in |

2125 |
let tf2 = hc_formula hcF f2 in |

2126 |
HcFormula.hashcons hcF (HCNORM (tf1, tf2)) |

2127 |
| NORMN (f1, f2) -> |

2128 |
let tf1 = hc_formula hcF f1 in |

2129 |
let tf2 = hc_formula hcF f2 in |

2130 |
HcFormula.hashcons hcF (HCNORMN (tf1, tf2)) |

2131 |
| CHC (f1, f2) -> |

2132 |
let tf1 = hc_formula hcF f1 in |

2133 |
let tf2 = hc_formula hcF f2 in |

2134 |
HcFormula.hashcons hcF (HCCHC (tf1, tf2)) |

2135 |
| FUS (first, f1) -> |

2136 |
let tf1 = hc_formula hcF f1 in |

2137 |
HcFormula.hashcons hcF (HCFUS (first, tf1)) |

2138 |
| MU (var, f1) -> |

2139 |
let tf1 = hc_formula hcF f1 in |

2140 |
HcFormula.hashcons hcF (HCMU (var, tf1)) |

2141 |
| NU (var, f1) -> |

2142 |
let tf1 = hc_formula hcF f1 in |

2143 |
HcFormula.hashcons hcF (HCNU (var, tf1)) |

2144 |
| AF _ |

2145 |
| EF _ |

2146 |
| AG _ |

2147 |
| EG _ |

2148 |
| AU _ |

2149 |
| EU _ -> |

2150 |
raise (CoAlgException ("nnf: CTL should have been removed at this point")) |

2151 | |

2152 |
(* Replace the Variable name in f with formula formula |

2153 |
hc_replace foo φ ψ => ψ[foo |-> φ] |

2154 |
*) |

2155 |
let rec hc_replace hcF name (formula: hcFormula) (f: hcFormula) = |

2156 |
let func = hc_replace hcF name formula in |

2157 |
let gennew = HcFormula.hashcons hcF in |

2158 |
match f.HC.node with |

2159 |
| HCTRUE |

2160 |
| HCFALSE |

2161 |
| HCAP _ |

2162 |
| HCNOT _ |

2163 |
| HCCONST _ |

2164 |
| HCCONSTN _ -> f |

2165 |
| HCVAR s -> |

2166 |
if compare s name == 0 |

2167 |
then formula |

2168 |
else f |

2169 |
| HCAT (s, f1) -> |

2170 |
let nf1 = func f1 in |

2171 |
if nf1 == f1 then f else gennew (HCAT(s, nf1)) |

2172 |
| HCOR (f1, f2) -> |

2173 |
let nf1 = func f1 in |

2174 |
let nf2 = func f2 in |

2175 |
if nf1 == f1 && nf2 == f2 then f else gennew (HCOR(nf1, nf2)) |

2176 |
| HCAND (f1, f2) -> |

2177 |
let nf1 = func f1 in |

2178 |
let nf2 = func f2 in |

2179 |
if nf1 == f1 && nf2 == f2 then f else gennew (HCAND(nf1, nf2)) |

2180 |
| HCEX (s, f1) -> |

2181 |
let nf1 = func f1 in |

2182 |
if nf1 == f1 then f else gennew (HCEX(s, nf1)) |

2183 |
| HCAX (s, f1) -> |

2184 |
let nf1 = func f1 in |

2185 |
if nf1 == f1 then f else gennew (HCAX(s, nf1)) |

2186 |
| HCENFORCES (s, f1) -> |

2187 |
let nf1 = func f1 in |

2188 |
if nf1 == f1 then f else gennew (HCENFORCES(s, nf1)) |

2189 |
| HCALLOWS (s, f1) -> |

2190 |
let nf1 = func f1 in |

2191 |
if nf1 == f1 then f else gennew (HCALLOWS(s, nf1)) |

2192 |
| HCMORETHAN (n, s, f1) -> |

2193 |
let nf1 = func f1 in |

2194 |
if nf1 == f1 then f else gennew (HCMORETHAN(n, s, nf1)) |

2195 |
| HCMAXEXCEPT (n, s, f1) -> |

2196 |
let nf1 = func f1 in |

2197 |
if nf1 == f1 then f else gennew (HCMAXEXCEPT(n, s, nf1)) |

2198 |
| HCATLEASTPROB (p, f1) -> |

2199 |
let nf1 = func f1 in |

2200 |
if nf1 == f1 then f else gennew (HCATLEASTPROB(p, nf1)) |

2201 |
| HCLESSPROBFAIL (p, f1) -> |

2202 |
let nf1 = func f1 in |

2203 |
if nf1 == f1 then f else gennew (HCLESSPROBFAIL(p, nf1)) |

2204 |
| HCID f1 -> |

2205 |
let nf1 = func f1 in |

2206 |
if nf1 == f1 then f else gennew (HCID(nf1)) |

2207 |
| HCNORM (f1, f2) -> |

2208 |
let nf1 = func f1 in |

2209 |
let nf2 = func f2 in |

2210 |
if nf1 == f1 && nf2 == f2 then f else gennew (HCNORM(nf1, nf2)) |

2211 |
| HCNORMN (f1, f2) -> |

2212 |
let nf1 = func f1 in |

2213 |
let nf2 = func f2 in |

2214 |
if nf1 == f1 && nf2 == f2 then f else gennew (HCNORMN(nf1, nf2)) |

2215 |
| HCCHC (f1, f2) -> |

2216 |
let nf1 = func f1 in |

2217 |
let nf2 = func f2 in |

2218 |
if nf1 == f1 && nf2 == f2 then f else gennew (HCCHC(nf1, nf2)) |

2219 |
| HCFUS (first, f1) -> |

2220 |
let nf1 = func f1 in |

2221 |
if nf1 == f1 then f else gennew (HCFUS(first, nf1)) |

2222 |
| HCMU (var, f1) -> |

2223 |
if compare var name != 0 then |

2224 |
let nf1 = func f1 in |

2225 |
if nf1 == f1 then f else gennew (HCMU(var, nf1)) |

2226 |
else |

2227 |
f |

2228 |
| HCNU (var, f1) -> |

2229 |
if compare var name != 0 then |

2230 |
let nf1 = func f1 in |

2231 |
if nf1 == f1 then f else gennew (HCNU(var, nf1)) |

2232 |
else |

2233 |
f |

2234 | |

2235 |
let rec hc_freeIn variable (f: hcFormula) = |

2236 |
match f.HC.node with |

2237 |
| HCTRUE |

2238 |
| HCFALSE |

2239 |
| HCAP _ |

2240 |
| HCNOT _ |

2241 |
| HCCONST _ |

2242 |
| HCCONSTN _ -> false |

2243 |
| HCVAR s -> |

2244 |
if compare variable s == 0 |

2245 |
then true |

2246 |
else false |

2247 |
| HCAT (s, f1) -> |

2248 |
hc_freeIn variable f1 |

2249 |
| HCOR (f1, f2) |

2250 |
| HCAND (f1, f2) -> |

2251 |
hc_freeIn variable f1 || hc_freeIn variable f2 |

2252 |
| HCEX (_, f1) |

2253 |
| HCAX (_, f1) |

2254 |
| HCENFORCES (_, f1) |

2255 |
| HCALLOWS (_, f1) |

2256 |
| HCMORETHAN (_, _, f1) |

2257 |
| HCMAXEXCEPT (_, _, f1) |

2258 |
| HCATLEASTPROB (_, f1) |

2259 |
| HCLESSPROBFAIL (_, f1) |

2260 |
| HCID f1 -> |

2261 |
hc_freeIn variable f1 |

2262 |
| HCNORM (f1, f2) |

2263 |
| HCNORMN (f1, f2) |

2264 |
| HCCHC (f1, f2) -> |

2265 |
hc_freeIn variable f1 || hc_freeIn variable f2 |

2266 |
| HCFUS (first, f1) -> |

2267 |
hc_freeIn variable f1 |

2268 |
| HCMU (var, f1) |

2269 |
| HCNU (var, f1) -> |

2270 |
(* Do we need to exclude bound variables here? *) |

2271 |
hc_freeIn variable f1 |

2272 | |

2273 | |

2274 |
(** An instantiation of a hash table (of the standard library) |

2275 |
for hash-consed formulae. The test for equality |

2276 |
and computing the hash value is done in constant time. |

2277 |
*) |

2278 |
module HcFHt = Hashtbl.Make( |

2279 |
struct |

2280 |
type t = hcFormula |

2281 |
let equal (f1 : t) f2 = f1.HC.tag = f2.HC.tag |

2282 |
let hash (f : t) = f.HC.tag |

2283 |
end |

2284 |
) |