small update

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"
 
 
+/*
+ * 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;