path extraction

diff --git a/modelchecker/coord.c b/modelchecker/coord.c
index d5aceb5..c59f66c 100644 (file)
--- a/modelchecker/coord.c
+++ b/modelchecker/coord.c
@@ -244,140 +244,154 @@ int check_visited(BDD s, BDD v, BDDSET vars){
 
 state_t *explstate(state *init, rels *rls, state *g){
     LACE_ME;
-    lurd_t *lrd = NULL;
     deque *state_queue = create();
     trans_t *t = NULL;
-    state_t *tmp_state = NULL;
+    state_t *tmp_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;
+    tmp_state->lrd = NULL;
     state_queue = enq(tmp_state, state_queue);
 
-    while (isEmpty(state_queue) == 1){
+    while (isEmpty(state_queue) == 0){
         tmp_state = get_front(state_queue);
         state_queue = deq(state_queue);
+        new = tmp_state->bdd;
         t = rls->rell;
-        new = sylvan_false;
         while (t != NULL){
-            new = sylvan_or(new, sylvan_relnext(new, t->bdd, t->varset.varset));
+            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 (check_visited(new, visited, init->vars.varset) == 0){
-            if (check_goal(new, g->bdd, init->vars.varset) == 0){
-                lurd_t *lrd = tmp_state->lrd;
-                state_t *new_state = NULL;
-                new_state = (state_t*)malloc(sizeof(state_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 {
-                lurd_t *lrd = tmp_state->lrd;
-                state_t *new_state = NULL;
-                new_state = (state_t*)malloc(sizeof(state_t));
-                new_state->bdd = new;
-                new_state->vars = init->vars;
-                lrd = lappend(lrd, 'l');
-                new_state->lrd = lrd;
-                return new_state;
+        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));
+                    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 = tmp_state->lrd;
+                    state_t *new_state = NULL;
+                    new_state = (state_t*)malloc(sizeof(state_t));
+                    new_state->bdd = new;
+                    new_state->vars = init->vars;
+                    lrd = lappend(lrd, 'l');
+                    new_state->lrd = lrd;
+                    return new_state;
+                }
             }
         }
 
         t = rls->relu;
-        new = sylvan_false;
         while (t != NULL){
-            new = sylvan_or(new, sylvan_relnext(new, t->bdd, t->varset.varset));
+            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 (check_visited(new, visited, init->vars.varset) == 0){
-            if (check_goal(new, g->bdd, init->vars.varset) == 0){
-                lurd_t *lrd = tmp_state->lrd;
-                state_t *new_state = NULL;
-                new_state = (state_t*)malloc(sizeof(state_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 {
-                lurd_t *lrd = tmp_state->lrd;
-                state_t *new_state = NULL;
-                new_state = (state_t*)malloc(sizeof(state_t));
-                new_state->bdd = new;
-                new_state->vars = init->vars;
-                lrd = lappend(lrd, 'u');
-                new_state->lrd = lrd;
-                return new_state;
+        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));
+                    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 = tmp_state->lrd;
+                    state_t *new_state = NULL;
+                    new_state = (state_t*)malloc(sizeof(state_t));
+                    new_state->bdd = new;
+                    new_state->vars = init->vars;
+                    lrd = lappend(lrd, 'u');
+                    new_state->lrd = lrd;
+                    return new_state;
+                }
             }
         }
 
         t = rls->relr;
-        new = sylvan_false;
         while (t != NULL){
-            new = sylvan_or(new, sylvan_relnext(new, t->bdd, t->varset.varset));
+            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 (check_visited(new, visited, init->vars.varset) == 0){
-            if (check_goal(new, g->bdd, init->vars.varset) == 0){
-                lurd_t *lrd = tmp_state->lrd;
-                state_t *new_state = NULL;
-                new_state = (state_t*)malloc(sizeof(state_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 {
-                lurd_t *lrd = tmp_state->lrd;
-                state_t *new_state = NULL;
-                new_state = (state_t*)malloc(sizeof(state_t));
-                new_state->bdd = new;
-                new_state->vars = init->vars;
-                lrd = lappend(lrd, 'r');
-                new_state->lrd = lrd;
-                return new_state;
+        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));
+                    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 = tmp_state->lrd;
+                    state_t *new_state = NULL;
+                    new_state = (state_t*)malloc(sizeof(state_t));
+                    new_state->bdd = new;
+                    new_state->vars = init->vars;
+                    lrd = lappend(lrd, 'r');
+                    new_state->lrd = lrd;
+                    return new_state;
+                }
             }
         }
 
+
         t = rls->reld;
-        new = sylvan_false;
         while (t != NULL){
-            new = sylvan_or(new, sylvan_relnext(new, t->bdd, t->varset.varset));
+            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 (check_visited(new, visited, init->vars.varset) == 0){
-            if (check_goal(new, g->bdd, init->vars.varset) == 0){
-                lurd_t *lrd = tmp_state->lrd;
-                state_t *new_state = NULL;
-                new_state = (state_t*)malloc(sizeof(state_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 {
-                lurd_t *lrd = tmp_state->lrd;
-                state_t *new_state = NULL;
-                new_state = (state_t*)malloc(sizeof(state_t));
-                new_state->bdd = new;
-                new_state->vars = init->vars;
-                lrd = lappend(lrd, 'd');
-                new_state->lrd = lrd;
-                return new_state;
+        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));
+                    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 = tmp_state->lrd;
+                    state_t *new_state = NULL;
+                    new_state = (state_t*)malloc(sizeof(state_t));
+                    new_state->bdd = new;
+                    new_state->vars = init->vars;
+                    lrd = lappend(lrd, 'd');
+                    new_state->lrd = lrd;
+                    return new_state;
+                }
             }
         }
 
+
     }
 
     return NULL;

diff --git a/modelchecker/coord.h b/modelchecker/coord.h
index fb4a08b..014579f 100644 (file)
--- a/modelchecker/coord.h
+++ b/modelchecker/coord.h
@@ -53,6 +53,8 @@ int check_visited(BDD s, BDD v, BDDSET vars);
 
 lurd_t *lappend(lurd_t *l, char c);
 
+state_t *explstate(state *init, rels *rls, state *g);
+
 int test_relprod();
 
 #endif

diff --git a/modelchecker/deque.c b/modelchecker/deque.c
index bff77ed..12ad6fc 100644 (file)
--- a/modelchecker/deque.c
+++ b/modelchecker/deque.c
@@ -66,6 +66,6 @@ int isEmpty(deque *d)
 
 state_t *get_front(deque *d)
 {
-    if (isEmpty(d) == 1) return d->front->s;
+    if (isEmpty(d) == 0) return d->front->s;
     else return NULL;
 }

diff --git a/modelchecker/main.c b/modelchecker/main.c
index b262660..0b0067b 100644 (file)
--- a/modelchecker/main.c
+++ b/modelchecker/main.c
@@ -77,10 +77,9 @@ int solve(FILE *inputstream, char *lurd)
        rels *rls = encode_rel(screen);
        time_end_rel = clock();
 
-
        //Actually solve
        time_start_solve = clock();
-       BDD old = sylvan_false;
+       //BDD old = sylvan_false;
        BDD new = init->bdd;
        //Do lurd
        while(*lurd != '\0'){
@@ -103,8 +102,10 @@ int solve(FILE *inputstream, char *lurd)
                }
                lurd++;
        }
-       int iteration = 0;
+       //int iteration = 0;
+
        bool found = false;
+    /*
        while(new != old){
                DPRINT("Iteration %d\n", iteration++);
                old = new;
@@ -119,6 +120,23 @@ int solve(FILE *inputstream, char *lurd)
                new = subsolve(rls->relr, new);
                new = subsolve(rls->reld, new);
        }
+    */
+    state_t *res = NULL;
+    state *cont = (state *)malloc(sizeof(cont));
+    cont->bdd = new;
+    cont->vars = init->vars;
+    res = explstate(cont, rls, goal);
+    if (res != NULL){
+        if (res->lrd == NULL) printf("wrong\n");
+        lurd_t *l = res->lrd;
+        while (l != NULL){
+            printf("%c", l->c);
+            l = l->next;
+        }
+        printf("\n");
+    } else found = 0;
+
+
        time_end_solve = clock();
 
        //Free and print stats