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

History | View | Annotate | Download (66.9 KB)

1 | 4fd28192 | Thorsten Wißmann | (** 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 | f1fa9ad5 | Thorsten Wißmann | module L = List |

10 | module Str = String |
||

11 | 4fd28192 | Thorsten Wißmann | |

12 | |||

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

14 | that can happen in the tableau procedure. |
||

15 | c5c25acf | Christoph Egger | More specific information is given in the argument. |

16 | 4fd28192 | Thorsten Wißmann | *) |

17 | exception CoAlgException of string |
||

18 | |||

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

20 | *) |
||

21 | type sort = int |
||

22 | |||

23 | e5422169 | Thorsten Wißmann | type rational = { nominator: int; denominator: int } |

24 | |||

25 | 86b07be8 | Thorsten Wißmann | let string_of_rational r = |

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

27 | |||

28 | e5422169 | Thorsten Wißmann | let rational_of_int n d = { nominator = n; denominator = d } |

29 | |||

30 | 4fd28192 | Thorsten Wißmann | (** Defines (unsorted) coalgebraic formulae. |

31 | *) |
||

32 | type formula = |
||

33 | | TRUE |
||

34 | | FALSE |
||

35 | 69a71d22 | Thorsten Wißmann | | AP of string (* atomic proposition *) |

36 | 4fd28192 | Thorsten Wißmann | | 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 | f1fa9ad5 | Thorsten Wißmann | | ENFORCES of int list * formula |

45 | | ALLOWS of int list * formula |
||

46 | 4fd28192 | Thorsten Wißmann | | MIN of int * string * formula |

47 | | MAX of int * string * formula |
||

48 | af276a36 | Thorsten Wißmann | | MORETHAN of int * string * formula (* diamond of GML *) |

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

50 | e5422169 | Thorsten Wißmann | | ATLEASTPROB of rational * formula (* = {>= 0.5} C ---> C occurs with *) |

51 | c5c25acf | Christoph Egger | (* probability of at least 50% *) |

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

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

54 | c49eea11 | Thorsten Wißmann | | CONST of string (* constant functor with value string *) |

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

56 | 19f5dad0 | Dirk Pattinson | | 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 | d58bba0f | Dirk Pattinson | | CHC of formula * formula (* Choice is self-dual *) |

60 | 4fd28192 | Thorsten Wißmann | | FUS of bool * formula |

61 | d29d35f7 | Christoph Egger | | MU of string * formula |

62 | | NU of string * formula |
||

63 | 9a3b23cc | Christoph Egger | | VAR of string |

64 | b179a57f | Christoph Egger | | 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 | 4fd28192 | Thorsten Wißmann | |

71 | ca99d0c6 | Thorsten Wißmann | exception ConversionException of formula |

72 | |||

73 | |||

74 | 4fd28192 | Thorsten Wißmann | (** Defines sorted coalgebraic formulae. |

75 | *) |
||

76 | type sortedFormula = sort * formula |
||

77 | |||

78 | |||

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

80 | @param A string s. |
||

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

82 | *) |
||

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

84 | |||

85 | |||

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

87 | @param f A formula. |
||

88 | @return The size of f. |
||

89 | *) |
||

90 | let rec sizeFormula f = |
||

91 | match f with |
||

92 | c5c25acf | Christoph Egger | | TRUE |

93 | | FALSE |
||

94 | 4fd28192 | Thorsten Wißmann | | AP _ -> 1 |

95 | | NOT f1 |
||

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

97 | c5c25acf | Christoph Egger | | OR (f1, f2) |

98 | 4fd28192 | Thorsten Wißmann | | AND (f1, f2) |

99 | c5c25acf | Christoph Egger | | EQU (f1, f2) |

100 | 4fd28192 | Thorsten Wißmann | | IMP (f1, f2) -> succ (sizeFormula f1 + sizeFormula f2) |

101 | | EX (_, f1) |
||

102 | f1fa9ad5 | Thorsten Wißmann | | AX (_, f1) |

103 | | ENFORCES (_, f1) |
||

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

105 | 4fd28192 | Thorsten Wißmann | | MIN (_, _, f1) |

106 | af276a36 | Thorsten Wißmann | | MAX (_, _, f1) |

107 | 81435cc4 | Thorsten Wißmann | | ATLEASTPROB (_, f1) |

108 | 9bae2c4f | Thorsten Wißmann | | LESSPROBFAIL (_, f1) |

109 | af276a36 | Thorsten Wißmann | | MORETHAN (_, _, f1) |

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

111 | 19f5dad0 | Dirk Pattinson | | ID (f1) -> succ (sizeFormula f1) |

112 | | NORM(f1, f2) |
||

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

114 | c49eea11 | Thorsten Wißmann | | CONST _ |

115 | | CONSTN _ -> 1 |
||

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

117 | 4fd28192 | Thorsten Wißmann | | FUS (_, f1) -> succ (sizeFormula f1) |

118 | a5f60450 | Christoph Egger | | MU (_, f1) |

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

120 | | VAR _ -> 1 |
||

121 | 8cac0897 | Christoph Egger | | AF _ | EF _ |

122 | | AG _ | EG _ |
||

123 | | AU _ | EU _ -> |
||

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

125 | 4fd28192 | Thorsten Wißmann | |

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

127 | @param f A sorted formula. |
||

128 | @return The size of f. |
||

129 | *) |
||

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

131 | |||

132 | |||

