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

History | View | Annotate | Download (73.4 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 |
exception NotAconjunctive of unit |

727 | |

728 |
let isMuAconjunctive (formula:formula) : bool = |

729 |
let module SS = Set.Make(String) in |

730 | |

731 |
(* Accepts formula f and a set of currently bound mu variables. Returns a subset |

732 |
* of those, which actually occured free in the formula. |

733 |
* Raises an CoAlgException if the formula is determined not to be aconjunctive *) |

734 |
let rec verifyMuAconjunctiveInternal (formula:formula) (bound_mu_vars: SS.t) : SS.t = |

735 |
let proc f = verifyMuAconjunctiveInternal f bound_mu_vars in |

736 |
match formula with |

737 |
| VAR s when SS.mem s bound_mu_vars -> SS.singleton s |

738 |
| VAR s -> SS.empty |

739 |
(* s is now bound by a nu and shadows any privious binding s *) |

740 |
| NU (s, a) -> verifyMuAconjunctiveInternal a (SS.remove s bound_mu_vars) |

741 |
(* Bind s in the recursive call but don't return it as occuring free *) |

742 |
| MU (s, a) -> |

743 |
SS.remove s (verifyMuAconjunctiveInternal a (SS.add s bound_mu_vars)) |

744 | |

745 |
(* This is the interesting case *) |

746 |
| AND (a, b) -> |

747 |
let a_vars = proc a in |

748 |
let b_vars = proc b in |

749 | |

750 |
(* If both subformulas contain free mu variables, the formula is not aconjunctive *) |

751 |
if not (SS.is_empty a_vars) && not (SS.is_empty b_vars) then |

752 |
raise (NotAconjunctive ()) |

753 |
else |

754 |
SS.union a_vars b_vars (* one of them is empty anyways *) |

755 | |

756 |
(* The other cases just pass argument and return value through *) |

757 |
| TRUE | FALSE | AP _ |

758 |
| CONST _ | CONSTN _ -> SS.empty |

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

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

761 |
| OR (a,b) | EQU (a,b) | IMP (a,b) -> SS.union (proc a) (proc b) |

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

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

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

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

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

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

768 |
| CHC (a,b) -> SS.union (proc a) (proc b) |

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

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

771 |
raise (CoAlgException ("verifyMuAconjunctiveInternal: CTL should have been removed at this point")) |

772 |
in |

773 |
try ignore (verifyMuAconjunctiveInternal formula SS.empty); true |

774 |
with NotAconjunctive () -> false |

775 | |

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

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

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

779 |
negations is even. |

780 |
*) |

781 |
let rec verifyMuMonotone negations formula = |

782 |
let proc = verifyMuMonotone negations in |

783 |
match formula with |

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

785 |
| CONST _ |

786 |
| CONSTN _ -> () |

787 |
| AT (_,a) |

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

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

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

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

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

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

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

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

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

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

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

799 |
| MU (s, f) |

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

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

802 |
verifyMuMonotone newNeg f |

803 |
| VAR s -> |

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

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

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

807 |
| NOT a -> |

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

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

810 |
verifyMuMonotone newNeg a |

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

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

813 | |

814 |
let rec verifyMuGuarded unguarded formula = |

815 |
let proc = verifyMuGuarded unguarded in |

816 |
match formula with |

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

818 |
| CONST _ |

819 |
| CONSTN _ -> () |

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

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

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

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

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

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

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

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

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

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

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

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

832 |
| MU (s, f) |

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

834 |
let newUnguard = s :: unguarded in |

835 |
verifyMuGuarded newUnguard f |

836 |
| VAR s -> |

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

838 |
if List.exists finder unguarded then |

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

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

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

842 | |

843 |
let verifyFormula formula = |

844 |
verifyMuAltFree formula; |

845 |
verifyMuMonotone [] formula; |

846 |
verifyMuGuarded [] formula |

847 | |

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

849 |
It is a standard recursive descent procedure. |

850 |
@param ts A token stream. |

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

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

853 |
*) |

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

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

856 |
let f1 = convertToMu formula in |

857 |
match Stream.peek ts with |

858 |
| None -> f1 |

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

860 |
Stream.junk ts; |

861 |
let f2 = parse_formula symtab ts in |

862 |
EQU (f1, f2) |

863 |
| _ -> f1 |

864 | |

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

866 |
It is a standard recursive descent procedure. |

867 |
@param ts A token stream. |

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

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

870 |
*) |

871 |
and parse_imp symtab ts= |

872 |
let f1 = parse_or symtab ts in |

873 |
match Stream.peek ts with |

874 |
| None -> f1 |

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

876 |
Stream.junk ts; |

877 |
let f2 = parse_imp symtab ts in |

878 |
IMP (f1, f2) |

879 |
| _ -> f1 |

880 | |

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

882 |
It is a standard recursive descent procedure. |

883 |
@param ts A token stream. |

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

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

886 |
*) |

887 |
and parse_or symtab ts = |

888 |
let f1 = parse_and symtab ts in |

889 |
match Stream.peek ts with |

890 |
| None -> f1 |

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

892 |
Stream.junk ts; |

893 |
let f2 = parse_or symtab ts in |

894 |
OR (f1, f2) |

895 |
| _ -> f1 |

896 | |

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

898 |
It is a standard recursive descent procedure. |

899 |
@param ts A token stream. |

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

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

902 |
*) |

903 |
and parse_and symtab ts = |

904 |
let f1 = parse_cimp symtab ts in |

905 |
match Stream.peek ts with |

906 |
| None -> f1 |

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

908 |
Stream.junk ts; |

909 |
let f2 = parse_and symtab ts in |

910 |
AND (f1, f2) |

911 |
| _ -> f1 |

912 | |

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

914 |
It is a standard recursive descent procedure. |

915 |
@param ts A token stream. |

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

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

918 |
*) |

919 |
and parse_cimp symtab ts = |

920 |
let f1 = parse_rest symtab ts in |

921 |
match Stream.peek ts with |

922 |
| None -> f1 |

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

924 |
Stream.junk ts; |

925 |
let f2 = parse_cimp symtab ts in |

926 |
NORM (f1, f2) |

927 |
| _ -> f1 |

928 | |

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

930 |
It is a standard recursive descent procedure. |

931 |
@param ts A token stream. |

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

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

934 |
*) |

935 |
and parse_rest symtab ts = |

936 |
let boxinternals noNo es = |

937 |
let n = |

938 |
if noNo then 0 |

939 |
else |

940 |
match Stream.next ts with |

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

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

943 |
in |

944 |
let (s,denominator) = |

945 |
match Stream.peek ts with |

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

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

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

949 |
Stream.junk ts; |

950 |
match Stream.next ts with |

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

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

953 |
end |

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

955 |
in |

