Project

General

Profile

Statistics
| Branch: | Revision:

cool / src / lib / CoAlgMisc.mli @ 1d36cd07

History | View | Annotate | Download (13.6 KB)

1 4fd28192 Thorsten Wißmann
(** Common types, functions, and data structures for the CoAlgebraic reasoner.
2
    @author Florian Widmann
3
 *)
4
5
6
(*****************************************************************************)
7
(*     Types that can be modified rather easily                              *)
8
(*     (of course you then have to modify the implementations below too)     *)
9
(*****************************************************************************)
10
11
(* This type has to be extended for additional logics. *)
12
type functors =
13
  | MultiModalK
14 a87192e8 Thorsten Wißmann
  | MultiModalKD
15 f4e43751 Christoph Egger
  | Monotone
16 f1fa9ad5 Thorsten Wißmann
  | CoalitionLogic
17 29b2e3f3 Thorsten Wißmann
  | GML
18 86b07be8 Thorsten Wißmann
  | PML
19 5e0983fe Thorsten Wißmann
  | Constant of string list
20 19f5dad0 Dirk Pattinson
  | Identity
21
  | DefaultImplication
22 4fd28192 Thorsten Wißmann
  | Choice
23
  | Fusion
24
25 5e0983fe Thorsten Wißmann
(* functors whose constructor takes additional parameters *)
26
type parametricFunctorName =
27
  | NameConstant
28
29
val functor_of_string : string -> string list -> functors option
30
val unaryfunctor_of_string : string -> string list -> functors option
31 db23edf7 Thorsten Wißmann
val string_of_functor : functors -> string
32
33 4fd28192 Thorsten Wißmann
(* This type may be extended for additional logics. *)
34
type formulaType =
35
  | Other
36 3b055ae8 dirk
  | TrueFalseF
37 4fd28192 Thorsten Wißmann
  | AndF
38
  | OrF
39
  | AtF
40
  | NomF
41
  | ExF
42
  | AxF
43 f1fa9ad5 Thorsten Wißmann
  | EnforcesF
44
  | AllowsF
45 af276a36 Thorsten Wißmann
  | MoreThanF
46
  | MaxExceptF
47 9bae2c4f Thorsten Wißmann
  | AtLeastProbF (* diamond for PML *)
48
  | LessProbFailF (* box for PML *)
49 c49eea11 Thorsten Wißmann
  | ConstF (* constant functor *)
50
  | ConstnF (* constant functor *)
51 19f5dad0 Dirk Pattinson
  | IdF (* Identity functor *)
52
  | NormF (* Default Implication *)
53
  | NormnF (* negation normal form of default implication *)
54 4fd28192 Thorsten Wißmann
  | ChcF
55
  | FusF
56 3b407438 Christoph Egger
  | MuF
57
  | NuF
58 4fd28192 Thorsten Wißmann
59
type localFormula
60
type bset
61
62
type atFormula
63
type cset
64
type csetSet
65
66
type lht
67
type fht
68
type nht
69
70
type state
71
72
type core
73
74
type setState
75
76
type setCore
77
78
type setCnstr
79
80
(*****************************************************************************)
81
(*                Types that are hard coded into the algorithm               *)
82
(*****************************************************************************)
83
84 269d93e5 Thorsten Wißmann
and 'a junction = | Disjunctive of 'a (*specifies that any of the 'a needs to be satifsfied *)
85
                  | Conjunctive of 'a (*specifies that all of the 'a need  to be satifsfied *)
86
87 b36e57bc Thorsten Wißmann
and stateExpander = unit -> ruleEnumeration
88 4fd28192 Thorsten Wißmann
89
and sort = CoAlgFormula.sort
90
91
and nodeStatus =
92
  | Expandable
93
  | Open
94
  | Sat
95
  | Unsat
96
97
and dependencies = bset list -> bset
98 269d93e5 Thorsten Wißmann
99 16af388e Christoph Egger
and rule = (dependencies * (sort * bset * bset) lazylist)
100 269d93e5 Thorsten Wißmann
101 a9949a25 Thorsten Wißmann
and 'a lazyliststep =
102 69243f7f Thorsten Wißmann
  | MultipleElements of 'a list
