repositories / mc1516pa.git / blob
? search:
summary | shortlog | log | commit | commitdiff | tree
history | raw | HEAD
some more trans var corrections
[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 //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 //Free Agent -> 1 0 1 0 0 1 Agent Free
568 //(0 1 0 0 1 1 1 0 0 0 1 1)
569 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};
570 BDDSET relvarset = sylvan_set_fromarray(relvars, 12);
571 uint8_t rel_enc[12] = {0, 1, 0, 0, 1, 1, 1, 0, 0, 0, 1, 1};
572 trs_current = (trans_t *)malloc(sizeof(trans_t));
573 trs_current->bdd = sylvan_cube(relvarset, rel_enc);
574 trs_current->varset.varset = relvarset;
575 trs_current->varset.size = 12;
576 trs_current->next_rel = trs;
577 trs = trs_current;
578
579 //Target Agent -> Targagent Free
580 //(0 1 1 1 1 0 1 0 0 0 1 1)
581 relvars[0] = deltai*3;
582 relvars[1] = deltai*3+1;
583 relvars[2] = deltai*3+2;
584 relvars[3] = deltai*3+3;
585 relvars[4] = deltai*3+4;
586 relvars[5] = deltai*3+5;
587 relvars[6] = i*3;
588 relvars[7] = i*3+1;
589 relvars[8] = i*3+2;
590 relvars[9] = i*3+3;
591 relvars[10] = i*3+4;
592 relvars[11] = i*3+5;
593 relvarset = sylvan_set_fromarray(relvars, 12);
594 rel_enc[0] = 0;
595 rel_enc[1] = 1;
596 rel_enc[2] = 1;
597 rel_enc[3] = 1;
598 rel_enc[4] = 1;
599 rel_enc[5] = 0;
600 rel_enc[6] = 1;
601 rel_enc[7] = 0;
602 rel_enc[8] = 0;
603 rel_enc[9] = 0;
604 rel_enc[10] = 1;
605 rel_enc[11] = 1;
606 trs_current = (trans_t *)malloc(sizeof(trans_t));
607 trs_current->bdd = sylvan_cube(relvarset, rel_enc);
608 trs_current->varset.varset = relvarset;
609 trs_current->varset.size = 12;
610 trs_current->next_rel = trs;
611 trs = trs_current;
612
613 //Free Targagent -> Agent Target
614 //(0 1 0 0 1 1 1 0 1 1 0 1)
615 relvars[0] = deltai*3;
616 relvars[1] = deltai*3+1;
617 relvars[2] = deltai*3+2;
618 relvars[3] = deltai*3+3;
619 relvars[4] = deltai*3+4;
620 relvars[5] = deltai*3+5;
621 relvars[6] = i*3;
622 relvars[7] = i*3+1;
623 relvars[8] = i*3+2;
624 relvars[9] = i*3+3;
625 relvars[10] = i*3+4;
626 relvars[11] = i*3+5;
627 relvarset = sylvan_set_fromarray(relvars, 12);
628 rel_enc[0] = 0;
629 rel_enc[1] = 1;
630 rel_enc[2] = 0;
631 rel_enc[3] = 0;
632 rel_enc[4] = 1;
633 rel_enc[5] = 1;
634 rel_enc[6] = 1;
635 rel_enc[7] = 0;
636 rel_enc[8] = 1;
637 rel_enc[9] = 1;
638 rel_enc[10] = 0;
639 rel_enc[11] = 1;
640 trs_current = (trans_t *)malloc(sizeof(trans_t));
641 trs_current->bdd = sylvan_cube(relvarset, rel_enc);
642 trs_current->varset.varset = relvarset;
643 trs_current->varset.size = 12;
644 trs_current->next_rel = trs;
645 trs = trs_current;
646
647 //Target Targagent -> Targagent Target
648 //(0 1 1 1 1 0 1 0 1 1 0 1)
649 relvars[0] = deltai*3;
650 relvars[1] = deltai*3+1;
651 relvars[2] = deltai*3+2;
652 relvars[3] = deltai*3+3;
653 relvars[4] = deltai*3+4;
654 relvars[5] = deltai*3+5;
655 relvars[6] = i*3;
656 relvars[7] = i*3+1;
657 relvars[8] = i*3+2;
658 relvars[9] = i*3+3;
659 relvars[10] = i*3+4;
660 relvars[11] = i*3+5;
661 relvarset = sylvan_set_fromarray(relvars, 12);
662 rel_enc[0] = 0;
663 rel_enc[1] = 1;
664 rel_enc[2] = 1;
665 rel_enc[3] = 1;
666 rel_enc[4] = 1;
667 rel_enc[5] = 0;
668 rel_enc[6] = 1;
669 rel_enc[7] = 0;
670 rel_enc[8] = 1;
671 rel_enc[9] = 1;
672 rel_enc[10] = 0;
673 rel_enc[11] = 1;
674 trs_current = (trans_t *)malloc(sizeof(trans_t));
675 trs_current->bdd = sylvan_cube(relvarset, rel_enc);
676 trs_current->varset.varset = relvarset;
677 trs_current->varset.size = 12;
678 trs_current->next_rel = trs;
679 trs = trs_current;
680
681 //Box Box Agent -> Box Box Agent
682 //(0 0 1 1 0 0 0 0 1 1 0 0 1 1 0 0 1 1)
683 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};
684 relvars1[0] = gammai*3;
685 relvars1[1] = gammai*3+1;
686 relvars1[2] = gammai*3+2;
687 relvars1[3] = gammai*3+3;
688 relvars1[4] = gammai*3+4;
689 relvars1[5] = gammai*3+5;
690 relvars1[6] = deltai*3;
691 relvars1[7] = deltai*3+1;
692 relvars1[8] = deltai*3+2;
693 relvars1[9] = deltai*3+3;
694 relvars1[10] = deltai*3+4;
695 relvars1[11] = deltai*3+5;
696 relvars1[12] = i*3;
697 relvars1[13] = i*3+1;
698 relvars1[14] = i*3+2;
699 relvars1[15] = i*3+3;
700 relvars1[16] = i*3+4;
701 relvars1[17] = i*3+5;
702 BDD relvarset1 = sylvan_set_fromarray(relvars1, 18);
703 uint8_t rel_enc1[18];
704 //(0 0 1 1 0 0 0 0 1 1 0 0 1 1 0 0 1 1)
705 rel_enc1[0] = 0;
706 rel_enc1[1] = 0;
707 rel_enc1[2] = 1;
708 rel_enc1[3] = 1;
709 rel_enc1[4] = 0;
710 rel_enc1[5] = 0;
711 rel_enc1[6] = 0;
712 rel_enc1[7] = 0;
713 rel_enc1[8] = 1;
714 rel_enc1[9] = 1;
715 rel_enc1[10] = 0;
716 rel_enc1[11] = 0;
717 rel_enc1[12] = 1;
718 rel_enc1[13] = 1;
719 rel_enc1[14] = 0;
720 rel_enc1[15] = 0;
721 rel_enc1[16] = 1;
722 rel_enc1[17] = 1;
723 trs_current = (trans_t *)malloc(sizeof(trans_t));
724 trs_current->bdd = sylvan_cube(relvarset1, rel_enc1);
725 trs_current->varset.varset = relvarset1;
726 trs_current->varset.size = 18;
727 trs_current->next_rel = trs;
728 trs = trs_current;
729
730 //Targbox Box Agent -> Targbox Box Agent
731 //(1 1 0 0 0 0 0 0 1 1 0 0 1 1 0 0 1 1)
732 relvars1[0] = gammai*3;
733 relvars1[1] = gammai*3+1;
734 relvars1[2] = gammai*3+2;
735 relvars1[3] = gammai*3+3;
736 relvars1[4] = gammai*3+4;
737 relvars1[5] = gammai*3+5;
738 relvars1[6] = deltai*3;
739 relvars1[7] = deltai*3+1;
740 relvars1[8] = deltai*3+2;
741 relvars1[9] = deltai*3+3;
742 relvars1[10] = deltai*3+4;
743 relvars1[11] = deltai*3+5;
744 relvars1[12] = i*3;
745 relvars1[13] = i*3+1;
746 relvars1[14] = i*3+2;
747 relvars1[15] = i*3+3;
748 relvars1[16] = i*3+4;
749 relvars1[17] = i*3+5;
750 relvarset1 = sylvan_set_fromarray(relvars1, 18);
751 //(1 1 0 0 0 0 0 0 1 1 0 0 1 1 0 0 1 1)
752 rel_enc1[0] = 1;
753 rel_enc1[1] = 1;
754 rel_enc1[2] = 0;
755 rel_enc1[3] = 0;
756 rel_enc1[4] = 0;
757 rel_enc1[5] = 0;
758 rel_enc1[6] = 0;
759 rel_enc1[7] = 0;
760 rel_enc1[8] = 1;
761 rel_enc1[9] = 1;
762 rel_enc1[10] = 0;
763 rel_enc1[11] = 0;
764 rel_enc1[12] = 1;
765 rel_enc1[13] = 1;
766 rel_enc1[14] = 0;
767 rel_enc1[15] = 0;
768 rel_enc1[16] = 1;
769 rel_enc1[17] = 1;
770 trs_current = (trans_t *)malloc(sizeof(trans_t));
771 trs_current->bdd = sylvan_cube(relvarset1, rel_enc1);
772 trs_current->varset.varset = relvarset1;
773 trs_current->varset.size = 18;
774 trs_current->next_rel = trs;
775 trs = trs_current;
776
777 //Box Box Targagent -> Box Box Targagent
778 //(0 0 1 1 0 0 0 0 1 1 0 0 1 1 1 1 0 0)
779 relvars1[0] = gammai*3;
780 relvars1[1] = gammai*3+1;
781 relvars1[2] = gammai*3+2;
782 relvars1[3] = gammai*3+3;
783 relvars1[4] = gammai*3+4;
784 relvars1[5] = gammai*3+5;
785 relvars1[6] = deltai*3;
786 relvars1[7] = deltai*3+1;
787 relvars1[8] = deltai*3+2;
788 relvars1[9] = deltai*3+3;
789 relvars1[10] = deltai*3+4;
790 relvars1[11] = deltai*3+5;
791 relvars1[12] = i*3;
792 relvars1[13] = i*3+1;
793 relvars1[14] = i*3+2;
794 relvars1[15] = i*3+3;
795 relvars1[16] = i*3+4;
796 relvars1[17] = i*3+5;
797 relvarset1 = sylvan_set_fromarray(relvars1, 18);
798 //(0 0 1 1 0 0 0 0 1 1 0 0 1 1 1 1 0 0)
799 rel_enc1[0] = 0;
800 rel_enc1[1] = 0;
801 rel_enc1[2] = 1;
802 rel_enc1[3] = 1;
803 rel_enc1[4] = 0;
804 rel_enc1[5] = 0;
805 rel_enc1[6] = 0;
806 rel_enc1[7] = 0;
807 rel_enc1[8] = 1;
808 rel_enc1[9] = 1;
809 rel_enc1[10] = 0;
810 rel_enc1[11] = 0;
811 rel_enc1[12] = 1;
812 rel_enc1[13] = 1;
813 rel_enc1[14] = 1;
814 rel_enc1[15] = 1;
815 rel_enc1[16] = 0;
816 rel_enc1[17] = 0;
817 trs_current = (trans_t *)malloc(sizeof(trans_t));
818 trs_current->bdd = sylvan_cube(relvarset1, rel_enc1);
819 trs_current->varset.varset = relvarset1;
820 trs_current->varset.size = 18;
821 trs_current->next_rel = trs;
822 trs = trs_current;
823
824 //Targbox Box Targagent -> Targbox Box Targagent
825 //(1 1 0 0 0 0 0 0 1 1 0 0 1 1 1 1 0 0)
826 relvars1[0] = gammai*3;
827 relvars1[1] = gammai*3+1;
828 relvars1[2] = gammai*3+2;
829 relvars1[3] = gammai*3+3;
830 relvars1[4] = gammai*3+4;
831 relvars1[5] = gammai*3+5;
832 relvars1[6] = deltai*3;
833 relvars1[7] = deltai*3+1;
834 relvars1[8] = deltai*3+2;
835 relvars1[9] = deltai*3+3;
836 relvars1[10] = deltai*3+4;
837 relvars1[11] = deltai*3+5;
838 relvars1[12] = i*3;
839 relvars1[13] = i*3+1;
840 relvars1[14] = i*3+2;
841 relvars1[15] = i*3+3;
842 relvars1[16] = i*3+4;
843 relvars1[17] = i*3+5;
844 relvarset1 = sylvan_set_fromarray(relvars1, 18);
845 //(1 1 0 0 0 0 0 0 1 1 0 0 1 1 1 1 0 0)
846 rel_enc1[0] = 1;
847 rel_enc1[1] = 1;
848 rel_enc1[2] = 0;
849 rel_enc1[3] = 0;
850 rel_enc1[4] = 0;
851 rel_enc1[5] = 0;
852 rel_enc1[6] = 0;
853 rel_enc1[7] = 0;
854 rel_enc1[8] = 1;
855 rel_enc1[9] = 1;
856 rel_enc1[10] = 0;
857 rel_enc1[11] = 0;
858 rel_enc1[12] = 1;
859 rel_enc1[13] = 1;
860 rel_enc1[14] = 1;
861 rel_enc1[15] = 1;
862 rel_enc1[16] = 0;
863 rel_enc1[17] = 0;
864 trs_current = (trans_t *)malloc(sizeof(trans_t));
865 trs_current->bdd = sylvan_cube(relvarset1, rel_enc1);
866 trs_current->varset.varset = relvarset1;
867 trs_current->varset.size = 18;
868 trs_current->next_rel = trs;
869 trs = trs_current;
870
871 //Free Box Agent -> Box Agent Free
872 //(0 0 0 1 1 0 0 1 1 0 0 1 1 0 0 0 1 1)
873 relvars1[0] = gammai*3;
874 relvars1[1] = gammai*3+1;
875 relvars1[2] = gammai*3+2;
876 relvars1[3] = gammai*3+3;
877 relvars1[4] = gammai*3+4;
878 relvars1[5] = gammai*3+5;
879 relvars1[6] = deltai*3;
880 relvars1[7] = deltai*3+1;
881 relvars1[8] = deltai*3+2;
882 relvars1[9] = deltai*3+3;
883 relvars1[10] = deltai*3+4;
884 relvars1[11] = deltai*3+5;
885 relvars1[12] = i*3;
886 relvars1[13] = i*3+1;
887 relvars1[14] = i*3+2;
888 relvars1[15] = i*3+3;
889 relvars1[16] = i*3+4;
890 relvars1[17] = i*3+5;
891 relvarset1 = sylvan_set_fromarray(relvars1, 18);
892 //(0 0 0 1 1 0 0 1 1 0 0 1 1 0 0 0 1 1)
893 rel_enc1[0] = 0;
894 rel_enc1[1] = 0;
895 rel_enc1[2] = 0;
896 rel_enc1[3] = 1;
897 rel_enc1[4] = 1;
898 rel_enc1[5] = 0;
899 rel_enc1[6] = 0;
900 rel_enc1[7] = 1;
901 rel_enc1[8] = 1;
902 rel_enc1[9] = 0;
903 rel_enc1[10] = 0;
904 rel_enc1[11] = 1;
905 rel_enc1[12] = 1;
906 rel_enc1[13] = 0;
907 rel_enc1[14] = 0;
908 rel_enc1[15] = 0;
909 rel_enc1[16] = 1;
910 rel_enc1[17] = 1;
911 trs_current = (trans_t *)malloc(sizeof(trans_t));
912 trs_current->bdd = sylvan_cube(relvarset1, rel_enc1);
913 trs_current->varset.varset = relvarset1;
914 trs_current->varset.size = 18;
915 trs_current->next_rel = trs;
916 trs = trs_current;
917
918 //Free Targbox Agent -> Box Targagent Free
919 //(0 0 0 1 1 0 1 1 0 1 0 0 1 0 0 0 1 1)
920 relvars1[0] = gammai*3;
921 relvars1[1] = gammai*3+1;
922 relvars1[2] = gammai*3+2;
923 relvars1[3] = gammai*3+3;
924 relvars1[4] = gammai*3+4;
925 relvars1[5] = gammai*3+5;
926 relvars1[6] = deltai*3;
927 relvars1[7] = deltai*3+1;
928 relvars1[8] = deltai*3+2;
929 relvars1[9] = deltai*3+3;
930 relvars1[10] = deltai*3+4;
931 relvars1[11] = deltai*3+5;
932 relvars1[12] = i*3;
933 relvars1[13] = i*3+1;
934 relvars1[14] = i*3+2;
935 relvars1[15] = i*3+3;
936 relvars1[16] = i*3+4;
937 relvars1[17] = i*3+5;
938 relvarset1 = sylvan_set_fromarray(relvars1, 18);
939 //(0 0 0 1 1 0 1 1 0 1 0 0 1 0 0 0 1 1)
940 rel_enc1[0] = 0;
941 rel_enc1[1] = 0;
942 rel_enc1[2] = 0;
943 rel_enc1[3] = 1;
944 rel_enc1[4] = 1;
945 rel_enc1[5] = 0;
946 rel_enc1[6] = 1;
947 rel_enc1[7] = 1;
948 rel_enc1[8] = 0;
949 rel_enc1[9] = 1;
950 rel_enc1[10] = 0;
951 rel_enc1[11] = 0;
952 rel_enc1[12] = 1;
953 rel_enc1[13] = 0;
954 rel_enc1[14] = 0;
955 rel_enc1[15] = 0;
956 rel_enc1[16] = 1;
957 rel_enc1[17] = 1;
958 trs_current = (trans_t *)malloc(sizeof(trans_t));
959 trs_current->bdd = sylvan_cube(relvarset1, rel_enc1);
960 trs_current->varset.varset = relvarset1;
961 trs_current->varset.size = 18;
962 trs_current->next_rel = trs;
963 trs = trs_current;
964
965 //Target Box Agent -> Targbox Agent Free
966 //(0 1 1 0 1 0 0 1 1 0 0 1 1 0 0 0 1 1)
967 relvars1[0] = gammai*3;
968 relvars1[1] = gammai*3+1;
969 relvars1[2] = gammai*3+2;
970 relvars1[3] = gammai*3+3;
971 relvars1[4] = gammai*3+4;
972 relvars1[5] = gammai*3+5;
973 relvars1[6] = deltai*3;
974 relvars1[7] = deltai*3+1;
975 relvars1[8] = deltai*3+2;
976 relvars1[9] = deltai*3+3;
977 relvars1[10] = deltai*3+4;
978 relvars1[11] = deltai*3+5;
979 relvars1[12] = i*3;
980 relvars1[13] = i*3+1;
981 relvars1[14] = i*3+2;
982 relvars1[15] = i*3+3;
983 relvars1[16] = i*3+4;
984 relvars1[17] = i*3+5;
985 relvarset1 = sylvan_set_fromarray(relvars1, 18);
986 //(0 1 1 0 1 0 0 1 1 0 0 1 1 0 0 0 1 1)
987 rel_enc1[0] = 0;
988 rel_enc1[1] = 1;
989 rel_enc1[2] = 1;
990 rel_enc1[3] = 0;
991 rel_enc1[4] = 1;
992 rel_enc1[5] = 0;
993 rel_enc1[6] = 0;
994 rel_enc1[7] = 1;
995 rel_enc1[8] = 1;
996 rel_enc1[9] = 0;
997 rel_enc1[10] = 0;
998 rel_enc1[11] = 1;
999 rel_enc1[12] = 1;
1000 rel_enc1[13] = 0;
1001 rel_enc1[14] = 0;
1002 rel_enc1[15] = 0;
1003 rel_enc1[16] = 1;
1004 rel_enc1[17] = 1;
1005 trs_current = (trans_t *)malloc(sizeof(trans_t));
1006 trs_current->bdd = sylvan_cube(relvarset1, rel_enc1);
1007 trs_current->varset.varset = relvarset1;
1008 trs_current->varset.size = 18;
1009 trs_current->next_rel = trs;
1010 trs = trs_current;
1011
1012 //Target Targbox Agent -> Targbox Targagent Free
1013 //(0 1 1 0 1 0 1 1 0 1 0 0 1 0 0 0 1 1)
1014 relvars1[0] = gammai*3;
1015 relvars1[1] = gammai*3+1;
1016 relvars1[2] = gammai*3+2;
1017 relvars1[3] = gammai*3+3;
1018 relvars1[4] = gammai*3+4;
1019 relvars1[5] = gammai*3+5;
1020 relvars1[6] = deltai*3;
1021 relvars1[7] = deltai*3+1;
1022 relvars1[8] = deltai*3+2;
1023 relvars1[9] = deltai*3+3;
1024 relvars1[10] = deltai*3+4;
1025 relvars1[11] = deltai*3+5;
1026 relvars1[12] = i*3;
1027 relvars1[13] = i*3+1;
1028 relvars1[14] = i*3+2;
1029 relvars1[15] = i*3+3;
1030 relvars1[16] = i*3+4;
1031 relvars1[17] = i*3+5;
1032 relvarset1 = sylvan_set_fromarray(relvars1, 18);
1033 //(0 1 1 0 1 0 1 1 0 1 0 0 1 0 0 0 1 1)
1034 rel_enc1[0] = 0;
1035 rel_enc1[1] = 1;
1036 rel_enc1[2] = 1;
1037 rel_enc1[3] = 0;
1038 rel_enc1[4] = 1;
1039 rel_enc1[5] = 0;
1040 rel_enc1[6] = 1;
1041 rel_enc1[7] = 1;
1042 rel_enc1[8] = 0;
1043 rel_enc1[9] = 1;
1044 rel_enc1[10] = 0;
1045 rel_enc1[11] = 0;
1046 rel_enc1[12] = 1;
1047 rel_enc1[13] = 0;
1048 rel_enc1[14] = 0;
1049 rel_enc1[15] = 0;
1050 rel_enc1[16] = 1;
1051 rel_enc1[17] = 1;
1052 trs_current = (trans_t *)malloc(sizeof(trans_t));
1053 trs_current->bdd = sylvan_cube(relvarset1, rel_enc1);
1054 trs_current->varset.varset = relvarset1;
1055 trs_current->varset.size = 18;
1056 trs_current->next_rel = trs;
1057 trs = trs_current;
1058
1059 //Free Box Targagent -> Box Agent Target
1060 //(0 0 0 1 1 0 0 1 1 0 0 1 1 0 1 1 0 1)
1061 relvars1[0] = gammai*3;
1062 relvars1[1] = gammai*3+1;
1063 relvars1[2] = gammai*3+2;
1064 relvars1[3] = gammai*3+3;
1065 relvars1[4] = gammai*3+4;
1066 relvars1[5] = gammai*3+5;
1067 relvars1[6] = deltai*3;
1068 relvars1[7] = deltai*3+1;
1069 relvars1[8] = deltai*3+2;
1070 relvars1[9] = deltai*3+3;
1071 relvars1[10] = deltai*3+4;
1072 relvars1[11] = deltai*3+5;
1073 relvars1[12] = i*3;
1074 relvars1[13] = i*3+1;
1075 relvars1[14] = i*3+2;
1076 relvars1[15] = i*3+3;
1077 relvars1[16] = i*3+4;
1078 relvars1[17] = i*3+5;
1079 relvarset1 = sylvan_set_fromarray(relvars1, 18);
1080 //(0 0 0 1 1 0 0 1 1 0 0 1 1 0 1 1 0 1)
1081 rel_enc1[0] = 0;
1082 rel_enc1[1] = 0;
1083 rel_enc1[2] = 0;
1084 rel_enc1[3] = 1;
1085 rel_enc1[4] = 1;
1086 rel_enc1[5] = 0;
1087 rel_enc1[6] = 0;
1088 rel_enc1[7] = 1;
1089 rel_enc1[8] = 1;
1090 rel_enc1[9] = 0;
1091 rel_enc1[10] = 0;
1092 rel_enc1[11] = 1;
1093 rel_enc1[12] = 1;
1094 rel_enc1[13] = 0;
1095 rel_enc1[14] = 1;
1096 rel_enc1[15] = 1;
1097 rel_enc1[16] = 0;
1098 rel_enc1[17] = 1;
1099 trs_current = (trans_t *)malloc(sizeof(trans_t));
1100 trs_current->bdd = sylvan_cube(relvarset1, rel_enc1);
1101 trs_current->varset.varset = relvarset1;
1102 trs_current->varset.size = 18;
1103 trs_current->next_rel = trs;
1104 trs = trs_current;
1105
1106 //Free Targbox Targagent -> Box Targagent Target
1107 //(0 0 0 1 1 0 1 1 0 1 0 0 1 0 1 1 0 1)
1108 relvars1[0] = gammai*3;
1109 relvars1[1] = gammai*3+1;
1110 relvars1[2] = gammai*3+2;
1111 relvars1[3] = gammai*3+3;
1112 relvars1[4] = gammai*3+4;
1113 relvars1[5] = gammai*3+5;
1114 relvars1[6] = deltai*3;
1115 relvars1[7] = deltai*3+1;
1116 relvars1[8] = deltai*3+2;
1117 relvars1[9] = deltai*3+3;
1118 relvars1[10] = deltai*3+4;
1119 relvars1[11] = deltai*3+5;
1120 relvars1[12] = i*3;
1121 relvars1[13] = i*3+1;
1122 relvars1[14] = i*3+2;
1123 relvars1[15] = i*3+3;
1124 relvars1[16] = i*3+4;
1125 relvars1[17] = i*3+5;
1126 relvarset1 = sylvan_set_fromarray(relvars1, 18);
1127 //(0 0 0 1 1 0 1 1 0 1 0 0 1 0 1 1 0 1)
1128 rel_enc1[0] = 0;
1129 rel_enc1[1] = 0;
1130 rel_enc1[2] = 0;
1131 rel_enc1[3] = 1;
1132 rel_enc1[4] = 1;
1133 rel_enc1[5] = 0;
1134 rel_enc1[6] = 1;
1135 rel_enc1[7] = 1;
1136 rel_enc1[8] = 0;
1137 rel_enc1[9] = 1;
1138 rel_enc1[10] = 0;
1139 rel_enc1[11] = 0;
1140 rel_enc1[12] = 1;
1141 rel_enc1[13] = 0;
1142 rel_enc1[14] = 1;
1143 rel_enc1[15] = 1;
1144 rel_enc1[16] = 0;
1145 rel_enc1[17] = 1;
1146 trs_current = (trans_t *)malloc(sizeof(trans_t));
1147 trs_current->bdd = sylvan_cube(relvarset1, rel_enc1);
1148 trs_current->varset.varset = relvarset1;
1149 trs_current->varset.size = 18;
1150 trs_current->next_rel = trs;
1151 trs = trs_current;
1152
1153 //Target Box Targagent -> Targbox Agent Target
1154 //(0 1 1 0 1 0 0 1 1 0 0 1 1 0 1 1 0 1)
1155 relvars1[0] = gammai*3;
1156 relvars1[1] = gammai*3+1;
1157 relvars1[2] = gammai*3+2;
1158 relvars1[3] = gammai*3+3;
1159 relvars1[4] = gammai*3+4;
1160 relvars1[5] = gammai*3+5;
1161 relvars1[6] = deltai*3;
1162 relvars1[7] = deltai*3+1;
1163 relvars1[8] = deltai*3+2;
1164 relvars1[9] = deltai*3+3;
1165 relvars1[10] = deltai*3+4;
1166 relvars1[11] = deltai*3+5;
1167 relvars1[12] = i*3;
1168 relvars1[13] = i*3+1;
1169 relvars1[14] = i*3+2;
1170 relvars1[15] = i*3+3;
1171 relvars1[16] = i*3+4;
1172 relvars1[17] = i*3+5;
1173 relvarset1 = sylvan_set_fromarray(relvars1, 18);
1174 //(0 1 1 0 1 0 0 1 1 0 0 1 1 0 1 1 0 1)
1175 rel_enc1[0] = 0;
1176 rel_enc1[1] = 1;
1177 rel_enc1[2] = 1;
1178 rel_enc1[3] = 0;
1179 rel_enc1[4] = 1;
1180 rel_enc1[5] = 0;
1181 rel_enc1[6] = 0;
1182 rel_enc1[7] = 1;
1183 rel_enc1[8] = 1;
1184 rel_enc1[9] = 0;
1185 rel_enc1[10] = 0;
1186 rel_enc1[11] = 1;
1187 rel_enc1[12] = 1;
1188 rel_enc1[13] = 0;
1189 rel_enc1[14] = 1;
1190 rel_enc1[15] = 1;
1191 rel_enc1[16] = 0;
1192 rel_enc1[17] = 1;
1193 trs_current = (trans_t *)malloc(sizeof(trans_t));
1194 trs_current->bdd = sylvan_cube(relvarset1, rel_enc1);
1195 trs_current->varset.varset = relvarset1;
1196 trs_current->varset.size = 18;
1197 trs_current->next_rel = trs;
1198 trs = trs_current;
1199
1200 //Target Targbox Targagent -> Targbox Targagent Target
1201 //(0 1 1 0 1 0 1 1 0 1 0 0 1 0 1 1 0 1)
1202 relvars1[0] = gammai*3;
1203 relvars1[1] = gammai*3+1;
1204 relvars1[2] = gammai*3+2;
1205 relvars1[3] = gammai*3+3;
1206 relvars1[4] = gammai*3+4;
1207 relvars1[5] = gammai*3+5;
1208 relvars1[6] = deltai*3;
1209 relvars1[7] = deltai*3+1;
1210 relvars1[8] = deltai*3+2;
1211 relvars1[9] = deltai*3+3;
1212 relvars1[10] = deltai*3+4;
1213 relvars1[11] = deltai*3+5;
1214 relvars1[12] = i*3;
1215 relvars1[13] = i*3+1;
1216 relvars1[14] = i*3+2;
1217 relvars1[15] = i*3+3;
1218 relvars1[16] = i*3+4;
1219 relvars1[17] = i*3+5;
1220 relvarset1 = sylvan_set_fromarray(relvars1, 18);
1221 //(0 1 1 0 1 0 1 1 0 1 0 0 1 0 1 1 0 1)
1222 rel_enc1[0] = 0;
1223 rel_enc1[1] = 1;
1224 rel_enc1[2] = 1;
1225 rel_enc1[3] = 0;
1226 rel_enc1[4] = 1;
1227 rel_enc1[5] = 0;
1228 rel_enc1[6] = 1;
1229 rel_enc1[7] = 1;
1230 rel_enc1[8] = 0;
1231 rel_enc1[9] = 1;
1232 rel_enc1[10] = 0;
1233 rel_enc1[11] = 0;
1234 rel_enc1[12] = 1;
1235 rel_enc1[13] = 0;
1236 rel_enc1[14] = 1;
1237 rel_enc1[15] = 1;
1238 rel_enc1[16] = 0;
1239 rel_enc1[17] = 1;
1240 trs_current = (trans_t *)malloc(sizeof(trans_t));
1241 trs_current->bdd = sylvan_cube(relvarset1, rel_enc1);
1242 trs_current->varset.varset = relvarset1;
1243 trs_current->varset.size = 18;
1244 trs_current->next_rel = trs;
1245 trs = trs_current;
1246 }
1247 }
1248 trs_current = trs;
1249 return trs;
1250 }
1251
1252 rels *encode_rel(sokoban_screen *screen)
1253 {
1254 LACE_ME;
1255
1256 trans_t *tl = sylvan_false;
1257
1258 //left relation
1259 tl = create_single_rel(screen, LEFT);
1260
1261 //up relation
1262 trans_t *tu = create_single_rel(screen, UP);
1263
1264 //right relation
1265 trans_t *tr = create_single_rel(screen, RIGHT);
1266
1267 //down relation
1268 trans_t *td = create_single_rel(screen, DOWN);
1269
1270 rels *rls = NULL;
1271 rls = (rels *)malloc(sizeof(rels));
1272 rls->rell = tl;
1273 rls->relu = tu;
1274 rls->relr = tr;
1275 rls->reld = td;
1276
1277 return rls;
1278 }
1279
1280 int
1281 test_relprod()
1282 {
1283 LACE_ME;
1284
1285 BDDVAR vars[] = {0,2,4};
1286 BDDVAR all_vars[] = {0,1,2,3,4,5};
1287 BDDVAR all_vars2[] = {0,1};
1288 //BDDVAR short_vars[] = {0,1};
1289 /*BDDVAR short_vars2[] = {2,3};
1290 BDDVAR short_vars3[] = {0,1,2,3};*/
1291
1292 BDDSET vars_set = sylvan_set_fromarray(vars, 3);
1293 BDDSET all_vars_set = sylvan_set_fromarray(all_vars, 6);
1294 BDDSET all_vars_set2 = sylvan_set_fromarray(all_vars2, 2);
1295 //BDDSET short_vars_set = sylvan_set_fromarray(short_vars, 2);
1296 /*BDDSET short_vars_set2 = sylvan_set_fromarray(short_vars2, 2);
1297 BDDSET short_vars_set3 = sylvan_set_fromarray(short_vars3, 4);*/
1298
1299 BDD s, t, next, prev;
1300 BDD zeroes, ones;
1301
1302 // transition relation: 000 --> 111 and !000 --> 000
1303 t = sylvan_false;
1304 t = sylvan_union_cube(t, all_vars_set2, ((uint8_t[]){0,1}));
1305 //t = sylvan_union_cube(t, all_vars_set, ((uint8_t[]){1,0,2,0,2,0}));
1306 t = sylvan_union_cube(t, all_vars_set2, ((uint8_t[]){1,0}));
1307 // t = sylvan_union_cube(t, all_vars_set, ((uint8_t[]){0,1}));
1308
1309 s = sylvan_cube(vars_set, (uint8_t[]){0,0,0});
1310 zeroes = sylvan_cube(vars_set, (uint8_t[]){1,0,0});
1311 ones = sylvan_cube(vars_set, (uint8_t[]){0,0,0});
1312
1313 next = sylvan_relnext(s, t, all_vars_set);
1314 prev = sylvan_relprev(t, next, all_vars_set);
1315 if (next == zeroes) printf("Pass 1\n");
1316 if (prev == ones) printf("Pass 2\n");
1317 //trans *ts;
1318 //ts = NULL;
1319
1320 return 0;
1321 }
Unnamed repository; edit this file 'description' to name the repository.