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

History | View | Annotate | Download (71.3 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 |
| AR of formula * formula |

71 |
| ER of formula * formula |

72 |
| AB of formula * formula |

73 |
| EB of formula * formula |

74 | |

75 | |

76 |
(** Defines (unsorted) coalgebraic axioms for the TBox. |

77 |
*) |

78 |
type axiom = |

79 |
| DEFINITION of formula * formula |

80 |
| INCLUSION of formula * formula |

81 | |

82 |
exception ConversionException of formula |

83 | |

84 |
(** Defines sorted coalgebraic formulae. |

85 |
*) |

86 |
type sortedFormula = sort * formula |

87 | |

88 | |

89 |
(** Defines sorted coalgebraic axioms. |

90 |
*) |

91 |
type sortedAxiom = sort * axiom |

92 | |

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

94 |
@param A string s. |

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

96 |
*) |

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

98 | |

99 | |

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

101 |
@param f A formula. |

102 |
@return The size of f. |

103 |
*) |

104 |
let rec sizeFormula f = |

105 |
match f with |

106 |
| TRUE |

107 |
| FALSE |

108 |
| AP _ -> 1 |

109 |
| NOT f1 |

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

111 |
| OR (f1, f2) |

112 |
| AND (f1, f2) |

113 |
| EQU (f1, f2) |

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

115 |
| EX (_, f1) |

116 |
| AX (_, f1) |

117 |
| ENFORCES (_, f1) |

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

119 |
| MIN (_, _, f1) |

120 |
| MAX (_, _, f1) |

121 |
| ATLEASTPROB (_, f1) |

122 |
| LESSPROBFAIL (_, f1) |

123 |
| MORETHAN (_, _, f1) |

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

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

126 |
| NORM(f1, f2) |

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

128 |
| CONST _ |

129 |
| CONSTN _ -> 1 |

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

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

132 |
| MU (_, f1) |

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

134 |
| VAR _ -> 1 |

135 |
| AF _ | EF _ |

136 |
| AG _ | EG _ |

137 |
| AU _ | EU _ |

138 |
| AR _ | ER _ |

139 |
| AB _ | EB _ -> |

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

141 | |

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

143 |
@param f A sorted formula. |

144 |
@return The size of f. |

145 |
*) |

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

147 | |

148 | |

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

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

151 |
let rec iter func formula = |

152 |
func formula; |

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

154 |
match formula with |

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

156 |
| CONST _ |

157 |
| CONSTN _ -> () |

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

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

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

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

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

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

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

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

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

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

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

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

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

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

172 |
| AU (f1, f2) | EU (f1, f2) |

173 |
| AR (f1, f2) | ER (f1, f2) |

174 |
| AB (f1, f2) | EB (f1, f2) -> (proc f1; proc f2) |

175 | |

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

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

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

179 |
let formula = (match formula with |

180 |
(* 0-ary constructors *) |

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

182 |
| CONST _ |

183 |
| CONSTN _ -> formula |

184 |
(* unary *) |

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

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

187 |
(* binary *) |

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

214 |
| EU (f1, f2) -> EU (c f1, c f2) |

215 |
| AR (f1, f2) -> AR (c f1, c f2) |

216 |
| ER (f1, f2) -> ER (c f1, c f2) |

217 |
| AB (f1, f2) -> AB (c f1, c f2) |

218 |
| EB (f1, f2) -> EB (c f1, c f2)) |

219 |
in |

220 |
func formula |

221 | |

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

223 |
let helper formula = match formula with |

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

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

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

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

228 |
| TRUE | FALSE |

229 |
| EQU _ | IMP _ |

230 |
| AND _ | OR _ |

231 |
| AP _ | NOT _ |

232 |
| AX _ | EX _ |

233 |
| CHC _ | FUS _ -> formula |

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

235 |
in |

236 |
convert_post helper formula |

237 | |

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

239 |
let helper formula = match formula with |

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

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

242 |
| TRUE | FALSE |

243 |
| EQU _ | IMP _ |

244 |
| AND _ | OR _ |

245 |
| AP _ | NOT _ |

246 |
| CHC _ | FUS _ -> formula |

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

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

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

250 |
in |

251 |
convert_post helper formula |

252 | |

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

254 | |

255 |
let convertToMu formula = |

256 |
let name = Stream.next gensym in |

257 |
let helper formula = |

258 |
match formula with |

259 |
| AF f1 -> |

260 |
MU (name, (OR (f1, (AX ("", (VAR name)))))) |

261 |
| EF f1 -> |

262 |
MU (name, (OR (f1, (EX ("", (VAR name)))))) |

263 |
| AG f1 -> |

264 |
NU (name, (AND (f1, (AX ("", (VAR name)))))) |

265 |
| EG f1 -> |

266 |
NU (name, (AND (f1, (EX ("", (VAR name)))))) |

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

268 |
MU (name, (OR (f2, (AND (f1, (AX ("", (VAR name)))))))) |

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

270 |
MU (name, (OR (f2, (AND (f1, (EX ("", (VAR name)))))))) |

271 |
| AR (f1, f2) -> |

272 |
NU (name, (AND (f2, (OR (f1, (AX ("", (VAR name)))))))) |

273 |
| ER (f1, f2) -> |

274 |
NU (name, (AND (f2, (OR (f1, (EX ("", (VAR name)))))))) |

275 |
| AB (f1, f2) -> |

276 |
NOT (MU (name, (OR (f2, (AND ((NOT f1), (EX ("", (VAR name))))))))) |

277 |
| EB (f1, f2) -> |

278 |
NOT (MU (name, (OR (f2, (AND ((NOT f1), (AX ("", (VAR name))))))))) |

279 |
| _ -> formula |

280 |
in |

281 |
convert_post helper formula |

282 | |

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

284 |
Parentheses are ommited where possible |

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

286 |
@param sb A string buffer. |

287 |
@param f A formula. |

288 |
*) |

289 |
let rec exportFormula_buffer sb f = |

290 |
let negate = function |

291 |
| NOT f -> f |

292 |
| f -> NOT f |

293 |
in |

294 |
let prio n lf = |

295 |
let prionr = function |

296 |
| EQU _ -> 0 |

297 |
| IMP _ -> 1 |

298 |
| OR _ -> 2 |

299 |
| AND _ -> 3 |

300 |
| _ -> 4 |

301 |
in |

302 |
if prionr lf < n then begin |

303 |
Buffer.add_char sb '('; |

304 |
exportFormula_buffer sb lf; |

305 |
Buffer.add_char sb ')' |

306 |
end |

307 |
else exportFormula_buffer sb lf |

308 |
in |

309 |
match f with |

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

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

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

313 |
| NOT f1 -> |

314 |
Buffer.add_string sb "~"; |

315 |
prio 4 f1 |

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

317 |
Buffer.add_string sb "@ "; |

318 |
Buffer.add_string sb s; |

319 |
Buffer.add_string sb " "; |

320 |
prio 4 f1 |

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

322 |
prio 2 f1; |

323 |
Buffer.add_string sb " | "; |

324 |
prio 2 f2 |

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

326 |
prio 3 f1; |

327 |
Buffer.add_string sb " & "; |

328 |
prio 3 f2 |

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

330 |
prio 0 f1; |

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

332 |
prio 0 f2 |

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

334 |
prio 2 f1; |

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

336 |
prio 2 f2 |

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

338 |
Buffer.add_string sb "<"; |

339 |
Buffer.add_string sb s; |

340 |
Buffer.add_string sb ">"; |

341 |
prio 4 f1 |

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

343 |
Buffer.add_string sb "["; |

344 |
Buffer.add_string sb s; |

345 |
Buffer.add_string sb "]"; |

346 |
prio 4 f1 |

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

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

349 |
Buffer.add_string sb ( |

350 |
match s with |

351 |
| [] -> " " |

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

353 |
); |

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

355 |
prio 4 f1 |

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

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

358 |
Buffer.add_string sb ( |

359 |
match s with |

360 |
| [] -> " " |

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

362 |
); |

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

364 |
prio 4 f1 |

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

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

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

368 |
Buffer.add_string sb "}"; |

369 |
prio 4 f1 |

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

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

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

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

374 |
prio 4 f1 |

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

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

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

378 |
Buffer.add_string sb " "; |

379 |
Buffer.add_string sb s; |

380 |
Buffer.add_string sb "}"; |

381 |
prio 4 f1 |

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

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

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

385 |
Buffer.add_string sb " "; |

386 |
Buffer.add_string sb s; |

387 |
Buffer.add_string sb "}"; |