956 |
if (denominator < n) then begin |

957 |
let explanation = |

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

959 |
in |

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

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

962 |
) |

963 |
end; |

964 |
let _ = |

965 |
match Stream.next ts with |

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

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

968 |
in |

969 |
(n, denominator, s) |

970 |
in |

971 |
let rec agentlist es = |

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

973 |
match Stream.next ts with |

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

975 |
then n::(agentlist es) |

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

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

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

979 |
in |

980 |
match Stream.next ts with |

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

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

983 |
AP "true" |

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

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

986 |
AP "false" |

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

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

989 |
| A.Ident s -> |

990 |
(try |

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

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

993 |
VAR symbol |

994 |
with Not_found -> AP s) |

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

996 |
let f = parse_rest symtab ts in |

997 |
NOT f |

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

999 |
let s = |

1000 |
match Stream.next ts with |

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

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

1003 |
in |

1004 |
let f = parse_rest symtab ts in |

1005 |
AT (s, f) |

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

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

1008 |
let f1 = parse_rest symtab ts in |

1009 |
EX (s, f1) |

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

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

1012 |
let f1 = parse_rest symtab ts in |

1013 |
AX (s, f1) |

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

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

1016 |
let f1 = parse_rest symtab ts in |

1017 |
ENFORCES (ls, f1) |

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

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

1020 |
let f1 = parse_rest symtab ts in |

1021 |
ALLOWS (ls, f1) |

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

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

1024 |
let f1 = parse_rest symtab ts in |

1025 |
if (denom <> 0) |

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

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

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

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

1030 |
let f1 = parse_rest symtab ts in |

1031 |
if (denom <> 0) |

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

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

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

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

1036 |
let f1 = parse_rest symtab ts in |

1037 |
if (denom <> 0) |

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

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

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

1041 |
match Stream.next ts with |

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

1043 |
| A.Kwd s |

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

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

1046 |
end |

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

1048 |
let f = parse_formula symtab ts in |

1049 |
match Stream.next ts with |

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

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

1052 |
let f2 = parse_formula symtab ts in |

1053 |
match Stream.next ts with |

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

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

1056 |
end |

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

1058 |
end |

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

1060 |
let f = parse_rest symtab ts in |

1061 |
ID f |

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

1063 |
let f = parse_rest symtab ts in |

1064 |
FUS (true, f) |

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

1066 |
let f = parse_rest symtab ts in |

1067 |
FUS (false, f) |

1068 |
| A.Kwd "μ" | A.Kwd "µ" -> |

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

1070 |
let symbol = Stream.next gensym in |

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

1072 |
let f1 = parse_rest newtab ts in |

1073 |
MU (symbol, f1) |

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

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

1076 |
let symbol = Stream.next gensym in |

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

1078 |
let f1 = parse_rest newtab ts in |

1079 |
NU (symbol, f1) |

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

1081 |
let f = parse_rest symtab ts in |

1082 |
AF f |

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

1084 |
let f = parse_rest symtab ts in |

1085 |
EF f |

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

1087 |
let f = parse_rest symtab ts in |

1088 |
AG f |

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

1090 |
let f = parse_rest symtab ts in |

1091 |
EG f |

1092 |
| A.Kwd "A" -> |

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

1094 |
let f1 = parse_formula symtab ts in begin |

1095 |
match Stream.next ts with |

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

1097 |
let f2 = parse_formula symtab ts in |

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

1099 |
AU (f1, f2) |

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

1101 |
let f2 = parse_formula symtab ts in |

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

1103 |
AR (f1, f2) |

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

1105 |
let f2 = parse_formula symtab ts in |

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

1107 |
AB (f1, f2) |

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

1109 |
end |

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

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

1112 |
let f1 = parse_formula symtab ts in begin |

1113 |
match Stream.next ts with |

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

1115 |
let f2 = parse_formula symtab ts in |

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

1117 |
EU (f1, f2) |

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

1119 |
let f2 = parse_formula symtab ts in |

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

1121 |
ER (f1, f2) |

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

1123 |
let f2 = parse_formula symtab ts in |

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

1125 |
EB (f1, f2) |

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

1127 |
end |

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

1129 |
let f1 = parse_rest symtab ts in |

1130 |
AX ("", f1) |

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

1132 |
let f1 = parse_rest symtab ts in |

1133 |
EX ("", f1) |

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

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

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

1137 | |

1138 |
(** Parses a sorted formula. |

1139 |
@param ts A token stream. |

1140 |
@return A sorted formula. |

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

1142 |
*) |

1143 |
let parse_sortedFormula ts = |

1144 |
let nr = |

1145 |
match Stream.peek ts with |

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

1147 |
if n >= 0 then begin |

1148 |
Stream.junk ts; |

1149 |
let () = |

1150 |
match Stream.next ts with |

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

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

1153 |
in |

1154 |
n |

1155 |
end else |

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

1157 |
| _ -> 0 |

1158 |
in |

1159 |
let f = parse_formula [] ts in |

1160 |
(nr, f) |

1161 | |

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

1163 |
@param ts A token stream. |

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

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

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

1167 |
*) |

1168 |
let rec parse_sortedFormulaList ts acc = |

1169 |
let f1 = parse_sortedFormula ts in |

1170 |
match Stream.peek ts with |

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

1172 |
Stream.junk ts; |

1173 |
parse_sortedFormulaList ts (f1::acc) |

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

1175 | |

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

1177 |
@param fkt An import function. |

1178 |
@param s A string. |

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

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

1181 |
*) |

1182 |
let importWrapper fkt s = |

1183 |
let ts = lexer s in |

1184 |
try |

1185 |
let res = fkt ts in |

1186 |
let _ = |

1187 |
match Stream.peek ts with |

1188 |
| None -> () |

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

1190 |
in |

1191 |
res |

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

1193 | |

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

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

1196 |
@return The resulting formula. |

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

1198 |
*) |

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

1200 | |

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

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

1203 |
@return The sorted formula. |

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

1205 |
*) |

1206 |
let importSortedFormula s = importWrapper parse_sortedFormula s |

1207 | |

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

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

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

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

1212 |
f is a sorted formula. |

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

1214 |
*) |

1215 |
let importQuery s = |

1216 |
let fkt ts = |

1217 |
match Stream.peek ts with |

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

1219 |
Stream.junk ts; |

1220 |
let f = parse_sortedFormula ts in |

1221 |
([], f) |

1222 |
| _ -> |

1223 |
let fl = parse_sortedFormulaList ts [] in |

1224 |
match Stream.peek ts with |

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

1226 |
Stream.junk ts; |

1227 |
let f = parse_sortedFormula ts in |

1228 |
(fl, f) |

1229 |
| _ -> |

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

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

1232 |
in |

1233 |
importWrapper fkt s |

