From: Alexander Fedotov Date: Tue, 19 Apr 2016 18:59:10 +0000 (+0200) Subject: transitions fix X-Git-Url: https://git.martlubbers.net/?a=commitdiff_plain;h=8054a7885e6e03b2998bf5bfd3b415816cd61cf9;p=mc1516pa.git transitions fix --- diff --git a/modelchecker/coord.c b/modelchecker/coord.c index cd30e27..f9dd7e5 100644 --- a/modelchecker/coord.c +++ b/modelchecker/coord.c @@ -869,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 @@ -913,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}; @@ -957,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}; @@ -985,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 {