133 | c49eea11 | Thorsten Wißmann | (* think of func: (formula -> unit) -> formula -> unit as identity. |

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

135 | dbcce612 | Thorsten Wißmann | let rec iter func formula = |

136 | func formula; |
||

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

138 | match formula with |
||

139 | 309b71a5 | Christoph Egger | | TRUE | FALSE | AP _ | VAR _ -> () |

140 | c49eea11 | Thorsten Wißmann | | CONST _ |

141 | | CONSTN _ -> () |
||

142 | dbcce612 | Thorsten Wißmann | | NOT a | AT (_,a) |

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

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

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

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

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

148 | 9bae2c4f | Thorsten Wißmann | | ATLEASTPROB (_, a) | LESSPROBFAIL (_, a) |

149 | dbcce612 | Thorsten Wißmann | | MORETHAN (_,_,a) | MAXEXCEPT (_,_,a) -> proc a |

150 | 19f5dad0 | Dirk Pattinson | | ID(a) -> proc a |

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

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

153 | dbcce612 | Thorsten Wißmann | | FUS (_,a) -> proc a |

154 | 309b71a5 | Christoph Egger | | MU (_, f) | NU (_, f) -> proc f |

155 | fbffb079 | Christoph Egger | | AF f | EF f | AG f | EG f -> proc f |

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

157 | dbcce612 | Thorsten Wißmann | |

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

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

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

161 | let formula = (match formula with |
||

162 | (* 0-ary constructors *) |
||

163 | 7b944a64 | Christoph Egger | | TRUE | FALSE | AP _ | VAR _ -> formula |

164 | c49eea11 | Thorsten Wißmann | | CONST _ |

165 | | CONSTN _ -> formula |
||

166 | dbcce612 | Thorsten Wißmann | (* unary *) |

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

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

169 | (* binary *) |
||

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

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

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

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

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

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

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

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

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

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

180 | 81435cc4 | Thorsten Wißmann | | ATLEASTPROB (p,a) -> ATLEASTPROB (p, c a) |

181 | 9bae2c4f | Thorsten Wißmann | | LESSPROBFAIL (p,a) -> LESSPROBFAIL (p, c a) |

182 | dbcce612 | Thorsten Wißmann | | MORETHAN (n,s,a) -> MORETHAN (n,s,c a) |

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

184 | 19f5dad0 | Dirk Pattinson | | ID(a) -> ID (c a) |

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

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

187 | dbcce612 | Thorsten Wißmann | | CHC (a,b) -> CHC (c a, c b) |

188 | 7b944a64 | Christoph Egger | | FUS (s,a) -> FUS (s, c a) |

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

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

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

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

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

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

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

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

197 | dbcce612 | Thorsten Wißmann | func formula |

198 | |||

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

200 | let helper formula = match formula with |
||

201 | ca99d0c6 | Thorsten Wißmann | | ENFORCES _ | ALLOWS _ -> raise (ConversionException formula) |

202 | dbcce612 | Thorsten Wißmann | | MORETHAN (0,s,a) | MIN (1,s,a) -> EX (s,a) |

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

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

205 | ca99d0c6 | Thorsten Wißmann | | TRUE | FALSE |

206 | | EQU _ | IMP _ |
||

207 | | AND _ | OR _ |
||

208 | | AP _ | NOT _ |
||

209 | dbcce612 | Thorsten Wißmann | | AX _ | EX _ |

210 | d58bba0f | Dirk Pattinson | | CHC _ | FUS _ -> formula |

211 | ca99d0c6 | Thorsten Wißmann | | _ -> raise (ConversionException formula) |

212 | dbcce612 | Thorsten Wißmann | in |

213 | convert_post helper formula |
||

214 | |||

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

216 | let helper formula = match formula with |
||

217 | ca99d0c6 | Thorsten Wißmann | | ENFORCES _ | ALLOWS _ -> raise (ConversionException formula) |

218 | dbcce612 | Thorsten Wißmann | | MORETHAN _ | MIN _ | MAX _ | MAXEXCEPT _ -> formula |

219 | ca99d0c6 | Thorsten Wißmann | | TRUE | FALSE |

220 | | EQU _ | IMP _ |
||

221 | | AND _ | OR _ |
||

222 | | AP _ | NOT _ |
||

223 | d58bba0f | Dirk Pattinson | | CHC _ | FUS _ -> formula |

224 | dbcce612 | Thorsten Wißmann | | AX (r,a) -> MAXEXCEPT (0,r,a) |

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

226 | ca99d0c6 | Thorsten Wißmann | | _ -> raise (ConversionException formula) |

227 | dbcce612 | Thorsten Wißmann | in |

228 | convert_post helper formula |
||

229 | |||

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

231 | |||

232 | c5105465 | Christoph Egger | let convertToMu formula = |

233 | 17af2794 | Christoph Egger | let helper formula = |

234 | c5c25acf | Christoph Egger | match formula with |

235 | | AF f1 -> |
||

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

237 | c5c25acf | Christoph Egger | | EF f1 -> |

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

239 | c5c25acf | Christoph Egger | | AG f1 -> |

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

241 | c5c25acf | Christoph Egger | | EG f1 -> |

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

243 | c5c25acf | Christoph Egger | | AU (f1, f2) -> |

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

245 | c5c25acf | Christoph Egger | | EU (f1, f2) -> |

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

247 | c5c25acf | Christoph Egger | | _ -> formula |

248 | c5105465 | Christoph Egger | in |

249 | convert_post helper formula |
||

250 | |||

251 | 4fd28192 | Thorsten Wißmann | (** Appends a string representation of a formula to a string buffer. |

252 | Parentheses are ommited where possible |
||

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

254 | @param sb A string buffer. |
||

255 | @param f A formula. |
||

256 | *) |
||

257 | let rec exportFormula_buffer sb f = |
||

258 | let negate = function |
||

259 | | NOT f -> f |
||

260 | | f -> NOT f |
||

261 | in |
||

262 | let prio n lf = |
||

263 | let prionr = function |
||

264 | | EQU _ -> 0 |
||

265 | c5c25acf | Christoph Egger | | IMP _ -> 1 |

266 | 4fd28192 | Thorsten Wißmann | | OR _ -> 2 |

267 | | AND _ -> 3 |
||

268 | | _ -> 4 |
||

269 | in |
||

270 | if prionr lf < n then begin |
||

271 | Buffer.add_char sb '('; |
||

272 | exportFormula_buffer sb lf; |
||

273 | Buffer.add_char sb ')' |
||

274 | end |
||

275 | else exportFormula_buffer sb lf |
||

276 | in |
||

277 | match f with |
||

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

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

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

281 | | NOT f1 -> |
||

282 | Buffer.add_string sb "~"; |
||

283 | prio 4 f1 |
||

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

285 | Buffer.add_string sb "@ "; |
||

286 | Buffer.add_string sb s; |
||

287 | Buffer.add_string sb " "; |
||

288 | prio 4 f1 |
||

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

290 | prio 2 f1; |
||

291 | Buffer.add_string sb " | "; |
||

292 | prio 2 f2 |
||

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

294 | prio 3 f1; |
||

295 | Buffer.add_string sb " & "; |
||

296 | prio 3 f2 |
||

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

298 | prio 0 f1; |
||

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

300 | prio 0 f2 |
||

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

302 | prio 2 f1; |
||

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

304 | prio 2 f2 |
||

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

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

307 | Buffer.add_string sb s; |
||

308 | Buffer.add_string sb ">"; |
||

309 | prio 4 f1 |
||

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

311 | Buffer.add_string sb "["; |
||

312 | Buffer.add_string sb s; |
||

313 | Buffer.add_string sb "]"; |
||

314 | prio 4 f1 |
||

315 | f1fa9ad5 | Thorsten Wißmann | | ALLOWS (s, f1) -> |

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

317 | c16fd631 | Thorsten Wißmann | Buffer.add_string sb ( |

318 | match s with |
||

319 | | [] -> " " |
||

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

321 | ); |
||

322 | f1fa9ad5 | Thorsten Wißmann | Buffer.add_string sb "}>"; |

323 | prio 4 f1 |
||

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

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

326 | c16fd631 | Thorsten Wißmann | Buffer.add_string sb ( |

327 | match s with |
||

328 | | [] -> " " |
||

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

330 | ); |
||

331 | f1fa9ad5 | Thorsten Wißmann | Buffer.add_string sb "}]"; |

332 | prio 4 f1 |
||

333 | 86b07be8 | Thorsten Wißmann | | ATLEASTPROB (p, f1) -> |

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

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

336 | Buffer.add_string sb "}"; |
||

337 | prio 4 f1 |
||

338 | 9bae2c4f | Thorsten Wißmann | | LESSPROBFAIL (p, f1) -> |

339 | c855ba91 | Thorsten Wißmann | Buffer.add_string sb "{<"; |

340 | 86b07be8 | Thorsten Wißmann | Buffer.add_string sb (string_of_rational p); |

341 | 9bae2c4f | Thorsten Wißmann | Buffer.add_string sb "} ~ "; |

342 | 86b07be8 | Thorsten Wißmann | prio 4 f1 |

343 | 4fd28192 | Thorsten Wißmann | | MIN (n, s, f1) -> |

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

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

346 | Buffer.add_string sb " "; |
||

347 | Buffer.add_string sb s; |
||

348 | Buffer.add_string sb "}"; |
||

349 | prio 4 f1 |
||

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

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

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

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

354 | Buffer.add_string sb s; |
||

355 | Buffer.add_string sb "}"; |
||

356 | prio 4 f1 |
||

357 | af276a36 | Thorsten Wißmann | | MORETHAN (n, s, f1) -> |

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

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

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

361 | Buffer.add_string sb s; |
||

362 | Buffer.add_string sb "}"; |
||

363 | prio 4 f1 |
||

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

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

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

367 | Buffer.add_string sb " ~ "; |
||

368 | Buffer.add_string sb s; |
||

369 | Buffer.add_string sb "}"; |
||

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

371 | 19f5dad0 | Dirk Pattinson | | ID (f1) -> |

372 | Buffer.add_string sb "O"; |
||

373 | prio 4 f1 |
||

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

375 | Buffer.add_string sb "("; |
||

376 | exportFormula_buffer sb f1; |
||

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

378 | exportFormula_buffer sb f2; |
||

379 | Buffer.add_string sb ")" |
||

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

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

382 | exportFormula_buffer sb (negate f1); |
||

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

384 | exportFormula_buffer sb (negate f2); |
||

385 | Buffer.add_string sb ")" |
||

386 | 4fd28192 | Thorsten Wißmann | | CHC (f1, f2) -> |

387 | Buffer.add_string sb "("; |
||

388 | exportFormula_buffer sb f1; |
||

389 | Buffer.add_string sb " + "; |
||

390 | exportFormula_buffer sb f2; |
||

391 | Buffer.add_string sb ")" |
||

392 | c49eea11 | Thorsten Wißmann | | CONST s -> Buffer.add_string sb "="; |

393 | Buffer.add_string sb s |
||

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

395 | Buffer.add_string sb s |
||

396 | 4fd28192 | Thorsten Wißmann | | FUS (first, f1) -> |

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

398 | prio 4 f1 |
||

399 | 8334c748 | Christoph Egger | | MU (s, f1) -> |

400 | Buffer.add_string sb "μ"; |
||

401 | d29d35f7 | Christoph Egger | Buffer.add_string sb s; |

402 | 8334c748 | Christoph Egger | Buffer.add_string sb "."; |

403 | prio 4 f1 |
||

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

405 | Buffer.add_string sb "ν"; |
||

406 | c5c25acf | Christoph Egger | Buffer.add_string sb s; |

407 | 8334c748 | Christoph Egger | Buffer.add_string sb "."; |

408 | prio 4 f1 |
||

409 | | VAR s -> |
||

410 | Buffer.add_string sb s |
||

411 | 0aa34675 | Christoph Egger | | AF f1 -> |

412 | c5c25acf | Christoph Egger | Buffer.add_string sb "AF "; |

413 | prio 4 f1 |
||

414 | 0aa34675 | Christoph Egger | | EF f1 -> |

415 | c5c25acf | Christoph Egger | Buffer.add_string sb "EF "; |

416 | prio 4 f1 |
||

417 | 0aa34675 | Christoph Egger | | AG f1 -> |

418 | c5c25acf | Christoph Egger | Buffer.add_string sb "AG "; |

419 | prio 4 f1 |
||

420 | 0aa34675 | Christoph Egger | | EG f1 -> |

421 | c5c25acf | Christoph Egger | Buffer.add_string sb "EG "; |

422 | prio 4 f1 |
||

423 | 0aa34675 | Christoph Egger | | AU (f1, f2) -> |

424 | c5c25acf | Christoph Egger | Buffer.add_string sb "A ("; |

425 | prio 4 f1; |
||

426 | Buffer.add_string sb " U "; |
||

427 | prio 4 f2; |
||

428 | Buffer.add_string sb ")" |
||

429 | 0aa34675 | Christoph Egger | | EU (f1, f2) -> |

430 | c5c25acf | Christoph Egger | Buffer.add_string sb "E ("; |

431 | prio 4 f1; |
||

432 | Buffer.add_string sb " U "; |
||

433 | prio 4 f2; |
||

434 | Buffer.add_string sb ")" |
||

435 | 4fd28192 | Thorsten Wißmann | |

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

437 | Parentheses are ommited where possible |
||

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

439 | @param f A formula. |
||

440 | @return A string representing f. |
||

441 | *) |
||

442 | let exportFormula f = |
||

443 | let sb = Buffer.create 128 in |
||

444 | exportFormula_buffer sb f; |
||

445 | Buffer.contents sb |
||

446 | |||

447 | ca99d0c6 | Thorsten Wißmann | let string_of_formula = exportFormula |

448 | |||

449 | 01b1ab69 | Thorsten Wißmann | (** export (CL)-formula suitable for tatl-inputs *) |

450 | let rec exportTatlFormula_buffer sb f = |
||

451 | let prio n lf = |
||

452 | let prionr = function |
||

453 | | EQU _ -> 0 |
||

454 | c5c25acf | Christoph Egger | | IMP _ -> 1 |

455 | 01b1ab69 | Thorsten Wißmann | | OR _ -> 2 |

456 | | AND _ -> 3 |
||

457 | | _ -> 4 |
||

458 | in |
||

459 | if prionr lf < n then begin |
||

460 | Buffer.add_char sb '('; |
||

461 | 064f3099 | Thorsten Wißmann | exportTatlFormula_buffer sb lf; |

462 | 01b1ab69 | Thorsten Wißmann | Buffer.add_char sb ')' |

463 | end |
||

464 | 064f3099 | Thorsten Wißmann | else exportTatlFormula_buffer sb lf |

465 | 01b1ab69 | Thorsten Wißmann | in |

466 | match f with |
||

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

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

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

470 | | NOT f1 -> |
||

471 | Buffer.add_string sb "~"; |
||

472 | prio 4 f1 |
||

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

474 | prio 2 f1; |
||

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

476 | prio 2 f2 |
||

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

478 | prio 3 f1; |
||

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

480 | prio 3 f2 |
||

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

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

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

484 | prio 2 f1; |
||

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

486 | prio 2 f2 |
||

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

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

489 | Buffer.add_string sb ( |
||

490 | match s with |
||

491 | | [] -> " " |
||

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

493 | ); |
||

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

495 | prio 4 f1 |
||

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

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

498 | Buffer.add_string sb ( |
||

499 | match s with |
||

500 | | [] -> " " |
||

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

502 | ); |
||

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

504 | prio 4 f1 |
||

505 | | EX _ |
||

506 | | AX _ |
||

507 | | MIN _ |
||

508 | | MAX _ |
||

509 | | MORETHAN _ |
||

510 | | MAXEXCEPT _ |
||

511 | | AT _ |
||

512 | c49eea11 | Thorsten Wißmann | | CONST _ |

513 | | CONSTN _ |
||

514 | 01b1ab69 | Thorsten Wißmann | | CHC _ |

515 | 86b07be8 | Thorsten Wißmann | | ATLEASTPROB _ |

516 | 9bae2c4f | Thorsten Wißmann | | LESSPROBFAIL _ |

517 | 19f5dad0 | Dirk Pattinson | | ID _ |

518 | | NORM _ |
||

519 | | NORMN _ |
||

520 | 8cac0897 | Christoph Egger | | FUS _ |

521 | | MU _ |
||

522 | | NU _ |
||

523 | | VAR _ |
||

524 | | AF _ |
||

525 | | EF _ |
||

526 | | AG _ |
||

527 | | EG _ |
||

528 | | AU _ |
||

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

530 | 01b1ab69 | Thorsten Wißmann | |

531 | let exportTatlFormula f = |
||

532 | let sb = Buffer.create 128 in |
||

533 | exportTatlFormula_buffer sb f; |
||

534 | Buffer.contents sb |
||

535 | |||

536 | 4fd28192 | Thorsten Wißmann | (** Appends a string representation of a sorted formula to a string buffer. |

537 | Parentheses are ommited where possible |
||

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

539 | @param sb A string buffer. |
||

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

541 | *) |
||

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

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

544 | Buffer.add_string sb ": "; |
||

545 | exportFormula_buffer sb f |
||

546 | |||

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

548 | Parentheses are ommited where possible |
||

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

550 | @param f A sorted formula. |
||

551 | @return A string representing f. |
||

552 | *) |
||

