## cool / src / lib / CoAlgFormula.ml @ 1d36cd07

History | View | Annotate | Download (74.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 |
let depthFormula form = |

139 |
let rec depth f = |

140 |
match f with |

141 |
| TRUE |

142 |
| FALSE |

143 |
| AP _ -> 0 |

144 |
| NOT f1 |

145 |
| AT (_, f1) -> (depth f1) |

146 |
| OR (f1, f2) |

147 |
| AND (f1, f2) |

148 |
| EQU (f1, f2) |

149 |
| IMP (f1, f2) -> (max (depth f1)(depth f2)) |

150 |
| EX (_, f1) |

151 |
| AX (_, f1) |

152 |
| ENFORCES (_, f1) |

153 |
| ALLOWS (_, f1) -> succ ((depth f1)) |

154 |
| MIN (_, _, f1) |

155 |
| MAX (_, _, f1) |

156 |
| ATLEASTPROB (_, f1) |

157 |
| LESSPROBFAIL (_, f1) |

158 |
| MORETHAN (_, _, f1) |

159 |
| MAXEXCEPT (_, _, f1) -> succ ((depth f1)) |

160 |
| ID (f1) -> succ ((depth f1)) |

161 |
| NORM(f1, f2) |

162 |
| NORMN(f1, f2) -> succ ((max (depth f1) (depth f2))) |

163 |
| CONST _ |

164 |
| CONSTN _ -> 1 |

165 |
| CHC (f1, f2) -> succ ((max (depth f1) (depth f2))) |

166 |
| FUS (_, f1) -> succ (depth f1) |

167 |
| MU (_, f1) |

168 |
| NU (_, f1) -> depth f1 |

169 |
| VAR _ -> 0 |

170 |
in |

171 |
depth form |

172 | |

173 | |

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

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

176 |
let rec iter func formula = |

177 |
func formula; |

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

179 |
match formula with |

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

181 |
| CONST _ |

182 |
| CONSTN _ -> () |

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

200 | |

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

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

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

204 |
let formula = (match formula with |

205 |
(* 0-ary constructors *) |

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

207 |
| CONST _ |

208 |
| CONSTN _ -> formula |

209 |
(* unary *) |

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

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

212 |
(* binary *) |

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

244 |
in |

245 |
func formula |

246 | |

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

248 |
let helper formula = match formula with |

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

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

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

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

253 |
| TRUE | FALSE |

254 |
| EQU _ | IMP _ |

255 |
| AND _ | OR _ |

256 |
| AP _ | NOT _ |

257 |
| AX _ | EX _ |

258 |
| CHC _ | FUS _ -> formula |

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

260 |
in |

261 |
convert_post helper formula |

262 | |

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

264 |
let helper formula = match formula with |

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

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

267 |
| TRUE | FALSE |

268 |
| EQU _ | IMP _ |

269 |
| AND _ | OR _ |

270 |
| AP _ | NOT _ |

271 |
| CHC _ | FUS _ -> formula |

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

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

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

275 |
in |

276 |
convert_post helper formula |

277 | |

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

279 | |

280 |
let convertToMu formula = |

281 |
let name = Stream.next gensym in |

282 |
let helper formula = |

283 |
match formula with |

284 |
| AF f1 -> |

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

286 |
| EF f1 -> |

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

288 |
| AG f1 -> |

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

290 |
| EG f1 -> |

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

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

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

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

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

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

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

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

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

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

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

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

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

304 |
| _ -> formula |

305 |
in |

306 |
convert_post helper formula |

307 | |

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

309 |
Parentheses are ommited where possible |

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

311 |
@param sb A string buffer. |

312 |
@param f A formula. |

313 |
*) |

314 |
let rec exportFormula_buffer sb f = |

315 |
let negate = function |

316 |
| NOT f -> f |

317 |
| f -> NOT f |

318 |
in |

319 |
let prio n lf = |

320 |
let prionr = function |

321 |
| EQU _ -> 0 |

322 |
| IMP _ -> 1 |

323 |
| OR _ -> 2 |

324 |
| AND _ -> 3 |

325 |
| _ -> 4 |

326 |
in |

327 |
if prionr lf < n then begin |

328 |
Buffer.add_char sb '('; |

329 |
exportFormula_buffer sb lf; |

330 |
Buffer.add_char sb ')' |

331 |
end |

332 |
else exportFormula_buffer sb lf |

333 |
in |

334 |
match f with |

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

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

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

338 |
| NOT f1 -> |

339 |
Buffer.add_string sb "~"; |

340 |
prio 4 f1 |

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

342 |
Buffer.add_string sb "@ "; |

343 |
Buffer.add_string sb s; |

344 |
Buffer.add_string sb " "; |

345 |
prio 4 f1 |

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

347 |
prio 2 f1; |

348 |
Buffer.add_string sb " | "; |

349 |
prio 2 f2 |

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

351 |
prio 3 f1; |

352 |
Buffer.add_string sb " & "; |

353 |
prio 3 f2 |

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

355 |
prio 0 f1; |

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

357 |
prio 0 f2 |

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

359 |
prio 2 f1; |

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

361 |
prio 2 f2 |

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

363 |
Buffer.add_string sb "<"; |

364 |
Buffer.add_string sb s; |

365 |
Buffer.add_string sb ">"; |

366 |
prio 4 f1 |

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

368 |
Buffer.add_string sb "["; |

369 |
Buffer.add_string sb s; |

370 |
Buffer.add_string sb "]"; |

371 |
prio 4 f1 |

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

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

374 |
Buffer.add_string sb ( |

375 |
match s with |

376 |
| [] -> " " |

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

378 |
); |

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

380 |
prio 4 f1 |

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

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

383 |
Buffer.add_string sb ( |

384 |
match s with |

385 |
| [] -> " " |

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

387 |
); |

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

389 |
prio 4 f1 |

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

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

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

393 |
Buffer.add_string sb "}"; |

394 |
prio 4 f1 |

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

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

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

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

399 |
prio 4 f1 |

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

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

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

403 |
Buffer.add_string sb " "; |

404 |
Buffer.add_string sb s; |

405 |
Buffer.add_string sb "}"; |

406 |
prio 4 f1 |

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

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

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

410 |
Buffer.add_string sb " "; |

411 |
Buffer.add_string sb s; |

412 |
Buffer.add_string sb "}"; |

413 |
prio 4 f1 |

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

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

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

417 |
Buffer.add_string sb " "; |

418 |
Buffer.add_string sb s; |

419 |
Buffer.add_string sb "}"; |

420 |
prio 4 f1 |

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

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

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

424 |
Buffer.add_string sb " ~ "; |

425 |
Buffer.add_string sb s; |

426 |
Buffer.add_string sb "}"; |

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

428 |
| ID (f1) -> |

429 |
Buffer.add_string sb "O"; |

430 |
prio 4 f1 |

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

432 |
Buffer.add_string sb "("; |

433 |
exportFormula_buffer sb f1; |

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

435 |
exportFormula_buffer sb f2; |

436 |
Buffer.add_string sb ")" |

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

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

439 |
exportFormula_buffer sb (negate f1); |

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

441 |
exportFormula_buffer sb (negate f2); |

442 |
Buffer.add_string sb ")" |

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

444 |
Buffer.add_string sb "("; |

445 |
exportFormula_buffer sb f1; |

446 |
Buffer.add_string sb " + "; |

447 |
exportFormula_buffer sb f2; |

448 |
Buffer.add_string sb ")" |

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

450 |
Buffer.add_string sb s |

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

452 |
Buffer.add_string sb s |

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

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

455 |
prio 4 f1 |

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

457 |
Buffer.add_string sb "μ"; |

458 |
Buffer.add_string sb s; |

459 |
Buffer.add_string sb "."; |

460 |
prio 4 f1 |

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

462 |
Buffer.add_string sb "ν"; |

463 |
Buffer.add_string sb s; |

464 |
Buffer.add_string sb "."; |

465 |
prio 4 f1 |

466 |
| VAR s -> |

467 |
Buffer.add_string sb s |

468 |
| AF f1 -> |

469 |
Buffer.add_string sb "AF "; |

470 |
prio 4 f1 |

471 |
| EF f1 -> |

472 |
Buffer.add_string sb "EF "; |

473 |
prio 4 f1 |

474 |
| AG f1 -> |

475 |
Buffer.add_string sb "AG "; |

476 |
prio 4 f1 |

477 |
| EG f1 -> |

478 |
Buffer.add_string sb "EG "; |

479 |
prio 4 f1 |

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

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

482 |
prio 4 f1; |

483 |
Buffer.add_string sb " U "; |

484 |
prio 4 f2; |

485 |
Buffer.add_string sb ")" |

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

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

488 |
prio 4 f1; |

489 |
Buffer.add_string sb " U "; |

490 |
prio 4 f2; |

491 |
Buffer.add_string sb ")" |

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

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

494 |
prio 4 f1; |

495 |
Buffer.add_string sb " R "; |

496 |
prio 4 f2; |

497 |
Buffer.add_string sb ")" |

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

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

500 |
prio 4 f1; |

501 |
Buffer.add_string sb " R "; |

502 |
prio 4 f2; |

503 |
Buffer.add_string sb ")" |

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

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

506 |
prio 4 f1; |

507 |
Buffer.add_string sb " B "; |

508 |
prio 4 f2; |

509 |
Buffer.add_string sb ")" |

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

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

512 |
prio 4 f1; |

513 |
Buffer.add_string sb " B "; |

514 |
prio 4 f2; |

515 |
Buffer.add_string sb ")" |

516 | |

517 | |

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

519 |
Parentheses are ommited where possible |

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

521 |
@param f A formula. |

522 |
@return A string representing f. |

523 |
*) |

