## cool / src / lib / CoAlgFormula.ml @ 2a36974b

History | View | Annotate | Download (69.2 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 |
exception ConversionException of formula |

76 | |

77 | |

78 |
(** Defines sorted coalgebraic formulae. |

79 |
*) |

80 |
type sortedFormula = sort * formula |

81 | |

82 | |

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

84 |
@param A string s. |

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

86 |
*) |

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

88 | |

89 | |

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

91 |
@param f A formula. |

92 |
@return The size of f. |

93 |
*) |

94 |
let rec sizeFormula f = |

95 |
match f with |

96 |
| TRUE |

97 |
| FALSE |

98 |
| AP _ -> 1 |

99 |
| NOT f1 |

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

101 |
| OR (f1, f2) |

102 |
| AND (f1, f2) |

103 |
| EQU (f1, f2) |

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

105 |
| EX (_, f1) |

106 |
| AX (_, f1) |

107 |
| ENFORCES (_, f1) |

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

109 |
| MIN (_, _, f1) |

110 |
| MAX (_, _, f1) |

111 |
| ATLEASTPROB (_, f1) |

112 |
| LESSPROBFAIL (_, f1) |

113 |
| MORETHAN (_, _, f1) |

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

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

116 |
| NORM(f1, f2) |

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

118 |
| CONST _ |

119 |
| CONSTN _ -> 1 |

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

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

122 |
| MU (_, f1) |

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

124 |
| VAR _ -> 1 |

125 |
| AF _ | EF _ |

126 |
| AG _ | EG _ |

127 |
| AU _ | EU _ |

128 |
| AR _ | ER _ |

129 |
| AB _ | EB _ -> |

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

131 | |

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

133 |
@param f A sorted formula. |

134 |
@return The size of f. |

135 |
*) |

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

137 | |

138 | |

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

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

141 |
let rec iter func formula = |

142 |
func formula; |

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

144 |
match formula with |

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

146 |
| CONST _ |

147 |
| CONSTN _ -> () |

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

165 | |

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

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

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

169 |
let formula = (match formula with |

170 |
(* 0-ary constructors *) |

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

172 |
| CONST _ |

173 |
| CONSTN _ -> formula |

174 |
(* unary *) |

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

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

177 |
(* binary *) |

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

209 |
in |

210 |
func formula |

211 | |

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

213 |
let helper formula = match formula with |

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

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

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

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

218 |
| TRUE | FALSE |

219 |
| EQU _ | IMP _ |

220 |
| AND _ | OR _ |

221 |
| AP _ | NOT _ |

222 |
| AX _ | EX _ |

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

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

225 |
in |

226 |
convert_post helper formula |

227 | |

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

229 |
let helper formula = match formula with |

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

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

232 |
| TRUE | FALSE |

233 |
| EQU _ | IMP _ |

234 |
| AND _ | OR _ |

235 |
| AP _ | NOT _ |

236 |
| CHC _ | FUS _ -> formula |

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

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

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

240 |
in |

241 |
convert_post helper formula |

242 | |

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

244 | |

245 |
let convertToMu formula = |

246 |
let name = Stream.next gensym in |

247 |
let helper formula = |

248 |
match formula with |

249 |
| AF f1 -> |

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

251 |
| EF f1 -> |

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

253 |
| AG f1 -> |

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

255 |
| EG f1 -> |

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

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

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

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

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

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

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

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

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

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

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

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

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

269 |
| _ -> formula |

270 |
in |

271 |
convert_post helper formula |

272 | |

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

274 |
Parentheses are ommited where possible |

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

276 |
@param sb A string buffer. |

277 |
@param f A formula. |

278 |
*) |

279 |
let rec exportFormula_buffer sb f = |

280 |
let negate = function |

281 |
| NOT f -> f |

282 |
| f -> NOT f |

283 |
in |

284 |
let prio n lf = |

285 |
let prionr = function |

286 |
| EQU _ -> 0 |

287 |
| IMP _ -> 1 |

288 |
| OR _ -> 2 |

289 |
| AND _ -> 3 |

290 |
| _ -> 4 |

291 |
in |

292 |
if prionr lf < n then begin |

293 |
Buffer.add_char sb '('; |

294 |
exportFormula_buffer sb lf; |

295 |
Buffer.add_char sb ')' |

296 |
end |

297 |
else exportFormula_buffer sb lf |

298 |
in |

299 |
match f with |

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

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

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

303 |
| NOT f1 -> |

304 |
Buffer.add_string sb "~"; |

305 |
prio 4 f1 |

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

307 |
Buffer.add_string sb "@ "; |

308 |
Buffer.add_string sb s; |

309 |
Buffer.add_string sb " "; |

310 |
prio 4 f1 |

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

312 |
prio 2 f1; |

313 |
Buffer.add_string sb " | "; |

314 |
prio 2 f2 |

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

316 |
prio 3 f1; |

317 |
Buffer.add_string sb " & "; |

318 |
prio 3 f2 |

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

320 |
prio 0 f1; |

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

322 |
prio 0 f2 |

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

324 |
prio 2 f1; |

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

326 |
prio 2 f2 |

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

328 |
Buffer.add_string sb "<"; |

329 |
Buffer.add_string sb s; |

330 |
Buffer.add_string sb ">"; |

331 |
prio 4 f1 |

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

333 |
Buffer.add_string sb "["; |

334 |
Buffer.add_string sb s; |

335 |
Buffer.add_string sb "]"; |

336 |
prio 4 f1 |

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

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

339 |
Buffer.add_string sb ( |

340 |
match s with |

341 |
| [] -> " " |

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

343 |
); |

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

345 |
prio 4 f1 |

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

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

348 |
Buffer.add_string sb ( |

349 |
match s with |

350 |
| [] -> " " |

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

352 |
); |

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

354 |
prio 4 f1 |

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

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

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

358 |
Buffer.add_string sb "}"; |

359 |
prio 4 f1 |

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

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

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

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

364 |
prio 4 f1 |

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

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

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

368 |
Buffer.add_string sb " "; |

369 |
Buffer.add_string sb s; |

370 |
Buffer.add_string sb "}"; |

371 |
prio 4 f1 |

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

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

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

375 |
Buffer.add_string sb " "; |

376 |
Buffer.add_string sb s; |

377 |
Buffer.add_string sb "}"; |

378 |
prio 4 f1 |

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

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

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

382 |
Buffer.add_string sb " "; |

383 |
Buffer.add_string sb s; |

384 |
Buffer.add_string sb "}"; |

385 |
prio 4 f1 |

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

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

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

389 |
Buffer.add_string sb " ~ "; |

390 |
Buffer.add_string sb s; |

391 |
Buffer.add_string sb "}"; |

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

393 |
| ID (f1) -> |

394 |
Buffer.add_string sb "O"; |

395 |
prio 4 f1 |

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

397 |
Buffer.add_string sb "("; |

398 |
exportFormula_buffer sb f1; |

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

400 |
exportFormula_buffer sb f2; |

401 |
Buffer.add_string sb ")" |

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

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

404 |
exportFormula_buffer sb (negate f1); |

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

406 |
exportFormula_buffer sb (negate f2); |

407 |
Buffer.add_string sb ")" |

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

409 |
Buffer.add_string sb "("; |

410 |
exportFormula_buffer sb f1; |

411 |
Buffer.add_string sb " + "; |

412 |
exportFormula_buffer sb f2; |

413 |
Buffer.add_string sb ")" |

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

415 |
Buffer.add_string sb s |

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

417 |
Buffer.add_string sb s |

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

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

420 |
prio 4 f1 |

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

422 |
Buffer.add_string sb "μ"; |

423 |
Buffer.add_string sb s; |

424 |
Buffer.add_string sb "."; |

425 |
prio 4 f1 |

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

427 |
Buffer.add_string sb "ν"; |

428 |
Buffer.add_string sb s; |

