From 3461b7c4dd08242328dd59b44c6ddbcc00af6a0e Mon Sep 17 00:00:00 2001
From: Alexander Fedotov <soyaxhoya@gmail.com>
Date: Thu, 7 Apr 2016 10:17:13 +0100
Subject: [PATCH 1/1] small update

---
 modelchecker/coord.c | 14 ++++++++++++++
 1 file changed, 14 insertions(+)

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;
-- 
2.20.1