some checks

diff --git a/modelchecker/coord.c b/modelchecker/coord.c
index 5ff92e1..cd30e27 100644 (file)
--- a/modelchecker/coord.c
+++ b/modelchecker/coord.c
@@ -310,9 +310,9 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir)
                        trs = trs_current;
 
             //Agent Target -> Free Targagent
-            //(1 0 0 0 1 1 - 0 1 1 1 1 0)
+            //(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)
+            //(0 1 1 1 1 0 1 0 0 0 1 1)
                        relvarset = sylvan_set_fromarray(relvars, 12);
             if (i < deltai){
                 uint8_t rel_enc2[12] = {1, 0, 0, 0, 1, 1, 0, 1, 1, 1, 1, 0};
@@ -539,16 +539,17 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir)
 
             //Agent Box Box -> Agent Box Box
                        //(1 1 0 0 1 1 0 0 1 1 0 0 0 0 1 1 0 0)
+            //(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)
+            //(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)
+            //(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)
+            //(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)
+            //(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)
+            //(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];
@@ -569,11 +570,11 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir)
                 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
             }
             else if ((deltai < i) < gammai){
-                uint8_t rel_enc__[18] = {0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 1, 1, 0, 0, 1};
+                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] = {1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0};
+                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));
             }
 
@@ -585,17 +586,17 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir)
                        trs = trs_current;
 
             //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)
+            //(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)
+            //(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)
+            //(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)
+            //(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)
+            //(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)
+            //(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);
             if ((i < 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};
@@ -718,16 +719,22 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir)
 
                        //Agent Box Free -> Free Agent Box
             //(1 0 0 0 1 1 0 1 1 0 0 1 0 0 0 1 1 0)
+            //(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)
+            //(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)
+            //(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)
+            //(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)
+            //(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)
+            //(0 0 0 1 1 0 0 1 1 0 0 1 1 0 0 0 1 1
                        relvarset1 = sylvan_set_fromarray(relvars1, 18);
             if ((i < 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};
@@ -762,16 +769,22 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir)
 
                        //Agent Targbox Free -> Free Targagent Box
             //(1 0 0 0 1 1 1 1 0 1 0 0 0 0 0 1 1 0)
+            //(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)
+            //(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)
+            //(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)
+            //(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)
+            //(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)
+            //(0 0 0 1 1 0 1 1 0 1 0 0 1 0 0 0 1 1
                        relvarset1 = sylvan_set_fromarray(relvars1, 18);
             if ((i < 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};
@@ -806,16 +819,22 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir)
 
                        //Agent Box Target -> Free Agent Targbox
             //(1 0 0 0 1 1 0 1 1 0 0 1 0 1 1 0 1 0)
+            //(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)
+            //(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)
+            //(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)
+            //(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)
+            //(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)
+            //(0 1 1 0 1 0 0 1 1 0 0 1 1 0 0 0 1 1
                        relvarset1 = sylvan_set_fromarray(relvars1, 18);
             if ((i < 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};