#include <argp.h>
-#include <inttypes.h>
-#include <locale.h>
#include <stdio.h>
#include <stdlib.h>
-#include <string.h>
-#include <sys/time.h>
-
-#ifdef HAVE_PROFILER
-#include <gperftools/profiler.h>
-#endif
-
#include <sylvan.h>
-#include <llmsset.h>
#include <lace.h>
#include "coord.h"
#include "sokoban.h"
+#include "deque.h"
typedef struct {
memset(f, 0, sizeof(xy_bddvar_map));
f->key.x = r->coord.x;
f->key.y = r->coord.y;
- f->value.var[0] = varcount;
- f->value.var[1] = varcount + 1;
- f->value.var[2] = varcount + 2;
+ f->value.var[0] = varcount * 2;
+ f->value.var[1] = (varcount + 1) * 2;
+ f->value.var[2] = (varcount + 2) * 2;
HASH_ADD(hh, xybdd, key, sizeof(xy), f);
for (int i = 0; i <3; i++){
bddvar_xy_map *t = NULL;
t = (bddvar_xy_map *)malloc(sizeof(bddvar_xy_map));
memset(t, 0, sizeof(bddvar_xy_map));
- t->key = varcount + i;
+ t->key = (varcount + i) * 2;
t->value.x = r->coord.x;
t->value.y = r->coord.y;
HASH_ADD(hh, bddxy, key, sizeof(int), t);
tile_index++;
st_enc[tile_index] = 0;
tile_index++;
+
st_enc[tile_index] = 1;
tile_index++;
break;
return fullState;
}
+lurd_t *lappend(lurd_t *l, char c){
+ lurd_t *temp_lrd = NULL;
+ if (l == NULL){
+ temp_lrd = (lurd_t *)malloc(sizeof(lurd_t));
+ temp_lrd->c = c;
+ temp_lrd->next = NULL;
+ l = temp_lrd;
+ }
+ else {
+ temp_lrd = l;
+ while (temp_lrd->next != NULL){
+ temp_lrd = temp_lrd->next;
+ }
+ temp_lrd->next = (lurd_t *)malloc(sizeof(lurd_t));
+ temp_lrd->next->c = c;
+ temp_lrd->next->next = NULL;
+ }
+ return l;
+}
+
+int check_goal(BDD s, BDD g, BDDSET vars){
+ LACE_ME;
+ if(sylvan_satcount(sylvan_and(s, g), vars) > 0) return 1;
+ else return 0;
+}
+
+int check_visited(BDD s, BDD v, BDDSET vars){
+ LACE_ME;
+ if(sylvan_satcount(sylvan_and(s, v), vars) > 0) return 1;
+ else return 0;
+}
+
+state_t *explstate(state *init, rels *rls, state *g){
+ LACE_ME;
+ deque *state_queue = create();
+ trans_t *t = NULL;
+ state_t *tmp_state = (state_t *)malloc(sizeof(state_t));
+ lurd_t *lrd = (lurd_t *)malloc(sizeof(lurd_t));
+ //state_t *new_state = (state_t *)malloc(sizeof(state_t));
+ BDD visited = init->bdd;
+ BDD new;
+ tmp_state->bdd = init->bdd;
+ tmp_state->vars = init->vars;
+ tmp_state->lrd = lrd;
+ state_queue = enq(tmp_state, state_queue);
+
+ while (isEmpty(state_queue) == 0){
+ tmp_state = get_front(state_queue);
+ state_queue = deq(state_queue);
+ new = tmp_state->bdd;
+ t = rls->rell;
+ while (t != NULL){
+ new = sylvan_relnext(tmp_state->bdd, t->bdd, t->varset.varset);
+ if (new != sylvan_false && new != tmp_state->bdd) break;
+ t = t->next_rel;
+ }
+ if (new != sylvan_false && new != tmp_state->bdd){
+ if (check_visited(new, visited, init->vars.varset) == 0){
+ if (check_goal(new, g->bdd, init->vars.varset) == 0){
+ lurd_t *lrd = (lurd_t *)malloc(sizeof(lurd_t));
+ state_t *new_state = (state_t *)malloc(sizeof(state_t));
+ memcpy(lrd, tmp_state->lrd, sizeof(lurd_t));
+ new_state->bdd = new;
+ new_state->vars = init->vars;
+ lrd = lappend(lrd, 'l');
+ new_state->lrd = lrd;
+ state_queue = enq(new_state, state_queue);
+ visited = sylvan_or(new, visited);
+ }
+ else {
+ printf("GOAL\n");
+ lurd_t *lrd = (lurd_t *)malloc(sizeof(lurd_t));
+ state_t *new_state = (state_t *)malloc(sizeof(state_t));
+ memcpy(lrd, tmp_state->lrd, sizeof(lurd_t));
+ new_state->bdd = new;
+ new_state->vars = init->vars;
+ lrd = lappend(lrd, 'l');
+ new_state->lrd = lrd;
+ return new_state;
+ }
+ }
+ }
+
+ t = rls->relu;
+ while (t != NULL){
+ new = sylvan_relnext(tmp_state->bdd, t->bdd, t->varset.varset);
+ if (new != sylvan_false && new != tmp_state->bdd) break;
+ t = t->next_rel;
+ }
+ if (new != sylvan_false && new != tmp_state->bdd){
+ if (check_visited(new, visited, init->vars.varset) == 0){
+ if (check_goal(new, g->bdd, init->vars.varset) == 0){
+ lurd_t *lrd = (lurd_t *)malloc(sizeof(lurd_t));
+ state_t *new_state = (state_t *)malloc(sizeof(state_t));
+ memcpy(lrd, tmp_state->lrd, sizeof(lurd_t));
+ new_state->bdd = new;
+ new_state->vars = init->vars;
+ lrd = lappend(lrd, 'u');
+ new_state->lrd = lrd;
+ state_queue = enq(new_state, state_queue);
+ visited = sylvan_or(new, visited);
+ }
+ else {
+ printf("GOAL\n");
+ lurd_t *lrd = (lurd_t *)malloc(sizeof(lurd_t));
+ state_t *new_state = (state_t *)malloc(sizeof(state_t));
+ memcpy(lrd, tmp_state->lrd, sizeof(lurd_t));
+ new_state->bdd = new;
+ new_state->vars = init->vars;
+ lrd = lappend(lrd, 'u');
+ new_state->lrd = lrd;
+ return new_state;
+ }
+ }
+ }
+
+ t = rls->relr;
+ while (t != NULL){
+ new = sylvan_relnext(tmp_state->bdd, t->bdd, t->varset.varset);
+ if (new != sylvan_false && new != tmp_state->bdd) break;
+ t = t->next_rel;
+ }
+ if (new != sylvan_false && new != tmp_state->bdd){
+ if (check_visited(new, visited, init->vars.varset) == 0){
+ if (check_goal(new, g->bdd, init->vars.varset) == 0){
+ lurd_t *lrd = (lurd_t *)malloc(sizeof(lurd_t));
+ state_t *new_state = (state_t *)malloc(sizeof(state_t));
+ memcpy(lrd, tmp_state->lrd, sizeof(lurd_t));
+
+ new_state->bdd = new;
+ new_state->vars = init->vars;
+ lrd = lappend(lrd, 'r');
+ new_state->lrd = lrd;
+ state_queue = enq(new_state, state_queue);
+ visited = sylvan_or(new, visited);
+ }
+ else {
+ printf("GOAL\n");
+ lurd_t *lrd = (lurd_t *)malloc(sizeof(lurd_t));
+ state_t *new_state = (state_t *)malloc(sizeof(state_t));
+ memcpy(lrd, tmp_state->lrd, sizeof(lurd_t));
+
+ new_state->bdd = new;
+ new_state->vars = init->vars;
+ lrd = lappend(lrd, 'r');
+ new_state->lrd = lrd;
+ return new_state;
+ }
+ }
+ }
+
+
+ t = rls->reld;
+ while (t != NULL){
+ new = sylvan_relnext(tmp_state->bdd, t->bdd, t->varset.varset);
+ if (new != sylvan_false && new != tmp_state->bdd) break;
+ t = t->next_rel;
+ }
+ if (new != sylvan_false && new != tmp_state->bdd){
+ if (check_visited(new, visited, init->vars.varset) == 0){
+ if (check_goal(new, g->bdd, init->vars.varset) == 0){
+
+ lurd_t *lrd = (lurd_t *)malloc(sizeof(lurd_t));
+ state_t *new_state = (state_t *)malloc(sizeof(state_t));
+ memcpy(lrd, tmp_state->lrd, sizeof(lurd_t));
+
+ new_state->bdd = new;
+ new_state->vars = init->vars;
+ lrd = lappend(lrd, 'd');
+ new_state->lrd = lrd;
+ state_queue = enq(new_state, state_queue);
+ visited = sylvan_or(new, visited);
+ }
+ else {
+ printf("GOAL\n");
+ lurd_t *lrd = (lurd_t *)malloc(sizeof(lurd_t));
+ state_t *new_state = (state_t *)malloc(sizeof(state_t));
+ memcpy(lrd, tmp_state->lrd, sizeof(lurd_t));
+
+ new_state->bdd = new;
+ new_state->vars = init->vars;
+ lrd = lappend(lrd, 'd');
+ new_state->lrd = lrd;
+ return new_state;
+ }
+ }
+ }
+
+
+ }
+
+ return NULL;
+}
+
+state *encode_goal(sokoban_screen *screen){
+ int boxes = 0;
+ int targets = 0;
+
+ LACE_ME;
+
+ BDDVAR vars[HASH_COUNT(screen) * 3];
+ for (uint8_t i = 0; i < HASH_COUNT(screen) * 3; i++){
+ vars[i] = i * 2;
+ }
+
+ uint8_t st_enc[HASH_COUNT(screen) * 3];
+
+ BDDSET varset = sylvan_set_fromarray(vars, HASH_COUNT(screen) * 3);
+ BDD s;
+ state *fullState = NULL;
+ fullState = (state *)malloc(sizeof(state));
+ fullState->vars.varset = varset;
+ fullState->vars.size = HASH_COUNT(screen) * 3;
+ int tile_index = 0;
+ sokoban_screen *r;
+ for(r=screen; r != NULL; r = (sokoban_screen *)(r->hh.next)){
+ switch(r->tile){
+ case FREE: //001 -> any
+ st_enc[tile_index] = 2;
+ tile_index++;
+ st_enc[tile_index] = 2;
+ tile_index++;
+ st_enc[tile_index] = 2;
+ tile_index++;
+ break;
+ case WALL: //000 -> stays the same
+ st_enc[tile_index] = 0;
+ tile_index++;
+ st_enc[tile_index] = 0;
+ tile_index++;
+ st_enc[tile_index] = 0;
+ tile_index++;
+ break;
+ case BOX: //010 -> any
+ boxes++;
+ st_enc[tile_index] = 2;
+ tile_index++;
+ st_enc[tile_index] = 2;
+ tile_index++;
+ st_enc[tile_index] = 2;
+ tile_index++;
+ break;
+ case TARGET: //011 -> targbox
+ targets++;
+ st_enc[tile_index] = 1;
+ tile_index++;
+ st_enc[tile_index] = 0;
+ tile_index++;
+ st_enc[tile_index] = 0;
+ tile_index++;
+ break;
+ case AGENT: //101 -> any
+ st_enc[tile_index] = 2;
+ tile_index++;
+ st_enc[tile_index] = 2;
+ tile_index++;
+ st_enc[tile_index] = 2;
+ tile_index++;
+ break;
+ case TARGAGENT: //110 -> targbox
+ targets++;
+ st_enc[tile_index] = 1;
+ tile_index++;
+ st_enc[tile_index] = 0;
+ tile_index++;
+ st_enc[tile_index] = 0;
+ tile_index++;
+ break;
+ case TARGBOX: //100 -> stays the same
+ targets++;
+ boxes++;
+ st_enc[tile_index] = 1;
+ tile_index++;
+ st_enc[tile_index] = 0;
+ tile_index++;
+ st_enc[tile_index] = 0;
+ tile_index++;
+ break;
+ }
+ }
+ s = sylvan_cube(varset, st_enc);
+ fullState->bdd = s;
+ printf("Goal state encoded\n");
+ if (targets == 0 || (boxes != targets)) return NULL;
+ else return fullState;
+
+}
+
+//test
+//int countTrans(trans_t *trs);
+
trans_t *create_single_rel(sokoban_screen *screen, direction dir)
{
LACE_ME;
}
for (unsigned int i = 0; i < HASH_COUNT(screen); i++){
- bddxy = getbdd(i*3, bm->t);
+ bddxy = getbdd(i*6, bm->t);
x = bddxy->value.x;
y = bddxy->value.y;
if (check_space(x, y, dir, 1, bm) == 0){
-
//Agent -> Agent
//1 1 0 0 1 1 (1 0 1 -> 1 0 1)
- BDDVAR relvars[6] = {i * 3, i * 3 + 1, i * 3 + 2, i * 3 + 3, i * 3 + 4, i * 3 + 5};
+ BDDVAR relvars[6] = {i * 6, i * 6 + 1, i * 6 + 2, i * 6 + 3, i * 6 + 4, i * 6 + 5};
BDDSET relvarset = sylvan_set_fromarray(relvars, 6);
uint8_t rel_enc[6] = {1, 1, 0, 0, 1, 1};
-
trs_current = (trans_t *)malloc(sizeof(trans_t));
trs_current->bdd = sylvan_cube(relvarset, rel_enc);
trs_current->varset.varset = relvarset;
//Targagent -> Targagent
//1 1 1 1 0 0 (1 1 0 -> 1 1 0)
- relvars[0] = i * 3;
- relvars[1] = i * 3 + 1;
- relvars[2] = i * 3 + 2;
- relvars[3] = i * 3 + 3;
- relvars[4] = i * 3 + 4;
- relvars[5] = i * 3 + 5;
relvarset = sylvan_set_fromarray(relvars, 6);
- rel_enc[0] = 1;
- rel_enc[1] = 1;
- rel_enc[2] = 1;
- rel_enc[3] = 1;
- rel_enc[4] = 0;
- rel_enc[5] = 0;
+ uint8_t rel_enc1[6] = {1, 1, 1, 1, 0, 0};
+ memcpy(rel_enc, rel_enc1, 6*sizeof(uint8_t));
trs_current = (trans_t *)malloc(sizeof(trans_t));
trs_current->bdd = sylvan_cube(relvarset, rel_enc);
trs = trs_current;
}
- else if (check_space(x, y, dir, 1, bm) == 1 && check_space(x, y, dir, 2, bm) == 0){
+ else if (check_space(x, y, dir, 1, bm) == 1 && check_space(x, y, dir, 2, bm) == 0){
xy_bddvar_map *bddvar = getxy(x + xdelta, y + ydelta, bm->f);
- int deltai = bddvar->value.var[0];
-
- //Free Agent -> Agent Free
- //(0 1 0 0 1 1 1 0 0 0 1 1)
- 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};
+ unsigned int deltai = bddvar->value.var[0];
+ //Agent Free -> Free Agent
+ //(1 0 0 0 1 1 0 1 0 0 1 1)
+ //or
+ //(0 1 0 0 1 1 1 0 0 0 1 1)
+ 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};
BDDSET relvarset = sylvan_set_fromarray(relvars, 12);
- uint8_t rel_enc[12] = {0, 1, 0, 0, 1, 1, 1, 0, 0, 0, 1, 1};
+ uint8_t rel_enc[12];
+ if (i*6 < deltai){
+ uint8_t rel_enc0[12] = {1, 0, 0, 0, 1, 1, 0, 1, 0, 0, 1, 1};
+ memcpy(rel_enc, rel_enc0, 12*sizeof(uint8_t));
+ }
+ else {
+ uint8_t rel_enc0[12] = {0, 1, 0, 0, 1, 1, 1, 0, 0, 0, 1, 1};
+ memcpy(rel_enc, rel_enc0, 12*sizeof(uint8_t));
+ }
trs_current = (trans_t *)malloc(sizeof(trans_t));
trs_current->bdd = sylvan_cube(relvarset, rel_enc);
trs_current->varset.varset = relvarset;
trs_current->next_rel = trs;
trs = trs_current;
- //Target Agent -> Targagent Free
- //(0 1 1 1 1 0 1 0 0 0 1 1)
- relvars[0] = deltai*3;
- relvars[1] = deltai*3+1;
- relvars[2] = deltai*3+2;
- relvars[3] = deltai*3+3;
- relvars[4] = deltai*3+4;
- relvars[5] = deltai*3+5;
- relvars[6] = i*3;
- relvars[7] = i*3+1;
- relvars[8] = i*3+2;
- relvars[9] = i*3+3;
- relvars[10] = i*3+4;
- relvars[11] = i*3+5;
+ //Agent Target -> Free Targagent
+ //(1 0 0 0 1 1 0 1 1 1 1 0)
+ //or
+ //(0 1 1 1 1 0 1 0 0 0 1 1)
relvarset = sylvan_set_fromarray(relvars, 12);
- rel_enc[0] = 0;
- rel_enc[1] = 1;
- rel_enc[2] = 1;
- rel_enc[3] = 1;
- rel_enc[4] = 1;
- rel_enc[5] = 0;
- rel_enc[6] = 1;
- rel_enc[7] = 0;
- rel_enc[8] = 0;
- rel_enc[9] = 0;
- rel_enc[10] = 1;
- rel_enc[11] = 1;
+ if (i*6 < deltai){
+ uint8_t rel_enc2[12] = {1, 0, 0, 0, 1, 1, 0, 1, 1, 1, 1, 0};
+ memcpy(rel_enc, rel_enc2, 12*sizeof(uint8_t));
+ }
+ else {
+ uint8_t rel_enc2[12] = {0, 1, 1, 1, 1, 0, 1, 0, 0, 0, 1, 1};
+ memcpy(rel_enc, rel_enc2, 12*sizeof(uint8_t));
+ }
trs_current = (trans_t *)malloc(sizeof(trans_t));
trs_current->bdd = sylvan_cube(relvarset, rel_enc);
trs_current->varset.varset = relvarset;
trs_current->next_rel = trs;
trs = trs_current;
- //Must be: Free Targagent -> Agent Target
- //(0 1 0 0 1 1 1 0 1 1 0 1)
- relvars[0] = deltai*3;
- relvars[1] = deltai*3+1;
- relvars[2] = deltai*3+2;
- relvars[3] = deltai*3+3;
- relvars[4] = deltai*3+4;
- relvars[5] = deltai*3+5;
- relvars[6] = i*3;
- relvars[7] = i*3+1;
- relvars[8] = i*3+2;
- relvars[9] = i*3+3;
- relvars[10] = i*3+4;
- relvars[11] = i*3+5;
+ //Targagent Free -> Target Agent
+ //(1 0 1 1 0 1 0 1 0 0 1 1)
+ //or
+ //(0 1 0 0 1 1 1 0 1 1 0 1)
relvarset = sylvan_set_fromarray(relvars, 12);
- rel_enc[0] = 0;
- rel_enc[1] = 1;
- rel_enc[2] = 0;
- rel_enc[3] = 0;
- rel_enc[4] = 1;
- rel_enc[5] = 1;
- rel_enc[6] = 1;
- rel_enc[7] = 0;
- rel_enc[8] = 1;
- rel_enc[9] = 1;
- rel_enc[10] = 0;
- rel_enc[11] = 1;
+ if (i*6 < deltai){
+ uint8_t rel_enc3[12] = {1, 0, 1, 1, 0, 1, 0, 1, 0, 0, 1, 1};
+ memcpy(rel_enc, rel_enc3, 12*sizeof(uint8_t));
+ }
+ else {
+ uint8_t rel_enc3[12] = {0, 1, 0, 0, 1, 1, 1, 0, 1, 1, 0, 1};
+ memcpy(rel_enc, rel_enc3, 12*sizeof(uint8_t));
+ }
trs_current = (trans_t *)malloc(sizeof(trans_t));
trs_current->bdd = sylvan_cube(relvarset, rel_enc);
trs_current->varset.varset = relvarset;
trs_current->next_rel = trs;
trs = trs_current;
- //Target Targagent -> Targagent Target
- //(0 1 1 1 1 0 1 0 1 1 0 1)
- relvars[0] = deltai*3;
- relvars[1] = deltai*3+1;
- relvars[2] = deltai*3+2;
- relvars[3] = deltai*3+3;
- relvars[4] = deltai*3+4;
- relvars[5] = deltai*3+5;
- relvars[6] = i*3;
- relvars[7] = i*3+1;
- relvars[8] = i*3+2;
- relvars[9] = i*3+3;
- relvars[10] = i*3+4;
- relvars[11] = i*3+5;
+ //Targagent Target -> Target Targagent
+ //(1 0 1 1 0 1 0 1 1 1 1 0)
+ //or
+ //(0 1 1 1 1 0 1 0 1 1 0 1)
relvarset = sylvan_set_fromarray(relvars, 12);
- rel_enc[0] = 0;
- rel_enc[1] = 1;
- rel_enc[2] = 1;
- rel_enc[3] = 1;
- rel_enc[4] = 1;
- rel_enc[5] = 0;
- rel_enc[6] = 1;
- rel_enc[7] = 0;
- rel_enc[8] = 1;
- rel_enc[9] = 1;
- rel_enc[10] = 0;
- rel_enc[11] = 1;
+ if (i*6 < deltai){
+ uint8_t rel_enc4[12] = {1, 0, 1, 1, 0, 1, 0, 1, 1, 1, 1, 0};
+ memcpy(rel_enc, rel_enc4, 12*sizeof(uint8_t));
+ }
+ else {
+ uint8_t rel_enc4[12] = {0, 1, 1, 1, 1, 0, 1, 0, 1, 1, 0, 1};
+ memcpy(rel_enc, rel_enc4, 12*sizeof(uint8_t));
+ }
trs_current = (trans_t *)malloc(sizeof(trans_t));
trs_current->bdd = sylvan_cube(relvarset, rel_enc);
trs_current->varset.varset = relvarset;
trs_current->next_rel = trs;
trs = trs_current;
- //Box Agent -> Box Agent
- //(0 0 1 1 0 0 1 1 0 0 1 1)
- relvars[0] = deltai*3;
- relvars[1] = deltai*3+1;
- relvars[2] = deltai*3+2;
- relvars[3] = deltai*3+3;
- relvars[4] = deltai*3+4;
- relvars[5] = deltai*3+5;
- relvars[6] = i*3;
- relvars[7] = i*3+1;
- relvars[8] = i*3+2;
- relvars[9] = i*3+3;
- relvars[10] = i*3+4;
- relvars[11] = i*3+5;
+ //Agent Box -> Agent Box
+ //(1 1 0 0 1 1 0 0 1 1 0 0)
+ //or
+ //(0 0 1 1 0 0 1 1 0 0 1 1)
relvarset = sylvan_set_fromarray(relvars, 12);
- rel_enc[0] = 0;
- rel_enc[1] = 0;
- rel_enc[2] = 1;
- rel_enc[3] = 1;
- rel_enc[4] = 0;
- rel_enc[5] = 0;
- rel_enc[6] = 1;
- rel_enc[7] = 1;
- rel_enc[8] = 0;
- rel_enc[9] = 0;
- rel_enc[10] = 1;
- rel_enc[11] = 1;
+ if (i*6 < deltai){
+ uint8_t rel_enc5[12] = {1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0};
+ memcpy(rel_enc, rel_enc5, 12*sizeof(uint8_t));
+ }
+ else {
+ uint8_t rel_enc5[12] = {0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1};
+ memcpy(rel_enc, rel_enc5, 12*sizeof(uint8_t));
+ }
trs_current = (trans_t *)malloc(sizeof(trans_t));
trs_current->bdd = sylvan_cube(relvarset, rel_enc);
trs_current->varset.varset = relvarset;
trs_current->next_rel = trs;
trs = trs_current;
- //Targbox Agent -> Targbox Agent
- //(1 1 0 0 0 0 1 1 0 0 1 1)
- relvars[0] = deltai*3;
- relvars[1] = deltai*3+1;
- relvars[2] = deltai*3+2;
- relvars[3] = deltai*3+3;
- relvars[4] = deltai*3+4;
- relvars[5] = deltai*3+5;
- relvars[6] = i*3;
- relvars[7] = i*3+1;
- relvars[8] = i*3+2;
- relvars[9] = i*3+3;
- relvars[10] = i*3+4;
- relvars[11] = i*3+5;
+ //Agent Targbox -> Agent Targbox
+ //(1 1 0 0 1 1 1 1 0 0 0 0)
+ //
+ //(1 1 0 0 0 0 1 1 0 0 1 1)
relvarset = sylvan_set_fromarray(relvars, 12);
- rel_enc[0] = 1;
- rel_enc[1] = 1;
- rel_enc[2] = 0;
- rel_enc[3] = 0;
- rel_enc[4] = 0;
- rel_enc[5] = 0;
- rel_enc[6] = 1;
- rel_enc[7] = 1;
- rel_enc[8] = 0;
- rel_enc[9] = 0;
- rel_enc[10] = 1;
- rel_enc[11] = 1;
+ if (i*6 < deltai){
+ uint8_t rel_enc6[12] = {1, 1, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0};
+ memcpy(rel_enc, rel_enc6, 12*sizeof(uint8_t));
+ }
+ else {
+ uint8_t rel_enc6[12] = {1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1};
+ memcpy(rel_enc, rel_enc6, 12*sizeof(uint8_t));
+ }
trs_current = (trans_t *)malloc(sizeof(trans_t));
trs_current->bdd = sylvan_cube(relvarset, rel_enc);
trs_current->varset.varset = relvarset;
trs_current->next_rel = trs;
trs = trs_current;
- //Box Targagent -> Box Targagent
- //(0 0 1 1 0 0 1 1 1 1 0 0)
- relvars[0] = deltai*3;
- relvars[1] = deltai*3+1;
- relvars[2] = deltai*3+2;
- relvars[3] = deltai*3+3;
- relvars[4] = deltai*3+4;
- relvars[5] = deltai*3+5;
- relvars[6] = i*3;
- relvars[7] = i*3+1;
- relvars[8] = i*3+2;
- relvars[9] = i*3+3;
- relvars[10] = i*3+4;
- relvars[11] = i*3+5;
+ //Targagent Box -> Targagent Box
+ //(1 1 1 1 0 0 0 0 1 1 0 0)
+ //or
+ //(0 0 1 1 0 0 1 1 1 1 0 0)
relvarset = sylvan_set_fromarray(relvars, 12);
- rel_enc[0] = 0;
- rel_enc[1] = 0;
- rel_enc[2] = 1;
- rel_enc[3] = 1;
- rel_enc[4] = 0;
- rel_enc[5] = 0;
- rel_enc[6] = 1;
- rel_enc[7] = 1;
- rel_enc[8] = 1;
- rel_enc[9] = 1;
- rel_enc[10] = 0;
- rel_enc[11] = 0;
+ if (i*6 < deltai){
+ uint8_t rel_enc7[12] = {1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0};
+ memcpy(rel_enc, rel_enc7, 12*sizeof(uint8_t));
+ }
+ else {
+ uint8_t rel_enc7[12] = {0, 0, 1, 1, 0, 0, 1, 1, 1, 1, 0, 0};
+ memcpy(rel_enc, rel_enc7, 12*sizeof(uint8_t));
+ }
trs_current = (trans_t *)malloc(sizeof(trans_t));
trs_current->bdd = sylvan_cube(relvarset, rel_enc);
trs_current->varset.varset = relvarset;
trs_current->next_rel = trs;
trs = trs_current;
- //Targbox Targagent -> Targbox Targagent
- //(1 1 0 0 0 0 1 1 1 1 0 0)
- relvars[0] = deltai*3;
- relvars[1] = deltai*3+1;
- relvars[2] = deltai*3+2;
- relvars[3] = deltai*3+3;
- relvars[4] = deltai*3+4;
- relvars[5] = deltai*3+5;
- relvars[6] = i*3;
- relvars[7] = i*3+1;
- relvars[8] = i*3+2;
- relvars[9] = i*3+3;
- relvars[10] = i*3+4;
- relvars[11] = i*3+5;
+ //Targagent Targbox -> Targagent Targbox
+ //(1 1 1 1 0 0 1 1 0 0 0 0)
+ //or
+ //(1 1 0 0 0 0 1 1 1 1 0 0)
relvarset = sylvan_set_fromarray(relvars, 12);
- rel_enc[0] = 1;
- rel_enc[1] = 1;
- rel_enc[2] = 0;
- rel_enc[3] = 0;
- rel_enc[4] = 0;
- rel_enc[5] = 0;
- rel_enc[6] = 1;
- rel_enc[7] = 1;
- rel_enc[8] = 1;
- rel_enc[9] = 1;
- rel_enc[10] = 0;
- rel_enc[11] = 0;
+ if (i*6 < deltai){
+ uint8_t rel_enc8[12] = {1, 1, 1, 1, 0, 0, 1, 1, 0, 0, 0, 0};
+ memcpy(rel_enc, rel_enc8, 12*sizeof(uint8_t));
+ }
+ else {
+ uint8_t rel_enc8[12] = {1, 1, 0, 0, 0, 0, 1, 1, 1, 1, 0, 0};
+ memcpy(rel_enc, rel_enc8, 12*sizeof(uint8_t));
+ }
trs_current = (trans_t *)malloc(sizeof(trans_t));
trs_current->bdd = sylvan_cube(relvarset, rel_enc);
trs_current->varset.varset = relvarset;
trs_current->next_rel = trs;
trs = trs_current;
+
}
- else if (check_space(x, y, dir, 1, bm) == 1 && check_space(x, y, dir, 2, bm) == 1){
+ else if (check_space(x, y, dir, 1, bm) == 1 && check_space(x, y, dir, 2, bm) == 1){
xy_bddvar_map *bddvar = getxy(x + xdelta, y + ydelta, bm->f);
- int deltai = bddvar->value.var[0];
+ unsigned int deltai = bddvar->value.var[0];
bddvar = getxy(x + xgamma, y + ygamma, bm->f);
- int gammai = bddvar->value.var[0];
-
- //Free Agent -> 1 0 1 0 0 1 Agent Free
- //(0 1 0 0 1 1 1 0 0 0 1 1)
- 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};
+ unsigned int gammai = bddvar->value.var[0];
+ //Agent Free -> Free Agent
+ //(1 0 0 0 1 1 0 1 0 0 1 1)
+ //or
+ //(0 1 0 0 1 1 1 0 0 0 1 1)
+ 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};
BDDSET relvarset = sylvan_set_fromarray(relvars, 12);
- uint8_t rel_enc[12] = {0, 1, 0, 0, 1, 1, 1, 0, 0, 0, 1, 1};
+ uint8_t rel_enc[12];
+ if (i*6 < deltai){
+ uint8_t rel_enc_[12] = {1, 0, 0, 0, 1, 1, 0, 1, 0, 0, 1, 1};
+ memcpy(rel_enc, rel_enc_, 12*sizeof(uint8_t));
+ }
+ else {
+ uint8_t rel_enc_[12] = {0, 1, 0, 0, 1, 1, 1, 0, 0, 0, 1, 1};
+ memcpy(rel_enc, rel_enc_, 12*sizeof(uint8_t));
+ }
trs_current = (trans_t *)malloc(sizeof(trans_t));
trs_current->bdd = sylvan_cube(relvarset, rel_enc);
trs_current->varset.varset = relvarset;
trs_current->next_rel = trs;
trs = trs_current;
- //Target Agent -> Targagent Free
- //(0 1 1 1 1 0 1 0 0 0 1 1)
- relvars[0] = deltai*3;
- relvars[1] = deltai*3+1;
- relvars[2] = deltai*3+2;
- relvars[3] = deltai*3+3;
- relvars[4] = deltai*3+4;
- relvars[5] = deltai*3+5;
- relvars[6] = i*3;
- relvars[7] = i*3+1;
- relvars[8] = i*3+2;
- relvars[9] = i*3+3;
- relvars[10] = i*3+4;
- relvars[11] = i*3+5;
+ //Agent Target -> Free Targagent
+ //(1 0 0 0 1 1 0 1 1 1 1 0)
+ //or
+ //(0 1 1 1 1 0 1 0 0 0 1 1)
relvarset = sylvan_set_fromarray(relvars, 12);
- rel_enc[0] = 0;
- rel_enc[1] = 1;
- rel_enc[2] = 1;
- rel_enc[3] = 1;
- rel_enc[4] = 1;
- rel_enc[5] = 0;
- rel_enc[6] = 1;
- rel_enc[7] = 0;
- rel_enc[8] = 0;
- rel_enc[9] = 0;
- rel_enc[10] = 1;
- rel_enc[11] = 1;
+ if (i*6 < deltai){
+ uint8_t rel_enc9[12] = {1, 0, 0, 0, 1, 1, 0, 1, 1, 1, 1, 0};
+ memcpy(rel_enc, rel_enc9, 12*sizeof(uint8_t));
+ }
+ else {
+ uint8_t rel_enc9[12] = {0, 1, 1, 1, 1, 0, 1, 0, 0, 0, 1, 1};
+ memcpy(rel_enc, rel_enc9, 12*sizeof(uint8_t));
+ }
trs_current = (trans_t *)malloc(sizeof(trans_t));
trs_current->bdd = sylvan_cube(relvarset, rel_enc);
trs_current->varset.varset = relvarset;
trs_current->next_rel = trs;
trs = trs_current;
- //Free Targagent -> Agent Target
- //(0 1 0 0 1 1 1 0 1 1 0 1)
- relvars[0] = deltai*3;
- relvars[1] = deltai*3+1;
- relvars[2] = deltai*3+2;
- relvars[3] = deltai*3+3;
- relvars[4] = deltai*3+4;
- relvars[5] = deltai*3+5;
- relvars[6] = i*3;
- relvars[7] = i*3+1;
- relvars[8] = i*3+2;
- relvars[9] = i*3+3;
- relvars[10] = i*3+4;
- relvars[11] = i*3+5;
+ //Targagent Free -> Target Agent (LEFT || UP)
+ //(1 0 1 1 0 1 0 1 0 0 1 1)
+ //or
+ //(0 1 0 0 1 1 1 0 1 1 0 1)
relvarset = sylvan_set_fromarray(relvars, 12);
- rel_enc[0] = 0;
- rel_enc[1] = 1;
- rel_enc[2] = 0;
- rel_enc[3] = 0;
- rel_enc[4] = 1;
- rel_enc[5] = 1;
- rel_enc[6] = 1;
- rel_enc[7] = 0;
- rel_enc[8] = 1;
- rel_enc[9] = 1;
- rel_enc[10] = 0;
- rel_enc[11] = 1;
+ if (i*6 < deltai){
+ uint8_t rel_enc10[12] = {1, 0, 1, 1, 0, 1, 0, 1, 0, 0, 1, 1};
+ memcpy(rel_enc, rel_enc10, 12*sizeof(uint8_t));
+ }
+ else {
+ uint8_t rel_enc10[12] = {0, 1, 0, 0, 1, 1, 1, 0, 1, 1, 0, 1};
+ memcpy(rel_enc, rel_enc10, 12*sizeof(uint8_t));
+ }
trs_current = (trans_t *)malloc(sizeof(trans_t));
trs_current->bdd = sylvan_cube(relvarset, rel_enc);
trs_current->varset.varset = relvarset;
trs_current->next_rel = trs;
trs = trs_current;
- //Target Targagent -> Targagent Target
- //(0 1 1 1 1 0 1 0 1 1 0 1)
- relvars[0] = deltai*3;
- relvars[1] = deltai*3+1;
- relvars[2] = deltai*3+2;
- relvars[3] = deltai*3+3;
- relvars[4] = deltai*3+4;
- relvars[5] = deltai*3+5;
- relvars[6] = i*3;
- relvars[7] = i*3+1;
- relvars[8] = i*3+2;
- relvars[9] = i*3+3;
- relvars[10] = i*3+4;
- relvars[11] = i*3+5;
+ //Targagent Target -> Target Targagent (LEFT || UP)
+ //(1 0 1 1 0 1 0 1 1 1 1 0)
+ //or
+ //(0 1 1 1 1 0 1 0 1 1 0 1)
relvarset = sylvan_set_fromarray(relvars, 12);
- rel_enc[0] = 0;
- rel_enc[1] = 1;
- rel_enc[2] = 1;
- rel_enc[3] = 1;
- rel_enc[4] = 1;
- rel_enc[5] = 0;
- rel_enc[6] = 1;
- rel_enc[7] = 0;
- rel_enc[8] = 1;
- rel_enc[9] = 1;
- rel_enc[10] = 0;
- rel_enc[11] = 1;
+ if (i*6 < deltai){
+ uint8_t rel_enc11[12] = {1, 0, 1, 1, 0, 1, 0, 1, 1, 1, 1, 0};
+ memcpy(rel_enc, rel_enc11, 12*sizeof(uint8_t));
+ }
+ else {
+ uint8_t rel_enc11[12] = {0, 1, 1, 1, 1, 0, 1, 0, 1, 1, 0, 1};
+ memcpy(rel_enc, rel_enc11, 12*sizeof(uint8_t));
+ }
trs_current = (trans_t *)malloc(sizeof(trans_t));
trs_current->bdd = sylvan_cube(relvarset, rel_enc);
trs_current->varset.varset = relvarset;
trs_current->next_rel = trs;
trs = trs_current;
- //Box Box Agent -> Box Box Agent
- //(0 0 1 1 0 0 0 0 1 1 0 0 1 1 0 0 1 1)
- 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};
- relvars1[0] = gammai*3;
- relvars1[1] = gammai*3+1;
- relvars1[2] = gammai*3+2;
- relvars1[3] = gammai*3+3;
- relvars1[4] = gammai*3+4;
- relvars1[5] = gammai*3+5;
- relvars1[6] = deltai*3;
- relvars1[7] = deltai*3+1;
- relvars1[8] = deltai*3+2;
- relvars1[9] = deltai*3+3;
- relvars1[10] = deltai*3+4;
- relvars1[11] = deltai*3+5;
- relvars1[12] = i*3;
- relvars1[13] = i*3+1;
- relvars1[14] = i*3+2;
- relvars1[15] = i*3+3;
- relvars1[16] = i*3+4;
- relvars1[17] = i*3+5;
+ //Agent Box Box -> Agent Box Box
+ //(1 1 0 0 1 1 0 0 1 1 0 0 0 0 1 1 0 0 (i delta gamma)
+ //or
+ //(0 0 1 1 0 0 0 0 1 1 0 0 1 1 0 0 1 1) (delta gamma i)
+ //or
+ //(0 0 1 1 0 0 1 1 0 0 1 1 0 0 1 1 0 0) (gamma i delta)
+ //or
+ //(1 1 0 0 1 1 0 0 1 1 0 0 0 0 1 1 0 0) (i gamma delta)
+ //or
+ //(0 0 1 1 0 0 1 1 0 0 1 1 0 0 1 1 0 0) (delta i gamma)
+ //or
+ //(0 0 1 1 0 0 0 0 1 1 0 0 1 1 0 0 1 1) (gamma delta i)
+ 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};
BDD relvarset1 = sylvan_set_fromarray(relvars1, 18);
uint8_t rel_enc1[18];
- //(0 0 1 1 0 0 0 0 1 1 0 0 1 1 0 0 1 1)
- rel_enc1[0] = 0;
- rel_enc1[1] = 0;
- rel_enc1[2] = 1;
- rel_enc1[3] = 1;
- rel_enc1[4] = 0;
- rel_enc1[5] = 0;
- rel_enc1[6] = 0;
- rel_enc1[7] = 0;
- rel_enc1[8] = 1;
- rel_enc1[9] = 1;
- rel_enc1[10] = 0;
- rel_enc1[11] = 0;
- rel_enc1[12] = 1;
- rel_enc1[13] = 1;
- rel_enc1[14] = 0;
- rel_enc1[15] = 0;
- rel_enc1[16] = 1;
- rel_enc1[17] = 1;
+ if (i*6 < deltai && deltai < gammai){
+ uint8_t rel_enc__[18] = {1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0};
+ memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
+ }
+ else if (deltai < gammai && gammai < i*6){
+ uint8_t rel_enc__[18] = {0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1};
+ memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
+ }
+ else if (gammai < i*6 && i*6 < deltai){
+ uint8_t rel_enc__[18] = {0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0};
+ memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
+ }
+ else if (i*6 < gammai && gammai < deltai){
+ uint8_t rel_enc__[18] = {1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0};
+ memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
+ }
+ else if (deltai < i*6 && i*6 < gammai){
+ uint8_t rel_enc__[18] = {0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0};
+ memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
+ }
+ else {
+ uint8_t rel_enc__[18] = {0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1};
+ memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
+ }
+
trs_current = (trans_t *)malloc(sizeof(trans_t));
trs_current->bdd = sylvan_cube(relvarset1, rel_enc1);
trs_current->varset.varset = relvarset1;
trs_current->next_rel = trs;
trs = trs_current;
- //Targbox Box Agent -> Targbox Box Agent
- //(1 1 0 0 0 0 0 0 1 1 0 0 1 1 0 0 1 1)
- relvars1[0] = gammai*3;
- relvars1[1] = gammai*3+1;
- relvars1[2] = gammai*3+2;
- relvars1[3] = gammai*3+3;
- relvars1[4] = gammai*3+4;
- relvars1[5] = gammai*3+5;
- relvars1[6] = deltai*3;
- relvars1[7] = deltai*3+1;
- relvars1[8] = deltai*3+2;
- relvars1[9] = deltai*3+3;
- relvars1[10] = deltai*3+4;
- relvars1[11] = deltai*3+5;
- relvars1[12] = i*3;
- relvars1[13] = i*3+1;
- relvars1[14] = i*3+2;
- relvars1[15] = i*3+3;
- relvars1[16] = i*3+4;
- relvars1[17] = i*3+5;
+ //Agent Box Targbox -> Agent Box Targbox (LEFT || UP)
+ //(1 1 0 0 1 1 0 0 1 1 0 0 1 1 0 0 0 0) (i delta gamma)
+ //or
+ //(0 0 1 1 0 0 1 1 0 0 0 0 1 1 0 0 1 1) (delta gamma i)
+ //or
+ //(1 1 0 0 0 0 1 1 0 0 1 1 0 0 1 1 0 0) (gamma i delta)
+ //or
+ //(1 1 0 0 1 1 1 1 0 0 0 0 0 0 1 1 0 0) (i gamma delta)
+ //or
+ //(0 0 1 1 0 0 1 1 0 0 1 1 1 1 0 0 0 0) (delta i gamma)
+ //or
+ //(1 1 0 0 0 0 0 0 1 1 0 0 1 1 0 0 1 1) (gamma delta i)
relvarset1 = sylvan_set_fromarray(relvars1, 18);
- //(1 1 0 0 0 0 0 0 1 1 0 0 1 1 0 0 1 1)
- rel_enc1[0] = 1;
- rel_enc1[1] = 1;
- rel_enc1[2] = 0;
- rel_enc1[3] = 0;
- rel_enc1[4] = 0;
- rel_enc1[5] = 0;
- rel_enc1[6] = 0;
- rel_enc1[7] = 0;
- rel_enc1[8] = 1;
- rel_enc1[9] = 1;
- rel_enc1[10] = 0;
- rel_enc1[11] = 0;
- rel_enc1[12] = 1;
- rel_enc1[13] = 1;
- rel_enc1[14] = 0;
- rel_enc1[15] = 0;
- rel_enc1[16] = 1;
- rel_enc1[17] = 1;
+ if (i*6 < deltai && deltai < gammai){
+ uint8_t rel_enc__[18] = {1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 0};
+ memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
+ }
+ else if (deltai < gammai && gammai < i*6){
+ uint8_t rel_enc__[18] = {0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1};
+ memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
+ }
+ else if (gammai < i*6 && i*6 < deltai){
+ uint8_t rel_enc__[18] = {1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0};
+ memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
+ }
+ else if (i*6 < gammai && gammai < deltai){
+ uint8_t rel_enc__[18] = {1, 1, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0};
+ memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
+ }
+ else if (deltai < i*6 && i*6 < gammai){
+ uint8_t rel_enc__[18] = {0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0};
+ memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
+ }
+ else {
+ uint8_t rel_enc__[18] = {1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1};
+ memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
+ }
trs_current = (trans_t *)malloc(sizeof(trans_t));
trs_current->bdd = sylvan_cube(relvarset1, rel_enc1);
trs_current->varset.varset = relvarset1;
trs_current->next_rel = trs;
trs = trs_current;
- //Box Box Targagent -> Box Box Targagent
- //(0 0 1 1 0 0 0 0 1 1 0 0 1 1 1 1 0 0)
- relvars1[0] = gammai*3;
- relvars1[1] = gammai*3+1;
- relvars1[2] = gammai*3+2;
- relvars1[3] = gammai*3+3;
- relvars1[4] = gammai*3+4;
- relvars1[5] = gammai*3+5;
- relvars1[6] = deltai*3;
- relvars1[7] = deltai*3+1;
- relvars1[8] = deltai*3+2;
- relvars1[9] = deltai*3+3;
- relvars1[10] = deltai*3+4;
- relvars1[11] = deltai*3+5;
- relvars1[12] = i*3;
- relvars1[13] = i*3+1;
- relvars1[14] = i*3+2;
- relvars1[15] = i*3+3;
- relvars1[16] = i*3+4;
- relvars1[17] = i*3+5;
+ //Targagent Box Box -> Targagent Box Box
+ //(1 1 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0)
+ //or
+ //(0 0 1 1 0 0 0 0 1 1 0 0 1 1 1 1 0 0)
+ //or
+ //(0 0 1 1 0 0 1 1 1 1 0 0 0 0 1 1 0 0)
+ //or
+ //(1 1 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0)
+ //or
+ //(0 0 1 1 0 0 1 1 1 1 0 0 0 0 1 1 0 0)
+ //or
+ //(0 0 1 1 0 0 0 0 1 1 0 0 1 1 1 1 0 0)
relvarset1 = sylvan_set_fromarray(relvars1, 18);
- //(0 0 1 1 0 0 0 0 1 1 0 0 1 1 1 1 0 0)
- rel_enc1[0] = 0;
- rel_enc1[1] = 0;
- rel_enc1[2] = 1;
- rel_enc1[3] = 1;
- rel_enc1[4] = 0;
- rel_enc1[5] = 0;
- rel_enc1[6] = 0;
- rel_enc1[7] = 0;
- rel_enc1[8] = 1;
- rel_enc1[9] = 1;
- rel_enc1[10] = 0;
- rel_enc1[11] = 0;
- rel_enc1[12] = 1;
- rel_enc1[13] = 1;
- rel_enc1[14] = 1;
- rel_enc1[15] = 1;
- rel_enc1[16] = 0;
- rel_enc1[17] = 0;
+ if (i*6 < deltai && deltai < gammai){
+ uint8_t rel_enc__[18] = {1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0};
+ memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
+ }
+ else if (deltai < gammai && gammai < i*6){
+ uint8_t rel_enc__[18] = {0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 1, 1, 0, 0};
+ memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
+ }
+ else if (gammai < i*6 && i*6 < deltai){
+ uint8_t rel_enc__[18] = {0, 0, 1, 1, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0};
+ memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
+ }
+ else if (i*6 < gammai && gammai < deltai){
+ uint8_t rel_enc__[18] = {1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0};
+ memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
+ }
+ else if (deltai < i*6 && i*6 < gammai){
+ uint8_t rel_enc__[18] = {0, 0, 1, 1, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0};
+ memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
+ }
+ else {
+ uint8_t rel_enc__[18] = {0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 1, 1, 0, 0};
+ memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
+ }
trs_current = (trans_t *)malloc(sizeof(trans_t));
trs_current->bdd = sylvan_cube(relvarset1, rel_enc1);
trs_current->varset.varset = relvarset1;
trs_current->next_rel = trs;
trs = trs_current;
- //Targbox Box Targagent -> Targbox Box Targagent
- //(1 1 0 0 0 0 0 0 1 1 0 0 1 1 1 1 0 0)
- relvars1[0] = gammai*3;
- relvars1[1] = gammai*3+1;
- relvars1[2] = gammai*3+2;
- relvars1[3] = gammai*3+3;
- relvars1[4] = gammai*3+4;
- relvars1[5] = gammai*3+5;
- relvars1[6] = deltai*3;
- relvars1[7] = deltai*3+1;
- relvars1[8] = deltai*3+2;
- relvars1[9] = deltai*3+3;
- relvars1[10] = deltai*3+4;
- relvars1[11] = deltai*3+5;
- relvars1[12] = i*3;
- relvars1[13] = i*3+1;
- relvars1[14] = i*3+2;
- relvars1[15] = i*3+3;
- relvars1[16] = i*3+4;
- relvars1[17] = i*3+5;
+ //Targagent Box Targbox -> Targagent Box Targbox (LEFT || UP)
+ //(1 1 1 1 0 0 0 0 1 1 0 0 1 1 0 0 0 0)
+ //or
+ //(0 0 1 1 0 0 1 1 0 0 0 0 1 1 1 1 0 0)
+ //or
+ //(1 1 0 0 0 0 1 1 1 1 0 0 0 0 1 1 0 0)
+ //or
+ //(1 1 1 1 0 0 1 1 0 0 0 0 0 0 1 1 0 0)
+ //or
+ //(0 0 1 1 0 0 1 1 1 1 0 0 1 1 0 0 0 0)
+ //or
+ //(1 1 0 0 0 0 0 0 1 1 0 0 1 1 1 1 0 0)
relvarset1 = sylvan_set_fromarray(relvars1, 18);
- //(1 1 0 0 0 0 0 0 1 1 0 0 1 1 1 1 0 0)
- rel_enc1[0] = 1;
- rel_enc1[1] = 1;
- rel_enc1[2] = 0;
- rel_enc1[3] = 0;
- rel_enc1[4] = 0;
- rel_enc1[5] = 0;
- rel_enc1[6] = 0;
- rel_enc1[7] = 0;
- rel_enc1[8] = 1;
- rel_enc1[9] = 1;
- rel_enc1[10] = 0;
- rel_enc1[11] = 0;
- rel_enc1[12] = 1;
- rel_enc1[13] = 1;
- rel_enc1[14] = 1;
- rel_enc1[15] = 1;
- rel_enc1[16] = 0;
- rel_enc1[17] = 0;
+ if (i*6 < deltai && deltai < gammai){
+ uint8_t rel_enc__[18] = {1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 0};
+ memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
+ }
+ else if (deltai < gammai && gammai < i*6){
+ uint8_t rel_enc__[18] = {0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 1, 1, 0, 0};
+ memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
+ }
+ else if (gammai < i*6 && i*6 < deltai){
+ uint8_t rel_enc__[18] = {1, 1, 0, 0, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0};
+ memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
+ }
+ else if (i*6 < gammai && gammai < deltai){
+ uint8_t rel_enc__[18] = {1, 1, 1, 1, 0, 0, 1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0};
+ memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
+ }
+ else if (deltai < i*6 && i*6 < gammai){
+ uint8_t rel_enc__[18] = {0, 0, 1, 1, 0, 0, 1, 1, 1, 1, 0, 0, 1, 1, 0, 0, 0, 0};
+ memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
+ }
+ else {
+ uint8_t rel_enc__[18] = {1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 1, 1, 0, 0};
+ memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
+ }
trs_current = (trans_t *)malloc(sizeof(trans_t));
trs_current->bdd = sylvan_cube(relvarset1, rel_enc1);
trs_current->varset.varset = relvarset1;
trs_current->next_rel = trs;
trs = trs_current;
- //Free Box Agent -> Box Agent Free
- //(0 0 0 1 1 0 0 1 1 0 0 1 1 0 0 0 1 1)
- relvars1[0] = gammai*3;
- relvars1[1] = gammai*3+1;
- relvars1[2] = gammai*3+2;
- relvars1[3] = gammai*3+3;
- relvars1[4] = gammai*3+4;
- relvars1[5] = gammai*3+5;
- relvars1[6] = deltai*3;
- relvars1[7] = deltai*3+1;
- relvars1[8] = deltai*3+2;
- relvars1[9] = deltai*3+3;
- relvars1[10] = deltai*3+4;
- relvars1[11] = deltai*3+5;
- relvars1[12] = i*3;
- relvars1[13] = i*3+1;
- relvars1[14] = i*3+2;
- relvars1[15] = i*3+3;
- relvars1[16] = i*3+4;
- relvars1[17] = i*3+5;
+ //Agent Box Free -> Free Agent Box
+ //(1 0 0 0 1 1 0 1 1 0 0 1 0 0 0 1 1 0)
+ //or
+ //(0 1 1 0 0 1 0 0 0 1 1 0 1 0 0 0 1 1)
+ //or
+ //(0 0 0 1 1 0 1 0 0 0 1 1 0 1 1 0 0 1)
+ //or
+ //(1 0 0 0 1 1 0 0 0 1 1 0 0 1 1 0 0 1)
+ //or
+ //(0 1 1 0 0 1 1 0 0 0 1 1 0 0 0 1 1 0)
+ //or
+ //(0 0 0 1 1 0 0 1 1 0 0 1 1 0 0 0 1 1)
relvarset1 = sylvan_set_fromarray(relvars1, 18);
- //(0 0 0 1 1 0 0 1 1 0 0 1 1 0 0 0 1 1)
- rel_enc1[0] = 0;
- rel_enc1[1] = 0;
- rel_enc1[2] = 0;
- rel_enc1[3] = 1;
- rel_enc1[4] = 1;
- rel_enc1[5] = 0;
- rel_enc1[6] = 0;
- rel_enc1[7] = 1;
- rel_enc1[8] = 1;
- rel_enc1[9] = 0;
- rel_enc1[10] = 0;
- rel_enc1[11] = 1;
- rel_enc1[12] = 1;
- rel_enc1[13] = 0;
- rel_enc1[14] = 0;
- rel_enc1[15] = 0;
- rel_enc1[16] = 1;
- rel_enc1[17] = 1;
+ if (i*6 < deltai && deltai < gammai){
+ uint8_t rel_enc__[18] = {1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 0, 1, 0, 0, 0, 1, 1, 0};
+ memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
+ }
+
+ else if (deltai < gammai && gammai < i*6){
+ uint8_t rel_enc__[18] = {0, 1, 1, 0, 0, 1, 0, 0, 0, 1, 1, 0, 1, 0, 0, 0, 1, 1};
+ memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
+ }
+
+ else if (gammai < i*6 && i*6 < deltai){
+ uint8_t rel_enc__[18] = {0, 0, 0, 1, 1, 0, 1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 0, 1};
+ memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
+ }
+
+ else if (i*6 < gammai && gammai < deltai){
+ uint8_t rel_enc__[18] = {1, 0, 0, 0, 1, 1, 0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1};
+ memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
+ }
+ else if (deltai < i*6 && i*6 < gammai){
+ uint8_t rel_enc__[18] = {0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 1, 1, 0, 0, 0, 1, 1, 0};
+ memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
+ }
+ else {
+ uint8_t rel_enc__[18] = {0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 1, 1};
+ memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
+ }
+
trs_current = (trans_t *)malloc(sizeof(trans_t));
+
trs_current->bdd = sylvan_cube(relvarset1, rel_enc1);
trs_current->varset.varset = relvarset1;
trs_current->varset.size = 18;
trs_current->next_rel = trs;
trs = trs_current;
- //Free Targbox Agent -> Box Targagent Free
- //(0 0 0 1 1 0 1 1 0 1 0 0 1 0 0 0 1 1)
- relvars1[0] = gammai*3;
- relvars1[1] = gammai*3+1;
- relvars1[2] = gammai*3+2;
- relvars1[3] = gammai*3+3;
- relvars1[4] = gammai*3+4;
- relvars1[5] = gammai*3+5;
- relvars1[6] = deltai*3;
- relvars1[7] = deltai*3+1;
- relvars1[8] = deltai*3+2;
- relvars1[9] = deltai*3+3;
- relvars1[10] = deltai*3+4;
- relvars1[11] = deltai*3+5;
- relvars1[12] = i*3;
- relvars1[13] = i*3+1;
- relvars1[14] = i*3+2;
- relvars1[15] = i*3+3;
- relvars1[16] = i*3+4;
- relvars1[17] = i*3+5;
+ //Agent Targbox Free -> Free Targagent Box
+ //(1 0 0 0 1 1 1 1 0 1 0 0 0 0 0 1 1 0)
+ //or
+ //(1 1 0 1 0 0 0 0 0 1 1 0 1 0 0 0 1 1)
+ //or
+ //(0 0 0 1 1 0 1 0 0 0 1 1 1 1 0 1 0 0)
+ //or
+ //(1 0 0 0 1 1 0 0 0 1 1 0 1 1 0 1 0 0)
+ //or
+ //(1 1 0 1 0 0 1 0 0 0 1 1 0 0 0 1 1 0)
+ //or
+ //(0 0 0 1 1 0 1 1 0 1 0 0 1 0 0 0 1 1)
relvarset1 = sylvan_set_fromarray(relvars1, 18);
- //(0 0 0 1 1 0 1 1 0 1 0 0 1 0 0 0 1 1)
- rel_enc1[0] = 0;
- rel_enc1[1] = 0;
- rel_enc1[2] = 0;
- rel_enc1[3] = 1;
- rel_enc1[4] = 1;
- rel_enc1[5] = 0;
- rel_enc1[6] = 1;
- rel_enc1[7] = 1;
- rel_enc1[8] = 0;
- rel_enc1[9] = 1;
- rel_enc1[10] = 0;
- rel_enc1[11] = 0;
- rel_enc1[12] = 1;
- rel_enc1[13] = 0;
- rel_enc1[14] = 0;
- rel_enc1[15] = 0;
- rel_enc1[16] = 1;
- rel_enc1[17] = 1;
+ if (i*6 < deltai && deltai < gammai){
+ uint8_t rel_enc__[18] = {1, 0, 0, 0, 1, 1, 1, 1, 0, 1, 0, 0, 0, 0, 0, 1, 1, 0};
+ memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
+ }
+ else if (deltai < gammai && gammai < i*6){
+ uint8_t rel_enc__[18] = {1, 1, 0, 1, 0, 0, 0, 0, 0, 1, 1, 0, 1, 0, 0, 0, 1, 1};
+ memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
+ }
+ else if (gammai < i*6 && i*6 < deltai){
+ uint8_t rel_enc__[18] = {0, 0, 0, 1, 1, 0, 1, 0, 0, 0, 1, 1, 1, 1, 0, 1, 0, 0};
+ memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
+ }
+ else if (i*6 < gammai && gammai < deltai){
+ uint8_t rel_enc__[18] = {1, 0, 0, 0, 1, 1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0, 0};
+ memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
+ }
+ else if (deltai < i*6 && i*6 < gammai){
+ uint8_t rel_enc__[18] = {1, 1, 0, 1, 0, 0, 1, 0, 0, 0, 1, 1, 0, 0, 0, 1, 1, 0};
+ memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
+ }
+ else {
+ uint8_t rel_enc__[18] = {0, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0, 0, 1, 0, 0, 0, 1, 1};
+ memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
+ }
trs_current = (trans_t *)malloc(sizeof(trans_t));
trs_current->bdd = sylvan_cube(relvarset1, rel_enc1);
trs_current->varset.varset = relvarset1;
trs_current->next_rel = trs;
trs = trs_current;
- //Target Box Agent -> Targbox Agent Free
- //(0 1 1 0 1 0 0 1 1 0 0 1 1 0 0 0 1 1)
- relvars1[0] = gammai*3;
- relvars1[1] = gammai*3+1;
- relvars1[2] = gammai*3+2;
- relvars1[3] = gammai*3+3;
- relvars1[4] = gammai*3+4;
- relvars1[5] = gammai*3+5;
- relvars1[6] = deltai*3;
- relvars1[7] = deltai*3+1;
- relvars1[8] = deltai*3+2;
- relvars1[9] = deltai*3+3;
- relvars1[10] = deltai*3+4;
- relvars1[11] = deltai*3+5;
- relvars1[12] = i*3;
- relvars1[13] = i*3+1;
- relvars1[14] = i*3+2;
- relvars1[15] = i*3+3;
- relvars1[16] = i*3+4;
- relvars1[17] = i*3+5;
+ //Agent Box Target -> Free Agent Targbox
+ //(1 0 0 0 1 1 0 1 1 0 0 1 0 1 1 0 1 0)
+ //or
+ //(0 1 1 0 0 1 0 1 1 0 1 0 1 0 0 0 1 1)
+ //or
+ //(0 1 1 0 1 0 1 0 0 0 1 1 0 1 1 0 0 1)
+ //or
+ //(1 0 0 0 1 1 0 1 1 0 1 0 0 1 1 0 0 1)
+ //or
+ //(0 1 1 0 0 1 1 0 0 0 1 1 0 1 1 0 1 0)
+ //or
+ //(0 1 1 0 1 0 0 1 1 0 0 1 1 0 0 0 1 1)
relvarset1 = sylvan_set_fromarray(relvars1, 18);
- //(0 1 1 0 1 0 0 1 1 0 0 1 1 0 0 0 1 1)
- rel_enc1[0] = 0;
- rel_enc1[1] = 1;
- rel_enc1[2] = 1;
- rel_enc1[3] = 0;
- rel_enc1[4] = 1;
- rel_enc1[5] = 0;
- rel_enc1[6] = 0;
- rel_enc1[7] = 1;
- rel_enc1[8] = 1;
- rel_enc1[9] = 0;
- rel_enc1[10] = 0;
- rel_enc1[11] = 1;
- rel_enc1[12] = 1;
- rel_enc1[13] = 0;
- rel_enc1[14] = 0;
- rel_enc1[15] = 0;
- rel_enc1[16] = 1;
- rel_enc1[17] = 1;
+ if (i*6 < deltai && deltai < gammai){
+ uint8_t rel_enc__[18] = {1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 0, 1, 0, 1, 1, 0, 1, 0};
+ memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
+ }
+ else if (deltai < gammai && gammai < i*6){
+ uint8_t rel_enc__[18] = {0, 1, 1, 0, 0, 1, 0, 1, 1, 0, 1, 0, 1, 0, 0, 0, 1, 1};
+ memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
+ }
+ else if (gammai < i*6 && i*6 < deltai){
+ uint8_t rel_enc__[18] = {0, 1, 1, 0, 1, 0, 1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 0, 1};
+ memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
+ }
+ else if (i*6 < gammai && gammai < deltai){
+ uint8_t rel_enc__[18] = {1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0, 0, 1, 1, 0, 0, 1};
+ memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
+ }
+ else if (deltai < i*6 && i*6 < gammai){
+ uint8_t rel_enc__[18] = {0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0};
+ memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
+ }
+ else {
+ uint8_t rel_enc__[18] = {0, 1, 1, 0, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 1, 1};
+ memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
+ }
trs_current = (trans_t *)malloc(sizeof(trans_t));
trs_current->bdd = sylvan_cube(relvarset1, rel_enc1);
trs_current->varset.varset = relvarset1;
trs_current->next_rel = trs;
trs = trs_current;
- //Target Targbox Agent -> Targbox Targagent Free
- //(0 1 1 0 1 0 1 1 0 1 0 0 1 0 0 0 1 1)
- relvars1[0] = gammai*3;
- relvars1[1] = gammai*3+1;
- relvars1[2] = gammai*3+2;
- relvars1[3] = gammai*3+3;
- relvars1[4] = gammai*3+4;
- relvars1[5] = gammai*3+5;
- relvars1[6] = deltai*3;
- relvars1[7] = deltai*3+1;
- relvars1[8] = deltai*3+2;
- relvars1[9] = deltai*3+3;
- relvars1[10] = deltai*3+4;
- relvars1[11] = deltai*3+5;
- relvars1[12] = i*3;
- relvars1[13] = i*3+1;
- relvars1[14] = i*3+2;
- relvars1[15] = i*3+3;
- relvars1[16] = i*3+4;
- relvars1[17] = i*3+5;
+ //Agent Targbox Target -> Free Targagent Targbox
+ //(1 0 0 0 1 1 1 1 0 1 0 0 0 1 1 0 1 0)
+ //or
+ //(1 1 0 1 0 0 0 1 1 0 1 0 1 0 0 0 1 1)
+ //or
+ //(0 1 1 0 1 0 1 0 0 0 1 1 1 1 0 1 0 0)
+ //or
+ //(1 0 0 0 1 1 0 1 1 0 1 0 1 1 0 1 0 0)
+ //or
+ //(1 1 0 1 0 0 1 0 0 0 1 1 0 1 1 0 1 0)
+ //or
+ //(0 1 1 0 1 0 1 1 0 1 0 0 1 0 0 0 1 1)
relvarset1 = sylvan_set_fromarray(relvars1, 18);
- //(0 1 1 0 1 0 1 1 0 1 0 0 1 0 0 0 1 1)
- rel_enc1[0] = 0;
- rel_enc1[1] = 1;
- rel_enc1[2] = 1;
- rel_enc1[3] = 0;
- rel_enc1[4] = 1;
- rel_enc1[5] = 0;
- rel_enc1[6] = 1;
- rel_enc1[7] = 1;
- rel_enc1[8] = 0;
- rel_enc1[9] = 1;
- rel_enc1[10] = 0;
- rel_enc1[11] = 0;
- rel_enc1[12] = 1;
- rel_enc1[13] = 0;
- rel_enc1[14] = 0;
- rel_enc1[15] = 0;
- rel_enc1[16] = 1;
- rel_enc1[17] = 1;
+ if (i*6 < deltai && deltai < gammai){
+ uint8_t rel_enc__[18] = {1, 0, 0, 0, 1, 1, 1, 1, 0, 1, 0, 0, 0, 1, 1, 0, 1, 0};
+ memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
+ }
+ else if (deltai < gammai && gammai < i*6){
+ uint8_t rel_enc__[18] = {1, 1, 0, 1, 0, 0, 0, 1, 1, 0, 1, 0, 1, 0, 0, 0, 1, 1};
+ memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
+ }
+ else if (gammai < i*6 && i*6 < deltai){
+ uint8_t rel_enc__[18] = {0, 1, 1, 0, 1, 0, 1, 0, 0, 0, 1, 1, 1, 1, 0, 1, 0, 0};
+ memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
+ }
+ else if (i*6 < gammai && gammai < deltai){
+ uint8_t rel_enc__[18] = {1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0, 0};
+ memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
+ }
+ else if (deltai < i*6 && i*6 < gammai){
+ uint8_t rel_enc__[18] = {1, 1, 0, 1, 0, 0, 1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0};
+ memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
+ }
+ else {
+ uint8_t rel_enc__[18] = {0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0, 0, 1, 0, 0, 0, 1, 1};
+ memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
+ }
trs_current = (trans_t *)malloc(sizeof(trans_t));
trs_current->bdd = sylvan_cube(relvarset1, rel_enc1);
trs_current->varset.varset = relvarset1;
trs_current->next_rel = trs;
trs = trs_current;
- //Free Box Targagent -> Box Agent Target
- //(0 0 0 1 1 0 0 1 1 0 0 1 1 0 1 1 0 1)
- relvars1[0] = gammai*3;
- relvars1[1] = gammai*3+1;
- relvars1[2] = gammai*3+2;
- relvars1[3] = gammai*3+3;
- relvars1[4] = gammai*3+4;
- relvars1[5] = gammai*3+5;
- relvars1[6] = deltai*3;
- relvars1[7] = deltai*3+1;
- relvars1[8] = deltai*3+2;
- relvars1[9] = deltai*3+3;
- relvars1[10] = deltai*3+4;
- relvars1[11] = deltai*3+5;
- relvars1[12] = i*3;
- relvars1[13] = i*3+1;
- relvars1[14] = i*3+2;
- relvars1[15] = i*3+3;
- relvars1[16] = i*3+4;
- relvars1[17] = i*3+5;
+ //Targagent Box Free -> Target Agent Box
+ //(1 0 1 1 0 1 0 1 1 0 0 1 0 0 0 1 1 0)
+ //or
+ //(0 1 1 0 0 1 0 0 0 1 1 0 1 0 1 1 0 1)
+ //or
+ //(0 0 0 1 1 0 1 0 1 1 0 1 0 1 1 0 0 1)
+ //or
+ //(1 0 1 1 0 1 0 0 0 1 1 0 0 1 1 0 0 1)
+ //or
+ //(0 1 1 0 0 1 1 0 1 1 0 1 0 0 0 1 1 0)
+ //or
+ //(0 0 0 1 1 0 0 1 1 0 0 1 1 0 1 1 0 1)
relvarset1 = sylvan_set_fromarray(relvars1, 18);
- //(0 0 0 1 1 0 0 1 1 0 0 1 1 0 1 1 0 1)
- rel_enc1[0] = 0;
- rel_enc1[1] = 0;
- rel_enc1[2] = 0;
- rel_enc1[3] = 1;
- rel_enc1[4] = 1;
- rel_enc1[5] = 0;
- rel_enc1[6] = 0;
- rel_enc1[7] = 1;
- rel_enc1[8] = 1;
- rel_enc1[9] = 0;
- rel_enc1[10] = 0;
- rel_enc1[11] = 1;
- rel_enc1[12] = 1;
- rel_enc1[13] = 0;
- rel_enc1[14] = 1;
- rel_enc1[15] = 1;
- rel_enc1[16] = 0;
- rel_enc1[17] = 1;
+ if (i*6 < deltai && deltai < gammai){
+ uint8_t rel_enc__[18] = {1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 0, 1, 0, 0, 0, 1, 1, 0};
+ memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
+ }
+ else if (deltai < gammai && gammai < i*6){
+ uint8_t rel_enc__[18] = {0, 1, 1, 0, 0, 1, 0, 0, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1};
+ memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
+ }
+ else if (gammai < i*6 && i*6 < deltai){
+ uint8_t rel_enc__[18] = {0, 0, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 0, 1};
+ memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
+ }
+ else if (i*6 < gammai && gammai < deltai){
+ uint8_t rel_enc__[18] = {1, 0, 1, 1, 0, 1, 0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1};
+ memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
+ }
+ else if (deltai < i*6 && i*6 < gammai){
+ uint8_t rel_enc__[18] = {0, 1, 1, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0, 0, 0, 1, 1, 0};
+ memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
+ }
+ else {
+ uint8_t rel_enc__[18] = {0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 1, 1, 0, 1};
+ memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
+ }
trs_current = (trans_t *)malloc(sizeof(trans_t));
trs_current->bdd = sylvan_cube(relvarset1, rel_enc1);
trs_current->varset.varset = relvarset1;
trs_current->next_rel = trs;
trs = trs_current;
- //Free Targbox Targagent -> Box Targagent Target
- //(0 0 0 1 1 0 1 1 0 1 0 0 1 0 1 1 0 1)
- relvars1[0] = gammai*3;
- relvars1[1] = gammai*3+1;
- relvars1[2] = gammai*3+2;
- relvars1[3] = gammai*3+3;
- relvars1[4] = gammai*3+4;
- relvars1[5] = gammai*3+5;
- relvars1[6] = deltai*3;
- relvars1[7] = deltai*3+1;
- relvars1[8] = deltai*3+2;
- relvars1[9] = deltai*3+3;
- relvars1[10] = deltai*3+4;
- relvars1[11] = deltai*3+5;
- relvars1[12] = i*3;
- relvars1[13] = i*3+1;
- relvars1[14] = i*3+2;
- relvars1[15] = i*3+3;
- relvars1[16] = i*3+4;
- relvars1[17] = i*3+5;
+ //Targagent Targbox Free -> Target Targagent Box
+ //(1 0 1 1 0 1 1 1 0 1 0 0 0 0 0 1 1 0)
+ //or
+ //(1 1 0 1 0 0 0 0 0 1 1 0 1 0 1 1 0 1)
+ //or
+ //(0 0 0 1 1 0 1 0 1 1 0 1 1 1 0 1 0 0)
+ //or
+ //(1 0 1 1 0 1 0 0 0 1 1 0 1 1 0 1 0 0)
+ //or
+ //(1 1 0 1 0 0 1 0 1 1 0 1 0 0 0 1 1 0)
+ //or
+ //(0 0 0 1 1 0 1 1 0 1 0 0 1 0 1 1 0 1)
relvarset1 = sylvan_set_fromarray(relvars1, 18);
- //(0 0 0 1 1 0 1 1 0 1 0 0 1 0 1 1 0 1)
- rel_enc1[0] = 0;
- rel_enc1[1] = 0;
- rel_enc1[2] = 0;
- rel_enc1[3] = 1;
- rel_enc1[4] = 1;
- rel_enc1[5] = 0;
- rel_enc1[6] = 1;
- rel_enc1[7] = 1;
- rel_enc1[8] = 0;
- rel_enc1[9] = 1;
- rel_enc1[10] = 0;
- rel_enc1[11] = 0;
- rel_enc1[12] = 1;
- rel_enc1[13] = 0;
- rel_enc1[14] = 1;
- rel_enc1[15] = 1;
- rel_enc1[16] = 0;
- rel_enc1[17] = 1;
+ if (i*6 < deltai && deltai < gammai){
+ uint8_t rel_enc__[18] = {1, 0, 1, 1, 0, 1, 1, 1, 0, 1, 0, 0, 0, 0, 0, 1, 1, 0};
+ memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
+ }
+ else if (deltai < gammai && gammai < i*6){
+ uint8_t rel_enc__[18] = {1, 1, 0, 1, 0, 0, 0, 0, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1};
+ memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
+ }
+ else if (gammai < i*6 && i*6 < deltai){
+ uint8_t rel_enc__[18] = {0, 0, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 1, 1, 0, 1, 0, 0};
+ memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
+ }
+ else if (i*6 < gammai && gammai < deltai){
+ uint8_t rel_enc__[18] = {1, 0, 1, 1, 0, 1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0, 0};
+ memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
+ }
+ else if (deltai < i*6 && i*6 < gammai){
+ uint8_t rel_enc__[18] = {1, 1, 0, 1, 0, 0, 1, 0, 1, 1, 0, 1, 0, 0, 0, 1 ,1, 0};
+ memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
+ }
+ else {
+ uint8_t rel_enc__[18] = {0, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0, 0, 1, 0, 1, 1, 0, 1};
+ memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
+ }
trs_current = (trans_t *)malloc(sizeof(trans_t));
trs_current->bdd = sylvan_cube(relvarset1, rel_enc1);
trs_current->varset.varset = relvarset1;
trs_current->next_rel = trs;
trs = trs_current;
- //Target Box Targagent -> Targbox Agent Target
- //(0 1 1 0 1 0 0 1 1 0 0 1 1 0 1 1 0 1)
- relvars1[0] = gammai*3;
- relvars1[1] = gammai*3+1;
- relvars1[2] = gammai*3+2;
- relvars1[3] = gammai*3+3;
- relvars1[4] = gammai*3+4;
- relvars1[5] = gammai*3+5;
- relvars1[6] = deltai*3;
- relvars1[7] = deltai*3+1;
- relvars1[8] = deltai*3+2;
- relvars1[9] = deltai*3+3;
- relvars1[10] = deltai*3+4;
- relvars1[11] = deltai*3+5;
- relvars1[12] = i*3;
- relvars1[13] = i*3+1;
- relvars1[14] = i*3+2;
- relvars1[15] = i*3+3;
- relvars1[16] = i*3+4;
- relvars1[17] = i*3+5;
+ //Targagent Box Target -> Target Agent Targbox
+ //(1 0 1 1 0 1 0 1 1 0 0 1 0 1 1 0 1 0)
+ //or
+ //(0 1 1 0 0 1 0 1 1 0 1 0 1 0 1 1 0 1)
+ //or
+ //(0 1 1 0 1 0 1 0 1 1 0 1 0 1 1 0 0 1)
+ //or
+ //(1 0 1 1 0 1 0 1 1 0 1 0 0 1 1 0 0 1)
+ //or
+ //(0 1 1 0 0 1 1 0 1 1 0 1 0 1 1 0 1 0)
+ //or
+ //(0 1 1 0 1 0 0 1 1 0 0 1 1 0 1 1 0 1)
relvarset1 = sylvan_set_fromarray(relvars1, 18);
- //(0 1 1 0 1 0 0 1 1 0 0 1 1 0 1 1 0 1)
- rel_enc1[0] = 0;
- rel_enc1[1] = 1;
- rel_enc1[2] = 1;
- rel_enc1[3] = 0;
- rel_enc1[4] = 1;
- rel_enc1[5] = 0;
- rel_enc1[6] = 0;
- rel_enc1[7] = 1;
- rel_enc1[8] = 1;
- rel_enc1[9] = 0;
- rel_enc1[10] = 0;
- rel_enc1[11] = 1;
- rel_enc1[12] = 1;
- rel_enc1[13] = 0;
- rel_enc1[14] = 1;
- rel_enc1[15] = 1;
- rel_enc1[16] = 0;
- rel_enc1[17] = 1;
+ if (i*6 < deltai && deltai < gammai){
+ uint8_t rel_enc__[18] = {1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 0, 1, 0, 1, 1, 0, 1, 0};
+ memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
+ }
+ else if (deltai < gammai && gammai < i*6){
+ uint8_t rel_enc__[18] = {0, 1, 1, 0, 0, 1, 0, 1, 1, 0, 1, 0, 1, 0, 1, 1, 0, 1};
+ memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
+ }
+ else if (gammai < i*6 && i*6 < deltai){
+ uint8_t rel_enc__[18] = {0, 1, 1, 0, 1, 0, 1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 0, 1};
+ memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
+ }
+ else if (i*6 < gammai && gammai < deltai){
+ uint8_t rel_enc__[18] = {1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0, 0, 1, 1, 0, 0, 1};
+ memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
+ }
+ else if (deltai < i*6 && i*6 < gammai){
+ uint8_t rel_enc__[18] = {0, 1, 1, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0};
+ memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
+ }
+ else {
+ uint8_t rel_enc__[18] = {0, 1, 1, 0, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 1, 1, 0, 1};
+ memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
+ }
trs_current = (trans_t *)malloc(sizeof(trans_t));
trs_current->bdd = sylvan_cube(relvarset1, rel_enc1);
trs_current->varset.varset = relvarset1;
trs_current->next_rel = trs;
trs = trs_current;
- //Target Targbox Targagent -> Targbox Targagent Target
- //(0 1 1 0 1 0 1 1 0 1 0 0 1 0 1 1 0 1)
- relvars1[0] = gammai*3;
- relvars1[1] = gammai*3+1;
- relvars1[2] = gammai*3+2;
- relvars1[3] = gammai*3+3;
- relvars1[4] = gammai*3+4;
- relvars1[5] = gammai*3+5;
- relvars1[6] = deltai*3;
- relvars1[7] = deltai*3+1;
- relvars1[8] = deltai*3+2;
- relvars1[9] = deltai*3+3;
- relvars1[10] = deltai*3+4;
- relvars1[11] = deltai*3+5;
- relvars1[12] = i*3;
- relvars1[13] = i*3+1;
- relvars1[14] = i*3+2;
- relvars1[15] = i*3+3;
- relvars1[16] = i*3+4;
- relvars1[17] = i*3+5;
+ //Targagent Targbox Target -> Target Targagent Targbox
+ //(1 0 1 1 0 1 1 1 0 1 0 0 0 1 1 0 1 0)
+ //or
+ //(1 1 0 1 0 0 0 1 1 0 1 0 1 0 1 1 0 1)
+ //or
+ //(0 1 1 0 1 0 1 0 1 1 0 1 1 1 0 1 0 0)
+ //or
+ //(1 0 1 1 0 1 0 1 1 0 1 0 1 1 0 1 0 0)
+ //or
+ //(1 1 0 1 0 0 1 0 1 1 0 1 0 1 1 0 1 0)
+ //or
+ //(1 1 0 1 0 0 1 0 1 1 0 1 0 1 1 0 1 0)
relvarset1 = sylvan_set_fromarray(relvars1, 18);
- //(0 1 1 0 1 0 1 1 0 1 0 0 1 0 1 1 0 1)
- rel_enc1[0] = 0;
- rel_enc1[1] = 1;
- rel_enc1[2] = 1;
- rel_enc1[3] = 0;
- rel_enc1[4] = 1;
- rel_enc1[5] = 0;
- rel_enc1[6] = 1;
- rel_enc1[7] = 1;
- rel_enc1[8] = 0;
- rel_enc1[9] = 1;
- rel_enc1[10] = 0;
- rel_enc1[11] = 0;
- rel_enc1[12] = 1;
- rel_enc1[13] = 0;
- rel_enc1[14] = 1;
- rel_enc1[15] = 1;
- rel_enc1[16] = 0;
- rel_enc1[17] = 1;
+ if (i*6 < deltai && deltai < gammai){
+ uint8_t rel_enc__[18] = {1, 0, 1, 1, 0, 1, 1, 1, 0, 1, 0, 0, 0, 1, 1, 0, 1, 0};
+ memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
+ }
+ else if (deltai < gammai && gammai < i*6){
+ uint8_t rel_enc__[18] = {1, 1, 0, 1, 0, 0, 0, 1, 1, 0, 1, 0, 1, 0, 1, 1, 0, 1};
+ memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
+ }
+ else if (gammai < i*6 && i*6 < deltai){
+ uint8_t rel_enc__[18] = {0, 1, 1, 0, 1, 0, 1, 0, 1, 1, 0, 1, 1, 1, 0, 1, 0, 0};
+ memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
+ }
+ else if (i*6 < gammai && gammai < deltai){
+ uint8_t rel_enc__[18] = {1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0, 0};
+ memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
+ }
+ else if (deltai < i*6 && i*6 < gammai){
+ uint8_t rel_enc__[18] = {1, 1, 0, 1, 0, 0, 1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0};
+ memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
+ }
+ else {
+ uint8_t rel_enc__[18] = {0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0, 0, 1, 0, 1, 1, 0, 1};
+ memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
+ }
trs_current = (trans_t *)malloc(sizeof(trans_t));
trs_current->bdd = sylvan_cube(relvarset1, rel_enc1);
trs_current->varset.varset = relvarset1;
trs_current->next_rel = trs;
trs = trs_current;
}
+
}
trs_current = trs;
+
+ //test
+ /*
+ switch(dir){
+ case LEFT:
+ if (trs_current != NULL) printf("LEFT ok!\n");
+ else printf ("LEFT is empty\n");
+ printf("Num of trans relations:%d\n", countTrans(trs));
+ break;
+ case UP:
+ if (trs_current != NULL) printf("UP ok!\n");
+ else printf ("UP is empty\n");
+ printf("Num of trans relations:%d\n", countTrans(trs));
+ break;
+ case RIGHT:
+ if (trs_current != NULL) printf("RIGHT ok!\n");
+ else printf ("RIGHT is empty\n");
+ printf("Num of trans relations:%d\n", countTrans(trs));
+ break;
+ case DOWN:
+ if (trs_current != NULL) printf("DOWN ok!\n");
+ else printf ("DOWN is empty\n");
+ printf("Num of trans relations:%d\n", countTrans(trs));
+ break;
+ }
+ */
return trs;
}
+//test
+/*
+int countTrans(trans_t *trs)
+{
+ int counter = 0;
+ while (trs != NULL){
+ counter++;
+ trs = trs->next_rel;
+ }
+ return counter;
+}
+*/
rels *encode_rel(sokoban_screen *screen)
{
LACE_ME;
return rls;
}
-int
-test_relprod()
+int test_trans(state *s, trans_t *t)
{
LACE_ME;
-
- BDDVAR vars[] = {0,2,4};
- BDDVAR all_vars[] = {0,1,2,3,4,5};
- BDDVAR all_vars2[] = {0,1};
- //BDDVAR short_vars[] = {0,1};
- /*BDDVAR short_vars2[] = {2,3};
- BDDVAR short_vars3[] = {0,1,2,3};*/
-
- BDDSET vars_set = sylvan_set_fromarray(vars, 3);
- BDDSET all_vars_set = sylvan_set_fromarray(all_vars, 6);
- BDDSET all_vars_set2 = sylvan_set_fromarray(all_vars2, 2);
- //BDDSET short_vars_set = sylvan_set_fromarray(short_vars, 2);
- /*BDDSET short_vars_set2 = sylvan_set_fromarray(short_vars2, 2);
- BDDSET short_vars_set3 = sylvan_set_fromarray(short_vars3, 4);*/
-
- BDD s, t, next, prev;
- BDD zeroes, ones;
-
- // transition relation: 000 --> 111 and !000 --> 000
- t = sylvan_false;
- t = sylvan_union_cube(t, all_vars_set2, ((uint8_t[]){0,1}));
- //t = sylvan_union_cube(t, all_vars_set, ((uint8_t[]){1,0,2,0,2,0}));
- t = sylvan_union_cube(t, all_vars_set2, ((uint8_t[]){1,0}));
- // t = sylvan_union_cube(t, all_vars_set, ((uint8_t[]){0,1}));
-
- s = sylvan_cube(vars_set, (uint8_t[]){0,0,0});
- zeroes = sylvan_cube(vars_set, (uint8_t[]){1,0,0});
- ones = sylvan_cube(vars_set, (uint8_t[]){0,0,0});
-
- next = sylvan_relnext(s, t, all_vars_set);
- prev = sylvan_relprev(t, next, all_vars_set);
- if (next == zeroes) printf("Pass 1\n");
- if (prev == ones) printf("Pass 2\n");
- //trans *ts;
- //ts = NULL;
-
- return 0;
+ BDD next = sylvan_false;
+ while (t != NULL){
+ next = sylvan_relnext(s->bdd, t->bdd, t->varset.varset);
+ if (next == s->bdd) printf("Same\n");
+ if (next != s->bdd && next != sylvan_false) printf("Different\n");
+ if (next == sylvan_false) printf("False\n");
+ t = t->next_rel;
+ }
+ return 1;
}
repositories / mc1516pa.git / blobdiff