524 |
let exportFormula f = |

525 |
let sb = Buffer.create 128 in |

526 |
exportFormula_buffer sb f; |

527 |
Buffer.contents sb |

528 | |

529 |
let string_of_formula = exportFormula |

530 | |

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

532 |
let rec exportTatlFormula_buffer sb f = |

533 |
let prio n lf = |

534 |
let prionr = function |

535 |
| EQU _ -> 0 |

536 |
| IMP _ -> 1 |

537 |
| OR _ -> 2 |

538 |
| AND _ -> 3 |

539 |
| _ -> 4 |

540 |
in |

541 |
if prionr lf < n then begin |

542 |
Buffer.add_char sb '('; |

543 |
exportTatlFormula_buffer sb lf; |

544 |
Buffer.add_char sb ')' |

545 |
end |

546 |
else exportTatlFormula_buffer sb lf |

547 |
in |

548 |
match f with |

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

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

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

552 |
| NOT f1 -> |

553 |
Buffer.add_string sb "~"; |

554 |
prio 4 f1 |

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

556 |
prio 2 f1; |

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

558 |
prio 2 f2 |

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

560 |
prio 3 f1; |

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

562 |
prio 3 f2 |

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

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

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

566 |
prio 2 f1; |

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

568 |
prio 2 f2 |

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

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

571 |
Buffer.add_string sb ( |

572 |
match s with |

573 |
| [] -> " " |

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

575 |
); |

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

577 |
prio 4 f1 |

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

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

580 |
Buffer.add_string sb ( |

581 |
match s with |

582 |
| [] -> " " |

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

584 |
); |

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

586 |
prio 4 f1 |

587 |
| EX _ |

588 |
| AX _ |

589 |
| MIN _ |

590 |
| MAX _ |

591 |
| MORETHAN _ |

592 |
| MAXEXCEPT _ |

593 |
| AT _ |

594 |
| CONST _ |

595 |
| CONSTN _ |

596 |
| CHC _ |

597 |
| ATLEASTPROB _ |

598 |
| LESSPROBFAIL _ |

599 |
| ID _ |

600 |
| NORM _ |

601 |
| NORMN _ |

602 |
| FUS _ |

603 |
| MU _ |

604 |
| NU _ |

605 |
| VAR _ |

606 |
| AF _ |

607 |
| EF _ |

608 |
| AG _ |

609 |
| EG _ |

610 |
| AU _ |

611 |
| EU _ |

612 |
| AR _ |

613 |
| ER _ |

614 |
| AB _ |

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

616 | |

617 |
let exportTatlFormula f = |

618 |
let sb = Buffer.create 128 in |

619 |
exportTatlFormula_buffer sb f; |

620 |
Buffer.contents sb |

621 | |

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

623 |
Parentheses are ommited where possible |

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

625 |
@param sb A string buffer. |

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

627 |
*) |

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

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

630 |
Buffer.add_string sb ": "; |

631 |
exportFormula_buffer sb f |

632 | |

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

634 |
Parentheses are ommited where possible |

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

636 |
@param f A sorted formula. |

637 |
@return A string representing f. |

638 |
*) |

639 |
let exportSortedFormula f = |

640 |
let sb = Buffer.create 128 in |

641 |
exportSortedFormula_buffer sb f; |

642 |
Buffer.contents sb |

643 | |

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

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

646 |
@param f A sorted formula. |

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

648 |
*) |

649 |
let exportQuery tbox f = |

650 |
let sb = Buffer.create 1000 in |

651 |
let rec expFl = function |

652 |
| [] -> () |

653 |
| h::tl -> |

654 |
exportSortedFormula_buffer sb h; |

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

656 |
expFl tl |

657 |
in |

658 |
expFl tbox; |

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

660 |
exportSortedFormula_buffer sb f; |

661 |
Buffer.contents sb |

662 | |

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

664 |
coalg can read it again using importQuery |

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

666 |
@param f A sorted formula. |

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

668 |
*) |

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

670 |
let sb = Buffer.create 1000 in |

671 |
let rec expFl = function |

672 |
| [] -> () |

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

674 |
exportFormula_buffer sb h; |

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

676 |
expFl tl |

677 |
in |

678 |
expFl tbox; |

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

680 |
exportFormula_buffer sb f; |

681 |
Buffer.contents sb |

682 | |

683 | |

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

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

686 |
*) |

687 |
let lexer = A.make_lexer |

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

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

690 |
;"μ";"µ";"ν";"." |

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

692 |
] |

693 | |

694 |
let mk_exn s = CoAlgException s |

695 | |

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

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

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

699 |
*) |

700 |
let rec verifyMuAltFree formula = |

701 |
let proc = verifyMuAltFree in |

702 |
match formula with |

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

704 |
| CONST _ |

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

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

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

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

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

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

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

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

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

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

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

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

717 |
else |

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

733 |
else |

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

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

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

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

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

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

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

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

742 |
if newfree = [] then |

743 |
("none", []) |

744 |
else |

745 |
("μ", newfree) |

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

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

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

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

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

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

752 |
if newfree = [] then |

753 |
("none", []) |

754 |
else |

755 |
("ν", newfree) |

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

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

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

759 | |

760 | |

761 |
exception NotAconjunctive of unit |

762 | |

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

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

765 | |

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

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

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

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

770 |
let proc f = verifyMuAconjunctiveInternal f bound_mu_vars in |

771 |
match formula with |

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

773 |
| VAR s -> SS.empty |

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

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

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

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

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

779 | |

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

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

782 |
let a_vars = proc a in |

783 |
let b_vars = proc b in |

784 | |

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

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

787 |
raise (NotAconjunctive ()) |

788 |
else |

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

790 | |

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

792 |
| TRUE | FALSE | AP _ |

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

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

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

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

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

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

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

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

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

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

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

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

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

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

807 |
in |

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

809 |
with NotAconjunctive () -> false |

810 | |

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

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

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

814 |
negations is even. |

815 |
*) |

816 |
let rec verifyMuMonotone negations formula = |

817 |
let proc = verifyMuMonotone negations in |

818 |
match formula with |

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

820 |
| CONST _ |

821 |
| CONSTN _ -> () |

822 |
| AT (_,a) |

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

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

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

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

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

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

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

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

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

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

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

834 |
| MU (s, f) |

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

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

837 |
verifyMuMonotone newNeg f |

838 |
| VAR s -> |

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

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

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

842 |
| NOT a -> |

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

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

845 |
verifyMuMonotone newNeg a |

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

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

848 | |

849 |
let rec verifyMuGuarded unguarded formula = |

850 |
let proc = verifyMuGuarded unguarded in |

851 |
match formula with |

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

853 |
| CONST _ |

854 |
| CONSTN _ -> () |

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

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

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

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

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

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

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

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

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

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

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

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

867 |
| MU (s, f) |

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

869 |
let newUnguard = s :: unguarded in |

870 |
verifyMuGuarded newUnguard f |

871 |
| VAR s -> |

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

873 |
if List.exists finder unguarded then |

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

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

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

877 | |

878 |
let verifyFormula formula = |

879 |
verifyMuAltFree formula; |

880 |
verifyMuMonotone [] formula; |

881 |
verifyMuGuarded [] formula |

882 | |

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

884 |
It is a standard recursive descent procedure. |

885 |
@param ts A token stream. |

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

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

888 |
*) |

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

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

891 |
let f1 = convertToMu formula in |

892 |
match Stream.peek ts with |

893 |
| None -> f1 |

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

895 |
Stream.junk ts; |

