transitions fix

[mc1516pa.git] / modelchecker / coord.c

diff --git a/modelchecker/coord.c b/modelchecker/coord.c
index 5b81b3b..f9dd7e5 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};
@@ -538,17 +538,18 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir)
                        trs = trs_current;
 
             //Agent Box Box -> Agent Box Box
-                       //abb(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)
+            //(1 1 0 0 1 1 0 0 1 1 0 0 0 0 1 1 0 0 (i delta gamma)
             //or
-            //bba(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
-            //bab(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
-            //abb(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
-            //bab(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
-            //bba(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];
@@ -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)
-            //a b bt(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
-            //b tb a(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
-            //tb a b(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
-            //a tb b(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
-            //b a tb(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
-            //tb b a(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};
@@ -629,17 +630,17 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir)
                        trs = trs_current;
 
             //Targagent Box Box -> Targagent Box Box
-                       //tabb(1 1 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0)
+                       //(1 1 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0)
             //or
-            //bbta(0 0 1 1 0 0 0 0 1 1 0 0 1 1 1 1 0 0)
+            //(0 0 1 1 0 0 0 0 1 1 0 0 1 1 1 1 0 0)
             //or
-            //btab(0 0 1 1 0 0 1 1 1 1 0 0 0 0 1 1 0 0)
+            //(0 0 1 1 0 0 1 1 1 1 0 0 0 0 1 1 0 0)
             //or
-            //tabb(1 1 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0)
+            //(1 1 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0)
             //or
-            //btab(0 0 1 1 0 0 1 1 1 1 0 0 0 0 1 1 0 0)
+            //(0 0 1 1 0 0 1 1 1 1 0 0 0 0 1 1 0 0)
             //or
-            //bbta(0 0 1 1 0 0 0 0 1 1 0 0 1 1 1 1 0 0)
+            //(0 0 1 1 0 0 0 0 1 1 0 0 1 1 1 1 0 0)
                        relvarset1 = sylvan_set_fromarray(relvars1, 18);
             if ((i < 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};
@@ -673,17 +674,17 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir)
                        trs = trs_current;
 
             //Targagent Box Targbox -> Targagent Box Targbox (LEFT || UP)
-            //tabtb(1 1 1 1 0 0 0 0 1 1 0 0 1 1 0 0 0 0)
+            //(1 1 1 1 0 0 0 0 1 1 0 0 1 1 0 0 0 0)
             //or
-            //btatb(0 0 1 1 0 0 1 1 0 0 0 0 1 1 1 1 0 0)
+            //(0 0 1 1 0 0 1 1 0 0 0 0 1 1 1 1 0 0)
             //or
-            //tbtab(1 1 0 0 0 0 1 1 1 1 0 0 0 0 1 1 0 0)
+            //(1 1 0 0 0 0 1 1 1 1 0 0 0 0 1 1 0 0)
             //or
-            //tatbb(1 1 1 1 0 0 1 1 0 0 0 0 0 0 1 1 0 0)
+            //(1 1 1 1 0 0 1 1 0 0 0 0 0 0 1 1 0 0)
             //or
-            //btatb(0 0 1 1 0 0 1 1 1 1 0 0 1 1 0 0 0 0)
+            //(0 0 1 1 0 0 1 1 1 1 0 0 1 1 0 0 0 0)
             //or
-            //tbbta(1 1 0 0 0 0 0 0 1 1 0 0 1 1 1 1 0 0)
+            //(1 1 0 0 0 0 0 0 1 1 0 0 1 1 1 1 0 0)
                        relvarset1 = sylvan_set_fromarray(relvars1, 18);
             if ((i < 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};
@@ -717,36 +718,42 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir)
                        trs = trs_current;
 
                        //Agent Box Free -> Free Agent Box
-            //abf-fab(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)
+            //(1 0 0 0 1 1 0 1 1 0 0 1 0 0 0 1 1 0)
             //or
-            //bfa-baf(0 0 1 1 0 0 0 1 0 0 1 1 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 1 0 0 0 1 1
             //or