429 |
Buffer.add_string sb "."; |

430 |
prio 4 f1 |

431 |
| VAR s -> |

432 |
Buffer.add_string sb s |

433 |
| AF f1 -> |

434 |
Buffer.add_string sb "AF "; |

435 |
prio 4 f1 |

436 |
| EF f1 -> |

437 |
Buffer.add_string sb "EF "; |

438 |
prio 4 f1 |

439 |
| AG f1 -> |

440 |
Buffer.add_string sb "AG "; |

441 |
prio 4 f1 |

442 |
| EG f1 -> |

443 |
Buffer.add_string sb "EG "; |

444 |
prio 4 f1 |

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

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

447 |
prio 4 f1; |

448 |
Buffer.add_string sb " U "; |

449 |
prio 4 f2; |

450 |
Buffer.add_string sb ")" |

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

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

453 |
prio 4 f1; |

454 |
Buffer.add_string sb " U "; |

455 |
prio 4 f2; |

456 |
Buffer.add_string sb ")" |

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

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

459 |
prio 4 f1; |

460 |
Buffer.add_string sb " R "; |

461 |
prio 4 f2; |

462 |
Buffer.add_string sb ")" |

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

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

465 |
prio 4 f1; |

466 |
Buffer.add_string sb " R "; |

467 |
prio 4 f2; |

468 |
Buffer.add_string sb ")" |

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

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

471 |
prio 4 f1; |

472 |
Buffer.add_string sb " B "; |

473 |
prio 4 f2; |

474 |
Buffer.add_string sb ")" |

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

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

477 |
prio 4 f1; |

478 |
Buffer.add_string sb " B "; |

479 |
prio 4 f2; |

480 |
Buffer.add_string sb ")" |

481 | |

482 | |

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

484 |
Parentheses are ommited where possible |

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

486 |
@param f A formula. |

487 |
@return A string representing f. |

488 |
*) |

489 |
let exportFormula f = |

490 |
let sb = Buffer.create 128 in |

491 |
exportFormula_buffer sb f; |

492 |
Buffer.contents sb |

493 | |

494 |
let string_of_formula = exportFormula |

495 | |

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

497 |
let rec exportTatlFormula_buffer sb f = |

498 |
let prio n lf = |

499 |
let prionr = function |

500 |
| EQU _ -> 0 |

501 |
| IMP _ -> 1 |

502 |
| OR _ -> 2 |

503 |
| AND _ -> 3 |

504 |
| _ -> 4 |

505 |
in |

506 |
if prionr lf < n then begin |

507 |
Buffer.add_char sb '('; |

508 |
exportTatlFormula_buffer sb lf; |

509 |
Buffer.add_char sb ')' |

510 |
end |

511 |
else exportTatlFormula_buffer sb lf |

512 |
in |

513 |
match f with |

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

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

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

517 |
| NOT f1 -> |

518 |
Buffer.add_string sb "~"; |

519 |
prio 4 f1 |

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

521 |
prio 2 f1; |

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

523 |
prio 2 f2 |

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

525 |
prio 3 f1; |

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

527 |
prio 3 f2 |

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

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

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

531 |
prio 2 f1; |

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

533 |
prio 2 f2 |

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

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

536 |
Buffer.add_string sb ( |

537 |
match s with |

538 |
| [] -> " " |

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

540 |
); |

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

542 |
prio 4 f1 |

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

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

545 |
Buffer.add_string sb ( |

546 |
match s with |

547 |
| [] -> " " |

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

549 |
); |

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

551 |
prio 4 f1 |

552 |
| EX _ |

553 |
| AX _ |

554 |
| MIN _ |

555 |
| MAX _ |

556 |
| MORETHAN _ |

557 |
| MAXEXCEPT _ |

558 |
| AT _ |

559 |
| CONST _ |

560 |
| CONSTN _ |

561 |
| CHC _ |

562 |
| ATLEASTPROB _ |

563 |
| LESSPROBFAIL _ |

564 |
| ID _ |

565 |
| NORM _ |

566 |
| NORMN _ |

567 |
| FUS _ |

568 |
| MU _ |

569 |
| NU _ |

570 |
| VAR _ |

571 |
| AF _ |

572 |
| EF _ |

573 |
| AG _ |

574 |
| EG _ |

575 |
| AU _ |

576 |
| EU _ |

577 |
| AR _ |

578 |
| ER _ |

579 |
| AB _ |

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

581 | |

582 |
let exportTatlFormula f = |

583 |
let sb = Buffer.create 128 in |

584 |
exportTatlFormula_buffer sb f; |

585 |
Buffer.contents sb |

586 | |

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

588 |
Parentheses are ommited where possible |

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

590 |
@param sb A string buffer. |

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

592 |
*) |

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

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

595 |
Buffer.add_string sb ": "; |

596 |
exportFormula_buffer sb f |

597 | |

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

599 |
Parentheses are ommited where possible |

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

601 |
@param f A sorted formula. |

602 |
@return A string representing f. |

603 |
*) |

604 |
let exportSortedFormula f = |

605 |
let sb = Buffer.create 128 in |

606 |
exportSortedFormula_buffer sb f; |

607 |
Buffer.contents sb |

608 | |

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

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

611 |
@param f A sorted formula. |

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

613 |
*) |

614 |
let exportQuery tbox f = |

615 |
let sb = Buffer.create 1000 in |

616 |
let rec expFl = function |

617 |
| [] -> () |

618 |
| h::tl -> |

619 |
exportSortedFormula_buffer sb h; |

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

621 |
expFl tl |

622 |
in |

623 |
expFl tbox; |

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

625 |
exportSortedFormula_buffer sb f; |

626 |
Buffer.contents sb |

627 | |

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

629 |
coalg can read it again using importQuery |

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

631 |
@param f A sorted formula. |

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

633 |
*) |

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

635 |
let sb = Buffer.create 1000 in |

636 |
let rec expFl = function |

637 |
| [] -> () |

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

639 |
exportFormula_buffer sb h; |

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

641 |
expFl tl |

642 |
in |

643 |
expFl tbox; |

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

645 |
exportFormula_buffer sb f; |

646 |
Buffer.contents sb |

647 | |

648 | |

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

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

651 |
*) |

652 |
let lexer = A.make_lexer |

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

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

655 |
;"μ";"ν";"." |

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

657 |
] |

658 | |

659 |
let mk_exn s = CoAlgException s |

660 | |

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

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

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

664 |
*) |

665 |
let rec verifyMuAltFree formula = |

666 |
let proc = verifyMuAltFree in |

667 |
match formula with |

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

669 |
| CONST _ |

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

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

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

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

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

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

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

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

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

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

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

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

682 |
else |

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

698 |
else |

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

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

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

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

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

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

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

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

707 |
if newfree = [] then |

708 |
("none", []) |

709 |
else |

710 |
("μ", newfree) |

711 |
| NU (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 |
| VAR s -> ("none", [s]) |

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

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

724 | |

725 | |

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

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

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

729 |
negations is even. |

730 |
*) |

731 |
let rec verifyMuMonotone negations formula = |

732 |
let proc = verifyMuMonotone negations in |

733 |
match formula with |

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

735 |
| CONST _ |

736 |
| CONSTN _ -> () |

737 |
| AT (_,a) |

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

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

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

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

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

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

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

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

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

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

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

749 |
| MU (s, f) |

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

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

752 |
verifyMuMonotone newNeg f |

753 |
| VAR s -> |

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

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

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

757 |
| NOT a -> |

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

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

760 |
verifyMuMonotone newNeg a |

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

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

763 | |

764 |
let rec verifyMuGuarded unguarded formula = |

765 |
let proc = verifyMuGuarded unguarded in |

766 |
match formula with |

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

768 |
| CONST _ |

769 |
| CONSTN _ -> () |

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

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

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

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

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

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

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

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

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

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

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

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