103
  | SingleElement    of 'a
104
  | NoMoreElements
105
106 a9949a25 Thorsten Wißmann
(* a lazylist returns on successive calls the entire list until it eventually
107
   returns NoMoreElements
108
*)
109
and 'a lazylist = unit -> 'a lazyliststep
110
111
and ruleEnumeration = rule lazyliststep
112
113
val lazylistFromList : 'a list -> 'a lazylist
114 4fd28192 Thorsten Wißmann
115 672429b4 Thorsten Wißmann
val listFromLazylist : 'a lazylist -> 'a list
116
117 4fd28192 Thorsten Wißmann
type nominal = sort * localFormula
118
119
type node =
120
  | State of state
121
  | Core of core
122
123
type constrnt =
124
  | UnsatC
125
  | SatC
126
  | OpenC of node list
127
  | UnexpandedC of node list
128
129 269d93e5 Thorsten Wißmann
type propagateElement = (* TODO: What does the prefix "U" mean? unsat? *)
130 4fd28192 Thorsten Wißmann
  | UState of state * int option
131
  | UCore of core * bool
132
  | UCnstr of cset
133
134
type queueElement =
135
  | QState of state
136
  | QCore of core
137
  | QCnstr of cset
138
  | QEmpty
139
140
type sortTable = (functors * int list) array
141
142
exception CoAlg_finished of bool
143
144
145
val sortTable : sortTable ref
146
147 269d93e5 Thorsten Wißmann
(* evaluate a junction in the obvious way *)
148
val junctionEvalBool : bool list junction -> bool
149
val junctionEval: ('a -> bool) -> 'a list junction -> bool
150
val optionalizeOperator: ('a -> 'b -> 'c) -> ('a option -> 'b option -> 'c option)
151
val junctionEvalBoolOption : bool option list junction -> bool option
152
153
(* decompose a junction in it's content and its constructor,
154
   such that: eval∘junctionExtract = id
155
   (with eval: X × (X -> Y) -> Y)
156
 *)
157
val junctionExtract: 'a junction -> ('a * ('b -> 'b junction))
158 4fd28192 Thorsten Wißmann
159
(*****************************************************************************)
160
(*      "Module type" and a specific implementation of the main queue        *)
161
(*****************************************************************************)
162
163
val queueInit : unit -> unit
164
val queueIsEmpty : unit -> bool
165
val queueInsertState : state -> unit
166
val queueInsertCore : core -> unit
167
val queueInsertCnstr : cset -> unit
168
val queueGetElement : unit -> queueElement
169 c2cc0c2e Thorsten Wißmann
val queuePrettyStatus : unit -> string
170 4fd28192 Thorsten Wißmann
171 55dc0a64 Christoph Egger
val setPropagationCounter : int -> unit
172 4fd28192 Thorsten Wißmann
val doNominalPropagation : unit -> bool
173
val doSatPropagation : unit -> bool
174
175
176
(*****************************************************************************)
177
(*        "Module type" and a specific implementation of the graph           *)
178
(*****************************************************************************)
179
180
val graphInit : unit -> unit
181
val graphIterStates : (state -> unit) -> unit
182
val graphIterCores : (core -> unit) -> unit
183
val graphIterCnstrs : (cset -> constrnt -> unit) -> unit
184
val graphClearCnstr : unit -> unit
185 16af388e Christoph Egger
val graphFindState : sort -> (bset * bset) -> state option
186
val graphFindCore : sort -> (bset * bset) -> core option
187 4fd28192 Thorsten Wißmann
val graphFindCnstr : cset -> constrnt option
188 16af388e Christoph Egger
val graphInsertState : sort -> (bset * bset) -> state -> unit
189
val graphInsertCore : sort -> (bset * bset) -> core -> unit
190 4fd28192 Thorsten Wißmann
val graphInsertCnstr : cset -> constrnt -> unit
191
val graphReplaceCnstr : cset -> constrnt -> unit
192
val graphSizeState : unit -> int
193
val graphSizeCore : unit -> int
194
val graphSizeCnstr : unit -> int
195
val graphAddRoot : core -> unit
196
val graphGetRoot : unit -> core
197
198 86c2c2ee Hans-Peter Deifel
(** Generate a graphviz dot description of the current reasoner graph *)
199
val graphToDot : unit -> string
200
201 4fd28192 Thorsten Wißmann
202
(*****************************************************************************)
203
(*     "Module type" and a specific implementation of sets of constraints    *)
204
(*****************************************************************************)
205
206
val cssEmpty : csetSet
207
val cssExists : (cset -> bool) -> csetSet -> bool
208
val cssForall : (cset -> bool) -> csetSet -> bool
209
val cssUnion : csetSet -> csetSet -> csetSet
210
val cssAdd : cset -> csetSet -> csetSet
211
val cssFold : (cset -> 'a -> 'a) -> csetSet -> 'a -> 'a
212
val cssSingleton : cset -> csetSet
213
val cssEqual : csetSet -> csetSet -> bool
214 f335015f Thorsten Wißmann
val cssIter : (cset -> unit) -> csetSet -> unit
215 4fd28192 Thorsten Wißmann
216
(*****************************************************************************)
217
(*      "Module type" and a specific implementation of state nodes           *)
218
(*****************************************************************************)
219
220 3285ac30 Christoph Egger
val stateMake : sort -> bset -> bset -> stateExpander -> state
221 4fd28192 Thorsten Wißmann
val stateGetSort : state -> sort
222
val stateGetBs : state -> bset
223
val stateSetBs : state -> bset -> unit
224 3285ac30 Christoph Egger
val stateGetDeferral : state -> bset
225
val stateSetDeferral : state -> bset -> unit
226 4fd28192 Thorsten Wißmann
val stateGetStatus : state -> nodeStatus
227
val stateSetStatus : state -> nodeStatus -> unit
228
val stateGetParents : state -> core list
229
val stateAddParent : state -> core -> unit
230
val stateGetRule : state -> int -> dependencies * core list
231
val stateGetRules : state -> (dependencies * core list) list
232
val stateAddRule : state -> dependencies -> core list -> int
233
val stateGetConstraints : state -> csetSet
234
val stateSetConstraints : state -> csetSet -> unit
235 b36e57bc Thorsten Wißmann
val stateNextRule : state -> ruleEnumeration
236 73762b19 Thorsten Wißmann
val stateToString : state -> string
237
val stateGetIdx : state -> int
238 4fd28192 Thorsten Wißmann
239
240
(*****************************************************************************)
241
(*      "Module type" and a specific implementation of core nodes            *)
242
(*****************************************************************************)
243
244 9f1263ec Christoph Egger
val coreMake : sort -> bset -> bset -> Minisat.solver option -> fht -> core
245 4fd28192 Thorsten Wißmann
val coreGetSort : core -> sort
246
val coreGetBs : core -> bset
247 b9a8d969 Christoph Egger
val coreSetBs : core -> bset -> unit
248 3285ac30 Christoph Egger
val coreGetDeferral : core -> bset
249 b9a8d969 Christoph Egger
val coreSetDeferral : core -> bset -> unit
250 4fd28192 Thorsten Wißmann
val coreGetStatus : core -> nodeStatus
251
val coreSetStatus : core -> nodeStatus -> unit
252 b9a8d969 Christoph Egger
val coreGetParents : core -> (state * int) list
253 4fd28192 Thorsten Wißmann
val coreAddParent : core -> state -> int -> unit
254
val coreGetChildren : core -> state list
255
val coreAddChild : core -> state -> unit
256
val coreGetConstraints : core -> csetSet
257
val coreSetConstraints : core -> csetSet -> unit
258 e0e6eb62 Hans-Peter Deifel
259
(** Return minisat solver of a core, if allocated
260
   @raise Failure if no solver is allocated for this core
261
 *)
