redid two things

diff --git a/modelchecker/coord.c b/modelchecker/coord.c
index 5ff92e1..5b81b3b 100644 (file)
--- a/modelchecker/coord.c
+++ b/modelchecker/coord.c
@@ -538,17 +538,17 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir)
                        trs = trs_current;
 
             //Agent Box Box -> Agent Box Box
-                       //(1 1 0 0 1 1 0 0 1 1 0 0 0 0 1 1 0 0)
+                       //abb(1 1 0 0 1 1 0 0 1 1 0 0 0 0 1 1 0 0)
             //or
-            //(0 0 1 1 0 0 0 0 1 1 0 0 1 1 0 0 1 1)
+            //bba(0 0 1 1 0 0 0 0 1 1 0 0 1 1 0 0 1 1)
             //or
-            //(0 0 1 1 0 0 1 1 0 0 1 1 0 0 1 1 0 0)
+            //bab(0 0 1 1 0 0 1 1 0 0 1 1 0 0 1 1 0 0)
             //or
-            //(1 1 0 0 1 1 0 0 1 1 0 0 0 0 1 1 0 0)
+            //abb(1 1 0 0 1 1 0 0 1 1 0 0 0 0 1 1 0 0)
             //or
-            //(0 0 1 1 0 0 1 1 0 0 1 1 0 0 1 1 0 0)
+            //bab(0 0 1 1 0 0 1 1 0 0 1 1 0 0 1 1 0 0)
             //or
-            //(0 0 1 1 0 0 0 0 1 1 0 0 1 1 0 0 1 1)
+            //bba(0 0 1 1 0 0 0 0 1 1 0 0 1 1 0 0 1 1)
                        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 +569,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 +585,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)
+            //a b bt(1 1 0 0 1 1 0 0 1 1 0 0 1 1 0 0 0 0)
             //or
-            //(0 0 1 1 0 0 1 1 0 0 0 0 1 1 0 0 1 1)
+            //b tb a(0 0 1 1 0 0 1 1 0 0 0 0 1 1 0 0 1 1)
             //or
-            //(1 1 0 0 0 0 1 1 0 0 1 1 0 0 1 1 0 0)
+            //tb a b(1 1 0 0 0 0 1 1 0 0 1 1 0 0 1 1 0 0)
             //or
-            //(1 1 0 0 1 1 1 1 0 0 0 0 0 0 1 1 0 0)
+            //a tb b(1 1 0 0 1 1 1 1 0 0 0 0 0 0 1 1 0 0)
             //or
-            //(0 0 1 1 0 0 1 1 0 0 1 1 1 1 0 0 0 0)
+            //b a tb(0 0 1 1 0 0 1 1 0 0 1 1 1 1 0 0 0 0)
             //or
-            //(1 1 0 0 0 0 0 0 1 1 0 0 1 1 0 0 1 1)
+            //tb b a(1 1 0 0 0 0 0 0 1 1 0 0 1 1 0 0 1 1)
                        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 +629,17 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir)
                        trs = trs_current;
 
             //Targagent Box Box -> Targagent Box Box
-                       //(1 1 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0)
+                       //tabb(1 1 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0)
             //or
-            //(0 0 1 1 0 0 0 0 1 1 0 0 1 1 1 1 0 0)
+            //bbta(0 0 1 1 0 0 0 0 1 1 0 0 1 1 1 1 0 0)
             //or
-            //(0 0 1 1 0 0 1 1 1 1 0 0 0 0 1 1 0 0)
+            //btab(0 0 1 1 0 0 1 1 1 1 0 0 0 0 1 1 0 0)
             //or
-            //(1 1 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0)
+            //tabb(1 1 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0)
             //or
-            //(0 0 1 1 0 0 1 1 1 1 0 0 0 0 1 1 0 0)
+            //btab(0 0 1 1 0 0 1 1 1 1 0 0 0 0 1 1 0 0)
             //or
-            //(0 0 1 1 0 0 0 0 1 1 0 0 1 1 1 1 0 0)
+            //bbta(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 +673,17 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir)
                        trs = trs_current;
 
             //Targagent Box Targbox -> Targagent Box Targbox (LEFT || UP)
-            //(1 1 1 1 0 0 0 0 1 1 0 0 1 1 0 0 0 0)
+            //tabtb(1 1 1 1 0 0 0 0 1 1 0 0 1 1 0 0 0 0)
             //or
-            //(0 0 1 1 0 0 1 1 0 0 0 0 1 1 1 1 0 0)
+            //btatb(0 0 1 1 0 0 1 1 0 0 0 0 1 1 1 1 0 0)
             //or
-            //(1 1 0 0 0 0 1 1 1 1 0 0 0 0 1 1 0 0)
+            //tbtab(1 1 0 0 0 0 1 1 1 1 0 0 0 0 1 1 0 0)
             //or
