repositories / mc1516pa.git / blob
? search:


d9a924a5bffe263c9feae12ced853e09df901401
[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;
70 f->value.var[1] = varcount + 1;
71 f->value.var[2] = varcount + 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;
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*3, 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 rel_enc[0] = 1;
277 rel_enc[1] = 1;
278 rel_enc[2] = 1;
279 rel_enc[3] = 1;
280 rel_enc[4] = 0;
281 rel_enc[5] = 0;
282
283 trs_current = (trans_t *)malloc(sizeof(trans_t));
284 trs_current->bdd = sylvan_cube(relvarset, rel_enc);
285 trs_current->varset.varset = relvarset;
286 trs_current->varset.size = 6;
287 trs_current->next_rel = trs;
288 trs = trs_current;
289
290 }
291 else if (check_space(x, y, dir, 1, bm) == 1 && check_space(x, y, dir, 2, bm) == 0){
292
293 xy_bddvar_map *bddvar = getxy(x + xdelta, y + ydelta, bm->f);
294 int deltai = bddvar->value.var[0];
295
296 //Agent Free -> Free Agent
297 //(1 0 0 0 1 1 0 1 0 0 1 1)
298 BDDVAR relvars[12] = {i*6, i*6+1, i*6+2, i*6+3, i*6+4, i*6+5, 2*deltai, 2*deltai+1, 2*deltai+2, 2*deltai+3, 2*deltai+4, 2*deltai+5};
299 BDDSET relvarset = sylvan_set_fromarray(relvars, 12);
300 uint8_t rel_enc[12] = {1, 0, 0, 0, 1, 1, 0, 1, 0, 0, 1, 1};
301 trs_current = (trans_t *)malloc(sizeof(trans_t));
302 trs_current->bdd = sylvan_cube(relvarset, rel_enc);
303 trs_current->varset.varset = relvarset;
304 trs_current->varset.size = 12;
305 trs_current->next_rel = trs;
306 trs = trs_current;
307
308 //Agent Target -> Free Targagent
309 //(1 0 0 0 1 1 0 1 1 1 1 0)
310 relvarset = sylvan_set_fromarray(relvars, 12);
311 rel_enc[0] = 1;
312 rel_enc[1] = 0;
313 rel_enc[2] = 0;
314 rel_enc[3] = 0;
315 rel_enc[4] = 1;
316 rel_enc[5] = 1;
317 rel_enc[6] = 0;
318 rel_enc[7] = 1;
319 rel_enc[8] = 1;
320 rel_enc[9] = 1;
321 rel_enc[10] = 1;
322 rel_enc[11] = 0;
323 trs_current = (trans_t *)malloc(sizeof(trans_t));
324 trs_current->bdd = sylvan_cube(relvarset, rel_enc);
325 trs_current->varset.varset = relvarset;
326 trs_current->varset.size = 12;
327 trs_current->next_rel = trs;
328 trs = trs_current;
329
330 //Targagent Free -> Target Agent
331 //(1 0 1 1 0 1 0 1 0 0 1 1)
332 relvarset = sylvan_set_fromarray(relvars, 12);
333 rel_enc[0] = 1;
334 rel_enc[1] = 0;
335 rel_enc[2] = 1;
336 rel_enc[3] = 1;
337 rel_enc[4] = 0;
338 rel_enc[5] = 1;
339 rel_enc[6] = 0;
340 rel_enc[7] = 1;
341 rel_enc[8] = 0;
342 rel_enc[9] = 0;
343 rel_enc[10] = 1;
344 rel_enc[11] = 1;
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 relvarset = sylvan_set_fromarray(relvars, 12);
355 rel_enc[0] = 1;
356 rel_enc[1] = 0;
357 rel_enc[2] = 1;
358 rel_enc[3] = 1;
359 rel_enc[4] = 0;
360 rel_enc[5] = 1;
361 rel_enc[6] = 0;
362 rel_enc[7] = 1;
363 rel_enc[8] = 1;
364 rel_enc[9] = 1;
365 rel_enc[10] = 1;
366 rel_enc[11] = 0;
367 trs_current = (trans_t *)malloc(sizeof(trans_t));
368 trs_current->bdd = sylvan_cube(relvarset, rel_enc);
369 trs_current->varset.varset = relvarset;
370 trs_current->varset.size = 12;
371 trs_current->next_rel = trs;
372 trs = trs_current;
373
374 //Agent Box -> Agent Box
375 //(1 1 0 0 1 1 0 0 1 1 0 0)
376 relvarset = sylvan_set_fromarray(relvars, 12);
377 rel_enc[0] = 1;
378 rel_enc[1] = 1;
379 rel_enc[2] = 0;
380 rel_enc[3] = 0;
381 rel_enc[4] = 1;
382 rel_enc[5] = 1;
383 rel_enc[6] = 0;
384 rel_enc[7] = 0;
385 rel_enc[8] = 1;
386 rel_enc[9] = 1;
387 rel_enc[10] = 0;
388 rel_enc[11] = 0;
389 trs_current = (trans_t *)malloc(sizeof(trans_t));
390 trs_current->bdd = sylvan_cube(relvarset, rel_enc);
391 trs_current->varset.varset = relvarset;
392 trs_current->varset.size = 12;
393 trs_current->next_rel = trs;
394 trs = trs_current;
395
396 //Agent Targbox -> Agent Targbox
397 //(1 1 0 0 1 1 1 1 0 0 0 0)
398 relvarset = sylvan_set_fromarray(relvars, 12);
399 rel_enc[0] = 1;
400 rel_enc[1] = 1;
401 rel_enc[2] = 0;
402 rel_enc[3] = 0;
403 rel_enc[4] = 1;
404 rel_enc[5] = 1;
405 rel_enc[6] = 1;
406 rel_enc[7] = 1;
407 rel_enc[8] = 0;
408 rel_enc[9] = 0;
409 rel_enc[10] = 0;
410 rel_enc[11] = 0;
411 trs_current = (trans_t *)malloc(sizeof(trans_t));
412 trs_current->bdd = sylvan_cube(relvarset, rel_enc);
413 trs_current->varset.varset = relvarset;
414 trs_current->varset.size = 12;
415 trs_current->next_rel = trs;
416 trs = trs_current;
417
418 //Targagent Box -> Targagent Box
419 //(1 1 1 1 0 0 0 0 1 1 0 0)
420 relvarset = sylvan_set_fromarray(relvars, 12);
421 rel_enc[0] = 1;
422 rel_enc[1] = 1;
423 rel_enc[2] = 1;
424 rel_enc[3] = 1;
425 rel_enc[4] = 0;
426 rel_enc[5] = 0;
427 rel_enc[6] = 0;
428 rel_enc[7] = 0;
429 rel_enc[8] = 1;
430 rel_enc[9] = 1;
431 rel_enc[10] = 0;
432 rel_enc[11] = 0;
433 trs_current = (trans_t *)malloc(sizeof(trans_t));
434 trs_current->bdd = sylvan_cube(relvarset, rel_enc);
435 trs_current->varset.varset = relvarset;
436 trs_current->varset.size = 12;
437 trs_current->next_rel = trs;
438 trs = trs_current;
439
440 //Targagent Targbox -> Targagent Targbox
441 //(1 1 1 1 0 0 1 1 0 0 0 0)
442 relvarset = sylvan_set_fromarray(relvars, 12);
443 rel_enc[0] = 1;
444 rel_enc[1] = 1;
445 rel_enc[2] = 1;
446 rel_enc[3] = 1;
447 rel_enc[4] = 0;
448 rel_enc[5] = 0;
449 rel_enc[6] = 1;
450 rel_enc[7] = 1;
451 rel_enc[8] = 0;
452 rel_enc[9] = 0;
453 rel_enc[10] = 0;
454 rel_enc[11] = 0;
455 trs_current = (trans_t *)malloc(sizeof(trans_t));
456 trs_current->bdd = sylvan_cube(relvarset, rel_enc);
457 trs_current->varset.varset = relvarset;
458 trs_current->varset.size = 12;
459 trs_current->next_rel = trs;
460 trs = trs_current;
461
462 }
463 else if (check_space(x, y, dir, 1, bm) == 1 && check_space(x, y, dir, 2, bm) == 1){
464
465 xy_bddvar_map *bddvar = getxy(x + xdelta, y + ydelta, bm->f);
466 int deltai = bddvar->value.var[0];
467 bddvar = getxy(x + xgamma, y + ygamma, bm->f);
468 int gammai = bddvar->value.var[0];
469
470 //Agent Free -> Free Agent
471 //(1 0 0 0 1 1 0 1 0 0 1 1)
472 BDDVAR relvars[12] = {i*6, i*6+1, i*6+2, i*6+3, i*6+4, i*6+5, 2*deltai, 2*deltai+1, i*deltai+2, 2*deltai+3, 2*deltai+4, 2*deltai+5};
473 BDDSET relvarset = sylvan_set_fromarray(relvars, 12);
474 uint8_t rel_enc[12] = {1, 0, 0, 0, 1, 1, 0, 1, 0, 0, 1, 1};
475 trs_current = (trans_t *)malloc(sizeof(trans_t));
476 trs_current->bdd = sylvan_cube(relvarset, rel_enc);
477 trs_current->varset.varset = relvarset;
478 trs_current->varset.size = 12;
479 trs_current->next_rel = trs;
480 trs = trs_current;
481
482 //Agent Target -> Free Targagent
483 //(1 0 0 0 1 1 0 1 1 1 1 0)
484 relvarset = sylvan_set_fromarray(relvars, 12);
485 rel_enc[0] = 1;
486 rel_enc[1] = 0;
487 rel_enc[2] = 0;
488 rel_enc[3] = 0;
489 rel_enc[4] = 1;
490 rel_enc[5] = 1;
491 rel_enc[6] = 0;
492 rel_enc[7] = 1;
493 rel_enc[8] = 1;
494 rel_enc[9] = 1;
495 rel_enc[10] = 1;
496 rel_enc[11] = 0;
497 trs_current = (trans_t *)malloc(sizeof(trans_t));
498 trs_current->bdd = sylvan_cube(relvarset, rel_enc);
499 trs_current->varset.varset = relvarset;
500 trs_current->varset.size = 12;
501 trs_current->next_rel = trs;
502 trs = trs_current;
503
504 //Targagent Free -> Target Agent
505 //(1 0 1 1 0 1 0 1 0 0 1 1)
506 relvarset = sylvan_set_fromarray(relvars, 12);
507 rel_enc[0] = 1;
508 rel_enc[1] = 0;
509 rel_enc[2] = 1;
510 rel_enc[3] = 1;
511 rel_enc[4] = 0;
512 rel_enc[5] = 1;
513 rel_enc[6] = 0;
514 rel_enc[7] = 1;
515 rel_enc[8] = 0;
516 rel_enc[9] = 0;
517 rel_enc[10] = 1;
518 rel_enc[11] = 1;
519 trs_current = (trans_t *)malloc(sizeof(trans_t));
520 trs_current->bdd = sylvan_cube(relvarset, rel_enc);
521 trs_current->varset.varset = relvarset;
522 trs_current->varset.size = 12;
523 trs_current->next_rel = trs;
524 trs = trs_current;
525
526 //Targagent Target -> Target Targagent
527 //(1 0 1 1 0 1 0 1 1 1 1 0)
528 relvarset = sylvan_set_fromarray(relvars, 12);
529 rel_enc[0] = 1;
530 rel_enc[1] = 0;
531 rel_enc[2] = 1;
532 rel_enc[3] = 1;
533 rel_enc[4] = 0;
534 rel_enc[5] = 1;
535 rel_enc[6] = 0;
536 rel_enc[7] = 1;
537 rel_enc[8] = 1;
538 rel_enc[9] = 1;
539 rel_enc[10] = 1;
540 rel_enc[11] = 0;
541 trs_current = (trans_t *)malloc(sizeof(trans_t));
542 trs_current->bdd = sylvan_cube(relvarset, rel_enc);
543 trs_current->varset.varset = relvarset;
544 trs_current->varset.size = 12;
545 trs_current->next_rel = trs;
546 trs = trs_current;
547
548 //Agent Box Box -> Agent Box Box
549 //(1 1 0 0 1 1 0 0 1 1 0 0 0 0 1 1 0 0)
550 BDDVAR relvars1[18] = {i*6, i*6+1, i*6+2, i*6+3, i*6+4, i*6+5, 2*deltai, 2*deltai+1, 2*deltai+2, 2*deltai+3, 2*deltai+4, 2*deltai+5, 2*gammai, 2*gammai+1, 2*gammai+2, 2*gammai+3, 2*gammai+4, 2*gammai+5};
551 BDD relvarset1 = sylvan_set_fromarray(relvars1, 18);
552 uint8_t rel_enc1[18];
553 rel_enc1[0] = 1;
554 rel_enc1[1] = 1;
555 rel_enc1[2] = 0;
556 rel_enc1[3] = 0;
557 rel_enc1[4] = 1;
558 rel_enc1[5] = 1;
559 rel_enc1[6] = 0;
560 rel_enc1[7] = 0;
561 rel_enc1[8] = 1;
562 rel_enc1[9] = 1;
563 rel_enc1[10] = 0;
564 rel_enc1[11] = 0;
565 rel_enc1[12] = 0;
566 rel_enc1[13] = 0;
567 rel_enc1[14] = 1;
568 rel_enc1[15] = 1;
569 rel_enc1[16] = 0;
570 rel_enc1[17] = 0;
571 trs_current = (trans_t *)malloc(sizeof(trans_t));
572 trs_current->bdd = sylvan_cube(relvarset1, rel_enc1);
573 trs_current->varset.varset = relvarset1;
574 trs_current->varset.size = 18;
575 trs_current->next_rel = trs;
576 trs = trs_current;
577
578 //Agent Box Targbox -> Agent Box Targbox
579 //(1 1 0 0 1 1 0 0 1 1 0 0 1 1 0 0 0 0)
580 relvarset1 = sylvan_set_fromarray(relvars1, 18);
581 rel_enc1[0] = 1;
582 rel_enc1[1] = 1;
583 rel_enc1[2] = 0;
584 rel_enc1[3] = 0;
585 rel_enc1[4] = 1;
586 rel_enc1[5] = 1;
587 rel_enc1[6] = 0;
588 rel_enc1[7] = 0;
589 rel_enc1[8] = 1;
590 rel_enc1[9] = 1;
591 rel_enc1[10] = 0;
592 rel_enc1[11] = 0;
593 rel_enc1[12] = 1;
594 rel_enc1[13] = 1;
595 rel_enc1[14] = 0;
596 rel_enc1[15] = 0;
597 rel_enc1[16] = 0;
598 rel_enc1[17] = 0;
599 trs_current = (trans_t *)malloc(sizeof(trans_t));
600 trs_current->bdd = sylvan_cube(relvarset1, rel_enc1);
601 trs_current->varset.varset = relvarset1;
602 trs_current->varset.size = 18;
603 trs_current->next_rel = trs;
604 trs = trs_current;
605
606 //Targagent Box Box -> Targagent Box Box
607 //(1 1 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0)
608 relvarset1 = sylvan_set_fromarray(relvars1, 18);
609 rel_enc1[0] = 1;
610 rel_enc1[1] = 1;
611 rel_enc1[2] = 1;
612 rel_enc1[3] = 1;
613 rel_enc1[4] = 0;
614 rel_enc1[5] = 0;
615 rel_enc1[6] = 0;
616 rel_enc1[7] = 0;
617 rel_enc1[8] = 1;
618 rel_enc1[9] = 1;
619 rel_enc1[10] = 0;
620 rel_enc1[11] = 0;
621 rel_enc1[12] = 0;
622 rel_enc1[13] = 0;
623 rel_enc1[14] = 1;
624 rel_enc1[15] = 1;
625 rel_enc1[16] = 0;
626 rel_enc1[17] = 0;
627 trs_current = (trans_t *)malloc(sizeof(trans_t));
628 trs_current->bdd = sylvan_cube(relvarset1, rel_enc1);
629 trs_current->varset.varset = relvarset1;
630 trs_current->varset.size = 18;
631 trs_current->next_rel = trs;
632 trs = trs_current;
633
634 //Targagent Box Targbox -> Targagent Box Targbox
635 //(1 1 1 1 0 0 0 0 1 1 0 0 1 1 0 0 0 0)
636 relvarset1 = sylvan_set_fromarray(relvars1, 18);
637 rel_enc1[0] = 1;
638 rel_enc1[1] = 1;
639 rel_enc1[2] = 1;
640 rel_enc1[3] = 1;
641 rel_enc1[4] = 0;
642 rel_enc1[5] = 0;
643 rel_enc1[6] = 0;
644 rel_enc1[7] = 0;
645 rel_enc1[8] = 1;
646 rel_enc1[9] = 1;
647 rel_enc1[10] = 0;
648 rel_enc1[11] = 0;
649 rel_enc1[12] = 1;
650 rel_enc1[13] = 1;
651 rel_enc1[14] = 0;
652 rel_enc1[15] = 0;
653 rel_enc1[16] = 0;
654 rel_enc1[17] = 0;
655 trs_current = (trans_t *)malloc(sizeof(trans_t));
656 trs_current->bdd = sylvan_cube(relvarset1, rel_enc1);
657 trs_current->varset.varset = relvarset1;
658 trs_current->varset.size = 18;
659 trs_current->next_rel = trs;
660 trs = trs_current;
661
662 //Agent Box Free -> Free Agent Box
663 //(1 0 0 0 1 1 0 1 1 0 0 1 0 0 0 1 1 0)
664 relvarset1 = sylvan_set_fromarray(relvars1, 18);
665 rel_enc1[0] = 1;
666 rel_enc1[1] = 0;
667 rel_enc1[2] = 0;
668 rel_enc1[3] = 0;
669 rel_enc1[4] = 1;
670 rel_enc1[5] = 1;
671 rel_enc1[6] = 0;
672 rel_enc1[7] = 1;
673 rel_enc1[8] = 1;
674 rel_enc1[9] = 0;
675 rel_enc1[10] = 0;
676 rel_enc1[11] = 1;
677 rel_enc1[12] = 0;
678 rel_enc1[13] = 0;
679 rel_enc1[14] = 0;
680 rel_enc1[15] = 1;
681 rel_enc1[16] = 1;
682 rel_enc1[17] = 0;
683 trs_current = (trans_t *)malloc(sizeof(trans_t));
684 trs_current->bdd = sylvan_cube(relvarset1, rel_enc1);
685 trs_current->varset.varset = relvarset1;
686 trs_current->varset.size = 18;
687 trs_current->next_rel = trs;
688 trs = trs_current;
689
690 //Agent Targbox Free -> Free Targagent Box
691 //(1 0 0 0 1 1 1 1 0 1 0 0 0 0 0 1 1 0)
692 relvarset1 = sylvan_set_fromarray(relvars1, 18);
693 rel_enc1[0] = 1;
694 rel_enc1[1] = 0;
695 rel_enc1[2] = 0;
696 rel_enc1[3] = 0;
697 rel_enc1[4] = 1;
698 rel_enc1[5] = 1;
699 rel_enc1[6] = 1;
700 rel_enc1[7] = 1;
701 rel_enc1[8] = 0;
702 rel_enc1[9] = 1;
703 rel_enc1[10] = 0;
704 rel_enc1[11] = 0;
705 rel_enc1[12] = 0;
706 rel_enc1[13] = 0;
707 rel_enc1[14] = 0;
708 rel_enc1[15] = 1;
709 rel_enc1[16] = 1;
710 rel_enc1[17] = 0;
711 trs_current = (trans_t *)malloc(sizeof(trans_t));
712 trs_current->bdd = sylvan_cube(relvarset1, rel_enc1);
713 trs_current->varset.varset = relvarset1;
714 trs_current->varset.size = 18;
715 trs_current->next_rel = trs;
716 trs = trs_current;
717
718 //Agent Box Target -> Free Agent Targbox
719 //(1 0 0 0 1 1 0 1 1 0 0 1 0 1 1 0 1 0)
720 relvarset1 = sylvan_set_fromarray(relvars1, 18);
721 rel_enc1[0] = 1;
722 rel_enc1[1] = 0;
723 rel_enc1[2] = 0;
724 rel_enc1[3] = 0;
725 rel_enc1[4] = 1;
726 rel_enc1[5] = 1;
727 rel_enc1[6] = 0;
728 rel_enc1[7] = 1;
729 rel_enc1[8] = 1;
730 rel_enc1[9] = 0;
731 rel_enc1[10] = 0;
732 rel_enc1[11] = 1;
733 rel_enc1[12] = 0;
734 rel_enc1[13] = 1;
735 rel_enc1[14] = 1;
736 rel_enc1[15] = 0;
737 rel_enc1[16] = 1;
738 rel_enc1[17] = 0;
739 trs_current = (trans_t *)malloc(sizeof(trans_t));
740 trs_current->bdd = sylvan_cube(relvarset1, rel_enc1);
741 trs_current->varset.varset = relvarset1;
742 trs_current->varset.size = 18;
743 trs_current->next_rel = trs;
744 trs = trs_current;
745
746 //Agent Targbox Target -> Free Targagent Targbox
747 //(1 0 0 0 1 1 1 1 0 1 0 0 0 1 1 0 1 0)
748 relvarset1 = sylvan_set_fromarray(relvars1, 18);
749 rel_enc1[0] = 1;
750 rel_enc1[1] = 0;
751 rel_enc1[2] = 0;
752 rel_enc1[3] = 0;
753 rel_enc1[4] = 1;
754 rel_enc1[5] = 1;
755 rel_enc1[6] = 1;
756 rel_enc1[7] = 1;
757 rel_enc1[8] = 0;
758 rel_enc1[9] = 1;
759 rel_enc1[10] = 0;
760 rel_enc1[11] = 0;
761 rel_enc1[12] = 0;
762 rel_enc1[13] = 1;
763 rel_enc1[14] = 1;
764 rel_enc1[15] = 0;
765 rel_enc1[16] = 1;
766 rel_enc1[17] = 0;
767 trs_current = (trans_t *)malloc(sizeof(trans_t));
768 trs_current->bdd = sylvan_cube(relvarset1, rel_enc1);
769 trs_current->varset.varset = relvarset1;
770 trs_current->varset.size = 18;
771 trs_current->next_rel = trs;
772 trs = trs_current;
773
774 //Targagent Box Free -> Target Agent Box
775 //(1 0 1 1 0 1 0 1 1 0 0 1 0 0 0 1 1 0)
776 relvarset1 = sylvan_set_fromarray(relvars1, 18);
777 rel_enc1[0] = 0;
778 rel_enc1[1] = 0;
779 rel_enc1[2] = 0;
780 rel_enc1[3] = 1;
781 rel_enc1[4] = 1;
782 rel_enc1[5] = 0;
783 rel_enc1[6] = 0;
784 rel_enc1[7] = 1;
785 rel_enc1[8] = 1;
786 rel_enc1[9] = 0;
787 rel_enc1[10] = 0;
788 rel_enc1[11] = 1;
789 rel_enc1[12] = 1;
790 rel_enc1[13] = 0;
791 rel_enc1[14] = 1;
792 rel_enc1[15] = 1;
793 rel_enc1[16] = 0;
794 rel_enc1[17] = 1;
795 trs_current = (trans_t *)malloc(sizeof(trans_t));
796 trs_current->bdd = sylvan_cube(relvarset1, rel_enc1);
797 trs_current->varset.varset = relvarset1;
798 trs_current->varset.size = 18;
799 trs_current->next_rel = trs;
800 trs = trs_current;
801
802 //Targagent Targbox Free -> Target Targagent Box
803 //(1 0 1 1 0 1 1 1 0 1 0 0 0 0 0 1 1 0)
804 relvarset1 = sylvan_set_fromarray(relvars1, 18);
805 rel_enc1[0] = 0;
806 rel_enc1[1] = 0;
807 rel_enc1[2] = 0;
808 rel_enc1[3] = 1;
809 rel_enc1[4] = 1;
810 rel_enc1[5] = 0;
811 rel_enc1[6] = 1;
812 rel_enc1[7] = 1;
813 rel_enc1[8] = 0;
814 rel_enc1[9] = 1;
815 rel_enc1[10] = 0;
816 rel_enc1[11] = 0;
817 rel_enc1[12] = 1;
818 rel_enc1[13] = 0;
819 rel_enc1[14] = 1;
820 rel_enc1[15] = 1;
821 rel_enc1[16] = 0;
822 rel_enc1[17] = 1;
823 trs_current = (trans_t *)malloc(sizeof(trans_t));
824 trs_current->bdd = sylvan_cube(relvarset1, rel_enc1);
825 trs_current->varset.varset = relvarset1;
826 trs_current->varset.size = 18;
827 trs_current->next_rel = trs;
828 trs = trs_current;
829
830 //Targagent Box Target -> Target Agent Targbox
831 //(1 0 1 1 0 1 0 1 1 0 0 1 0 1 1 0 1 0)
832 relvarset1 = sylvan_set_fromarray(relvars1, 18);
833 rel_enc1[0] = 1;
834 rel_enc1[1] = 0;
835 rel_enc1[2] = 1;
836 rel_enc1[3] = 1;
837 rel_enc1[4] = 0;
838 rel_enc1[5] = 1;
839 rel_enc1[6] = 0;
840 rel_enc1[7] = 1;
841 rel_enc1[8] = 1;
842 rel_enc1[9] = 0;
843 rel_enc1[10] = 0;
844 rel_enc1[11] = 1;
845 rel_enc1[12] = 0;
846 rel_enc1[13] = 1;
847 rel_enc1[14] = 1;
848 rel_enc1[15] = 0;
849 rel_enc1[16] = 1;
850 rel_enc1[17] = 0;
851 trs_current = (trans_t *)malloc(sizeof(trans_t));
852 trs_current->bdd = sylvan_cube(relvarset1, rel_enc1);
853 trs_current->varset.varset = relvarset1;
854 trs_current->varset.size = 18;
855 trs_current->next_rel = trs;
856 trs = trs_current;
857
858 //Targagent Targbox Target -> Target Targagent Targbox
859 //(1 0 1 1 0 1 1 1 0 1 0 0 0 1 1 0 1 0)
860 relvarset1 = sylvan_set_fromarray(relvars1, 18);
861 rel_enc1[0] = 1;
862 rel_enc1[1] = 0;
863 rel_enc1[2] = 1;
864 rel_enc1[3] = 1;
865 rel_enc1[4] = 0;
866 rel_enc1[5] = 1;
867 rel_enc1[6] = 1;
868 rel_enc1[7] = 1;
869 rel_enc1[8] = 0;
870 rel_enc1[9] = 1;
871 rel_enc1[10] = 0;
872 rel_enc1[11] = 0;
873 rel_enc1[12] = 0;
874 rel_enc1[13] = 1;
875 rel_enc1[14] = 1;
876 rel_enc1[15] = 0;
877 rel_enc1[16] = 1;
878 rel_enc1[17] = 0;
879 trs_current = (trans_t *)malloc(sizeof(trans_t));
880 trs_current->bdd = sylvan_cube(relvarset1, rel_enc1);
881 trs_current->varset.varset = relvarset1;
882 trs_current->varset.size = 18;
883 trs_current->next_rel = trs;
884 trs = trs_current;
885 }
886 }
887 trs_current = trs;
888
889 //test
890 switch(dir){
891 case LEFT:
892 if (trs_current != NULL) printf("LEFT ok!\n");
893 else printf ("LEFT is empty\n");
894 printf("Num of trans relations:%d\n", countTrans(trs));
895 break;
896 case UP:
897 if (trs_current != NULL) printf("UP ok!\n");
898 else printf ("UP is empty\n");
899 printf("Num of trans relations:%d\n", countTrans(trs));
900 break;
901 case RIGHT:
902 if (trs_current != NULL) printf("RIGHT ok!\n");
903 else printf ("RIGHT is empty\n");
904 printf("Num of trans relations:%d\n", countTrans(trs));
905 break;
906 case DOWN:
907 if (trs_current != NULL) printf("DOWN ok!\n");
908 else printf ("DOWN is empty\n");
909 printf("Num of trans relations:%d\n", countTrans(trs));
910 break;
911 }
912
913 return trs;
914 }
915
916 //test
917 int countTrans(trans_t *trs)
918 {
919 int counter = 0;
920 while (trs != NULL){
921 counter++;
922 trs = trs->next_rel;
923 }
924 return counter;
925 }
926
927 rels *encode_rel(sokoban_screen *screen)
928 {
929 LACE_ME;
930
931 trans_t *tl = sylvan_false;
932
933 //left relation
934 tl = create_single_rel(screen, LEFT);
935
936 //up relation
937 trans_t *tu = create_single_rel(screen, UP);
938
939 //right relation
940 trans_t *tr = create_single_rel(screen, RIGHT);
941
942 //down relation
943 trans_t *td = create_single_rel(screen, DOWN);
944
945 rels *rls = NULL;
946 rls = (rels *)malloc(sizeof(rels));
947 rls->rell = tl;
948 rls->relu = tu;
949 rls->relr = tr;
950 rls->reld = td;
951
952 return rls;
953 }
954
955 int test_trans(state *s, trans_t *t)
956 {
957 LACE_ME;
958 int counter = 0;
959 BDD next = sylvan_false;
960 while (t != NULL){
961 next = sylvan_relnext(s->bdd, t->bdd, t->varset.varset);
962 if (next == s->bdd) printf("Same\n");
963 if (next != s->bdd && next != sylvan_false) printf("Different\n");
964 if (next == sylvan_false) printf("False\n");
965 t = t->next_rel;
966 }
967 printf("Trans:%d\n", counter);
968 return 1;
969 }
Unnamed repository; edit this file 'description' to name the repository.