782 |
| MU (s, f) |

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

784 |
let newUnguard = s :: unguarded in |

785 |
verifyMuGuarded newUnguard f |

786 |
| VAR s -> |

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

788 |
if List.exists finder unguarded then |

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

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

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

792 | |

793 |
let verifyFormula formula = |

794 |
verifyMuAltFree formula; |

795 |
verifyMuMonotone [] formula; |

796 |
verifyMuGuarded [] formula |

797 | |

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

799 |
It is a standard recursive descent procedure. |

800 |
@param ts A token stream. |

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

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

803 |
*) |

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

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

806 |
let f1 = convertToMu formula in |

807 |
match Stream.peek ts with |

808 |
| None -> f1 |

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

810 |
Stream.junk ts; |

811 |
let f2 = parse_formula symtab ts in |

812 |
EQU (f1, f2) |

813 |
| _ -> f1 |

814 | |

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

816 |
It is a standard recursive descent procedure. |

817 |
@param ts A token stream. |

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

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

820 |
*) |

821 |
and parse_imp symtab ts= |

822 |
let f1 = parse_or symtab ts in |

823 |
match Stream.peek ts with |

824 |
| None -> f1 |

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

826 |
Stream.junk ts; |

827 |
let f2 = parse_imp symtab ts in |

828 |
IMP (f1, f2) |

829 |
| _ -> f1 |

830 | |

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

832 |
It is a standard recursive descent procedure. |

833 |
@param ts A token stream. |

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

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

836 |
*) |

837 |
and parse_or symtab ts = |

838 |
let f1 = parse_and symtab ts in |

839 |
match Stream.peek ts with |

840 |
| None -> f1 |

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

842 |
Stream.junk ts; |

843 |
let f2 = parse_or symtab ts in |

844 |
OR (f1, f2) |

845 |
| _ -> f1 |

846 | |

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

848 |
It is a standard recursive descent procedure. |

849 |
@param ts A token stream. |

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

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

852 |
*) |

853 |
and parse_and symtab ts = |

854 |
let f1 = parse_cimp symtab ts in |

855 |
match Stream.peek ts with |

856 |
| None -> f1 |

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

858 |
Stream.junk ts; |

859 |
let f2 = parse_and symtab ts in |

860 |
AND (f1, f2) |

861 |
| _ -> f1 |

862 | |

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

864 |
It is a standard recursive descent procedure. |

865 |
@param ts A token stream. |

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

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

868 |
*) |

869 |
and parse_cimp symtab ts = |

870 |
let f1 = parse_rest symtab ts in |

871 |
match Stream.peek ts with |

872 |
| None -> f1 |

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

874 |
Stream.junk ts; |

875 |
let f2 = parse_cimp symtab ts in |

876 |
NORM (f1, f2) |

877 |
| _ -> f1 |

878 | |

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

880 |
It is a standard recursive descent procedure. |

881 |
@param ts A token stream. |

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

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

884 |
*) |

885 |
and parse_rest symtab ts = |

886 |
let boxinternals noNo es = |

887 |
let n = |

888 |
if noNo then 0 |

889 |
else |

890 |
match Stream.next ts with |

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

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

893 |
in |

894 |
let (s,denominator) = |

895 |
match Stream.peek ts with |

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

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

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

899 |
Stream.junk ts; |

900 |
match Stream.next ts with |

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

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

903 |
end |

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

905 |
in |

906 |
if (denominator < n) then begin |

907 |
let explanation = |

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

909 |
in |

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

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

912 |
) |

913 |
end; |

914 |
let _ = |

915 |
match Stream.next ts with |

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

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

918 |
in |

919 |
(n, denominator, s) |

920 |
in |

921 |
let rec agentlist es = |

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

923 |
match Stream.next ts with |

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

925 |
then n::(agentlist es) |

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

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

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

929 |
in |

930 |
match Stream.next ts with |

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

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

933 |
AP "true" |

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

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

936 |
AP "false" |

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

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

939 |
| A.Ident s -> |

940 |
(try |

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

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

943 |
VAR symbol |

944 |
with Not_found -> AP s) |

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

946 |
let f = parse_rest symtab ts in |

947 |
NOT f |

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

949 |
let s = |

950 |
match Stream.next ts with |

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

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

953 |
in |

954 |
let f = parse_rest symtab ts in |

955 |
AT (s, f) |

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

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

958 |
let f1 = parse_rest symtab ts in |

959 |
EX (s, f1) |

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

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

962 |
let f1 = parse_rest symtab ts in |

963 |
AX (s, f1) |

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

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

966 |
let f1 = parse_rest symtab ts in |

967 |
ENFORCES (ls, f1) |

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

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

970 |
let f1 = parse_rest symtab ts in |

971 |
ALLOWS (ls, f1) |

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

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

974 |
let f1 = parse_rest symtab ts in |

975 |
if (denom <> 0) |

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

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

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

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

980 |
let f1 = parse_rest symtab ts in |

981 |
if (denom <> 0) |

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

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

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

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

986 |
let f1 = parse_rest symtab ts in |

987 |
if (denom <> 0) |

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

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

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

991 |
match Stream.next ts with |

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

993 |
| A.Kwd s |

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

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

996 |
end |

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

998 |
let f = parse_formula symtab ts in |

999 |
match Stream.next ts with |

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

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

1002 |
let f2 = parse_formula symtab ts in |

1003 |
match Stream.next ts with |

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

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

1006 |
end |

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

1008 |
end |

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

1010 |
let f = parse_rest symtab ts in |

1011 |
ID f |

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

1013 |
let f = parse_rest symtab ts in |

1014 |
FUS (true, f) |

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

1016 |
let f = parse_rest symtab ts in |

1017 |
FUS (false, f) |

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

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

1020 |
let symbol = Stream.next gensym in |

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

1022 |
let f1 = parse_rest newtab ts in |

1023 |
MU (symbol, f1) |

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

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

1026 |
let symbol = Stream.next gensym in |

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

1028 |
let f1 = parse_rest newtab ts in |

1029 |
NU (symbol, f1) |

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

1031 |
let f = parse_rest symtab ts in |

1032 |
AF f |

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

1034 |
let f = parse_rest symtab ts in |

1035 |
EF f |

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

1037 |
let f = parse_rest symtab ts in |

1038 |
AG f |

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

1040 |
let f = parse_rest symtab ts in |

1041 |
EG f |

1042 |
| A.Kwd "A" -> |

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

1044 |
let f1 = parse_formula symtab ts in begin |

1045 |
match Stream.next ts with |

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

1047 |
let f2 = parse_formula symtab ts in |

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

1049 |
AU (f1, f2) |

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

1051 |
let f2 = parse_formula symtab ts in |

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

1053 |
AR (f1, f2) |

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

1055 |
let f2 = parse_formula symtab ts in |

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

1057 |
AB (f1, f2) |

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

1059 |
end |

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

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

1062 |
let f1 = parse_formula symtab ts in begin |

1063 |
match Stream.next ts with |

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

1065 |
let f2 = parse_formula symtab ts in |

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

1067 |
EU (f1, f2) |

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

1069 |
let f2 = parse_formula symtab ts in |

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

1071 |
ER (f1, f2) |

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

1073 |
let f2 = parse_formula symtab ts in |

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

1075 |
EB (f1, f2) |

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

1077 |
end |

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

1079 |
let f1 = parse_rest symtab ts in |

1080 |
AX ("", f1) |

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

1082 |
let f1 = parse_rest symtab ts in |

1083 |
EX ("", f1) |

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

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

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

1087 | |

1088 |
(** Parses a sorted formula. |

1089 |
@param ts A token stream. |

1090 |
@return A sorted formula. |

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

1092 |
*) |

1093 |
let parse_sortedFormula ts = |

1094 |
let nr = |

1095 |
match Stream.peek ts with |

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

1097 |
if n >= 0 then begin |