1234 | |

1235 | |

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

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

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

1239 |
@param f A formula. |

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

1241 |
that is equivalent to ~f. |

1242 |
*) |

1243 | |

1244 |
let rec equals f_1 f_2 = |

1245 |
match f_1, f_2 with |

1246 |
| TRUE, TRUE -> true |

1247 |
| FALSE, FALSE -> true |

1248 |
| AP s1, AP s2 -> compare s1 s2 = 0 |

1249 |
| VAR f1, VAR f2 -> compare f1 f2 = 0 |

1250 |
| NOT f1, NOT f2 -> equals f1 f2 |

1251 |
| AT(s1,f1), AT(s2,f2) -> (compare s1 s2 = 0) && (equals f1 f2) |

1252 |
| AND(f1,g1), AND(f2,g2) -> (equals f1 f2) && (equals g1 g2) |

1253 |
| OR(f1,g1), OR(f2,g2) -> (equals f1 f2) && (equals g1 g2) |

1254 |
| EQU(f1,g1), EQU(f2,g2) -> (equals f1 f2) && (equals g1 g2) |

1255 |
| IMP(f1,g1), IMP(f2,g2) -> (equals f1 f2) && (equals g1 g2) |

1256 |
| EX(s1,g1), EX(s2,g2) -> (compare s1 s2 = 0) && (equals g1 g2) |

1257 |
| AX(s1,g1), AX(s2,g2) -> (compare s1 s2 = 0) && (equals g1 g2) |

1258 |
| ENFORCES(s1,g1), ENFORCES(s2,g2) -> (compare s1 s2 = 0) && (equals g1 g2) |

1259 |
| ALLOWS(s1,g1), ALLOWS(s2,g2) -> (compare s1 s2 = 0) && (equals g1 g2) |

1260 |
| MIN(n1,s1,g1), MIN(n2,s2,g2) -> (compare n1 n2 = 0) && (compare s1 s2 = 0) && (equals g1 g2) |

1261 |
| MAX(n1,s1,g1), MAX(n2,s2,g2) -> (compare n1 n2 = 0) && (compare s1 s2 = 0) && (equals g1 g2) |

1262 |
| MORETHAN(n1,s1,g1), MORETHAN(n2,s2,g2) -> (compare n1 n2 = 0) && (compare s1 s2 = 0) && (equals g1 g2) |

1263 |
| MAXEXCEPT(n1,s1,g1), MAXEXCEPT(n2,s2,g2) -> (compare n1 n2 = 0) && (compare s1 s2 = 0) && (equals g1 g2) |

1264 |
| ATLEASTPROB(p1,g1), ATLEASTPROB(p2,g2) -> (compare p1 p2 = 0) && (equals g1 g2) |

1265 |
| LESSPROBFAIL(p1,g1), LESSPROBFAIL(p2,g2) -> (compare p1 p2 = 0) && (equals g1 g2) |

1266 |
| CONST s1, CONST s2 -> compare s1 s2 = 0 |

1267 |
| CONSTN s1, CONSTN s2 -> compare s1 s2 = 0 |

1268 |
| ID(f1), ID(f2) -> equals f1 f2 |

1269 |
| NORM(f1,g1),NORM(f2,g2) -> (equals f1 f2) && (equals g1 g2) |

1270 |
| NORMN(f1,g1), NORMN(f2,g2) -> (equals f1 f2) && (equals g1 g2) |

1271 |
| CHC(f1,g1), CHC(f2,g2) -> (equals f1 f2) && (equals g1 g2) |

1272 |
| FUS(b1,g1), FUS(b2,g2) -> (compare b1 b2 = 0) && (equals g1 g2) |

1273 |
| MU(s1,g1), MU(s2,g2) -> (compare s1 s2 = 0) && (equals g1 g2) |

1274 |
| NU(s1,g1), NU(s2,g2) -> (compare s1 s2 = 0) && (equals g1 g2) |

1275 |
| _ -> false |

1276 | |

1277 | |

1278 |
let rec nnfNeg f = |

1279 |
match f with |

1280 |
| TRUE -> FALSE |

1281 |
| FALSE -> TRUE |

1282 |
| AP _ -> NOT f |

1283 |
| VAR _ -> f |

1284 |
| NOT f1 -> nnf f1 |

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

1300 |
| CONST s -> CONSTN s |

1301 |
| CONSTN s -> CONST s |

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

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

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

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

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

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

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

1309 |
| AF _ | EF _ |

1310 |
| AG _ | EG _ |

1311 |
| AU _ | EU _ |

1312 |
| AR _ | ER _ |

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

1314 | |

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

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

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

1318 |
@param f A formula. |

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

1320 |
that is equivalent to f. |

1321 |
*) |

1322 |
and nnf f = |

1323 |
match f with |

1324 |
| TRUE |

1325 |
| FALSE |

1326 |
| AP _ |

1327 |
| NOT (AP _) |

1328 |
| CONST _ |

1329 |
| CONSTN _ |

1330 |
| VAR _ -> f |

1331 |
| NOT f1 -> nnfNeg f1 |

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

1333 |
let ft1 = nnf f1 in |

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

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

1336 |
let ft1 = nnf f1 in |

1337 |
let ft2 = nnf f2 in |

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

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

1340 |
let ft1 = nnf f1 in |

1341 |
let ft2 = nnf f2 in |

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

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

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

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

1346 |
let ft = nnf f1 in |

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

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

1349 |
let ft = nnf f1 in |

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

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

1352 |
let ft = nnf f1 in |

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

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

1355 |
let ft = nnf f1 in |

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

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

1358 |
if n = 0 then TRUE |

1359 |
else |

1360 |
let ft = nnf f1 in |

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

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

1363 |
let ft = nnfNeg f1 in |

1364 |
MAXEXCEPT (n,s, ft) |

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

1366 |
let ft = nnf f1 in |

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

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

1369 |
let ft = nnf f1 in |

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

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

1372 |
let ft = nnf f1 in |

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

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

1375 |
let ft = nnf f1 in |

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

1377 |
| ID (f1) -> |

1378 |
let ft = nnf f1 in |

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

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

1381 |
let ft1 = nnf f1 in |

1382 |
let ft2 = nnf f2 in |

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

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

1385 |
let ft1 = nnf f1 in |

1386 |
let ft2 = nnf f2 in |

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

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

1389 |
let ft1 = nnf f1 in |

1390 |
let ft2 = nnf f2 in |

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

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

1393 |
let ft = nnf f1 in |

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

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

1396 |
let ft = nnf f1 in |

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

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

1399 |
let ft = nnf f1 in |

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

1401 |
| AF _ | EF _ |

1402 |
| AG _ | EG _ |

1403 |
| AU _ | EU _ |

1404 |
| AR _ | ER _ |

