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