1098 |
Stream.junk ts; |

1099 |
let () = |

1100 |
match Stream.next ts with |

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

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

1103 |
in |

1104 |
n |

1105 |
end else |

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

1107 |
| _ -> 0 |

1108 |
in |

1109 |
let f = parse_formula [] ts in |

1110 |
(nr, f) |

1111 | |

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

1113 |
@param ts A token stream. |

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

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

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

1117 |
*) |

1118 |
let rec parse_sortedFormulaList ts acc = |

1119 |
let f1 = parse_sortedFormula ts in |

1120 |
match Stream.peek ts with |

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

1122 |
Stream.junk ts; |

1123 |
parse_sortedFormulaList ts (f1::acc) |

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

1125 | |

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

1127 |
@param fkt An import function. |

1128 |
@param s A string. |

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

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

1131 |
*) |

1132 |
let importWrapper fkt s = |

1133 |
let ts = lexer s in |

1134 |
try |

1135 |
let res = fkt ts in |

1136 |
let _ = |

1137 |
match Stream.peek ts with |

1138 |
| None -> () |

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

1140 |
in |

1141 |
res |

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

1143 | |

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

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

1146 |
@return The resulting formula. |

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

1148 |
*) |

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

1150 | |

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

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

1153 |
@return The sorted formula. |

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

1155 |
*) |

1156 |
let importSortedFormula s = importWrapper parse_sortedFormula s |

1157 | |

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

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

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

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

1162 |
f is a sorted formula. |

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

1164 |
*) |

1165 |
let importQuery s = |

1166 |
let fkt ts = |

1167 |
match Stream.peek ts with |

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

1169 |
Stream.junk ts; |

1170 |
let f = parse_sortedFormula ts in |

1171 |
([], f) |

1172 |
| _ -> |

1173 |
let fl = parse_sortedFormulaList ts [] in |

1174 |
match Stream.peek ts with |

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

1176 |
Stream.junk ts; |

1177 |
let f = parse_sortedFormula ts in |

1178 |
(fl, f) |

1179 |
| _ -> |

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

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

1182 |
in |

1183 |
importWrapper fkt s |

1184 | |

1185 | |

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

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

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

1189 |
@param f A formula. |

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

1191 |
that is equivalent to ~f. |

1192 |
*) |

1193 |
let rec nnfNeg f = |

1194 |
match f with |

1195 |
| TRUE -> FALSE |

1196 |
| FALSE -> TRUE |

1197 |
| AP _ -> NOT f |

1198 |
| VAR _ -> f |

1199 |
| NOT f1 -> nnf f1 |

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

1215 |
| CONST s -> CONSTN s |

1216 |
| CONSTN s -> CONST s |

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

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

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

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

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

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

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

1224 |
| AF _ | EF _ |

1225 |
| AG _ | EG _ |

1226 |
| AU _ | EU _ |

1227 |
| AR _ | ER _ |

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

1229 | |

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

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

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

1233 |
@param f A formula. |

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

1235 |
that is equivalent to f. |

1236 |
*) |

1237 |
and nnf f = |

1238 |
match f with |

1239 |
| TRUE |

1240 |
| FALSE |

1241 |
| AP _ |

1242 |
| NOT (AP _) |

1243 |
| CONST _ |

1244 |
| CONSTN _ |

1245 |
| VAR _ -> f |

1246 |
| NOT f1 -> nnfNeg f1 |

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

1248 |
let ft1 = nnf f1 in |

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

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

1251 |
let ft1 = nnf f1 in |

1252 |
let ft2 = nnf f2 in |

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

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

1255 |
let ft1 = nnf f1 in |

1256 |
let ft2 = nnf f2 in |

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

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

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

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

1261 |
let ft = nnf f1 in |

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

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

1264 |
let ft = nnf f1 in |

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

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

1267 |
let ft = nnf f1 in |

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

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

1270 |
let ft = nnf f1 in |

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

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

1273 |
if n = 0 then TRUE |

1274 |
else |

1275 |
let ft = nnf f1 in |

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

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

1278 |
let ft = nnfNeg f1 in |

1279 |
MAXEXCEPT (n,s, ft) |

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

1281 |
let ft = nnf f1 in |

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

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

1284 |
let ft = nnf f1 in |

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

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

1287 |
let ft = nnf f1 in |

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

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

1290 |
let ft = nnf f1 in |

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

1292 |
| ID (f1) -> |

1293 |
let ft = nnf f1 in |

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

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

1296 |
let ft1 = nnf f1 in |

1297 |
let ft2 = nnf f2 in |

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

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

1300 |
let ft1 = nnf f1 in |

1301 |
let ft2 = nnf f2 in |

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

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

1304 |
let ft1 = nnf f1 in |

1305 |
let ft2 = nnf f2 in |

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

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

1308 |
let ft = nnf f1 in |

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

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

1311 |
let ft = nnf f1 in |

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

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

1314 |
let ft = nnf f1 in |

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

1316 |
| AF _ | EF _ |

1317 |
| AG _ | EG _ |

1318 |
| AU _ | EU _ |

1319 |
| AR _ | ER _ |

1320 |
| AB _ | EB _ -> |

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

1322 | |

1323 |
(** Simplifies a formula. |

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

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

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

1327 |
*) |

1328 |
let rec simplify f = |

1329 |
match f with |

1330 |
| TRUE |

1331 |
| FALSE |

1332 |
| AP _ |

1333 |
| NOT (AP _) |

1334 |
| VAR _ |

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

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

1337 |
let ft = simplify f1 in |

1338 |
begin |

1339 |
match ft with |

1340 |
| FALSE -> FALSE |

1341 |
| TRUE -> TRUE |

1342 |
| AT _ -> ft |

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

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

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

1346 |
end |

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

1348 |
let ft1 = simplify f1 in |

1349 |
let ft2 = simplify f2 in |

1350 |
begin |

1351 |
match ft1, ft2 with |

1352 |
| TRUE, _ -> TRUE |

1353 |
| FALSE, _ -> ft2 |

1354 |
| _, TRUE -> TRUE |

1355 |
| _, FALSE -> ft1 |

1356 |
| _, _ -> |

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

1358 |
else OR (ft1, ft2) |

1359 |
end |

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

1361 |
let ft1 = simplify f1 in |

1362 |
let ft2 = simplify f2 in |

1363 |
begin |

1364 |
match ft1, ft2 with |

1365 |
| TRUE, _ -> ft2 |

1366 |
| FALSE, _ -> FALSE |

1367 |
| _, TRUE -> ft1 |

1368 |
| _, FALSE -> FALSE |

1369 |
| _, _ -> |

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

1371 |
else AND (ft1, ft2) |

1372 |
end |

1373 |
| NOT _ |

1374 |
| EQU _ |

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

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

1377 |
let ft = simplify f1 in |

1378 |
begin |

1379 |
match ft with |

1380 |
| FALSE -> FALSE |

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

1382 |
end |

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

1384 |
let ft = simplify f1 in |

1385 |
begin |

1386 |
match ft with |

1387 |
| TRUE -> TRUE |

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

1389 |
end |

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

1391 |
let ft = simplify f1 in |

1392 |
begin |

1393 |
match ft with |

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

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

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

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

1398 |
*) |

1399 |
| TRUE -> TRUE |

1400 |
| FALSE -> FALSE |

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

1402 |
end |

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

1404 |
let ft = simplify f1 in |

1405 |
begin |

1406 |
match ft with |

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

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

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

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

1411 |
*) |

1412 |
| TRUE -> TRUE |

1413 |
| FALSE -> FALSE |

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

1415 |
end |

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

1417 |
if n = 0 then TRUE |

1418 |
else |

1419 |
let ft = simplify f1 in |

1420 |
begin |

1421 |
match ft with |

1422 |
| FALSE -> FALSE |

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

1424 |
end |

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