1405 |
| AB _ | EB _ -> |

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

1407 | |

1408 |
(** Simplifies a formula. |

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

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

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

1412 |
*) |

1413 |
let rec simplify f = |

1414 |
match f with |

1415 |
| TRUE |

1416 |
| FALSE |

1417 |
| AP _ |

1418 |
| NOT (AP _) |

1419 |
| VAR _ |

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

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

1422 |
let ft = simplify f1 in |

1423 |
begin |

1424 |
match ft with |

1425 |
| FALSE -> FALSE |

1426 |
| TRUE -> TRUE |

1427 |
| AT _ -> ft |

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

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

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

1431 |
end |

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

1433 |
let ft1 = simplify f1 in |

1434 |
let ft2 = simplify f2 in |

1435 |
begin |

1436 |
match ft1, ft2 with |

1437 |
| TRUE, _ -> TRUE |

1438 |
| FALSE, _ -> ft2 |

1439 |
| _, TRUE -> TRUE |

1440 |
| _, FALSE -> ft1 |

1441 |
| _, _ -> |

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

1443 |
else OR (ft1, ft2) |

1444 |
end |

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

1446 |
let ft1 = simplify f1 in |

1447 |
let ft2 = simplify f2 in |

1448 |
begin |

1449 |
match ft1, ft2 with |

1450 |
| TRUE, _ -> ft2 |

1451 |
| FALSE, _ -> FALSE |

1452 |
| _, TRUE -> ft1 |

1453 |
| _, FALSE -> FALSE |

1454 |
| _, _ -> |

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

1456 |
else AND (ft1, ft2) |

1457 |
end |

1458 |
| NOT _ |

1459 |
| EQU _ |

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

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

1462 |
let ft = simplify f1 in |

1463 |
begin |

1464 |
match ft with |

1465 |
| FALSE -> FALSE |

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

1467 |
end |

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

1469 |
let ft = simplify f1 in |

1470 |
begin |

1471 |
match ft with |

1472 |
| TRUE -> TRUE |

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

1474 |
end |

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

1476 |
let ft = simplify f1 in |

1477 |
begin |

1478 |
match ft with |

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

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

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

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

1483 |
*) |

1484 |
| TRUE -> TRUE |

1485 |
| FALSE -> FALSE |

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

1487 |
end |

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

1489 |
let ft = simplify f1 in |

1490 |
begin |

1491 |
match ft with |

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

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

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

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

1496 |
*) |

1497 |
| TRUE -> TRUE |

1498 |
| FALSE -> FALSE |

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

1500 |
end |

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

1502 |
if n = 0 then TRUE |

1503 |
else |

1504 |
let ft = simplify f1 in |

1505 |
begin |

1506 |
match ft with |

1507 |
| FALSE -> FALSE |

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

1509 |
end |

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

1511 |
let ft = simplify f1 in |

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

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

1514 |
let ft = simplify f1 in |

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

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

1517 |
let ft = simplify f1 in |

1518 |
begin |

1519 |
match ft with |

1520 |
| FALSE -> TRUE |

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

1522 |
end |

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

1524 |
let ft1 = simplify f1 in |

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

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

1527 |
let ft1 = simplify f1 in |

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

1529 |
| CONST _ |

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

1531 |
| ID (f1) -> |

1532 |
let ft1 = simplify f1 in |

1533 |
begin |

1534 |
match ft1 with |

1535 |
| TRUE -> TRUE |

1536 |
| FALSE -> FALSE |

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

1538 |
end |

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

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

1541 |
let ft1 = simplify f1 in |

1542 |
let ft2 = simplify f2 in |

1543 |
begin |

1544 |
match ft2 with |

1545 |
| TRUE -> TRUE |

1546 |
| _ -> |

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

1548 |
else NORM (ft1, ft2) |

1549 |
end |

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

1551 |
let ft1 = simplify f1 in |

1552 |
let ft2 = simplify f2 in |

1553 |
begin |

1554 |
match ft2 with |

1555 |
| FALSE -> FALSE |

1556 |
| _ -> |

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

1558 |
else NORMN (ft1, ft2) |

1559 |
end |

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

1561 |
let ft1 = simplify f1 in |

1562 |
let ft2 = simplify f2 in |

1563 |
begin |

1564 |
match ft1, ft2 with |

1565 |
| TRUE, TRUE -> TRUE |

1566 |
| FALSE, FALSE -> FALSE |

1567 |
| _, _ -> |

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

1569 |
else CHC (ft1, ft2) |

1570 |
end |

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

1572 |
let ft = simplify f1 in |

1573 |
begin |

1574 |
match ft with |

1575 |
| FALSE -> FALSE |

1576 |
| TRUE -> TRUE |

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

1578 |
end |

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

1580 |
let ft = simplify f1 in |

1581 |
begin |

1582 |
match ft with |

1583 |
| TRUE -> TRUE |

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

1585 |
end |

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

1587 |
let ft = simplify f1 in |

1588 |
begin |

1589 |
match ft with |

1590 |
| TRUE -> TRUE |

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

1592 |
end |

1593 |
| AF _ | EF _ |

1594 |
| AG _ | EG _ |

1595 |
| AU _ | EU _ |

1596 |
| AR _ | ER _ |

1597 |
| AB _ | EB _ -> |

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

1599 | |

1600 |
(** Destructs an atomic proposition. |

1601 |
@param f An atomic proposition. |

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

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

1604 |
*) |

1605 |
let dest_ap f = |

1606 |
match f with |

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

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

1609 | |

1610 |
(** Destructs a nominal. |

1611 |
@param f A nominal. |

1612 |
@return The name of the nominal |

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

1614 |
*) |

1615 |
let dest_nom f = |

1616 |
match f with |

1617 |
| AP s when isNominal s -> s |

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

1619 | |

1620 |
(** Destructs a negation. |

1621 |
@param f A negation. |

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

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

1624 |
*) |

1625 |
let dest_not f = |

1626 |
match f with |

1627 |
| NOT f1 -> f1 |

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

1629 | |

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

1631 |
@param f An @-formula. |

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

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

1634 |
*) |

1635 |
let dest_at f = |

1636 |
match f with |

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

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

1639 | |

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

1641 |
@param f An or-formula. |

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

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

1644 |
*) |

1645 |
let dest_or f = |

1646 |
match f with |

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

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

1649 | |

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

1651 |
@param f An and-formula. |

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

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

1654 |
*) |

1655 |
let dest_and f = |

1656 |
match f with |

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

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

1659 | |

1660 |
(** Destructs an equivalence. |

1661 |
@param f An equivalence. |

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

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

1664 |
*) |

1665 |
let dest_equ f = |

1666 |
match f with |

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

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

1669 | |

1670 |
(** Destructs an implication. |

1671 |
@param f An implication. |

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

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

1674 |
*) |

