repositories / mc1516pa.git / blob
? search:


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