1426 |
let ft = simplify f1 in |

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

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

1429 |
let ft = simplify f1 in |

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

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

1432 |
let ft = simplify f1 in |

1433 |
begin |

1434 |
match ft with |

1435 |
| FALSE -> TRUE |

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

1437 |
end |

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

1439 |
let ft1 = simplify f1 in |

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

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

1442 |
let ft1 = simplify f1 in |

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

1444 |
| CONST _ |

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

1446 |
| ID (f1) -> |

1447 |
let ft1 = simplify f1 in |

1448 |
begin |

1449 |
match ft1 with |

1450 |
| TRUE -> TRUE |

1451 |
| FALSE -> FALSE |

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

1453 |
end |

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

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

1456 |
let ft1 = simplify f1 in |

1457 |
let ft2 = simplify f2 in |

1458 |
begin |

1459 |
match ft2 with |

1460 |
| TRUE -> TRUE |

1461 |
| _ -> |

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

1463 |
else NORM (ft1, ft2) |

1464 |
end |

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

1466 |
let ft1 = simplify f1 in |

1467 |
let ft2 = simplify f2 in |

1468 |
begin |

1469 |
match ft2 with |

1470 |
| FALSE -> FALSE |

1471 |
| _ -> |

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

1473 |
else NORMN (ft1, ft2) |

1474 |
end |

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

1476 |
let ft1 = simplify f1 in |

1477 |
let ft2 = simplify f2 in |

1478 |
begin |

1479 |
match ft1, ft2 with |

1480 |
| TRUE, TRUE -> TRUE |

1481 |
| FALSE, FALSE -> FALSE |

1482 |
| _, _ -> |

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

1484 |
else CHC (ft1, ft2) |

1485 |
end |

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

1487 |
let ft = simplify f1 in |

1488 |
begin |

1489 |
match ft with |

1490 |
| FALSE -> FALSE |

1491 |
| TRUE -> TRUE |

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

1493 |
end |

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

1495 |
let ft = simplify f1 in |

1496 |
begin |

1497 |
match ft with |

1498 |
| TRUE -> TRUE |

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

1500 |
end |

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

1502 |
let ft = simplify f1 in |

1503 |
begin |

1504 |
match ft with |

1505 |
| TRUE -> TRUE |

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

1507 |
end |

1508 |
| AF _ | EF _ |

1509 |
| AG _ | EG _ |

1510 |
| AU _ | EU _ |

1511 |
| AR _ | ER _ |

1512 |
| AB _ | EB _ -> |

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

1514 | |

1515 |
(** Destructs an atomic proposition. |

1516 |
@param f An atomic proposition. |

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

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

1519 |
*) |

1520 |
let dest_ap f = |

1521 |
match f with |

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

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

1524 | |

1525 |
(** Destructs a nominal. |

1526 |
@param f A nominal. |

1527 |
@return The name of the nominal |

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

1529 |
*) |

1530 |
let dest_nom f = |

1531 |
match f with |

1532 |
| AP s when isNominal s -> s |

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

1534 | |

1535 |
(** Destructs a negation. |

1536 |
@param f A negation. |

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

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

1539 |
*) |

1540 |
let dest_not f = |

1541 |
match f with |

1542 |
| NOT f1 -> f1 |

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

1544 | |

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

1546 |
@param f An @-formula. |

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

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

1549 |
*) |

1550 |
let dest_at f = |

1551 |
match f with |

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

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

1554 | |

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

1556 |
@param f An or-formula. |

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

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

1559 |
*) |

1560 |
let dest_or f = |

1561 |
match f with |

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

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

1564 | |

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

1566 |
@param f An and-formula. |

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

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

1569 |
*) |

1570 |
let dest_and f = |

1571 |
match f with |

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

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

1574 | |

1575 |
(** Destructs an equivalence. |

1576 |
@param f An equivalence. |

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

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

1579 |
*) |

1580 |
let dest_equ f = |

1581 |
match f with |

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

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

1584 | |

1585 |
(** Destructs an implication. |

1586 |
@param f An implication. |

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

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

1589 |
*) |

1590 |
let dest_imp f = |

1591 |
match f with |

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

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

1594 | |

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

1596 |
@param f An EX-formula. |

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

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

1599 |
*) |

1600 |
let dest_ex f = |

1601 |
match f with |

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

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

1604 | |

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

1606 |
@param f An AX-formula. |

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

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

1609 |
*) |

1610 |
let dest_ax f = |

1611 |
match f with |

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

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

1614 | |

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

1616 |
@param f A MIN-formula. |

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

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

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

1620 |
*) |

1621 |
let dest_min f = |

1622 |
match f with |

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

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

1625 | |

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

1627 |
@param f A MAX-formula. |

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

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

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

1631 |
*) |

1632 |
let dest_max f = |

1633 |
match f with |

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

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

1636 | |

1637 |
(** Destructs a choice formula. |

1638 |
@param f A choice formula. |

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

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

1641 |
*) |

1642 |
let dest_choice f = |

1643 |
match f with |

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

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

1646 | |

1647 |
(** Destructs a fusion formula. |

1648 |
@param f A fusion formula. |

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

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

1651 |
f1 is the immediate subformulae of f. |

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

1653 |
*) |

1654 |
let dest_fusion f = |

1655 |
match f with |

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

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

1658 | |

1659 | |

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

1661 |
@param f A formula. |

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

1663 |
*) |

1664 |
let is_true f = |

1665 |
match f with |

1666 |
| TRUE -> true |

1667 |
| _ -> false |

1668 | |

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

1670 |
@param f A formula. |

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

1672 |
*) |

1673 |
let is_false f = |

1674 |
match f with |

1675 |
| FALSE -> true |

1676 |
| _ -> false |

1677 | |

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

1679 |
@param f A formula. |

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

1681 |
*) |

1682 |
let is_ap f = |

1683 |
match f with |

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

1685 |
| _ -> false |

1686 | |

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

1688 |
@param f A formula. |

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

1690 |
*) |

1691 |
let is_nom f = |

1692 |
match f with |

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

1694 |
| _ -> false |

1695 | |

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

1697 |
@param f A formula. |

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

1699 |
*) |

1700 |
let is_not f = |

1701 |
match f with |

1702 |
| NOT _ -> true |

1703 |
| _ -> false |

1704 | |

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

1706 |
@param f A formula. |

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

1708 |
*) |

1709 |
let is_at f = |

1710 |
match f with |

1711 |
| AT _ -> true |

1712 |
| _ -> false |

1713 | |

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

1715 |
@param f A formula. |

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

1717 |
*) |

1718 |
let is_or f = |

1719 |
match f with |

1720 |
| OR _ -> true |

1721 |
| _ -> false |

1722 | |

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

1724 |
@param f A formula. |

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

1726 |
*) |

1727 |
let is_and f = |

1728 |
match f with |

1729 |
| AND _ -> true |

1730 |
| _ -> false |

1731 | |

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

1733 |
@param f A formula. |

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

1735 |
*) |

1736 |
let is_equ f = |

1737 |
match f with |

1738 |
| EQU _ -> true |

1739 |
| _ -> false |

1740 | |

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

1742 |
@param f A formula. |

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

1744 |
*) |

1745 |
let is_imp f = |

1746 |
match f with |

1747 |
| IMP _ -> true |

1748 |
| _ -> false |

1749 | |

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

1751 |
@param f A formula. |

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

1753 |
*) |

1754 |
let is_ex f = |

1755 |
match f with |

1756 |
| EX _ -> true |

1757 |
| _ -> false |

1758 | |

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

1760 |
@param f A formula. |

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

1762 |
*) |

1763 |
let is_ax f = |

1764 |
match f with |

1765 |
| AX _ -> true |

1766 |
| _ -> false |

1767 | |

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

1769 |
@param f A formula. |

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

1771 |
*) |

1772 |
let is_min f = |

1773 |
match f with |

