From: Mart Lubbers Date: Sun, 17 Apr 2016 16:16:23 +0000 (+0200) Subject: revert X-Git-Url: https://git.martlubbers.net/?a=commitdiff_plain;h=f20e4641f467d5e4fdf761592f2e2af8daf28509;p=mc1516pa.git revert --- diff --git a/modelchecker/coord.c b/modelchecker/coord.c index 5b81b3b..5ff92e1 100644 --- 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 - //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) //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) //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) //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) //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) //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) 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, 0, 1, 1, 0, 0}; + uint8_t rel_enc__[18] = {0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 1, 1, 0, 0, 1}; memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); } else { - uint8_t rel_enc__[18] = {0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1}; + uint8_t rel_enc__[18] = {1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0}; 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) - //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) //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) //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) //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) //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) //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) 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 - //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 +673,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 +717,36 @@ 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) //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) //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) //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) //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) //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) 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 +761,28 @@ 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) + //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) 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 +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, 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));