-            //fab-afb(0 1 0 0 1 1 1 0 0 0 1 1 0 0 1 1 0 0)
+            //(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
-            //afb-fab(1 0 0 0 1 1 0 1 0 0 1 1 0 0 1 1 0 0)
+            //(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
-            //baf-bfa(0 0 1 1 0 0 1 0 0 0 1 1 0 1 0 0 1 1)
+            //(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
-            //fba-baf(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)
+            //(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};
                 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
             }
             else if ((deltai < gammai) < i){
-                uint8_t rel_enc__[18] = {0, 0, 1, 1, 0, 0, 0, 1, 0, 0, 1, 1, 1, 0, 0, 0, 1, 1};
+                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) < deltai){
-                uint8_t rel_enc__[18] = {0, 1, 0, 0, 1, 1, 1, 0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0};
+                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 < gammai) < deltai){
-                uint8_t rel_enc__[18] = {1, 0, 0, 0, 1, 1, 0, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0};
+                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) < gammai){
-                uint8_t rel_enc__[18] = {0, 0, 1, 1, 0, 0, 1, 0, 0, 0, 1, 1, 0, 1, 0, 0, 1, 1};
+                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 {
@@ -761,28 +768,34 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir)
                        trs = trs_current;
 
                        //Agent Targbox Free -> Free Targagent Box
-            //atbf-fatb(1 0 0 0 1 1 1 1 0 0 0 1 0 1 0 0 1 0)
-            //or -   
-            //tbfa-tbaf(1 1 0 0 0 0 0 1 0 0 1 1 1 0 0 0 1 1)
-            //or -   
-            //fatb-aftb(0 1 0 0 1 1 1 0 0 0 1 1 1 1 0 0 0 0)
-            //or -   
-            //aftb-fatb(1 0 0 0 1 1 0 1 0 0 1 1 1 1 0 0 0 0)
-            //or -   
-            //tbaf-tbfa(1 1 0 0 0 0 1 0 0 0 1 1 0 1 0 0 1 1)
-            //or -   
-            //ftba-tbaf(0 1 0 0 1 0 1 1 0 0 0 1 1 0 0 0 1 1)
+            //(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, 0, 0, 1, 0, 1, 0, 0, 1, 0};
+                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) < i){
-                uint8_t rel_enc__[18] = {1, 1, 0, 0, 0, 0, 0, 1, 0, 0, 1, 1, 1, 0, 0, 0, 1, 1};
+                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) < deltai){
-                uint8_t rel_enc__[18] = {1, 0, 0, 0, 1, 1, 0, 1, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0};
+                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 < gammai) < deltai){
@@ -790,11 +803,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] = {1, 1, 0, 0, 0, 0, 1, 0, 0, 0, 1, 1, 0, 1, 0, 0, 1, 1};
+                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, 1, 0, 0, 1, 0, 1, 1, 0, 0, 0, 1, 1, 0, 0, 0, 1, 1};
+                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));
@@ -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};
@@ -850,6 +869,7 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir)
 
                        //Agent Targbox Target -> Free Targagent Targbox
             //(1 0 0 0 1 1 1 1 0 1 0 0 0 1 1 0 1 0)
+            //(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
@@ -894,16 +914,22 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir)
 
                        //Targagent Box Free -> Target Agent Box
             //(1 0 1 1 0 1 0 1 1 0 0 1 0 0 0 1 1 0)
+            //(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)
+            //(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)
+            //(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)
+            //(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)
+            //(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)
+            //(0 0 0 1 1 0 0 1 1 0 0 1 1 0 1 1 0 1
                        relvarset1 = sylvan_set_fromarray(relvars1, 18);
             if ((i < 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};
@@ -938,16 +964,22 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir)
 
                        //Targagent Targbox Free -> Target Targagent Box
             //(1 0 1 1 0 1 1 1 0 1 0 0 0 0 0 1 1 0)
+            //(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)
+            //(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)
+            //(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)
+            //(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)
+            //(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)
+            //(0 0 0 1 1 0 1 1 0 1 0 0 1 0 1 1 0 1
                        relvarset1 = sylvan_set_fromarray(relvars1, 18);
             if ((i < 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};
@@ -966,7 +998,7 @@ 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] = {1, 1, 0, 1, 0, 0, 1, 0, 1, 1, 0, 1, 0, 0, 0, 1, 1, 0};
+                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 {