checked all 1 and 2 cases

[mc1516pa.git] / modelchecker / coord.c

diff --git a/modelchecker/coord.c b/modelchecker/coord.c
index caa7b78..5ff92e1 100644 (file)
--- a/modelchecker/coord.c
+++ b/modelchecker/coord.c
@@ -310,16 +310,16 @@ 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 0 1 1 1 1 0)
+            //(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};
                 memcpy(rel_enc, rel_enc2, 12*sizeof(uint8_t));
             }
             else {
-                uint8_t rel_enc2[12] = {0, 1, 1, 1, 1, 0, 0, 1, 1, 1, 1, 0};
+                uint8_t rel_enc2[12] = {0, 1, 1, 1, 1, 0, 1, 0, 0, 0, 1, 1};
                 memcpy(rel_enc, rel_enc2, 12*sizeof(uint8_t));
             }
                        trs_current = (trans_t *)malloc(sizeof(trans_t));