553 | let exportSortedFormula f = |
||

554 | let sb = Buffer.create 128 in |
||

555 | exportSortedFormula_buffer sb f; |
||

556 | Buffer.contents sb |
||

557 | |||

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

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

560 | @param f A sorted formula. |
||

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

562 | *) |
||

563 | let exportQuery tbox f = |
||

564 | let sb = Buffer.create 1000 in |
||

565 | let rec expFl = function |
||

566 | | [] -> () |
||

567 | | h::tl -> |
||

568 | exportSortedFormula_buffer sb h; |
||

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

570 | expFl tl |
||

571 | in |
||

572 | expFl tbox; |
||

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

574 | exportSortedFormula_buffer sb f; |
||

575 | Buffer.contents sb |
||

576 | |||

577 | b59059c4 | Thorsten Wißmann | (** Converts a (sorted) formula query into a string representation. Such that |

578 | coalg can read it again using importQuery |
||

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

580 | @param f A sorted formula. |
||

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

582 | *) |
||

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

584 | let sb = Buffer.create 1000 in |
||

585 | let rec expFl = function |
||

586 | | [] -> () |
||

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

588 | exportFormula_buffer sb h; |
||

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

590 | expFl tl |
||

591 | in |
||

592 | expFl tbox; |
||

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

594 | exportFormula_buffer sb f; |
||

595 | Buffer.contents sb |
||

596 | |||

597 | 4fd28192 | Thorsten Wißmann | |

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

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

600 | *) |
||

601 | c5c25acf | Christoph Egger | let lexer = A.make_lexer |

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

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

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

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

606 | ] |
||

607 | 4fd28192 | Thorsten Wißmann | |

608 | let mk_exn s = CoAlgException s |
||

609 | |||

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

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

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

613 | *) |
||

614 | let rec verifyMuAltFree formula = |
||

615 | let proc = verifyMuAltFree in |
||

616 | match formula with |
||

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

618 | | CONST _ |
||

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

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

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

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

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

624 | c5c25acf | Christoph Egger | let (atype, afree) = proc a |

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

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

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

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

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

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

631 | else |
||

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

633 | 63710593 | Christoph Egger | | ENFORCES (_,a) | ALLOWS (_,a) |

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

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

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

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

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

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

640 | c5c25acf | Christoph Egger | let (atype, afree) = proc a |

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

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

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

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

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

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

647 | else |
||

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

649 | 63710593 | Christoph Egger | | FUS (_,a) -> proc a |

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

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

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

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

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

655 | 63710593 | Christoph Egger | let newfree = List.filter predicate free in |

656 | c5c25acf | Christoph Egger | if newfree = [] then |

657 | ("none", []) |
||

658 | else |
||

659 | ("μ", newfree) |
||

660 | 63710593 | Christoph Egger | | NU (s, f) -> |

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

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

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

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

665 | 63710593 | Christoph Egger | let newfree = List.filter predicate free in |

666 | c5c25acf | Christoph Egger | if newfree = [] then |

667 | ("none", []) |
||

668 | else |
||

669 | ("ν", newfree) |
||

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

671 | 939f5bab | Christoph Egger | | AF _ | EF _ | AG _ | EG _ | AU _ | EU _ -> |

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

673 | 939f5bab | Christoph Egger | |

674 | 63710593 | Christoph Egger | |

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

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

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

678 | negations is even. |
||

679 | *) |
||

680 | let rec verifyMuMonotone negations formula = |
||

681 | let proc = verifyMuMonotone negations in |
||

682 | match formula with |
||

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

684 | | CONST _ |
||

685 | | CONSTN _ -> () |
||

686 | | AT (_,a) |
||

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

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

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

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

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

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

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

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

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

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

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

698 | | MU (s, f) |
||

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

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

701 | verifyMuMonotone newNeg f |
||

702 | 63710593 | Christoph Egger | | VAR s -> |

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

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

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

706 | 63710593 | Christoph Egger | | NOT a -> |

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

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

709 | verifyMuMonotone newNeg a |
||

710 | 939f5bab | Christoph Egger | | AF _ | EF _ | AG _ | EG _ | AU _ | EU _ -> |

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

712 | 63710593 | Christoph Egger | |

713 | 26cfb2dc | Christoph Egger | let rec verifyMuGuarded unguarded formula = |

714 | let proc = verifyMuGuarded unguarded in |
||

715 | match formula with |
||

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

717 | | CONST _ |
||

718 | | CONSTN _ -> () |
||

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

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

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

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

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

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

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

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

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

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

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

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

731 | | MU (s, f) |
||

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

733 | c5c25acf | Christoph Egger | let newUnguard = s :: unguarded in |

734 | verifyMuGuarded newUnguard f |
||

735 | 26cfb2dc | Christoph Egger | | VAR s -> |

736 | c5c25acf | Christoph Egger | let finder x = compare x s == 0 in |

737 | if List.exists finder unguarded then |
||

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

739 | 939f5bab | Christoph Egger | | AF _ | EF _ | AG _ | EG _ | AU _ | EU _ -> |

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

741 | 63710593 | Christoph Egger | |

742 | let verifyFormula formula = |
||

743 | verifyMuAltFree formula; |
||

744 | verifyMuMonotone [] formula; |
||

745 | 26cfb2dc | Christoph Egger | verifyMuGuarded [] formula |

746 | 63710593 | Christoph Egger | |

747 | 4fd28192 | Thorsten Wißmann | (** These functions parse a token stream to obtain a formula. |

748 | It is a standard recursive descent procedure. |
||

749 | @param ts A token stream. |
||

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

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

752 | *) |
||

753 | 0b908205 | Christoph Egger | let rec parse_formula (symtab: 'a list) ts = |

754 | 1484d8cb | Christoph Egger | let formula = (parse_imp symtab ts) in |

755 | let f1 = convertToMu formula in |
||

756 | 4fd28192 | Thorsten Wißmann | match Stream.peek ts with |

757 | | None -> f1 |
||

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

759 | Stream.junk ts; |
||

760 | 0b908205 | Christoph Egger | let f2 = parse_formula symtab ts in |

761 | 4fd28192 | Thorsten Wißmann | EQU (f1, f2) |

762 | | _ -> f1 |
||

763 | |||

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

765 | It is a standard recursive descent procedure. |
||

766 | @param ts A token stream. |
||

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

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

769 | *) |
||

770 | 0b908205 | Christoph Egger | and parse_imp symtab ts= |

771 | let f1 = parse_or symtab ts in |
||

772 | 4fd28192 | Thorsten Wißmann | match Stream.peek ts with |

773 | | None -> f1 |
||

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

775 | Stream.junk ts; |
||

776 | 0b908205 | Christoph Egger | let f2 = parse_imp symtab ts in |

777 | 4fd28192 | Thorsten Wißmann | IMP (f1, f2) |

778 | | _ -> f1 |
||

779 | |||

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

781 | It is a standard recursive descent procedure. |
||

782 | @param ts A token stream. |
||

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

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

785 | *) |
||

786 | 0b908205 | Christoph Egger | and parse_or symtab ts = |

787 | let f1 = parse_and symtab ts in |
||

788 | 4fd28192 | Thorsten Wißmann | match Stream.peek ts with |

789 | | None -> f1 |
||

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

791 | Stream.junk ts; |
||

792 | 0b908205 | Christoph Egger | let f2 = parse_or symtab ts in |

793 | 4fd28192 | Thorsten Wißmann | OR (f1, f2) |

794 | | _ -> f1 |
||

795 | |||

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

797 | It is a standard recursive descent procedure. |
||

798 | @param ts A token stream. |
||

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

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

801 | *) |
||

802 | 0b908205 | Christoph Egger | and parse_and symtab ts = |

803 | let f1 = parse_cimp symtab ts in |
||

804 | 4fd28192 | Thorsten Wißmann | match Stream.peek ts with |

805 | | None -> f1 |
||

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

807 | Stream.junk ts; |
||

808 | 0b908205 | Christoph Egger | let f2 = parse_and symtab ts in |

809 | 4fd28192 | Thorsten Wißmann | AND (f1, f2) |

810 | | _ -> f1 |
||

811 | |||

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

813 | It is a standard recursive descent procedure. |
||

814 | @param ts A token stream. |
||

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

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

817 | *) |
||

818 | 0b908205 | Christoph Egger | and parse_cimp symtab ts = |

819 | let f1 = parse_rest symtab ts in |
||

820 | 19f5dad0 | Dirk Pattinson | match Stream.peek ts with |

821 | | None -> f1 |
||

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

823 | Stream.junk ts; |
||

824 | 0b908205 | Christoph Egger | let f2 = parse_cimp symtab ts in |

825 | 19f5dad0 | Dirk Pattinson | NORM (f1, f2) |

826 | | _ -> f1 |
||

827 | |||

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

829 | It is a standard recursive descent procedure. |
||

830 | @param ts A token stream. |
||

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

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

833 | *) |
||

834 | 0b908205 | Christoph Egger | and parse_rest symtab ts = |

835 | 4fd28192 | Thorsten Wißmann | let boxinternals noNo es = |

836 | let n = |
||

837 | if noNo then 0 |
||

838 | else |
||

839 | match Stream.next ts with |
||

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

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

842 | in |
||

843 | e5422169 | Thorsten Wißmann | let (s,denominator) = |

844 | 4fd28192 | Thorsten Wißmann | match Stream.peek ts with |

845 | e5422169 | Thorsten Wißmann | | Some (A.Ident s1) -> Stream.junk ts; (s1,0) |

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

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

848 | Stream.junk ts; |
||

849 | match Stream.next ts with |
||

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

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

852 | end |
||

853 | 4fd28192 | Thorsten Wißmann | | _ -> A.printError mk_exn ~ts ("role name or \"" ^ es ^ "\" expected: ") |

854 | in |
||

855 | eda515b6 | Thorsten Wißmann | if (denominator < n) then begin |

856 | let explanation = |
||

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

858 | in |
||

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

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

861 | ) |
||

862 | e5422169 | Thorsten Wißmann | end; |

863 | 4fd28192 | Thorsten Wißmann | let _ = |

864 | match Stream.next ts with |
||

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

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

867 | in |
||

868 | e5422169 | Thorsten Wißmann | (n, denominator, s) |

