X-Git-Url: https://git.martlubbers.net/?a=blobdiff_plain;f=modelchecker%2Fcoord.c;h=f9dd7e5c7abe754af61a6b1dc2795bdb86c2b767;hb=8054a7885e6e03b2998bf5bfd3b415816cd61cf9;hp=5b81b3b2622af32849e62e4e2900d197c4fab55e;hpb=9e8bfa77bd5043ba4a8748794e9f13b4df39ed4e;p=mc1516pa.git diff --git a/modelchecker/coord.c b/modelchecker/coord.c index 5b81b3b..f9dd7e5 100644 --- 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 {