896 |
let f2 = parse_formula symtab ts in |

897 |
EQU (f1, f2) |

898 |
| _ -> f1 |

899 | |

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

901 |
It is a standard recursive descent procedure. |

902 |
@param ts A token stream. |

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

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

905 |
*) |

906 |
and parse_imp symtab ts= |

907 |
let f1 = parse_or symtab ts in |

908 |
match Stream.peek ts with |

909 |
| None -> f1 |

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

911 |
Stream.junk ts; |

912 |
let f2 = parse_imp symtab ts in |

913 |
IMP (f1, f2) |

914 |
| _ -> f1 |

915 | |

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

917 |
It is a standard recursive descent procedure. |

918 |
@param ts A token stream. |

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

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

921 |
*) |

922 |
and parse_or symtab ts = |

923 |
let f1 = parse_and symtab ts in |

924 |
match Stream.peek ts with |

925 |
| None -> f1 |

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

927 |
Stream.junk ts; |

928 |
let f2 = parse_or symtab ts in |

929 |
OR (f1, f2) |

930 |
| _ -> f1 |

931 | |

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

933 |
It is a standard recursive descent procedure. |

934 |
@param ts A token stream. |

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

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

937 |
*) |

938 |
and parse_and symtab ts = |

939 |
let f1 = parse_cimp symtab ts in |

940 |
match Stream.peek ts with |

941 |
| None -> f1 |

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

943 |
Stream.junk ts; |

944 |
let f2 = parse_and symtab ts in |

945 |
AND (f1, f2) |

946 |
| _ -> f1 |

947 | |

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

949 |
It is a standard recursive descent procedure. |

950 |
@param ts A token stream. |

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

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

953 |
*) |

954 |
and parse_cimp symtab ts = |

955 |
let f1 = parse_rest symtab ts in |

956 |
match Stream.peek ts with |

957 |
| None -> f1 |

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

959 |
Stream.junk ts; |

960 |
let f2 = parse_cimp symtab ts in |

961 |
NORM (f1, f2) |

962 |
| _ -> f1 |

963 | |

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

965 |
It is a standard recursive descent procedure. |

966 |
@param ts A token stream. |

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

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

969 |
*) |

970 |
and parse_rest symtab ts = |

971 |
let boxinternals noNo es = |

972 |
let n = |

973 |
if noNo then 0 |

974 |
else |

975 |
match Stream.next ts with |

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

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

978 |
in |

979 |
let (s,denominator) = |

980 |
match Stream.peek ts with |

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

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

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

984 |
Stream.junk ts; |

985 |
match Stream.next ts with |

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

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

988 |
end |

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

990 |
in |

991 |
if (denominator < n) then begin |

992 |
let explanation = |

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

994 |
in |

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

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

997 |
) |

998 |
end; |

999 |
let _ = |

1000 |
match Stream.next ts with |

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

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

1003 |
in |

1004 |
(n, denominator, s) |

1005 |
in |

1006 |
let rec agentlist es = |

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

1008 |
match Stream.next ts with |

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

1010 |
then n::(agentlist es) |

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

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

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

1014 |
in |

1015 |
match Stream.next ts with |

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

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

1018 |
AP "true" |

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

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

1021 |
AP "false" |

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

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

1024 |
| A.Ident s -> |

1025 |
(try |

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

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

1028 |
VAR symbol |

1029 |
with Not_found -> AP s) |

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

1031 |
let f = parse_rest symtab ts in |

1032 |
NOT f |

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

1034 |
let s = |

1035 |
match Stream.next ts with |

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

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

1038 |
in |

1039 |
let f = parse_rest symtab ts in |

1040 |
AT (s, f) |

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

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

1043 |
let f1 = parse_rest symtab ts in |

1044 |
EX (s, f1) |

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

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

1047 |
let f1 = parse_rest symtab ts in |

1048 |
AX (s, f1) |

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

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

1051 |
let f1 = parse_rest symtab ts in |

1052 |
ENFORCES (ls, f1) |

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

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

1055 |
let f1 = parse_rest symtab ts in |

1056 |
ALLOWS (ls, f1) |

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

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

1059 |
let f1 = parse_rest symtab ts in |

1060 |
if (denom <> 0) |

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

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

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

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

1065 |
let f1 = parse_rest symtab ts in |

1066 |
if (denom <> 0) |

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

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

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

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

1071 |
let f1 = parse_rest symtab ts in |

1072 |
if (denom <> 0) |

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

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

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

1076 |
match Stream.next ts with |

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

1078 |
| A.Kwd s |

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

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

1081 |
end |

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

1083 |
let f = parse_formula symtab ts in |

1084 |
match Stream.next ts with |

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

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

1087 |
let f2 = parse_formula symtab ts in |

1088 |
match Stream.next ts with |

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

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

1091 |
end |

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

1093 |
end |

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

1095 |
let f = parse_rest symtab ts in |

1096 |
ID f |

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

1098 |
let f = parse_rest symtab ts in |

1099 |
FUS (true, f) |

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

1101 |
let f = parse_rest symtab ts in |

1102 |
FUS (false, f) |

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

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

1105 |
let symbol = Stream.next gensym in |

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

1107 |
let f1 = parse_rest newtab ts in |

1108 |
MU (symbol, f1) |

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

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

1111 |
let symbol = Stream.next gensym in |

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

1113 |
let f1 = parse_rest newtab ts in |

1114 |
NU (symbol, f1) |

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

1116 |
let f = parse_rest symtab ts in |

1117 |
AF f |

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

1119 |
let f = parse_rest symtab ts in |

1120 |
EF f |

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

1122 |
let f = parse_rest symtab ts in |

1123 |
AG f |

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

1125 |
let f = parse_rest symtab ts in |

1126 |
EG f |

1127 |
| A.Kwd "A" -> |

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

1129 |
let f1 = parse_formula symtab ts in begin |

1130 |
match Stream.next ts with |

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

1132 |
let f2 = parse_formula symtab ts in |

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

1134 |
AU (f1, f2) |

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

1136 |
let f2 = parse_formula symtab ts in |

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

1138 |
AR (f1, f2) |

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

1140 |
let f2 = parse_formula symtab ts in |

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

1142 |
AB (f1, f2) |

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

1144 |
end |

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

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

1147 |
let f1 = parse_formula symtab ts in begin |

1148 |
match Stream.next ts with |

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

1150 |
let f2 = parse_formula symtab ts in |

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

1152 |
EU (f1, f2) |

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

1154 |
let f2 = parse_formula symtab ts in |

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

1156 |
ER (f1, f2) |

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

1158 |
let f2 = parse_formula symtab ts in |

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

1160 |
EB (f1, f2) |

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

1162 |
end |

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

1164 |
let f1 = parse_rest symtab ts in |

1165 |
AX ("", f1) |

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

1167 |
let f1 = parse_rest symtab ts in |

1168 |
EX ("", f1) |

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

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

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

1172 | |

1173 |
(** Parses a sorted formula. |

1174 |
@param ts A token stream. |

1175 |
@return A sorted formula. |

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

1177 |
*) |

1178 |
let parse_sortedFormula ts = |

1179 |
let nr = |

1180 |
match Stream.peek ts with |

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

1182 |
if n >= 0 then begin |

1183 |
Stream.junk ts; |

1184 |
let () = |

1185 |
match Stream.next ts with |

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

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

1188 |
in |

1189 |
n |

1190 |
end else |

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

1192 |
| _ -> 0 |

1193 |
in |

1194 |
let f = parse_formula [] ts in |

1195 |
(nr, f) |

1196 | |

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

1198 |
@param ts A token stream. |

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

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

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

1202 |
*) |

1203 |
let rec parse_sortedFormulaList ts acc = |

1204 |
let f1 = parse_sortedFormula ts in |

1205 |
match Stream.peek ts with |

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

1207 |
Stream.junk ts; |

1208 |
parse_sortedFormulaList ts (f1::acc) |

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

1210 | |

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

1212 |
@param fkt An import function. |

1213 |
@param s A string. |

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

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

1216 |
*) |

1217 |
let importWrapper fkt s = |

1218 |
let ts = lexer s in |

1219 |
try |

1220 |
let res = fkt ts in |

1221 |
let _ = |

1222 |
match Stream.peek ts with |

1223 |
| None -> () |

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

1225 |
in |

1226 |
res |

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

1228 | |

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

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

1231 |
@return The resulting formula. |

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

1233 |
*) |

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

1235 | |

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

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

1238 |
@return The sorted formula. |

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

1240 |
*) |

1241 |
let importSortedFormula s = importWrapper parse_sortedFormula s |