869 | 4fd28192 | Thorsten Wißmann | in |

870 | f1fa9ad5 | Thorsten Wißmann | let rec agentlist es = |

871 | e2dc68f7 | Thorsten Wißmann | let allAgents = CoolUtils.cl_get_agents () in |

872 | f1fa9ad5 | Thorsten Wißmann | match Stream.next ts with |

873 | e2dc68f7 | Thorsten Wißmann | | A.Int n -> if CoolUtils.TArray.elem n allAgents |

874 | then n::(agentlist es) |
||

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

876 | f1fa9ad5 | Thorsten Wißmann | | A.Kwd c when c = es -> [] |

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

878 | in |
||

879 | 4fd28192 | Thorsten Wißmann | match Stream.next ts with |

880 | 19f5dad0 | Dirk Pattinson | | A.Kwd "true" -> |

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

882 | AP "true" |
||

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

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

885 | AP "false" |
||

886 | 4fd28192 | Thorsten Wißmann | | A.Kwd "True" -> TRUE |

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

888 | c3e13ca6 | Christoph Egger | | A.Ident s -> |

889 | c5c25acf | Christoph Egger | (try |

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

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

892 | VAR symbol |
||

893 | with Not_found -> AP s) |
||

894 | 4fd28192 | Thorsten Wißmann | | A.Kwd "~" -> |

895 | 0b908205 | Christoph Egger | let f = parse_rest symtab ts in |

896 | 4fd28192 | Thorsten Wißmann | NOT f |

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

898 | let s = |
||

899 | match Stream.next ts with |
||

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

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

902 | in |
||

903 | 0b908205 | Christoph Egger | let f = parse_rest symtab ts in |

904 | 4fd28192 | Thorsten Wißmann | AT (s, f) |

905 | c5c25acf | Christoph Egger | | A.Kwd "<" -> |

906 | e5422169 | Thorsten Wißmann | let (_, _, s) = boxinternals true ">" in |

907 | 0b908205 | Christoph Egger | let f1 = parse_rest symtab ts in |

908 | c5c25acf | Christoph Egger | EX (s, f1) |

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

910 | e5422169 | Thorsten Wißmann | let (_, _, s) = boxinternals true "]" in |

911 | 0b908205 | Christoph Egger | let f1 = parse_rest symtab ts in |

912 | 4fd28192 | Thorsten Wißmann | AX (s, f1) |

913 | c5c25acf | Christoph Egger | | A.Kwd "[{" -> |

914 | 7aa620ce | Thorsten Wißmann | let ls = agentlist "}]" in |

915 | 0b908205 | Christoph Egger | let f1 = parse_rest symtab ts in |

916 | 7aa620ce | Thorsten Wißmann | ENFORCES (ls, f1) |

917 | c5c25acf | Christoph Egger | | A.Kwd "<{" -> |

918 | 7aa620ce | Thorsten Wißmann | let ls = agentlist "}>" in |

919 | 0b908205 | Christoph Egger | let f1 = parse_rest symtab ts in |

920 | 7aa620ce | Thorsten Wißmann | ALLOWS (ls, f1) |

921 | c5c25acf | Christoph Egger | | A.Kwd "{>=" -> |

922 | e5422169 | Thorsten Wißmann | let (n, denom, s) = boxinternals false "}" in |

923 | 0b908205 | Christoph Egger | let f1 = parse_rest symtab ts in |

924 | e5422169 | Thorsten Wißmann | if (denom <> 0) |

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

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

927 | c5c25acf | Christoph Egger | | A.Kwd "{<=" -> |

928 | e5422169 | Thorsten Wißmann | let (n, denom, s) = boxinternals false "}" in |

929 | 0b908205 | Christoph Egger | let f1 = parse_rest symtab ts in |

930 | e5422169 | Thorsten Wißmann | if (denom <> 0) |

931 | c855ba91 | Thorsten Wißmann | then A.printError mk_exn ~ts "Can not express {<= probability}" |

932 | e5422169 | Thorsten Wißmann | else MAX (n, s, f1) |

933 | c5c25acf | Christoph Egger | | A.Kwd "{<" -> |

934 | c855ba91 | Thorsten Wißmann | let (n, denom, s) = boxinternals false "}" in |

935 | 0b908205 | Christoph Egger | let f1 = parse_rest symtab ts in |

936 | c855ba91 | Thorsten Wißmann | if (denom <> 0) |

937 | 9bae2c4f | Thorsten Wißmann | then LESSPROBFAIL (rational_of_int n denom, NOT f1) |

938 | c855ba91 | Thorsten Wißmann | else A.printError mk_exn ~ts "The \"Less than\" < is not implemented yet" |

939 | c49eea11 | Thorsten Wißmann | | A.Kwd "=" -> begin |

940 | match Stream.next ts with |
||

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

942 | | A.Kwd s |
||

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

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

945 | end |
||

946 | 4fd28192 | Thorsten Wißmann | | A.Kwd "(" -> begin |

947 | 0b908205 | Christoph Egger | let f = parse_formula symtab ts in |

948 | 4fd28192 | Thorsten Wißmann | match Stream.next ts with |

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

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

951 | 0b908205 | Christoph Egger | let f2 = parse_formula symtab ts in |

952 | 4fd28192 | Thorsten Wißmann | match Stream.next ts with |

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

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

955 | end |
||

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

957 | end |
||

958 | 19f5dad0 | Dirk Pattinson | | A.Kwd "O" -> |

959 | 0b908205 | Christoph Egger | let f = parse_rest symtab ts in |

960 | 19f5dad0 | Dirk Pattinson | ID f |

961 | 4fd28192 | Thorsten Wißmann | | A.Kwd "[pi1]" -> |

962 | 0b908205 | Christoph Egger | let f = parse_rest symtab ts in |

963 | 4fd28192 | Thorsten Wißmann | FUS (true, f) |

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

965 | 0b908205 | Christoph Egger | let f = parse_rest symtab ts in |

966 | 4fd28192 | Thorsten Wißmann | FUS (false, f) |

967 | 8334c748 | Christoph Egger | | A.Kwd "μ" -> |

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

969 | c5c25acf | Christoph Egger | let symbol = Stream.next gensym in |

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

971 | 80aa0b2f | Christoph Egger | let f1 = parse_rest newtab ts in |

972 | MU (symbol, f1) |
||

973 | 8334c748 | Christoph Egger | | A.Kwd "ν" -> |

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

975 | c5c25acf | Christoph Egger | let symbol = Stream.next gensym in |

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

977 | 80aa0b2f | Christoph Egger | let f1 = parse_rest newtab ts in |

978 | NU (symbol, f1) |
||

979 | 0aa34675 | Christoph Egger | | A.Kwd "AF" -> |

980 | c5c25acf | Christoph Egger | let f = parse_rest symtab ts in |

981 | AF f |
||

982 | 0aa34675 | Christoph Egger | | A.Kwd "EF" -> |

983 | c5c25acf | Christoph Egger | let f = parse_rest symtab ts in |

984 | EF f |
||

985 | 0aa34675 | Christoph Egger | | A.Kwd "AG" -> |

986 | c5c25acf | Christoph Egger | let f = parse_rest symtab ts in |

987 | AG f |
||

988 | 0aa34675 | Christoph Egger | | A.Kwd "EG" -> |

989 | c5c25acf | Christoph Egger | let f = parse_rest symtab ts in |

990 | EG f |
||

991 | 0aa34675 | Christoph Egger | | A.Kwd "A" -> |

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

993 | let f1 = parse_formula symtab ts in |
||

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

995 | let f2 = parse_formula symtab ts in |
||

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

997 | AU (f1, f2) |
||

998 | 0aa34675 | Christoph Egger | | A.Kwd "E" -> |

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

1000 | let f1 = parse_formula symtab ts in |
||

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

1002 | let f2 = parse_formula symtab ts in |
||

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

1004 | EU (f1, f2) |
||

1005 | 0aa34675 | Christoph Egger | | A.Kwd "AX" -> |

1006 | c5c25acf | Christoph Egger | let f1 = parse_rest symtab ts in |

1007 | AX ("", f1) |
||

1008 | 0aa34675 | Christoph Egger | | A.Kwd "EX" -> |

1009 | c5c25acf | Christoph Egger | let f1 = parse_rest symtab ts in |

1010 | EX ("", f1) |
||

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

1012 | 19f5dad0 | Dirk Pattinson | "\"<\", \"[\", \"{>=\", \"{<=\", \"@\", \"~\", \"(\", |

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

1014 | 8334c748 | Christoph Egger | |

1015 | 4fd28192 | Thorsten Wißmann | (** Parses a sorted formula. |

1016 | @param ts A token stream. |
||

1017 | @return A sorted formula. |
||

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

1019 | *) |
||

1020 | let parse_sortedFormula ts = |
||

1021 | c5c25acf | Christoph Egger | let nr = |

1022 | 4fd28192 | Thorsten Wißmann | match Stream.peek ts with |

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

1024 | if n >= 0 then begin |
||

1025 | Stream.junk ts; |
||

1026 | let () = |
||

1027 | match Stream.next ts with |
||

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

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

1030 | in |
||

1031 | n |
||

1032 | end else |
||

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

1034 | c5c25acf | Christoph Egger | | _ -> 0 |

1035 | 4fd28192 | Thorsten Wißmann | in |

1036 | 0b908205 | Christoph Egger | let f = parse_formula [] ts in |

1037 | 4fd28192 | Thorsten Wißmann | (nr, f) |

1038 | |||

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

1040 | @param ts A token stream. |
||

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

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

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

1044 | *) |
||

1045 | let rec parse_sortedFormulaList ts acc = |
||

1046 | let f1 = parse_sortedFormula ts in |
||

1047 | match Stream.peek ts with |
||

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

1049 | Stream.junk ts; |
||

1050 | parse_sortedFormulaList ts (f1::acc) |
||

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

1052 | |||

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

1054 | @param fkt An import function. |
||

1055 | @param s A string. |
||

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

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

1058 | *) |
||

1059 | let importWrapper fkt s = |
||

1060 | let ts = lexer s in |
||

1061 | try |
||

1062 | let res = fkt ts in |
||

1063 | let _ = |
||

1064 | match Stream.peek ts with |
||

1065 | | None -> () |
||

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

1067 | in |
||

1068 | res |
||

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

1070 | |||

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

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

1073 | @return The resulting formula. |
||

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

1075 | *) |
||

1076 | 0b908205 | Christoph Egger | let importFormula s = importWrapper (parse_formula []) s |

1077 | 4fd28192 | Thorsten Wißmann | |

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

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

1080 | @return The sorted formula. |
||

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

1082 | *) |
||

1083 | let importSortedFormula s = importWrapper parse_sortedFormula s |
||

1084 | |||

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

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

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

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

1089 | f is a sorted formula. |
||

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

1091 | *) |
||

1092 | let importQuery s = |
||

1093 | let fkt ts = |
||

1094 | match Stream.peek ts with |
||

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

1096 | Stream.junk ts; |
||

1097 | let f = parse_sortedFormula ts in |
||