262
val coreGetSolver : core -> Minisat.solver
263 9f1263ec Christoph Egger
val coreDeallocateSolver : core -> unit
264 4fd28192 Thorsten Wißmann
val coreGetFht : core -> fht
265 73762b19 Thorsten Wißmann
val coreGetIdx : core -> int
266 4fd28192 Thorsten Wißmann
val coreGetConstraintParents : core -> cset list
267
val coreAddConstraintParent : core -> cset -> unit
268 f335015f Thorsten Wißmann
val coreToString : core -> string
269 4fd28192 Thorsten Wißmann
270
271
(*****************************************************************************)
272
(*      "Module type" and a specific implementation of sets of               *)
273
(*      states, cores, and constraints for the sat propagation               *)
274
(*****************************************************************************)
275
276
val setEmptyState : unit -> setState
277
val setEmptyCore : unit -> setCore
278 5956a56d Christoph Egger
val setCopyState : setState -> setState
279
val setCopyCore : setCore -> setCore
280 4fd28192 Thorsten Wißmann
val setEmptyCnstr : unit -> setCnstr
281
val setAddState : setState -> state -> unit
282
val setAddCore : setCore -> core -> unit
283
val setAddCnstr : setCnstr -> cset -> unit
284
val setMemState : setState -> state -> bool
285
val setMemCore : setCore -> core -> bool
286
val setMemCnstr : setCnstr -> cset -> bool
287
val setRemoveState : setState -> state -> unit
288
val setRemoveCore : setCore -> core -> unit
289
val setRemoveCnstr : setCnstr -> cset -> unit
290
val setIterState : (state -> unit) -> setState -> unit
291
val setIterCore : (core -> unit) -> setCore -> unit
292
val setIterCnstr : (cset -> unit) -> setCnstr -> unit
293 50df1dc2 Christoph Egger
val setLengthState : setState -> int
294
val setLengthCore : setCore -> int
295 4fd28192 Thorsten Wißmann
296
297
(*****************************************************************************)
298
(*        "Module type" and a specific implementation of the mapping         *)
299
(*        between (local) formulae and literals of the sat solver,           *)
300
(*        and of a mapping of nominals to sets of formulae                   *)
301
(*****************************************************************************)
302
303
val lhtInit : unit -> lht
304
val lhtAdd : lht -> Minisat.lit -> localFormula -> unit
305
val lhtFind : lht -> Minisat.lit -> localFormula option
306
307
val fhtInit : unit -> fht
308
val fhtAdd : fht -> localFormula -> Minisat.lit -> unit
309
val fhtFind : fht -> localFormula -> Minisat.lit option
310
311
val nhtInit : unit -> nht
312
val nhtAdd : nht -> nominal -> bset -> unit
313
val nhtFind : nht -> nominal -> bset option
314
val nhtFold : (nominal -> bset -> 'a -> 'a) -> nht -> 'a -> 'a
315
316
317
(*****************************************************************************)
318
(*         "Module type" and a specific implementation of sets of            *)
319
(*         local formulae and @-formulae                                     *)
320
(*****************************************************************************)
321
322 45d554b0 Thorsten Wißmann
val bsetMake : unit -> bset (* a new bset which only contains True *)
323
val bsetMakeRealEmpty : unit -> bset (* a new bset without containing True *)
324 e7aaefa9 Hans-Peter Deifel
val bsetSingleton : localFormula -> bset
325 4fd28192 Thorsten Wißmann
val bsetAdd : bset -> localFormula -> unit
326
val bsetMem : bset -> localFormula -> bool
327 f20718d2 Christoph Egger
val bsetRem : bset -> int -> unit
328 16af388e Christoph Egger
val bsetCompare : bset -> bset -> int
329 4fd28192 Thorsten Wißmann
val bsetFold : (localFormula -> 'a -> 'a) -> bset -> 'a -> 'a
330
val bsetIter : (localFormula -> unit) -> bset -> unit
331 e4cd869a Thorsten Wißmann
val bsetFilter : bset -> (localFormula -> bool) -> bset
332 4fd28192 Thorsten Wißmann
val bsetAddTBox : sort -> bset -> bset
333 b7c3a47e Thorsten Wißmann
val bsetCopy : bset -> bset
334 f335015f Thorsten Wißmann
val bsetToString : sort -> bset -> string
335 4fd28192 Thorsten Wißmann
336
val csetMake : unit -> cset
337
val csetAdd : cset -> atFormula -> unit
338
val csetCopy : cset -> cset
339
val csetUnion : cset -> cset -> cset
340
val csetHasDot : cset -> bool
341
val csetAddDot : cset -> unit
342
val csetRemDot : cset -> unit
343
val csetAddTBox : sort -> cset -> bset
344
val csetIter : cset -> (atFormula -> unit) -> unit
345 f335015f Thorsten Wißmann
val csetToString : sort -> cset -> string
346 4fd28192 Thorsten Wißmann
347
348
(*****************************************************************************)
349
(*            "Module type" and a specific implementation of                 *)
350
(*            local formulae and @-formulae                                  *)
351
(*****************************************************************************)
352
353
val lfGetType : sort -> localFormula -> formulaType
354
val lfGetDest1 : sort -> localFormula -> localFormula
355
val lfGetDest2 : sort -> localFormula -> localFormula
356
val lfGetDest3 : sort -> localFormula -> int
357 c67aca42 Christoph Egger
val lfGetDeferral : sort -> localFormula -> int
358 29b2e3f3 Thorsten Wißmann
val lfGetDestNum : sort -> localFormula -> int
359 eda515b6 Thorsten Wißmann
val lfGetDestNum2 : sort -> localFormula -> int
360 f1fa9ad5 Thorsten Wißmann
val lfGetDestAg : sort -> localFormula -> int array
361 4fd28192 Thorsten Wißmann
val lfGetNeg : sort -> localFormula -> localFormula option
362
val lfGetAt : nominal -> localFormula -> atFormula
363 a0cffef0 Thorsten Wißmann
val lfToInt : localFormula -> int
364
val lfFromInt : int -> localFormula
365 f335015f Thorsten Wißmann
val lfGetFormula : sort -> localFormula -> CoAlgFormula.formula
366 4fd28192 Thorsten Wißmann
367
val atFormulaGetSubformula : atFormula -> localFormula
368
val atFormulaGetNominal : atFormula -> nominal
369
370
val lfToAt : sort -> localFormula -> atFormula
371
372 b6653b96 Hans-Peter Deifel
(** Sum of different fragments of the full mu-calculus.
373
 
374
   Used by the reasoner to select between different specific algorithms for
375
   individual fragments.
376
 *)