1242 | |

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

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

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

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

1247 |
f is a sorted formula. |

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

1249 |
*) |

1250 |
let importQuery s = |

1251 |
let fkt ts = |

1252 |
match Stream.peek ts with |

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

1254 |
Stream.junk ts; |

1255 |
let f = parse_sortedFormula ts in |

1256 |
([], f) |

1257 |
| _ -> |

1258 |
let fl = parse_sortedFormulaList ts [] in |

1259 |
match Stream.peek ts with |

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

1261 |
Stream.junk ts; |

1262 |
let f = parse_sortedFormula ts in |

1263 |
(fl, f) |

1264 |
| _ -> |

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

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

1267 |
in |

1268 |
importWrapper fkt s |

1269 | |

1270 | |

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

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

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

1274 |
@param f A formula. |

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

1276 |
that is equivalent to ~f. |

1277 |
*) |

1278 | |

1279 |
let rec equals f_1 f_2 = |

1280 |
match f_1, f_2 with |

1281 |
| TRUE, TRUE -> true |

1282 |
| FALSE, FALSE -> true |

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

1310 |
| _ -> false |

1311 | |

1312 | |

1313 |
let rec nnfNeg f = |

1314 |
match f with |

1315 |
| TRUE -> FALSE |

1316 |
| FALSE -> TRUE |

1317 |
| AP _ -> NOT f |

1318 |
| VAR _ -> f |

1319 |
| NOT f1 -> nnf f1 |

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

1335 |
| CONST s -> CONSTN s |

1336 |
| CONSTN s -> CONST s |

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

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

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

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

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

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

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

1344 |
| AF _ | EF _ |

1345 |
| AG _ | EG _ |

1346 |
| AU _ | EU _ |

1347 |
| AR _ | ER _ |

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

1349 | |

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

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

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

1353 |
@param f A formula. |

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

1355 |
that is equivalent to f. |

1356 |
*) |

1357 |
and nnf f = |

1358 |
match f with |

1359 |
| TRUE |

1360 |
| FALSE |

1361 |
| AP _ |

1362 |
| NOT (AP _) |

1363 |
| CONST _ |

1364 |
| CONSTN _ |

1365 |
| VAR _ -> f |

1366 |
| NOT f1 -> nnfNeg f1 |

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

1368 |
let ft1 = nnf f1 in |

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

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

1371 |
let ft1 = nnf f1 in |

1372 |
let ft2 = nnf f2 in |

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

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

1375 |
let ft1 = nnf f1 in |

1376 |
let ft2 = nnf f2 in |

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

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

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

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

1381 |
let ft = nnf f1 in |

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

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

1384 |
let ft = nnf f1 in |

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

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

1387 |
let ft = nnf f1 in |

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

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

1390 |
let ft = nnf f1 in |

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

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

1393 |
if n = 0 then TRUE |

1394 |
else |

1395 |
let ft = nnf f1 in |

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

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

1398 |
let ft = nnfNeg f1 in |

1399 |
MAXEXCEPT (n,s, ft) |

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

1401 |
let ft = nnf f1 in |

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

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

1404 |
let ft = nnf f1 in |

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

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

1407 |
let ft = nnf f1 in |

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

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

1410 |
let ft = nnf f1 in |

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

1412 |
| ID (f1) -> |

1413 |
let ft = nnf f1 in |

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

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

1416 |
let ft1 = nnf f1 in |

1417 |
let ft2 = nnf f2 in |

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

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

1420 |
let ft1 = nnf f1 in |

1421 |
let ft2 = nnf f2 in |

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

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

1424 |
let ft1 = nnf f1 in |

1425 |
let ft2 = nnf f2 in |

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

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

1428 |
let ft = nnf f1 in |

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

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

1431 |
let ft = nnf f1 in |

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

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

1434 |
let ft = nnf f1 in |

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

1436 |
| AF _ | EF _ |

1437 |
| AG _ | EG _ |

1438 |
| AU _ | EU _ |

1439 |
| AR _ | ER _ |

1440 |
| AB _ | EB _ -> |

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

1442 | |

1443 |
(** Simplifies a formula. |

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

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

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

1447 |
*) |

1448 |
let rec simplify f = |

1449 |
match f with |

1450 |
| TRUE |

1451 |
| FALSE |

1452 |
| AP _ |

1453 |
| NOT (AP _) |

1454 |
| VAR _ |

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

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

1457 |
let ft = simplify f1 in |

1458 |
begin |

1459 |
match ft with |

1460 |
| FALSE -> FALSE |

1461 |
| TRUE -> TRUE |

1462 |
| AT _ -> ft |

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

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

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

1466 |
end |

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

1468 |
let ft1 = simplify f1 in |

1469 |
let ft2 = simplify f2 in |

1470 |
begin |

1471 |
match ft1, ft2 with |

1472 |
| TRUE, _ -> TRUE |

1473 |
| FALSE, _ -> ft2 |

1474 |
| _, TRUE -> TRUE |

1475 |
| _, FALSE -> ft1 |

1476 |
| _, _ -> |

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

1478 |
else OR (ft1, ft2) |

1479 |
end |

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

1481 |
let ft1 = simplify f1 in |

1482 |
let ft2 = simplify f2 in |

1483 |
begin |

1484 |
match ft1, ft2 with |

1485 |
| TRUE, _ -> ft2 |

1486 |
| FALSE, _ -> FALSE |

1487 |
| _, TRUE -> ft1 |

1488 |
| _, FALSE -> FALSE |

1489 |
| _, _ -> |

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

1491 |
else AND (ft1, ft2) |

1492 |
end |

1493 |
| NOT _ |

1494 |
| EQU _ |

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

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

1497 |
let ft = simplify f1 in |

1498 |
begin |

1499 |
match ft with |

1500 |
| FALSE -> FALSE |

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

1502 |
end |

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

1504 |
let ft = simplify f1 in |

1505 |
begin |

1506 |
match ft with |

1507 |
| TRUE -> TRUE |

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

1509 |
end |

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

1511 |
let ft = simplify f1 in |

1512 |
begin |

1513 |
match ft with |

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

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

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

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

1518 |
*) |

1519 |
| TRUE -> TRUE |

1520 |
| FALSE -> FALSE |

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

1522 |
end |

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

1524 |
let ft = simplify f1 in |

1525 |
begin |

1526 |
match ft with |

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

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

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

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

1531 |
*) |

1532 |
| TRUE -> TRUE |

1533 |
| FALSE -> FALSE |

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

1535 |
end |

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

1537 |
if n = 0 then TRUE |

1538 |
else |

1539 |
let ft = simplify f1 in |

1540 |
begin |

1541 |
match ft with |

1542 |
| FALSE -> FALSE |

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

1544 |
end |

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

1546 |
let ft = simplify f1 in |

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

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

1549 |
let ft = simplify f1 in |

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

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

1552 |
let ft = simplify f1 in |

1553 |
begin |

1554 |
match ft with |

1555 |
| FALSE -> TRUE |

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

1557 |
end |

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

1559 |
let ft1 = simplify f1 in |

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

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

1562 |
let ft1 = simplify f1 in |

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

1564 |
| CONST _ |

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

1566 |
| ID (f1) -> |

1567 |
let ft1 = simplify f1 in |

1568 |
begin |

1569 |
match ft1 with |

1570 |
| TRUE -> TRUE |

1571 |
| FALSE -> FALSE |

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

1573 |
end |

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

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

1576 |
let ft1 = simplify f1 in |

1577 |
let ft2 = simplify f2 in |

1578 |
begin |

1579 |
match ft2 with |

1580 |
| TRUE -> TRUE |

1581 |
| _ -> |

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

1583 |
else NORM (ft1, ft2) |

1584 |
end |

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

1586 |
let ft1 = simplify f1 in |

1587 |
let ft2 = simplify f2 in |

1588 |
begin |

1589 |
match ft2 with |

1590 |
| FALSE -> FALSE |

1591 |
| _ -> |

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

1593 |
else NORMN (ft1, ft2) |

1594 |
end |

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

1596 |
let ft1 = simplify f1 in |

1597 |
let ft2 = simplify f2 in |

1598 |
begin |

1599 |
match ft1, ft2 with |

1600 |
| TRUE, TRUE -> TRUE |

1601 |
| FALSE, FALSE -> FALSE |

1602 |
| _, _ -> |

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

1604 |
else CHC (ft1, ft2) |

1605 |
end |

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

1607 |
let ft = simplify f1 in |

1608 |
begin |

1609 |
match ft with |

1610 |
| FALSE -> FALSE |

1611 |
| TRUE -> TRUE |

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

