X-Git-Url: https://git.martlubbers.net/?a=blobdiff_plain;ds=sidebyside;f=modelchecker%2Fcoord.c;h=68ad5a3ae0715810355e31bbf6e84f9ed2d46b8d;hb=3461b7c4dd08242328dd59b44c6ddbcc00af6a0e;hp=4c19a604e0719559332e1af0ec03288f58b84bf9;hpb=363cf737b04fbeab89362b6252b97db10d25ca02;p=mc1516pa.git

diff --git a/modelchecker/coord.c b/modelchecker/coord.c
index 4c19a60..68ad5a3 100644
--- a/modelchecker/coord.c
+++ b/modelchecker/coord.c
@@ -18,6 +18,20 @@
 #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;