1098 | ([], f) |
||

1099 | | _ -> |
||

1100 | let fl = parse_sortedFormulaList ts [] in |
||

1101 | match Stream.peek ts with |
||

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

1103 | Stream.junk ts; |
||

1104 | let f = parse_sortedFormula ts in |
||

1105 | (fl, f) |
||

1106 | c5c25acf | Christoph Egger | | _ -> |

1107 | 4fd28192 | Thorsten Wißmann | if List.length fl = 1 then ([], List.hd fl) |

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

1109 | in |
||

1110 | importWrapper fkt s |
||

1111 | |||

1112 | |||

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

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

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

1116 | @param f A formula. |
||

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

1118 | that is equivalent to ~f. |
||

1119 | *) |
||

1120 | let rec nnfNeg f = |
||

1121 | match f with |
||

1122 | | TRUE -> FALSE |
||

1123 | | FALSE -> TRUE |
||

1124 | | AP _ -> NOT f |
||

1125 | ff4dc786 | Christoph Egger | | VAR _ -> f |

1126 | 4fd28192 | Thorsten Wißmann | | NOT f1 -> nnf f1 |

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

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

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

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

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

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

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

1134 | f1fa9ad5 | Thorsten Wißmann | | ENFORCES (s, f1) -> ALLOWS (s, nnfNeg f1) |

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

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

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

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

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

1140 | 9bae2c4f | Thorsten Wißmann | | ATLEASTPROB (p, f1) -> LESSPROBFAIL (p, nnfNeg f1) |

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

1142 | c49eea11 | Thorsten Wißmann | | CONST s -> CONSTN s |

1143 | | CONSTN s -> CONST s |
||

1144 | 19f5dad0 | Dirk Pattinson | | ID (f1) -> ID (nnfNeg f1) |

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

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

1147 | c5c25acf | Christoph Egger | | CHC (f1, f2) -> CHC (nnfNeg f1, nnfNeg f2) |

1148 | 4fd28192 | Thorsten Wißmann | | FUS (first, f1) -> FUS (first, nnfNeg f1) |

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

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

1151 | 8cac0897 | Christoph Egger | | AF _ |

1152 | | EF _ |
||

1153 | | AG _ |
||

1154 | | EG _ |
||

1155 | | AU _ |
||

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

1157 | c5c25acf | Christoph Egger | |

1158 | 4fd28192 | Thorsten Wißmann | (** Converts a formula to negation normal form |

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

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

1161 | @param f A formula. |
||

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

1163 | that is equivalent to f. |
||

1164 | *) |
||

1165 | and nnf f = |
||

1166 | match f with |
||

1167 | | TRUE |
||

1168 | | FALSE |
||

1169 | | AP _ |
||

1170 | c49eea11 | Thorsten Wißmann | | NOT (AP _) |

1171 | | CONST _ |
||

1172 | ff4dc786 | Christoph Egger | | CONSTN _ |

1173 | | VAR _ -> f |
||

1174 | 4fd28192 | Thorsten Wißmann | | NOT f1 -> nnfNeg f1 |

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

1176 | let ft1 = nnf f1 in |
||

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

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

1179 | let ft1 = nnf f1 in |
||

1180 | let ft2 = nnf f2 in |
||

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

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

1183 | let ft1 = nnf f1 in |
||

1184 | let ft2 = nnf f2 in |
||

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

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

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

1188 | c5c25acf | Christoph Egger | | EX (s, f1) -> |

1189 | 4fd28192 | Thorsten Wißmann | let ft = nnf f1 in |

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

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

1192 | let ft = nnf f1 in |
||

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

1194 | c5c25acf | Christoph Egger | | ENFORCES (s, f1) -> |

1195 | f1fa9ad5 | Thorsten Wißmann | let ft = nnf f1 in |

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

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

1198 | let ft = nnf f1 in |
||

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

1200 | 4fd28192 | Thorsten Wißmann | | MIN (n, s, f1) -> |

1201 | if n = 0 then TRUE |
||

1202 | else |
||

1203 | let ft = nnf f1 in |
||

1204 | 87926e98 | Thorsten Wißmann | MORETHAN (n-1,s,ft) |

1205 | 4fd28192 | Thorsten Wißmann | | MAX (n, s, f1) -> |

1206 | af276a36 | Thorsten Wißmann | let ft = nnfNeg f1 in |

1207 | MAXEXCEPT (n,s, ft) |
||

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

1209 | 4fd28192 | Thorsten Wißmann | let ft = nnf f1 in |

1210 | af276a36 | Thorsten Wißmann | if ft = f1 then f else MORETHAN (n,s,ft) |

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

1212 | let ft = nnf f1 in |
||

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

1214 | 86b07be8 | Thorsten Wißmann | | ATLEASTPROB (p, f1) -> |

1215 | let ft = nnf f1 in |
||

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

1217 | 9bae2c4f | Thorsten Wißmann | | LESSPROBFAIL (p, f1) -> |

1218 | 86b07be8 | Thorsten Wißmann | let ft = nnf f1 in |

1219 | 9bae2c4f | Thorsten Wißmann | if ft == f1 then f else LESSPROBFAIL (p, ft) |

1220 | 19f5dad0 | Dirk Pattinson | | ID (f1) -> |

1221 | let ft = nnf f1 in |
||

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

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

1224 | let ft1 = nnf f1 in |
||

1225 | let ft2 = nnf f2 in |
||

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

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

1228 | let ft1 = nnf f1 in |
||

1229 | let ft2 = nnf f2 in |
||

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

1231 | 4fd28192 | Thorsten Wißmann | | CHC (f1, f2) -> |

1232 | let ft1 = nnf f1 in |
||

1233 | let ft2 = nnf f2 in |
||

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

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

1236 | let ft = nnf f1 in |
||

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

1238 | ff4dc786 | Christoph Egger | | MU (s, f1) -> |

1239 | let ft = nnf f1 in |
||

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

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

1242 | let ft = nnf f1 in |
||

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

1244 | 8cac0897 | Christoph Egger | | AF _ |

1245 | | EF _ |
||

1246 | | AG _ |
||

1247 | | EG _ |
||

1248 | | AU _ |
||

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

1250 | 4fd28192 | Thorsten Wißmann | |

1251 | (** Simplifies a formula. |
||

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

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

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

1255 | *) |
||

1256 | let rec simplify f = |
||

1257 | match f with |
||

1258 | | TRUE |
||

1259 | | FALSE |
||

1260 | | AP _ |
||

1261 | fbffb079 | Christoph Egger | | NOT (AP _) |

1262 | | VAR _ |
||

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

1264 | 4fd28192 | Thorsten Wißmann | | AT (s, f1) -> |

1265 | let ft = simplify f1 in |
||

1266 | begin |
||

1267 | match ft with |
||

1268 | | FALSE -> FALSE |
||

1269 | | TRUE -> TRUE |
||

1270 | | AT _ -> ft |
||

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

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

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

1274 | end |
||

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

1276 | let ft1 = simplify f1 in |
||

1277 | let ft2 = simplify f2 in |
||

1278 | begin |
||

1279 | match ft1, ft2 with |
||

1280 | | TRUE, _ -> TRUE |
||

1281 | | FALSE, _ -> ft2 |
||

1282 | | _, TRUE -> TRUE |
||

1283 | | _, FALSE -> ft1 |
||

1284 | | _, _ -> |
||

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

1286 | 4fd28192 | Thorsten Wißmann | else OR (ft1, ft2) |

1287 | end |
||

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

1289 | let ft1 = simplify f1 in |
||

1290 | let ft2 = simplify f2 in |
||

1291 | begin |
||

1292 | match ft1, ft2 with |
||

1293 | | TRUE, _ -> ft2 |
||

1294 | | FALSE, _ -> FALSE |
||

1295 | | _, TRUE -> ft1 |
||

1296 | | _, FALSE -> FALSE |
||

1297 | | _, _ -> |
||

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

1299 | 4fd28192 | Thorsten Wißmann | else AND (ft1, ft2) |

1300 | end |
||

1301 | | NOT _ |
||

1302 | | EQU _ |
||

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

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

1305 | let ft = simplify f1 in |
||

1306 | begin |
||

1307 | match ft with |
||

1308 | | FALSE -> FALSE |
||

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

1310 | end |
||

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

1312 | let ft = simplify f1 in |
||

1313 | begin |
||

1314 | match ft with |
||

1315 | | TRUE -> TRUE |
||

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

1317 | end |
||

1318 | f1fa9ad5 | Thorsten Wißmann | | ENFORCES (s, f1) -> |

1319 | let ft = simplify f1 in |
||

1320 | begin |
||

1321 | match ft with |
||

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

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

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

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

1326 | *) |
||

1327 | | TRUE -> TRUE |
||

1328 | | FALSE -> FALSE |
||

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

1330 | end |
||

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

1332 | let ft = simplify f1 in |
||

1333 | begin |
||

1334 | match ft with |
||

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

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

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

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

1339 | *) |
||

1340 | | TRUE -> TRUE |
||

1341 | | FALSE -> FALSE |
||

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

1343 | end |
||

1344 | 4fd28192 | Thorsten Wißmann | | MIN (n, s, f1) -> |

1345 | if n = 0 then TRUE |
||

1346 | else |
||

1347 | let ft = simplify f1 in |
||

1348 | begin |
||

1349 | match ft with |
||

1350 | | FALSE -> FALSE |
||

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

1352 | end |
||

1353 | af276a36 | Thorsten Wißmann | | MORETHAN (n,s,f1) -> |

1354 | let ft = simplify f1 in |
||

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

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

1357 | let ft = simplify f1 in |
||

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

1359 | 4fd28192 | Thorsten Wißmann | | MAX (n, s, f1) -> |

1360 | let ft = simplify f1 in |
||

1361 | begin |
||

1362 | match ft with |
||

1363 | | FALSE -> TRUE |
||

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

1365 | end |
||

1366 | 9bae2c4f | Thorsten Wißmann | | LESSPROBFAIL (p,f1) -> |

1367 | 86b07be8 | Thorsten Wißmann | let ft1 = simplify f1 in |

1368 | 9bae2c4f | Thorsten Wißmann | if (ft1 == f1) then f else LESSPROBFAIL (p,ft1) |

1369 | 86b07be8 | Thorsten Wißmann | | ATLEASTPROB (p,f1) -> |

1370 | let ft1 = simplify f1 in |
||

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

1372 | c49eea11 | Thorsten Wißmann | | CONST _ |

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

1374 | 19f5dad0 | Dirk Pattinson | | ID (f1) -> |

1375 | let ft1 = simplify f1 in |
||

1376 | begin |
||

1377 | match ft1 with |
||

1378 | | TRUE -> TRUE |
||

1379 | | FALSE -> FALSE |
||

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

1381 | end |
||

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

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

1384 | let ft1 = simplify f1 in |
||

1385 | let ft2 = simplify f2 in |
||

1386 | begin |
||

1387 | match ft2 with |
||

1388 | | TRUE -> TRUE |
||