1613 |
end |

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

1615 |
let ft = simplify f1 in |

1616 |
begin |

1617 |
match ft with |

1618 |
| TRUE -> TRUE |

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

1620 |
end |

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

1622 |
let ft = simplify f1 in |

1623 |
begin |

1624 |
match ft with |

1625 |
| TRUE -> TRUE |

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

1627 |
end |

1628 |
| AF _ | EF _ |

1629 |
| AG _ | EG _ |

1630 |
| AU _ | EU _ |

1631 |
| AR _ | ER _ |

1632 |
| AB _ | EB _ -> |

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

1634 | |

1635 |
(** Destructs an atomic proposition. |

1636 |
@param f An atomic proposition. |

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

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

1639 |
*) |

1640 |
let dest_ap f = |

1641 |
match f with |

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

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

1644 | |

1645 |
(** Destructs a nominal. |

1646 |
@param f A nominal. |

1647 |
@return The name of the nominal |

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

1649 |
*) |

1650 |
let dest_nom f = |

1651 |
match f with |

1652 |
| AP s when isNominal s -> s |

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

1654 | |

1655 |
(** Destructs a negation. |

1656 |
@param f A negation. |

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

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

1659 |
*) |

1660 |
let dest_not f = |

1661 |
match f with |

1662 |
| NOT f1 -> f1 |

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

1664 | |

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

1666 |
@param f An @-formula. |

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

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

1669 |
*) |

1670 |
let dest_at f = |

1671 |
match f with |

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

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

1674 | |

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

1676 |
@param f An or-formula. |

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

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

1679 |
*) |

1680 |
let dest_or f = |

1681 |
match f with |

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

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

1684 | |

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

1686 |
@param f An and-formula. |

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

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

1689 |
*) |

1690 |
let dest_and f = |

1691 |
match f with |

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

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

1694 | |

1695 |
(** Destructs an equivalence. |

1696 |
@param f An equivalence. |

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

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

1699 |
*) |

1700 |
let dest_equ f = |

1701 |
match f with |

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

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

1704 | |

1705 |
(** Destructs an implication. |

1706 |
@param f An implication. |

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

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

1709 |
*) |

1710 |
let dest_imp f = |

1711 |
match f with |

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

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

1714 | |

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

1716 |
@param f An EX-formula. |

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

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

1719 |
*) |

1720 |
let dest_ex f = |

1721 |
match f with |

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

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

1724 | |

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

1726 |
@param f An AX-formula. |

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

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

1729 |
*) |

1730 |
let dest_ax f = |

1731 |
match f with |

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

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

1734 | |

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

1736 |
@param f A MIN-formula. |

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

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

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

1740 |
*) |

1741 |
let dest_min f = |

1742 |
match f with |

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

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

1745 | |

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

1747 |
@param f A MAX-formula. |

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

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

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

1751 |
*) |

1752 |
let dest_max f = |

1753 |
match f with |

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

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

1756 | |

1757 |
(** Destructs a choice formula. |

1758 |
@param f A choice formula. |

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

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

1761 |
*) |

1762 |
let dest_choice f = |

1763 |
match f with |

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

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

1766 | |

1767 |
(** Destructs a fusion formula. |

1768 |
@param f A fusion formula. |

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

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

1771 |
f1 is the immediate subformulae of f. |

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

1773 |
*) |

1774 |
let dest_fusion f = |

1775 |
match f with |

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

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

1778 | |

1779 | |

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

1781 |
@param f A formula. |

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

1783 |
*) |

1784 |
let is_true f = |

1785 |
match f with |

1786 |
| TRUE -> true |

1787 |
| _ -> false |

1788 | |

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

1790 |
@param f A formula. |

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

1792 |
*) |

1793 |
let is_false f = |

1794 |
match f with |

1795 |
| FALSE -> true |

1796 |
| _ -> false |

1797 | |

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

1799 |
@param f A formula. |

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

1801 |
*) |

1802 |
let is_ap f = |

1803 |
match f with |

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

1805 |
| _ -> false |

1806 | |

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

1808 |
@param f A formula. |

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

1810 |
*) |

1811 |
let is_nom f = |

1812 |
match f with |

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

1814 |
| _ -> false |

1815 | |

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

1817 |
@param f A formula. |

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

1819 |
*) |

1820 |
let is_not f = |

1821 |
match f with |

1822 |
| NOT _ -> true |

1823 |
| _ -> false |

1824 | |

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

1826 |
@param f A formula. |

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

1828 |
*) |

1829 |
let is_at f = |

1830 |
match f with |

1831 |
| AT _ -> true |

1832 |
| _ -> false |

1833 | |

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

1835 |
@param f A formula. |

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

1837 |
*) |

1838 |
let is_or f = |

1839 |
match f with |

1840 |
| OR _ -> true |

1841 |
| _ -> false |

1842 | |

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

1844 |
@param f A formula. |

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

1846 |
*) |

1847 |
let is_and f = |

1848 |
match f with |

1849 |
| AND _ -> true |

1850 |
| _ -> false |

1851 | |

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

1853 |
@param f A formula. |

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

1855 |
*) |

1856 |
let is_equ f = |

1857 |
match f with |

1858 |
| EQU _ -> true |

1859 |
| _ -> false |

1860 | |

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

1862 |
@param f A formula. |

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

1864 |
*) |

1865 |
let is_imp f = |

1866 |
match f with |

1867 |
| IMP _ -> true |

1868 |
| _ -> false |

1869 | |

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

1871 |
@param f A formula. |

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

1873 |
*) |

1874 |
let is_ex f = |

1875 |
match f with |

1876 |
| EX _ -> true |

1877 |
| _ -> false |

1878 | |

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

1880 |
@param f A formula. |

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

1882 |
*) |

1883 |
let is_ax f = |

1884 |
match f with |

1885 |
| AX _ -> true |

1886 |
| _ -> false |

1887 | |

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

1889 |
@param f A formula. |

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

1891 |
*) |

1892 |
let is_min f = |

1893 |
match f with |

1894 |
| MIN _ -> true |

1895 |
| _ -> false |

1896 | |

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

1898 |
@param f A formula. |

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

1900 |
*) |

1901 |
let is_max f = |

1902 |
match f with |

1903 |
| MAX _ -> true |

1904 |
| _ -> false |

1905 | |

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

1907 |
@param f A formula. |

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

1909 |
*) |

1910 |
let is_choice f = |

1911 |
match f with |

1912 |
| CHC _ -> true |

1913 |
| _ -> false |

1914 | |

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

1916 |
@param f A formula. |

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

1918 |
*) |

1919 |
let is_fusion f = |

1920 |
match f with |

1921 |
| FUS _ -> true |

1922 |
| _ -> false |

1923 | |

1924 | |

1925 |
(** The constant True. |

1926 |
*) |

1927 |
let const_true = TRUE |

1928 | |

1929 |
(** The constant False. |

1930 |
*) |

1931 |
let const_false = FALSE |

1932 | |

1933 |
(** Constructs an atomic proposition. |

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

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

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

1937 |
*) |

1938 |
let const_ap s = |

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

1940 |
else AP s |

1941 | |

1942 |
(** Constructs a nominal. |

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

1944 |
@return A nominal with name s. |

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

1946 |
*) |

1947 |
let const_nom s = |

1948 |
if isNominal s then AP s |

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

1950 | |

1951 |
(** Negates a formula. |

1952 |
@param f A formula. |

1953 |
@return The negation of f. |

1954 |
*) |

1955 |
let const_not f = NOT f |

1956 | |

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

1958 |
@param s A nominal name. |

1959 |
@param f A formula. |

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

1961 |
*) |

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

1963 | |

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

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

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

1967 |
@return The formula f1 | f2. |

1968 |
*) |

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

1970 | |

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

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

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

1974 |
@return The formula f1 & f2. |

1975 |
*) |

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

1977 | |

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

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

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

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

1982 |
*) |

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

1984 | |

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

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

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

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

1989 |
*) |

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

1991 | |

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

1993 |
@param s A role name. |

1994 |
@param f A formula. |

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

1996 |
*) |

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

1998 | |

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

2000 |
@param s A role name. |

2001 |
@param f A formula. |

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

2003 |
*) |

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

2005 | |

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

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

2008 |
@param s A role name. |

2009 |
@param f A formula. |

2010 |
@return The formula MIN f. |

2011 |
@raise CoAlgException Iff n is negative. |

2012 |
*) |

2013 |
let const_min n s f = |

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

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

2016 | |

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

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

2019 |
@param s A role name. |

2020 |
@param f A formula. |

2021 |
@return The formula MAX f. |

