X-Git-Url: https://git.martlubbers.net/?a=blobdiff_plain;f=modelchecker%2Fcoord.c;h=42ad6cee7c9e787d2b7c2ee5a5f7349e90a69f47;hb=313c58c1cd85852f33ff7ca7c638ccb3066d5069;hp=63250915d82f2f3f651f497666b84bae949be66f;hpb=6b4ffb3fcb69b5380bc75440a4bc73b5dc963921;p=mc1516pa.git

diff --git a/modelchecker/coord.c b/modelchecker/coord.c
index 6325091..42ad6ce 100644
--- a/modelchecker/coord.c
+++ b/modelchecker/coord.c
@@ -6,7 +6,6 @@
 
 #include "coord.h"
 #include "sokoban.h"
-#include "deque.h"
 
 
 typedef struct {
@@ -123,7 +122,6 @@ int check_space(int x, int y, direction d, int delta, bimap *bm)
  * It seems that the move variable is not necessary since non-deterministic moves can be emvedded
  * directly in transition relations.
  */
-
 state *encode_screen(sokoban_screen *screen)
 {
 	LACE_ME;
@@ -142,272 +140,51 @@ state *encode_screen(sokoban_screen *screen)
 	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)){
+	for(sokoban_screen *r=screen; r != NULL; r = r->hh.next){
 		switch(r->tile){
 		case FREE: //001
-			st_enc[tile_index] = 0;
-			tile_index++;
-			st_enc[tile_index] = 0;
-			tile_index++;
-			st_enc[tile_index] = 1;
-			tile_index++;
+			st_enc[tile_index++] = 0;
+			st_enc[tile_index++] = 0;
+			st_enc[tile_index++] = 1;
 			break;
 		case WALL: //000
-			st_enc[tile_index] = 0;
-			tile_index++;
-			st_enc[tile_index] = 0;
-			tile_index++;
-			st_enc[tile_index] = 0;
-			tile_index++;
+			st_enc[tile_index++] = 0;
+			st_enc[tile_index++] = 0;
+			st_enc[tile_index++] = 0;
 			break;
 		case BOX: //010
-			st_enc[tile_index] = 0;
-			tile_index++;
-			st_enc[tile_index] = 1;
-			tile_index++;
-			st_enc[tile_index] = 0;
-			tile_index++;
+			st_enc[tile_index++] = 0;
+			st_enc[tile_index++] = 1;
+			st_enc[tile_index++] = 0;
 			break;
 		case TARGET: //011
-			st_enc[tile_index] = 0;
-			tile_index++;
-			st_enc[tile_index] = 1;
-			tile_index++;
-			st_enc[tile_index] = 1;
-			tile_index++;
+			st_enc[tile_index++] = 0;
+			st_enc[tile_index++] = 1;
+			st_enc[tile_index++] = 1;
 			break;
 		case AGENT: //101
-			st_enc[tile_index] = 1;
-			tile_index++;
-			st_enc[tile_index] = 0;
-			tile_index++;
-
-			st_enc[tile_index] = 1;
-			tile_index++;
+			st_enc[tile_index++] = 1;
+			st_enc[tile_index++] = 0;
+			st_enc[tile_index++] = 1;
 			break;
 		case TARGAGENT: //110
-			st_enc[tile_index] = 1;
-			tile_index++;
-			st_enc[tile_index] = 1;
-			tile_index++;
-			st_enc[tile_index] = 0;
-			tile_index++;
+			st_enc[tile_index++] = 1;
+			st_enc[tile_index++] = 1;
+			st_enc[tile_index++] = 0;
 			break;
 		case TARGBOX: //100
-			st_enc[tile_index] = 1;
-			tile_index++;
-			st_enc[tile_index] = 0;
-			tile_index++;
-			st_enc[tile_index] = 0;
-			tile_index++;
+			st_enc[tile_index++] = 1;
+			st_enc[tile_index++] = 0;
+			st_enc[tile_index++] = 0;
 			break;
 		}
 	}
 	s = sylvan_cube(varset, st_enc);
 	fullState->bdd = s;
-	printf("Initial state encoded\n");
 	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];
@@ -424,83 +201,50 @@ state *encode_goal(sokoban_screen *screen){
 	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)){
+	for(sokoban_screen *r=screen; r != NULL; r=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++;
+			st_enc[tile_index++] = 2;
+			st_enc[tile_index++] = 2;
+			st_enc[tile_index++] = 2;
 			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++;
+			st_enc[tile_index++] = 0;
+			st_enc[tile_index++] = 0;
+			st_enc[tile_index++] = 0;
 			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++;
+			st_enc[tile_index++] = 2;
+			st_enc[tile_index++] = 2;
+			st_enc[tile_index++] = 2;
 			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++;
+			st_enc[tile_index++] = 1;
+			st_enc[tile_index++] = 0;
+			st_enc[tile_index++] = 0;
 			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++;
+			st_enc[tile_index++] = 2;
+			st_enc[tile_index++] = 2;
+			st_enc[tile_index++] = 2;
 			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++;
+			st_enc[tile_index++] = 1;
+			st_enc[tile_index++] = 0;
+			st_enc[tile_index++] = 0;
 			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++;
+			st_enc[tile_index++] = 1;
+			st_enc[tile_index++] = 0;
+			st_enc[tile_index++] = 0;
 			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;
-
+	return fullState;
 }
 
-//test
-//int countTrans(trans_t *trs);
-
 trans_t *create_single_rel(sokoban_screen *screen, direction dir)
 {
 	LACE_ME;
@@ -571,9 +315,7 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir)
 			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) == 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);
 			unsigned int deltai = bddvar->value.var[0];
             //Agent Free -> Free Agent
@@ -737,11 +479,7 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir)
 			trs_current->varset.size = 12;
 			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);
 			unsigned int deltai = bddvar->value.var[0];
 			bddvar = getxy(x + xgamma, y + ygamma, bm->f);
@@ -1367,47 +1105,9 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir)
 
 	}
 	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;
@@ -1416,14 +1116,8 @@ rels *encode_rel(sokoban_screen *screen)
 
 	//left relation
 	tl = create_single_rel(screen, LEFT);
-
-	//up relation
 	trans_t *tu = create_single_rel(screen, UP);
-
-	//right relation
 	trans_t *tr = create_single_rel(screen, RIGHT);
-
-	//down relation
 	trans_t *td = create_single_rel(screen, DOWN);
 
 	rels *rls = NULL;
@@ -1435,17 +1129,3 @@ rels *encode_rel(sokoban_screen *screen)
 
 	return rls;
 }
-
-int test_trans(state *s, trans_t *t)
-{
-    LACE_ME;
-    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;
-}