1774 |
| MIN _ -> true |

1775 |
| _ -> false |

1776 | |

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

1778 |
@param f A formula. |

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

1780 |
*) |

1781 |
let is_max f = |

1782 |
match f with |

1783 |
| MAX _ -> true |

1784 |
| _ -> false |

1785 | |

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

1787 |
@param f A formula. |

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

1789 |
*) |

1790 |
let is_choice f = |

1791 |
match f with |

1792 |
| CHC _ -> true |

1793 |
| _ -> false |

1794 | |

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

1796 |
@param f A formula. |

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

1798 |
*) |

1799 |
let is_fusion f = |

1800 |
match f with |

1801 |
| FUS _ -> true |

1802 |
| _ -> false |

1803 | |

1804 | |

1805 |
(** The constant True. |

1806 |
*) |

1807 |
let const_true = TRUE |

1808 | |

1809 |
(** The constant False. |

1810 |
*) |

1811 |
let const_false = FALSE |

1812 | |

1813 |
(** Constructs an atomic proposition. |

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

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

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

1817 |
*) |

1818 |
let const_ap s = |

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

1820 |
else AP s |

1821 | |

1822 |
(** Constructs a nominal. |

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

1824 |
@return A nominal with name s. |

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

1826 |
*) |

1827 |
let const_nom s = |

1828 |
if isNominal s then AP s |

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

1830 | |

1831 |
(** Negates a formula. |

1832 |
@param f A formula. |

1833 |
@return The negation of f. |

1834 |
*) |

1835 |
let const_not f = NOT f |

1836 | |

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

1838 |
@param s A nominal name. |

1839 |
@param f A formula. |

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

1841 |
*) |

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

1843 | |

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

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

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

1847 |
@return The formula f1 | f2. |

1848 |
*) |

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

1850 | |

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

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

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

1854 |
@return The formula f1 & f2. |

1855 |
*) |

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

1857 | |

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

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

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

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

1862 |
*) |

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

1864 | |

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

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

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

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

1869 |
*) |

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

1871 | |

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

1873 |
@param s A role name. |

1874 |
@param f A formula. |

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

1876 |
*) |

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

1878 | |

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

1880 |
@param s A role name. |

1881 |
@param f A formula. |

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

1883 |
*) |

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

1885 | |

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

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

1888 |
@param s A role name. |

1889 |
@param f A formula. |

1890 |
@return The formula MIN f. |

1891 |
@raise CoAlgException Iff n is negative. |

1892 |
*) |

1893 |
let const_min n s f = |

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

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

1896 | |

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

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

1899 |
@param s A role name. |

1900 |
@param f A formula. |

1901 |
@return The formula MAX f. |

1902 |
@raise CoAlgException Iff n is negative. |

1903 |
*) |

1904 |
let const_max n s f = |

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

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

1907 | |

1908 |
let const_enforces p f = |

1909 |
ENFORCES (p,f) |

1910 | |

1911 |
let const_allows p f = |

1912 |
ALLOWS (p,f) |

1913 | |

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

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

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

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

1918 |
*) |

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

1920 | |

1921 |
(** Constructs a fusion formula. |

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

1923 |
@param f1 A formula. |

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

1925 |
*) |

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

1927 | |

1928 | |

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

1930 |
such that structural and physical equality coincide. |

1931 | |

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

1933 |
constructs |

1934 |
*) |

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

1936 |
and hcFormula_node = |

1937 |
| HCTRUE |

1938 |
| HCFALSE |

1939 |
| HCAP of string |

1940 |
| HCNOT of string |

1941 |
| HCAT of string * hcFormula |

1942 |
| HCOR of hcFormula * hcFormula |

1943 |
| HCAND of hcFormula * hcFormula |

1944 |
| HCEX of string * hcFormula |

1945 |
| HCAX of string * hcFormula |

1946 |
| HCENFORCES of int list * hcFormula |

1947 |
| HCALLOWS of int list * hcFormula |

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

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

1950 |
| HCATLEASTPROB of rational * hcFormula |

1951 |
| HCLESSPROBFAIL of rational * hcFormula |

1952 |
| HCCONST of string |

1953 |
| HCCONSTN of string |

1954 |
| HCID of hcFormula |

1955 |
| HCNORM of hcFormula * hcFormula |

1956 |
| HCNORMN of hcFormula * hcFormula |

1957 |
| HCCHC of hcFormula * hcFormula |

1958 |
| HCFUS of bool * hcFormula |

1959 |
| HCMU of string * hcFormula |

1960 |
| HCNU of string * hcFormula |

1961 |
| HCVAR of string |

1962 | |

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

1964 |
@param f1 The first formula node. |

1965 |
@param f2 The second formula node. |

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

1967 |
*) |

1968 |
let equal_hcFormula_node f1 f2 = |

1969 |
match f1, f2 with |

1970 |
| HCTRUE, HCTRUE -> true |

1971 |
| HCFALSE, HCFALSE -> true |

1972 |
| HCCONST s1, HCCONST s2 |

1973 |
| HCCONSTN s1, HCCONSTN s2 |

1974 |
| HCAP s1, HCAP s2 |

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

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

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

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

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

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

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

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

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

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

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

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

1987 |
p1 = p2 && f1 == f2 |

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

1989 |
p1 = p2 && f1 == f2 |

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

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

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

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

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

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

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

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

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

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

2000 |
| HCTRUE, _ |

2001 |
| HCFALSE, _ |

2002 |
| HCAP _, _ |

2003 |
| HCNOT _, _ |

2004 |
| HCAT _, _ |

2005 |
| HCOR _, _ |

2006 |
| HCAND _, _ |

2007 |
| HCEX _, _ |

2008 |
| HCAX _, _ |

2009 |
| HCENFORCES _, _ |

2010 |
| HCALLOWS _, _ |

2011 |
| HCMORETHAN _, _ |

2012 |
| HCMAXEXCEPT _, _ |

2013 |
| HCATLEASTPROB _, _ |

2014 |
| HCLESSPROBFAIL _, _ |

2015 |
| HCCONST _, _ |

2016 |
| HCCONSTN _, _ |

2017 |
| HCID _, _ |

2018 |
| HCNORM _, _ |

2019 |
| HCNORMN _, _ |

2020 |
| HCCHC _, _ |

2021 |
| HCFUS _, _ |

2022 |
| HCMU _, _ |

2023 |
| HCNU _, _ |

2024 |
| HCVAR _, _ -> false |

2025 | |

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

2027 |
@param f A formula node. |

2028 |
@return The hash value of f. |

2029 |
*) |

2030 |
let hash_hcFormula_node f = |

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

2032 |
match f with |

2033 |
| HCTRUE -> 0 |

2034 |
| HCFALSE -> 1 |

2035 |
| HCAP s |

2036 |
| HCNOT s |

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

2058 | |

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

2060 |
@param f A formula node. |

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

2062 |
*) |

2063 |
let toFml_hcFormula_node f = |

2064 |
match f with |

2065 |
| HCTRUE -> TRUE |

2066 |
| HCFALSE -> FALSE |

2067 |
| HCAP s -> AP s |

2068 |
| HCVAR s -> VAR s |

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

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

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

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

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

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

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

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

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

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

2079 |
| HCATLEASTPROB (p, f1) -> ATLEASTPROB (p, f1.HC.fml) |

2080 |
| HCLESSPROBFAIL (p, f1) -> LESSPROBFAIL (p, f1.HC.fml) |

2081 |
| HCCONST s -> CONST s |

2082 |
| HCCONSTN s -> CONSTN s |

2083 |
| HCID (f1) -> ID(f1.HC.fml) |

2084 |
| HCNORM (f1, f2) -> NORM(f1.HC.fml, f2.HC.fml) |

2085 |
| HCNORMN (f1, f2) -> NORMN(f1.HC.fml, f2.HC.fml) |