1389 | | _ -> |
||

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

1391 | 19f5dad0 | Dirk Pattinson | else NORM (ft1, ft2) |

1392 | end |
||

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

1394 | let ft1 = simplify f1 in |
||

1395 | let ft2 = simplify f2 in |
||

1396 | begin |
||

1397 | match ft2 with |
||

1398 | | FALSE -> FALSE |
||

1399 | | _ -> |
||

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

1401 | 19f5dad0 | Dirk Pattinson | else NORMN (ft1, ft2) |

1402 | end |
||

1403 | 4fd28192 | Thorsten Wißmann | | CHC (f1, f2) -> |

1404 | let ft1 = simplify f1 in |
||

1405 | let ft2 = simplify f2 in |
||

1406 | begin |
||

1407 | match ft1, ft2 with |
||

1408 | | TRUE, TRUE -> TRUE |
||

1409 | | FALSE, FALSE -> FALSE |
||

1410 | | _, _ -> |
||

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

1412 | 4fd28192 | Thorsten Wißmann | else CHC (ft1, ft2) |

1413 | end |
||

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

1415 | let ft = simplify f1 in |
||

1416 | begin |
||

1417 | match ft with |
||

1418 | | FALSE -> FALSE |
||

1419 | | TRUE -> TRUE |
||

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

1421 | end |
||

1422 | fbffb079 | Christoph Egger | | MU (s, f1) -> |

1423 | let ft = simplify f1 in |
||

1424 | begin |
||

1425 | match ft with |
||

1426 | | TRUE -> TRUE |
||

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

1428 | end |
||

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

1430 | let ft = simplify f1 in |
||

1431 | begin |
||

1432 | match ft with |
||

1433 | | TRUE -> TRUE |
||

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

1435 | end |
||

1436 | 8cac0897 | Christoph Egger | | AF _ |

1437 | | EF _ |
||

1438 | | AG _ |
||

1439 | | EG _ |
||

1440 | | AU _ |
||

1441 | | EU _ -> |
||

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

1443 | 4fd28192 | Thorsten Wißmann | |

1444 | (** Destructs an atomic proposition. |
||

1445 | @param f An atomic proposition. |
||

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

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

1448 | *) |
||

1449 | let dest_ap f = |
||

1450 | match f with |
||

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

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

1453 | |||

1454 | (** Destructs a nominal. |
||

1455 | @param f A nominal. |
||

1456 | @return The name of the nominal |
||

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

1458 | *) |
||

1459 | let dest_nom f = |
||

1460 | match f with |
||

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

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

1463 | |||

1464 | (** Destructs a negation. |
||

1465 | @param f A negation. |
||

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

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

1468 | *) |
||

1469 | let dest_not f = |
||

1470 | match f with |
||

1471 | | NOT f1 -> f1 |
||

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

1473 | |||

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

1475 | @param f An @-formula. |
||

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

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

1478 | *) |
||

1479 | let dest_at f = |
||

1480 | match f with |
||

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

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

1483 | |||

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

1485 | @param f An or-formula. |
||

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

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

1488 | *) |
||

1489 | let dest_or f = |
||

1490 | match f with |
||

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

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

1493 | |||

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

1495 | @param f An and-formula. |
||

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

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

1498 | *) |
||

1499 | let dest_and f = |
||

1500 | match f with |
||

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

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

1503 | |||

1504 | (** Destructs an equivalence. |
||

1505 | @param f An equivalence. |
||

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

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

1508 | *) |
||

1509 | let dest_equ f = |
||

1510 | match f with |
||

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

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

1513 | |||

1514 | (** Destructs an implication. |
||

1515 | @param f An implication. |
||

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

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

1518 | *) |
||

1519 | let dest_imp f = |
||

1520 | match f with |
||

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

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

1523 | |||

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

1525 | @param f An EX-formula. |
||

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

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

1528 | *) |
||

1529 | let dest_ex f = |
||

1530 | match f with |
||

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

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

1533 | |||

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

1535 | @param f An AX-formula. |
||

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

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

1538 | *) |
||

1539 | let dest_ax f = |
||

1540 | match f with |
||

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

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

1543 | |||

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

1545 | @param f A MIN-formula. |
||

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

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

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

1549 | *) |
||

1550 | let dest_min f = |
||

1551 | match f with |
||

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

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

1554 | |||

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

1556 | @param f A MAX-formula. |
||

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

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

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

1560 | *) |
||

1561 | let dest_max f = |
||

1562 | match f with |
||

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

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

1565 | |||

1566 | (** Destructs a choice formula. |
||

1567 | @param f A choice formula. |
||

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

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

1570 | *) |
||

1571 | let dest_choice f = |
||

1572 | match f with |
||

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

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

1575 | |||

1576 | (** Destructs a fusion formula. |
||

1577 | @param f A fusion formula. |
||

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

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

1580 | f1 is the immediate subformulae of f. |
||

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

1582 | *) |
||

1583 | let dest_fusion f = |
||

1584 | match f with |
||

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

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

1587 | |||

1588 | |||

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

1590 | @param f A formula. |
||

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

1592 | *) |
||

1593 | let is_true f = |
||

1594 | match f with |
||

1595 | | TRUE -> true |
||

1596 | | _ -> false |
||

1597 | |||

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

1599 | @param f A formula. |
||

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

1601 | *) |
||

1602 | let is_false f = |
||

1603 | match f with |
||

1604 | | FALSE -> true |
||

1605 | | _ -> false |
||

1606 | |||

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

1608 | @param f A formula. |
||

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

1610 | *) |
||

1611 | let is_ap f = |
||

1612 | match f with |
||

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

1614 | | _ -> false |
||

1615 | |||

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

1617 | @param f A formula. |
||

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

1619 | *) |
||

1620 | let is_nom f = |
||

1621 | match f with |
||

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

1623 | | _ -> false |
||

1624 | |||

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

1626 | @param f A formula. |
||

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

1628 | *) |
||

1629 | let is_not f = |
||

1630 | match f with |
||

1631 | | NOT _ -> true |
||

1632 | | _ -> false |
||

1633 | |||

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

1635 | @param f A formula. |
||

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

1637 | *) |
||

1638 | let is_at f = |
||

1639 | match f with |
||

1640 | | AT _ -> true |
||

1641 | | _ -> false |
||

1642 | |||

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

1644 | @param f A formula. |
||

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

1646 | *) |
||

1647 | let is_or f = |
||

1648 | match f with |
||

1649 | | OR _ -> true |
||

1650 | | _ -> false |
||

1651 | |||

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

1653 | @param f A formula. |
||

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

1655 | *) |
||

1656 | let is_and f = |
||

1657 | match f with |
||

1658 | | AND _ -> true |
||

1659 | | _ -> false |
||

1660 | |||

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

1662 | @param f A formula. |
||

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

1664 | *) |
||

1665 | let is_equ f = |
||

1666 | match f with |
||

1667 | | EQU _ -> true |
||

1668 | | _ -> false |
||

1669 | |||

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

1671 | @param f A formula. |
||

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

1673 | *) |
||

1674 | let is_imp f = |
||

1675 | match f with |
||

1676 | | IMP _ -> true |
||

1677 | | _ -> false |
||

1678 | |||

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

1680 | @param f A formula. |
||

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

1682 | *) |
||

1683 | let is_ex f = |
||

1684 | match f with |
||

1685 | | EX _ -> true |
||

1686 | | _ -> false |
||

1687 | |||

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

1689 | @param f A formula. |
||

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

1691 | *) |
||

1692 | let is_ax f = |
||

1693 | match f with |
||

1694 | | AX _ -> true |
||

1695 | | _ -> false |
||

1696 | |||

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

1698 | @param f A formula. |
||

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

1700 | *) |
||

1701 | let is_min f = |
||

1702 | match f with |
||

1703 | | MIN _ -> true |
||

1704 | | _ -> false |
||

1705 | |||

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

1707 | @param f A formula. |
||

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

1709 | *) |
||

1710 | let is_max f = |
||

1711 | match f with |
||

1712 | | MAX _ -> true |
||

1713 | | _ -> false |
||

1714 | |||

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

1716 | @param f A formula. |
||

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

1718 | *) |
||

1719 | let is_choice f = |
||

1720 | match f with |
||

1721 | | CHC _ -> true |
||

1722 | | _ -> false |
||

1723 | |||

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

1725 | @param f A formula. |
||

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

1727 | *) |
||

1728 | let is_fusion f = |
||

1729 | match f with |
||

1730 | | FUS _ -> true |
||

1731 | | _ -> false |
||

1732 | |||

1733 | c5c25acf | Christoph Egger | |

1734 | 4fd28192 | Thorsten Wißmann | (** The constant True. |

1735 | *) |
||

1736 | let const_true = TRUE |
||

1737 | |||

1738 | (** The constant False. |
||

1739 | *) |
||

1740 | let const_false = FALSE |
||

1741 | c5c25acf | Christoph Egger | |

1742 | 4fd28192 | Thorsten Wißmann | (** Constructs an atomic proposition. |

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

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

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

1746 | *) |
||

1747 | let const_ap s = |
||

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

1749 | else AP s |
||

1750 | |||

1751 | (** Constructs a nominal. |
||

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

1753 | @return A nominal with name s. |
||

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

1755 | *) |
||

1756 | let const_nom s = |
||

1757 | if isNominal s then AP s |
||

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

1759 | |||

1760 | (** Negates a formula. |
||

1761 | @param f A formula. |
||

1762 | @return The negation of f. |
||

1763 | *) |
||

1764 | let const_not f = NOT f |
||

1765 | c5c25acf | Christoph Egger | |

1766 | 4fd28192 | Thorsten Wißmann | (** Constructs an @-formula from a name and a formula. |

1767 | @param s A nominal name. |
||

1768 | @param f A formula. |
||

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

1770 | *) |
||

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

1772 | |||

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

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

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

1776 | @return The formula f1 | f2. |
||

1777 | *) |
||

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

1779 | |||

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

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

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

1783 | @return The formula f1 & f2. |
||

1784 | c5c25acf | Christoph Egger | *) |

1785 | 4fd28192 | Thorsten Wißmann | let const_and f1 f2 = AND (f1, f2) |

1786 | |||

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

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

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

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

1791 | *) |
||

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

1793 | |||

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

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

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

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

1798 | *) |
||

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

1800 | |||

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

1802 | @param s A role name. |
||

1803 | @param f A formula. |
||

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

1805 | *) |
||

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

1807 | |||

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

1809 | @param s A role name. |
||

1810 | @param f A formula. |
||

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

1812 | *) |
||

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

1814 | |||

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

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

1817 | @param s A role name. |
||

1818 | @param f A formula. |
||

1819 | @return The formula MIN f. |
||

1820 | @raise CoAlgException Iff n is negative. |
||

1821 | *) |
||

1822 | let const_min n s f = |
||

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

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

1825 | |||

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

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

1828 | @param s A role name. |
||

1829 | @param f A formula. |
||

1830 | @return The formula MAX f. |
||

1831 | @raise CoAlgException Iff n is negative. |
||

