## cool / src / lib / CoAlgFormula.mli @ 946e8213

History | View | Annotate | Download (6.47 KB)

1 |
(** 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 |
type rational = { nominator: int; denominator: int } |

12 | |

13 |
val rational_of_int : int -> int -> rational |

14 | |

15 |
type formula = |

16 |
| TRUE |

17 |
| FALSE |

18 |
| AP of string (* named atom *) |

19 |
| NOT of formula |

20 |
| AT of string * formula (* @ *) |

21 |
| OR of formula * formula |

22 |
| AND of formula * formula |

23 |
| 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 |
| 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 *) |

34 |
(* probability of at least 50% *) |

35 |
| LESSPROBFAIL of rational * formula (* = [1/2] C = {< 1/2} ¬ C ---> C fails with *) |

36 |
(* 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 |
| 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 |
| CHC of formula * formula |

43 |
| FUS of bool * formula |

44 |
| MU of string * formula |

45 |
| NU of string * formula |

46 |
| VAR of string |

47 |
| 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 |
| AR of formula * formula |

54 |
| ER of formula * formula |

55 |
| AB of formula * formula |

56 |
| EB of formula * formula |

57 | |

58 |
exception ConversionException of formula |

59 | |

60 |
type sortedFormula = sort * formula |

61 | |

62 |
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 |
val convertToMu : formula -> formula (* tries to convert a formula to a pure Mu formula *) |

67 | |

68 |
val isNominal : string -> bool |

69 | |

70 |
val sizeFormula : formula -> int |

71 |
val sizeSortedFormula : sortedFormula -> int |

72 | |

73 |
val string_of_formula : formula -> string |

74 |
val exportFormula : formula -> string |

75 |
val exportTatlFormula : formula -> string |

76 |
val exportSortedFormula : sortedFormula -> string |

77 |
val exportQuery : sortedFormula list -> sortedFormula -> string |

78 |
val exportQueryParsable : sortedFormula list -> sortedFormula -> string |

79 |
val importFormula : string -> formula |

80 |
val importSortedFormula : string -> sortedFormula |

81 |
val importQuery : string -> sortedFormula list * sortedFormula |

82 | |

83 |
(** Decides whether a fomula is aconjunctive. |

84 | |

85 |
A formula is aconjunctive if for every conjunction (a ʌ b), at most one of |

86 |
the conjuncts a, b contains a free μ-variable. *) |

87 |
val isMuAconjunctive : formula -> bool |

88 | |

89 |
val verifyFormula : formula -> unit |

90 | |

91 |
val nnfNeg : formula -> formula |

92 |
val nnf : formula -> formula |

93 | |

94 |
val simplify : formula -> formula |

95 | |

96 |
val dest_ap : formula -> string |

97 |
val dest_nom : formula -> string |

98 |
val dest_not : formula -> formula |

99 |
val dest_at : formula -> string * formula |

100 |
val dest_or : formula -> formula * formula |

101 |
val dest_and : formula -> formula * formula |

102 |
val dest_equ : formula -> formula * formula |

103 |
val dest_imp : formula -> formula * formula |

104 |
val dest_ex : formula -> string * formula |

105 |
val dest_ax : formula -> string * formula |

106 |
val dest_min : formula -> int * string * formula |

107 |
val dest_max : formula -> int * string * formula |

108 |
val dest_choice : formula -> formula * formula |

109 |
val dest_fusion : formula -> bool * formula |

110 | |

111 |
val is_true : formula -> bool |

112 |
val is_false : formula -> bool |

113 |
val is_ap : formula -> bool |

114 |
val is_nom : formula -> bool |

115 |
val is_not : formula -> bool |

116 |
val is_at : formula -> bool |

117 |
val is_or : formula -> bool |

118 |
val is_and : formula -> bool |

119 |
val is_equ : formula -> bool |

120 |
val is_imp : formula -> bool |

121 |
val is_ex : formula -> bool |

122 |
val is_ax : formula -> bool |

123 |
val is_min : formula -> bool |

124 |
val is_max : formula -> bool |

125 |
val is_choice : formula -> bool |

126 |
val is_fusion : formula -> bool |

127 | |

128 |
val const_true : formula |

129 |
val const_false : formula |

130 |
val const_ap : string -> formula |

131 |
val const_nom : string -> formula |

132 |
val const_not : formula -> formula |

133 |
val const_at : string -> formula -> formula |

134 |
val const_or : formula -> formula -> formula |

135 |
val const_and : formula -> formula -> formula |

136 |
val const_equ : formula -> formula -> formula |

137 |
val const_imp : formula -> formula -> formula |

138 |
val const_ex : string -> formula -> formula |

139 |
val const_ax : string -> formula -> formula |

140 |
val const_min : int -> string -> formula -> formula |

141 |
val const_max : int -> string -> formula -> formula |

142 |
val const_enforces : int list -> formula -> formula |

143 |
val const_allows : int list -> formula -> formula |

144 |
val const_choice : formula -> formula -> formula |

145 |
val const_fusion : bool -> formula -> formula |

146 | |

147 |
type hcFormula = (hcFormula_node, formula) HashConsing.hash_consed |

148 |
and hcFormula_node = |

149 |
| HCTRUE |

150 |
| HCFALSE |

151 |
| HCAP of string |

152 |
| HCNOT of string |

153 |
| HCAT of string * hcFormula |

154 |
| HCOR of hcFormula * hcFormula |

155 |
| HCAND of hcFormula * hcFormula |

156 |
| HCEX of string * hcFormula |

157 |
| HCAX of string * hcFormula |

158 |
| HCENFORCES of int list * hcFormula |

159 |
| HCALLOWS of int list * hcFormula |

160 |
| HCMORETHAN of int * string * hcFormula (* GML Diamond *) |

161 |
| HCMAXEXCEPT of int * string * hcFormula (* GML Box *) |

162 |
| HCATLEASTPROB of rational * hcFormula |

163 |
| HCLESSPROBFAIL of rational * hcFormula (* the probability for failing is less than ... *) |

164 |
| HCCONST of string |

165 |
| HCCONSTN of string |

166 |
| HCID of hcFormula |

167 |
| HCNORM of hcFormula * hcFormula |

168 |
| HCNORMN of hcFormula * hcFormula |

169 |
| HCCHC of hcFormula * hcFormula |

170 |
| HCFUS of bool * hcFormula |

171 |
| HCMU of string * hcFormula |

172 |
| HCNU of string * hcFormula |

173 |
| HCVAR of string |

174 | |

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

176 | |

177 |
val hc_formula : HcFormula.t -> formula -> hcFormula |

178 |
val hc_replace : HcFormula.t -> string -> hcFormula -> hcFormula -> hcFormula |

179 |
val hc_freeIn : string -> hcFormula -> bool |

180 | |

181 |
module HcFHt : (Hashtbl.S with type key = hcFormula) |

182 | |

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