2086 |
| HCCHC (f1, f2) -> CHC (f1.HC.fml, f2.HC.fml) |

2087 |
| HCFUS (first, f1) -> FUS (first, f1.HC.fml) |

2088 |
| HCMU (var, f1) -> MU (var, f1.HC.fml) |

2089 |
| HCNU (var, f1) -> NU (var, f1.HC.fml) |

2090 | |

2091 |
(** Determines the negation (in negation normal form) of a formula node. |

2092 |
@param f A formula node. |

2093 |
@return The negation (in negation normal form) of f. |

2094 |
*) |

2095 |
let negNde_hcFormula_node f = |

2096 |
match f with |

2097 |
| HCTRUE -> HCFALSE |

2098 |
| HCFALSE -> HCTRUE |

2099 |
| HCAP s -> HCNOT s |

2100 |
| HCNOT s -> HCAP s |

2101 |
| HCVAR s -> f |

2102 |
| HCAT (s, f1) -> HCAT (s, f1.HC.neg) |

2103 |
| HCOR (f1, f2) -> HCAND (f1.HC.neg, f2.HC.neg) |

2104 |
| HCAND (f1, f2) -> HCOR (f1.HC.neg, f2.HC.neg) |

2105 |
| HCEX (s, f2) -> HCAX (s, f2.HC.neg) |

2106 |
| HCAX (s, f2) -> HCEX (s, f2.HC.neg) |

2107 |
| HCENFORCES (s, f2) -> HCALLOWS (s, f2.HC.neg) |

2108 |
| HCALLOWS (s, f2) -> HCENFORCES (s, f2.HC.neg) |

2109 |
| HCMORETHAN (n, s, f1) -> HCMAXEXCEPT (n, s, f1.HC.neg) |

2110 |
| HCMAXEXCEPT (n, s, f1) -> HCMORETHAN (n, s, f1.HC.neg) |

2111 |
| HCATLEASTPROB (p, f1) -> HCLESSPROBFAIL (p, f1.HC.neg) |

2112 |
| HCLESSPROBFAIL (p, f1) -> HCATLEASTPROB (p, f1.HC.neg) |

2113 |
| HCCONST s -> HCCONSTN s |

2114 |
| HCCONSTN s -> HCCONST s |

2115 |
| HCID (f1) -> HCID(f1.HC.neg) |

2116 |
| HCNORM (f1, f2) -> HCNORMN(f1.HC.neg, f2.HC.neg) |

2117 |
| HCNORMN (f1, f2) -> HCNORM(f1.HC.neg, f2.HC.neg) |

2118 |
| HCCHC (f1, f2) -> HCCHC (f1.HC.neg, f2.HC.neg) |

2119 |
| HCFUS (first, f1) -> HCFUS (first, f1.HC.neg) |

2120 |
| HCMU (name, f1) -> HCNU (name, f1.HC.neg) |

2121 |
| HCNU (name, f1) -> HCMU (name, f1.HC.neg) |

2122 | |

2123 |
(** An instantiation of hash-consing for formulae. |

2124 |
*) |

2125 |
module HcFormula = HC.Make( |

2126 |
struct |

2127 |
type nde = hcFormula_node |

2128 |
type fml = formula |

2129 |
let equal (n1 : nde) n2 = equal_hcFormula_node n1 n2 |

2130 |
let hash (n : nde) = hash_hcFormula_node n |

2131 |
let negNde (n : nde) = negNde_hcFormula_node n |

2132 |
let toFml (n : nde) = toFml_hcFormula_node n |

2133 |
end |

2134 |
) |

2135 | |

2136 |
(** Converts a formula into its hash-consed version. |

2137 |
@param hcF A hash-cons table for formulae. |

2138 |
@param f A formula in negation normal form. |

2139 |
@return The hash-consed version of f. |

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

2141 |
*) |

2142 |
let rec hc_formula hcF f = |

2143 |
match f with |

2144 |
| TRUE -> HcFormula.hashcons hcF HCTRUE |

2145 |
| FALSE -> HcFormula.hashcons hcF HCFALSE |

2146 |
| AP s -> HcFormula.hashcons hcF (HCAP s) |

2147 |
| VAR s -> HcFormula.hashcons hcF (HCVAR s) |

2148 |
| NOT (AP s) -> HcFormula.hashcons hcF (HCNOT s) |

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

2150 |
let tf1 = hc_formula hcF f1 in |

2151 |
HcFormula.hashcons hcF (HCAT (s, tf1)) |

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

2153 |
let tf1 = hc_formula hcF f1 in |

2154 |
let tf2 = hc_formula hcF f2 in |

2155 |
HcFormula.hashcons hcF (HCOR (tf1, tf2)) |

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

2157 |
let tf1 = hc_formula hcF f1 in |

2158 |
let tf2 = hc_formula hcF f2 in |

2159 |
HcFormula.hashcons hcF (HCAND (tf1, tf2)) |

2160 |
| NOT _ |

2161 |
| EQU _ |

2162 |
| MIN _ |

2163 |
| MAX _ |

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

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

2166 |
let tf1 = hc_formula hcF f1 in |

2167 |
HcFormula.hashcons hcF (HCEX (s, tf1)) |

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

2169 |
let tf1 = hc_formula hcF f1 in |

2170 |
HcFormula.hashcons hcF (HCAX (s, tf1)) |

2171 |
| ENFORCES (s, f1) -> |

2172 |
let tf1 = hc_formula hcF f1 in |

2173 |
HcFormula.hashcons hcF (HCENFORCES (s, tf1)) |

2174 |
| ALLOWS (s, f1) -> |

2175 |
let tf1 = hc_formula hcF f1 in |

2176 |
HcFormula.hashcons hcF (HCALLOWS (s, tf1)) |

2177 |
| MORETHAN (n, s, f1) -> |

2178 |
let tf1 = hc_formula hcF f1 in |

2179 |
HcFormula.hashcons hcF (HCMORETHAN (n, s, tf1)) |

2180 |
| MAXEXCEPT (n, s, f1) -> |

2181 |
let tf1 = hc_formula hcF f1 in |

2182 |
HcFormula.hashcons hcF (HCMAXEXCEPT (n, s, tf1)) |

2183 |
| ATLEASTPROB (p, f1) -> |

2184 |
HcFormula.hashcons hcF (HCATLEASTPROB (p, hc_formula hcF f1)) |

2185 |
| LESSPROBFAIL (p, f1) -> |

2186 |
HcFormula.hashcons hcF (HCLESSPROBFAIL (p, hc_formula hcF f1)) |

2187 |
| CONST s -> |

2188 |
HcFormula.hashcons hcF (HCCONST s) |

2189 |
| CONSTN s -> |

2190 |
HcFormula.hashcons hcF (HCCONSTN s) |

2191 |
| ID f1 -> |

2192 |
let tf1 = hc_formula hcF f1 in |

2193 |
HcFormula.hashcons hcF (HCID tf1) |

2194 |
| NORM (f1, f2) -> |

2195 |
let tf1 = hc_formula hcF f1 in |

2196 |
let tf2 = hc_formula hcF f2 in |

2197 |
HcFormula.hashcons hcF (HCNORM (tf1, tf2)) |

2198 |
| NORMN (f1, f2) -> |

2199 |
let tf1 = hc_formula hcF f1 in |

2200 |
let tf2 = hc_formula hcF f2 in |

2201 |
HcFormula.hashcons hcF (HCNORMN (tf1, tf2)) |

2202 |
| CHC (f1, f2) -> |

2203 |
let tf1 = hc_formula hcF f1 in |

2204 |
let tf2 = hc_formula hcF f2 in |

2205 |
HcFormula.hashcons hcF (HCCHC (tf1, tf2)) |

2206 |
| FUS (first, f1) -> |

2207 |
let tf1 = hc_formula hcF f1 in |

2208 |
HcFormula.hashcons hcF (HCFUS (first, tf1)) |