388 |
prio 4 f1 |

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

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

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

392 |
Buffer.add_string sb " "; |

393 |
Buffer.add_string sb s; |

394 |
Buffer.add_string sb "}"; |

395 |
prio 4 f1 |

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

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

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

399 |
Buffer.add_string sb " ~ "; |

400 |
Buffer.add_string sb s; |

401 |
Buffer.add_string sb "}"; |

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

403 |
| ID (f1) -> |

404 |
Buffer.add_string sb "O"; |

405 |
prio 4 f1 |

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

407 |
Buffer.add_string sb "("; |

408 |
exportFormula_buffer sb f1; |

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

410 |
exportFormula_buffer sb f2; |

411 |
Buffer.add_string sb ")" |

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

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

414 |
exportFormula_buffer sb (negate f1); |

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

416 |
exportFormula_buffer sb (negate f2); |

417 |
Buffer.add_string sb ")" |

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

419 |
Buffer.add_string sb "("; |

420 |
exportFormula_buffer sb f1; |

421 |
Buffer.add_string sb " + "; |

422 |
exportFormula_buffer sb f2; |

423 |
Buffer.add_string sb ")" |

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

425 |
Buffer.add_string sb s |

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

427 |
Buffer.add_string sb s |

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

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

430 |
prio 4 f1 |

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

432 |
Buffer.add_string sb "μ"; |

433 |
Buffer.add_string sb s; |

434 |
Buffer.add_string sb "."; |

435 |
prio 4 f1 |

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

437 |
Buffer.add_string sb "ν"; |

438 |
Buffer.add_string sb s; |

439 |
Buffer.add_string sb "."; |

440 |
prio 4 f1 |

441 |
| VAR s -> |

442 |
Buffer.add_string sb s |

443 |
| AF f1 -> |

444 |
Buffer.add_string sb "AF "; |

445 |
prio 4 f1 |

446 |
| EF f1 -> |

447 |
Buffer.add_string sb "EF "; |

448 |
prio 4 f1 |

449 |
| AG f1 -> |

450 |
Buffer.add_string sb "AG "; |

451 |
prio 4 f1 |

452 |
| EG f1 -> |

453 |
Buffer.add_string sb "EG "; |

454 |
prio 4 f1 |

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

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

457 |
prio 4 f1; |

458 |
Buffer.add_string sb " U "; |

459 |
prio 4 f2; |

460 |
Buffer.add_string sb ")" |

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

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

463 |
prio 4 f1; |

464 |
Buffer.add_string sb " U "; |

465 |
prio 4 f2; |

466 |
Buffer.add_string sb ")" |

467 |
| AR (f1, f2) -> |

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

469 |
prio 4 f1; |

470 |
Buffer.add_string sb " R "; |

471 |
prio 4 f2; |

472 |
Buffer.add_string sb ")" |

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

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

475 |
prio 4 f1; |

476 |
Buffer.add_string sb " R "; |

477 |
prio 4 f2; |

478 |
Buffer.add_string sb ")" |

479 |
| AB (f1, f2) -> |

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

481 |
prio 4 f1; |

482 |
Buffer.add_string sb " B "; |

483 |
prio 4 f2; |

484 |
Buffer.add_string sb ")" |

485 |
| EB (f1, f2) -> |

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

487 |
prio 4 f1; |

488 |
Buffer.add_string sb " B "; |

489 |
prio 4 f2; |

490 |
Buffer.add_string sb ")" |

491 | |

492 | |

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

494 |
Parentheses are ommited where possible |

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

496 |
@param f A formula. |

497 |
@return A string representing f. |

498 |
*) |

499 |
let exportFormula f = |

500 |
let sb = Buffer.create 128 in |

501 |
exportFormula_buffer sb f; |

502 |
Buffer.contents sb |

503 | |

504 |
let string_of_formula = exportFormula |

505 | |

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

507 |
let rec exportTatlFormula_buffer sb f = |

508 |
let prio n lf = |

509 |
let prionr = function |

510 |
| EQU _ -> 0 |

511 |
| IMP _ -> 1 |

512 |
| OR _ -> 2 |

513 |
| AND _ -> 3 |

514 |
| _ -> 4 |

515 |
in |

516 |
if prionr lf < n then begin |

517 |
Buffer.add_char sb '('; |

518 |
exportTatlFormula_buffer sb lf; |

519 |
Buffer.add_char sb ')' |

520 |
end |

521 |
else exportTatlFormula_buffer sb lf |

522 |
in |

523 |
match f with |

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

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

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

527 |
| NOT f1 -> |

528 |
Buffer.add_string sb "~"; |

529 |
prio 4 f1 |

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

531 |
prio 2 f1; |

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

533 |
prio 2 f2 |

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

535 |
prio 3 f1; |

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

537 |
prio 3 f2 |

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

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

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

541 |
prio 2 f1; |

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

543 |
prio 2 f2 |

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

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

546 |
Buffer.add_string sb ( |

547 |
match s with |

548 |
| [] -> " " |

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

550 |
); |

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

552 |
prio 4 f1 |

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

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

555 |
Buffer.add_string sb ( |

556 |
match s with |

557 |
| [] -> " " |

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

559 |
); |

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

561 |
prio 4 f1 |

562 |
| EX _ |

563 |
| AX _ |

564 |
| MIN _ |

565 |
| MAX _ |

566 |
| MORETHAN _ |

567 |
| MAXEXCEPT _ |

568 |
| AT _ |

569 |
| CONST _ |

570 |
| CONSTN _ |

571 |
| CHC _ |

572 |
| ATLEASTPROB _ |

573 |
| LESSPROBFAIL _ |

574 |
| ID _ |

575 |
| NORM _ |

576 |
| NORMN _ |

577 |
| FUS _ |

578 |
| MU _ |

579 |
| NU _ |

580 |
| VAR _ |

581 |
| AF _ |

582 |
| EF _ |

583 |
| AG _ |

584 |
| EG _ |

585 |
| AU _ |

586 |
| EU _ |

587 |
| AR _ |

588 |
| ER _ |

589 |
| AB _ |

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

591 | |

592 |
let exportTatlFormula f = |

593 |
let sb = Buffer.create 128 in |

594 |
exportTatlFormula_buffer sb f; |

595 |
Buffer.contents sb |

596 | |

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

598 |
Parentheses are ommited where possible |

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

600 |
@param sb A string buffer. |

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

602 |
*) |

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

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

605 |
Buffer.add_string sb ": "; |

606 |
exportFormula_buffer sb f |

607 | |

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

609 |
Parentheses are ommited where possible |

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

611 |
@param f A sorted formula. |

612 |
@return A string representing f. |

613 |
*) |

614 |
let exportSortedFormula f = |

615 |
let sb = Buffer.create 128 in |

616 |
exportSortedFormula_buffer sb f; |

617 |
Buffer.contents sb |

618 | |

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

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

621 |
@param f A sorted formula. |

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

623 |
*) |

624 |
let exportQuery tbox f = |

625 |
let sb = Buffer.create 1000 in |

626 |
let rec expFl = function |

627 |
| [] -> () |

628 |
| h::tl -> |

629 |
exportSortedFormula_buffer sb h; |

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

631 |
expFl tl |

632 |
in |

633 |
expFl tbox; |

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

635 |
exportSortedFormula_buffer sb f; |

636 |
Buffer.contents sb |

637 | |

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

639 |
coalg can read it again using importQuery |

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

641 |
@param f A sorted formula. |

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

643 |
*) |

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

645 |
let sb = Buffer.create 1000 in |

646 |
let rec expFl = function |

647 |
| [] -> () |

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

649 |
exportFormula_buffer sb h; |

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

651 |
expFl tl |

652 |
in |

653 |
expFl tbox; |

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

655 |
exportFormula_buffer sb f; |

656 |
Buffer.contents sb |

657 | |

658 | |

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

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

661 |
*) |

662 |
let lexer = A.make_lexer |

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

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

665 |
;"μ";"ν";"." |

666 |
;"AX";"EX";"AF";"EF";"AG";"EG";"A";"E";"U";"R";"B" |

667 |
] |

668 | |

669 |
let mk_exn s = CoAlgException s |

670 | |

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

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

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

674 |
*) |

675 |
let rec verifyMuAltFree formula = |

676 |
let proc = verifyMuAltFree in |

677 |
match formula with |

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

679 |
| CONST _ |

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

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

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

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

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

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

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

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

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

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

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

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

692 |
else |

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

708 |
else |

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

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

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

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

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

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

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

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

717 |
if newfree = [] then |

718 |
("none", []) |