-            //(1 1 1 1 0 0 1 1 0 0 0 0 0 0 1 1 0 0)
+            //tatbb(1 1 1 1 0 0 1 1 0 0 0 0 0 0 1 1 0 0)
             //or
-            //(0 0 1 1 0 0 1 1 1 1 0 0 1 1 0 0 0 0)
+            //btatb(0 0 1 1 0 0 1 1 1 1 0 0 1 1 0 0 0 0)
             //or
-            //(1 1 0 0 0 0 0 0 1 1 0 0 1 1 1 1 0 0)
+            //tbbta(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 +717,36 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir)
                        trs = trs_current;
 
                        //Agent Box Free -> Free Agent Box
-            //(1 0 0 0 1 1 0 1 1 0 0 1 0 0 0 1 1 0)
+            //abf-fab(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)
+            //bfa-baf(0 0 1 1 0 0 0 1 0 0 1 1 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)
+            //fab-afb(0 1 0 0 1 1 1 0 0 0 1 1 0 0 1 1 0 0)
             //or
-            //(1 0 0 0 1 1 0 0 0 1 1 0 0 1 1 0 0 1)
+            //afb-fab(1 0 0 0 1 1 0 1 0 0 1 1 0 0 1 1 0 0)
             //or
-            //(0 1 1 0 0 1 1 0 0 0 1 1 0 0 0 1 1 0)
+            //baf-bfa(0 0 1 1 0 0 1 0 0 0 1 1 0 1 0 0 1 1)
             //or
-            //(0 0 0 1 1 0 0 1 1 0 0 1 1 0 0 0 1 1)
+            //fba-baf(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, 1, 1, 0, 0, 1, 0, 0, 0, 1, 1, 0, 1, 0, 0, 0, 1, 1};
+                uint8_t rel_enc__[18] = {0, 0, 1, 1, 0, 0, 0, 1, 0, 0, 1, 1, 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, 0, 0, 1, 1, 0, 1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 0, 1};
+                uint8_t rel_enc__[18] = {0, 1, 0, 0, 1, 1, 1, 0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0};
                 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, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1};
+                uint8_t rel_enc__[18] = {1, 0, 0, 0, 1, 1, 0, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0};
                 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
             }
             else if ((deltai < i) < gammai){
-                uint8_t rel_enc__[18] = {0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 1, 1, 0, 0, 0, 1, 1, 0};
+                uint8_t rel_enc__[18] = {0, 0, 1, 1, 0, 0, 1, 0, 0, 0, 1, 1, 0, 1, 0, 0, 1, 1};
                 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
             }
             else {
@@ -761,28 +761,28 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir)
                        trs = trs_current;
 
                        //Agent Targbox Free -> Free Targagent Box
-            //(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)
-            //or
-            //(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)
-            //or
-            //(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)
+            //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)
                        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};
+                uint8_t rel_enc__[18] = {1, 0, 0, 0, 1, 1, 1, 1, 0, 0, 0, 1, 0, 1, 0, 0, 1, 0};
                 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
             }
             else if ((deltai < gammai) < i){
-                uint8_t rel_enc__[18] = {1, 1, 0, 1, 0, 0, 0, 0, 0, 1, 1, 0, 1, 0, 0, 0, 1, 1};
+                uint8_t rel_enc__[18] = {1, 1, 0, 0, 0, 0, 0, 1, 0, 0, 1, 1, 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, 0, 0, 1, 1, 0, 1, 0, 0, 0, 1, 1, 1, 1, 0, 1, 0, 0};
+                uint8_t rel_enc__[18] = {1, 0, 0, 0, 1, 1, 0, 1, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0};
                 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
             }
             else if ((i < gammai) < deltai){
@@ -790,11 +790,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, 1, 0, 0, 1, 0, 0, 0, 1, 1, 0, 0, 0, 1, 1, 0};
+                uint8_t rel_enc__[18] = {1, 1, 0, 0, 0, 0, 1, 0, 0, 0, 1, 1, 0, 1, 0, 0, 1, 1};
                 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
             }
             else {
-                uint8_t rel_enc__[18] = {0, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0, 0, 1, 0, 0, 0, 1, 1};
+                uint8_t rel_enc__[18] = {0, 1, 0, 0, 1, 0, 1, 1, 0, 0, 0, 1, 1, 0, 0, 0, 1, 1};
                 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
             }
                        trs_current = (trans_t *)malloc(sizeof(trans_t));

diff --git a/modelchecker/toy.screen b/modelchecker/toy.screen
index a381e1a..87d52be 100644 (file)
--- a/modelchecker/toy.screen
+++ b/modelchecker/toy.screen
@@ -1,2 +1 @@
-@
-.
+@ $