1675 |
let dest_imp f = |

1676 |
match f with |

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

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

1679 | |

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

1681 |
@param f An EX-formula. |

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

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

1684 |
*) |

1685 |
let dest_ex f = |

1686 |
match f with |

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

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

1689 | |

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

1691 |
@param f An AX-formula. |

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

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

1694 |
*) |

1695 |
let dest_ax f = |

1696 |
match f with |

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

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

1699 | |

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

1701 |
@param f A MIN-formula. |

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

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

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

1705 |
*) |

1706 |
let dest_min f = |

1707 |
match f with |

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

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

1710 | |

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

1712 |
@param f A MAX-formula. |

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

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

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

1716 |
*) |

1717 |
let dest_max f = |

1718 |
match f with |

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

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

1721 | |

1722 |
(** Destructs a choice formula. |

1723 |
@param f A choice formula. |

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

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

1726 |
*) |

1727 |
let dest_choice f = |

1728 |
match f with |

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

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

1731 | |

1732 |
(** Destructs a fusion formula. |

1733 |
@param f A fusion formula. |

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

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

1736 |
f1 is the immediate subformulae of f. |

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

1738 |
*) |

1739 |
let dest_fusion f = |

1740 |
match f with |

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

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

1743 | |

1744 | |

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

1746 |
@param f A formula. |

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

1748 |
*) |

1749 |
let is_true f = |

1750 |
match f with |

1751 |
| TRUE -> true |

1752 |
| _ -> false |

1753 | |

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

1755 |
@param f A formula. |

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

1757 |
*) |

1758 |
let is_false f = |

1759 |
match f with |

1760 |
| FALSE -> true |

1761 |
| _ -> false |

1762 | |

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

1764 |
@param f A formula. |

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

1766 |
*) |

1767 |
let is_ap f = |

1768 |
match f with |

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

1770 |
| _ -> false |

1771 | |

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

1773 |
@param f A formula. |

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

1775 |
*) |

1776 |
let is_nom f = |

1777 |
match f with |

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

1779 |
| _ -> false |

1780 | |

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

1782 |
@param f A formula. |

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

1784 |
*) |

1785 |
let is_not f = |

1786 |
match f with |

1787 |
| NOT _ -> true |

1788 |
| _ -> false |

1789 | |

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

1791 |
@param f A formula. |

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

1793 |
*) |

1794 |
let is_at f = |

1795 |
match f with |

1796 |
| AT _ -> true |

1797 |
| _ -> false |

1798 | |

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

1800 |
@param f A formula. |

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

1802 |
*) |

1803 |
let is_or f = |

1804 |
match f with |

1805 |
| OR _ -> true |

1806 |
| _ -> false |

1807 | |

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

1809 |
@param f A formula. |

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

1811 |
*) |

1812 |
let is_and f = |

1813 |
match f with |

1814 |
| AND _ -> true |

1815 |
| _ -> false |

1816 | |

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

1818 |
@param f A formula. |

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

1820 |
*) |

1821 |
let is_equ f = |

1822 |
match f with |

1823 |
| EQU _ -> true |

1824 |
| _ -> false |

1825 | |

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

1827 |
@param f A formula. |

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

1829 |
*) |

1830 |
let is_imp f = |

1831 |
match f with |

1832 |
| IMP _ -> true |

1833 |
| _ -> false |

1834 | |

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

1836 |
@param f A formula. |

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

1838 |
*) |

1839 |
let is_ex f = |

1840 |
match f with |

1841 |
| EX _ -> true |

1842 |
| _ -> false |

1843 | |

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

1845 |
@param f A formula. |

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

1847 |
*) |

1848 |
let is_ax f = |

1849 |
match f with |

1850 |
| AX _ -> true |

1851 |
| _ -> false |

1852 | |

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

1854 |
@param f A formula. |

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

1856 |
*) |

1857 |
let is_min f = |

1858 |
match f with |

1859 |
| MIN _ -> true |

1860 |
| _ -> false |

1861 | |

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

1863 |
@param f A formula. |

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

1865 |
*) |

1866 |
let is_max f = |

1867 |
match f with |

1868 |
| MAX _ -> true |

1869 |
| _ -> false |

1870 | |

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

1872 |
@param f A formula. |

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

1874 |
*) |

1875 |
let is_choice f = |

1876 |
match f with |

1877 |
| CHC _ -> true |

1878 |
| _ -> false |

1879 | |

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

1881 |
@param f A formula. |

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

1883 |
*) |

1884 |
let is_fusion f = |

1885 |
match f with |

1886 |
| FUS _ -> true |

1887 |
| _ -> false |

1888 | |

1889 | |

1890 |
(** The constant True. |

1891 |
*) |

1892 |
let const_true = TRUE |

1893 | |

1894 |
(** The constant False. |

1895 |
*) |

1896 |
let const_false = FALSE |

1897 | |

1898 |
(** Constructs an atomic proposition. |

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

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

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

1902 |
*) |

1903 |
let const_ap s = |

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

1905 |
else AP s |

1906 | |

1907 |
(** Constructs a nominal. |

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

1909 |
@return A nominal with name s. |

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

1911 |
*) |

1912 |
let const_nom s = |

1913 |
if isNominal s then AP s |

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

1915 | |

1916 |
(** Negates a formula. |

1917 |
@param f A formula. |

1918 |
@return The negation of f. |

1919 |
*) |

1920 |
let const_not f = NOT f |

1921 | |

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

1923 |
@param s A nominal name. |

1924 |
@param f A formula. |

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

1926 |
*) |

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

1928 | |

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

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

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

1932 |
@return The formula f1 | f2. |

1933 |
*) |

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

1935 | |

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

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

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

1939 |
@return The formula f1 & f2. |

1940 |
*) |

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

1942 | |

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

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

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

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

1947 |
*) |

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

1949 | |

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

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

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

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

1954 |
*) |

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

1956 | |

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

1958 |
@param s A role name. |

1959 |
@param f A formula. |

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

1961 |
*) |

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

1963 | |

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

1965 |
@param s A role name. |

1966 |
@param f A formula. |

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

1968 |
*) |

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

1970 | |

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

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

1973 |
@param s A role name. |

1974 |
@param f A formula. |

1975 |
@return The formula MIN f. |

1976 |
@raise CoAlgException Iff n is negative. |

1977 |
*) |

1978 |
let const_min n s f = |

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

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

1981 | |

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

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

1984 |
@param s A role name. |

1985 |
@param f A formula. |

1986 |
@return The formula MAX f. |

1987 |
@raise CoAlgException Iff n is negative. |

1988 |
*) |

1989 |
let const_max n s f = |

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

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

1992 | |

1993 |
let const_enforces p f = |