719 |
else |

720 |
("μ", newfree) |

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

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

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

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

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

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

727 |
if newfree = [] then |

728 |
("none", []) |

729 |
else |

730 |
("ν", newfree) |

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

732 |
| AF _ | EF _ | AG _ | EG _ | AU _ | EU _ | AR _ | ER _ | AB _ | EB _ -> |

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

734 | |

735 | |

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

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

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

739 |
negations is even. |

740 |
*) |

741 |
let rec verifyMuMonotone negations formula = |

742 |
let proc = verifyMuMonotone negations in |

743 |
match formula with |

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

745 |
| CONST _ |

746 |
| CONSTN _ -> () |

747 |
| AT (_,a) |

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

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

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

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

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

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

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

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

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

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

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

759 |
| MU (s, f) |

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

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

762 |
verifyMuMonotone newNeg f |

763 |
| VAR s -> |

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

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

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

767 |
| NOT a -> |

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

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

770 |
verifyMuMonotone newNeg a |

771 |
| AF _ | EF _ | AG _ | EG _ | AU _ | EU _ | AR _ | ER _ | AB _ | EB _ -> |

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

773 | |

774 |
let rec verifyMuGuarded unguarded formula = |

775 |
let proc = verifyMuGuarded unguarded in |

776 |
match formula with |

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

778 |
| CONST _ |

779 |
| CONSTN _ -> () |

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

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

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

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

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

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

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

787 |
| MORETHAN (_,_,a) | MAXEXCEPT (_,_,a) -> verifyMuGuarded [] a |

788 |
| ID(a) -> verifyMuGuarded [] a |

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

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

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

792 |
| MU (s, f) |

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

794 |
let newUnguard = s :: unguarded in |

795 |
verifyMuGuarded newUnguard f |

796 |
| VAR s -> |

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

798 |
if List.exists finder unguarded then |

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

800 |
| AF _ | EF _ | AG _ | EG _ | AU _ | EU _ | AR _ | ER _ | AB _ | EB _ -> |

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

802 | |

803 |
let verifyFormula formula = |

804 |
verifyMuAltFree formula; |

805 |
verifyMuMonotone [] formula; |

806 |
verifyMuGuarded [] formula |

807 | |

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

809 |
It is a standard recursive descent procedure. |

810 |
@param ts A token stream. |

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

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

813 |
*) |

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

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

816 |
let f1 = convertToMu formula in |

817 |
match Stream.peek ts with |

818 |
| None -> f1 |

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

820 |
Stream.junk ts; |

821 |
let f2 = parse_formula symtab ts in |

822 |
EQU (f1, f2) |

823 |
| _ -> f1 |

824 | |

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

826 |
It is a standard recursive descent procedure. |

827 |
@param ts A token stream. |

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

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

830 |
*) |

831 |
and parse_imp symtab ts= |

832 |
let f1 = parse_or symtab ts in |

833 |
match Stream.peek ts with |

834 |
| None -> f1 |

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

836 |
Stream.junk ts; |

837 |
let f2 = parse_imp symtab ts in |

838 |
IMP (f1, f2) |

839 |
| _ -> f1 |

840 | |

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

842 |
It is a standard recursive descent procedure. |

843 |
@param ts A token stream. |

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

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

846 |
*) |

847 |
and parse_or symtab ts = |

848 |
let f1 = parse_and symtab ts in |

849 |
match Stream.peek ts with |

850 |
| None -> f1 |

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

852 |
Stream.junk ts; |

853 |
let f2 = parse_or symtab ts in |

854 |
OR (f1, f2) |

855 |
| _ -> f1 |

856 | |

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

858 |
It is a standard recursive descent procedure. |

859 |
@param ts A token stream. |

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

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

862 |
*) |

863 |
and parse_and symtab ts = |

864 |
let f1 = parse_cimp symtab ts in |

865 |
match Stream.peek ts with |

866 |
| None -> f1 |

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

868 |
Stream.junk ts; |

869 |
let f2 = parse_and symtab ts in |

870 |
AND (f1, f2) |

871 |
| _ -> f1 |

872 | |

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

874 |
It is a standard recursive descent procedure. |

875 |
@param ts A token stream. |

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

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

878 |
*) |

879 |
and parse_cimp symtab ts = |

880 |
let f1 = parse_rest symtab ts in |

881 |
match Stream.peek ts with |

882 |
| None -> f1 |

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

884 |
Stream.junk ts; |

885 |
let f2 = parse_cimp symtab ts in |

886 |
NORM (f1, f2) |

887 |
| _ -> f1 |

888 | |

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

890 |
It is a standard recursive descent procedure. |

891 |
@param ts A token stream. |

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

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

894 |
*) |

895 |
and parse_rest symtab ts = |

896 |
let boxinternals noNo es = |

897 |
let n = |

898 |
if noNo then 0 |

899 |
else |

900 |
match Stream.next ts with |

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

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

903 |
in |

904 |
let (s,denominator) = |

905 |
match Stream.peek ts with |

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

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

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

909 |
Stream.junk ts; |

910 |
match Stream.next ts with |

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

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

913 |
end |

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

915 |
in |

916 |
if (denominator < n) then begin |

917 |
let explanation = |

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

919 |
in |

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

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

922 |
) |

923 |
end; |

924 |
let _ = |

925 |
match Stream.next ts with |

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

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

928 |
in |

929 |
(n, denominator, s) |

930 |
in |

931 |
let rec agentlist es = |

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

933 |
match Stream.next ts with |

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

935 |
then n::(agentlist es) |

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

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

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

939 |
in |

940 |
match Stream.next ts with |

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

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

943 |
AP "true" |

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

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

946 |
AP "false" |

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

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

949 |
| A.Ident s -> |

950 |
(try |

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

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

953 |
VAR symbol |

954 |
with Not_found -> AP s) |

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

956 |
let f = parse_rest symtab ts in |

957 |
NOT f |

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

959 |
let s = |

960 |
match Stream.next ts with |

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

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

963 |
in |

964 |
let f = parse_rest symtab ts in |

965 |
AT (s, f) |

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

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

968 |
let f1 = parse_rest symtab ts in |

969 |
EX (s, f1) |

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

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

972 |
let f1 = parse_rest symtab ts in |

973 |
AX (s, f1) |

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

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

976 |
let f1 = parse_rest symtab ts in |

977 |
ENFORCES (ls, f1) |

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

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

980 |
let f1 = parse_rest symtab ts in |

981 |
ALLOWS (ls, f1) |

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

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

984 |
let f1 = parse_rest symtab ts in |

985 |
if (denom <> 0) |

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

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

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

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

990 |
let f1 = parse_rest symtab ts in |

991 |
if (denom <> 0) |

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

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

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

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

996 |
let f1 = parse_rest symtab ts in |

997 |
if (denom <> 0) |

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

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

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

1001 |
match Stream.next ts with |

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

1003 |
| A.Kwd s |

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

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

1006 |
end |

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

1008 |
let f = parse_formula symtab ts in |

1009 |
match Stream.next ts with |

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

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

1012 |
let f2 = parse_formula symtab ts in |

1013 |
match Stream.next ts with |

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

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

1016 |
end |

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

1018 |
end |

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

1020 |
let f = parse_rest symtab ts in |

1021 |
ID f |

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

1023 |
let f = parse_rest symtab ts in |

1024 |
FUS (true, f) |

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

1026 |
let f = parse_rest symtab ts in |

1027 |
FUS (false, f) |

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

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

1030 |
let symbol = Stream.next gensym in |

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

1032 |
let f1 = parse_rest newtab ts in |

1033 |
MU (symbol, f1) |

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

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

1036 |
let symbol = Stream.next gensym in |

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

1038 |
let f1 = parse_rest newtab ts in |

1039 |
NU (symbol, f1) |

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

1041 |
let f = parse_rest symtab ts in |

1042 |
AF f |

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

1044 |
let f = parse_rest symtab ts in |

1045 |
EF f |

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

1047 |
let f = parse_rest symtab ts in |

1048 |
AG f |

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

1050 |
let f = parse_rest symtab ts in |

1051 |
EG f |

1052 |
| A.Kwd "A" -> |

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

1054 |
let f1 = parse_formula symtab ts in begin |

1055 |
match Stream.next ts with |

1056 |
| A.Kwd "U" -> |

1057 |
let f2 = parse_formula symtab ts in |

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

1059 |
AU (f1, f2) |

1060 |
| A.Kwd "R" -> |

1061 |
let f2 = parse_formula symtab ts in |

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

1063 |
AR (f1, f2) |

