diff --git a/LavaGap.prism b/LavaGap.prism
new file mode 100644
index 0000000..b011590
--- /dev/null
+++ b/LavaGap.prism
@@ -0,0 +1,28 @@
+mdp
+
+formula AgentCannotMoveEastWall = (colAgent=4&rowAgent=1) | (colAgent=4&rowAgent=2) | (colAgent=4&rowAgent=3) | (colAgent=4&rowAgent=4);
+formula AgentCannotMoveNorthWall = (colAgent=3&rowAgent=1) | (colAgent=4&rowAgent=1) | (colAgent=1&rowAgent=1) | (colAgent=2&rowAgent=1);
+formula AgentCannotMoveSouthWall = (colAgent=1&rowAgent=4) | (colAgent=3&rowAgent=4) | (colAgent=4&rowAgent=4) | (colAgent=2&rowAgent=4);
+formula AgentCannotMoveWestWall = (colAgent=1&rowAgent=2) | (colAgent=1&rowAgent=3) | (colAgent=1&rowAgent=4) | (colAgent=1&rowAgent=1);
+formula AgentIsOnSlippery = false;
+formula AgentIsOnLava = (colAgent=2&rowAgent=1) | (colAgent=2&rowAgent=3) | (colAgent=2&rowAgent=4);
+label "AgentIsOnLava" = AgentIsOnLava;
+formula AgentIsOnGoal = (colAgent=4&rowAgent=4);
+init
+  true
+endinit
+
+
+module Agent
+  colAgent : [1..4];
+  rowAgent : [1..4];
+  viewAgent : [0..3];
+
+  [Agent_turn_right] !AgentIsOnLava &true -> 1.000000: (viewAgent'=mod(viewAgent+1,4));
+  [Agent_turn_left] !AgentIsOnLava &viewAgent>0 -> 1.000000: (viewAgent'=viewAgent-1);
+  [Agent_turn_left] !AgentIsOnLava &viewAgent=0 -> 1.000000: (viewAgent'=3);
+  [Agent_move_North] viewAgent=3 & !AgentIsOnLava & !AgentIsOnGoal & !AgentCannotMoveNorthWall -> 1.000000: (rowAgent'=rowAgent-1);
+  [Agent_move_East] viewAgent=0 & !AgentIsOnLava & !AgentIsOnGoal & !AgentCannotMoveEastWall -> 1.000000: (colAgent'=colAgent+1);
+  [Agent_move_South] viewAgent=1 & !AgentIsOnLava & !AgentIsOnGoal & !AgentCannotMoveSouthWall -> 1.000000: (rowAgent'=rowAgent+1);
+  [Agent_move_West] viewAgent=2 & !AgentIsOnLava & !AgentIsOnGoal & !AgentCannotMoveWestWall -> 1.000000: (colAgent'=colAgent-1);
+endmodule
diff --git a/lavagap.dot b/lavagap.dot
new file mode 100644
index 0000000..630b5f2
--- /dev/null
+++ b/lavagap.dot
@@ -0,0 +1,743 @@
+digraph model {
+	0 [ label = "0[colAgent=1	& rowAgent=1	& viewAgent=0]
+: {init}" ];
+	1 [ label = "1[colAgent=2	& rowAgent=1	& viewAgent=0]
+: {AgentIsOnLava, deadlock
+init}", style=filled, color=red ];
+	2 [ label = "2[colAgent=3	& rowAgent=1	& viewAgent=0]
+: {init}" ];
+	3 [ label = "3[colAgent=4	& rowAgent=1	& viewAgent=0]
+: {init}" ];
+	4 [ label = "4[colAgent=2	& rowAgent=2	& viewAgent=0]
+: {init}" ];
+	5 [ label = "5[colAgent=3	& rowAgent=2	& viewAgent=0]
+: {init}" ];
+	6 [ label = "6[colAgent=4	& rowAgent=2	& viewAgent=0]
+: {init}" ];
+	7 [ label = "7[colAgent=2	& rowAgent=3	& viewAgent=0]
+: {AgentIsOnLava, deadlock
+init}", style=filled, color=red ];
+	8 [ label = "8[colAgent=3	& rowAgent=3	& viewAgent=0]
+: {init}" ];
+	9 [ label = "9[colAgent=4	& rowAgent=3	& viewAgent=0]
+: {init}" ];
+	10 [ label = "10[colAgent=2	& rowAgent=4	& viewAgent=0]
+: {AgentIsOnLava, deadlock
+init}", style=filled, color=red ];
+	11 [ label = "11[colAgent=3	& rowAgent=4	& viewAgent=0]
+: {init}" ];
+	12 [ label = "12[colAgent=4	& rowAgent=4	& viewAgent=0]
+: {init}" ];
+	13 [ label = "13[colAgent=2	& rowAgent=2	& viewAgent=1]
+: {init}" ];
+	14 [ label = "14[colAgent=3	& rowAgent=2	& viewAgent=1]
+: {init}" ];
+	15 [ label = "15[colAgent=4	& rowAgent=2	& viewAgent=1]
+: {init}" ];
+	16 [ label = "16[colAgent=2	& rowAgent=3	& viewAgent=1]
+: {AgentIsOnLava, deadlock
+init}", style=filled, color=red ];
+	17 [ label = "17[colAgent=3	& rowAgent=3	& viewAgent=1]
+: {init}" ];
+	18 [ label = "18[colAgent=4	& rowAgent=3	& viewAgent=1]
+: {init}" ];
+	19 [ label = "19[colAgent=2	& rowAgent=4	& viewAgent=1]
+: {AgentIsOnLava, deadlock
+init}", style=filled, color=red ];
+	20 [ label = "20[colAgent=3	& rowAgent=4	& viewAgent=1]
+: {init}" ];
+	21 [ label = "21[colAgent=4	& rowAgent=4	& viewAgent=1]
+: {init}" ];
+	22 [ label = "22[colAgent=2	& rowAgent=2	& viewAgent=2]
+: {init}" ];
+	23 [ label = "23[colAgent=3	& rowAgent=2	& viewAgent=2]
+: {init}" ];
+	24 [ label = "24[colAgent=4	& rowAgent=2	& viewAgent=2]
+: {init}" ];
+	25 [ label = "25[colAgent=2	& rowAgent=3	& viewAgent=2]
+: {AgentIsOnLava, deadlock
+init}", style=filled, color=red ];
+	26 [ label = "26[colAgent=3	& rowAgent=3	& viewAgent=2]
+: {init}" ];
+	27 [ label = "27[colAgent=4	& rowAgent=3	& viewAgent=2]
+: {init}" ];
+	28 [ label = "28[colAgent=2	& rowAgent=4	& viewAgent=2]
+: {AgentIsOnLava, deadlock
+init}", style=filled, color=red ];
+	29 [ label = "29[colAgent=3	& rowAgent=4	& viewAgent=2]
+: {init}" ];
+	30 [ label = "30[colAgent=4	& rowAgent=4	& viewAgent=2]
+: {init}" ];
+	31 [ label = "31[colAgent=2	& rowAgent=2	& viewAgent=3]
+: {init}" ];
+	32 [ label = "32[colAgent=3	& rowAgent=2	& viewAgent=3]
+: {init}" ];
+	33 [ label = "33[colAgent=4	& rowAgent=2	& viewAgent=3]
+: {init}" ];
+	34 [ label = "34[colAgent=2	& rowAgent=3	& viewAgent=3]
+: {AgentIsOnLava, deadlock
+init}", style=filled, color=red ];
+	35 [ label = "35[colAgent=3	& rowAgent=3	& viewAgent=3]
+: {init}" ];
+	36 [ label = "36[colAgent=4	& rowAgent=3	& viewAgent=3]
+: {init}" ];
+	37 [ label = "37[colAgent=2	& rowAgent=4	& viewAgent=3]
+: {AgentIsOnLava, deadlock
+init}", style=filled, color=red ];
+	38 [ label = "38[colAgent=3	& rowAgent=4	& viewAgent=3]
+: {init}" ];
+	39 [ label = "39[colAgent=4	& rowAgent=4	& viewAgent=3]
+: {init}" ];
+	40 [ label = "40[colAgent=1	& rowAgent=1	& viewAgent=1]
+: {}" ];
+	41 [ label = "41[colAgent=1	& rowAgent=1	& viewAgent=3]
+: {}" ];
+	42 [ label = "42[colAgent=3	& rowAgent=1	& viewAgent=1]
+: {}" ];
+	43 [ label = "43[colAgent=3	& rowAgent=1	& viewAgent=3]
+: {}" ];
+	44 [ label = "44[colAgent=4	& rowAgent=1	& viewAgent=1]
+: {}" ];
+	45 [ label = "45[colAgent=4	& rowAgent=1	& viewAgent=3]
+: {}" ];
+	46 [ label = "46[colAgent=1	& rowAgent=2	& viewAgent=2]
+: {}" ];
+	47 [ label = "47[colAgent=2	& rowAgent=1	& viewAgent=3]
+: {AgentIsOnLava, deadlock
+}", style=filled, color=red ];
+	48 [ label = "48[colAgent=1	& rowAgent=1	& viewAgent=2]
+: {}" ];
+	49 [ label = "49[colAgent=1	& rowAgent=2	& viewAgent=1]
+: {}" ];
+	50 [ label = "50[colAgent=3	& rowAgent=1	& viewAgent=2]
+: {}" ];
+	51 [ label = "51[colAgent=4	& rowAgent=1	& viewAgent=2]
+: {}" ];
+	52 [ label = "52[colAgent=1	& rowAgent=2	& viewAgent=3]
+: {}" ];
+	53 [ label = "53[colAgent=1	& rowAgent=2	& viewAgent=0]
+: {}" ];
+	54 [ label = "54[colAgent=1	& rowAgent=3	& viewAgent=1]
+: {}" ];
+	55 [ label = "55[colAgent=2	& rowAgent=1	& viewAgent=2]
+: {AgentIsOnLava, deadlock
+}", style=filled, color=red ];
+	56 [ label = "56[colAgent=1	& rowAgent=3	& viewAgent=2]
+: {}" ];
+	57 [ label = "57[colAgent=1	& rowAgent=3	& viewAgent=0]
+: {}" ];
+	58 [ label = "58[colAgent=1	& rowAgent=4	& viewAgent=1]
+: {}" ];
+	59 [ label = "59[colAgent=1	& rowAgent=3	& viewAgent=3]
+: {}" ];
+	60 [ label = "60[colAgent=1	& rowAgent=4	& viewAgent=2]
+: {}" ];
+	61 [ label = "61[colAgent=1	& rowAgent=4	& viewAgent=0]
+: {}" ];
+	62 [ label = "62[colAgent=1	& rowAgent=4	& viewAgent=3]
+: {}" ];
+	"0c0" [shape = "point"];
+	0 -> "0c0" [ label = "{Agent_turn_right}"]
+;
+	"0c0" -> 40 [ label= "1" ];
+	"0c1" [shape = "point"];
+	0 -> "0c1" [ label = "{Agent_turn_left}"]
+;
+	"0c1" -> 41 [ label= "1" ];
+	"0c2" [shape = "point"];
+	0 -> "0c2" [ label = "{Agent_move_East}"]
+;
+	"0c2" -> 1 [ label= "1" ];
+	"1c0" [shape = "point"];
+	1 -> "1c0" [ label = "{}"]
+;
+	"1c0" -> 1 [ label= "1" ];
+	"2c0" [shape = "point"];
+	2 -> "2c0" [ label = "{Agent_turn_right}"]
+;
+	"2c0" -> 42 [ label= "1" ];
+	"2c1" [shape = "point"];
+	2 -> "2c1" [ label = "{Agent_turn_left}"]
+;
+	"2c1" -> 43 [ label= "1" ];
+	"2c2" [shape = "point"];
+	2 -> "2c2" [ label = "{Agent_move_East}"]
+;
+	"2c2" -> 3 [ label= "1" ];
+	"3c0" [shape = "point"];
+	3 -> "3c0" [ label = "{Agent_turn_right}"]
+;
+	"3c0" -> 44 [ label= "1" ];
+	"3c1" [shape = "point"];
+	3 -> "3c1" [ label = "{Agent_turn_left}"]
+;
+	"3c1" -> 45 [ label= "1" ];
+	"4c0" [shape = "point"];
+	4 -> "4c0" [ label = "{Agent_turn_right}"]
+;
+	"4c0" -> 13 [ label= "1" ];
+	"4c1" [shape = "point"];
+	4 -> "4c1" [ label = "{Agent_turn_left}"]
+;
+	"4c1" -> 31 [ label= "1" ];
+	"4c2" [shape = "point"];
+	4 -> "4c2" [ label = "{Agent_move_East}"]
+;
+	"4c2" -> 5 [ label= "1" ];
+	"5c0" [shape = "point"];
+	5 -> "5c0" [ label = "{Agent_turn_right}"]
+;
+	"5c0" -> 14 [ label= "1" ];
+	"5c1" [shape = "point"];
+	5 -> "5c1" [ label = "{Agent_turn_left}"]
+;
+	"5c1" -> 32 [ label= "1" ];
+	"5c2" [shape = "point"];
+	5 -> "5c2" [ label = "{Agent_move_East}"]
+;
+	"5c2" -> 6 [ label= "1" ];
+	"6c0" [shape = "point"];
+	6 -> "6c0" [ label = "{Agent_turn_right}"]
+;
+	"6c0" -> 15 [ label= "1" ];
+	"6c1" [shape = "point"];
+	6 -> "6c1" [ label = "{Agent_turn_left}"]
+;
+	"6c1" -> 33 [ label= "1" ];
+	"7c0" [shape = "point"];
+	7 -> "7c0" [ label = "{}"]
+;
+	"7c0" -> 7 [ label= "1" ];
+	"8c0" [shape = "point"];
+	8 -> "8c0" [ label = "{Agent_turn_right}"]
+;
+	"8c0" -> 17 [ label= "1" ];
+	"8c1" [shape = "point"];
+	8 -> "8c1" [ label = "{Agent_turn_left}"]
+;
+	"8c1" -> 35 [ label= "1" ];
+	"8c2" [shape = "point"];
+	8 -> "8c2" [ label = "{Agent_move_East}"]
+;
+	"8c2" -> 9 [ label= "1" ];
+	"9c0" [shape = "point"];
+	9 -> "9c0" [ label = "{Agent_turn_right}"]
+;
+	"9c0" -> 18 [ label= "1" ];
+	"9c1" [shape = "point"];
+	9 -> "9c1" [ label = "{Agent_turn_left}"]
+;
+	"9c1" -> 36 [ label= "1" ];
+	"10c0" [shape = "point"];
+	10 -> "10c0" [ label = "{}"]
+;
+	"10c0" -> 10 [ label= "1" ];
+	"11c0" [shape = "point"];
+	11 -> "11c0" [ label = "{Agent_turn_right}"]
+;
+	"11c0" -> 20 [ label= "1" ];
+	"11c1" [shape = "point"];
+	11 -> "11c1" [ label = "{Agent_turn_left}"]
+;
+	"11c1" -> 38 [ label= "1" ];
+	"11c2" [shape = "point"];
+	11 -> "11c2" [ label = "{Agent_move_East}"]
+;
+	"11c2" -> 12 [ label= "1" ];
+	"12c0" [shape = "point"];
+	12 -> "12c0" [ label = "{Agent_turn_right}"]
+;
+	"12c0" -> 21 [ label= "1" ];
+	"12c1" [shape = "point"];
+	12 -> "12c1" [ label = "{Agent_turn_left}"]
+;
+	"12c1" -> 39 [ label= "1" ];
+	"13c0" [shape = "point"];
+	13 -> "13c0" [ label = "{Agent_turn_right}"]
+;
+	"13c0" -> 22 [ label= "1" ];
+	"13c1" [shape = "point"];
+	13 -> "13c1" [ label = "{Agent_turn_left}"]
+;
+	"13c1" -> 4 [ label= "1" ];
+	"13c2" [shape = "point"];
+	13 -> "13c2" [ label = "{Agent_move_South}"]
+;
+	"13c2" -> 16 [ label= "1" ];
+	"14c0" [shape = "point"];
+	14 -> "14c0" [ label = "{Agent_turn_right}"]
+;
+	"14c0" -> 23 [ label= "1" ];
+	"14c1" [shape = "point"];
+	14 -> "14c1" [ label = "{Agent_turn_left}"]
+;
+	"14c1" -> 5 [ label= "1" ];
+	"14c2" [shape = "point"];
+	14 -> "14c2" [ label = "{Agent_move_South}"]
+;
+	"14c2" -> 17 [ label= "1" ];
+	"15c0" [shape = "point"];
+	15 -> "15c0" [ label = "{Agent_turn_right}"]
+;
+	"15c0" -> 24 [ label= "1" ];
+	"15c1" [shape = "point"];
+	15 -> "15c1" [ label = "{Agent_turn_left}"]
+;
+	"15c1" -> 6 [ label= "1" ];
+	"15c2" [shape = "point"];
+	15 -> "15c2" [ label = "{Agent_move_South}"]
+;
+	"15c2" -> 18 [ label= "1" ];
+	"16c0" [shape = "point"];
+	16 -> "16c0" [ label = "{}"]
+;
+	"16c0" -> 16 [ label= "1" ];
+	"17c0" [shape = "point"];
+	17 -> "17c0" [ label = "{Agent_turn_right}"]
+;
+	"17c0" -> 26 [ label= "1" ];
+	"17c1" [shape = "point"];
+	17 -> "17c1" [ label = "{Agent_turn_left}"]
+;
+	"17c1" -> 8 [ label= "1" ];
+	"17c2" [shape = "point"];
+	17 -> "17c2" [ label = "{Agent_move_South}"]
+;
+	"17c2" -> 20 [ label= "1" ];
+	"18c0" [shape = "point"];
+	18 -> "18c0" [ label = "{Agent_turn_right}"]
+;
+	"18c0" -> 27 [ label= "1" ];
+	"18c1" [shape = "point"];
+	18 -> "18c1" [ label = "{Agent_turn_left}"]
+;
+	"18c1" -> 9 [ label= "1" ];
+	"18c2" [shape = "point"];
+	18 -> "18c2" [ label = "{Agent_move_South}"]
+;
+	"18c2" -> 21 [ label= "1" ];
+	"19c0" [shape = "point"];
+	19 -> "19c0" [ label = "{}"]
+;
+	"19c0" -> 19 [ label= "1" ];
+	"20c0" [shape = "point"];
+	20 -> "20c0" [ label = "{Agent_turn_right}"]
+;
+	"20c0" -> 29 [ label= "1" ];
+	"20c1" [shape = "point"];
+	20 -> "20c1" [ label = "{Agent_turn_left}"]
+;
+	"20c1" -> 11 [ label= "1" ];
+	"21c0" [shape = "point"];
+	21 -> "21c0" [ label = "{Agent_turn_right}"]
+;
+	"21c0" -> 30 [ label= "1" ];
+	"21c1" [shape = "point"];
+	21 -> "21c1" [ label = "{Agent_turn_left}"]
+;
+	"21c1" -> 12 [ label= "1" ];
+	"22c0" [shape = "point"];
+	22 -> "22c0" [ label = "{Agent_turn_right}"]
+;
+	"22c0" -> 31 [ label= "1" ];
+	"22c1" [shape = "point"];
+	22 -> "22c1" [ label = "{Agent_turn_left}"]
+;
+	"22c1" -> 13 [ label= "1" ];
+	"22c2" [shape = "point"];
+	22 -> "22c2" [ label = "{Agent_move_West}"]
+;
+	"22c2" -> 46 [ label= "1" ];
+	"23c0" [shape = "point"];
+	23 -> "23c0" [ label = "{Agent_turn_right}"]
+;
+	"23c0" -> 32 [ label= "1" ];
+	"23c1" [shape = "point"];
+	23 -> "23c1" [ label = "{Agent_turn_left}"]
+;
+	"23c1" -> 14 [ label= "1" ];
+	"23c2" [shape = "point"];
+	23 -> "23c2" [ label = "{Agent_move_West}"]
+;
+	"23c2" -> 22 [ label= "1" ];
+	"24c0" [shape = "point"];
+	24 -> "24c0" [ label = "{Agent_turn_right}"]
+;
+	"24c0" -> 33 [ label= "1" ];
+	"24c1" [shape = "point"];
+	24 -> "24c1" [ label = "{Agent_turn_left}"]
+;
+	"24c1" -> 15 [ label= "1" ];
+	"24c2" [shape = "point"];
+	24 -> "24c2" [ label = "{Agent_move_West}"]
+;
+	"24c2" -> 23 [ label= "1" ];
+	"25c0" [shape = "point"];
+	25 -> "25c0" [ label = "{}"]
+;
+	"25c0" -> 25 [ label= "1" ];
+	"26c0" [shape = "point"];
+	26 -> "26c0" [ label = "{Agent_turn_right}"]
+;
+	"26c0" -> 35 [ label= "1" ];
+	"26c1" [shape = "point"];
+	26 -> "26c1" [ label = "{Agent_turn_left}"]
+;
+	"26c1" -> 17 [ label= "1" ];
+	"26c2" [shape = "point"];
+	26 -> "26c2" [ label = "{Agent_move_West}"]
+;
+	"26c2" -> 25 [ label= "1" ];
+	"27c0" [shape = "point"];
+	27 -> "27c0" [ label = "{Agent_turn_right}"]
+;
+	"27c0" -> 36 [ label= "1" ];
+	"27c1" [shape = "point"];
+	27 -> "27c1" [ label = "{Agent_turn_left}"]
+;
+	"27c1" -> 18 [ label= "1" ];
+	"27c2" [shape = "point"];
+	27 -> "27c2" [ label = "{Agent_move_West}"]
+;
+	"27c2" -> 26 [ label= "1" ];
+	"28c0" [shape = "point"];
+	28 -> "28c0" [ label = "{}"]
+;
+	"28c0" -> 28 [ label= "1" ];
+	"29c0" [shape = "point"];
+	29 -> "29c0" [ label = "{Agent_turn_right}"]
+;
+	"29c0" -> 38 [ label= "1" ];
+	"29c1" [shape = "point"];
+	29 -> "29c1" [ label = "{Agent_turn_left}"]
+;
+	"29c1" -> 20 [ label= "1" ];
+	"29c2" [shape = "point"];
+	29 -> "29c2" [ label = "{Agent_move_West}"]
+;
+	"29c2" -> 28 [ label= "1" ];
+	"30c0" [shape = "point"];
+	30 -> "30c0" [ label = "{Agent_turn_right}"]
+;
+	"30c0" -> 39 [ label= "1" ];
+	"30c1" [shape = "point"];
+	30 -> "30c1" [ label = "{Agent_turn_left}"]
+;
+	"30c1" -> 21 [ label= "1" ];
+	"31c0" [shape = "point"];
+	31 -> "31c0" [ label = "{Agent_turn_right}"]
+;
+	"31c0" -> 4 [ label= "1" ];
+	"31c1" [shape = "point"];
+	31 -> "31c1" [ label = "{Agent_turn_left}"]
+;
+	"31c1" -> 22 [ label= "1" ];
+	"31c2" [shape = "point"];
+	31 -> "31c2" [ label = "{Agent_move_North}"]
+;
+	"31c2" -> 47 [ label= "1" ];
+	"32c0" [shape = "point"];
+	32 -> "32c0" [ label = "{Agent_turn_right}"]
+;
+	"32c0" -> 5 [ label= "1" ];
+	"32c1" [shape = "point"];
+	32 -> "32c1" [ label = "{Agent_turn_left}"]
+;
+	"32c1" -> 23 [ label= "1" ];
+	"32c2" [shape = "point"];
+	32 -> "32c2" [ label = "{Agent_move_North}"]
+;
+	"32c2" -> 43 [ label= "1" ];
+	"33c0" [shape = "point"];
+	33 -> "33c0" [ label = "{Agent_turn_right}"]
+;
+	"33c0" -> 6 [ label= "1" ];
+	"33c1" [shape = "point"];
+	33 -> "33c1" [ label = "{Agent_turn_left}"]
+;
+	"33c1" -> 24 [ label= "1" ];
+	"33c2" [shape = "point"];
+	33 -> "33c2" [ label = "{Agent_move_North}"]
+;
+	"33c2" -> 45 [ label= "1" ];
+	"34c0" [shape = "point"];
+	34 -> "34c0" [ label = "{}"]
+;
+	"34c0" -> 34 [ label= "1" ];
+	"35c0" [shape = "point"];
+	35 -> "35c0" [ label = "{Agent_turn_right}"]
+;
+	"35c0" -> 8 [ label= "1" ];
+	"35c1" [shape = "point"];
+	35 -> "35c1" [ label = "{Agent_turn_left}"]
+;
+	"35c1" -> 26 [ label= "1" ];
+	"35c2" [shape = "point"];
+	35 -> "35c2" [ label = "{Agent_move_North}"]
+;
+	"35c2" -> 32 [ label= "1" ];
+	"36c0" [shape = "point"];
+	36 -> "36c0" [ label = "{Agent_turn_right}"]
+;
+	"36c0" -> 9 [ label= "1" ];
+	"36c1" [shape = "point"];
+	36 -> "36c1" [ label = "{Agent_turn_left}"]
+;
+	"36c1" -> 27 [ label= "1" ];
+	"36c2" [shape = "point"];
+	36 -> "36c2" [ label = "{Agent_move_North}"]
+;
+	"36c2" -> 33 [ label= "1" ];
+	"37c0" [shape = "point"];
+	37 -> "37c0" [ label = "{}"]
+;
+	"37c0" -> 37 [ label= "1" ];
+	"38c0" [shape = "point"];
+	38 -> "38c0" [ label = "{Agent_turn_right}"]
+;
+	"38c0" -> 11 [ label= "1" ];
+	"38c1" [shape = "point"];
+	38 -> "38c1" [ label = "{Agent_turn_left}"]
+;
+	"38c1" -> 29 [ label= "1" ];
+	"38c2" [shape = "point"];
+	38 -> "38c2" [ label = "{Agent_move_North}"]
+;
+	"38c2" -> 35 [ label= "1" ];
+	"39c0" [shape = "point"];
+	39 -> "39c0" [ label = "{Agent_turn_right}"]
+;
+	"39c0" -> 12 [ label= "1" ];
+	"39c1" [shape = "point"];
+	39 -> "39c1" [ label = "{Agent_turn_left}"]
+;
+	"39c1" -> 30 [ label= "1" ];
+	"40c0" [shape = "point"];
+	40 -> "40c0" [ label = "{Agent_turn_right}"]
+;
+	"40c0" -> 48 [ label= "1" ];
+	"40c1" [shape = "point"];
+	40 -> "40c1" [ label = "{Agent_turn_left}"]
+;
+	"40c1" -> 0 [ label= "1" ];
+	"40c2" [shape = "point"];
+	40 -> "40c2" [ label = "{Agent_move_South}"]
+;
+	"40c2" -> 49 [ label= "1" ];
+	"41c0" [shape = "point"];
+	41 -> "41c0" [ label = "{Agent_turn_right}"]
+;
+	"41c0" -> 0 [ label= "1" ];
+	"41c1" [shape = "point"];
+	41 -> "41c1" [ label = "{Agent_turn_left}"]
+;
+	"41c1" -> 48 [ label= "1" ];
+	"42c0" [shape = "point"];
+	42 -> "42c0" [ label = "{Agent_turn_right}"]
+;
+	"42c0" -> 50 [ label= "1" ];
+	"42c1" [shape = "point"];
+	42 -> "42c1" [ label = "{Agent_turn_left}"]
+;
+	"42c1" -> 2 [ label= "1" ];
+	"42c2" [shape = "point"];
+	42 -> "42c2" [ label = "{Agent_move_South}"]
+;
+	"42c2" -> 14 [ label= "1" ];
+	"43c0" [shape = "point"];
+	43 -> "43c0" [ label = "{Agent_turn_right}"]
+;
+	"43c0" -> 2 [ label= "1" ];
+	"43c1" [shape = "point"];
+	43 -> "43c1" [ label = "{Agent_turn_left}"]
+;
+	"43c1" -> 50 [ label= "1" ];
+	"44c0" [shape = "point"];
+	44 -> "44c0" [ label = "{Agent_turn_right}"]
+;
+	"44c0" -> 51 [ label= "1" ];
+	"44c1" [shape = "point"];
+	44 -> "44c1" [ label = "{Agent_turn_left}"]
+;
+	"44c1" -> 3 [ label= "1" ];
+	"44c2" [shape = "point"];
+	44 -> "44c2" [ label = "{Agent_move_South}"]
+;
+	"44c2" -> 15 [ label= "1" ];
+	"45c0" [shape = "point"];
+	45 -> "45c0" [ label = "{Agent_turn_right}"]
+;
+	"45c0" -> 3 [ label= "1" ];
+	"45c1" [shape = "point"];
+	45 -> "45c1" [ label = "{Agent_turn_left}"]
+;
+	"45c1" -> 51 [ label= "1" ];
+	"46c0" [shape = "point"];
+	46 -> "46c0" [ label = "{Agent_turn_right}"]
+;
+	"46c0" -> 52 [ label= "1" ];
+	"46c1" [shape = "point"];
+	46 -> "46c1" [ label = "{Agent_turn_left}"]
+;
+	"46c1" -> 49 [ label= "1" ];
+	"47c0" [shape = "point"];
+	47 -> "47c0" [ label = "{}"]
+;
+	"47c0" -> 47 [ label= "1" ];
+	"48c0" [shape = "point"];
+	48 -> "48c0" [ label = "{Agent_turn_right}"]
+;
+	"48c0" -> 41 [ label= "1" ];
+	"48c1" [shape = "point"];
+	48 -> "48c1" [ label = "{Agent_turn_left}"]
+;
+	"48c1" -> 40 [ label= "1" ];
+	"49c0" [shape = "point"];
+	49 -> "49c0" [ label = "{Agent_turn_right}"]
+;
+	"49c0" -> 46 [ label= "1" ];
+	"49c1" [shape = "point"];
+	49 -> "49c1" [ label = "{Agent_turn_left}"]
+;
+	"49c1" -> 53 [ label= "1" ];
+	"49c2" [shape = "point"];
+	49 -> "49c2" [ label = "{Agent_move_South}"]
+;
+	"49c2" -> 54 [ label= "1" ];
+	"50c0" [shape = "point"];
+	50 -> "50c0" [ label = "{Agent_turn_right}"]
+;
+	"50c0" -> 43 [ label= "1" ];
+	"50c1" [shape = "point"];
+	50 -> "50c1" [ label = "{Agent_turn_left}"]
+;
+	"50c1" -> 42 [ label= "1" ];
+	"50c2" [shape = "point"];
+	50 -> "50c2" [ label = "{Agent_move_West}"]
+;
+	"50c2" -> 55 [ label= "1" ];
+	"51c0" [shape = "point"];
+	51 -> "51c0" [ label = "{Agent_turn_right}"]
+;
+	"51c0" -> 45 [ label= "1" ];
+	"51c1" [shape = "point"];
+	51 -> "51c1" [ label = "{Agent_turn_left}"]
+;
+	"51c1" -> 44 [ label= "1" ];
+	"51c2" [shape = "point"];
+	51 -> "51c2" [ label = "{Agent_move_West}"]
+;
+	"51c2" -> 50 [ label= "1" ];
+	"52c0" [shape = "point"];
+	52 -> "52c0" [ label = "{Agent_turn_right}"]
+;
+	"52c0" -> 53 [ label= "1" ];
+	"52c1" [shape = "point"];
+	52 -> "52c1" [ label = "{Agent_turn_left}"]
+;
+	"52c1" -> 46 [ label= "1" ];
+	"52c2" [shape = "point"];
+	52 -> "52c2" [ label = "{Agent_move_North}"]
+;
+	"52c2" -> 41 [ label= "1" ];
+	"53c0" [shape = "point"];
+	53 -> "53c0" [ label = "{Agent_turn_right}"]
+;
+	"53c0" -> 49 [ label= "1" ];
+	"53c1" [shape = "point"];
+	53 -> "53c1" [ label = "{Agent_turn_left}"]
+;
+	"53c1" -> 52 [ label= "1" ];
+	"53c2" [shape = "point"];
+	53 -> "53c2" [ label = "{Agent_move_East}"]
+;
+	"53c2" -> 4 [ label= "1" ];
+	"54c0" [shape = "point"];
+	54 -> "54c0" [ label = "{Agent_turn_right}"]
+;
+	"54c0" -> 56 [ label= "1" ];
+	"54c1" [shape = "point"];
+	54 -> "54c1" [ label = "{Agent_turn_left}"]
+;
+	"54c1" -> 57 [ label= "1" ];
+	"54c2" [shape = "point"];
+	54 -> "54c2" [ label = "{Agent_move_South}"]
+;
+	"54c2" -> 58 [ label= "1" ];
+	"55c0" [shape = "point"];
+	55 -> "55c0" [ label = "{}"]
+;
+	"55c0" -> 55 [ label= "1" ];
+	"56c0" [shape = "point"];
+	56 -> "56c0" [ label = "{Agent_turn_right}"]
+;
+	"56c0" -> 59 [ label= "1" ];
+	"56c1" [shape = "point"];
+	56 -> "56c1" [ label = "{Agent_turn_left}"]
+;
+	"56c1" -> 54 [ label= "1" ];
+	"57c0" [shape = "point"];
+	57 -> "57c0" [ label = "{Agent_turn_right}"]
+;
+	"57c0" -> 54 [ label= "1" ];
+	"57c1" [shape = "point"];
+	57 -> "57c1" [ label = "{Agent_turn_left}"]
+;
+	"57c1" -> 59 [ label= "1" ];
+	"57c2" [shape = "point"];
+	57 -> "57c2" [ label = "{Agent_move_East}"]
+;
+	"57c2" -> 7 [ label= "1" ];
+	"58c0" [shape = "point"];
+	58 -> "58c0" [ label = "{Agent_turn_right}"]
+;
+	"58c0" -> 60 [ label= "1" ];
+	"58c1" [shape = "point"];
+	58 -> "58c1" [ label = "{Agent_turn_left}"]
+;
+	"58c1" -> 61 [ label= "1" ];
+	"59c0" [shape = "point"];
+	59 -> "59c0" [ label = "{Agent_turn_right}"]
+;
+	"59c0" -> 57 [ label= "1" ];
+	"59c1" [shape = "point"];
+	59 -> "59c1" [ label = "{Agent_turn_left}"]
+;
+	"59c1" -> 56 [ label= "1" ];
+	"59c2" [shape = "point"];
+	59 -> "59c2" [ label = "{Agent_move_North}"]
+;
+	"59c2" -> 52 [ label= "1" ];
+	"60c0" [shape = "point"];
+	60 -> "60c0" [ label = "{Agent_turn_right}"]
+;
+	"60c0" -> 62 [ label= "1" ];
+	"60c1" [shape = "point"];
+	60 -> "60c1" [ label = "{Agent_turn_left}"]
+;
+	"60c1" -> 58 [ label= "1" ];
+	"61c0" [shape = "point"];
+	61 -> "61c0" [ label = "{Agent_turn_right}"]
+;
+	"61c0" -> 58 [ label= "1" ];
+	"61c1" [shape = "point"];
+	61 -> "61c1" [ label = "{Agent_turn_left}"]
+;
+	"61c1" -> 62 [ label= "1" ];
+	"61c2" [shape = "point"];
+	61 -> "61c2" [ label = "{Agent_move_East}"]
+;
+	"61c2" -> 10 [ label= "1" ];
+	"62c0" [shape = "point"];
+	62 -> "62c0" [ label = "{Agent_turn_right}"]
+;
+	"62c0" -> 61 [ label= "1" ];
+	"62c1" [shape = "point"];
+	62 -> "62c1" [ label = "{Agent_turn_left}"]
+;
+	"62c1" -> 60 [ label= "1" ];
+	"62c2" [shape = "point"];
+	62 -> "62c2" [ label = "{Agent_move_North}"]
+;
+	"62c2" -> 59 [ label= "1" ];
+}
diff --git a/lavagap.pdf b/lavagap.pdf
new file mode 100644
index 0000000..5b1daaf
Binary files /dev/null and b/lavagap.pdf differ
diff --git a/lavagap_with_phi.pdf b/lavagap_with_phi.pdf
new file mode 100644
index 0000000..71276c9
Binary files /dev/null and b/lavagap_with_phi.pdf differ