1994 |
ENFORCES (p,f) |

1995 | |

1996 |
let const_allows p f = |

1997 |
ALLOWS (p,f) |

1998 | |

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

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

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

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

2003 |
*) |

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

2005 | |

2006 |
(** Constructs a fusion formula. |

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

2008 |
@param f1 A formula. |

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

2010 |
*) |

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

2012 | |

2013 | |

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

2015 |
such that structural and physical equality coincide. |

2016 | |

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

2018 |
constructs |

2019 |
*) |

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

2021 |
and hcFormula_node = |

2022 |
| HCTRUE |

2023 |
| HCFALSE |

2024 |
| HCAP of string |

2025 |
| HCNOT of string |

2026 |
| HCAT of string * hcFormula |

2027 |
| HCOR of hcFormula * hcFormula |

2028 |
| HCAND of hcFormula * hcFormula |

2029 |
| HCEX of string * hcFormula |

2030 |
| HCAX of string * hcFormula |

2031 |
| HCENFORCES of int list * hcFormula |

2032 |
| HCALLOWS of int list * hcFormula |

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

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

2035 |
| HCATLEASTPROB of rational * hcFormula |

2036 |
| HCLESSPROBFAIL of rational * hcFormula |

2037 |
| HCCONST of string |

2038 |
| HCCONSTN of string |

2039 |
| HCID of hcFormula |

2040 |
| HCNORM of hcFormula * hcFormula |

2041 |
| HCNORMN of hcFormula * hcFormula |

2042 |
| HCCHC of hcFormula * hcFormula |

2043 |
| HCFUS of bool * hcFormula |

2044 |
| HCMU of string * hcFormula |

2045 |
| HCNU of string * hcFormula |

2046 |
| HCVAR of string |

2047 | |

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

2049 |
@param f1 The first formula node. |

2050 |
@param f2 The second formula node. |

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

2052 |
*) |

2053 |
let equal_hcFormula_node f1 f2 = |

2054 |
match f1, f2 with |

2055 |
| HCTRUE, HCTRUE -> true |

2056 |
| HCFALSE, HCFALSE -> true |

2057 |
| HCCONST s1, HCCONST s2 |

2058 |
| HCCONSTN s1, HCCONSTN s2 |

2059 |
| HCAP s1, HCAP s2 |

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

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

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

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

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

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

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

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

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

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

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

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

2072 |
p1 = p2 && f1 == f2 |

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

2074 |
p1 = p2 && f1 == f2 |

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

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

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

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

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

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

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

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

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

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

2085 |
| HCTRUE, _ |

2086 |
| HCFALSE, _ |

2087 |
| HCAP _, _ |

2088 |
| HCNOT _, _ |

2089 |
| HCAT _, _ |

2090 |
| HCOR _, _ |

2091 |
| HCAND _, _ |

2092 |
| HCEX _, _ |

2093 |
| HCAX _, _ |

2094 |
| HCENFORCES _, _ |

2095 |
| HCALLOWS _, _ |

2096 |
| HCMORETHAN _, _ |

2097 |
| HCMAXEXCEPT _, _ |

2098 |
| HCATLEASTPROB _, _ |

2099 |
| HCLESSPROBFAIL _, _ |

2100 |
| HCCONST _, _ |

2101 |
| HCCONSTN _, _ |

2102 |
| HCID _, _ |

2103 |
| HCNORM _, _ |

2104 |
| HCNORMN _, _ |

2105 |
| HCCHC _, _ |

2106 |
| HCFUS _, _ |

2107 |
| HCMU _, _ |

2108 |
| HCNU _, _ |

2109 |
| HCVAR _, _ -> false |

2110 | |

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

2112 |
@param f A formula node. |

2113 |
@return The hash value of f. |

2114 |
*) |

2115 |
let hash_hcFormula_node f = |

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

2117 |
match f with |

2118 |
| HCTRUE -> 0 |

2119 |
| HCFALSE -> 1 |

2120 |
| HCAP s |

2121 |
| HCNOT s |

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

2143 | |

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

2145 |
@param f A formula node. |

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

2147 |
*) |

2148 |
let toFml_hcFormula_node f = |

2149 |
match f with |

2150 |
| HCTRUE -> TRUE |

2151 |
| HCFALSE -> FALSE |

2152 |
| HCAP s -> AP s |

2153 |
| HCVAR s -> VAR s |

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

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

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

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

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

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

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

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

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

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

2164 |
| HCATLEASTPROB (p, f1) -> ATLEASTPROB (p, f1.HC.fml) |

2165 |
| HCLESSPROBFAIL (p, f1) -> LESSPROBFAIL (p, f1.HC.fml) |

2166 |
| HCCONST s -> CONST s |

2167 |
| HCCONSTN s -> CONSTN s |

2168 |
| HCID (f1) -> ID(f1.HC.fml) |

2169 |
| HCNORM (f1, f2) -> NORM(f1.HC.fml, f2.HC.fml) |

2170 |
| HCNORMN (f1, f2) -> NORMN(f1.HC.fml, f2.HC.fml) |

2171 |
| HCCHC (f1, f2) -> CHC (f1.HC.fml, f2.HC.fml) |

2172 |
| HCFUS (first, f1) -> FUS (first, f1.HC.fml) |

2173 |
| HCMU (var, f1) -> MU (var, f1.HC.fml) |

2174 |
| HCNU (var, f1) -> NU (var, f1.HC.fml) |

2175 | |

2176 |
(** Determines the negation (in negation normal form) of a formula node. |

2177 |
@param f A formula node. |

2178 |
@return The negation (in negation normal form) of f. |

2179 |
*) |

2180 |
let negNde_hcFormula_node f = |

2181 |
match f with |

2182 |
| HCTRUE -> HCFALSE |

2183 |
| HCFALSE -> HCTRUE |

2184 |
| HCAP s -> HCNOT s |

2185 |
| HCNOT s -> HCAP s |

2186 |
| HCVAR s -> f |

2187 |
| HCAT (s, f1) -> HCAT (s, f1.HC.neg) |

2188 |
| HCOR (f1, f2) -> HCAND (f1.HC.neg, f2.HC.neg) |

2189 |
| HCAND (f1, f2) -> HCOR (f1.HC.neg, f2.HC.neg) |

2190 |
| HCEX (s, f2) -> HCAX (s, f2.HC.neg) |

2191 |
| HCAX (s, f2) -> HCEX (s, f2.HC.neg) |

2192 |
| HCENFORCES (s, f2) -> HCALLOWS (s, f2.HC.neg) |

2193 |
| HCALLOWS (s, f2) -> HCENFORCES (s, f2.HC.neg) |

2194 |
| HCMORETHAN (n, s, f1) -> HCMAXEXCEPT (n, s, f1.HC.neg) |