1064 |
| A.Kwd "B" -> |

1065 |
let f2 = parse_formula symtab ts in |

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

1067 |
AB (f1, f2) |

1068 |
| t -> A.printError mk_exn ~t ~ts "one of \"U\" \"R\" \"B\" expected: " |

1069 |
end |

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

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

1072 |
let f1 = parse_formula symtab ts in begin |

1073 |
match Stream.next ts with |

1074 |
| A.Kwd "U" -> |

1075 |
let f2 = parse_formula symtab ts in |

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

1077 |
EU (f1, f2) |

1078 |
| A.Kwd "R" -> |

1079 |
let f2 = parse_formula symtab ts in |

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

1081 |
ER (f1, f2) |

1082 |
| A.Kwd "B" -> |

1083 |
let f2 = parse_formula symtab ts in |

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

1085 |
EB (f1, f2) |

1086 |
| t -> A.printError mk_exn ~t ~ts "one of \"U\" \"R\" \"B\" expected: " |

1087 |
end |

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

1089 |
let f1 = parse_rest symtab ts in |

1090 |
AX ("", f1) |

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

1092 |
let f1 = parse_rest symtab ts in |

1093 |
EX ("", f1) |

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

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

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

1097 | |

1098 |
(** Parses a sorted formula. |

1099 |
@param ts A token stream. |

1100 |
@return A sorted formula. |

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

1102 |
*) |

1103 |
let parse_sortedFormula ts = |

1104 |
let nr = |

1105 |
match Stream.peek ts with |

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

1107 |
if n >= 0 then begin |

1108 |
Stream.junk ts; |

1109 |
let () = |

1110 |
match Stream.next ts with |

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

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

1113 |
in |

1114 |
n |

1115 |
end else |

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

1117 |
| _ -> 0 |

1118 |
in |

1119 |
let f = parse_formula [] ts in |

1120 |
(nr, f) |

1121 | |

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

1123 |
@param ts A token stream. |

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

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

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

1127 |
*) |

1128 |
let rec parse_sortedFormulaList ts acc = |

1129 |
let f1 = parse_sortedFormula ts in |

1130 |
match Stream.peek ts with |

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

1132 |
Stream.junk ts; |

1133 |
parse_sortedFormulaList ts (f1::acc) |

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

1135 | |

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

1137 |
@param fkt An import function. |

1138 |
@param s A string. |

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

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

1141 |
*) |

1142 |
let importWrapper fkt s = |

1143 |
let ts = lexer s in |

1144 |
try |

1145 |
let res = fkt ts in |

1146 |
let _ = |

1147 |
match Stream.peek ts with |

1148 |
| None -> () |

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

1150 |
in |

1151 |
res |

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

1153 | |

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

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

1156 |
@return The resulting formula. |

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

1158 |
*) |

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

1160 | |

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

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

1163 |
@return The sorted formula. |

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

1165 |
*) |

1166 |
let importSortedFormula s = importWrapper parse_sortedFormula s |

1167 | |

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

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

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

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

1172 |
f is a sorted formula. |

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

1174 |
*) |

1175 |
let importQuery s = |

1176 |
let fkt ts = |

1177 |
match Stream.peek ts with |

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

1179 |
Stream.junk ts; |

1180 |
let f = parse_sortedFormula ts in |

1181 |
([], f) |

1182 |
| _ -> |

1183 |
let fl = parse_sortedFormulaList ts [] in |

1184 |
match Stream.peek ts with |

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

1186 |
Stream.junk ts; |

1187 |
let f = parse_sortedFormula ts in |

1188 |
(fl, f) |

1189 |
| _ -> |

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

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

1192 |
in |

1193 |
importWrapper fkt s |

1194 | |

1195 | |

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

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

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

1199 |
@param f A formula. |

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

1201 |
that is equivalent to ~f. |

1202 |
*) |

1203 |
let rec nnfNeg f = |

1204 |
match f with |

1205 |
| TRUE -> FALSE |

1206 |
| FALSE -> TRUE |

1207 |
| AP _ -> NOT f |

1208 |
| VAR _ -> f |

1209 |
| NOT f1 -> nnf f1 |

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

1225 |
| CONST s -> CONSTN s |

1226 |
| CONSTN s -> CONST s |

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

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

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

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

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

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

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

1234 |
| AF _ | EF _ |

1235 |
| AG _ | EG _ |

1236 |
| AU _ | EU _ |

1237 |
| AR _ | ER _ |

1238 |
| AB _ | EB _ -> raise (CoAlgException ("nnfNeg: CTL should have been removed at this point")) |

1239 | |

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

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

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

1243 |
@param f A formula. |

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

1245 |
that is equivalent to f. |

1246 |
*) |

1247 |
and nnf f = |

1248 |
match f with |

1249 |
| TRUE |

1250 |
| FALSE |

1251 |
| AP _ |

1252 |
| NOT (AP _) |

1253 |
| CONST _ |

1254 |
| CONSTN _ |

1255 |
| VAR _ -> f |

1256 |
| NOT f1 -> nnfNeg f1 |

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

1258 |
let ft1 = nnf f1 in |

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

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

1261 |
let ft1 = nnf f1 in |

1262 |
let ft2 = nnf f2 in |

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

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

1265 |
let ft1 = nnf f1 in |

1266 |
let ft2 = nnf f2 in |

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

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

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

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

1271 |
let ft = nnf f1 in |

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

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

1274 |
let ft = nnf f1 in |

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

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

1277 |
let ft = nnf f1 in |

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

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

1280 |
let ft = nnf f1 in |

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

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

1283 |
if n = 0 then TRUE |

1284 |
else |

1285 |
let ft = nnf f1 in |

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

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

1288 |
let ft = nnfNeg f1 in |

1289 |
MAXEXCEPT (n,s, ft) |

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

1291 |
let ft = nnf f1 in |

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

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

1294 |
let ft = nnf f1 in |

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

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

1297 |
let ft = nnf f1 in |

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

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

1300 |
let ft = nnf f1 in |

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

1302 |
| ID (f1) -> |

1303 |
let ft = nnf f1 in |

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

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

1306 |
let ft1 = nnf f1 in |

1307 |
let ft2 = nnf f2 in |

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

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

1310 |
let ft1 = nnf f1 in |

1311 |
let ft2 = nnf f2 in |

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

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

1314 |
let ft1 = nnf f1 in |

1315 |
let ft2 = nnf f2 in |

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

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

1318 |
let ft = nnf f1 in |

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

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

1321 |
let ft = nnf f1 in |

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

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

1324 |
let ft = nnf f1 in |

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

1326 |
| AF _ | EF _ |

1327 |
| AG _ | EG _ |

1328 |
| AU _ | EU _ |

1329 |
| AR _ | ER _ |

1330 |
| AB _ | EB _ -> |

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

1332 | |

1333 |
(** Simplifies a formula. |

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

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

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

1337 |
*) |

1338 |
let rec simplify f = |

1339 |
match f with |

1340 |
| TRUE |

1341 |
| FALSE |

1342 |
| AP _ |

1343 |
| NOT (AP _) |

1344 |
| VAR _ |

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

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

1347 |
let ft = simplify f1 in |

1348 |
begin |

1349 |
match ft with |

1350 |
| FALSE -> FALSE |

1351 |
| TRUE -> TRUE |

1352 |
| AT _ -> ft |

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

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

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

1356 |
end |

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

1358 |
let ft1 = simplify f1 in |

1359 |
let ft2 = simplify f2 in |

1360 |
begin |

1361 |
match ft1, ft2 with |

1362 |
| TRUE, _ -> TRUE |

1363 |
| FALSE, _ -> ft2 |

1364 |
| _, TRUE -> TRUE |

1365 |
| _, FALSE -> ft1 |

1366 |
| _, _ -> |

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

1368 |
else OR (ft1, ft2) |

1369 |
end |

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

1371 |
let ft1 = simplify f1 in |

1372 |
let ft2 = simplify f2 in |

1373 |
begin |

1374 |
match ft1, ft2 with |

1375 |
| TRUE, _ -> ft2 |

1376 |
| FALSE, _ -> FALSE |

1377 |
| _, TRUE -> ft1 |

1378 |
| _, FALSE -> FALSE |

1379 |
| _, _ -> |

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

1381 |
else AND (ft1, ft2) |

1382 |
end |

1383 |
| NOT _ |

1384 |
| EQU _ |

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

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

1387 |
let ft = simplify f1 in |

1388 |
begin |

1389 |
match ft with |

1390 |
| FALSE -> FALSE |

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

1392 |
end |

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