2022 |
@raise CoAlgException Iff n is negative. |

2023 |
*) |

2024 |
let const_max n s f = |

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

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

2027 | |

2028 |
let const_enforces p f = |

2029 |
ENFORCES (p,f) |

2030 | |

2031 |
let const_allows p f = |

2032 |
ALLOWS (p,f) |

2033 | |

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

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

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

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

2038 |
*) |

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

2040 | |

2041 |
(** Constructs a fusion formula. |

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

2043 |
@param f1 A formula. |

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

2045 |
*) |

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

2047 | |

2048 | |

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

2050 |
such that structural and physical equality coincide. |

2051 | |

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

2053 |
constructs |

2054 |
*) |

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

2056 |
and hcFormula_node = |

2057 |
| HCTRUE |

2058 |
| HCFALSE |

2059 |
| HCAP of string |

2060 |
| HCNOT of string |

2061 |
| HCAT of string * hcFormula |

2062 |
| HCOR of hcFormula * hcFormula |

2063 |
| HCAND of hcFormula * hcFormula |

2064 |
| HCEX of string * hcFormula |

2065 |
| HCAX of string * hcFormula |

2066 |
| HCENFORCES of int list * hcFormula |

2067 |
| HCALLOWS of int list * hcFormula |

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

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

2070 |
| HCATLEASTPROB of rational * hcFormula |

2071 |
| HCLESSPROBFAIL of rational * hcFormula |

2072 |
| HCCONST of string |

2073 |
| HCCONSTN of string |

2074 |
| HCID of hcFormula |

2075 |
| HCNORM of hcFormula * hcFormula |

2076 |
| HCNORMN of hcFormula * hcFormula |

2077 |
| HCCHC of hcFormula * hcFormula |

2078 |
| HCFUS of bool * hcFormula |

2079 |
| HCMU of string * hcFormula |

2080 |
| HCNU of string * hcFormula |

2081 |
| HCVAR of string |

2082 | |

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

2084 |
@param f1 The first formula node. |

2085 |
@param f2 The second formula node. |

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

2087 |
*) |

2088 |
let equal_hcFormula_node f1 f2 = |

2089 |
match f1, f2 with |

2090 |
| HCTRUE, HCTRUE -> true |

2091 |
| HCFALSE, HCFALSE -> true |

2092 |
| HCCONST s1, HCCONST s2 |

2093 |
| HCCONSTN s1, HCCONSTN s2 |

2094 |
| HCAP s1, HCAP s2 |

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

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

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

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

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

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

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

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

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

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

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

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

2107 |
p1 = p2 && f1 == f2 |

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

2109 |
p1 = p2 && f1 == f2 |

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

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

2112 |
| HCCHC (f1a, f1b), HCCHC (f2a, f2b) -> f1a == f2a && f1b == f2b |

2113 |
| HCFUS (first1, f1), HCFUS (first2, f2) -> first1 = first2 && f1 == f2 |

2114 |
| HCMU (name1, f1), HCMU(name2, f2) -> compare name1 name2 = 0 && f1 == f2 |

2115 |
| HCNU (name1, f1), HCNU(name2, f2) -> compare name1 name2 = 0 && f1 == f2 |

2116 |
| HCVAR name1, HCVAR name2 -> compare name1 name2 = 0 |

2117 |
(* The rest could be shortened to | _ -> false, |

2118 |
but then the compiler would not warn if the formula type is extended |

2119 |
and this function is not updated accordingly.*) |

2120 |
| HCTRUE, _ |

2121 |
| HCFALSE, _ |

2122 |
| HCAP _, _ |

2123 |
| HCNOT _, _ |

2124 |
| HCAT _, _ |

2125 |
| HCOR _, _ |

2126 |
| HCAND _, _ |

2127 |
| HCEX _, _ |

2128 |
| HCAX _, _ |

2129 |
| HCENFORCES _, _ |

2130 |
| HCALLOWS _, _ |

2131 |
| HCMORETHAN _, _ |

2132 |
| HCMAXEXCEPT _, _ |

2133 |
| HCATLEASTPROB _, _ |

2134 |
| HCLESSPROBFAIL _, _ |

2135 |
| HCCONST _, _ |

2136 |
| HCCONSTN _, _ |

2137 |
| HCID _, _ |

2138 |
| HCNORM _, _ |

2139 |
| HCNORMN _, _ |

2140 |
| HCCHC _, _ |

2141 |
| HCFUS _, _ |

2142 |
| HCMU _, _ |

2143 |
| HCNU _, _ |

2144 |
| HCVAR _, _ -> false |

2145 | |

2146 |
(** Computes the hash value of a formula node. |

2147 |
@param f A formula node. |

2148 |
@return The hash value of f. |

2149 |
*) |

2150 |
let hash_hcFormula_node f = |

2151 |
let base = 23 in (* should be larger than the no of constructors *) |

2152 |
match f with |

2153 |
| HCTRUE -> 0 |

2154 |
| HCFALSE -> 1 |

2155 |
| HCAP s |

2156 |
| HCNOT s |

2157 |
| HCVAR s -> base * Hashtbl.hash s + 1 |

2158 |
| HCAT (s, f1) -> base * (base * (Hashtbl.hash s) + f1.HC.hkey) + 2 |

2159 |
| HCOR (f1, f2) -> base * (base * f1.HC.hkey + f2.HC.hkey) + 5 |

2160 |
| HCAND (f1, f2) -> base * (base * f1.HC.hkey + f2.HC.hkey) + 6 |

2161 |
| HCEX (s, f1) -> base * (base * (Hashtbl.hash s) + f1.HC.hkey) + 3 |

2162 |
| HCAX (s, f1) -> base * (base * (Hashtbl.hash s) + f1.HC.hkey) + 4 |

2163 |
| HCMORETHAN (n, s, f1) -> base * (base * (base * (Hashtbl.hash s) + n) + f1.HC.hkey) + 7 |

2164 |
| HCMAXEXCEPT (n, s, f1) -> base * (base * (base * (Hashtbl.hash s) + n) + f1.HC.hkey) + 8 |

2165 |
| HCATLEASTPROB (p,f1) -> base * (base * (base * p.nominator + p.denominator) + f1.HC.hkey) + 9 |

2166 |
| HCLESSPROBFAIL (p,f1) -> base * (base * (base * p.nominator + p.denominator) + f1.HC.hkey) + 10 |

2167 |
| HCCHC (f1, f2) -> base * (base * f1.HC.hkey + f2.HC.hkey) + 11 |

2168 |
| HCFUS (first, f1) -> base * (base * (Hashtbl.hash first) + f1.HC.hkey) + 13 |

2169 |
| HCENFORCES (s, f1) -> base * (base * (Hashtbl.hash s) + f1.HC.hkey) + 14 |

2170 |
| HCALLOWS (s, f1) -> base * (base * (Hashtbl.hash s) + f1.HC.hkey) + 15 |

2171 |
| HCCONST s -> Hashtbl.hash s + 16 |

2172 |
| HCCONSTN s -> Hashtbl.hash s + 17 |

2173 |
| HCNORM (f1, f2) -> base * (base * f1.HC.hkey + f2.HC.hkey) + 18 |

2174 |
| HCNORMN (f1, f2) -> base * (base * f1.HC.hkey + f2.HC.hkey) + 19 |

2175 |
| HCID (f1) -> base * f1.HC.hkey + 20 |

2176 |
| HCMU (s, f1) -> base * (base * (Hashtbl.hash s) + f1.HC.hkey) + 21 |

2177 |
| HCNU (s, f1) -> base * (base * (Hashtbl.hash s) + f1.HC.hkey) + 22 |

2178 | |

2179 |
(** Determines the "real" formula of a formula node. |

2180 |
@param f A formula node. |

2181 |
@return The formula (in negation normal form) which corresponds to f. |

2182 |
*) |

2183 |
let toFml_hcFormula_node f = |

2184 |
match f with |

2185 |
| HCTRUE -> TRUE |

2186 |
| HCFALSE -> FALSE |

2187 |
| HCAP s -> AP s |

2188 |
| HCVAR s -> VAR s |

2189 |
| HCNOT s -> NOT (AP s) |

2190 |
| HCAT (s, f1) -> AT (s, f1.HC.fml) |

2191 |
| HCOR (f1, f2) -> OR (f1.HC.fml, f2.HC.fml) |

2192 |
| HCAND (f1, f2) -> AND (f1.HC.fml, f2.HC.fml) |

2193 |
| HCEX (s, f1) -> EX (s, f1.HC.fml) |

2194 |
| HCAX (s, f1) -> AX (s, f1.HC.fml) |

