From: Alexander Fedotov Date: Tue, 19 Apr 2016 18:01:37 +0000 (+0200) Subject: some checks X-Git-Url: https://git.martlubbers.net/?a=commitdiff_plain;h=82a071f2894cfcc59511458c69e8e59581055880;p=mc1516pa.git some checks --- diff --git a/modelchecker/coord.c b/modelchecker/coord.c index 5ff92e1..cd30e27 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}; @@ -539,16 +539,17 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir) //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) + //(0 0 1 1 0 0 0 0 1 1 0 0 1 1 0 0 1 1) (delta gamma i) //or - //(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 - //(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 - //(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 - //(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]; @@ -569,11 +570,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, 1, 1, 0, 0, 1}; + 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 { - uint8_t rel_enc__[18] = {1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0}; + 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)); } @@ -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) - //(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 - //(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 - //(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 - //(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 - //(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 - //(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}; @@ -718,16 +719,22 @@ 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){ uint8_t rel_enc__[18] = {1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 0, 1, 0, 0, 0, 1, 1, 0}; @@ -762,16 +769,22 @@ 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){ uint8_t rel_enc__[18] = {1, 0, 0, 0, 1, 1, 1, 1, 0, 1, 0, 0, 0, 0, 0, 1, 1, 0}; @@ -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};