repositories / mc1516pa.git / blob
? search:
summary | shortlog | log | commit | commitdiff | tree
history | raw | HEAD
some repairs for transition vars
[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 //Agent -> Agent
268 //1 1 0 0 1 1 (1 0 1 -> 1 0 1)
269 BDDVAR relvars[6] = {i * 3, i * 3 + 1, i * 3 + 2, i * 3 + 3, i * 3 + 4, i * 3 + 5};
270 BDDSET relvarset = sylvan_set_fromarray(relvars, 6);
271 uint8_t rel_enc[6] = {1, 1, 0, 0, 1, 1};
272
273 trs_current = (trans_t *)malloc(sizeof(trans_t));
274 trs_current->bdd = sylvan_cube(relvarset, rel_enc);
275 trs_current->varset.varset = relvarset;
276 trs_current->varset.size = 6;
277 trs_current->next_rel = trs;
278 trs = trs_current;
279
280 //Targagent -> Targagent
281 //1 1 1 1 0 0 (1 1 0 -> 1 1 0)
282 relvars[0] = i * 3;
283 relvars[1] = i * 3 + 1;
284 relvars[2] = i * 3 + 2;
285 relvars[3] = i * 3 + 3;
286 relvars[4] = i * 3 + 4;
287 relvars[5] = i * 3 + 5;
288 relvarset = sylvan_set_fromarray(relvars, 6);
289 rel_enc[0] = 1;
290 rel_enc[1] = 1;
291 rel_enc[2] = 1;
292 rel_enc[3] = 1;
293 rel_enc[4] = 0;
294 rel_enc[5] = 0;
295
296 trs_current = (trans_t *)malloc(sizeof(trans_t));
297 trs_current->bdd = sylvan_cube(relvarset, rel_enc);
298 trs_current->varset.varset = relvarset;
299 trs_current->varset.size = 6;
300 trs_current->next_rel = trs;
301 trs = trs_current;
302
303 }
304 else if (check_space(x, y, dir, 1, bm) == 1 && check_space(x, y, dir, 2, bm) == 0){
305
306 xy_bddvar_map *bddvar = getxy(x + xdelta, y + ydelta, bm->f);
307 int deltai = bddvar->value.var[0];
308
309 //Free Agent -> Agent Free
310 //(0 1 0 0 1 1 1 0 0 0 1 1)
311 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};
312 BDDSET relvarset = sylvan_set_fromarray(relvars, 12);
313 uint8_t rel_enc[12] = {0, 1, 0, 0, 1, 1, 1, 0, 0, 0, 1, 1};
314 trs_current = (trans_t *)malloc(sizeof(trans_t));
315 trs_current->bdd = sylvan_cube(relvarset, rel_enc);
316 trs_current->varset.varset = relvarset;
317 trs_current->varset.size = 12;
318 trs_current->next_rel = trs;
319 trs = trs_current;
320
321 //Target Agent -> Targagent Free
322 //(0 1 1 1 1 0 1 0 0 0 1 1)
323 relvars[0] = deltai*3;
324 relvars[1] = deltai*3+1;
325 relvars[2] = deltai*3+2;
326 relvars[3] = deltai*3+3;
327 relvars[4] = deltai*3+4;
328 relvars[5] = deltai*3+5;
329 relvars[6] = i*3;
330 relvars[7] = i*3+1;
331 relvars[8] = i*3+2;
332 relvars[9] = i*3+3;
333 relvars[10] = i*3+4;
334 relvars[11] = i*3+5;
335 relvarset = sylvan_set_fromarray(relvars, 12);
336 rel_enc[0] = 0;
337 rel_enc[1] = 1;
338 rel_enc[2] = 1;
339 rel_enc[3] = 1;
340 rel_enc[4] = 1;
341 rel_enc[5] = 0;
342 rel_enc[6] = 1;
343 rel_enc[7] = 0;
344 rel_enc[8] = 0;
345 rel_enc[9] = 0;
346 rel_enc[10] = 1;
347 rel_enc[11] = 1;
348 trs_current = (trans_t *)malloc(sizeof(trans_t));
349 trs_current->bdd = sylvan_cube(relvarset, rel_enc);
350 trs_current->varset.varset = relvarset;
351 trs_current->varset.size = 12;
352 trs_current->next_rel = trs;
353 trs = trs_current;
354
355 //REPAIR! Must be: Free Targagent -> Agent Target
356 //(0 1 0 0 1 1 1 0 1 1 0 1)
357 relvars[0] = deltai*3;
358 relvars[1] = deltai*3+1;
359 relvars[2] = deltai*3+2;
360 relvars[3] = deltai*3+3;
361 relvars[4] = deltai*3+4;
362 relvars[5] = deltai*3+5;
363 relvars[6] = i*3;
364 relvars[7] = i*3+1;
365 relvars[8] = i*3+2;
366 relvars[9] = i*3+3;
367 relvars[10] = i*3+4;
368 relvars[11] = i*3+5;
369 relvarset = sylvan_set_fromarray(relvars, 12);
370 rel_enc[0] = 0;
371 rel_enc[1] = 1;
372 rel_enc[2] = 0;
373 rel_enc[3] = 0;
374 rel_enc[4] = 1;
375 rel_enc[5] = 1;
376 rel_enc[6] = 1;
377 rel_enc[7] = 0;
378 rel_enc[8] = 1;
379 rel_enc[9] = 1;
380 rel_enc[10] = 0;
381 rel_enc[11] = 1;
382 trs_current = (trans_t *)malloc(sizeof(trans_t));
383 trs_current->bdd = sylvan_cube(relvarset, rel_enc);
384 trs_current->varset.varset = relvarset;
385 trs_current->varset.size = 12;
386 trs_current->next_rel = trs;
387 trs = trs_current;
388
389 //Target Targagent -> Targagent Target
390 //(0 1 1 1 1 0 1 0 1 1 0 1)
391 relvars[0] = deltai*3;
392 relvars[1] = deltai*3+1;
393 relvars[2] = deltai*3+2;
394 relvars[3] = deltai*3+3;
395 relvars[4] = deltai*3+4;
396 relvars[5] = deltai*3+5;
397 relvars[6] = i*3;
398 relvars[7] = i*3+1;
399 relvars[8] = i*3+2;
400 relvars[9] = i*3+3;
401 relvars[10] = i*3+4;
402 relvars[11] = i*3+5;
403 relvarset = sylvan_set_fromarray(relvars, 12);
404 rel_enc[0] = 0;
405 rel_enc[1] = 1;
406 rel_enc[2] = 1;
407 rel_enc[3] = 1;
408 rel_enc[4] = 1;
409 rel_enc[5] = 0;
410 rel_enc[6] = 1;
411 rel_enc[7] = 0;
412 rel_enc[8] = 1;
413 rel_enc[9] = 1;
414 rel_enc[10] = 0;
415 rel_enc[11] = 1;
416 trs_current = (trans_t *)malloc(sizeof(trans_t));
417 trs_current->bdd = sylvan_cube(relvarset, rel_enc);
418 trs_current->varset.varset = relvarset;
419 trs_current->varset.size = 12;
420 trs_current->next_rel = trs;
421 trs = trs_current;
422
423 //Box Agent -> Box Agent
424 //(0 0 1 1 0 0 1 1 0 0 1 1)
425 relvars[0] = deltai*3;
426 relvars[1] = deltai*3+1;
427 relvars[2] = deltai*3+2;
428 relvars[3] = deltai*3+3;
429 relvars[4] = deltai*3+4;
430 relvars[5] = deltai*3+5;
431 relvars[6] = i*3;
432 relvars[7] = i*3+1;
433 relvars[8] = i*3+2;
434 relvars[9] = i*3+3;
435 relvars[10] = i*3+4;
436 relvars[11] = i*3+5;
437 relvarset = sylvan_set_fromarray(relvars, 12);
438 rel_enc[0] = 0;
439 rel_enc[1] = 0;
440 rel_enc[2] = 1;
441 rel_enc[3] = 1;
442 rel_enc[4] = 0;
443 rel_enc[5] = 0;
444 rel_enc[6] = 1;
445 rel_enc[7] = 1;
446 rel_enc[8] = 0;
447 rel_enc[9] = 0;
448 rel_enc[10] = 1;
449 rel_enc[11] = 1;
450 trs_current = (trans_t *)malloc(sizeof(trans_t));
451 trs_current->bdd = sylvan_cube(relvarset, rel_enc);
452 trs_current->varset.varset = relvarset;
453 trs_current->varset.size = 12;
454 trs_current->next_rel = trs;
455 trs = trs_current;
456
457 //Targbox Agent -> Targbox Agent
458 //(1 1 0 0 0 0 1 1 0 0 1 1)
459 relvars[0] = deltai*3;
460 relvars[1] = deltai*3+1;
461 relvars[2] = deltai*3+2;
462 relvars[3] = deltai*3+3;
463 relvars[4] = deltai*3+4;
464 relvars[5] = deltai*3+5;
465 relvars[6] = i*3;
466 relvars[7] = i*3+1;
467 relvars[8] = i*3+2;
468 relvars[9] = i*3+3;
469 relvars[10] = i*3+4;
470 relvars[11] = i*3+5;
471 relvarset = sylvan_set_fromarray(relvars, 12);
472 rel_enc[0] = 1;
473 rel_enc[1] = 1;
474 rel_enc[2] = 0;
475 rel_enc[3] = 0;
476 rel_enc[4] = 0;
477 rel_enc[5] = 0;
478 rel_enc[6] = 1;
479 rel_enc[7] = 1;
480 rel_enc[8] = 0;
481 rel_enc[9] = 0;
482 rel_enc[10] = 1;
483 rel_enc[11] = 1;
484 trs_current = (trans_t *)malloc(sizeof(trans_t));
485 trs_current->bdd = sylvan_cube(relvarset, rel_enc);
486 trs_current->varset.varset = relvarset;
487 trs_current->varset.size = 12;
488 trs_current->next_rel = trs;
489 trs = trs_current;
490
491 //Box Targagent -> Box Targagent
492 //(0 0 1 1 0 0 1 1 1 1 0 0)
493 relvars[0] = deltai*3;
494 relvars[1] = deltai*3+1;
495 relvars[2] = deltai*3+2;
496 relvars[3] = deltai*3+3;
497 relvars[4] = deltai*3+4;
498 relvars[5] = deltai*3+5;
499 relvars[6] = i*3;
500 relvars[7] = i*3+1;
501 relvars[8] = i*3+2;
502 relvars[9] = i*3+3;
503 relvars[10] = i*3+4;
504 relvars[11] = i*3+5;
505 relvarset = sylvan_set_fromarray(relvars, 12);
506 rel_enc[0] = 0;
507 rel_enc[1] = 0;
508 rel_enc[2] = 1;
509 rel_enc[3] = 1;
510 rel_enc[4] = 0;
511 rel_enc[5] = 0;
512 rel_enc[6] = 1;
513 rel_enc[7] = 1;
514 rel_enc[8] = 1;
515 rel_enc[9] = 1;
516 rel_enc[10] = 0;
517 rel_enc[11] = 0;
518 trs_current = (trans_t *)malloc(sizeof(trans_t));
519 trs_current->bdd = sylvan_cube(relvarset, rel_enc);
520 trs_current->varset.varset = relvarset;
521 trs_current->varset.size = 12;
522 trs_current->next_rel = trs;
523 trs = trs_current;
524
525 //Targbox Targagent -> Targbox Targagent
526 //(1 1 0 0 0 0 1 1 1 1 0 0)
527 relvars[0] = deltai*3;
528 relvars[1] = deltai*3+1;
529 relvars[2] = deltai*3+2;
530 relvars[3] = deltai*3+3;
531 relvars[4] = deltai*3+4;
532 relvars[5] = deltai*3+5;
533 relvars[6] = i*3;
534 relvars[7] = i*3+1;
535 relvars[8] = i*3+2;
536 relvars[9] = i*3+3;
537 relvars[10] = i*3+4;
538 relvars[11] = i*3+5;
539 relvarset = sylvan_set_fromarray(relvars, 12);
540 rel_enc[0] = 1;
541 rel_enc[1] = 1;
542 rel_enc[2] = 0;
543 rel_enc[3] = 0;
544 rel_enc[4] = 0;
545 rel_enc[5] = 0;
546 rel_enc[6] = 1;
547 rel_enc[7] = 1;
548 rel_enc[8] = 1;
549 rel_enc[9] = 1;
550 rel_enc[10] = 0;
551 rel_enc[11] = 0;
552 trs_current = (trans_t *)malloc(sizeof(trans_t));
553 trs_current->bdd = sylvan_cube(relvarset, rel_enc);
554 trs_current->varset.varset = relvarset;
555 trs_current->varset.size = 12;
556 trs_current->next_rel = trs;
557 trs = trs_current;
558
559 }
560 else if (check_space(x, y, dir, 1, bm) == 1 && check_space(x, y, dir, 2, bm) == 1){
561
562 xy_bddvar_map *bddvar = getxy(x + xdelta, y + ydelta, bm->f);
563 int deltai = bddvar->value.var[0];
564 bddvar = getxy(x + xgamma, y + ygamma, bm->f);
565 int gammai = bddvar->value.var[0];
566
567 //(0 1 0 0 1 1 1 0 0 0 1 1)
568 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};
569 BDDSET relvarset = sylvan_set_fromarray(relvars, 12);
570 uint8_t rel_enc[12] = {0, 1, 0, 0, 1, 1, 1, 0, 0, 0, 1, 1};
571 trs_current = (trans_t *)malloc(sizeof(trans_t));
572 trs_current->bdd = sylvan_cube(relvarset, rel_enc);
573 trs_current->varset.varset = relvarset;
574 trs_current->varset.size = 12;
575 trs_current->next_rel = trs;
576 trs = trs_current;
577
578 //(0 1 1 0 1 1 1 0 0 1 1 1)
579 relvars[0] = deltai*3;
580 relvars[1] = deltai*3+1;
581 relvars[2] = deltai*3+2;
582 relvars[3] = deltai*3+3;
583 relvars[4] = deltai*3+4;
584 relvars[5] = deltai*3+5;
585 relvars[6] = i*3;
586 relvars[7] = i*3+1;
587 relvars[8] = i*3+2;
588 relvars[9] = i*3+3;
589 relvars[10] = i*3+4;
590 relvars[11] = i*3+5;
591 relvarset = sylvan_set_fromarray(relvars, 12);
592 rel_enc[0] = 0;
593 rel_enc[1] = 1;
594 rel_enc[2] = 1;
595 rel_enc[3] = 0;
596 rel_enc[4] = 1;
597 rel_enc[5] = 1;
598 rel_enc[6] = 1;
599 rel_enc[7] = 0;
600 rel_enc[8] = 0;
601 rel_enc[9] = 1;
602 rel_enc[10] = 1;
603 rel_enc[11] = 1;
604 trs_current = (trans_t *)malloc(sizeof(trans_t));
605 trs_current->bdd = sylvan_cube(relvarset, rel_enc);
606 trs_current->varset.varset = relvarset;
607 trs_current->varset.size = 12;
608 trs_current->next_rel = trs;
609 trs = trs_current;
610
611 //(0 1 0 1 1 0 1 0 1 0 0 1)
612 relvars[0] = deltai*3;
613 relvars[1] = deltai*3+1;
614 relvars[2] = deltai*3+2;
615 relvars[3] = deltai*3+3;
616 relvars[4] = deltai*3+4;
617 relvars[5] = deltai*3+5;
618 relvars[6] = i*3;
619 relvars[7] = i*3+1;
620 relvars[8] = i*3+2;
621 relvars[9] = i*3+3;
622 relvars[10] = i*3+4;
623 relvars[11] = i*3+5;
624 relvarset = sylvan_set_fromarray(relvars, 12);
625 rel_enc[0] = 0;
626 rel_enc[1] = 1;
627 rel_enc[2] = 0;
628 rel_enc[3] = 1;
629 rel_enc[4] = 1;
630 rel_enc[5] = 0;
631 rel_enc[6] = 1;
632 rel_enc[7] = 0;
633 rel_enc[8] = 1;
634 rel_enc[9] = 0;
635 rel_enc[10] = 0;
636 rel_enc[11] = 1;
637 trs_current = (trans_t *)malloc(sizeof(trans_t));
638 trs_current->bdd = sylvan_cube(relvarset, rel_enc);
639 trs_current->varset.varset = relvarset;
640 trs_current->varset.size = 12;
641 trs_current->next_rel = trs;
642 trs = trs_current;
643
644 //(0 1 1 1 1 0 1 0 1 1 0 1)
645 relvars[0] = deltai*3;
646 relvars[1] = deltai*3+1;
647 relvars[2] = deltai*3+2;
648 relvars[3] = deltai*3+3;
649 relvars[4] = deltai*3+4;
650 relvars[5] = deltai*3+5;
651 relvars[6] = i*3;
652 relvars[7] = i*3+1;
653 relvars[8] = i*3+2;
654 relvars[9] = i*3+3;
655 relvars[10] = i*3+4;
656 relvars[11] = i*3+5;
657 relvarset = sylvan_set_fromarray(relvars, 12);
658 rel_enc[0] = 0;
659 rel_enc[1] = 1;
660 rel_enc[2] = 1;
661 rel_enc[3] = 1;
662 rel_enc[4] = 1;
663 rel_enc[5] = 0;
664 rel_enc[6] = 1;
665 rel_enc[7] = 0;
666 rel_enc[8] = 1;
667 rel_enc[9] = 1;
668 rel_enc[10] = 0;
669 rel_enc[11] = 1;
670 trs_current = (trans_t *)malloc(sizeof(trans_t));
671 trs_current->bdd = sylvan_cube(relvarset, rel_enc);
672 trs_current->varset.varset = relvarset;
673 trs_current->varset.size = 12;
674 trs_current->next_rel = trs;
675 trs = trs_current;
676
677 //(0 0 1 1 0 0 0 0 1 1 0 0 1 1 0 0 1 1)
678 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};
679 relvars1[0] = gammai*3;
680 relvars1[1] = gammai*3+1;
681 relvars1[2] = gammai*3+2;
682 relvars1[3] = gammai*3+3;
683 relvars1[4] = gammai*3+4;
684 relvars1[5] = gammai*3+5;
685 relvars1[6] = deltai*3;
686 relvars1[7] = deltai*3+1;
687 relvars1[8] = deltai*3+2;
688 relvars1[9] = deltai*3+3;
689 relvars1[10] = deltai*3+4;
690 relvars1[11] = deltai*3+5;
691 relvars1[12] = i*3;
692 relvars1[13] = i*3+1;
693 relvars1[14] = i*3+2;
694 relvars1[15] = i*3+3;
695 relvars1[16] = i*3+4;
696 relvars1[17] = i*3+5;
697 BDD relvarset1 = sylvan_set_fromarray(relvars1, 18);
698 uint8_t rel_enc1[18];
699 rel_enc1[0] = 0;
700 rel_enc1[1] = 0;
701 rel_enc1[2] = 1;
702 rel_enc1[3] = 1;
703 rel_enc1[4] = 0;
704 rel_enc1[5] = 0;
705 rel_enc1[6] = 0;
706 rel_enc1[7] = 0;
707 rel_enc1[8] = 1;
708 rel_enc1[9] = 1;
709 rel_enc1[10] = 0;
710 rel_enc1[11] = 0;
711 rel_enc1[12] = 1;
712 rel_enc1[13] = 1;
713 rel_enc1[14] = 0;
714 rel_enc1[15] = 0;
715 rel_enc1[16] = 1;
716 rel_enc1[17] = 1;
717 trs_current = (trans_t *)malloc(sizeof(trans_t));
718 trs_current->bdd = sylvan_cube(relvarset1, rel_enc1);
719 trs_current->varset.varset = relvarset1;
720 trs_current->varset.size = 18;
721 trs_current->next_rel = trs;
722 trs = trs_current;
723
724 //(1 1 0 0 0 0 0 0 1 1 0 0 1 1 0 0 1 1)
725 relvars1[0] = gammai*3;
726 relvars1[1] = gammai*3+1;
727 relvars1[2] = gammai*3+2;
728 relvars1[3] = gammai*3+3;
729 relvars1[4] = gammai*3+4;
730 relvars1[5] = gammai*3+5;
731 relvars1[6] = deltai*3;
732 relvars1[7] = deltai*3+1;
733 relvars1[8] = deltai*3+2;
734 relvars1[9] = deltai*3+3;
735 relvars1[10] = deltai*3+4;
736 relvars1[11] = deltai*3+5;
737 relvars1[12] = i*3;
738 relvars1[13] = i*3+1;
739 relvars1[14] = i*3+2;
740 relvars1[15] = i*3+3;
741 relvars1[16] = i*3+4;
742 relvars1[17] = i*3+5;
743 relvarset1 = sylvan_set_fromarray(relvars1, 18);
744 rel_enc1[0] = 1;
745 rel_enc1[1] = 1;
746 rel_enc1[2] = 0;
747 rel_enc1[3] = 0;
748 rel_enc1[4] = 0;
749 rel_enc1[5] = 0;
750 rel_enc1[6] = 0;
751 rel_enc1[7] = 0;
752 rel_enc1[8] = 1;
753 rel_enc1[9] = 1;
754 rel_enc1[10] = 0;
755 rel_enc1[11] = 0;
756 rel_enc1[12] = 1;
757 rel_enc1[13] = 1;
758 rel_enc1[14] = 0;
759 rel_enc1[15] = 0;
760 rel_enc1[16] = 1;
761 rel_enc1[17] = 1;
762 trs_current = (trans_t *)malloc(sizeof(trans_t));
763 trs_current->bdd = sylvan_cube(relvarset1, rel_enc1);
764 trs_current->varset.varset = relvarset1;
765 trs_current->varset.size = 18;
766 trs_current->next_rel = trs;
767 trs = trs_current;
768
769 //(0 0 1 1 0 0 0 0 1 1 0 0 1 1 1 1 0 0)
770 relvars1[0] = gammai*3;
771 relvars1[1] = gammai*3+1;
772 relvars1[2] = gammai*3+2;
773 relvars1[3] = gammai*3+3;
774 relvars1[4] = gammai*3+4;
775 relvars1[5] = gammai*3+5;
776 relvars1[6] = deltai*3;
777 relvars1[7] = deltai*3+1;
778 relvars1[8] = deltai*3+2;
779 relvars1[9] = deltai*3+3;
780 relvars1[10] = deltai*3+4;
781 relvars1[11] = deltai*3+5;
782 relvars1[12] = i*3;
783 relvars1[13] = i*3+1;
784 relvars1[14] = i*3+2;
785 relvars1[15] = i*3+3;
786 relvars1[16] = i*3+4;
787 relvars1[17] = i*3+5;
788 relvarset1 = sylvan_set_fromarray(relvars1, 18);
789 //(0 0 1 1 0 0 0 0 1 1 0 0 1 1 1 1 0 0)
790 rel_enc1[0] = 0;
791 rel_enc1[1] = 0;
792 rel_enc1[2] = 1;
793 rel_enc1[3] = 1;
794 rel_enc1[4] = 0;
795 rel_enc1[5] = 0;
796 rel_enc1[6] = 0;
797 rel_enc1[7] = 0;
798 rel_enc1[8] = 1;
799 rel_enc1[9] = 1;
800 rel_enc1[10] = 0;
801 rel_enc1[11] = 0;
802 rel_enc1[12] = 1;
803 rel_enc1[13] = 1;
804 rel_enc1[14] = 1;
805 rel_enc1[15] = 1;
806 rel_enc1[16] = 0;
807 rel_enc1[17] = 0;
808 trs_current = (trans_t *)malloc(sizeof(trans_t));
809 trs_current->bdd = sylvan_cube(relvarset1, rel_enc1);
810 trs_current->varset.varset = relvarset1;
811 trs_current->varset.size = 18;
812 trs_current->next_rel = trs;
813 trs = trs_current;
814
815 //(1 1 0 0 0 0 0 0 1 1 0 0 1 1 1 1 0 0)
816 relvars1[0] = gammai*3;
817 relvars1[1] = gammai*3+1;
818 relvars1[2] = gammai*3+2;
819 relvars1[3] = gammai*3+3;
820 relvars1[4] = gammai*3+4;
821 relvars1[5] = gammai*3+5;
822 relvars1[6] = deltai*3;
823 relvars1[7] = deltai*3+1;
824 relvars1[8] = deltai*3+2;
825 relvars1[9] = deltai*3+3;
826 relvars1[10] = deltai*3+4;
827 relvars1[11] = deltai*3+5;
828 relvars1[12] = i*3;
829 relvars1[13] = i*3+1;
830 relvars1[14] = i*3+2;
831 relvars1[15] = i*3+3;
832 relvars1[16] = i*3+4;
833 relvars1[17] = i*3+5;
834 relvarset1 = sylvan_set_fromarray(relvars1, 18);
835 //(1 1 0 0 0 0 0 0 1 1 0 0 1 1 1 1 0 0)
836 rel_enc1[0] = 1;
837 rel_enc1[1] = 1;
838 rel_enc1[2] = 0;
839 rel_enc1[3] = 0;
840 rel_enc1[4] = 0;
841 rel_enc1[5] = 0;
842 rel_enc1[6] = 0;
843 rel_enc1[7] = 0;
844 rel_enc1[8] = 1;
845 rel_enc1[9] = 1;
846 rel_enc1[10] = 0;
847 rel_enc1[11] = 0;
848 rel_enc1[12] = 1;
849 rel_enc1[13] = 1;
850 rel_enc1[14] = 1;
851 rel_enc1[15] = 1;
852 rel_enc1[16] = 0;
853 rel_enc1[17] = 0;
854 trs_current = (trans_t *)malloc(sizeof(trans_t));
855 trs_current->bdd = sylvan_cube(relvarset1, rel_enc1);
856 trs_current->varset.varset = relvarset1;
857 trs_current->varset.size = 18;
858 trs_current->next_rel = trs;
859 trs = trs_current;
860
861 //free box agent -> box agent free
862 //(0 0 0 1 1 0 0 1 1 0 0 1 1 0 0 0 1 1)
863 relvars1[0] = gammai*3;
864 relvars1[1] = gammai*3+1;
865 relvars1[2] = gammai*3+2;
866 relvars1[3] = gammai*3+3;
867 relvars1[4] = gammai*3+4;
868 relvars1[5] = gammai*3+5;
869 relvars1[6] = deltai*3;
870 relvars1[7] = deltai*3+1;
871 relvars1[8] = deltai*3+2;
872 relvars1[9] = deltai*3+3;
873 relvars1[10] = deltai*3+4;
874 relvars1[11] = deltai*3+5;
875 relvars1[12] = i*3;
876 relvars1[13] = i*3+1;
877 relvars1[14] = i*3+2;
878 relvars1[15] = i*3+3;
879 relvars1[16] = i*3+4;
880 relvars1[17] = i*3+5;
881 relvarset1 = sylvan_set_fromarray(relvars1, 18);
882 //(0 0 0 1 1 0 0 1 1 0 0 1 1 0 0 0 1 1)
883 rel_enc1[0] = 0;
884 rel_enc1[1] = 0;
885 rel_enc1[2] = 0;
886 rel_enc1[3] = 1;
887 rel_enc1[4] = 1;
888 rel_enc1[5] = 0;
889 rel_enc1[6] = 0;
890 rel_enc1[7] = 1;
891 rel_enc1[8] = 1;
892 rel_enc1[9] = 0;
893 rel_enc1[10] = 0;
894 rel_enc1[11] = 1;
895 rel_enc1[12] = 1;
896 rel_enc1[13] = 0;
897 rel_enc1[14] = 0;
898 rel_enc1[15] = 0;
899 rel_enc1[16] = 1;
900 rel_enc1[17] = 1;
901 trs_current = (trans_t *)malloc(sizeof(trans_t));
902 trs_current->bdd = sylvan_cube(relvarset1, rel_enc1);
903 trs_current->varset.varset = relvarset1;
904 trs_current->varset.size = 18;
905 trs_current->next_rel = trs;
906 trs = trs_current;
907
908 //(free targbox agent -> box targagent free)
909 //(0 0 0 1 1 0 1 1 0 1 0 0 1 0 0 0 1 1)
910 relvars1[0] = gammai*3;
911 relvars1[1] = gammai*3+1;
912 relvars1[2] = gammai*3+2;
913 relvars1[3] = gammai*3+3;
914 relvars1[4] = gammai*3+4;
915 relvars1[5] = gammai*3+5;
916 relvars1[6] = deltai*3;
917 relvars1[7] = deltai*3+1;
918 relvars1[8] = deltai*3+2;
919 relvars1[9] = deltai*3+3;
920 relvars1[10] = deltai*3+4;
921 relvars1[11] = deltai*3+5;
922 relvars1[12] = i*3;
923 relvars1[13] = i*3+1;
924 relvars1[14] = i*3+2;
925 relvars1[15] = i*3+3;
926 relvars1[16] = i*3+4;
927 relvars1[17] = i*3+5;
928 relvarset1 = sylvan_set_fromarray(relvars1, 18);
929 //(0 0 0 1 1 0 1 1 0 1 0 0 1 0 0 0 1 1)
930 rel_enc1[0] = 0;
931 rel_enc1[1] = 0;
932 rel_enc1[2] = 0;
933 rel_enc1[3] = 1;
934 rel_enc1[4] = 1;
935 rel_enc1[5] = 0;
936 rel_enc1[6] = 1;
937 rel_enc1[7] = 1;
938 rel_enc1[8] = 0;
939 rel_enc1[9] = 1;
940 rel_enc1[10] = 0;
941 rel_enc1[11] = 0;
942 rel_enc1[12] = 1;
943 rel_enc1[13] = 0;
944 rel_enc1[14] = 0;
945 rel_enc1[15] = 0;
946 rel_enc1[16] = 1;
947 rel_enc1[17] = 1;
948 trs_current = (trans_t *)malloc(sizeof(trans_t));
949 trs_current->bdd = sylvan_cube(relvarset1, rel_enc1);
950 trs_current->varset.varset = relvarset1;
951 trs_current->varset.size = 18;
952 trs_current->next_rel = trs;
953 trs = trs_current;
954
955 //(target box agent -> targbox agent free)
956 //(0 1 1 0 1 0 0 1 1 0 0 1 1 0 0 0 1 1)
957 relvars1[0] = gammai*3;
958 relvars1[1] = gammai*3+1;
959 relvars1[2] = gammai*3+2;
960 relvars1[3] = gammai*3+3;
961 relvars1[4] = gammai*3+4;
962 relvars1[5] = gammai*3+5;
963 relvars1[6] = deltai*3;
964 relvars1[7] = deltai*3+1;
965 relvars1[8] = deltai*3+2;
966 relvars1[9] = deltai*3+3;
967 relvars1[10] = deltai*3+4;
968 relvars1[11] = deltai*3+5;
969 relvars1[12] = i*3;
970 relvars1[13] = i*3+1;
971 relvars1[14] = i*3+2;
972 relvars1[15] = i*3+3;
973 relvars1[16] = i*3+4;
974 relvars1[17] = i*3+5;
975 relvarset1 = sylvan_set_fromarray(relvars1, 18);
976 //(0 1 1 0 1 0 0 1 1 0 0 1 1 0 0 0 1 1)
977 rel_enc1[0] = 0;
978 rel_enc1[1] = 1;
979 rel_enc1[2] = 1;
980 rel_enc1[3] = 0;
981 rel_enc1[4] = 1;
982 rel_enc1[5] = 0;
983 rel_enc1[6] = 0;
984 rel_enc1[7] = 1;
985 rel_enc1[8] = 1;
986 rel_enc1[9] = 0;
987 rel_enc1[10] = 0;
988 rel_enc1[11] = 1;
989 rel_enc1[12] = 1;
990 rel_enc1[13] = 0;
991 rel_enc1[14] = 0;
992 rel_enc1[15] = 0;
993 rel_enc1[16] = 1;
994 rel_enc1[17] = 1;
995 trs_current = (trans_t *)malloc(sizeof(trans_t));
996 trs_current->bdd = sylvan_cube(relvarset1, rel_enc1);
997 trs_current->varset.varset = relvarset1;
998 trs_current->varset.size = 18;
999 trs_current->next_rel = trs;
1000 trs = trs_current;
1001
1002 //(target targbox agent -> targbox targagent free)
1003 //(0 1 1 0 1 0 1 1 0 1 0 0 1 0 0 0 1 1)
1004 relvars1[0] = gammai*3;
1005 relvars1[1] = gammai*3+1;
1006 relvars1[2] = gammai*3+2;
1007 relvars1[3] = gammai*3+3;
1008 relvars1[4] = gammai*3+4;
1009 relvars1[5] = gammai*3+5;
1010 relvars1[6] = deltai*3;
1011 relvars1[7] = deltai*3+1;
1012 relvars1[8] = deltai*3+2;
1013 relvars1[9] = deltai*3+3;
1014 relvars1[10] = deltai*3+4;
1015 relvars1[11] = deltai*3+5;
1016 relvars1[12] = i*3;
1017 relvars1[13] = i*3+1;
1018 relvars1[14] = i*3+2;
1019 relvars1[15] = i*3+3;
1020 relvars1[16] = i*3+4;
1021 relvars1[17] = i*3+5;
1022 relvarset1 = sylvan_set_fromarray(relvars1, 18);
1023 //(0 1 1 0 1 0 1 1 0 1 0 0 1 0 0 0 1 1)
1024 rel_enc1[0] = 0;
1025 rel_enc1[1] = 1;
1026 rel_enc1[2] = 1;
1027 rel_enc1[3] = 0;
1028 rel_enc1[4] = 1;
1029 rel_enc1[5] = 0;
1030 rel_enc1[6] = 1;
1031 rel_enc1[7] = 1;
1032 rel_enc1[8] = 0;
1033 rel_enc1[9] = 1;
1034 rel_enc1[10] = 0;
1035 rel_enc1[11] = 0;
1036 rel_enc1[12] = 1;
1037 rel_enc1[13] = 0;
1038 rel_enc1[14] = 0;
1039 rel_enc1[15] = 0;
1040 rel_enc1[16] = 1;
1041 rel_enc1[17] = 1;
1042 trs_current = (trans_t *)malloc(sizeof(trans_t));
1043 trs_current->bdd = sylvan_cube(relvarset1, rel_enc1);
1044 trs_current->varset.varset = relvarset1;
1045 trs_current->varset.size = 18;
1046 trs_current->next_rel = trs;
1047 trs = trs_current;
1048
1049 //(free box targagent -> box agent target)
1050 //(0 0 0 1 1 0 0 1 1 0 0 1 1 0 1 1 0 1)
1051 relvars1[0] = gammai*3;
1052 relvars1[1] = gammai*3+1;
1053 relvars1[2] = gammai*3+2;
1054 relvars1[3] = gammai*3+3;
1055 relvars1[4] = gammai*3+4;
1056 relvars1[5] = gammai*3+5;
1057 relvars1[6] = deltai*3;
1058 relvars1[7] = deltai*3+1;
1059 relvars1[8] = deltai*3+2;
1060 relvars1[9] = deltai*3+3;
1061 relvars1[10] = deltai*3+4;
1062 relvars1[11] = deltai*3+5;
1063 relvars1[12] = i*3;
1064 relvars1[13] = i*3+1;
1065 relvars1[14] = i*3+2;
1066 relvars1[15] = i*3+3;
1067 relvars1[16] = i*3+4;
1068 relvars1[17] = i*3+5;
1069 relvarset1 = sylvan_set_fromarray(relvars1, 18);
1070 //(0 0 0 1 1 0 0 1 1 0 0 1 1 0 1 1 0 1)
1071 rel_enc1[0] = 0;
1072 rel_enc1[1] = 0;
1073 rel_enc1[2] = 0;
1074 rel_enc1[3] = 1;
1075 rel_enc1[4] = 1;
1076 rel_enc1[5] = 0;
1077 rel_enc1[6] = 0;
1078 rel_enc1[7] = 1;
1079 rel_enc1[8] = 1;
1080 rel_enc1[9] = 0;
1081 rel_enc1[10] = 0;
1082 rel_enc1[11] = 1;
1083 rel_enc1[12] = 1;
1084 rel_enc1[13] = 0;
1085 rel_enc1[14] = 1;
1086 rel_enc1[15] = 1;
1087 rel_enc1[16] = 0;
1088 rel_enc1[17] = 1;
1089 trs_current = (trans_t *)malloc(sizeof(trans_t));
1090 trs_current->bdd = sylvan_cube(relvarset1, rel_enc1);
1091 trs_current->varset.varset = relvarset1;
1092 trs_current->varset.size = 18;
1093 trs_current->next_rel = trs;
1094 trs = trs_current;
1095
1096 //(free targbox targagent -> box targagent target)
1097 //(0 0 0 1 1 0 1 1 0 1 0 0 1 0 1 1 0 1)
1098 relvars1[0] = gammai*3;
1099 relvars1[1] = gammai*3+1;
1100 relvars1[2] = gammai*3+2;
1101 relvars1[3] = gammai*3+3;
1102 relvars1[4] = gammai*3+4;
1103 relvars1[5] = gammai*3+5;
1104 relvars1[6] = deltai*3;
1105 relvars1[7] = deltai*3+1;
1106 relvars1[8] = deltai*3+2;
1107 relvars1[9] = deltai*3+3;
1108 relvars1[10] = deltai*3+4;
1109 relvars1[11] = deltai*3+5;
1110 relvars1[12] = i*3;
1111 relvars1[13] = i*3+1;
1112 relvars1[14] = i*3+2;
1113 relvars1[15] = i*3+3;
1114 relvars1[16] = i*3+4;
1115 relvars1[17] = i*3+5;
1116 relvarset1 = sylvan_set_fromarray(relvars1, 18);
1117 //(0 0 0 1 1 0 1 1 0 1 0 0 1 0 1 1 0 1)
1118 rel_enc1[0] = 0;
1119 rel_enc1[1] = 0;
1120 rel_enc1[2] = 0;
1121 rel_enc1[3] = 1;
1122 rel_enc1[4] = 1;
1123 rel_enc1[5] = 0;
1124 rel_enc1[6] = 1;
1125 rel_enc1[7] = 1;
1126 rel_enc1[8] = 0;
1127 rel_enc1[9] = 1;
1128 rel_enc1[10] = 0;
1129 rel_enc1[11] = 0;
1130 rel_enc1[12] = 1;
1131 rel_enc1[13] = 0;
1132 rel_enc1[14] = 1;
1133 rel_enc1[15] = 1;
1134 rel_enc1[16] = 0;
1135 rel_enc1[17] = 1;
1136 trs_current = (trans_t *)malloc(sizeof(trans_t));
1137 trs_current->bdd = sylvan_cube(relvarset1, rel_enc1);
1138 trs_current->varset.varset = relvarset1;
1139 trs_current->varset.size = 18;
1140 trs_current->next_rel = trs;
1141 trs = trs_current;
1142
1143 //(target box targagent -> targbox agent target)
1144 //(0 1 1 0 1 0 0 1 1 0 0 1 1 0 1 1 0 1)
1145 relvars1[0] = gammai*3;
1146 relvars1[1] = gammai*3+1;
1147 relvars1[2] = gammai*3+2;
1148 relvars1[3] = gammai*3+3;
1149 relvars1[4] = gammai*3+4;
1150 relvars1[5] = gammai*3+5;
1151 relvars1[6] = deltai*3;
1152 relvars1[7] = deltai*3+1;
1153 relvars1[8] = deltai*3+2;
1154 relvars1[9] = deltai*3+3;
1155 relvars1[10] = deltai*3+4;
1156 relvars1[11] = deltai*3+5;
1157 relvars1[12] = i*3;
1158 relvars1[13] = i*3+1;
1159 relvars1[14] = i*3+2;
1160 relvars1[15] = i*3+3;
1161 relvars1[16] = i*3+4;
1162 relvars1[17] = i*3+5;
1163 relvarset1 = sylvan_set_fromarray(relvars1, 18);
1164 //(0 1 1 0 1 0 0 1 1 0 0 1 1 0 1 1 0 1)
1165 rel_enc1[0] = 0;
1166 rel_enc1[1] = 1;
1167 rel_enc1[2] = 1;
1168 rel_enc1[3] = 0;
1169 rel_enc1[4] = 1;
1170 rel_enc1[5] = 0;
1171 rel_enc1[6] = 0;
1172 rel_enc1[7] = 1;
1173 rel_enc1[8] = 1;
1174 rel_enc1[9] = 0;
1175 rel_enc1[10] = 0;
1176 rel_enc1[11] = 1;
1177 rel_enc1[12] = 1;
1178 rel_enc1[13] = 0;
1179 rel_enc1[14] = 1;
1180 rel_enc1[15] = 1;
1181 rel_enc1[16] = 0;
1182 rel_enc1[17] = 1;
1183 trs_current = (trans_t *)malloc(sizeof(trans_t));
1184 trs_current->bdd = sylvan_cube(relvarset1, rel_enc1);
1185 trs_current->varset.varset = relvarset1;
1186 trs_current->varset.size = 18;
1187 trs_current->next_rel = trs;
1188 trs = trs_current;
1189
1190 //(target targbox targagent -> targbox targagent target)
1191 //(0 1 1 0 1 0 1 1 0 1 0 0 1 0 1 1 0 1)
1192 relvars1[0] = gammai*3;
1193 relvars1[1] = gammai*3+1;
1194 relvars1[2] = gammai*3+2;
1195 relvars1[3] = gammai*3+3;
1196 relvars1[4] = gammai*3+4;
1197 relvars1[5] = gammai*3+5;
1198 relvars1[6] = deltai*3;
1199 relvars1[7] = deltai*3+1;
1200 relvars1[8] = deltai*3+2;
1201 relvars1[9] = deltai*3+3;
1202 relvars1[10] = deltai*3+4;
1203 relvars1[11] = deltai*3+5;
1204 relvars1[12] = i*3;
1205 relvars1[13] = i*3+1;
1206 relvars1[14] = i*3+2;
1207 relvars1[15] = i*3+3;
1208 relvars1[16] = i*3+4;
1209 relvars1[17] = i*3+5;
1210 relvarset1 = sylvan_set_fromarray(relvars1, 18);
1211 //(0 1 1 0 1 0 1 1 0 1 0 0 1 0 1 1 0 1)
1212 rel_enc1[0] = 0;
1213 rel_enc1[1] = 1;
1214 rel_enc1[2] = 1;
1215 rel_enc1[3] = 0;
1216 rel_enc1[4] = 1;
1217 rel_enc1[5] = 0;
1218 rel_enc1[6] = 1;
1219 rel_enc1[7] = 1;
1220 rel_enc1[8] = 0;
1221 rel_enc1[9] = 1;
1222 rel_enc1[10] = 0;
1223 rel_enc1[11] = 0;
1224 rel_enc1[12] = 1;
1225 rel_enc1[13] = 0;
1226 rel_enc1[14] = 1;
1227 rel_enc1[15] = 1;
1228 rel_enc1[16] = 0;
1229 rel_enc1[17] = 1;
1230 trs_current = (trans_t *)malloc(sizeof(trans_t));
1231 trs_current->bdd = sylvan_cube(relvarset1, rel_enc1);
1232 trs_current->varset.varset = relvarset1;
1233 trs_current->varset.size = 18;
1234 trs_current->next_rel = trs;
1235 trs = trs_current;
1236 }
1237 }
1238 trs_current = trs;
1239 return trs;
1240 }
1241
1242 rels *encode_rel(sokoban_screen *screen)
1243 {
1244 LACE_ME;
1245
1246 trans_t *tl = sylvan_false;
1247
1248 //left relation
1249 tl = create_single_rel(screen, LEFT);
1250
1251 //up relation
1252 trans_t *tu = create_single_rel(screen, UP);
1253
1254 //right relation
1255 trans_t *tr = create_single_rel(screen, RIGHT);
1256
1257 //down relation
1258 trans_t *td = create_single_rel(screen, DOWN);
1259
1260 rels *rls = NULL;
1261 rls = (rels *)malloc(sizeof(rels));
1262 rls->rell = tl;
1263 rls->relu = tu;
1264 rls->relr = tr;
1265 rls->reld = td;
1266
1267 return rls;
1268 }
1269
1270 int
1271 test_relprod()
1272 {
1273 LACE_ME;
1274
1275 BDDVAR vars[] = {0,2,4};
1276 BDDVAR all_vars[] = {0,1,2,3,4,5};
1277 BDDVAR all_vars2[] = {0,1};
1278 //BDDVAR short_vars[] = {0,1};
1279 /*BDDVAR short_vars2[] = {2,3};
1280 BDDVAR short_vars3[] = {0,1,2,3};*/
1281
1282 BDDSET vars_set = sylvan_set_fromarray(vars, 3);
1283 BDDSET all_vars_set = sylvan_set_fromarray(all_vars, 6);
1284 BDDSET all_vars_set2 = sylvan_set_fromarray(all_vars2, 2);
1285 //BDDSET short_vars_set = sylvan_set_fromarray(short_vars, 2);
1286 /*BDDSET short_vars_set2 = sylvan_set_fromarray(short_vars2, 2);
1287 BDDSET short_vars_set3 = sylvan_set_fromarray(short_vars3, 4);*/
1288
1289 BDD s, t, next, prev;
1290 BDD zeroes, ones;
1291
1292 // transition relation: 000 --> 111 and !000 --> 000
1293 t = sylvan_false;
1294 t = sylvan_union_cube(t, all_vars_set2, ((uint8_t[]){0,1}));
1295 //t = sylvan_union_cube(t, all_vars_set, ((uint8_t[]){1,0,2,0,2,0}));
1296 t = sylvan_union_cube(t, all_vars_set2, ((uint8_t[]){1,0}));
1297 // t = sylvan_union_cube(t, all_vars_set, ((uint8_t[]){0,1}));
1298
1299 s = sylvan_cube(vars_set, (uint8_t[]){0,0,0});
1300 zeroes = sylvan_cube(vars_set, (uint8_t[]){1,0,0});
1301 ones = sylvan_cube(vars_set, (uint8_t[]){0,0,0});
1302
1303 next = sylvan_relnext(s, t, all_vars_set);
1304 prev = sylvan_relprev(t, next, all_vars_set);
1305 if (next == zeroes) printf("Pass 1\n");
1306 if (prev == ones) printf("Pass 2\n");
1307 //trans *ts;
1308 //ts = NULL;
1309
1310 return 0;
1311 }
Unnamed repository; edit this file 'description' to name the repository.