2195 |
| HCENFORCES (s, f1) -> ENFORCES (s, f1.HC.fml) |

2196 |
| HCALLOWS (s, f1) -> ALLOWS (s, f1.HC.fml) |

2197 |
| HCMORETHAN (n, s, f1) -> MORETHAN (n, s, f1.HC.fml) |

2198 |
| HCMAXEXCEPT (n, s, f1) -> MAXEXCEPT (n, s, f1.HC.fml) |

2199 |
| HCATLEASTPROB (p, f1) -> ATLEASTPROB (p, f1.HC.fml) |

2200 |
| HCLESSPROBFAIL (p, f1) -> LESSPROBFAIL (p, f1.HC.fml) |

2201 |
| HCCONST s -> CONST s |

2202 |
| HCCONSTN s -> CONSTN s |

2203 |
| HCID (f1) -> ID(f1.HC.fml) |

2204 |
| HCNORM (f1, f2) -> NORM(f1.HC.fml, f2.HC.fml) |

2205 |
| HCNORMN (f1, f2) -> NORMN(f1.HC.fml, f2.HC.fml) |

2206 |
| HCCHC (f1, f2) -> CHC (f1.HC.fml, f2.HC.fml) |

2207 |
| HCFUS (first, f1) -> FUS (first, f1.HC.fml) |

2208 |
| HCMU (var, f1) -> MU (var, f1.HC.fml) |

2209 |
| HCNU (var, f1) -> NU (var, f1.HC.fml) |

2210 | |

2211 |
(** Determines the negation (in negation normal form) of a formula node. |

2212 |
@param f A formula node. |

2213 |
@return The negation (in negation normal form) of f. |

2214 |
*) |

2215 |
let negNde_hcFormula_node f = |

2216 |
match f with |

2217 |
| HCTRUE -> HCFALSE |

2218 |
| HCFALSE -> HCTRUE |

2219 |
| HCAP s -> HCNOT s |

2220 |
| HCNOT s -> HCAP s |

2221 |
| HCVAR s -> f |

2222 |
| HCAT (s, f1) -> HCAT (s, f1.HC.neg) |

2223 |
| HCOR (f1, f2) -> HCAND (f1.HC.neg, f2.HC.neg) |

2224 |
| HCAND (f1, f2) -> HCOR (f1.HC.neg, f2.HC.neg) |

2225 |
| HCEX (s, f2) -> HCAX (s, f2.HC.neg) |

2226 |
| HCAX (s, f2) -> HCEX (s, f2.HC.neg) |

2227 |
| HCENFORCES (s, f2) -> HCALLOWS (s, f2.HC.neg) |

2228 |
| HCALLOWS (s, f2) -> HCENFORCES (s, f2.HC.neg) |

2229 |
| HCMORETHAN (n, s, f1) -> HCMAXEXCEPT (n, s, f1.HC.neg) |

2230 |
| HCMAXEXCEPT (n, s, f1) -> HCMORETHAN (n, s, f1.HC.neg) |

2231 |
| HCATLEASTPROB (p, f1) -> HCLESSPROBFAIL (p, f1.HC.neg) |

2232 |
| HCLESSPROBFAIL (p, f1) -> HCATLEASTPROB (p, f1.HC.neg) |

2233 |
| HCCONST s -> HCCONSTN s |

2234 |
| HCCONSTN s -> HCCONST s |

2235 |
| HCID (f1) -> HCID(f1.HC.neg) |

2236 |
| HCNORM (f1, f2) -> HCNORMN(f1.HC.neg, f2.HC.neg) |

2237 |
| HCNORMN (f1, f2) -> HCNORM(f1.HC.neg, f2.HC.neg) |

2238 |
| HCCHC (f1, f2) -> HCCHC (f1.HC.neg, f2.HC.neg) |

2239 |
| HCFUS (first, f1) -> HCFUS (first, f1.HC.neg) |

2240 |
| HCMU (name, f1) -> HCNU (name, f1.HC.neg) |

2241 |
| HCNU (name, f1) -> HCMU (name, f1.HC.neg) |

2242 | |

2243 |
(** An instantiation of hash-consing for formulae. |

2244 |
*) |

2245 |
module HcFormula = HC.Make( |

2246 |
struct |

2247 |
type nde = hcFormula_node |

2248 |
type fml = formula |

2249 |
let equal (n1 : nde) n2 = equal_hcFormula_node n1 n2 |

2250 |
let hash (n : nde) = hash_hcFormula_node n |

2251 |
let negNde (n : nde) = negNde_hcFormula_node n |

2252 |
let toFml (n : nde) = toFml_hcFormula_node n |

2253 |
end |

2254 |
) |

2255 | |

2256 |
(** Converts a formula into its hash-consed version. |

2257 |
@param hcF A hash-cons table for formulae. |

2258 |
@param f A formula in negation normal form. |

2259 |
@return The hash-consed version of f. |

2260 |
@raise CoAlgException if f is not in negation normal form. |

2261 |
*) |

2262 |
let rec hc_formula hcF f = |

2263 |
match f with |

2264 |
| TRUE -> HcFormula.hashcons hcF HCTRUE |

2265 |
| FALSE -> HcFormula.hashcons hcF HCFALSE |

2266 |
| AP s -> HcFormula.hashcons hcF (HCAP s) |

2267 |
| VAR s -> HcFormula.hashcons hcF (HCVAR s) |

2268 |
| NOT (AP s) -> HcFormula.hashcons hcF (HCNOT s) |

2269 |
| AT (s, f1) -> |

2270 |
let tf1 = hc_formula hcF f1 in |

2271 |
HcFormula.hashcons hcF (HCAT (s, tf1)) |

2272 |
| OR (f1, f2) -> |

2273 |
let tf1 = hc_formula hcF f1 in |

2274 |
let tf2 = hc_formula hcF f2 in |

2275 |
HcFormula.hashcons hcF (HCOR (tf1, tf2)) |

2276 |
| AND (f1, f2) -> |

2277 |
let tf1 = hc_formula hcF f1 in |

2278 |
let tf2 = hc_formula hcF f2 in |

2279 |
HcFormula.hashcons hcF (HCAND (tf1, tf2)) |

2280 |
| NOT _ |

2281 |
| EQU _ |

2282 |
| MIN _ |

2283 |
| MAX _ |

2284 |
| IMP _ -> raise (CoAlgException "Formula is not in negation normal form.") |

2285 |
| EX (s, f1) -> |

2286 |
let tf1 = hc_formula hcF f1 in |

2287 |
HcFormula.hashcons hcF (HCEX (s, tf1)) |

2288 |
| AX (s, f1) -> |

2289 |
let tf1 = hc_formula hcF f1 in |

2290 |
HcFormula.hashcons hcF (HCAX (s, tf1)) |

2291 |
| ENFORCES (s, f1) -> |

2292 |
let tf1 = hc_formula hcF f1 in |

2293 |
HcFormula.hashcons hcF (HCENFORCES (s, tf1)) |

2294 |
| ALLOWS (s, f1) -> |

2295 |
let tf1 = hc_formula hcF f1 in |

2296 |
HcFormula.hashcons hcF (HCALLOWS (s, tf1)) |

2297 |
| MORETHAN (n, s, f1) -> |

2298 |
let tf1 = hc_formula hcF f1 in |

2299 |
HcFormula.hashcons hcF (HCMORETHAN (n, s, tf1)) |

2300 |
| MAXEXCEPT (n, s, f1) -> |

2301 |
let tf1 = hc_formula hcF f1 in |

2302 |
HcFormula.hashcons hcF (HCMAXEXCEPT (n, s, tf1)) |

2303 |
| ATLEASTPROB (p, f1) -> |

2304 |
HcFormula.hashcons hcF (HCATLEASTPROB (p, hc_formula hcF f1)) |

2305 |
| LESSPROBFAIL (p, f1) -> |

2306 |
HcFormula.hashcons hcF (HCLESSPROBFAIL (p, hc_formula hcF f1)) |

2307 |
| CONST s -> |

2308 |
HcFormula.hashcons hcF (HCCONST s) |

2309 |
| CONSTN s -> |

2310 |
HcFormula.hashcons hcF (HCCONSTN s) |

2311 |
| ID f1 -> |

2312 |
let tf1 = hc_formula hcF f1 in |

2313 |
HcFormula.hashcons hcF (HCID tf1) |

2314 |
| NORM (f1, f2) -> |

2315 |
let tf1 = hc_formula hcF f1 in |

2316 |
let tf2 = hc_formula hcF f2 in |

2317 |
HcFormula.hashcons hcF (HCNORM (tf1, tf2)) |