1832 | *) |
||

1833 | let const_max n s f = |
||

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

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

1836 | |||

1837 | 7993e0bf | Thorsten Wißmann | let const_enforces p f = |

1838 | ENFORCES (p,f) |
||

1839 | |||

1840 | let const_allows p f = |
||

1841 | ALLOWS (p,f) |
||

1842 | |||

1843 | 4fd28192 | Thorsten Wißmann | (** Constructs a choice formula from two formulae. |

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

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

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

1847 | *) |
||

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

1849 | |||

1850 | (** Constructs a fusion formula. |
||

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

1852 | @param f1 A formula. |
||

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

1854 | *) |
||

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

1856 | |||

1857 | |||

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

1859 | such that structural and physical equality coincide. |
||

1860 | 87d5082f | Christoph Egger | |

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

1862 | constructs |
||

1863 | 4fd28192 | Thorsten Wißmann | *) |

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

1865 | and hcFormula_node = |
||

1866 | | HCTRUE |
||

1867 | | HCFALSE |
||

1868 | | HCAP of string |
||

1869 | | HCNOT of string |
||

1870 | | HCAT of string * hcFormula |
||

1871 | | HCOR of hcFormula * hcFormula |
||

1872 | | HCAND of hcFormula * hcFormula |
||

1873 | | HCEX of string * hcFormula |
||

1874 | | HCAX of string * hcFormula |
||

1875 | f1fa9ad5 | Thorsten Wißmann | | HCENFORCES of int list * hcFormula |

1876 | | HCALLOWS of int list * hcFormula |
||

1877 | af276a36 | Thorsten Wißmann | | HCMORETHAN of int * string * hcFormula (* GML Diamond *) |

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

1879 | 86b07be8 | Thorsten Wißmann | | HCATLEASTPROB of rational * hcFormula |

1880 | 9bae2c4f | Thorsten Wißmann | | HCLESSPROBFAIL of rational * hcFormula |

1881 | c49eea11 | Thorsten Wißmann | | HCCONST of string |

1882 | | HCCONSTN of string |
||

1883 | 19f5dad0 | Dirk Pattinson | | HCID of hcFormula |

1884 | | HCNORM of hcFormula * hcFormula |
||

1885 | | HCNORMN of hcFormula * hcFormula |
||

1886 | 4fd28192 | Thorsten Wißmann | | HCCHC of hcFormula * hcFormula |

1887 | | HCFUS of bool * hcFormula |
||

1888 | 87d5082f | Christoph Egger | | HCMU of string * hcFormula |

1889 | | HCNU of string * hcFormula |
||

1890 | | HCVAR of string |
||

1891 | 4fd28192 | Thorsten Wißmann | |

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

1893 | @param f1 The first formula node. |
||

1894 | @param f2 The second formula node. |
||

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

1896 | *) |
||

1897 | let equal_hcFormula_node f1 f2 = |
||

1898 | match f1, f2 with |
||

1899 | | HCTRUE, HCTRUE -> true |
||

1900 | | HCFALSE, HCFALSE -> true |
||

1901 | c49eea11 | Thorsten Wißmann | | HCCONST s1, HCCONST s2 |

1902 | | HCCONSTN s1, HCCONSTN s2 |
||

1903 | 4fd28192 | Thorsten Wißmann | | HCAP s1, HCAP s2 |

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

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

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

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

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

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

1910 | bc6db513 | Thorsten Wißmann | | HCENFORCES (s1, f1), HCENFORCES (s2, f2) |

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

1912 | af276a36 | Thorsten Wißmann | | HCMORETHAN (n1, s1, f1), HCMORETHAN (n2, s2, f2) |

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

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

1915 | 86b07be8 | Thorsten Wißmann | | HCATLEASTPROB (p1, f1), HCATLEASTPROB (p2,f2) -> |

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

1917 | 9bae2c4f | Thorsten Wißmann | | HCLESSPROBFAIL (p1, f1), HCLESSPROBFAIL (p2,f2) -> |

1918 | 86b07be8 | Thorsten Wißmann | p1 = p2 && f1 == f2 |

1919 | 19f5dad0 | Dirk Pattinson | | HCID f1, HCID f2 -> f1 == f2 |

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

1921 | 4fd28192 | Thorsten Wißmann | | HCCHC (f1a, f1b), HCCHC (f2a, f2b) -> f1a == f2a && f1b == f2b |

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

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

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

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

1926 | 4fd28192 | Thorsten Wißmann | (* The rest could be shortened to | _ -> false, |

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

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

1929 | | HCTRUE, _ |
||

1930 | | HCFALSE, _ |
||

1931 | | HCAP _, _ |
||

1932 | | HCNOT _, _ |
||

1933 | | HCAT _, _ |
||

1934 | | HCOR _, _ |
||

1935 | | HCAND _, _ |
||

1936 | | HCEX _, _ |
||

1937 | | HCAX _, _ |
||

1938 | f1fa9ad5 | Thorsten Wißmann | | HCENFORCES _, _ |

1939 | | HCALLOWS _, _ |
||

1940 | af276a36 | Thorsten Wißmann | | HCMORETHAN _, _ |

1941 | | HCMAXEXCEPT _, _ |
||

1942 | 86b07be8 | Thorsten Wißmann | | HCATLEASTPROB _, _ |

1943 | 9bae2c4f | Thorsten Wißmann | | HCLESSPROBFAIL _, _ |

1944 | c49eea11 | Thorsten Wißmann | | HCCONST _, _ |

1945 | | HCCONSTN _, _ |
||

1946 | 19f5dad0 | Dirk Pattinson | | HCID _, _ |

1947 | | HCNORM _, _ |
||

1948 | | HCNORMN _, _ |
||

1949 | 4fd28192 | Thorsten Wißmann | | HCCHC _, _ |

1950 | a7ae917b | Christoph Egger | | HCFUS _, _ |

1951 | | HCMU _, _ |
||

1952 | | HCNU _, _ |
||

1953 | | HCVAR _, _ -> false |
||

1954 | 4fd28192 | Thorsten Wißmann | |

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

1956 | @param f A formula node. |
||

1957 | @return The hash value of f. |
||

1958 | *) |
||

1959 | let hash_hcFormula_node f = |
||

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

1961 | 4fd28192 | Thorsten Wißmann | match f with |

1962 | | HCTRUE -> 0 |
||

1963 | | HCFALSE -> 1 |
||

1964 | | HCAP s |
||

1965 | 508e3c33 | Christoph Egger | | HCNOT s |

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

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

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

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

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

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

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

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

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

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

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

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

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

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

1980 | c49eea11 | Thorsten Wißmann | | HCCONST s -> Hashtbl.hash s + 16 |

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

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

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

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

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

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

1987 | 4fd28192 | Thorsten Wißmann | |

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

1989 | @param f A formula node. |
||

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

1991 | *) |
||

1992 | let toFml_hcFormula_node f = |
||

1993 | match f with |
||

1994 | | HCTRUE -> TRUE |
||

1995 | | HCFALSE -> FALSE |
||

1996 | | HCAP s -> AP s |
||

1997 | 508e3c33 | Christoph Egger | | HCVAR s -> VAR s |

1998 | 4fd28192 | Thorsten Wißmann | | HCNOT s -> NOT (AP s) |

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

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

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

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

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

2004 | f1fa9ad5 | Thorsten Wißmann | | HCENFORCES (s, f1) -> ENFORCES (s, f1.HC.fml) |

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

2006 | af276a36 | Thorsten Wißmann | | HCMORETHAN (n, s, f1) -> MORETHAN (n, s, f1.HC.fml) |

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

2008 | 86b07be8 | Thorsten Wißmann | | HCATLEASTPROB (p, f1) -> ATLEASTPROB (p, f1.HC.fml) |

2009 | 9bae2c4f | Thorsten Wißmann | | HCLESSPROBFAIL (p, f1) -> LESSPROBFAIL (p, f1.HC.fml) |

2010 | c49eea11 | Thorsten Wißmann | | HCCONST s -> CONST s |

2011 | | HCCONSTN s -> CONSTN s |
||

2012 | 19f5dad0 | Dirk Pattinson | | HCID (f1) -> ID(f1.HC.fml) |

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

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

2015 | 4fd28192 | Thorsten Wißmann | | HCCHC (f1, f2) -> CHC (f1.HC.fml, f2.HC.fml) |

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

2017 | 508e3c33 | Christoph Egger | | HCMU (var, f1) -> MU (var, f1.HC.fml) |

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

2019 | 4fd28192 | Thorsten Wißmann | |

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

2021 | @param f A formula node. |
||

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

2023 | *) |
||

2024 | let negNde_hcFormula_node f = |
||

2025 | match f with |
||

2026 | | HCTRUE -> HCFALSE |
||

2027 | | HCFALSE -> HCTRUE |
||

2028 | | HCAP s -> HCNOT s |
||

2029 | | HCNOT s -> HCAP s |
||

2030 | 92feed46 | Christoph Egger | | HCVAR s -> f |

2031 | 4fd28192 | Thorsten Wißmann | | HCAT (s, f1) -> HCAT (s, f1.HC.neg) |

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

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

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

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

2036 | f1fa9ad5 | Thorsten Wißmann | | HCENFORCES (s, f2) -> HCALLOWS (s, f2.HC.neg) |

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

2038 | af276a36 | Thorsten Wißmann | | HCMORETHAN (n, s, f1) -> HCMAXEXCEPT (n, s, f1.HC.neg) |

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

2040 | 9bae2c4f | Thorsten Wißmann | | HCATLEASTPROB (p, f1) -> HCLESSPROBFAIL (p, f1.HC.neg) |

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

2042 | c49eea11 | Thorsten Wißmann | | HCCONST s -> HCCONSTN s |

2043 | | HCCONSTN s -> HCCONST s |
||

2044 | 19f5dad0 | Dirk Pattinson | | HCID (f1) -> HCID(f1.HC.neg) |

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

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

2047 | d58bba0f | Dirk Pattinson | | HCCHC (f1, f2) -> HCCHC (f1.HC.neg, f2.HC.neg) |

2048 | 4fd28192 | Thorsten Wißmann | | HCFUS (first, f1) -> HCFUS (first, f1.HC.neg) |

2049 | 92feed46 | Christoph Egger | | HCMU (name, f1) -> HCNU (name, f1.HC.neg) |

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

2051 | 4fd28192 | Thorsten Wißmann | |

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

2053 | *) |
||

2054 | module HcFormula = HC.Make( |
||

2055 | struct |
||

2056 | type nde = hcFormula_node |
||

2057 | type fml = formula |
||

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

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

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

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

2062 | end |
||

2063 | ) |
||

2064 | |||

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

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

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

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

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

2070 | *) |
||

2071 | let rec hc_formula hcF f = |
||

2072 | match f with |
||

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

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

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

2076 | 508e3c33 | Christoph Egger | | VAR s -> HcFormula.hashcons hcF (HCVAR s) |

2077 | 4fd28192 | Thorsten Wißmann | | NOT (AP s) -> HcFormula.hashcons hcF (HCNOT s) |

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