2209 |
| MU (var, f1) -> |

2210 |
let tf1 = hc_formula hcF f1 in |

2211 |
HcFormula.hashcons hcF (HCMU (var, tf1)) |

2212 |
| NU (var, f1) -> |

2213 |
let tf1 = hc_formula hcF f1 in |

2214 |
HcFormula.hashcons hcF (HCNU (var, tf1)) |

2215 |
| AF _ | EF _ |

2216 |
| AG _ | EG _ |

2217 |
| AU _ | EU _ |

2218 |
| AR _ | ER _ |

2219 |
| AB _ | EB _ -> |

2220 |
raise (CoAlgException ("nnf: CTL should have been removed at this point")) |

2221 | |

2222 |
(* Replace the Variable name in f with formula formula |

2223 |
hc_replace foo φ ψ => ψ[foo |-> φ] |

2224 |
*) |

2225 |
let rec hc_replace hcF name (formula: hcFormula) (f: hcFormula) = |

2226 |
let func = hc_replace hcF name formula in |

2227 |
let gennew = HcFormula.hashcons hcF in |

2228 |
match f.HC.node with |

2229 |
| HCTRUE |

2230 |
| HCFALSE |

2231 |
| HCAP _ |

2232 |
| HCNOT _ |

2233 |
| HCCONST _ |

2234 |
| HCCONSTN _ -> f |

2235 |
| HCVAR s -> |

2236 |
if compare s name == 0 |

2237 |
then formula |

2238 |
else f |

2239 |
| HCAT (s, f1) -> |

2240 |
let nf1 = func f1 in |

2241 |
if nf1 == f1 then f else gennew (HCAT(s, nf1)) |

2242 |
| HCOR (f1, f2) -> |

2243 |
let nf1 = func f1 in |

2244 |
let nf2 = func f2 in |

2245 |
if nf1 == f1 && nf2 == f2 then f else gennew (HCOR(nf1, nf2)) |

2246 |
| HCAND (f1, f2) -> |

2247 |
let nf1 = func f1 in |

2248 |
let nf2 = func f2 in |

2249 |
if nf1 == f1 && nf2 == f2 then f else gennew (HCAND(nf1, nf2)) |

2250 |
| HCEX (s, f1) -> |

2251 |
let nf1 = func f1 in |

2252 |
if nf1 == f1 then f else gennew (HCEX(s, nf1)) |

2253 |
| HCAX (s, f1) -> |

2254 |
let nf1 = func f1 in |

2255 |
if nf1 == f1 then f else gennew (HCAX(s, nf1)) |

2256 |
| HCENFORCES (s, f1) -> |

2257 |
let nf1 = func f1 in |

2258 |
if nf1 == f1 then f else gennew (HCENFORCES(s, nf1)) |

2259 |
| HCALLOWS (s, f1) -> |

2260 |
let nf1 = func f1 in |

2261 |
if nf1 == f1 then f else gennew (HCALLOWS(s, nf1)) |

2262 |
| HCMORETHAN (n, s, f1) -> |

2263 |
let nf1 = func f1 in |

2264 |
if nf1 == f1 then f else gennew (HCMORETHAN(n, s, nf1)) |

2265 |
| HCMAXEXCEPT (n, s, f1) -> |

2266 |
let nf1 = func f1 in |

2267 |
if nf1 == f1 then f else gennew (HCMAXEXCEPT(n, s, nf1)) |

2268 |
| HCATLEASTPROB (p, f1) -> |

2269 |
let nf1 = func f1 in |

2270 |
if nf1 == f1 then f else gennew (HCATLEASTPROB(p, nf1)) |

2271 |
| HCLESSPROBFAIL (p, f1) -> |

2272 |
let nf1 = func f1 in |

2273 |
if nf1 == f1 then f else gennew (HCLESSPROBFAIL(p, nf1)) |

2274 |
| HCID f1 -> |

2275 |
let nf1 = func f1 in |

2276 |
if nf1 == f1 then f else gennew (HCID(nf1)) |

2277 |
| HCNORM (f1, f2) -> |

2278 |
let nf1 = func f1 in |

2279 |
let nf2 = func f2 in |

2280 |
if nf1 == f1 && nf2 == f2 then f else gennew (HCNORM(nf1, nf2)) |

2281 |
| HCNORMN (f1, f2) -> |

2282 |
let nf1 = func f1 in |

2283 |
let nf2 = func f2 in |

2284 |
if nf1 == f1 && nf2 == f2 then f else gennew (HCNORMN(nf1, nf2)) |

2285 |
| HCCHC (f1, f2) -> |

2286 |
let nf1 = func f1 in |

2287 |
let nf2 = func f2 in |

2288 |
if nf1 == f1 && nf2 == f2 then f else gennew (HCCHC(nf1, nf2)) |

2289 |
| HCFUS (first, f1) -> |

2290 |
let nf1 = func f1 in |

2291 |
if nf1 == f1 then f else gennew (HCFUS(first, nf1)) |

2292 |
| HCMU (var, f1) -> |

2293 |
if compare var name != 0 then |

2294 |
let nf1 = func f1 in |

2295 |
if nf1 == f1 then f else gennew (HCMU(var, nf1)) |

2296 |
else |

2297 |
f |

2298 |
| HCNU (var, f1) -> |

2299 |
if compare var name != 0 then |

2300 |
let nf1 = func f1 in |

2301 |
if nf1 == f1 then f else gennew (HCNU(var, nf1)) |

2302 |
else |

2303 |
f |

2304 | |

2305 |
let rec hc_freeIn variable (f: hcFormula) = |

2306 |
match f.HC.node with |

2307 |
| HCTRUE |

2308 |
| HCFALSE |

2309 |
| HCAP _ |

2310 |
| HCNOT _ |

2311 |
| HCCONST _ |

2312 |
| HCCONSTN _ -> false |

2313 |
| HCVAR s -> |

2314 |
if compare variable s == 0 |

2315 |
then true |

2316 |
else false |

2317 |
| HCAT (s, f1) -> |

2318 |
hc_freeIn variable f1 |

2319 |
| HCOR (f1, f2) |

2320 |
| HCAND (f1, f2) -> |

2321 |
hc_freeIn variable f1 || hc_freeIn variable f2 |

2322 |
| HCEX (_, f1) |

2323 |
| HCAX (_, f1) |

2324 |
| HCENFORCES (_, f1) |

2325 |
| HCALLOWS (_, f1) |

2326 |
| HCMORETHAN (_, _, f1) |

2327 |
| HCMAXEXCEPT (_, _, f1) |

2328 |
| HCATLEASTPROB (_, f1) |

2329 |
| HCLESSPROBFAIL (_, f1) |

2330 |
| HCID f1 -> |

2331 |
hc_freeIn variable f1 |

2332 |
| HCNORM (f1, f2) |

2333 |
| HCNORMN (f1, f2) |

2334 |
| HCCHC (f1, f2) -> |

2335 |
hc_freeIn variable f1 || hc_freeIn variable f2 |

2336 |
| HCFUS (first, f1) -> |

2337 |
hc_freeIn variable f1 |

2338 |
| HCMU (var, f1) |

2339 |
| HCNU (var, f1) -> |

2340 |
(* Do we need to exclude bound variables here? *) |

2341 |
hc_freeIn variable f1 |

2342 | |

2343 | |

2344 |
(** An instantiation of a hash table (of the standard library) |

2345 |
for hash-consed formulae. The test for equality |

2346 |
and computing the hash value is done in constant time. |

2347 |
*) |

2348 |
module HcFHt = Hashtbl.Make( |

2349 |
struct |

2350 |
type t = hcFormula |

2351 |
let equal (f1 : t) f2 = f1.HC.tag = f2.HC.tag |

2352 |
let hash (f : t) = f.HC.tag |

2353 |
end |

2354 |
) |