377
type fragment = AlternationFree | AconjunctiveAltFree
378
379 f24367c4 Hans-Peter Deifel
type fragment_spec = Auto | Fragment of fragment
380
381 b6653b96 Hans-Peter Deifel
(** Return the fragment of the mu-calculus that the original formula uses *)
382
val getFragment : unit -> fragment
383
384 89613c41 Kristin Braun
val detClosure : string list -> (string -> int option) -> CoAlgFormula.HcFormula.t -> unit CoAlgFormula.HcFHt.t array -> string CoAlgFormula.HcFHt.t array -> unit CoAlgFormula.HcFHt.t -> (string,int) Hashtbl.t -> int -> CoAlgFormula.hcFormula -> unit
385
386 f24367c4 Hans-Peter Deifel
(** [ppFormulae fragment nomTbl tbox sf] initializes the array representation and various
387 b6653b96 Hans-Peter Deifel
    tables for the formula.
388
  
389
   @return (simplified NNF of f, simplified nnf of tbox, bitset containing f)
390
 *)
391 f24367c4 Hans-Peter Deifel
val ppFormulae : fragment_spec -> (string -> sort option) -> CoAlgFormula.sortedFormula list
392
                 -> CoAlgFormula.sortedFormula
393
                 -> CoAlgFormula.sortedFormula list * CoAlgFormula.sortedFormula * bset
394 f335015f Thorsten Wißmann
395 a57eb439 Hans-Peter Deifel
396
(* vim: set et sw=2 sts=2 ts=8 : *)