2195 |
| HCMAXEXCEPT (n, s, f1) -> HCMORETHAN (n, s, f1.HC.neg) |

2196 |
| HCATLEASTPROB (p, f1) -> HCLESSPROBFAIL (p, f1.HC.neg) |

2197 |
| HCLESSPROBFAIL (p, f1) -> HCATLEASTPROB (p, f1.HC.neg) |

2198 |
| HCCONST s -> HCCONSTN s |

2199 |
| HCCONSTN s -> HCCONST s |

2200 |
| HCID (f1) -> HCID(f1.HC.neg) |

2201 |
| HCNORM (f1, f2) -> HCNORMN(f1.HC.neg, f2.HC.neg) |

2202 |
| HCNORMN (f1, f2) -> HCNORM(f1.HC.neg, f2.HC.neg) |

2203 |
| HCCHC (f1, f2) -> HCCHC (f1.HC.neg, f2.HC.neg) |

2204 |
| HCFUS (first, f1) -> HCFUS (first, f1.HC.neg) |

2205 |
| HCMU (name, f1) -> HCNU (name, f1.HC.neg) |

2206 |
| HCNU (name, f1) -> HCMU (name, f1.HC.neg) |

2207 | |

2208 |
(** An instantiation of hash-consing for formulae. |

2209 |
*) |

2210 |
module HcFormula = HC.Make( |

2211 |
struct |

2212 |
type nde = hcFormula_node |

2213 |
type fml = formula |

2214 |
let equal (n1 : nde) n2 = equal_hcFormula_node n1 n2 |

2215 |
let hash (n : nde) = hash_hcFormula_node n |

2216 |
let negNde (n : nde) = negNde_hcFormula_node n |

2217 |
let toFml (n : nde) = toFml_hcFormula_node n |

2218 |
end |

2219 |
) |

2220 | |

2221 |
(** Converts a formula into its hash-consed version. |

2222 |
@param hcF A hash-cons table for formulae. |

2223 |
@param f A formula in negation normal form. |

2224 |
@return The hash-consed version of f. |

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

2226 |
*) |

2227 |
let rec hc_formula hcF f = |

2228 |
match f with |

2229 |
| TRUE -> HcFormula.hashcons hcF HCTRUE |

2230 |
| FALSE -> HcFormula.hashcons hcF HCFALSE |

2231 |
| AP s -> HcFormula.hashcons hcF (HCAP s) |

2232 |
| VAR s -> HcFormula.hashcons hcF (HCVAR s) |

2233 |
| NOT (AP s) -> HcFormula.hashcons hcF (HCNOT s) |

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

2235 |
let tf1 = hc_formula hcF f1 in |

2236 |
HcFormula.hashcons hcF (HCAT (s, tf1)) |

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

2238 |
let tf1 = hc_formula hcF f1 in |

2239 |
let tf2 = hc_formula hcF f2 in |

2240 |
HcFormula.hashcons hcF (HCOR (tf1, tf2)) |

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

2242 |
let tf1 = hc_formula hcF f1 in |

2243 |
let tf2 = hc_formula hcF f2 in |

2244 |
HcFormula.hashcons hcF (HCAND (tf1, tf2)) |

2245 |
| NOT _ |

2246 |
| EQU _ |

2247 |
| MIN _ |

2248 |
| MAX _ |

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

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

2251 |
let tf1 = hc_formula hcF f1 in |

2252 |
HcFormula.hashcons hcF (HCEX (s, tf1)) |

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

2254 |
let tf1 = hc_formula hcF f1 in |

2255 |
HcFormula.hashcons hcF (HCAX (s, tf1)) |

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

2257 |
let tf1 = hc_formula hcF f1 in |

2258 |
HcFormula.hashcons hcF (HCENFORCES (s, tf1)) |

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

2260 |
let tf1 = hc_formula hcF f1 in |

2261 |
HcFormula.hashcons hcF (HCALLOWS (s, tf1)) |

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

2263 |
let tf1 = hc_formula hcF f1 in |

2264 |
HcFormula.hashcons hcF (HCMORETHAN (n, s, tf1)) |

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

2266 |
let tf1 = hc_formula hcF f1 in |

2267 |
HcFormula.hashcons hcF (HCMAXEXCEPT (n, s, tf1)) |

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

2269 |
HcFormula.hashcons hcF (HCATLEASTPROB (p, hc_formula hcF f1)) |

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

2271 |
HcFormula.hashcons hcF (HCLESSPROBFAIL (p, hc_formula hcF f1)) |

2272 |
| CONST s -> |

2273 |
HcFormula.hashcons hcF (HCCONST s) |

2274 |
| CONSTN s -> |

2275 |
HcFormula.hashcons hcF (HCCONSTN s) |

2276 |
| ID f1 -> |

2277 |
let tf1 = hc_formula hcF f1 in |

2278 |
HcFormula.hashcons hcF (HCID tf1) |

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

2280 |
let tf1 = hc_formula hcF f1 in |

2281 |
let tf2 = hc_formula hcF f2 in |

2282 |
HcFormula.hashcons hcF (HCNORM (tf1, tf2)) |

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

2284 |
let tf1 = hc_formula hcF f1 in |

2285 |
let tf2 = hc_formula hcF f2 in |

2286 |
HcFormula.hashcons hcF (HCNORMN (tf1, tf2)) |

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

2288 |
let tf1 = hc_formula hcF f1 in |

2289 |
let tf2 = hc_formula hcF f2 in |

2290 |
HcFormula.hashcons hcF (HCCHC (tf1, tf2)) |

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

2292 |
let tf1 = hc_formula hcF f1 in |

2293 |
HcFormula.hashcons hcF (HCFUS (first, tf1)) |

2294 |
| MU (var, f1) -> |

2295 |
let tf1 = hc_formula hcF f1 in |

2296 |
HcFormula.hashcons hcF (HCMU (var, tf1)) |

2297 |
| NU (var, f1) -> |

2298 |
let tf1 = hc_formula hcF f1 in |

2299 |
HcFormula.hashcons hcF (HCNU (var, tf1)) |

2300 |
| AF _ | EF _ |

2301 |
| AG _ | EG _ |

2302 |
| AU _ | EU _ |

2303 |
| AR _ | ER _ |

2304 |
| AB _ | EB _ -> |

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

2306 | |

2307 |
(* Replace the Variable name in f with formula formula |

2308 |
hc_replace foo φ ψ => ψ[foo |-> φ] |

2309 |
*) |

2310 |
let rec hc_replace hcF name (formula: hcFormula) (f: hcFormula) = |

2311 |
let func = hc_replace hcF name formula in |

2312 |
let gennew = HcFormula.hashcons hcF in |

2313 |
match f.HC.node with |

2314 |
| HCTRUE |

2315 |
| HCFALSE |