2318 |
| NORMN (f1, f2) -> |

2319 |
let tf1 = hc_formula hcF f1 in |

2320 |
let tf2 = hc_formula hcF f2 in |

2321 |
HcFormula.hashcons hcF (HCNORMN (tf1, tf2)) |

2322 |
| CHC (f1, f2) -> |

2323 |
let tf1 = hc_formula hcF f1 in |

2324 |
let tf2 = hc_formula hcF f2 in |

2325 |
HcFormula.hashcons hcF (HCCHC (tf1, tf2)) |

2326 |
| FUS (first, f1) -> |

2327 |
let tf1 = hc_formula hcF f1 in |

2328 |
HcFormula.hashcons hcF (HCFUS (first, tf1)) |

2329 |
| MU (var, f1) -> |

2330 |
let tf1 = hc_formula hcF f1 in |

2331 |
HcFormula.hashcons hcF (HCMU (var, tf1)) |

2332 |
| NU (var, f1) -> |

2333 |
let tf1 = hc_formula hcF f1 in |

2334 |
HcFormula.hashcons hcF (HCNU (var, tf1)) |

2335 |
| AF _ | EF _ |

2336 |
| AG _ | EG _ |

2337 |
| AU _ | EU _ |

2338 |
| AR _ | ER _ |

2339 |
| AB _ | EB _ -> |

2340 |
raise (CoAlgException ("nnf: CTL should have been removed at this point")) |

2341 | |

2342 |
(* Replace the Variable name in f with formula formula |

2343 |
hc_replace foo φ ψ => ψ[foo |-> φ] |

2344 |
*) |

2345 |
let rec hc_replace hcF name (formula: hcFormula) (f: hcFormula) = |

2346 |
let func = hc_replace hcF name formula in |

2347 |
let gennew = HcFormula.hashcons hcF in |

2348 |
match f.HC.node with |

2349 |
| HCTRUE |

2350 |
| HCFALSE |

2351 |
| HCAP _ |

2352 |
| HCNOT _ |

2353 |
| HCCONST _ |

2354 |
| HCCONSTN _ -> f |

2355 |
| HCVAR s -> |

2356 |
if compare s name == 0 |

2357 |
then formula |

2358 |
else f |

2359 |
| HCAT (s, f1) -> |

2360 |
let nf1 = func f1 in |

2361 |
if nf1 == f1 then f else gennew (HCAT(s, nf1)) |

2362 |
| HCOR (f1, f2) -> |

2363 |
let nf1 = func f1 in |

2364 |
let nf2 = func f2 in |

2365 |
if nf1 == f1 && nf2 == f2 then f else gennew (HCOR(nf1, nf2)) |

2366 |
| HCAND (f1, f2) -> |

2367 |
let nf1 = func f1 in |

2368 |
let nf2 = func f2 in |

2369 |
if nf1 == f1 && nf2 == f2 then f else gennew (HCAND(nf1, nf2)) |

2370 |
| HCEX (s, f1) -> |

2371 |
let nf1 = func f1 in |

2372 |
if nf1 == f1 then f else gennew (HCEX(s, nf1)) |

2373 |
| HCAX (s, f1) -> |

2374 |
let nf1 = func f1 in |

2375 |
if nf1 == f1 then f else gennew (HCAX(s, nf1)) |

2376 |
| HCENFORCES (s, f1) -> |

2377 |
let nf1 = func f1 in |

2378 |
if nf1 == f1 then f else gennew (HCENFORCES(s, nf1)) |

2379 |
| HCALLOWS (s, f1) -> |

2380 |
let nf1 = func f1 in |

2381 |
if nf1 == f1 then f else gennew (HCALLOWS(s, nf1)) |

2382 |
| HCMORETHAN (n, s, f1) -> |

2383 |
let nf1 = func f1 in |

2384 |
if nf1 == f1 then f else gennew (HCMORETHAN(n, s, nf1)) |

2385 |
| HCMAXEXCEPT (n, s, f1) -> |

2386 |
let nf1 = func f1 in |

2387 |
if nf1 == f1 then f else gennew (HCMAXEXCEPT(n, s, nf1)) |

2388 |
| HCATLEASTPROB (p, f1) -> |

2389 |
let nf1 = func f1 in |

2390 |
if nf1 == f1 then f else gennew (HCATLEASTPROB(p, nf1)) |

2391 |
| HCLESSPROBFAIL (p, f1) -> |

2392 |
let nf1 = func f1 in |

2393 |
if nf1 == f1 then f else gennew (HCLESSPROBFAIL(p, nf1)) |

2394 |
| HCID f1 -> |

2395 |
let nf1 = func f1 in |

2396 |
if nf1 == f1 then f else gennew (HCID(nf1)) |

2397 |
| HCNORM (f1, f2) -> |

2398 |
let nf1 = func f1 in |

2399 |
let nf2 = func f2 in |

2400 |
if nf1 == f1 && nf2 == f2 then f else gennew (HCNORM(nf1, nf2)) |

2401 |
| HCNORMN (f1, f2) -> |

2402 |
let nf1 = func f1 in |

2403 |
let nf2 = func f2 in |

2404 |
if nf1 == f1 && nf2 == f2 then f else gennew (HCNORMN(nf1, nf2)) |

2405 |
| HCCHC (f1, f2) -> |

2406 |
let nf1 = func f1 in |

2407 |
let nf2 = func f2 in |

2408 |
if nf1 == f1 && nf2 == f2 then f else gennew (HCCHC(nf1, nf2)) |

2409 |
| HCFUS (first, f1) -> |

2410 |
let nf1 = func f1 in |

2411 |
if nf1 == f1 then f else gennew (HCFUS(first, nf1)) |

2412 |
| HCMU (var, f1) -> |

2413 |
if compare var name != 0 then |

2414 |
let nf1 = func f1 in |

2415 |
if nf1 == f1 then f else gennew (HCMU(var, nf1)) |

2416 |
else |

2417 |
f |

2418 |
| HCNU (var, f1) -> |

2419 |
if compare var name != 0 then |

2420 |
let nf1 = func f1 in |

2421 |
if nf1 == f1 then f else gennew (HCNU(var, nf1)) |

2422 |
else |

2423 |
f |

2424 | |

2425 |
let rec hc_freeIn variable (f: hcFormula) = |

2426 |
match f.HC.node with |

2427 |
| HCTRUE |

2428 |
| HCFALSE |

2429 |
| HCAP _ |

2430 |
| HCNOT _ |

2431 |
| HCCONST _ |

2432 |
| HCCONSTN _ -> false |

2433 |
| HCVAR s -> |

2434 |
if compare variable s == 0 |

2435 |
then true |

2436 |
else false |

2437 |
| HCAT (s, f1) -> |

2438 |
hc_freeIn variable f1 |

2439 |
| HCOR (f1, f2) |

2440 |
| HCAND (f1, f2) -> |

2441 |
hc_freeIn variable f1 || hc_freeIn variable f2 |

2442 |
| HCEX (_, f1) |

2443 |
| HCAX (_, f1) |

2444 |
| HCENFORCES (_, f1) |

2445 |
| HCALLOWS (_, f1) |

2446 |
| HCMORETHAN (_, _, f1) |

2447 |
| HCMAXEXCEPT (_, _, f1) |

2448 |
| HCATLEASTPROB (_, f1) |

2449 |
| HCLESSPROBFAIL (_, f1) |

2450 |
| HCID f1 -> |

2451 |
hc_freeIn variable f1 |

2452 |
| HCNORM (f1, f2) |

2453 |
| HCNORMN (f1, f2) |

2454 |
| HCCHC (f1, f2) -> |

2455 |
hc_freeIn variable f1 || hc_freeIn variable f2 |

2456 |
| HCFUS (first, f1) -> |

2457 |
hc_freeIn variable f1 |

2458 |
| HCMU (var, f1) |

2459 |
| HCNU (var, f1) -> |

2460 |
(* Do we need to exclude bound variables here? *) |

2461 |
hc_freeIn variable f1 |

2462 | |

2463 | |

2464 |
(** An instantiation of a hash table (of the standard library) |

2465 |
for hash-consed formulae. The test for equality |

2466 |
and computing the hash value is done in constant time. |

2467 |
*) |

2468 |
module HcFHt = Hashtbl.Make( |

2469 |
struct |

2470 |
type t = hcFormula |

2471 |
let equal (f1 : t) f2 = f1.HC.tag = f2.HC.tag |

2472 |
let hash (f : t) = f.HC.tag |

2473 |
end |

2474 |
) |

2475 | |

2476 |
(* vim: set et sw=2 sts=2 ts=8 : *) |