From 0212b386d85354399a194538538c0da541e987ea Mon Sep 17 00:00:00 2001 From: Alexander Fedotov Date: Wed, 20 Apr 2016 00:02:00 +0200 Subject: [PATCH] transition fix --- modelchecker/coord.c | 161 ++++++++++++++++--------------------------- modelchecker/main.c | 1 + 2 files changed, 62 insertions(+), 100 deletions(-) diff --git a/modelchecker/coord.c b/modelchecker/coord.c index 48f3b07..0f5a507 100644 --- a/modelchecker/coord.c +++ b/modelchecker/coord.c @@ -262,7 +262,6 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir) BDDVAR relvars[6] = {i * 6, i * 6 + 1, i * 6 + 2, i * 6 + 3, i * 6 + 4, i * 6 + 5}; BDDSET relvarset = sylvan_set_fromarray(relvars, 6); uint8_t rel_enc[6] = {1, 1, 0, 0, 1, 1}; - trs_current = (trans_t *)malloc(sizeof(trans_t)); trs_current->bdd = sylvan_cube(relvarset, rel_enc); trs_current->varset.varset = relvarset; @@ -449,6 +448,7 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir) trs_current->next_rel = trs; trs = trs_current; + } else if (check_space(x, y, dir, 1, bm) == 1 && check_space(x, y, dir, 2, bm) == 1){ xy_bddvar_map *bddvar = getxy(x + xdelta, y + ydelta, bm->f); @@ -538,7 +538,6 @@ 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) //(1 1 0 0 1 1 0 0 1 1 0 0 0 0 1 1 0 0 (i delta gamma) //or //(0 0 1 1 0 0 0 0 1 1 0 0 1 1 0 0 1 1) (delta gamma i) @@ -553,23 +552,23 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir) 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]; - if ((i < deltai) < gammai){ + if (i < deltai && deltai < gammai){ 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)); } - else if ((deltai < gammai) < i){ + else if (deltai < gammai && gammai < i){ 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)); } - else if ((gammai < i) < deltai){ + else if (gammai < i && i < deltai){ 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 if ((i < gammai) < deltai){ + else if (i < gammai && gammai < deltai){ 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)); } - else if ((deltai < i) < gammai){ + else if (deltai < i && 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}; memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); } @@ -598,23 +597,23 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir) //or //(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){ + if (i < deltai && 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}; memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); } - else if ((deltai < gammai) < i){ + else if (deltai < gammai && gammai < i){ uint8_t rel_enc__[18] = {0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1}; memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); } - else if ((gammai < i) < deltai){ + else if (gammai < i && i < deltai){ uint8_t rel_enc__[18] = {1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0}; memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); } - else if ((i < gammai) < deltai){ + else if (i < gammai && gammai < deltai){ uint8_t rel_enc__[18] = {1, 1, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0}; memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); } - else if ((deltai < i) < gammai){ + else if (deltai < i && i < gammai){ uint8_t rel_enc__[18] = {0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0}; memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); } @@ -642,23 +641,23 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir) //or //(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){ + if (i < deltai && 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}; memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); } - else if ((deltai < gammai) < i){ + else if (deltai < gammai && gammai < i){ uint8_t rel_enc__[18] = {0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 1, 1, 0, 0}; memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); } - else if ((gammai < i) < deltai){ + else if (gammai < i && i < deltai){ uint8_t rel_enc__[18] = {0, 0, 1, 1, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0}; memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); } - else if ((i < gammai) < deltai){ + else if (i < gammai && gammai < deltai){ uint8_t rel_enc__[18] = {1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0}; memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); } - else if ((deltai < i) < gammai){ + else if (deltai < i && i < gammai){ uint8_t rel_enc__[18] = {0, 0, 1, 1, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0}; memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); } @@ -686,23 +685,23 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir) //or //(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){ + if (i < deltai && 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}; memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); } - else if ((deltai < gammai) < i){ + else if (deltai < gammai && gammai < i){ uint8_t rel_enc__[18] = {0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 1, 1, 0, 0}; memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); } - else if ((gammai < i) < deltai){ + else if (gammai < i && i < deltai){ uint8_t rel_enc__[18] = {1, 1, 0, 0, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0}; memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); } - else if ((i < gammai) < deltai){ + else if (i < gammai && gammai < deltai){ uint8_t rel_enc__[18] = {1, 1, 1, 1, 0, 0, 1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0}; memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); } - else if ((deltai < i) < gammai){ + else if (deltai < i && i < gammai){ uint8_t rel_enc__[18] = {0, 0, 1, 1, 0, 0, 1, 1, 1, 1, 0, 0, 1, 1, 0, 0, 0, 0}; memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); } @@ -719,40 +718,34 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir) //Agent Box Free -> Free Agent Box //(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 //(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 //(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 //(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 //(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 //(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){ + if (i < deltai && 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){ + else if (deltai < gammai && 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}; memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); } - else if ((gammai < i) < deltai){ + else if (gammai < i && 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}; memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); } - else if ((i < gammai) < deltai){ + else if (i < gammai && 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}; memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); } - else if ((deltai < i) < gammai){ + else if (deltai < i && 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}; memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); } @@ -769,40 +762,34 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir) //Agent Targbox Free -> Free Targagent Box //(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){ + if (i < deltai && 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}; memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); } - else if ((deltai < gammai) < i){ + else if (deltai < gammai && 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}; memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); } - else if ((gammai < i) < deltai){ + else if (gammai < i && 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}; memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); } - else if ((i < gammai) < deltai){ + else if (i < gammai && gammai < deltai){ uint8_t rel_enc__[18] = {1, 0, 0, 0, 1, 1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0, 0}; memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); } - else if ((deltai < i) < gammai){ + else if (deltai < i && 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}; memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); } @@ -819,40 +806,34 @@ 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){ + if (i < deltai && 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}; memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); } - else if ((deltai < gammai) < i){ + else if (deltai < gammai && gammai < i){ uint8_t rel_enc__[18] = {0, 1, 1, 0, 0, 1, 0, 1, 1, 0, 1, 0, 1, 0, 0, 0, 1, 1}; memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); } - else if ((gammai < i) < deltai){ + else if (gammai < i && i < deltai){ uint8_t rel_enc__[18] = {0, 1, 1, 0, 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){ + else if (i < gammai && gammai < deltai){ uint8_t rel_enc__[18] = {1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0, 0, 1, 1, 0, 0, 1}; memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); } - else if ((deltai < i) < gammai){ + else if (deltai < i && i < gammai){ uint8_t rel_enc__[18] = {0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0}; memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); } @@ -869,7 +850,6 @@ 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 @@ -881,23 +861,23 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir) //or //(0 1 1 0 1 0 1 1 0 1 0 0 1 0 0 0 1 1) relvarset1 = sylvan_set_fromarray(relvars1, 18); - if ((i < deltai) < gammai){ + if (i < deltai && deltai < gammai){ uint8_t rel_enc__[18] = {1, 0, 0, 0, 1, 1, 1, 1, 0, 1, 0, 0, 0, 1, 1, 0, 1, 0}; memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); } - else if ((deltai < gammai) < i){ + else if (deltai < gammai && gammai < i){ uint8_t rel_enc__[18] = {1, 1, 0, 1, 0, 0, 0, 1, 1, 0, 1, 0, 1, 0, 0, 0, 1, 1}; memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); } - else if ((gammai < i) < deltai){ + else if (gammai < i && i < deltai){ uint8_t rel_enc__[18] = {0, 1, 1, 0, 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){ + else if (i < gammai && gammai < deltai){ uint8_t rel_enc__[18] = {1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0, 0}; memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); } - else if ((deltai < i) < gammai){ + else if (deltai < i && i < gammai){ uint8_t rel_enc__[18] = {1, 1, 0, 1, 0, 0, 1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0}; memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); } @@ -914,40 +894,34 @@ 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){ + if (i < deltai && 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}; memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); } - else if ((deltai < gammai) < i){ + else if (deltai < gammai && gammai < i){ uint8_t rel_enc__[18] = {0, 1, 1, 0, 0, 1, 0, 0, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1}; memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); } - else if ((gammai < i) < deltai){ + else if (gammai < i && i < deltai){ uint8_t rel_enc__[18] = {0, 0, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 0, 1}; memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); } - else if ((i < gammai) < deltai){ + else if (i < gammai && gammai < deltai){ uint8_t rel_enc__[18] = {1, 0, 1, 1, 0, 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){ + else if (deltai < i && i < gammai){ uint8_t rel_enc__[18] = {0, 1, 1, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0, 0, 0, 1, 1, 0}; memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); } @@ -964,40 +938,34 @@ 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){ + if (i < deltai && 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}; memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); } - else if ((deltai < gammai) < i){ + else if (deltai < gammai && gammai < i){ uint8_t rel_enc__[18] = {1, 1, 0, 1, 0, 0, 0, 0, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1}; memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); } - else if ((gammai < i) < deltai){ + else if (gammai < i && i < deltai){ uint8_t rel_enc__[18] = {0, 0, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 1, 1, 0, 1, 0, 0}; memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); } - else if ((i < gammai) < deltai){ + else if (i < gammai && gammai < deltai){ uint8_t rel_enc__[18] = {1, 0, 1, 1, 0, 1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0, 0}; memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); } - else if ((deltai < i) < gammai){ + else if (deltai < i && 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}; memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); } @@ -1025,23 +993,23 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir) //or //(0 1 1 0 1 0 0 1 1 0 0 1 1 0 1 1 0 1) relvarset1 = sylvan_set_fromarray(relvars1, 18); - if ((i < deltai) < gammai){ + if (i < deltai && deltai < gammai){ uint8_t rel_enc__[18] = {1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 0, 1, 0, 1, 1, 0, 1, 0}; memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); } - else if ((deltai < gammai) < i){ + else if (deltai < gammai && gammai < i){ uint8_t rel_enc__[18] = {0, 1, 1, 0, 0, 1, 0, 1, 1, 0, 1, 0, 1, 0, 1, 1, 0, 1}; memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); } - else if ((gammai < i) < deltai){ + else if (gammai < i && i < deltai){ uint8_t rel_enc__[18] = {0, 1, 1, 0, 1, 0, 1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 0, 1}; memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); } - else if ((i < gammai) < deltai){ + else if (i < gammai && gammai < deltai){ uint8_t rel_enc__[18] = {1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0, 0, 1, 1, 0, 0, 1}; memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); } - else if ((deltai < i) < gammai){ + else if (deltai < i && i < gammai){ uint8_t rel_enc__[18] = {0, 1, 1, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0}; memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); } @@ -1058,41 +1026,34 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir) //Targagent Targbox Target -> Target Targagent Targbox //(1 0 1 1 0 1 1 1 0 1 0 0 0 1 1 0 1 0) - //(1 0 1 1 0 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 1 1 0 1) - //(1 1 0 1 0 0 0 1 1 0 1 0 1 0 1 1 0 1 //or //(0 1 1 0 1 0 1 0 1 1 0 1 1 1 0 1 0 0) - //(0 1 1 0 1 0 1 0 1 1 0 1 1 1 0 1 0 0 //or //(1 0 1 1 0 1 0 1 1 0 1 0 1 1 0 1 0 0) - //(1 0 1 1 0 1 0 1 1 0 1 0 1 1 0 1 0 0 //or //(1 1 0 1 0 0 1 0 1 1 0 1 0 1 1 0 1 0) - //(1 1 0 1 0 0 1 0 1 1 0 1 0 1 1 0 1 0 //or //(1 1 0 1 0 0 1 0 1 1 0 1 0 1 1 0 1 0) - //(0 1 1 0 1 0 1 1 0 1 0 0 1 0 1 1 0 1 - //(0 1 1 0 1 0 1 1 0 1 0 0 1 0 1 1 0 1 relvarset1 = sylvan_set_fromarray(relvars1, 18); - if ((i < deltai) < gammai){ + if (i < deltai && deltai < gammai){ uint8_t rel_enc__[18] = {1, 0, 1, 1, 0, 1, 1, 1, 0, 1, 0, 0, 0, 1, 1, 0, 1, 0}; memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); } - else if ((deltai < gammai) < i){ + else if (deltai < gammai && gammai < i){ uint8_t rel_enc__[18] = {1, 1, 0, 1, 0, 0, 0, 1, 1, 0, 1, 0, 1, 0, 1, 1, 0, 1}; memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); } - else if ((gammai < i) < deltai){ + else if (gammai < i && i < deltai){ uint8_t rel_enc__[18] = {0, 1, 1, 0, 1, 0, 1, 0, 1, 1, 0, 1, 1, 1, 0, 1, 0, 0}; memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); } - else if ((i < gammai) < deltai){ + else if (i < gammai && gammai < deltai){ uint8_t rel_enc__[18] = {1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0, 0}; memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); } - else if ((deltai < i) < gammai){ + else if (deltai < i && i < gammai){ uint8_t rel_enc__[18] = {1, 1, 0, 1, 0, 0, 1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0}; memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); } diff --git a/modelchecker/main.c b/modelchecker/main.c index 20ad57b..5ca9c87 100644 --- a/modelchecker/main.c +++ b/modelchecker/main.c @@ -61,6 +61,7 @@ void solve(FILE *inputstream) state *init = encode_screen(screen); rels *rls = encode_rel(screen); + //test_trans(init, rls->reld); BDD old = sylvan_false; BDD new = init->bdd; -- 2.20.1