CoAlgFormula.mli 7 KB
Newer Older
Thorsten Wißmann's avatar
Thorsten Wißmann committed
1
2
3
4
5
6
7
8
9
10
(** This module implements coalgebraic formulae
    (e.g. parsing, printing, (de-)constructing, ...).
    @author Florian Widmann
 *)


exception CoAlgException of string

type sort = int

Thorsten Wißmann's avatar
Thorsten Wißmann committed
11
12
13
14
type rational = { nominator: int; denominator: int }

val rational_of_int : int -> int -> rational

Thorsten Wißmann's avatar
Thorsten Wißmann committed
15
16
17
type formula =
  | TRUE
  | FALSE
18
  | AP of string (* named atom *)
Thorsten Wißmann's avatar
Thorsten Wißmann committed
19
  | NOT of formula
20
  | AT of string * formula (* @ *)
Thorsten Wißmann's avatar
Thorsten Wißmann committed
21
22
  | OR of formula * formula
  | AND of formula * formula
23
24
25
26
27
28
29
30
  | EQU of formula * formula (* equivalence <=> *)
  | IMP of formula * formula (* implication <-> *)
  | EX of string * formula (* exists, diamond of K *)
  | AX of string * formula (* forall, box of K *)
  | ENFORCES of int list * formula (* CL *)
  | ALLOWS   of int list * formula (* CL *)
  | MIN of int * string * formula (* some more intuitive diamond for GML *)
  | MAX of int * string * formula (* some more intuitive box for GML *)
31
  | MORETHAN of int * string * formula (* diamond of GML *)
32
  | MAXEXCEPT of int * string * formula (* box of GML, means: ¬>_nR.¬C *)
33
  | ATLEASTPROB of rational * formula (* = {>= 1/2} C  ---> C occurs with *)
Thorsten Wißmann's avatar
Thorsten Wißmann committed
34
                                      (*  probability of at least 50% *) 
35
  | LESSPROBFAIL of rational * formula (* = [1/2] C = {< 1/2} ¬ C ---> C fails with *)
36
37
38
                                       (* probability of less than 50% *)
  | CONST of string  (* constant functor with value string *)
  | CONSTN of string  (* constant functor with value other than string *)
39
40
41
  | ID of formula (* modality of the identity functor *)
  | NORM of formula * formula (* default implication *)
  | NORMN of formula * formula (* \neg NORM (\neg A, \neg B) *)
Thorsten Wißmann's avatar
Thorsten Wißmann committed
42
43
  | CHC of formula * formula
  | FUS of bool * formula
44
45
  | MU of string * formula
  | NU of string * formula
46
  | VAR of string
Christoph Egger's avatar
Christoph Egger committed
47
48
49
50
51
52
  | AF of formula
  | EF of formula
  | AG of formula
  | EG of formula
  | AU of formula * formula
  | EU of formula * formula
53
54
  | AR of formula * formula
  | ER of formula * formula
55
56
  | AB of formula * formula
  | EB of formula * formula
Thorsten Wißmann's avatar
Thorsten Wißmann committed
57

58
59
exception ConversionException of formula

Thorsten Wißmann's avatar
Thorsten Wißmann committed
60
61
type sortedFormula = sort * formula

62
63
64
65
val iter : (formula -> unit) -> formula -> unit (* iterate over all sub formulas *)
val convert_post : (formula -> formula) -> formula -> formula (* run over all subformulas in post order *)
val convertToK : formula -> formula (* tries to convert a formula to a pure K formula *)
val convertToGML : formula -> formula (* tries to convert a formula to a pure GML formula *)
66
val convertToMu : formula -> formula (* tries to convert a formula to a pure Mu formula *)
67

Thorsten Wißmann's avatar
Thorsten Wißmann committed
68
69
70
71
val isNominal : string -> bool

val sizeFormula : formula -> int
val sizeSortedFormula : sortedFormula -> int
72
val depthFormula : formula -> int
Thorsten Wißmann's avatar
Thorsten Wißmann committed
73

74
val string_of_formula : formula -> string
Thorsten Wißmann's avatar
Thorsten Wißmann committed
75
val exportFormula : formula -> string
76
val exportTatlFormula : formula -> string
Thorsten Wißmann's avatar
Thorsten Wißmann committed
77
78
val exportSortedFormula : sortedFormula -> string
val exportQuery : sortedFormula list -> sortedFormula -> string
79
val exportQueryParsable : sortedFormula list -> sortedFormula -> string
Thorsten Wißmann's avatar
Thorsten Wißmann committed
80
81
82
83
val importFormula : string -> formula
val importSortedFormula : string -> sortedFormula
val importQuery : string -> sortedFormula list * sortedFormula

84
85
86
87
88
89
(** Decides whether a fomula is aconjunctive.

   A formula is aconjunctive if for every conjunction (a ʌ b), at most one of
   the conjuncts a, b contains a free μ-variable. *)
val isMuAconjunctive : formula -> bool

