From: Alexander Fedotov <soyaxhoya@gmail.com>
Date: Thu, 7 Apr 2016 09:17:13 +0000 (+0100)
Subject: small update
X-Git-Url: https://git.martlubbers.net/?a=commitdiff_plain;h=3461b7c4dd08242328dd59b44c6ddbcc00af6a0e;p=mc1516pa.git

small update
---

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;