repositories / mc1516pa.git / blob
? search:


200db36abd4b2d57a35604809303c56b86646843
[mc1516pa.git] / modelchecker / coord.c
1 #include <argp.h>
2 #include <stdio.h>
3 #include <stdlib.h>
4 #include <sylvan.h>
5 #include <lace.h>
6
7 #include "coord.h"
8 #include "sokoban.h"
9
10
11 typedef struct {
12 int x;
13 int y;
14 } xy;
15
16 typedef struct {
17 int var[3];
18 } bddvar;
19
20 typedef struct {
21 xy key;
22 bddvar value;
23 UT_hash_handle hh;
24 } xy_bddvar_map;
25
26 typedef struct {
27 int key;
28 xy value;
29 UT_hash_handle hh;
30 } bddvar_xy_map;
31
32 typedef struct {
33 xy_bddvar_map *f;
34 bddvar_xy_map *t;
35 } bimap;
36
37 xy_bddvar_map *getxy(int x, int y, xy_bddvar_map *map)
38 {
39 xy_bddvar_map k, *r = NULL;
40 memset(&k, 0, sizeof(xy_bddvar_map));
41 k.key.x = x;
42 k.key.y = y;
43 HASH_FIND(hh, map, &k.key, sizeof(xy), r);
44 return r;
45 }
46
47 bddvar_xy_map *getbdd(int key, bddvar_xy_map *map)
48 {
49 bddvar_xy_map k, *r = NULL;
50 memset(&k, 0, sizeof(bddvar_xy_map));
51 k.key = key;
52 HASH_FIND(hh, map, &k.key, sizeof(int), r);
53 return r;
54 }
55
56
57 bimap *create_bimap_helper(sokoban_screen *screen)
58 {
59 int varcount = 0;
60 sokoban_screen *r;
61 xy_bddvar_map *xybdd = NULL;
62 bddvar_xy_map *bddxy = NULL;
63 for(r=screen; r != NULL; r = (sokoban_screen *)(r->hh.next)){
64 xy_bddvar_map *f = NULL;
65 f = (xy_bddvar_map *)malloc(sizeof(xy_bddvar_map));
66 memset(f, 0, sizeof(xy_bddvar_map));
67 f->key.x = r->coord.x;
68 f->key.y = r->coord.y;
69 f->value.var[0] = varcount * 2;
70 f->value.var[1] = (varcount + 1) * 2;
71 f->value.var[2] = (varcount + 2) * 2;
72 HASH_ADD(hh, xybdd, key, sizeof(xy), f);
73
74 for (int i = 0; i <3; i++){
75 bddvar_xy_map *t = NULL;
76 t = (bddvar_xy_map *)malloc(sizeof(bddvar_xy_map));
77 memset(t, 0, sizeof(bddvar_xy_map));
78 t->key = (varcount + i) * 2;
79 t->value.x = r->coord.x;
80 t->value.y = r->coord.y;
81 HASH_ADD(hh, bddxy, key, sizeof(int), t);
82 }
83 varcount = varcount + 3;
84 }
85 bimap *bm = NULL;
86 bm = (bimap *)malloc(sizeof(bimap));
87 bm->f = xybdd;
88 bm->t = bddxy;
89 return bm;
90 }
91
92 int check_xy_exists(int x, int y, bimap *bm)
93 {
94 int res = 0;
95 if (getxy(x, y, bm->f) != NULL) res = 1;
96 return res;
97 }
98
99 int check_space(int x, int y, direction d, int delta, bimap *bm)
100 {
101 switch(d){
102 case LEFT: x = x - delta; break;
103 case UP: y = y - delta; break;
104 case RIGHT: x = x + delta; break;
105 case DOWN: y = y + delta; break;
106 }
107 return check_xy_exists(x, y, bm);
108 }
109
110 /*
111 * Each coordinate has three related boolean variables. The combination of those boolean variables
112 * defines tiles:
113 * 000: Wall
114 * 001: Free
115 * 010: Box
116 * 100: Box on target
117 * 011: Target
118 * 101: Agent
119 * 110: Agent on target
120 * In the BDD representation, the state is represented by n * 3 variables, where n is the number of
121 * tiles in the shrinked screen.
122 * It seems that the move variable is not necessary since non-deterministic moves can be emvedded
123 * directly in transition relations.
124 */
125
126 state *encode_screen(sokoban_screen *screen)
127 {
128 LACE_ME;
129
130 BDDVAR vars[HASH_COUNT(screen) * 3];
131 for (uint8_t i = 0; i < HASH_COUNT(screen) * 3; i++){
132 vars[i] = i * 2;
133 }
134
135 uint8_t st_enc[HASH_COUNT(screen) * 3];
136
137 BDDSET varset = sylvan_set_fromarray(vars, HASH_COUNT(screen) * 3);
138 BDD s;
139 state *fullState = NULL;
140 fullState = (state *)malloc(sizeof(state));
141 fullState->vars.varset = varset;
142 fullState->vars.size = HASH_COUNT(screen) * 3;
143 int tile_index = 0;
144 sokoban_screen *r;
145 for(r=screen; r != NULL; r = (sokoban_screen *)(r->hh.next)){
146 switch(r->tile){
147 case FREE: //001
148 st_enc[tile_index] = 0;
149 tile_index++;
150 st_enc[tile_index] = 0;
151 tile_index++;
152 st_enc[tile_index] = 1;
153 tile_index++;
154 break;
155 case WALL: //000
156 st_enc[tile_index] = 0;
157 tile_index++;
158 st_enc[tile_index] = 0;
159 tile_index++;
160 st_enc[tile_index] = 0;
161 tile_index++;
162 break;
163 case BOX: //010
164 st_enc[tile_index] = 0;
165 tile_index++;
166 st_enc[tile_index] = 1;
167 tile_index++;
168 st_enc[tile_index] = 0;
169 tile_index++;
170 break;
171 case TARGET: //011
172 st_enc[tile_index] = 0;
173 tile_index++;
174 st_enc[tile_index] = 1;
175 tile_index++;
176 st_enc[tile_index] = 1;
177 tile_index++;
178 break;
179 case AGENT: //101
180 st_enc[tile_index] = 1;
181 tile_index++;
182 st_enc[tile_index] = 0;
183 tile_index++;
184
185 st_enc[tile_index] = 1;
186 tile_index++;
187 break;
188 case TARGAGENT: //110
189 st_enc[tile_index] = 1;
190 tile_index++;
191 st_enc[tile_index] = 1;
192 tile_index++;
193 st_enc[tile_index] = 0;
194 tile_index++;
195 break;
196 case TARGBOX: //100
197 st_enc[tile_index] = 1;
198 tile_index++;
199 st_enc[tile_index] = 0;
200 tile_index++;
201 st_enc[tile_index] = 0;
202 tile_index++;
203 break;
204 }
205 }
206 s = sylvan_cube(varset, st_enc);
207 fullState->bdd = s;
208 printf("Initial state encoded\n");
209 return fullState;
210 }
211
212 //test
213 int countTrans(trans_t *trs);
214
215 trans_t *create_single_rel(sokoban_screen *screen, direction dir)
216 {
217 LACE_ME;
218 trans_t *trs, *trs_current;
219 bimap *bm = create_bimap_helper(screen);
220 int x = 0;
221 int y = 0;
222 bddvar_xy_map *bddxy = NULL;
223 int xdelta = 0;
224 int ydelta = 0;
225 int xgamma = 0;
226 int ygamma = 0;
227 trs = NULL;
228 switch(dir){
229 case LEFT:
230 xdelta = -1;
231 ydelta = 0;
232 xgamma = -2;
233 ygamma = 0;
234 break;
235 case UP:
236 xdelta = 0;
237 ydelta = -1;
238 xgamma = 0;
239 ygamma = -2;
240 break;
241 case RIGHT:
242 xdelta = 1;
243 ydelta = 0;
244 xgamma = 2;
245 ygamma = 0;
246 break;
247 case DOWN:
248 xdelta = 0;
249 ydelta = 1;
250 xgamma = 0;
251 ygamma = 2;
252 break;
253 }
254
255 for (unsigned int i = 0; i < HASH_COUNT(screen); i++){
256 bddxy = getbdd(i*6, bm->t);
257 x = bddxy->value.x;
258 y = bddxy->value.y;
259 if (check_space(x, y, dir, 1, bm) == 0){
260 //Agent -> Agent
261 //1 1 0 0 1 1 (1 0 1 -> 1 0 1)
262 BDDVAR relvars[6] = {i * 6, i * 6 + 1, i * 6 + 2, i * 6 + 3, i * 6 + 4, i * 6 + 5};
263 BDDSET relvarset = sylvan_set_fromarray(relvars, 6);
264 uint8_t rel_enc[6] = {1, 1, 0, 0, 1, 1};
265
266 trs_current = (trans_t *)malloc(sizeof(trans_t));
267 trs_current->bdd = sylvan_cube(relvarset, rel_enc);
268 trs_current->varset.varset = relvarset;
269 trs_current->varset.size = 6;
270 trs_current->next_rel = trs;
271 trs = trs_current;
272
273 //Targagent -> Targagent
274 //1 1 1 1 0 0 (1 1 0 -> 1 1 0)
275 relvarset = sylvan_set_fromarray(relvars, 6);
276 uint8_t rel_enc1[6] = {1, 1, 1, 1, 0, 0};
277 memcpy(rel_enc, rel_enc1, 6*sizeof(uint8_t));
278
279 trs_current = (trans_t *)malloc(sizeof(trans_t));
280 trs_current->bdd = sylvan_cube(relvarset, rel_enc);
281 trs_current->varset.varset = relvarset;
282 trs_current->varset.size = 6;
283 trs_current->next_rel = trs;
284 trs = trs_current;
285
286 }
287 else if (check_space(x, y, dir, 1, bm) == 1 && check_space(x, y, dir, 2, bm) == 0){
288 xy_bddvar_map *bddvar = getxy(x + xdelta, y + ydelta, bm->f);
289 unsigned int deltai = bddvar->value.var[0];
290 //Agent Free -> Free Agent
291 //(1 0 0 0 1 1 0 1 0 0 1 1)
292 //or
293 //(0 1 0 0 1 1 1 0 0 0 1 1)
294 BDDVAR relvars[12] = {i*6, i*6+1, i*6+2, i*6+3, i*6+4, i*6+5, deltai, deltai+1, deltai+2, deltai+3, deltai+4, deltai+5};
295 BDDSET relvarset = sylvan_set_fromarray(relvars, 12);
296 uint8_t rel_enc[12];
297 if (i < deltai){
298 uint8_t rel_enc0[12] = {1, 0, 0, 0, 1, 1, 0, 1, 0, 0, 1, 1};
299 memcpy(rel_enc, rel_enc0, 12*sizeof(uint8_t));
300 }
301 else {
302 uint8_t rel_enc0[12] = {0, 1, 0, 0, 1, 1, 1, 0, 0, 0, 1, 1};
303 memcpy(rel_enc, rel_enc0, 12*sizeof(uint8_t));
304 }
305 trs_current = (trans_t *)malloc(sizeof(trans_t));
306 trs_current->bdd = sylvan_cube(relvarset, rel_enc);
307 trs_current->varset.varset = relvarset;
308 trs_current->varset.size = 12;
309 trs_current->next_rel = trs;
310 trs = trs_current;
311
312 //Agent Target -> Free Targagent
313 //(1 0 0 0 1 1 0 1 1 1 1 0)
314 //or
315 //(0 1 1 1 1 0 0 1 1 1 1 0)
316 relvarset = sylvan_set_fromarray(relvars, 12);
317 if (i < deltai){
318 uint8_t rel_enc2[12] = {1, 0, 0, 0, 1, 1, 0, 1, 1, 1, 1, 0};
319 memcpy(rel_enc, rel_enc2, 12*sizeof(uint8_t));
320 }
321 else {
322 uint8_t rel_enc2[12] = {0, 1, 1, 1, 1, 0, 0, 1, 1, 1, 1, 0};
323 memcpy(rel_enc, rel_enc2, 12*sizeof(uint8_t));
324 }
325 trs_current = (trans_t *)malloc(sizeof(trans_t));
326 trs_current->bdd = sylvan_cube(relvarset, rel_enc);
327 trs_current->varset.varset = relvarset;
328 trs_current->varset.size = 12;
329 trs_current->next_rel = trs;
330 trs = trs_current;
331
332 //Targagent Free -> Target Agent
333 //(1 0 1 1 0 1 0 1 0 0 1 1)
334 //or
335 //(0 1 0 0 1 1 1 0 1 1 0 1)
336 relvarset = sylvan_set_fromarray(relvars, 12);
337 if (i < deltai){
338 uint8_t rel_enc3[12] = {1, 0, 1, 1, 0, 1, 0, 1, 0, 0, 1, 1};
339 memcpy(rel_enc, rel_enc3, 12*sizeof(uint8_t));
340 }
341 else {
342 uint8_t rel_enc3[12] = {0, 1, 0, 0, 1, 1, 1, 0, 1, 1, 0, 1};
343 memcpy(rel_enc, rel_enc3, 12*sizeof(uint8_t));
344 }
345 trs_current = (trans_t *)malloc(sizeof(trans_t));
346 trs_current->bdd = sylvan_cube(relvarset, rel_enc);
347 trs_current->varset.varset = relvarset;
348 trs_current->varset.size = 12;
349 trs_current->next_rel = trs;
350 trs = trs_current;
351
352 //Targagent Target -> Target Targagent
353 //(1 0 1 1 0 1 0 1 1 1 1 0)
354 //or
355 //(0 1 1 1 1 0 1 0 1 1 0 1)
356 relvarset = sylvan_set_fromarray(relvars, 12);
357 if (i < deltai){
358 uint8_t rel_enc4[12] = {1, 0, 1, 1, 0, 1, 0, 1, 1, 1, 1, 0};
359 memcpy(rel_enc, rel_enc4, 12*sizeof(uint8_t));
360 }
361 else {
362 uint8_t rel_enc4[12] = {0, 1, 1, 1, 1, 0, 1, 0, 1, 1, 0, 1};
363 memcpy(rel_enc, rel_enc4, 12*sizeof(uint8_t));
364 }
365 trs_current = (trans_t *)malloc(sizeof(trans_t));
366 trs_current->bdd = sylvan_cube(relvarset, rel_enc);
367 trs_current->varset.varset = relvarset;
368 trs_current->varset.size = 12;
369 trs_current->next_rel = trs;
370 trs = trs_current;
371
372 //Agent Box -> Agent Box
373 //(1 1 0 0 1 1 0 0 1 1 0 0)
374 //or
375 //(0 0 1 1 0 0 1 1 0 0 1 1)
376 relvarset = sylvan_set_fromarray(relvars, 12);
377 if (i < deltai){
378 uint8_t rel_enc5[12] = {1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0};
379 memcpy(rel_enc, rel_enc5, 12*sizeof(uint8_t));
380 }
381 else {
382 uint8_t rel_enc5[12] = {0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1};
383 memcpy(rel_enc, rel_enc5, 12*sizeof(uint8_t));
384 }
385 trs_current = (trans_t *)malloc(sizeof(trans_t));
386 trs_current->bdd = sylvan_cube(relvarset, rel_enc);
387 trs_current->varset.varset = relvarset;
388 trs_current->varset.size = 12;
389 trs_current->next_rel = trs;
390 trs = trs_current;
391
392 //Agent Targbox -> Agent Targbox
393 //(1 1 0 0 1 1 1 1 0 0 0 0)
394 //
395 //(1 1 0 0 0 0 1 1 0 0 1 1)
396 relvarset = sylvan_set_fromarray(relvars, 12);
397 if (i < deltai){
398 uint8_t rel_enc6[12] = {1, 1, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0};
399 memcpy(rel_enc, rel_enc6, 12*sizeof(uint8_t));
400 }
401 else {
402 uint8_t rel_enc6[12] = {1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1};
403 memcpy(rel_enc, rel_enc6, 12*sizeof(uint8_t));
404 }
405 trs_current = (trans_t *)malloc(sizeof(trans_t));
406 trs_current->bdd = sylvan_cube(relvarset, rel_enc);
407 trs_current->varset.varset = relvarset;
408 trs_current->varset.size = 12;
409 trs_current->next_rel = trs;
410 trs = trs_current;
411
412 //Targagent Box -> Targagent Box
413 //(1 1 1 1 0 0 0 0 1 1 0 0)
414 //or
415 //(0 0 1 1 0 0 1 1 1 1 0 0)
416 relvarset = sylvan_set_fromarray(relvars, 12);
417 if (i < deltai){
418 uint8_t rel_enc7[12] = {1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0};
419 memcpy(rel_enc, rel_enc7, 12*sizeof(uint8_t));
420 }
421 else {
422 uint8_t rel_enc7[12] = {0, 0, 1, 1, 0, 0, 1, 1, 1, 1, 0, 0};
423 memcpy(rel_enc, rel_enc7, 12*sizeof(uint8_t));
424 }
425 trs_current = (trans_t *)malloc(sizeof(trans_t));
426 trs_current->bdd = sylvan_cube(relvarset, rel_enc);
427 trs_current->varset.varset = relvarset;
428 trs_current->varset.size = 12;
429 trs_current->next_rel = trs;
430 trs = trs_current;
431
432 //Targagent Targbox -> Targagent Targbox
433 //(1 1 1 1 0 0 1 1 0 0 0 0)
434 //or
435 //(1 1 0 0 0 0 1 1 1 1 0 0)
436 relvarset = sylvan_set_fromarray(relvars, 12);
437 if (i < deltai){
438 uint8_t rel_enc8[12] = {1, 1, 1, 1, 0, 0, 1, 1, 0, 0, 0, 0};
439 memcpy(rel_enc, rel_enc8, 12*sizeof(uint8_t));
440 }
441 else {
442 uint8_t rel_enc8[12] = {1, 1, 0, 0, 0, 0, 1, 1, 1, 1, 0, 0};
443 memcpy(rel_enc, rel_enc8, 12*sizeof(uint8_t));
444 }
445 trs_current = (trans_t *)malloc(sizeof(trans_t));
446 trs_current->bdd = sylvan_cube(relvarset, rel_enc);
447 trs_current->varset.varset = relvarset;
448 trs_current->varset.size = 12;
449 trs_current->next_rel = trs;
450 trs = trs_current;
451
452 }
453 else if (check_space(x, y, dir, 1, bm) == 1 && check_space(x, y, dir, 2, bm) == 1){
454 xy_bddvar_map *bddvar = getxy(x + xdelta, y + ydelta, bm->f);
455 unsigned int deltai = bddvar->value.var[0];
456 bddvar = getxy(x + xgamma, y + ygamma, bm->f);
457 unsigned int gammai = bddvar->value.var[0];
458 //Agent Free -> Free Agent
459 //(1 0 0 0 1 1 0 1 0 0 1 1)
460 //or
461 //(0 1 0 0 1 1 1 0 0 0 1 1)
462 BDDVAR relvars[12] = {i*6, i*6+1, i*6+2, i*6+3, i*6+4, i*6+5, deltai, deltai+1, deltai+2, deltai+3, deltai+4, deltai+5};
463 BDDSET relvarset = sylvan_set_fromarray(relvars, 12);
464 uint8_t rel_enc[12];
465 if (i < deltai){
466 uint8_t rel_enc_[12] = {1, 0, 0, 0, 1, 1, 0, 1, 0, 0, 1, 1};
467 memcpy(rel_enc, rel_enc_, 12*sizeof(uint8_t));
468 }
469 else {
470 uint8_t rel_enc_[12] = {0, 1, 0, 0, 1, 1, 1, 0, 0, 0, 1, 1};
471 memcpy(rel_enc, rel_enc_, 12*sizeof(uint8_t));
472 }
473 trs_current = (trans_t *)malloc(sizeof(trans_t));
474 trs_current->bdd = sylvan_cube(relvarset, rel_enc);
475 trs_current->varset.varset = relvarset;
476 trs_current->varset.size = 12;
477 trs_current->next_rel = trs;
478 trs = trs_current;
479
480 //Agent Target -> Free Targagent
481 //(1 0 0 0 1 1 0 1 1 1 1 0)
482 //or
483 //(0 1 1 1 1 0 1 0 0 0 1 1)
484 relvarset = sylvan_set_fromarray(relvars, 12);
485 if (i < deltai){
486 uint8_t rel_enc9[12] = {1, 0, 0, 0, 1, 1, 0, 1, 1, 1, 1, 0};
487 memcpy(rel_enc, rel_enc9, 12*sizeof(uint8_t));
488 }
489 else {
490 uint8_t rel_enc9[12] = {0, 1, 1, 1, 1, 0, 1, 0, 0, 0, 1, 1};
491 memcpy(rel_enc, rel_enc9, 12*sizeof(uint8_t));
492 }
493 trs_current = (trans_t *)malloc(sizeof(trans_t));
494 trs_current->bdd = sylvan_cube(relvarset, rel_enc);
495 trs_current->varset.varset = relvarset;
496 trs_current->varset.size = 12;
497 trs_current->next_rel = trs;
498 trs = trs_current;
499
500 //Targagent Free -> Target Agent (LEFT || UP)
501 //(1 0 1 1 0 1 0 1 0 0 1 1)
502 //or
503 //(0 1 0 0 1 1 1 0 1 1 0 1)
504 relvarset = sylvan_set_fromarray(relvars, 12);
505 if (i < deltai){
506 uint8_t rel_enc10[12] = {1, 0, 1, 1, 0, 1, 0, 1, 0, 0, 1, 1};
507 memcpy(rel_enc, rel_enc10, 12*sizeof(uint8_t));
508 }
509 else {
510 uint8_t rel_enc10[12] = {0, 1, 0, 0, 1, 1, 1, 0, 1, 1, 0, 1};
511 memcpy(rel_enc, rel_enc10, 12*sizeof(uint8_t));
512 }
513 trs_current = (trans_t *)malloc(sizeof(trans_t));
514 trs_current->bdd = sylvan_cube(relvarset, rel_enc);
515 trs_current->varset.varset = relvarset;
516 trs_current->varset.size = 12;
517 trs_current->next_rel = trs;
518 trs = trs_current;
519
520 //Targagent Target -> Target Targagent (LEFT || UP)
521 //(1 0 1 1 0 1 0 1 1 1 1 0)
522 //or
523 //(0 1 1 1 1 0 1 0 1 1 0 1)
524 relvarset = sylvan_set_fromarray(relvars, 12);
525 if (i < deltai){
526 uint8_t rel_enc11[12] = {1, 0, 1, 1, 0, 1, 0, 1, 1, 1, 1, 0};
527 memcpy(rel_enc, rel_enc11, 12*sizeof(uint8_t));
528 }
529 else {
530 uint8_t rel_enc11[12] = {0, 1, 1, 1, 1, 0, 1, 0, 1, 1, 0, 1};
531 memcpy(rel_enc, rel_enc11, 12*sizeof(uint8_t));
532 }
533 trs_current = (trans_t *)malloc(sizeof(trans_t));
534 trs_current->bdd = sylvan_cube(relvarset, rel_enc);
535 trs_current->varset.varset = relvarset;
536 trs_current->varset.size = 12;
537 trs_current->next_rel = trs;
538 trs = trs_current;
539
540 //Agent Box Box -> Agent Box Box
541 //(1 1 0 0 1 1 0 0 1 1 0 0 0 0 1 1 0 0)
542 //or
543 //(0 0 1 1 0 0 0 0 1 1 0 0 1 1 0 0 1 1)
544 //or
545 //(0 0 1 1 0 0 1 1 0 0 1 1 0 0 1 1 0 0)
546 //or
547 //(1 1 0 0 1 1 0 0 1 1 0 0 0 0 1 1 0 0)
548 //or
549 //(0 0 1 1 0 0 1 1 0 0 1 1 0 0 1 1 0 0)
550 //or
551 //(0 0 1 1 0 0 0 0 1 1 0 0 1 1 0 0 1 1)
552 BDDVAR relvars1[18] = {i*6, i*6+1, i*6+2, i*6+3, i*6+4, i*6+5, deltai, deltai+1, deltai+2, deltai+3, deltai+4, deltai+5, gammai, gammai+1, gammai+2, gammai+3, gammai+4, gammai+5};
553 BDD relvarset1 = sylvan_set_fromarray(relvars1, 18);
554 uint8_t rel_enc1[18];
555 if ((i < deltai) < gammai){
556 uint8_t rel_enc__[18] = {1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0};
557 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
558 }
559 else if ((deltai < gammai) < i){
560 uint8_t rel_enc__[18] = {0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1};
561 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
562 }
563 else if ((gammai < i) < deltai){
564 uint8_t rel_enc__[18] = {0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0};
565 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
566 }
567 else if ((i < gammai) < deltai){
568 uint8_t rel_enc__[18] = {1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0};
569 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
570 }
571 else if ((deltai < i) < gammai){
572 uint8_t rel_enc__[18] = {0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 1, 1, 0, 0, 1};
573 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
574 }
575 else {
576 uint8_t rel_enc__[18] = {1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0};
577 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
578 }
579
580 trs_current = (trans_t *)malloc(sizeof(trans_t));
581 trs_current->bdd = sylvan_cube(relvarset1, rel_enc1);
582 trs_current->varset.varset = relvarset1;
583 trs_current->varset.size = 18;
584 trs_current->next_rel = trs;
585 trs = trs_current;
586
587 //Agent Box Targbox -> Agent Box Targbox (LEFT || UP)
588 //(1 1 0 0 1 1 0 0 1 1 0 0 1 1 0 0 0 0)
589 //or
590 //(0 0 1 1 0 0 1 1 0 0 0 0 1 1 0 0 1 1)
591 //or
592 //(1 1 0 0 0 0 1 1 0 0 1 1 0 0 1 1 0 0)
593 //or
594 //(1 1 0 0 1 1 1 1 0 0 0 0 0 0 1 1 0 0)
595 //or
596 //(0 0 1 1 0 0 1 1 0 0 1 1 1 1 0 0 0 0)
597 //or
598 //(1 1 0 0 0 0 0 0 1 1 0 0 1 1 0 0 1 1)
599 relvarset1 = sylvan_set_fromarray(relvars1, 18);
600 if ((i < deltai) < gammai){
601 uint8_t rel_enc__[18] = {1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 0};
602 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
603 }
604 else if ((deltai < gammai) < i){
605 uint8_t rel_enc__[18] = {0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1};
606 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
607 }
608 else if ((gammai < i) < deltai){
609 uint8_t rel_enc__[18] = {1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0};
610 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
611 }
612 else if ((i < gammai) < deltai){
613 uint8_t rel_enc__[18] = {1, 1, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0};
614 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
615 }
616 else if ((deltai < i) < gammai){
617 uint8_t rel_enc__[18] = {0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0};
618 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
619 }
620 else {
621 uint8_t rel_enc__[18] = {1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1};
622 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
623 }
624 trs_current = (trans_t *)malloc(sizeof(trans_t));
625 trs_current->bdd = sylvan_cube(relvarset1, rel_enc1);
626 trs_current->varset.varset = relvarset1;
627 trs_current->varset.size = 18;
628 trs_current->next_rel = trs;
629 trs = trs_current;
630
631 //Targagent Box Box -> Targagent Box Box
632 //(1 1 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0)
633 //or
634 //(0 0 1 1 0 0 0 0 1 1 0 0 1 1 1 1 0 0)
635 //or
636 //(0 0 1 1 0 0 1 1 1 1 0 0 0 0 1 1 0 0)
637 //or
638 //(1 1 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0)
639 //or
640 //(0 0 1 1 0 0 1 1 1 1 0 0 0 0 1 1 0 0)
641 //or
642 //(0 0 1 1 0 0 0 0 1 1 0 0 1 1 1 1 0 0)
643 relvarset1 = sylvan_set_fromarray(relvars1, 18);
644 if ((i < deltai) < gammai){
645 uint8_t rel_enc__[18] = {1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0};
646 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
647 }
648 else if ((deltai < gammai) < i){
649 uint8_t rel_enc__[18] = {0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 1, 1, 0, 0};
650 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
651 }
652 else if ((gammai < i) < deltai){
653 uint8_t rel_enc__[18] = {0, 0, 1, 1, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0};
654 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
655 }
656 else if ((i < gammai) < deltai){
657 uint8_t rel_enc__[18] = {1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0};
658 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
659 }
660 else if ((deltai < i) < gammai){
661 uint8_t rel_enc__[18] = {0, 0, 1, 1, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0};
662 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
663 }
664 else {
665 uint8_t rel_enc__[18] = {0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 1, 1, 0, 0};
666 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
667 }
668 trs_current = (trans_t *)malloc(sizeof(trans_t));
669 trs_current->bdd = sylvan_cube(relvarset1, rel_enc1);
670 trs_current->varset.varset = relvarset1;
671 trs_current->varset.size = 18;
672 trs_current->next_rel = trs;
673 trs = trs_current;
674
675 //Targagent Box Targbox -> Targagent Box Targbox (LEFT || UP)
676 //(1 1 1 1 0 0 0 0 1 1 0 0 1 1 0 0 0 0)
677 //or
678 //(0 0 1 1 0 0 1 1 0 0 0 0 1 1 1 1 0 0)
679 //or
680 //(1 1 0 0 0 0 1 1 1 1 0 0 0 0 1 1 0 0)
681 //or
682 //(1 1 1 1 0 0 1 1 0 0 0 0 0 0 1 1 0 0)
683 //or
684 //(0 0 1 1 0 0 1 1 1 1 0 0 1 1 0 0 0 0)
685 //or
686 //(1 1 0 0 0 0 0 0 1 1 0 0 1 1 1 1 0 0)
687 relvarset1 = sylvan_set_fromarray(relvars1, 18);
688 if ((i < deltai) < gammai){
689 uint8_t rel_enc__[18] = {1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 0};
690 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
691 }
692 else if ((deltai < gammai) < i){
693 uint8_t rel_enc__[18] = {0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 1, 1, 0, 0};
694 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
695 }
696 else if ((gammai < i) < deltai){
697 uint8_t rel_enc__[18] = {1, 1, 0, 0, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0};
698 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
699 }
700 else if ((i < gammai) < deltai){
701 uint8_t rel_enc__[18] = {1, 1, 1, 1, 0, 0, 1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0};
702 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
703 }
704 else if ((deltai < i) < gammai){
705 uint8_t rel_enc__[18] = {0, 0, 1, 1, 0, 0, 1, 1, 1, 1, 0, 0, 1, 1, 0, 0, 0, 0};
706 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
707 }
708 else {
709 uint8_t rel_enc__[18] = {1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 1, 1, 0, 0};
710 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
711 }
712 trs_current = (trans_t *)malloc(sizeof(trans_t));
713 trs_current->bdd = sylvan_cube(relvarset1, rel_enc1);
714 trs_current->varset.varset = relvarset1;
715 trs_current->varset.size = 18;
716 trs_current->next_rel = trs;
717 trs = trs_current;
718
719 //Agent Box Free -> Free Agent Box
720 //(1 0 0 0 1 1 0 1 1 0 0 1 0 0 0 1 1 0)
721 //or
722 //(0 1 1 0 0 1 0 0 0 1 1 0 1 0 0 0 1 1)
723 //or
724 //(0 0 0 1 1 0 1 0 0 0 1 1 0 1 1 0 0 1)
725 //or
726 //(1 0 0 0 1 1 0 0 0 1 1 0 0 1 1 0 0 1)
727 //or
728 //(0 1 1 0 0 1 1 0 0 0 1 1 0 0 0 1 1 0)
729 //or
730 //(0 0 0 1 1 0 0 1 1 0 0 1 1 0 0 0 1 1)
731 relvarset1 = sylvan_set_fromarray(relvars1, 18);
732 if ((i < deltai) < gammai){
733 uint8_t rel_enc__[18] = {1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 0, 1, 0, 0, 0, 1, 1, 0};
734 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
735 }
736 else if ((deltai < gammai) < i){
737 uint8_t rel_enc__[18] = {0, 1, 1, 0, 0, 1, 0, 0, 0, 1, 1, 0, 1, 0, 0, 0, 1, 1};
738 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
739 }
740 else if ((gammai < i) < deltai){
741 uint8_t rel_enc__[18] = {0, 0, 0, 1, 1, 0, 1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 0, 1};
742 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
743 }
744 else if ((i < gammai) < deltai){
745 uint8_t rel_enc__[18] = {1, 0, 0, 0, 1, 1, 0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1};
746 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
747 }
748 else if ((deltai < i) < gammai){
749 uint8_t rel_enc__[18] = {0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 1, 1, 0, 0, 0, 1, 1, 0};
750 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
751 }
752 else {
753 uint8_t rel_enc__[18] = {0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 1, 1};
754 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
755 }
756 trs_current = (trans_t *)malloc(sizeof(trans_t));
757 trs_current->bdd = sylvan_cube(relvarset1, rel_enc1);
758 trs_current->varset.varset = relvarset1;
759 trs_current->varset.size = 18;
760 trs_current->next_rel = trs;
761 trs = trs_current;
762
763 //Agent Targbox Free -> Free Targagent Box
764 //(1 0 0 0 1 1 1 1 0 1 0 0 0 0 0 1 1 0)
765 //or
766 //(1 1 0 1 0 0 0 0 0 1 1 0 1 0 0 0 1 1)
767 //or
768 //(0 0 0 1 1 0 1 0 0 0 1 1 1 1 0 1 0 0)
769 //or
770 //(1 0 0 0 1 1 0 0 0 1 1 0 1 1 0 1 0 0)
771 //or
772 //(1 1 0 1 0 0 1 0 0 0 1 1 0 0 0 1 1 0)
773 //or
774 //(0 0 0 1 1 0 1 1 0 1 0 0 1 0 0 0 1 1)
775 relvarset1 = sylvan_set_fromarray(relvars1, 18);
776 if ((i < deltai) < gammai){
777 uint8_t rel_enc__[18] = {1, 0, 0, 0, 1, 1, 1, 1, 0, 1, 0, 0, 0, 0, 0, 1, 1, 0};
778 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
779 }
780 else if ((deltai < gammai) < i){
781 uint8_t rel_enc__[18] = {1, 1, 0, 1, 0, 0, 0, 0, 0, 1, 1, 0, 1, 0, 0, 0, 1, 1};
782 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
783 }
784 else if ((gammai < i) < deltai){
785 uint8_t rel_enc__[18] = {0, 0, 0, 1, 1, 0, 1, 0, 0, 0, 1, 1, 1, 1, 0, 1, 0, 0};
786 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
787 }
788 else if ((i < gammai) < deltai){
789 uint8_t rel_enc__[18] = {1, 0, 0, 0, 1, 1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0, 0};
790 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
791 }
792 else if ((deltai < i) < gammai){
793 uint8_t rel_enc__[18] = {1, 1, 0, 1, 0, 0, 1, 0, 0, 0, 1, 1, 0, 0, 0, 1, 1, 0};
794 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
795 }
796 else {
797 uint8_t rel_enc__[18] = {0, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0, 0, 1, 0, 0, 0, 1, 1};
798 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
799 }
800 trs_current = (trans_t *)malloc(sizeof(trans_t));
801 trs_current->bdd = sylvan_cube(relvarset1, rel_enc1);
802 trs_current->varset.varset = relvarset1;
803 trs_current->varset.size = 18;
804 trs_current->next_rel = trs;
805 trs = trs_current;
806
807 //Agent Box Target -> Free Agent Targbox
808 //(1 0 0 0 1 1 0 1 1 0 0 1 0 1 1 0 1 0)
809 //or
810 //(0 1 1 0 0 1 0 1 1 0 1 0 1 0 0 0 1 1)
811 //or
812 //(0 1 1 0 1 0 1 0 0 0 1 1 0 1 1 0 0 1)
813 //or
814 //(1 0 0 0 1 1 0 1 1 0 1 0 0 1 1 0 0 1)
815 //or
816 //(0 1 1 0 0 1 1 0 0 0 1 1 0 1 1 0 1 0)
817 //or
818 //(0 1 1 0 1 0 0 1 1 0 0 1 1 0 0 0 1 1)
819 relvarset1 = sylvan_set_fromarray(relvars1, 18);
820 if ((i < deltai) < gammai){
821 uint8_t rel_enc__[18] = {1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 0, 1, 0, 1, 1, 0, 1, 0};
822 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
823 }
824 else if ((deltai < gammai) < i){
825 uint8_t rel_enc__[18] = {0, 1, 1, 0, 0, 1, 0, 1, 1, 0, 1, 0, 1, 0, 0, 0, 1, 1};
826 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
827 }
828 else if ((gammai < i) < deltai){
829 uint8_t rel_enc__[18] = {0, 1, 1, 0, 1, 0, 1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 0, 1};
830 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
831 }
832 else if ((i < gammai) < deltai){
833 uint8_t rel_enc__[18] = {1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0, 0, 1, 1, 0, 0, 1};
834 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
835 }
836 else if ((deltai < i) < gammai){
837 uint8_t rel_enc__[18] = {0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0};
838 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
839 }
840 else {
841 uint8_t rel_enc__[18] = {0, 1, 1, 0, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 1, 1};
842 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
843 }
844 trs_current = (trans_t *)malloc(sizeof(trans_t));
845 trs_current->bdd = sylvan_cube(relvarset1, rel_enc1);
846 trs_current->varset.varset = relvarset1;
847 trs_current->varset.size = 18;
848 trs_current->next_rel = trs;
849 trs = trs_current;
850
851 //Agent Targbox Target -> Free Targagent Targbox
852 //(1 0 0 0 1 1 1 1 0 1 0 0 0 1 1 0 1 0)
853 //or
854 //(1 1 0 1 0 0 0 1 1 0 1 0 1 0 0 0 1 1)
855 //or
856 //(0 1 1 0 1 0 1 0 0 0 1 1 1 1 0 1 0 0)
857 //or
858 //(1 0 0 0 1 1 0 1 1 0 1 0 1 1 0 1 0 0)
859 //or
860 //(1 1 0 1 0 0 1 0 0 0 1 1 0 1 1 0 1 0)
861 //or
862 //(0 1 1 0 1 0 1 1 0 1 0 0 1 0 0 0 1 1)
863 relvarset1 = sylvan_set_fromarray(relvars1, 18);
864 if ((i < deltai) < gammai){
865 uint8_t rel_enc__[18] = {1, 0, 0, 0, 1, 1, 1, 1, 0, 1, 0, 0, 0, 1, 1, 0, 1, 0};
866 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
867 }
868 else if ((deltai < gammai) < i){
869 uint8_t rel_enc__[18] = {1, 1, 0, 1, 0, 0, 0, 1, 1, 0, 1, 0, 1, 0, 0, 0, 1, 1};
870 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
871 }
872 else if ((gammai < i) < deltai){
873 uint8_t rel_enc__[18] = {0, 1, 1, 0, 1, 0, 1, 0, 0, 0, 1, 1, 1, 1, 0, 1, 0, 0};
874 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
875 }
876 else if ((i < gammai) < deltai){
877 uint8_t rel_enc__[18] = {1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0, 0};
878 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
879 }
880 else if ((deltai < i) < gammai){
881 uint8_t rel_enc__[18] = {1, 1, 0, 1, 0, 0, 1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0};
882 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
883 }
884 else {
885 uint8_t rel_enc__[18] = {0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0, 0, 1, 0, 0, 0, 1, 1};
886 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
887 }
888 trs_current = (trans_t *)malloc(sizeof(trans_t));
889 trs_current->bdd = sylvan_cube(relvarset1, rel_enc1);
890 trs_current->varset.varset = relvarset1;
891 trs_current->varset.size = 18;
892 trs_current->next_rel = trs;
893 trs = trs_current;
894
895 //Targagent Box Free -> Target Agent Box
896 //(1 0 1 1 0 1 0 1 1 0 0 1 0 0 0 1 1 0)
897 //or
898 //(0 1 1 0 0 1 0 0 0 1 1 0 1 0 1 1 0 1)
899 //or
900 //(0 0 0 1 1 0 1 0 1 1 0 1 0 1 1 0 0 1)
901 //or
902 //(1 0 1 1 0 1 0 0 0 1 1 0 0 1 1 0 0 1)
903 //or
904 //(0 1 1 0 0 1 1 0 1 1 0 1 0 0 0 1 1 0)
905 //or
906 //(0 0 0 1 1 0 0 1 1 0 0 1 1 0 1 1 0 1)
907 relvarset1 = sylvan_set_fromarray(relvars1, 18);
908 if ((i < deltai) < gammai){
909 uint8_t rel_enc__[18] = {1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 0, 1, 0, 0, 0, 1, 1, 0};
910 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
911 }
912 else if ((deltai < gammai) < i){
913 uint8_t rel_enc__[18] = {0, 1, 1, 0, 0, 1, 0, 0, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1};
914 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
915 }
916 else if ((gammai < i) < deltai){
917 uint8_t rel_enc__[18] = {0, 0, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 0, 1};
918 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
919 }
920 else if ((i < gammai) < deltai){
921 uint8_t rel_enc__[18] = {1, 0, 1, 1, 0, 1, 0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1};
922 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
923 }
924 else if ((deltai < i) < gammai){
925 uint8_t rel_enc__[18] = {0, 1, 1, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0, 0, 0, 1, 1, 0};
926 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
927 }
928 else {
929 uint8_t rel_enc__[18] = {0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 1, 1, 0, 1};
930 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
931 }
932 trs_current = (trans_t *)malloc(sizeof(trans_t));
933 trs_current->bdd = sylvan_cube(relvarset1, rel_enc1);
934 trs_current->varset.varset = relvarset1;
935 trs_current->varset.size = 18;
936 trs_current->next_rel = trs;
937 trs = trs_current;
938
939 //Targagent Targbox Free -> Target Targagent Box
940 //(1 0 1 1 0 1 1 1 0 1 0 0 0 0 0 1 1 0)
941 //or
942 //(1 1 0 1 0 0 0 0 0 1 1 0 1 0 1 1 0 1)
943 //or
944 //(0 0 0 1 1 0 1 0 1 1 0 1 1 1 0 1 0 0)
945 //or
946 //(1 0 1 1 0 1 0 0 0 1 1 0 1 1 0 1 0 0)
947 //or
948 //(1 1 0 1 0 0 1 0 1 1 0 1 0 0 0 1 1 0)
949 //or
950 //(0 0 0 1 1 0 1 1 0 1 0 0 1 0 1 1 0 1)
951 relvarset1 = sylvan_set_fromarray(relvars1, 18);
952 if ((i < deltai) < gammai){
953 uint8_t rel_enc__[18] = {1, 0, 1, 1, 0, 1, 1, 1, 0, 1, 0, 0, 0, 0, 0, 1, 1, 0};
954 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
955 }
956 else if ((deltai < gammai) < i){
957 uint8_t rel_enc__[18] = {1, 1, 0, 1, 0, 0, 0, 0, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1};
958 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
959 }
960 else if ((gammai < i) < deltai){
961 uint8_t rel_enc__[18] = {0, 0, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 1, 1, 0, 1, 0, 0};
962 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
963 }
964 else if ((i < gammai) < deltai){
965 uint8_t rel_enc__[18] = {1, 0, 1, 1, 0, 1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0, 0};
966 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
967 }
968 else if ((deltai < i) < gammai){
969 uint8_t rel_enc__[18] = {1, 1, 0, 1, 0, 0, 1, 0, 1, 1, 0, 1, 0, 0, 0, 1, 1, 0};
970 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
971 }
972 else {
973 uint8_t rel_enc__[18] = {0, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0, 0, 1, 0, 1, 1, 0, 1};
974 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
975 }
976 trs_current = (trans_t *)malloc(sizeof(trans_t));
977 trs_current->bdd = sylvan_cube(relvarset1, rel_enc1);
978 trs_current->varset.varset = relvarset1;
979 trs_current->varset.size = 18;
980 trs_current->next_rel = trs;
981 trs = trs_current;
982
983 //Targagent Box Target -> Target Agent Targbox
984 //(1 0 1 1 0 1 0 1 1 0 0 1 0 1 1 0 1 0)
985 //or
986 //(0 1 1 0 0 1 0 1 1 0 1 0 1 0 1 1 0 1)
987 //or
988 //(0 1 1 0 1 0 1 0 1 1 0 1 0 1 1 0 0 1)
989 //or
990 //(1 0 1 1 0 1 0 1 1 0 1 0 0 1 1 0 0 1)
991 //or
992 //(0 1 1 0 0 1 1 0 1 1 0 1 0 1 1 0 1 0)
993 //or
994 //(0 1 1 0 1 0 0 1 1 0 0 1 1 0 1 1 0 1)
995 relvarset1 = sylvan_set_fromarray(relvars1, 18);
996 if ((i < deltai) < gammai){
997 uint8_t rel_enc__[18] = {1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 0, 1, 0, 1, 1, 0, 1, 0};
998 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
999 }
1000 else if ((deltai < gammai) < i){
1001 uint8_t rel_enc__[18] = {0, 1, 1, 0, 0, 1, 0, 1, 1, 0, 1, 0, 1, 0, 1, 1, 0, 1};
1002 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
1003 }
1004 else if ((gammai < i) < deltai){
1005 uint8_t rel_enc__[18] = {0, 1, 1, 0, 1, 0, 1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 0, 1};
1006 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
1007 }
1008 else if ((i < gammai) < deltai){
1009 uint8_t rel_enc__[18] = {1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0, 0, 1, 1, 0, 0, 1};
1010 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
1011 }
1012 else if ((deltai < i) < gammai){
1013 uint8_t rel_enc__[18] = {0, 1, 1, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0};
1014 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
1015 }
1016 else {
1017 uint8_t rel_enc__[18] = {0, 1, 1, 0, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 1, 1, 0, 1};
1018 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
1019 }
1020 trs_current = (trans_t *)malloc(sizeof(trans_t));
1021 trs_current->bdd = sylvan_cube(relvarset1, rel_enc1);
1022 trs_current->varset.varset = relvarset1;
1023 trs_current->varset.size = 18;
1024 trs_current->next_rel = trs;
1025 trs = trs_current;
1026
1027 //Targagent Targbox Target -> Target Targagent Targbox
1028 //(1 0 1 1 0 1 1 1 0 1 0 0 0 1 1 0 1 0)
1029 //or
1030 //(1 1 0 1 0 0 0 1 1 0 1 0 1 0 1 1 0 1)
1031 //or
1032 //(0 1 1 0 1 0 1 0 1 1 0 1 1 1 0 1 0 0)
1033 //or
1034 //(1 0 1 1 0 1 0 1 1 0 1 0 1 1 0 1 0 0)
1035 //or
1036 //(1 1 0 1 0 0 1 0 1 1 0 1 0 1 1 0 1 0)
1037 //or
1038 //(1 1 0 1 0 0 1 0 1 1 0 1 0 1 1 0 1 0)
1039 relvarset1 = sylvan_set_fromarray(relvars1, 18);
1040 if ((i < deltai) < gammai){
1041 uint8_t rel_enc__[18] = {1, 0, 1, 1, 0, 1, 1, 1, 0, 1, 0, 0, 0, 1, 1, 0, 1, 0};
1042 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
1043 }
1044 else if ((deltai < gammai) < i){
1045 uint8_t rel_enc__[18] = {1, 1, 0, 1, 0, 0, 0, 1, 1, 0, 1, 0, 1, 0, 1, 1, 0, 1};
1046 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
1047 }
1048 else if ((gammai < i) < deltai){
1049 uint8_t rel_enc__[18] = {0, 1, 1, 0, 1, 0, 1, 0, 1, 1, 0, 1, 1, 1, 0, 1, 0, 0};
1050 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
1051 }
1052 else if ((i < gammai) < deltai){
1053 uint8_t rel_enc__[18] = {1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0, 0};
1054 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
1055 }
1056 else if ((deltai < i) < gammai){
1057 uint8_t rel_enc__[18] = {1, 1, 0, 1, 0, 0, 1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0};
1058 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
1059 }
1060 else {
1061 uint8_t rel_enc__[18] = {1, 1, 0, 1, 0, 0, 1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0};
1062 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
1063 }
1064 trs_current = (trans_t *)malloc(sizeof(trans_t));
1065 trs_current->bdd = sylvan_cube(relvarset1, rel_enc1);
1066 trs_current->varset.varset = relvarset1;
1067 trs_current->varset.size = 18;
1068 trs_current->next_rel = trs;
1069 trs = trs_current;
1070 }
1071 }
1072 trs_current = trs;
1073
1074 //test
1075 switch(dir){
1076 case LEFT:
1077 if (trs_current != NULL) printf("LEFT ok!\n");
1078 else printf ("LEFT is empty\n");
1079 printf("Num of trans relations:%d\n", countTrans(trs));
1080 break;
1081 case UP:
1082 if (trs_current != NULL) printf("UP ok!\n");
1083 else printf ("UP is empty\n");
1084 printf("Num of trans relations:%d\n", countTrans(trs));
1085 break;
1086 case RIGHT:
1087 if (trs_current != NULL) printf("RIGHT ok!\n");
1088 else printf ("RIGHT is empty\n");
1089 printf("Num of trans relations:%d\n", countTrans(trs));
1090 break;
1091 case DOWN:
1092 if (trs_current != NULL) printf("DOWN ok!\n");
1093 else printf ("DOWN is empty\n");
1094 printf("Num of trans relations:%d\n", countTrans(trs));
1095 break;
1096 }
1097
1098 return trs;
1099 }
1100
1101 //test
1102 int countTrans(trans_t *trs)
1103 {
1104 int counter = 0;
1105 while (trs != NULL){
1106 counter++;
1107 trs = trs->next_rel;
1108 }
1109 return counter;
1110 }
1111
1112 rels *encode_rel(sokoban_screen *screen)
1113 {
1114 LACE_ME;
1115
1116 trans_t *tl = sylvan_false;
1117
1118 //left relation
1119 tl = create_single_rel(screen, LEFT);
1120
1121 //up relation
1122 trans_t *tu = create_single_rel(screen, UP);
1123
1124 //right relation
1125 trans_t *tr = create_single_rel(screen, RIGHT);
1126
1127 //down relation
1128 trans_t *td = create_single_rel(screen, DOWN);
1129
1130 rels *rls = NULL;
1131 rls = (rels *)malloc(sizeof(rels));
1132 rls->rell = tl;
1133 rls->relu = tu;
1134 rls->relr = tr;
1135 rls->reld = td;
1136
1137 return rls;
1138 }
1139
1140 int test_trans(state *s, trans_t *t)
1141 {
1142 LACE_ME;
1143 int counter = 0;
1144 BDD next = sylvan_false;
1145 while (t != NULL){
1146 next = sylvan_relnext(s->bdd, t->bdd, t->varset.varset);
1147 if (next == s->bdd) printf("Same\n");
1148 if (next != s->bdd && next != sylvan_false) printf("Different\n");
1149 if (next == sylvan_false) printf("False\n");
1150 t = t->next_rel;
1151 }
1152 printf("Trans:%d\n", counter);
1153 return 1;
1154 }
Unnamed repository; edit this file 'description' to name the repository.