1394 |
let ft = simplify f1 in |

1395 |
begin |

1396 |
match ft with |

1397 |
| TRUE -> TRUE |

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

1399 |
end |

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

1401 |
let ft = simplify f1 in |

1402 |
begin |

1403 |
match ft with |

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

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

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

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

1408 |
*) |

1409 |
| TRUE -> TRUE |

1410 |
| FALSE -> FALSE |

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

1412 |
end |

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

1414 |
let ft = simplify f1 in |

1415 |
begin |

1416 |
match ft with |

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

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

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

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

1421 |
*) |

1422 |
| TRUE -> TRUE |

1423 |
| FALSE -> FALSE |

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

1425 |
end |

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

1427 |
if n = 0 then TRUE |

1428 |
else |

1429 |
let ft = simplify f1 in |

1430 |
begin |

1431 |
match ft with |

1432 |
| FALSE -> FALSE |

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

1434 |
end |

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

1436 |
let ft = simplify f1 in |

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

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

1439 |
let ft = simplify f1 in |

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

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

1442 |
let ft = simplify f1 in |

1443 |
begin |

1444 |
match ft with |

1445 |
| FALSE -> TRUE |

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

1447 |
end |

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

1449 |
let ft1 = simplify f1 in |

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

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

1452 |
let ft1 = simplify f1 in |

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

1454 |
| CONST _ |

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

1456 |
| ID (f1) -> |

1457 |
let ft1 = simplify f1 in |

1458 |
begin |

1459 |
match ft1 with |

1460 |
| TRUE -> TRUE |

1461 |
| FALSE -> FALSE |

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

1463 |
end |

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

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

1466 |
let ft1 = simplify f1 in |

1467 |
let ft2 = simplify f2 in |

1468 |
begin |

1469 |
match ft2 with |

1470 |
| TRUE -> TRUE |

1471 |
| _ -> |

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

1473 |
else NORM (ft1, ft2) |

1474 |
end |

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

1476 |
let ft1 = simplify f1 in |

1477 |
let ft2 = simplify f2 in |

1478 |
begin |

1479 |
match ft2 with |

1480 |
| FALSE -> FALSE |

1481 |
| _ -> |

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

1483 |
else NORMN (ft1, ft2) |

1484 |
end |

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

1486 |
let ft1 = simplify f1 in |

1487 |
let ft2 = simplify f2 in |

1488 |
begin |

1489 |
match ft1, ft2 with |

1490 |
| TRUE, TRUE -> TRUE |

1491 |
| FALSE, FALSE -> FALSE |

1492 |
| _, _ -> |

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

1494 |
else CHC (ft1, ft2) |

1495 |
end |

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

1497 |
let ft = simplify f1 in |

1498 |
begin |

1499 |
match ft with |

1500 |
| FALSE -> FALSE |

1501 |
| TRUE -> TRUE |

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

1503 |
end |

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

1505 |
let ft = simplify f1 in |

1506 |
begin |

1507 |
match ft with |

1508 |
| TRUE -> TRUE |

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

1510 |
end |

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

1512 |
let ft = simplify f1 in |

1513 |
begin |

1514 |
match ft with |

1515 |
| TRUE -> TRUE |

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

1517 |
end |

1518 |
| AF _ | EF _ |

1519 |
| AG _ | EG _ |

1520 |
| AU _ | EU _ |

1521 |
| AR _ | ER _ |

1522 |
| AB _ | EB _ -> |

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

1524 | |

1525 |
let exportSortedAxiom = function |

1526 |
| (s, INCLUSION(f1, f2)) -> (string_of_int s) ^ ": " ^ (exportFormula f1) ^ " [= " ^ (exportFormula f2) |

1527 |
| (s, DEFINITION(f1, f2)) -> (string_of_int s) ^ ": " ^ (exportFormula f1) ^ " := " ^ (exportFormula f2) |

1528 | |

1529 | |

1530 |
(** Destructs a nominal. |

1531 |
@param s the input stream |

1532 |
@return (tbox, query) in simplifyed nnf |

1533 |
*) |

1534 |
let importAxiomQuery s = |

1535 |
let fkt ts = |

1536 |
let rec parse_sortedAxiomList ts acc = |

1537 |
let nr = |

1538 |
match Stream.peek ts with |

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

1540 |
if n >= 0 then begin |

1541 |
Stream.junk ts; |

1542 |
let () = |

1543 |
match Stream.next ts with |

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

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

1546 |
in |

1547 |
n |

1548 |
end else |

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

1550 |
| _ -> 0 |

1551 |
in |

1552 |
let f1 = simplify (nnf (parse_formula [] ts)) in |

1553 |
let f = match Stream.peek ts with |

1554 |
| Some (A.Kwd ":=") -> |

1555 |
Stream.junk ts; |

1556 |
(nr, DEFINITION(f1, simplify (nnf (parse_formula [] ts)))) |

1557 |
| Some (A.Kwd "[=") -> |

1558 |
Stream.junk ts; |

1559 |
(nr, INCLUSION(f1, simplify (nnf (parse_formula [] ts)))) |

1560 |
| _ -> raise (CoAlgException "Exception parse_sortedAxiomList") |

1561 |
in |

1562 |
match Stream.peek ts with |

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

1564 |
Stream.junk ts; |

1565 |
parse_sortedAxiomList ts (f::acc) |

1566 |
| _ -> List.rev (f :: acc) |

1567 |
in |

1568 |
match Stream.peek ts with |

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

1570 |
Stream.junk ts; |

1571 |
([], parse_sortedAxiomList ts []) |

1572 |
| _ -> |

1573 |
let fl = parse_sortedAxiomList ts [] in |

1574 |
if Stream.peek ts = Some (A.Kwd "|-") |

1575 |
then begin |

1576 |
Stream.junk ts; |

1577 |
(fl, parse_sortedAxiomList ts []) |

1578 |
end else ([], fl) |

1579 |
in |

1580 |
importWrapper fkt s |

1581 | |

1582 |
(** Destructs an atomic proposition. |

1583 |
@param f An atomic proposition. |

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

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

1586 |
*) |

1587 |
let dest_ap f = |

1588 |
match f with |

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

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

1591 | |

1592 |
(** Destructs a nominal. |

1593 |
@param f A nominal. |

1594 |
@return The name of the nominal |

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

1596 |
*) |

1597 |
let dest_nom f = |

1598 |
match f with |

1599 |
| AP s when isNominal s -> s |

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

1601 | |

1602 |
(** Destructs a negation. |

1603 |
@param f A negation. |

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

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

1606 |
*) |

1607 |
let dest_not f = |

1608 |
match f with |

1609 |
| NOT f1 -> f1 |

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

1611 | |

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

1613 |
@param f An @-formula. |

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

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

1616 |
*) |

1617 |
let dest_at f = |

1618 |
match f with |

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

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

1621 | |

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

1623 |
@param f An or-formula. |

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

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

1626 |
*) |

1627 |
let dest_or f = |

1628 |
match f with |

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

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

1631 | |

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

1633 |
@param f An and-formula. |

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

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

1636 |
*) |

1637 |
let dest_and f = |

1638 |
match f with |

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

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

1641 | |

1642 |
(** Destructs an equivalence. |

1643 |
@param f An equivalence. |

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

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

1646 |
*) |

1647 |
let dest_equ f = |

1648 |
match f with |

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

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

1651 | |

1652 |
(** Destructs an implication. |

1653 |
@param f An implication. |

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

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

1656 |
*) |

1657 |
let dest_imp f = |

1658 |
match f with |

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

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

1661 | |

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

1663 |
@param f An EX-formula. |

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

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

1666 |
*) |

1667 |
let dest_ex f = |

1668 |
match f with |

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

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

1671 | |

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

1673 |
@param f An AX-formula. |

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

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

1676 |
*) |

1677 |
let dest_ax f = |

1678 |
match f with |

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

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

1681 | |

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

1683 |
@param f A MIN-formula. |

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

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

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

1687 |
*) |

1688 |
let dest_min f = |

1689 |
match f with |

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

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

1692 | |

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

1694 |
@param f A MAX-formula. |

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

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

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

1698 |
*) |

1699 |
let dest_max f = |

1700 |
match f with |

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

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

1703 | |

1704 |
(** Destructs a choice formula. |

1705 |
@param f A choice formula. |

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

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

1708 |
*) |

1709 |
let dest_choice f = |

1710 |
match f with |

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

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

1713 | |

1714 |
(** Destructs a fusion formula. |

1715 |
@param f A fusion formula. |

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

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

1718 |
f1 is the immediate subformulae of f. |

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

1720 |
*) |

