Project

General

Profile

Statistics
| Branch: | Revision:

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

History | View | Annotate | Download (6.54 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
exception CoAlgException of string
8
9
type sort = int
10
11 e5422169 Thorsten Wißmann
type rational = { nominator: int; denominator: int }
12
13
val rational_of_int : int -> int -> rational
14
15 4fd28192 Thorsten Wißmann
type formula =
16
  | TRUE
17
  | FALSE
18 0247525c Thorsten Wißmann
  | AP of string (* named atom *)
19 4fd28192 Thorsten Wißmann
  | NOT of formula
20 0247525c Thorsten Wißmann
  | AT of string * formula (* @ *)
21 4fd28192 Thorsten Wißmann
  | OR of formula * formula
22
  | AND of formula * formula
23 0247525c Thorsten Wißmann
  | EQU of formula * formula (* equivalence <=> *)
24
  | IMP of formula * formula (* implication <-> *)
25
  | EX of string * formula (* exists, diamond of K *)
26
  | AX of string * formula (* forall, box of K *)
27
  | ENFORCES of int list * formula (* CL *)
28
  | ALLOWS   of int list * formula (* CL *)
29
  | MIN of int * string * formula (* some more intuitive diamond for GML *)
30
  | MAX of int * string * formula (* some more intuitive box for GML *)
31 af276a36 Thorsten Wißmann
  | MORETHAN of int * string * formula (* diamond of GML *)
32 dbcce612 Thorsten Wißmann
  | MAXEXCEPT of int * string * formula (* box of GML, means: ¬>_nR.¬C *)
33 c855ba91 Thorsten Wißmann
  | ATLEASTPROB of rational * formula (* = {>= 1/2} C  ---> C occurs with *)
34 e5422169 Thorsten Wißmann
                                      (*  probability of at least 50% *) 
35 9bae2c4f Thorsten Wißmann
  | LESSPROBFAIL of rational * formula (* = [1/2] C = {< 1/2} ¬ C ---> C fails with *)
36 c49eea11 Thorsten Wißmann
                                       (* probability of less than 50% *)
37
  | CONST of string  (* constant functor with value string *)
38
  | CONSTN of string  (* constant functor with value other than string *)
39 19f5dad0 Dirk Pattinson
  | ID of formula (* modality of the identity functor *)
40
  | NORM of formula * formula (* default implication *)
41
  | NORMN of formula * formula (* \neg NORM (\neg A, \neg B) *)
42 4fd28192 Thorsten Wißmann
  | CHC of formula * formula
43
  | FUS of bool * formula
44 d29d35f7 Christoph Egger
  | MU of string * formula
45
  | NU of string * formula
46 9a3b23cc Christoph Egger
  | VAR of string
47 b179a57f Christoph Egger
  | AF of formula
48
  | EF of formula
49
  | AG of formula
50
  | EG of formula
51
  | AU of formula * formula
52
  | EU of formula * formula
53 e30caa42 Christoph Egger
  | AR of formula * formula
54
  | ER of formula * formula
55 97d73a78 Christoph Egger
  | AB of formula * formula
56
  | EB of formula * formula
57 4fd28192 Thorsten Wißmann
58 ca99d0c6 Thorsten Wißmann
exception ConversionException of formula
59
60 4fd28192 Thorsten Wißmann
type sortedFormula = sort * formula
61
62 dbcce612 Thorsten Wißmann
val iter : (formula -> unit) -> formula -> unit (* iterate over all sub formulas *)
63
val convert_post : (formula -> formula) -> formula -> formula (* run over all subformulas in post order *)
64
val convertToK : formula -> formula (* tries to convert a formula to a pure K formula *)
65
val convertToGML : formula -> formula (* tries to convert a formula to a pure GML formula *)
66 946e8213 Kristin Braun
val convertToMu : formula -> formula (* tries to convert a formula to a pure Mu formula *)
67 dbcce612 Thorsten Wißmann
68 4fd28192 Thorsten Wißmann
val isNominal : string -> bool
69
70
val sizeFormula : formula -> int
71
val sizeSortedFormula : sortedFormula -> int
72 1d36cd07 Kristin Braun
val depthFormula : formula -> int
73 4fd28192 Thorsten Wißmann
74 ca99d0c6 Thorsten Wißmann
val string_of_formula : formula -> string
75 4fd28192 Thorsten Wißmann
val exportFormula : formula -> string
76 01b1ab69 Thorsten Wißmann
val exportTatlFormula : formula -> string
77 4fd28192 Thorsten Wißmann
val exportSortedFormula : sortedFormula -> string
78
val exportQuery : sortedFormula list -> sortedFormula -> string
79 b59059c4 Thorsten Wißmann
val exportQueryParsable : sortedFormula list -> sortedFormula -> string
80 4fd28192 Thorsten Wißmann
val importFormula : string -> formula
81
val importSortedFormula : string -> sortedFormula
82
val importQuery : string -> sortedFormula list * sortedFormula
83
84 b6653b96 Hans-Peter Deifel
(** Decides whether a fomula is aconjunctive.
85
86
   A formula is aconjunctive if for every conjunction (a ʌ b), at most one of
87
   the conjuncts a, b contains a free μ-variable. *)
88
val isMuAconjunctive : formula -> bool
89
90 1484d8cb Christoph Egger
val verifyFormula : formula -> unit
91
92 bc0691dc Kristin Braun
val equals: formula -> formula -> bool
93 4fd28192 Thorsten Wißmann
val nnfNeg : formula -> formula
94
val nnf : formula -> formula
95
96
val simplify : formula -> formula
97
98
val dest_ap : formula -> string
99
val dest_nom : formula -> string
100
val dest_not : formula -> formula
101
val dest_at : formula -> string * formula
102
val dest_or : formula -> formula * formula
103
val dest_and : formula -> formula * formula
104
val dest_equ : formula -> formula * formula
105
val dest_imp : formula -> formula * formula
106
val dest_ex : formula -> string * formula
107
val dest_ax : formula -> string * formula
108
val dest_min : formula -> int * string * formula
109
val dest_max : formula -> int * string * formula
110
val dest_choice : formula -> formula * formula
111
val dest_fusion : formula -> bool * formula
112
113
val is_true : formula -> bool
114
val is_false : formula -> bool
115
val is_ap : formula -> bool
116
val is_nom : formula -> bool
117
val is_not : formula -> bool
118
val is_at : formula -> bool
119
val is_or : formula -> bool
120
val is_and : formula -> bool
121
val is_equ : formula -> bool
122
val is_imp : formula -> bool
123
val is_ex : formula -> bool
124
val is_ax : formula -> bool
125
val is_min : formula -> bool
126
val is_max : formula -> bool
127
val is_choice : formula -> bool
128
val is_fusion : formula -> bool
129 dbcce612 Thorsten Wißmann
130 4fd28192 Thorsten Wißmann
val const_true : formula
131
val const_false : formula
132
val const_ap : string -> formula
133
val const_nom : string -> formula
134
val const_not : formula -> formula
135
val const_at : string -> formula -> formula
136
val const_or : formula -> formula -> formula
137
val const_and : formula -> formula -> formula
138
val const_equ : formula -> formula -> formula
139
val const_imp : formula -> formula -> formula
140
val const_ex : string -> formula -> formula
141
val const_ax : string -> formula -> formula
142
val const_min : int -> string -> formula -> formula
143
val const_max : int -> string -> formula -> formula
144 7993e0bf Thorsten Wißmann
val const_enforces : int list -> formula -> formula
145
val const_allows : int list -> formula -> formula
146 4fd28192 Thorsten Wißmann
val const_choice : formula -> formula -> formula
147
val const_fusion : bool -> formula -> formula
148
149
type hcFormula = (hcFormula_node, formula) HashConsing.hash_consed
150
and hcFormula_node =
151
  | HCTRUE
152
  | HCFALSE
153
  | HCAP of string
154
  | HCNOT of string
155
  | HCAT of string * hcFormula
156
  | HCOR of hcFormula * hcFormula
157
  | HCAND of hcFormula * hcFormula
158
  | HCEX of string * hcFormula
159
  | HCAX of string * hcFormula
160 f1fa9ad5 Thorsten Wißmann
  | HCENFORCES of int list * hcFormula
161
  | HCALLOWS of int list * hcFormula
162 af276a36 Thorsten Wißmann
  | HCMORETHAN of int * string * hcFormula (* GML Diamond *)
163
  | HCMAXEXCEPT of int * string * hcFormula (* GML Box *)
164 86b07be8 Thorsten Wißmann
  | HCATLEASTPROB of rational * hcFormula
165 9bae2c4f Thorsten Wißmann
  | HCLESSPROBFAIL of rational * hcFormula (* the probability for failing is less than ... *)
166 c49eea11 Thorsten Wißmann
  | HCCONST of string
167
  | HCCONSTN of string
168 19f5dad0 Dirk Pattinson
  | HCID of hcFormula
169
  | HCNORM of hcFormula * hcFormula
170
  | HCNORMN of hcFormula * hcFormula
171 4fd28192 Thorsten Wißmann
  | HCCHC of hcFormula * hcFormula
172
  | HCFUS of bool * hcFormula
173 87d5082f Christoph Egger
  | HCMU of string * hcFormula
174
  | HCNU of string * hcFormula
175
  | HCVAR of string
176 4fd28192 Thorsten Wißmann
177
module HcFormula : (HashConsing.S with type nde = hcFormula_node and type fml = formula)
178
179
val hc_formula : HcFormula.t -> formula -> hcFormula
180 cc07e93d Christoph Egger
val hc_replace : HcFormula.t -> string -> hcFormula -> hcFormula -> hcFormula
181 5e7c8aa1 Christoph Egger
val hc_freeIn : string -> hcFormula -> bool
182 4fd28192 Thorsten Wißmann
183
module HcFHt : (Hashtbl.S with type key = hcFormula)
184 a57eb439 Hans-Peter Deifel
185
(* vim: set et sw=2 sts=2 ts=8 : *)