90
val verifyFormula : formula -> unit
Merlin's avatar
Merlin committed
91
val verifyMuAltFree : formula -> string * string list
92

93
val equals: formula -> formula -> bool
Thorsten Wißmann's avatar
Thorsten Wißmann committed
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
val nnfNeg : formula -> formula
val nnf : formula -> formula

val simplify : formula -> formula

val dest_ap : formula -> string
val dest_nom : formula -> string
val dest_not : formula -> formula
val dest_at : formula -> string * formula
val dest_or : formula -> formula * formula
val dest_and : formula -> formula * formula
val dest_equ : formula -> formula * formula
val dest_imp : formula -> formula * formula
val dest_ex : formula -> string * formula
val dest_ax : formula -> string * formula
val dest_min : formula -> int * string * formula
val dest_max : formula -> int * string * formula
val dest_choice : formula -> formula * formula
val dest_fusion : formula -> bool * formula

val is_true : formula -> bool
val is_false : formula -> bool
val is_ap : formula -> bool
val is_nom : formula -> bool
val is_not : formula -> bool
val is_at : formula -> bool
val is_or : formula -> bool
val is_and : formula -> bool
val is_equ : formula -> bool
val is_imp : formula -> bool
val is_ex : formula -> bool
val is_ax : formula -> bool
val is_min : formula -> bool
val is_max : formula -> bool
val is_choice : formula -> bool
val is_fusion : formula -> bool
130

Thorsten Wißmann's avatar
Thorsten Wißmann committed
131
132
133
134
135
136
137
138
139
140
141
142
143
144
val const_true : formula
val const_false : formula
val const_ap : string -> formula
val const_nom : string -> formula
val const_not : formula -> formula
val const_at : string -> formula -> formula
val const_or : formula -> formula -> formula
val const_and : formula -> formula -> formula
val const_equ : formula -> formula -> formula
val const_imp : formula -> formula -> formula
val const_ex : string -> formula -> formula
val const_ax : string -> formula -> formula
val const_min : int -> string -> formula -> formula
val const_max : int -> string -> formula -> formula
145
146
val const_enforces : int list -> formula -> formula
val const_allows : int list -> formula -> formula
Thorsten Wißmann's avatar
Thorsten Wißmann committed
147
148
149
150
151
152
153
154
155
156
157
158
159
160
val const_choice : formula -> formula -> formula
val const_fusion : bool -> formula -> formula

type hcFormula = (hcFormula_node, formula) HashConsing.hash_consed
and hcFormula_node =
  | HCTRUE
  | HCFALSE
  | HCAP of string
  | HCNOT of string
  | HCAT of string * hcFormula
  | HCOR of hcFormula * hcFormula
  | HCAND of hcFormula * hcFormula
  | HCEX of string * hcFormula
  | HCAX of string * hcFormula
Thorsten Wißmann's avatar
Thorsten Wißmann committed
161
162
  | HCENFORCES of int list * hcFormula
  | HCALLOWS of int list * hcFormula
163
164
  | HCMORETHAN of int * string * hcFormula (* GML Diamond *)
  | HCMAXEXCEPT of int * string * hcFormula (* GML Box *)
165
  | HCATLEASTPROB of rational * hcFormula
166
  | HCLESSPROBFAIL of rational * hcFormula (* the probability for failing is less than ... *)
167
168
  | HCCONST of string
  | HCCONSTN of string
169
170
171
  | HCID of hcFormula
  | HCNORM of hcFormula * hcFormula
  | HCNORMN of hcFormula * hcFormula
Thorsten Wißmann's avatar
Thorsten Wißmann committed
172
173
  | HCCHC of hcFormula * hcFormula
  | HCFUS of bool * hcFormula
174
175
176
  | HCMU of string * hcFormula
  | HCNU of string * hcFormula
  | HCVAR of string
Thorsten Wißmann's avatar
Thorsten Wißmann committed
177
178
179
180

module HcFormula : (HashConsing.S with type nde = hcFormula_node and type fml = formula)

val hc_formula : HcFormula.t -> formula -> hcFormula
181
val hc_replace : HcFormula.t -> string -> hcFormula -> hcFormula -> hcFormula
182
val hc_freeIn : string -> hcFormula -> bool
Thorsten Wißmann's avatar
Thorsten Wißmann committed
183

184
185
186
187
188
(* Variant of freeIn that respects bound variables
   FIXME: Merge into regular freeIn
 *)
val hc_freeIn2 : string -> hcFormula -> bool

Thorsten Wißmann's avatar
Thorsten Wißmann committed
189
module HcFHt : (Hashtbl.S with type key = hcFormula)
190

Simon Prucker's avatar
Simon Prucker committed
191
192
193
(**
Parses a formula into a tree representation, where each node contains a connective. The tree structure then supports simplification and recombination of formulae.    
**)
194
195
val parseFormulaToTree: formula -> formula CoolUtils.Tree.tree

Simon Prucker's avatar
Simon Prucker committed
196
197
val formula_of_string: string -> formula

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