1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
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
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
|
#ifndef _JH_KNOWLEDGE_KNOWLEDGE_H_
#define _JH_KNOWLEDGE_KNOWLEDGE_H_
#include "../core/char_types.h"
#include "../core/index_types.h"
#include "../error/error.h"
#include "knowledge_types.h"
int JH_knowledge_readlock_words
(
struct JH_knowledge k [const restrict static 1],
FILE io [const restrict static 1]
);
int JH_knowledge_writelock_words
(
struct JH_knowledge k [const restrict static 1],
FILE io [const restrict static 1]
);
int JH_knowledge_readunlock_words
(
struct JH_knowledge k [const restrict static 1],
FILE io [const restrict static 1]
);
int JH_knowledge_writeunlock_words
(
struct JH_knowledge k [const restrict static 1],
FILE io [const restrict static 1]
);
int JH_knowledge_readlock_word
(
struct JH_knowledge k [const restrict static 1],
const JH_index i,
FILE io [const restrict static 1]
);
int JH_knowledge_writelock_word
(
struct JH_knowledge k [const restrict static 1],
const JH_index i,
FILE io [const restrict static 1]
);
int JH_knowledge_readunlock_word
(
struct JH_knowledge k [const restrict static 1],
const JH_index i,
FILE io [const restrict static 1]
);
int JH_knowledge_writeunlock_word
(
struct JH_knowledge k [const restrict static 1],
const JH_index i,
FILE io [const restrict static 1]
);
int JH_knowledge_readlock_sequences
(
struct JH_knowledge k [const restrict static 1],
FILE io [const restrict static 1]
);
int JH_knowledge_writelock_sequences
(
struct JH_knowledge k [const restrict static 1],
FILE io [const restrict static 1]
);
int JH_knowledge_readunlock_sequences
(
struct JH_knowledge k [const restrict static 1],
FILE io [const restrict static 1]
);
int JH_knowledge_writeunlock_sequences
(
struct JH_knowledge k [const restrict static 1],
FILE io [const restrict static 1]
);
/*@
requires (\block_length(k) >= 1);
// Returns zero on success, -1 on failure.
assigns \result;
ensures ((\result == 0) || (\result == -1));
// On success, all fields of {*k} are set.
ensures ((\result == 0) ==> \valid(k));
// On success, the two reserved words are learnt.
ensures ((\result == 0) ==> (k->words_length == 2));
// On success, the mutex is initialized and unlocked.
ensures ((\result == 0) ==> (k->mutex == 1));
// At least some fields of k are set in any case.
assigns (*k);
@*/
int JH_knowledge_initialize (struct JH_knowledge k [const restrict static 1]);
void JH_knowledge_finalize (struct JH_knowledge k [const restrict static 1]);
/*
* When returning 0:
* {word} was added to {k}, or was already there.
* {*result} indicates where {word} is in {k->words}.
*
* When returning -1:
* Something went wrong when adding the occurrence of {word} to {k}.
* {k} remains semantically unchanged.
* {*result} may or may not have been altered.
*/
int JH_knowledge_learn_word
(
struct JH_knowledge k [const static 1],
const JH_char word [const restrict static 1],
const size_t word_length,
JH_index result [const restrict static 1],
FILE io [const restrict static 1]
);
int JH_knowledge_learn_sequence
(
struct JH_knowledge k [const restrict static 1],
const JH_index sequence [const restrict static 1],
const size_t sequence_length,
const JH_index markov_order,
FILE io [const restrict static 1]
);
int JH_knowledge_learn_markov_sequence
(
struct JH_knowledge k [const restrict static 1],
const JH_index sequence [const restrict static 1],
const JH_index markov_order, /* Pre (> markov_order 1) */
JH_index sequence_id [const restrict static 1],
FILE io [const restrict static 1]
);
void JH_knowledge_get_word
(
struct JH_knowledge k [const static 1],
const JH_index word_ref,
const JH_char * word [const restrict static 1],
JH_index word_length [const restrict static 1],
FILE io [const restrict static 1]
);
/*
* When returning 0:
* {word} is in {k}.
* {word} is located at {k->words[*result]}.
*
* When returning -1:
* {word} is not in {k}.
* {*result} is where {word} was expected to be found in
* {k->sorted_indices}.
*
* Does not acquire locks
*/
int JH_knowledge_find_word_id
(
const struct JH_knowledge k [const restrict static 1],
const JH_char word [const restrict static 1],
const size_t word_size,
JH_index result [const restrict static 1]
);
/*
* Does not acquire locks
*/
int JH_knowledge_find_sequence
(
const struct JH_knowledge k [const static 1],
const JH_index sequence [const restrict static 1],
const JH_index markov_order, /* Pre: (> 1) */
JH_index sequence_id [const restrict static 1]
);
int JH_knowledge_rarest_word
(
struct JH_knowledge k [const static 1],
const JH_index sequence [const restrict static 1],
const size_t sequence_length,
JH_index word_id [const restrict static 1],
FILE io [const restrict static 1]
);
/*
* Does not acquire locks
*/
int JH_knowledge_find_markov_sequence
(
const JH_index sequence_id,
const struct JH_knowledge_sequence_collection sc [const restrict static 1],
JH_index result [const restrict static 1]
);
/*
* Does not acquire locks
*/
int JH_knowledge_find_sequence_target
(
const JH_index target_id,
const struct JH_knowledge_sequence_data sd [const restrict static 1],
JH_index result [const restrict static 1]
);
int JH_knowledge_random_tws_target
(
struct JH_knowledge k [const static 1],
JH_index target [const restrict static 1],
const JH_index word_id,
const JH_index sequence_id,
FILE io [const restrict static 1]
);
int JH_knowledge_random_swt_target
(
struct JH_knowledge k [const static 1],
const JH_index sequence_id,
const JH_index word_id,
JH_index target [const restrict static 1],
FILE io [const restrict static 1]
);
int JH_knowledge_copy_random_swt_sequence
(
struct JH_knowledge k [const static 1],
JH_index sequence [const restrict static 1],
const JH_index word_id,
const JH_index markov_order,
FILE io [const restrict static 1]
);
int JH_knowledge_strengthen_swt
(
struct JH_knowledge k [const restrict static 1],
const JH_index sequence_id,
const JH_index word_id,
const JH_index target_id,
FILE io [const restrict static 1]
);
int JH_knowledge_strengthen_tws
(
struct JH_knowledge k [const restrict static 1],
const JH_index target_id,
const JH_index word_id,
const JH_index sequence_id,
FILE io [const restrict static 1]
);
/*
* TODO
*/
/*
int JH_knowledge_weaken_swt
(
struct JH_knowledge k [const restrict static 1],
const JH_index sequence_id,
const JH_index word_id,
const JH_index target_id,
FILE io [const restrict static 1]
);
int JH_knowledge_weaken_tws
(
struct JH_knowledge k [const restrict static 1],
const JH_index target_id,
const JH_index word_id,
const JH_index sequence_id,
FILE io [const restrict static 1]
);
*/
#endif
|
