Project

General

Profile

Statistics
| Branch: | Revision:

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

History | View | Annotate | Download (13.6 KB)

1
(** 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
  | MultiModalKD
15
  | Monotone
16
  | CoalitionLogic
17
  | GML
18
  | PML
19
  | Constant of string list
20
  | Identity
21
  | DefaultImplication
22
  | Choice
23
  | Fusion
24

    
25
(* 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
val string_of_functor : functors -> string
32

    
33
(* This type may be extended for additional logics. *)
34
type formulaType =
35
  | Other
36
  | TrueFalseF
37
  | AndF
38
  | OrF
39
  | AtF
40
  | NomF
41
  | ExF
42
  | AxF
43
  | EnforcesF
44
  | AllowsF
45
  | MoreThanF
46
  | MaxExceptF
47
  | AtLeastProbF (* diamond for PML *)
48
  | LessProbFailF (* box for PML *)
49
  | ConstF (* constant functor *)
50
  | ConstnF (* constant functor *)
51
  | IdF (* Identity functor *)
52
  | NormF (* Default Implication *)
53
  | NormnF (* negation normal form of default implication *)
54
  | ChcF
55
  | FusF
56
  | MuF
57
  | NuF
58

    
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
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
and stateExpander = unit -> ruleEnumeration
88

    
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

    
99
and rule = (dependencies * (sort * bset * bset) lazylist)
100

    
101
and 'a lazyliststep =
102
  | MultipleElements of 'a list
103
  | SingleElement    of 'a
104
  | NoMoreElements
105

    
106
(* 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

    
115
val listFromLazylist : 'a lazylist -> 'a list
116

    
117
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
type propagateElement = (* TODO: What does the prefix "U" mean? unsat? *)
130
  | 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
(* 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

    
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
val queuePrettyStatus : unit -> string
170

    
171
val setPropagationCounter : int -> unit
172
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
val graphFindState : sort -> (bset * bset) -> state option
186
val graphFindCore : sort -> (bset * bset) -> core option
187
val graphFindCnstr : cset -> constrnt option
188
val graphInsertState : sort -> (bset * bset) -> state -> unit
189
val graphInsertCore : sort -> (bset * bset) -> core -> unit
190
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
(** Generate a graphviz dot description of the current reasoner graph *)
199
val graphToDot : unit -> string
200

    
201

    
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
val cssIter : (cset -> unit) -> csetSet -> unit
215

    
216
(*****************************************************************************)
217
(*      "Module type" and a specific implementation of state nodes           *)
218
(*****************************************************************************)
219

    
220
val stateMake : sort -> bset -> bset -> stateExpander -> state
221
val stateGetSort : state -> sort
222
val stateGetBs : state -> bset
223
val stateSetBs : state -> bset -> unit
224
val stateGetDeferral : state -> bset
225
val stateSetDeferral : state -> bset -> unit
226
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
val stateNextRule : state -> ruleEnumeration
236
val stateToString : state -> string
237
val stateGetIdx : state -> int
238

    
239

    
240
(*****************************************************************************)
241
(*      "Module type" and a specific implementation of core nodes            *)
242
(*****************************************************************************)
243

    
244
val coreMake : sort -> bset -> bset -> Minisat.solver option -> fht -> core
245
val coreGetSort : core -> sort
246
val coreGetBs : core -> bset
247
val coreSetBs : core -> bset -> unit
248
val coreGetDeferral : core -> bset
249
val coreSetDeferral : core -> bset -> unit
250
val coreGetStatus : core -> nodeStatus
251
val coreSetStatus : core -> nodeStatus -> unit
252
val coreGetParents : core -> (state * int) list
253
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

    
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
val coreDeallocateSolver : core -> unit
264
val coreGetFht : core -> fht
265
val coreGetIdx : core -> int
266
val coreGetConstraintParents : core -> cset list
267
val coreAddConstraintParent : core -> cset -> unit
268
val coreToString : core -> string
269

    
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
val setCopyState : setState -> setState
279
val setCopyCore : setCore -> setCore
280
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
val setLengthState : setState -> int
294
val setLengthCore : setCore -> int
295

    
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
val bsetMake : unit -> bset (* a new bset which only contains True *)
323
val bsetMakeRealEmpty : unit -> bset (* a new bset without containing True *)
324
val bsetSingleton : localFormula -> bset
325
val bsetAdd : bset -> localFormula -> unit
326
val bsetMem : bset -> localFormula -> bool
327
val bsetRem : bset -> int -> unit
328
val bsetCompare : bset -> bset -> int
329
val bsetFold : (localFormula -> 'a -> 'a) -> bset -> 'a -> 'a
330
val bsetIter : (localFormula -> unit) -> bset -> unit
331
val bsetFilter : bset -> (localFormula -> bool) -> bset
332
val bsetAddTBox : sort -> bset -> bset
333
val bsetCopy : bset -> bset
334
val bsetToString : sort -> bset -> string
335

    
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
val csetToString : sort -> cset -> string
346

    
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
val lfGetDeferral : sort -> localFormula -> int
358
val lfGetDestNum : sort -> localFormula -> int
359
val lfGetDestNum2 : sort -> localFormula -> int
360
val lfGetDestAg : sort -> localFormula -> int array
361
val lfGetNeg : sort -> localFormula -> localFormula option
362
val lfGetAt : nominal -> localFormula -> atFormula
363
val lfToInt : localFormula -> int
364
val lfFromInt : int -> localFormula
365
val lfGetFormula : sort -> localFormula -> CoAlgFormula.formula
366

    
367
val atFormulaGetSubformula : atFormula -> localFormula
368
val atFormulaGetNominal : atFormula -> nominal
369

    
370
val lfToAt : sort -> localFormula -> atFormula
371

    
372
(** 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
type fragment_spec = Auto | Fragment of fragment
380

    
381
(** Return the fragment of the mu-calculus that the original formula uses *)
382
val getFragment : unit -> fragment
383

    
384
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
(** [ppFormulae fragment nomTbl tbox sf] initializes the array representation and various
387
    tables for the formula.
388
  
389
   @return (simplified NNF of f, simplified nnf of tbox, bitset containing f)
390
 *)
391
val ppFormulae : fragment_spec -> (string -> sort option) -> CoAlgFormula.sortedFormula list
392
                 -> CoAlgFormula.sortedFormula
393
                 -> CoAlgFormula.sortedFormula list * CoAlgFormula.sortedFormula * bset
394

    
395

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