1721 |
let dest_fusion f = |

1722 |
match f with |

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

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

1725 | |

1726 | |

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

1728 |
@param f A formula. |

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

1730 |
*) |

1731 |
let is_true f = |

1732 |
match f with |

1733 |
| TRUE -> true |

1734 |
| _ -> false |

1735 | |

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

1737 |
@param f A formula. |

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

1739 |
*) |

1740 |
let is_false f = |

1741 |
match f with |

1742 |
| FALSE -> true |

1743 |
| _ -> false |

1744 | |

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

1746 |
@param f A formula. |

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

1748 |
*) |

1749 |
let is_ap f = |

1750 |
match f with |

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

1752 |
| _ -> false |

1753 | |

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

1755 |
@param f A formula. |

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

1757 |
*) |

1758 |
let is_nom f = |

1759 |
match f with |

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

1761 |
| _ -> false |

1762 | |

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

1764 |
@param f A formula. |

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

1766 |
*) |

1767 |
let is_not f = |

1768 |
match f with |

1769 |
| NOT _ -> true |

1770 |
| _ -> false |

1771 | |

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

1773 |
@param f A formula. |

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

1775 |
*) |

1776 |
let is_at f = |

1777 |
match f with |

1778 |
| AT _ -> true |

1779 |
| _ -> false |

1780 | |

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

1782 |
@param f A formula. |

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

1784 |
*) |

1785 |
let is_or f = |

1786 |
match f with |

1787 |
| OR _ -> true |

1788 |
| _ -> false |

1789 | |

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

1791 |
@param f A formula. |

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

1793 |
*) |

1794 |
let is_and f = |

1795 |
match f with |

1796 |
| AND _ -> true |

1797 |
| _ -> false |

1798 | |

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

1800 |
@param f A formula. |

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

1802 |
*) |

1803 |
let is_equ f = |

1804 |
match f with |

1805 |
| EQU _ -> true |

1806 |
| _ -> false |

1807 | |

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

1809 |
@param f A formula. |

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

1811 |
*) |

1812 |
let is_imp f = |

1813 |
match f with |

1814 |
| IMP _ -> true |

1815 |
| _ -> false |

1816 | |

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

1818 |
@param f A formula. |

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

1820 |
*) |

1821 |
let is_ex f = |

1822 |
match f with |

1823 |
| EX _ -> true |

1824 |
| _ -> false |

1825 | |

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

1827 |
@param f A formula. |

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

1829 |
*) |

1830 |
let is_ax f = |

1831 |
match f with |

1832 |
| AX _ -> true |

1833 |
| _ -> false |

1834 | |

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

1836 |
@param f A formula. |

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

1838 |
*) |

1839 |
let is_min f = |

1840 |
match f with |

1841 |
| MIN _ -> true |

1842 |
| _ -> false |

1843 | |

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

1845 |
@param f A formula. |

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

1847 |
*) |

1848 |
let is_max f = |

1849 |
match f with |

1850 |
| MAX _ -> true |

1851 |
| _ -> false |

1852 | |

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

1854 |
@param f A formula. |

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

1856 |
*) |

1857 |
let is_choice f = |

1858 |
match f with |

1859 |
| CHC _ -> true |

1860 |
| _ -> false |

1861 | |

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

1863 |
@param f A formula. |

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

1865 |
*) |

1866 |
let is_fusion f = |

1867 |
match f with |

1868 |
| FUS _ -> true |

1869 |
| _ -> false |

1870 | |

1871 | |

1872 |
(** The constant True. |

1873 |
*) |

1874 |
let const_true = TRUE |

1875 | |

1876 |
(** The constant False. |

1877 |
*) |

1878 |
let const_false = FALSE |

1879 | |

1880 |
(** Constructs an atomic proposition. |

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

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

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

1884 |
*) |

1885 |
let const_ap s = |

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

1887 |
else AP s |

1888 | |

1889 |
(** Constructs a nominal. |

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

1891 |
@return A nominal with name s. |

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

1893 |
*) |

1894 |
let const_nom s = |

1895 |
if isNominal s then AP s |

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

1897 | |

1898 |
(** Negates a formula. |

1899 |
@param f A formula. |

1900 |
@return The negation of f. |

1901 |
*) |

1902 |
let const_not f = NOT f |

1903 | |

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

1905 |
@param s A nominal name. |

1906 |
@param f A formula. |

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

1908 |
*) |

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

1910 | |

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

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

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

1914 |
@return The formula f1 | f2. |

1915 |
*) |

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

1917 | |

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

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

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

1921 |
@return The formula f1 & f2. |

1922 |
*) |

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

1924 | |

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

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

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

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

1929 |
*) |

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

1931 | |

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

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

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

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

1936 |
*) |

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

1938 | |

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

1940 |
@param s A role name. |

1941 |
@param f A formula. |

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

1943 |
*) |

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

1945 | |

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

1947 |
@param s A role name. |

1948 |
@param f A formula. |

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

1950 |
*) |

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

1952 | |

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

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

1955 |
@param s A role name. |

1956 |
@param f A formula. |

1957 |
@return The formula MIN f. |

1958 |
@raise CoAlgException Iff n is negative. |

1959 |
*) |

1960 |
let const_min n s f = |

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

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

1963 | |

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

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

1966 |
@param s A role name. |

1967 |
@param f A formula. |

1968 |
@return The formula MAX f. |

1969 |
@raise CoAlgException Iff n is negative. |

1970 |
*) |

1971 |
let const_max n s f = |

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

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

1974 | |

1975 |
let const_enforces p f = |

1976 |
ENFORCES (p,f) |

1977 | |

1978 |
let const_allows p f = |

1979 |
ALLOWS (p,f) |

1980 | |

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

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

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

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

1985 |
*) |

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

1987 | |

1988 |
(** Constructs a fusion formula. |

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

1990 |
@param f1 A formula. |

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

1992 |
*) |

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

1994 | |

1995 | |

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

1997 |
such that structural and physical equality coincide. |

1998 | |

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

2000 |
constructs |

2001 |
*) |

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

2003 |
and hcFormula_node = |

2004 |
| HCTRUE |

2005 |
| HCFALSE |

2006 |
| HCAP of string |

2007 |
| HCNOT of string |

2008 |
| HCAT of string * hcFormula |

2009 |
| HCOR of hcFormula * hcFormula |

2010 |
| HCAND of hcFormula * hcFormula |

2011 |
| HCEX of string * hcFormula |

2012 |
| HCAX of string * hcFormula |

2013 |
| HCENFORCES of int list * hcFormula |

2014 |
| HCALLOWS of int list * hcFormula |

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

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

2017 |
| HCATLEASTPROB of rational * hcFormula |

2018 |
| HCLESSPROBFAIL of rational * hcFormula |

2019 |
| HCCONST of string |

2020 |
| HCCONSTN of string |

2021 |
| HCID of hcFormula |

2022 |
| HCNORM of hcFormula * hcFormula |

2023 |
| HCNORMN of hcFormula * hcFormula |

2024 |
| HCCHC of hcFormula * hcFormula |

2025 |
| HCFUS of bool * hcFormula |

2026 |
| HCMU of string * hcFormula |

2027 |
| HCNU of string * hcFormula |

2028 |
| HCVAR of string |

2029 | |

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

2031 |
@param f1 The first formula node. |

2032 |
@param f2 The second formula node. |

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

2034 |
*) |

2035 |
let equal_hcFormula_node f1 f2 = |

2036 |
match f1, f2 with |

2037 |
| HCTRUE, HCTRUE -> true |

2038 |
| HCFALSE, HCFALSE -> true |

2039 |
| HCCONST s1, HCCONST s2 |

2040 |
| HCCONSTN s1, HCCONSTN s2 |

2041 |
| HCAP s1, HCAP s2 |

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

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

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

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

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

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

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

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

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

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

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

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

2054 |
p1 = p2 && f1 == f2 |

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

2056 |
p1 = p2 && f1 == f2 |

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

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

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

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

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

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

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

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

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

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

2067 |
| HCTRUE, _ |

2068 |
| HCFALSE, _ |

2069 |
| HCAP _, _ |

2070 |
| HCNOT _, _ |

2071 |
| HCAT _, _ |

2072 |
| HCOR _, _ |

2073 |
| HCAND _, _ |

2074 |
| HCEX _, _ |

2075 |
| HCAX _, _ |

2076 |
| HCENFORCES _, _ |

2077 |
| HCALLOWS _, _ |

2078 |
| HCMORETHAN _, _ |

