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:
363cf73
)
small update
author
Alexander Fedotov
<soyaxhoya@gmail.com>
Thu, 7 Apr 2016 09:17:13 +0000
(10:17 +0100)
committer
Alexander Fedotov
<soyaxhoya@gmail.com>
Thu, 7 Apr 2016 09:17:13 +0000
(10:17 +0100)
modelchecker/coord.c
patch
|
blob
|
history
diff --git
a/modelchecker/coord.c
b/modelchecker/coord.c
index
4c19a60
..
68ad5a3
100644
(file)
--- a/
modelchecker/coord.c
+++ b/
modelchecker/coord.c
@@
-18,6
+18,20
@@
#include "sokoban.h"
#include "sokoban.h"
+/*
+ * Each coordinate has three related boolean variables. The combination of those boolean variables
+ * defines tiles:
+ * 000: Wall
+ * 001: Free
+ * 010: Box
+ * 100: Box on target
+ * 011: Target
+ * 101: Agent
+ * 110: Agent on target
+ * In the BDD representation, the state is represented by n * 3 variables, where n is the number of
+ * tiles in the shrinked screen.
+ */
+
BDD encode_screen(sokoban_screen *screen)
{
int num_tiles;
BDD encode_screen(sokoban_screen *screen)
{
int num_tiles;