2079 | let tf1 = hc_formula hcF f1 in |
||

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

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

2082 | let tf1 = hc_formula hcF f1 in |
||

2083 | let tf2 = hc_formula hcF f2 in |
||

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

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

2086 | let tf1 = hc_formula hcF f1 in |
||

2087 | let tf2 = hc_formula hcF f2 in |
||

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

2089 | | NOT _ |
||

2090 | | EQU _ |
||

2091 | af276a36 | Thorsten Wißmann | | MIN _ |

2092 | | MAX _ |
||

2093 | 4fd28192 | Thorsten Wißmann | | IMP _ -> raise (CoAlgException "Formula is not in negation normal form.") |

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

2095 | let tf1 = hc_formula hcF f1 in |
||

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

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

2098 | let tf1 = hc_formula hcF f1 in |
||

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

2100 | f1fa9ad5 | Thorsten Wißmann | | ENFORCES (s, f1) -> |

2101 | let tf1 = hc_formula hcF f1 in |
||

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

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

2104 | let tf1 = hc_formula hcF f1 in |
||

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

2106 | af276a36 | Thorsten Wißmann | | MORETHAN (n, s, f1) -> |

2107 | 4fd28192 | Thorsten Wißmann | let tf1 = hc_formula hcF f1 in |

2108 | af276a36 | Thorsten Wißmann | HcFormula.hashcons hcF (HCMORETHAN (n, s, tf1)) |

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

2110 | 4fd28192 | Thorsten Wißmann | let tf1 = hc_formula hcF f1 in |

2111 | af276a36 | Thorsten Wißmann | HcFormula.hashcons hcF (HCMAXEXCEPT (n, s, tf1)) |

2112 | 86b07be8 | Thorsten Wißmann | | ATLEASTPROB (p, f1) -> |

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

2114 | 9bae2c4f | Thorsten Wißmann | | LESSPROBFAIL (p, f1) -> |

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

2116 | c49eea11 | Thorsten Wißmann | | CONST s -> |

2117 | HcFormula.hashcons hcF (HCCONST s) |
||

2118 | | CONSTN s -> |
||

2119 | HcFormula.hashcons hcF (HCCONSTN s) |
||

2120 | 19f5dad0 | Dirk Pattinson | | ID f1 -> |

2121 | let tf1 = hc_formula hcF f1 in |
||

2122 | HcFormula.hashcons hcF (HCID tf1) |
||

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

2124 | let tf1 = hc_formula hcF f1 in |
||

2125 | let tf2 = hc_formula hcF f2 in |
||

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

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

2128 | let tf1 = hc_formula hcF f1 in |
||

2129 | let tf2 = hc_formula hcF f2 in |
||

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

2131 | 4fd28192 | Thorsten Wißmann | | CHC (f1, f2) -> |

2132 | let tf1 = hc_formula hcF f1 in |
||

2133 | let tf2 = hc_formula hcF f2 in |
||

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

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

2136 | let tf1 = hc_formula hcF f1 in |
||

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

2138 | 508e3c33 | Christoph Egger | | MU (var, f1) -> |

2139 | c5c25acf | Christoph Egger | let tf1 = hc_formula hcF f1 in |

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

2141 | 508e3c33 | Christoph Egger | | NU (var, f1) -> |

2142 | c5c25acf | Christoph Egger | let tf1 = hc_formula hcF f1 in |

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

2144 | 8cac0897 | Christoph Egger | | AF _ |

2145 | | EF _ |
||

2146 | | AG _ |
||

2147 | | EG _ |
||

2148 | | AU _ |
||

2149 | | EU _ -> |
||

2150 | c5c25acf | Christoph Egger | raise (CoAlgException ("nnf: CTL should have been removed at this point")) |

2151 | 4fd28192 | Thorsten Wißmann | |

2152 | cc07e93d | Christoph Egger | (* Replace the Variable name in f with formula formula |

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

2154 | *) |
||

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

2156 | let func = hc_replace hcF name formula in |
||

2157 | let gennew = HcFormula.hashcons hcF in |
||

2158 | match f.HC.node with |
||

2159 | | HCTRUE |
||

2160 | | HCFALSE |
||

2161 | | HCAP _ |
||

2162 | | HCNOT _ |
||

2163 | | HCCONST _ |
||

2164 | | HCCONSTN _ -> f |
||

2165 | | HCVAR s -> |
||

2166 | c5c25acf | Christoph Egger | if compare s name == 0 |

2167 | then formula |
||

2168 | else f |
||

2169 | cc07e93d | Christoph Egger | | HCAT (s, f1) -> |

2170 | c5c25acf | Christoph Egger | let nf1 = func f1 in |

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

2172 | cc07e93d | Christoph Egger | | HCOR (f1, f2) -> |

2173 | c5c25acf | Christoph Egger | let nf1 = func f1 in |

2174 | let nf2 = func f2 in |
||

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

2176 | cc07e93d | Christoph Egger | | HCAND (f1, f2) -> |

2177 | c5c25acf | Christoph Egger | let nf1 = func f1 in |

2178 | let nf2 = func f2 in |
||

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

2180 | cc07e93d | Christoph Egger | | HCEX (s, f1) -> |

2181 | c5c25acf | Christoph Egger | let nf1 = func f1 in |

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

2183 | cc07e93d | Christoph Egger | | HCAX (s, f1) -> |

2184 | let nf1 = func f1 in |
||

2185 | c5c25acf | Christoph Egger | if nf1 == f1 then f else gennew (HCAX(s, nf1)) |

2186 | cc07e93d | Christoph Egger | | HCENFORCES (s, f1) -> |

2187 | c5c25acf | Christoph Egger | let nf1 = func f1 in |

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

2189 | cc07e93d | Christoph Egger | | HCALLOWS (s, f1) -> |

2190 | let nf1 = func f1 in |
||

2191 | c5c25acf | Christoph Egger | if nf1 == f1 then f else gennew (HCALLOWS(s, nf1)) |

2192 | cc07e93d | Christoph Egger | | HCMORETHAN (n, s, f1) -> |

2193 | let nf1 = func f1 in |
||

2194 | c5c25acf | Christoph Egger | if nf1 == f1 then f else gennew (HCMORETHAN(n, s, nf1)) |

2195 | cc07e93d | Christoph Egger | | HCMAXEXCEPT (n, s, f1) -> |

2196 | c5c25acf | Christoph Egger | let nf1 = func f1 in |

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

2198 | cc07e93d | Christoph Egger | | HCATLEASTPROB (p, f1) -> |

2199 | let nf1 = func f1 in |
||

2200 | c5c25acf | Christoph Egger | if nf1 == f1 then f else gennew (HCATLEASTPROB(p, nf1)) |

2201 | cc07e93d | Christoph Egger | | HCLESSPROBFAIL (p, f1) -> |

2202 | let nf1 = func f1 in |
||

2203 | c5c25acf | Christoph Egger | if nf1 == f1 then f else gennew (HCLESSPROBFAIL(p, nf1)) |

2204 | cc07e93d | Christoph Egger | | HCID f1 -> |

2205 | let nf1 = func f1 in |
||

2206 | c5c25acf | Christoph Egger | if nf1 == f1 then f else gennew (HCID(nf1)) |

2207 | cc07e93d | Christoph Egger | | HCNORM (f1, f2) -> |

2208 | c5c25acf | Christoph Egger | let nf1 = func f1 in |

2209 | let nf2 = func f2 in |
||

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

2211 | cc07e93d | Christoph Egger | | HCNORMN (f1, f2) -> |

2212 | c5c25acf | Christoph Egger | let nf1 = func f1 in |

2213 | let nf2 = func f2 in |
||

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

2215 | cc07e93d | Christoph Egger | | HCCHC (f1, f2) -> |

2216 | c5c25acf | Christoph Egger | let nf1 = func f1 in |

2217 | let nf2 = func f2 in |
||

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

2219 | cc07e93d | Christoph Egger | | HCFUS (first, f1) -> |

2220 | let nf1 = func f1 in |
||

2221 | c5c25acf | Christoph Egger | if nf1 == f1 then f else gennew (HCFUS(first, nf1)) |

2222 | cc07e93d | Christoph Egger | | HCMU (var, f1) -> |

2223 | c5c25acf | Christoph Egger | if compare var name != 0 then |

2224 | 854e1338 | Christoph Egger | let nf1 = func f1 in |

2225 | c5c25acf | Christoph Egger | if nf1 == f1 then f else gennew (HCMU(var, nf1)) |

2226 | else |
||

2227 | f |
||

2228 | cc07e93d | Christoph Egger | | HCNU (var, f1) -> |

2229 | c5c25acf | Christoph Egger | if compare var name != 0 then |

2230 | 854e1338 | Christoph Egger | let nf1 = func f1 in |

2231 | c5c25acf | Christoph Egger | if nf1 == f1 then f else gennew (HCNU(var, nf1)) |

2232 | else |
||

2233 | f |
||

2234 | cc07e93d | Christoph Egger | |

2235 | 5e7c8aa1 | Christoph Egger | let rec hc_freeIn variable (f: hcFormula) = |

2236 | match f.HC.node with |
||

2237 | | HCTRUE |
||

2238 | | HCFALSE |
||

2239 | | HCAP _ |
||

2240 | | HCNOT _ |
||

2241 | | HCCONST _ |
||

2242 | | HCCONSTN _ -> false |
||

2243 | | HCVAR s -> |
||

2244 | if compare variable s == 0 |
||

2245 | then true |
||

2246 | else false |
||

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

2248 | hc_freeIn variable f1 |
||

2249 | | HCOR (f1, f2) |
||

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

2251 | hc_freeIn variable f1 || hc_freeIn variable f2 |
||

2252 | | HCEX (_, f1) |
||

2253 | | HCAX (_, f1) |
||

2254 | | HCENFORCES (_, f1) |
||

2255 | | HCALLOWS (_, f1) |
||

2256 | | HCMORETHAN (_, _, f1) |
||

2257 | | HCMAXEXCEPT (_, _, f1) |
||

2258 | | HCATLEASTPROB (_, f1) |
||

2259 | | HCLESSPROBFAIL (_, f1) |
||

2260 | | HCID f1 -> |
||

2261 | hc_freeIn variable f1 |
||

2262 | | HCNORM (f1, f2) |
||

2263 | | HCNORMN (f1, f2) |
||

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

2265 | hc_freeIn variable f1 || hc_freeIn variable f2 |
||

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

2267 | hc_freeIn variable f1 |
||

2268 | | HCMU (var, f1) |
||

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

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

2271 | hc_freeIn variable f1 |
||

2272 | |||

2273 | cc07e93d | Christoph Egger | |

2274 | 4fd28192 | Thorsten Wißmann | (** An instantiation of a hash table (of the standard library) |

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

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

2277 | *) |
||

2278 | module HcFHt = Hashtbl.Make( |
||

2279 | struct |
||

2280 | type t = hcFormula |
||

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

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

2283 | end |
||

2284 | ) |