2079 |
| HCMAXEXCEPT _, _ |

2080 |
| HCATLEASTPROB _, _ |

2081 |
| HCLESSPROBFAIL _, _ |

2082 |
| HCCONST _, _ |

2083 |
| HCCONSTN _, _ |

2084 |
| HCID _, _ |

2085 |
| HCNORM _, _ |

2086 |
| HCNORMN _, _ |

2087 |
| HCCHC _, _ |

2088 |
| HCFUS _, _ |

2089 |
| HCMU _, _ |

2090 |
| HCNU _, _ |

2091 |
| HCVAR _, _ -> false |

2092 | |

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

2094 |
@param f A formula node. |

2095 |
@return The hash value of f. |

2096 |
*) |

2097 |
let hash_hcFormula_node f = |

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

2099 |
match f with |

2100 |
| HCTRUE -> 0 |

2101 |
| HCFALSE -> 1 |

2102 |
| HCAP s |

2103 |
| HCNOT s |

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

2125 | |

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

2127 |
@param f A formula node. |

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

2129 |
*) |

2130 |
let toFml_hcFormula_node f = |

2131 |
match f with |

2132 |
| HCTRUE -> TRUE |

2133 |
| HCFALSE -> FALSE |

2134 |
| HCAP s -> AP s |

2135 |
| HCVAR s -> VAR s |

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

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

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

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

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

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

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

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

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

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

2146 |
| HCATLEASTPROB (p, f1) -> ATLEASTPROB (p, f1.HC.fml) |

2147 |
| HCLESSPROBFAIL (p, f1) -> LESSPROBFAIL (p, f1.HC.fml) |

2148 |
| HCCONST s -> CONST s |

2149 |
| HCCONSTN s -> CONSTN s |

2150 |
| HCID (f1) -> ID(f1.HC.fml) |

2151 |
| HCNORM (f1, f2) -> NORM(f1.HC.fml, f2.HC.fml) |

2152 |
| HCNORMN (f1, f2) -> NORMN(f1.HC.fml, f2.HC.fml) |

2153 |
| HCCHC (f1, f2) -> CHC (f1.HC.fml, f2.HC.fml) |

2154 |
| HCFUS (first, f1) -> FUS (first, f1.HC.fml) |

2155 |
| HCMU (var, f1) -> MU (var, f1.HC.fml) |

2156 |
| HCNU (var, f1) -> NU (var, f1.HC.fml) |

2157 | |

2158 |
(** Determines the negation (in negation normal form) of a formula node. |

2159 |
@param f A formula node. |

2160 |
@return The negation (in negation normal form) of f. |

2161 |
*) |

2162 |
let negNde_hcFormula_node f = |

2163 |
match f with |

2164 |
| HCTRUE -> HCFALSE |

2165 |
| HCFALSE -> HCTRUE |

2166 |
| HCAP s -> HCNOT s |

2167 |
| HCNOT s -> HCAP s |

2168 |
| HCVAR s -> f |

2169 |
| HCAT (s, f1) -> HCAT (s, f1.HC.neg) |

2170 |
| HCOR (f1, f2) -> HCAND (f1.HC.neg, f2.HC.neg) |

2171 |
| HCAND (f1, f2) -> HCOR (f1.HC.neg, f2.HC.neg) |

2172 |
| HCEX (s, f2) -> HCAX (s, f2.HC.neg) |

2173 |
| HCAX (s, f2) -> HCEX (s, f2.HC.neg) |

2174 |
| HCENFORCES (s, f2) -> HCALLOWS (s, f2.HC.neg) |

2175 |
| HCALLOWS (s, f2) -> HCENFORCES (s, f2.HC.neg) |

2176 |
| HCMORETHAN (n, s, f1) -> HCMAXEXCEPT (n, s, f1.HC.neg) |

2177 |
| HCMAXEXCEPT (n, s, f1) -> HCMORETHAN (n, s, f1.HC.neg) |

2178 |
| HCATLEASTPROB (p, f1) -> HCLESSPROBFAIL (p, f1.HC.neg) |

2179 |
| HCLESSPROBFAIL (p, f1) -> HCATLEASTPROB (p, f1.HC.neg) |

2180 |
| HCCONST s -> HCCONSTN s |

2181 |
| HCCONSTN s -> HCCONST s |

2182 |
| HCID (f1) -> HCID(f1.HC.neg) |

2183 |
| HCNORM (f1, f2) -> HCNORMN(f1.HC.neg, f2.HC.neg) |

2184 |
| HCNORMN (f1, f2) -> HCNORM(f1.HC.neg, f2.HC.neg) |

2185 |
| HCCHC (f1, f2) -> HCCHC (f1.HC.neg, f2.HC.neg) |

2186 |
| HCFUS (first, f1) -> HCFUS (first, f1.HC.neg) |

2187 |
| HCMU (name, f1) -> HCNU (name, f1.HC.neg) |

2188 |
| HCNU (name, f1) -> HCMU (name, f1.HC.neg) |

2189 | |

2190 |
(** An instantiation of hash-consing for formulae. |

2191 |
*) |

2192 |
module HcFormula = HC.Make( |

2193 |
struct |

2194 |
type nde = hcFormula_node |

2195 |
type fml = formula |

2196 |
let equal (n1 : nde) n2 = equal_hcFormula_node n1 n2 |

2197 |
let hash (n : nde) = hash_hcFormula_node n |

2198 |
let negNde (n : nde) = negNde_hcFormula_node n |

2199 |
let toFml (n : nde) = toFml_hcFormula_node n |

2200 |
end |

2201 |
) |

2202 | |

2203 |
(** Converts a formula into its hash-consed version. |

2204 |
@param hcF A hash-cons table for formulae. |

2205 |
@param f A formula in negation normal form. |

2206 |
@return The hash-consed version of f. |

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

2208 |
*) |

2209 |
let rec hc_formula hcF f = |

2210 |
match f with |

2211 |
| TRUE -> HcFormula.hashcons hcF HCTRUE |

2212 |
| FALSE -> HcFormula.hashcons hcF HCFALSE |

2213 |
| AP s -> HcFormula.hashcons hcF (HCAP s) |

2214 |
| VAR s -> HcFormula.hashcons hcF (HCVAR s) |

2215 |
| NOT (AP s) -> HcFormula.hashcons hcF (HCNOT s) |

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

2217 |
let tf1 = hc_formula hcF f1 in |

2218 |
HcFormula.hashcons hcF (HCAT (s, tf1)) |

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

2220 |
let tf1 = hc_formula hcF f1 in |

2221 |
let tf2 = hc_formula hcF f2 in |

2222 |
HcFormula.hashcons hcF (HCOR (tf1, tf2)) |

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

2224 |
let tf1 = hc_formula hcF f1 in |

2225 |
let tf2 = hc_formula hcF f2 in |

2226 |
HcFormula.hashcons hcF (HCAND (tf1, tf2)) |

2227 |
| NOT _ |

2228 |
| EQU _ |

2229 |
| MIN _ |

2230 |
| MAX _ |

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

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

2233 |
let tf1 = hc_formula hcF f1 in |

2234 |
HcFormula.hashcons hcF (HCEX (s, tf1)) |

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

2236 |
let tf1 = hc_formula hcF f1 in |

2237 |
HcFormula.hashcons hcF (HCAX (s, tf1)) |

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

2239 |
let tf1 = hc_formula hcF f1 in |

2240 |
HcFormula.hashcons hcF (HCENFORCES (s, tf1)) |

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

2242 |
let tf1 = hc_formula hcF f1 in |

2243 |
HcFormula.hashcons hcF (HCALLOWS (s, tf1)) |

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

2245 |
let tf1 = hc_formula hcF f1 in |

2246 |
HcFormula.hashcons hcF (HCMORETHAN (n, s, tf1)) |

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

2248 |
let tf1 = hc_formula hcF f1 in |

2249 |
HcFormula.hashcons hcF (HCMAXEXCEPT (n, s, tf1)) |

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

2251 |
HcFormula.hashcons hcF (HCATLEASTPROB (p, hc_formula hcF f1)) |

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

2253 |
HcFormula.hashcons hcF (HCLESSPROBFAIL (p, hc_formula hcF f1)) |

2254 |
| CONST s -> |

2255 |
HcFormula.hashcons hcF (HCCONST s) |

2256 |
| CONSTN s -> |

2257 |
HcFormula.hashcons hcF (HCCONSTN s) |

2258 |
| ID f1 -> |

2259 |
let tf1 = hc_formula hcF f1 in |

2260 |
HcFormula.hashcons hcF (HCID tf1) |

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

