Merge branch 'master' of github.com:dopefishh/mc1516pa

diff --git a/modelchecker/coord.c b/modelchecker/coord.c
index c59f66c..6325091 100644 (file)
--- a/modelchecker/coord.c
+++ b/modelchecker/coord.c
@@ -247,11 +247,13 @@ state_t *explstate(state *init, rels *rls, state *g){
     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 = NULL;
+    tmp_state->lrd = lrd;
     state_queue = enq(tmp_state, state_queue);
 
     while (isEmpty(state_queue) == 0){
@@ -268,8 +270,8 @@ state_t *explstate(state *init, rels *rls, state *g){
             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));
-                    lrd = tmp_state->lrd;
                     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');
@@ -279,9 +281,9 @@ state_t *explstate(state *init, rels *rls, state *g){
                 }
                 else {
                     printf("GOAL\n");
-                    lurd_t *lrd = tmp_state->lrd;
-                    state_t *new_state = NULL;
-                    new_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));
+                    memcpy(lrd, tmp_state->lrd, sizeof(lurd_t));
                     new_state->bdd = new;
                     new_state->vars = init->vars;
                     lrd = lappend(lrd, 'l');
@@ -301,8 +303,8 @@ state_t *explstate(state *init, rels *rls, state *g){
             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));
-                    lrd = tmp_state->lrd;
                     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');
@@ -312,9 +314,9 @@ state_t *explstate(state *init, rels *rls, state *g){
                 }
                 else {
                     printf("GOAL\n");
-                    lurd_t *lrd = tmp_state->lrd;
-                    state_t *new_state = NULL;
-                    new_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));
+                    memcpy(lrd, tmp_state->lrd, sizeof(lurd_t));
                     new_state->bdd = new;
                     new_state->vars = init->vars;
                     lrd = lappend(lrd, 'u');
@@ -334,8 +336,9 @@ state_t *explstate(state *init, rels *rls, state *g){
             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));
-                    lrd = tmp_state->lrd;
                     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');
@@ -345,9 +348,10 @@ state_t *explstate(state *init, rels *rls, state *g){
                 }
                 else {
                     printf("GOAL\n");
-                    lurd_t *lrd = tmp_state->lrd;
-                    state_t *new_state = NULL;
-                    new_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));
+                    memcpy(lrd, tmp_state->lrd, sizeof(lurd_t));
+
                     new_state->bdd = new;
                     new_state->vars = init->vars;
                     lrd = lappend(lrd, 'r');
@@ -367,9 +371,11 @@ state_t *explstate(state *init, rels *rls, state *g){
         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));
-                    lrd = tmp_state->lrd;
                     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');
@@ -379,9 +385,10 @@ state_t *explstate(state *init, rels *rls, state *g){
                 }
                 else {
                     printf("GOAL\n");
-                    lurd_t *lrd = tmp_state->lrd;
-                    state_t *new_state = NULL;
-                    new_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));
+                    memcpy(lrd, tmp_state->lrd, sizeof(lurd_t));
+
                     new_state->bdd = new;
                     new_state->vars = init->vars;
                     lrd = lappend(lrd, 'd');

diff --git a/modelchecker/main.c b/modelchecker/main.c
index 742feba..e799d77 100644 (file)
--- a/modelchecker/main.c
+++ b/modelchecker/main.c
@@ -104,7 +104,7 @@ int solve(FILE *inputstream, char *lurd)
        }
        //int iteration = 0;
 
-       bool found = false;
+       //bool found = false;
     /*
        while(new != old){
                DPRINT("Iteration %d\n", iteration++);
@@ -134,7 +134,7 @@ int solve(FILE *inputstream, char *lurd)
             l = l->next;
         }
         printf("\n");
-    } else found = 0;
+    }
 
 
        time_end_solve = clock();
@@ -147,10 +147,12 @@ int solve(FILE *inputstream, char *lurd)
        REPORT("Relation encoding: %fs\n", time_end_rel, time_start_rel);
        REPORT("Solving encoding: %fs\n", time_end_solve, time_start_solve);
 
+    /*
        if(!found){
                printf("no solution\n");
                return 1;
        }
+    */
        return 0;
 }