2316 |
| HCAP _ |

2317 |
| HCNOT _ |

2318 |
| HCCONST _ |

2319 |
| HCCONSTN _ -> f |

2320 |
| HCVAR s -> |

2321 |
if compare s name == 0 |

2322 |
then formula |

2323 |
else f |

2324 |
| HCAT (s, f1) -> |

2325 |
let nf1 = func f1 in |

2326 |
if nf1 == f1 then f else gennew (HCAT(s, nf1)) |

2327 |
| HCOR (f1, f2) -> |

2328 |
let nf1 = func f1 in |

2329 |
let nf2 = func f2 in |

2330 |
if nf1 == f1 && nf2 == f2 then f else gennew (HCOR(nf1, nf2)) |

2331 |
| HCAND (f1, f2) -> |

2332 |
let nf1 = func f1 in |

2333 |
let nf2 = func f2 in |

2334 |
if nf1 == f1 && nf2 == f2 then f else gennew (HCAND(nf1, nf2)) |

2335 |
| HCEX (s, f1) -> |

2336 |
let nf1 = func f1 in |

2337 |
if nf1 == f1 then f else gennew (HCEX(s, nf1)) |

2338 |
| HCAX (s, f1) -> |

2339 |
let nf1 = func f1 in |

2340 |
if nf1 == f1 then f else gennew (HCAX(s, nf1)) |

2341 |
| HCENFORCES (s, f1) -> |

2342 |
let nf1 = func f1 in |

2343 |
if nf1 == f1 then f else gennew (HCENFORCES(s, nf1)) |

2344 |
| HCALLOWS (s, f1) -> |

2345 |
let nf1 = func f1 in |

2346 |
if nf1 == f1 then f else gennew (HCALLOWS(s, nf1)) |

2347 |
| HCMORETHAN (n, s, f1) -> |

2348 |
let nf1 = func f1 in |

2349 |
if nf1 == f1 then f else gennew (HCMORETHAN(n, s, nf1)) |

2350 |
| HCMAXEXCEPT (n, s, f1) -> |

2351 |
let nf1 = func f1 in |

2352 |
if nf1 == f1 then f else gennew (HCMAXEXCEPT(n, s, nf1)) |

2353 |
| HCATLEASTPROB (p, f1) -> |

2354 |
let nf1 = func f1 in |

2355 |
if nf1 == f1 then f else gennew (HCATLEASTPROB(p, nf1)) |

2356 |
| HCLESSPROBFAIL (p, f1) -> |

2357 |
let nf1 = func f1 in |

2358 |
if nf1 == f1 then f else gennew (HCLESSPROBFAIL(p, nf1)) |

2359 |
| HCID f1 -> |

2360 |
let nf1 = func f1 in |

2361 |
if nf1 == f1 then f else gennew (HCID(nf1)) |

2362 |
| HCNORM (f1, f2) -> |

2363 |
let nf1 = func f1 in |

2364 |
let nf2 = func f2 in |

2365 |
if nf1 == f1 && nf2 == f2 then f else gennew (HCNORM(nf1, nf2)) |

2366 |
| HCNORMN (f1, f2) -> |

2367 |
let nf1 = func f1 in |

2368 |
let nf2 = func f2 in |

2369 |
if nf1 == f1 && nf2 == f2 then f else gennew (HCNORMN(nf1, nf2)) |

2370 |
| HCCHC (f1, f2) -> |

2371 |
let nf1 = func f1 in |

2372 |
let nf2 = func f2 in |

2373 |
if nf1 == f1 && nf2 == f2 then f else gennew (HCCHC(nf1, nf2)) |

2374 |
| HCFUS (first, f1) -> |

2375 |
let nf1 = func f1 in |

2376 |
if nf1 == f1 then f else gennew (HCFUS(first, nf1)) |

2377 |
| HCMU (var, f1) -> |

2378 |
if compare var name != 0 then |

2379 |
let nf1 = func f1 in |

2380 |
if nf1 == f1 then f else gennew (HCMU(var, nf1)) |

2381 |
else |

2382 |
f |

2383 |
| HCNU (var, f1) -> |

2384 |
if compare var name != 0 then |

2385 |
let nf1 = func f1 in |

2386 |
if nf1 == f1 then f else gennew (HCNU(var, nf1)) |

2387 |
else |

2388 |
f |

2389 | |

2390 |
let rec hc_freeIn variable (f: hcFormula) = |

2391 |
match f.HC.node with |

2392 |
| HCTRUE |

2393 |
| HCFALSE |

2394 |
| HCAP _ |

2395 |
| HCNOT _ |

2396 |
| HCCONST _ |

2397 |
| HCCONSTN _ -> false |

2398 |
| HCVAR s -> |

2399 |
if compare variable s == 0 |

2400 |
then true |

2401 |
else false |

2402 |
| HCAT (s, f1) -> |

2403 |
hc_freeIn variable f1 |

2404 |
| HCOR (f1, f2) |

2405 |
| HCAND (f1, f2) -> |

2406 |
hc_freeIn variable f1 || hc_freeIn variable f2 |

2407 |
| HCEX (_, f1) |

2408 |
| HCAX (_, f1) |

2409 |
| HCENFORCES (_, f1) |

2410 |
| HCALLOWS (_, f1) |

2411 |
| HCMORETHAN (_, _, f1) |

2412 |
| HCMAXEXCEPT (_, _, f1) |

2413 |
| HCATLEASTPROB (_, f1) |

2414 |
| HCLESSPROBFAIL (_, f1) |

2415 |
| HCID f1 -> |

2416 |
hc_freeIn variable f1 |

2417 |
| HCNORM (f1, f2) |

2418 |
| HCNORMN (f1, f2) |

2419 |
| HCCHC (f1, f2) -> |

2420 |
hc_freeIn variable f1 || hc_freeIn variable f2 |

2421 |
| HCFUS (first, f1) -> |

2422 |
hc_freeIn variable f1 |

2423 |
| HCMU (var, f1) |

2424 |
| HCNU (var, f1) -> |

2425 |
(* Do we need to exclude bound variables here? *) |

2426 |
hc_freeIn variable f1 |

2427 | |

2428 | |

2429 |
(** An instantiation of a hash table (of the standard library) |

2430 |
for hash-consed formulae. The test for equality |

2431 |
and computing the hash value is done in constant time. |

2432 |
*) |

2433 |
module HcFHt = Hashtbl.Make( |

2434 |
struct |

2435 |
type t = hcFormula |

2436 |
let equal (f1 : t) f2 = f1.HC.tag = f2.HC.tag |

2437 |
let hash (f : t) = f.HC.tag |

2438 |
end |

2439 |
) |

2440 | |

2441 |
(* vim: set et sw=2 sts=2 ts=8 : *) |