2262 |
let tf1 = hc_formula hcF f1 in |

2263 |
let tf2 = hc_formula hcF f2 in |

2264 |
HcFormula.hashcons hcF (HCNORM (tf1, tf2)) |

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

2266 |
let tf1 = hc_formula hcF f1 in |

2267 |
let tf2 = hc_formula hcF f2 in |

2268 |
HcFormula.hashcons hcF (HCNORMN (tf1, tf2)) |

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

2270 |
let tf1 = hc_formula hcF f1 in |

2271 |
let tf2 = hc_formula hcF f2 in |

2272 |
HcFormula.hashcons hcF (HCCHC (tf1, tf2)) |

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

2274 |
let tf1 = hc_formula hcF f1 in |

2275 |
HcFormula.hashcons hcF (HCFUS (first, tf1)) |

2276 |
| MU (var, f1) -> |

2277 |
let tf1 = hc_formula hcF f1 in |

2278 |
HcFormula.hashcons hcF (HCMU (var, tf1)) |

2279 |
| NU (var, f1) -> |

2280 |
let tf1 = hc_formula hcF f1 in |

2281 |
HcFormula.hashcons hcF (HCNU (var, tf1)) |

2282 |
| AF _ | EF _ |

2283 |
| AG _ | EG _ |

2284 |
| AU _ | EU _ |

2285 |
| AR _ | ER _ |

2286 |
| AB _ | EB _ -> |

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

2288 | |

2289 |
(* Replace the Variable name in f with formula formula |

2290 |
hc_replace foo φ ψ => ψ[foo |-> φ] |

2291 |
*) |

2292 |
let rec hc_replace hcF name (formula: hcFormula) (f: hcFormula) = |

2293 |
let func = hc_replace hcF name formula in |

2294 |
let gennew = HcFormula.hashcons hcF in |

2295 |
match f.HC.node with |

2296 |
| HCTRUE |

2297 |
| HCFALSE |

2298 |
| HCAP _ |

2299 |
| HCNOT _ |

2300 |
| HCCONST _ |

2301 |
| HCCONSTN _ -> f |

2302 |
| HCVAR s -> |

2303 |
if compare s name == 0 |

2304 |
then formula |

2305 |
else f |

2306 |
| HCAT (s, f1) -> |

2307 |
let nf1 = func f1 in |

2308 |
if nf1 == f1 then f else gennew (HCAT(s, nf1)) |

2309 |
| HCOR (f1, f2) -> |

2310 |
let nf1 = func f1 in |

2311 |
let nf2 = func f2 in |

2312 |
if nf1 == f1 && nf2 == f2 then f else gennew (HCOR(nf1, nf2)) |

2313 |
| HCAND (f1, f2) -> |

2314 |
let nf1 = func f1 in |

2315 |
let nf2 = func f2 in |

2316 |
if nf1 == f1 && nf2 == f2 then f else gennew (HCAND(nf1, nf2)) |

2317 |
| HCEX (s, f1) -> |

2318 |
let nf1 = func f1 in |

2319 |
if nf1 == f1 then f else gennew (HCEX(s, nf1)) |

2320 |
| HCAX (s, f1) -> |

2321 |
let nf1 = func f1 in |

2322 |
if nf1 == f1 then f else gennew (HCAX(s, nf1)) |

2323 |
| HCENFORCES (s, f1) -> |

2324 |
let nf1 = func f1 in |

2325 |
if nf1 == f1 then f else gennew (HCENFORCES(s, nf1)) |

2326 |
| HCALLOWS (s, f1) -> |

2327 |
let nf1 = func f1 in |

2328 |
if nf1 == f1 then f else gennew (HCALLOWS(s, nf1)) |

2329 |
| HCMORETHAN (n, s, f1) -> |

2330 |
let nf1 = func f1 in |

2331 |
if nf1 == f1 then f else gennew (HCMORETHAN(n, s, nf1)) |

2332 |
| HCMAXEXCEPT (n, s, f1) -> |

2333 |
let nf1 = func f1 in |

2334 |
if nf1 == f1 then f else gennew (HCMAXEXCEPT(n, s, nf1)) |

2335 |
| HCATLEASTPROB (p, f1) -> |

2336 |
let nf1 = func f1 in |

2337 |
if nf1 == f1 then f else gennew (HCATLEASTPROB(p, nf1)) |

2338 |
| HCLESSPROBFAIL (p, f1) -> |

2339 |
let nf1 = func f1 in |

2340 |
if nf1 == f1 then f else gennew (HCLESSPROBFAIL(p, nf1)) |

2341 |
| HCID f1 -> |

2342 |
let nf1 = func f1 in |

2343 |
if nf1 == f1 then f else gennew (HCID(nf1)) |

2344 |
| HCNORM (f1, f2) -> |

2345 |
let nf1 = func f1 in |

2346 |
let nf2 = func f2 in |

2347 |
if nf1 == f1 && nf2 == f2 then f else gennew (HCNORM(nf1, nf2)) |

2348 |
| HCNORMN (f1, f2) -> |

2349 |
let nf1 = func f1 in |

2350 |
let nf2 = func f2 in |

2351 |
if nf1 == f1 && nf2 == f2 then f else gennew (HCNORMN(nf1, nf2)) |

2352 |
| HCCHC (f1, f2) -> |

2353 |
let nf1 = func f1 in |

2354 |
let nf2 = func f2 in |

2355 |
if nf1 == f1 && nf2 == f2 then f else gennew (HCCHC(nf1, nf2)) |

2356 |
| HCFUS (first, f1) -> |

2357 |
let nf1 = func f1 in |

2358 |
if nf1 == f1 then f else gennew (HCFUS(first, nf1)) |

2359 |
| HCMU (var, f1) -> |

2360 |
if compare var name != 0 then |

2361 |
let nf1 = func f1 in |

2362 |
if nf1 == f1 then f else gennew (HCMU(var, nf1)) |

2363 |
else |

2364 |
f |

2365 |
| HCNU (var, f1) -> |

2366 |
if compare var name != 0 then |

2367 |
let nf1 = func f1 in |

2368 |
if nf1 == f1 then f else gennew (HCNU(var, nf1)) |

2369 |
else |

2370 |
f |

2371 | |

2372 |
let rec hc_freeIn variable (f: hcFormula) = |

2373 |
match f.HC.node with |

2374 |
| HCTRUE |

2375 |
| HCFALSE |

2376 |
| HCAP _ |

2377 |
| HCNOT _ |

2378 |
| HCCONST _ |

2379 |
| HCCONSTN _ -> false |

2380 |
| HCVAR s -> |

2381 |
if compare variable s == 0 |

2382 |
then true |

2383 |
else false |

2384 |
| HCAT (s, f1) -> |

2385 |
hc_freeIn variable f1 |

2386 |
| HCOR (f1, f2) |

2387 |
| HCAND (f1, f2) -> |

2388 |
hc_freeIn variable f1 || hc_freeIn variable f2 |

2389 |
| HCEX (_, f1) |

2390 |
| HCAX (_, f1) |

2391 |
| HCENFORCES (_, f1) |

2392 |
| HCALLOWS (_, f1) |

2393 |
| HCMORETHAN (_, _, f1) |

2394 |
| HCMAXEXCEPT (_, _, f1) |

2395 |
| HCATLEASTPROB (_, f1) |

2396 |
| HCLESSPROBFAIL (_, f1) |

2397 |
| HCID f1 -> |

2398 |
hc_freeIn variable f1 |

2399 |
| HCNORM (f1, f2) |

2400 |
| HCNORMN (f1, f2) |

2401 |
| HCCHC (f1, f2) -> |

2402 |
hc_freeIn variable f1 || hc_freeIn variable f2 |

2403 |
| HCFUS (first, f1) -> |

2404 |
hc_freeIn variable f1 |

2405 |
| HCMU (var, f1) |

2406 |
| HCNU (var, f1) -> |

2407 |
(* Do we need to exclude bound variables here? *) |

2408 |
hc_freeIn variable f1 |

2409 | |

2410 | |

2411 |
(** An instantiation of a hash table (of the standard library) |

2412 |
for hash-consed formulae. The test for equality |

2413 |
and computing the hash value is done in constant time. |

2414 |
*) |

2415 |
module HcFHt = Hashtbl.Make( |

2416 |
struct |

2417 |
type t = hcFormula |

2418 |
let equal (f1 : t) f2 = f1.HC.tag = f2.HC.tag |

2419 |
let hash (f : t) = f.HC.tag |

2420 |
end |

2421 |
) |