repositories
/
mc1516pa.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
|
inline
| side by side (from parent 1:
d849640
)
some checks
author
Alexander Fedotov
<soyaxhoya@gmail.com>
Tue, 19 Apr 2016 18:01:37 +0000
(20:01 +0200)
committer
Alexander Fedotov
<soyaxhoya@gmail.com>
Tue, 19 Apr 2016 18:01:37 +0000
(20:01 +0200)
modelchecker/coord.c
patch
|
blob
|
history
diff --git
a/modelchecker/coord.c
b/modelchecker/coord.c
index
5ff92e1
..
cd30e27
100644
(file)
--- 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
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
//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};
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)
//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
//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
//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
//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
//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
//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];
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){
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 {
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));
}
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)
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
//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
//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
//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
//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
//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};
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)
//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)
//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)
//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)
//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)
//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)
//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};
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)
//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)
//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)
//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)
//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)
//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)
//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};
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)
//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)
//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)
//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)
//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)
//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)
//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};
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};