working exercise2

diff --git a/uppaal/2.xml b/uppaal/2.xml
index 25de23c..0f68e2c 100644 (file)
--- a/uppaal/2.xml
+++ b/uppaal/2.xml
@@ -6,8 +6,10 @@
 //const int N=13;
 // Advanced
 //const int N = 7;
-//easy test puzzle
-const int N=3;
+//hard from website 1
+const int N=13;
+//hard from website 2
+//const int N=9;
 
 typedef int[0, N-1] id_c;
 
@@ -248,13 +250,15 @@ x:=x-1</label>
 
 
 //easy test puzzle
+/*
 RED = RedCar(0,2);
 V1 = VertCar(2, 1, 4, 3);
 V2 = VertCar(3, 2, 5, 2);
 system RED, V1, V2, Player;
+*/
 
 // Intermediate puzzle
-/*
+
 H1 = HorzCar(2, 0, 0, 5);
 H2 = HorzCar(2, 1, 2, 5);
 V3 = VertCar(2, 2, 4, 4);
@@ -269,7 +273,7 @@ VB = VertCar(2, 10, 3, 0);
 HC = HorzCar(2, 11, 4, 1);
 HD = HorzCar(2, 12, 4, 0);
 system H1, H2, V3, V4, V5, V6, H7, RED, V9, HA, VB, HC, HD, Player;
-*/
+
 
 // Advanced puzzle
 /*
@@ -277,12 +281,44 @@ H1 = HorzCar(2, 0, 0, 5);
 V2 = VertCar(2, 1, 2, 4);
 V3 = VertCar(3, 2, 3, 3);
 V4 = VertCar(3, 3, 0, 2);
-H5 = HorzCar(2, 4, 1, 3);
+RED = RedCar(4, 1);
 H6 = HorzCar(3, 5, 1, 2);
 H7 = HorzCar(3, 6, 3, 0);
-system H1, V2, V3, V4, H5, H6, H7
+system H1, V2, V3, V4, RED, H6, H7, Player;
+*/
+
+//Hard from website 1
+//Can not be solved
+/*
+V1 = VertCar(2, 0, 0, 3);
+V2 = VertCar(2, 1, 1, 0);
+V3 = VertCar(2, 2, 2, 1);
+V4 = VertCar(2, 3, 3, 4);
+V5 = VertCar(3, 4, 4, 3);
+V6 = VertCar(3, 5, 5, 3);
+H7 = HorzCar(2, 6, 0, 2);
+H8 = HorzCar(3, 7, 0, 5);
+H85= HorzCar(3,12, 1, 4); 
+H9 = HorzCar(2, 8, 2, 0);
+RED = RedCar(9, 2);
+HB = HorzCar(2,10, 4, 0);
+HC = HorzCar(2,11, 4, 1);
+system V1, V2, V3, V4, V5, V6, H7, H8, H85, H9, RED, HB, HC, Player;
 */
-    </system>\r
+
+//Hard from website 2
+/*
+V1 = VertCar(2, 0, 0, 0);
+V2 = VertCar(3, 1, 2, 3);
+V3 = VertCar(3, 2, 3, 0);
+V4 = VertCar(3, 3, 5, 3);
+H5 = HorzCar(2, 4, 1, 1);
+RED = RedCar(5, 3);
+H7 = HorzCar(2, 6, 3, 5);
+H8 = HorzCar(2, 7, 4, 0);
+H9 = HorzCar(2, 8, 4, 2);
+system V1, V2, V3, V4, H5, RED, H7, H8, H9, Player;
+*/</system>\r
        <queries>\r
                <query>\r
                        <formula>E&lt;&gt; Player.done == 1\r

diff --git a/uppaal/2hardTrace.xtr b/uppaal/2hardTrace.xtr
new file mode 100644 (file)
index 0000000..5a33f61
--- /dev/null
+++ b/uppaal/2hardTrace.xtr
@@ -0,0 +1,4245 @@
+1
+1
+1
+1
+5
+1
+1
+2
+.
+.
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+2
+0
+2
+4
+3
+3
+3
+2
+1
+3
+1
+3
+3
+0
+0
+.
+0
+1
+1
+1
+5
+1
+1
+2
+.
+.
+0
+0
+0
+0
+0
+1
+0
+0
+0
+0
+0
+1
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+2
+0
+2
+4
+3
+3
+3
+2
+1
+3
+1
+3
+3
+1
+0
+.
+0 1 ;
+7 2 ;
+.
+0
+0
+1
+1
+5
+1
+1
+2
+.
+.
+0
+0
+0
+0
+0
+1
+0
+0
+0
+0
+0
+1
+0
+0
+0
+0
+1
+1
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+2
+0
+2
+4
+3
+3
+3
+2
+1
+3
+1
+3
+3
+2
+0
+.
+1 1 ;
+7 2 ;
+.
+0
+0
+0
+1
+5
+1
+1
+2
+.
+.
+0
+0
+0
+0
+0
+1
+0
+0
+0
+0
+0
+1
+0
+0
+0
+0
+1
+1
+0
+0
+0
+1
+1
+1
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+2
+0
+2
+4
+3
+3
+3
+2
+1
+3
+1
+3
+3
+3
+0
+.
+2 1 ;
+7 2 ;
+.
+0
+0
+0
+0
+5
+1
+1
+2
+.
+.
+0
+0
+1
+1
+1
+1
+0
+0
+0
+0
+0
+1
+0
+0
+0
+0
+1
+1
+0
+0
+0
+1
+1
+1
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+2
+0
+2
+4
+3
+3
+3
+2
+1
+3
+1
+3
+3
+4
+0
+.
+3 1 ;
+7 2 ;
+.
+0
+0
+0
+0
+4
+1
+1
+2
+.
+.
+0
+0
+1
+1
+1
+1
+0
+0
+0
+1
+0
+1
+0
+0
+0
+1
+1
+1
+0
+0
+0
+1
+1
+1
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+2
+0
+2
+4
+3
+3
+3
+2
+1
+3
+1
+3
+3
+5
+0
+.
+4 9 ;
+7 2 ;
+.
+0
+0
+0
+0
+4
+0
+1
+2
+.
+.
+0
+0
+1
+1
+1
+1
+0
+0
+1
+1
+0
+1
+0
+0
+1
+1
+1
+1
+0
+0
+1
+1
+1
+1
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+2
+0
+2
+4
+3
+3
+3
+2
+1
+3
+1
+3
+3
+6
+0
+.
+5 1 ;
+7 2 ;
+.
+0
+0
+0
+0
+4
+0
+0
+2
+.
+.
+0
+0
+1
+1
+1
+1
+0
+0
+1
+1
+0
+1
+0
+0
+1
+1
+1
+1
+1
+0
+1
+1
+1
+1
+1
+0
+0
+0
+0
+0
+1
+0
+0
+0
+0
+0
+2
+0
+2
+4
+3
+3
+3
+2
+1
+3
+1
+3
+3
+7
+0
+.
+6 1 ;
+7 2 ;
+.
+2
+2
+2
+2
+3
+2
+2
+1
+.
+.
+0
+0
+1
+1
+1
+1
+0
+0
+1
+1
+0
+1
+0
+0
+1
+1
+1
+1
+1
+0
+1
+1
+1
+1
+1
+0
+0
+0
+0
+0
+1
+0
+0
+0
+0
+0
+2
+0
+2
+4
+3
+3
+3
+2
+1
+3
+1
+3
+3
+7
+0
+.
+7 1 ;
+0 0 ;
+1 0 ;
+2 0 ;
+3 0 ;
+4 8 ;
+5 0 ;
+6 0 ;
+.
+2
+2
+2
+2
+0
+2
+2
+1
+.
+.
+0
+0
+1
+1
+1
+1
+0
+0
+1
+1
+0
+1
+0
+0
+1
+1
+1
+1
+1
+0
+1
+1
+1
+1
+1
+0
+0
+0
+0
+0
+1
+0
+0
+0
+0
+0
+2
+0
+2
+4
+3
+3
+3
+2
+1
+3
+1
+3
+3
+7
+0
+.
+4 4 ;
+4 6 ;
+.
+2
+2
+2
+2
+0
+2
+2
+1
+.
+.
+0
+1
+1
+1
+0
+1
+0
+0
+1
+1
+0
+1
+0
+0
+1
+1
+1
+1
+1
+0
+1
+1
+1
+1
+1
+0
+0
+0
+0
+0
+1
+0
+0
+0
+0
+0
+2
+0
+2
+4
+3
+3
+3
+1
+1
+3
+1
+3
+3
+7
+0
+.
+3 2 ;
+.
+2
+2
+2
+2
+0
+2
+2
+1
+.
+.
+1
+1
+1
+0
+0
+1
+0
+0
+1
+1
+0
+1
+0
+0
+1
+1
+1
+1
+1
+0
+1
+1
+1
+1
+1
+0
+0
+0
+0
+0
+1
+0
+0
+0
+0
+0
+2
+0
+2
+4
+3
+3
+3
+0
+1
+3
+1
+3
+3
+7
+0
+.
+3 2 ;
+.
+2
+2
+2
+2
+0
+2
+2
+1
+.
+.
+1
+1
+1
+0
+0
+1
+0
+0
+0
+1
+0
+1
+0
+0
+1
+1
+1
+1
+1
+0
+1
+1
+1
+1
+1
+0
+1
+0
+0
+0
+1
+0
+0
+0
+0
+0
+2
+0
+2
+4
+3
+3
+3
+0
+1
+3
+2
+3
+3
+7
+0
+.
+5 3 ;
+.
+2
+2
+2
+2
+0
+2
+2
+1
+.
+.
+1
+1
+1
+0
+0
+1
+0
+0
+0
+1
+0
+1
+0
+0
+0
+1
+1
+1
+1
+0
+1
+1
+1
+1
+1
+0
+1
+0
+0
+0
+1
+0
+1
+0
+0
+0
+2
+0
+2
+4
+3
+3
+3
+0
+1
+3
+3
+3
+3
+7
+0
+.
+5 3 ;
+.
+2
+2
+2
+2
+3
+2
+2
+1
+.
+.
+1
+1
+1
+1
+0
+1
+0
+0
+0
+1
+0
+1
+0
+0
+0
+0
+1
+1
+1
+0
+1
+1
+1
+1
+1
+0
+1
+0
+0
+0
+1
+0
+1
+0
+0
+0
+2
+0
+2
+4
+3
+3
+3
+0
+0
+3
+3
+3
+3
+7
+0
+.
+4 3 ;
+.
+2
+2
+2
+2
+1
+2
+2
+1
+.
+.
+1
+1
+1
+1
+0
+1
+0
+0
+0
+1
+0
+1
+0
+0
+0
+0
+1
+1
+1
+0
+1
+1
+1
+1
+1
+0
+1
+0
+0
+0
+1
+0
+1
+0
+0
+0
+2
+0
+2
+4
+3
+3
+3
+0
+0
+3
+3
+3
+3
+7
+0
+.
+4 5 ;
+4 6 ;
+.
+2
+2
+2
+2
+1
+2
+2
+1
+.
+.
+1
+1
+1
+1
+0
+1
+0
+0
+0
+1
+0
+1
+0
+0
+0
+1
+1
+0
+1
+0
+1
+1
+1
+1
+1
+0
+1
+0
+0
+0
+1
+0
+1
+0
+0
+0
+2
+0
+2
+3
+3
+3
+3
+0
+0
+3
+3
+3
+3
+7
+0
+.
+1 2 ;
+.
+2
+2
+2
+2
+1
+2
+2
+1
+.
+.
+1
+1
+1
+1
+0
+1
+0
+0
+0
+1
+0
+1
+0
+0
+1
+1
+0
+0
+1
+0
+1
+1
+1
+1
+1
+0
+1
+0
+0
+0
+1
+0
+1
+0
+0
+0
+2
+0
+2
+2
+3
+3
+3
+0
+0
+3
+3
+3
+3
+7
+0
+.
+1 2 ;
+.
+2
+2
+2
+2
+1
+2
+2
+1
+.
+.
+1
+1
+1
+1
+0
+1
+0
+0
+0
+1
+0
+1
+0
+1
+1
+0
+0
+0
+1
+0
+1
+1
+1
+1
+1
+0
+1
+0
+0
+0
+1
+0
+1
+0
+0
+0
+2
+0
+2
+1
+3
+3
+3
+0
+0
+3
+3
+3
+3
+7
+0
+.
+1 2 ;
+.
+2
+2
+2
+2
+1
+2
+2
+1
+.
+.
+1
+1
+1
+1
+0
+1
+0
+0
+0
+1
+0
+1
+1
+1
+0
+0
+0
+0
+1
+0
+1
+1
+1
+1
+1
+0
+1
+0
+0
+0
+1
+0
+1
+0
+0
+0
+2
+0
+2
+0
+3
+3
+3
+0
+0
+3
+3
+3
+3
+7
+0
+.
+1 2 ;
+.
+2
+2
+2
+2
+1
+2
+2
+1
+.
+.
+1
+1
+1
+1
+0
+1
+0
+0
+0
+1
+0
+1
+1
+1
+1
+0
+0
+0
+1
+0
+1
+1
+1
+1
+1
+0
+1
+0
+0
+0
+1
+0
+0
+0
+0
+0
+2
+0
+2
+0
+3
+3
+3
+0
+0
+3
+2
+3
+3
+7
+0
+.
+5 2 ;
+.
+2
+2
+2
+2
+1
+2
+2
+1
+.
+.
+1
+1
+1
+1
+0
+1
+0
+0
+1
+1
+0
+1
+1
+1
+1
+0
+0
+0
+1
+0
+1
+1
+1
+1
+1
+0
+0
+0
+0
+0
+1
+0
+0
+0
+0
+0
+2
+0
+2
+0
+3
+3
+3
+0
+0
+3
+1
+3
+3
+7
+0
+.
+5 2 ;
+.
+2
+2
+2
+2
+1
+2
+2
+1
+.
+.
+1
+1
+1
+1
+0
+0
+0
+0
+1
+1
+0
+1
+1
+1
+1
+0
+0
+1
+1
+0
+1
+1
+1
+1
+1
+0
+0
+0
+0
+0
+1
+0
+0
+0
+0
+0
+2
+1
+2
+0
+3
+3
+3
+0
+0
+3
+1
+3
+3
+7
+0
+.
+0 3 ;
+.
+2
+2
+2
+2
+3
+2
+2
+1
+.
+.
+1
+1
+1
+0
+0
+0
+0
+0
+1
+1
+0
+1
+1
+1
+1
+1
+0
+1
+1
+0
+1
+1
+1
+1
+1
+0
+0
+0
+0
+0
+1
+0
+0
+0
+0
+0
+2
+1
+2
+0
+3
+3
+3
+0
+1
+3
+1
+3
+3
+7
+0
+.
+4 2 ;
+.
+2
+2
+2
+2
+0
+2
+2
+1
+.
+.
+1
+1
+1
+0
+0
+0
+0
+0
+1
+1
+0
+1
+1
+1
+1
+1
+0
+1
+1
+0
+1
+1
+1
+1
+1
+0
+0
+0
+0
+0
+1
+0
+0
+0
+0
+0
+2
+1
+2
+0
+3
+3
+3
+0
+1
+3
+1
+3
+3
+7
+0
+.
+4 4 ;
+4 6 ;
+.
+2
+2
+2
+2
+0
+2
+2
+1
+.
+.
+0
+1
+1
+1
+0
+0
+0
+0
+1
+1
+0
+1
+1
+1
+1
+1
+0
+1
+1
+0
+1
+1
+1
+1
+1
+0
+0
+0
+0
+0
+1
+0
+0
+0
+0
+0
+2
+1
+2
+0
+3
+3
+3
+1
+1
+3
+1
+3
+3
+7
+0
+.
+3 3 ;
+.
+2
+2
+2
+2
+0
+2
+2
+1
+.
+.
+0
+0
+1
+1
+1
+0
+0
+0
+1
+1
+0
+1
+1
+1
+1
+1
+0
+1
+1
+0
+1
+1
+1
+1
+1
+0
+0
+0
+0
+0
+1
+0
+0
+0
+0
+0
+2
+1
+2
+0
+3
+3
+3
+2
+1
+3
+1
+3
+3
+7
+0
+.
+3 3 ;
+.
+2
+2
+2
+2
+0
+2
+2
+1
+.
+.
+0
+0
+0
+1
+1
+1
+0
+0
+1
+1
+0
+1
+1
+1
+1
+1
+0
+1
+1
+0
+1
+1
+1
+1
+1
+0
+0
+0
+0
+0
+1
+0
+0
+0
+0
+0
+2
+1
+2
+0
+3
+3
+3
+3
+1
+3
+1
+3
+3
+7
+0
+.
+3 3 ;
+.
+2
+2
+2
+2
+0
+2
+2
+1
+.
+.
+0
+0
+1
+1
+1
+1
+0
+0
+1
+1
+0
+1
+1
+1
+1
+1
+0
+1
+1
+0
+0
+1
+1
+1
+1
+0
+0
+0
+0
+0
+1
+0
+0
+0
+0
+0
+2
+1
+2
+0
+3
+3
+3
+3
+1
+3
+0
+3
+3
+7
+0
+.
+5 2 ;
+.
+2
+2
+2
+2
+0
+2
+2
+1
+.
+.
+0
+0
+1
+1
+1
+1
+0
+0
+1
+1
+0
+1
+1
+1
+1
+1
+0
+1
+1
+0
+1
+1
+1
+0
+1
+0
+0
+0
+0
+0
+1
+0
+0
+0
+0
+0
+2
+1
+2
+0
+3
+2
+3
+3
+1
+3
+0
+3
+3
+7
+0
+.
+2 2 ;
+.
+2
+2
+2
+2
+0
+2
+2
+1
+.
+.
+0
+0
+1
+1
+1
+1
+0
+0
+1
+1
+0
+0
+1
+1
+1
+1
+0
+1
+1
+0
+1
+1
+1
+1
+1
+0
+0
+0
+0
+0
+1
+0
+0
+0
+0
+0
+2
+2
+2
+0
+3
+2
+3
+3
+1
+3
+0
+3
+3
+7
+0
+.
+0 3 ;
+.
+2
+2
+2
+2
+0
+2
+2
+1
+.
+.
+0
+0
+1
+1
+1
+1
+0
+0
+1
+1
+0
+0
+1
+1
+1
+1
+0
+0
+1
+0
+1
+1
+1
+1
+1
+0
+0
+0
+0
+1
+1
+0
+0
+0
+0
+0
+2
+3
+2
+0
+3
+2
+3
+3
+1
+3
+0
+3
+3
+7
+0
+.
+0 3 ;
+.
+2
+2
+2
+2
+0
+2
+2
+1
+.
+.
+0
+0
+1
+1
+1
+1
+0
+0
+1
+1
+0
+0
+1
+1
+1
+1
+0
+0
+1
+0
+1
+1
+1
+0
+1
+0
+0
+0
+0
+1
+1
+0
+0
+0
+0
+1
+2
+4
+2
+0
+3
+2
+3
+3
+1
+3
+0
+3
+3
+7
+0
+.
+0 3 ;
+.
+2
+2
+2
+2
+0
+2
+2
+1
+.
+.
+0
+0
+1
+1
+1
+1
+0
+0
+1
+1
+0
+0
+1
+1
+1
+1
+0
+0
+1
+0
+0
+1
+1
+1
+1
+0
+0
+0
+0
+1
+1
+0
+0
+0
+0
+1
+2
+4
+2
+0
+3
+3
+3
+3
+1
+3
+0
+3
+3
+7
+0
+.
+2 3 ;
+.
+2
+2
+2
+2
+0
+2
+2
+1
+.
+.
+0
+0
+0
+1
+1
+1
+0
+0
+1
+1
+0
+0
+1
+1
+1
+1
+0
+0
+1
+0
+1
+1
+1
+1
+1
+0
+0
+0
+0
+1
+1
+0
+0
+0
+0
+1
+2
+4
+2
+0
+3
+3
+3
+3
+1
+3
+1
+3
+3
+7
+0
+.
+5 3 ;
+.
+2
+2
+2
+2
+0
+2
+2
+1
+.
+.
+0
+0
+1
+1
+1
+0
+0
+0
+1
+1
+0
+0
+1
+1
+1
+1
+0
+0
+1
+0
+1
+1
+1
+1
+1
+0
+0
+0
+0
+1
+1
+0
+0
+0
+0
+1
+2
+4
+2
+0
+3
+3
+3
+2
+1
+3
+1
+3
+3
+7
+0
+.
+3 2 ;
+.
+2
+2
+2
+2
+0
+2
+2
+1
+.
+.
+0
+1
+1
+1
+0
+0
+0
+0
+1
+1
+0
+0
+1
+1
+1
+1
+0
+0
+1
+0
+1
+1
+1
+1
+1
+0
+0
+0
+0
+1
+1
+0
+0
+0
+0
+1
+2
+4
+2
+0
+3
+3
+3
+1
+1
+3
+1
+3
+3
+7
+0
+.
+3 2 ;
+.
+2
+2
+2
+2
+0
+2
+2
+1
+.
+.
+1
+1
+1
+0
+0
+0
+0
+0
+1
+1
+0
+0
+1
+1
+1
+1
+0
+0
+1
+0
+1
+1
+1
+1
+1
+0
+0
+0
+0
+1
+1
+0
+0
+0
+0
+1
+2
+4
+2
+0
+3
+3
+3
+0
+1
+3
+1
+3
+3
+7
+0
+.
+3 2 ;
+.
+2
+2
+2
+2
+0
+2
+2
+1
+.
+.
+1
+1
+1
+0
+0
+0
+0
+0
+0
+1
+0
+0
+1
+1
+1
+1
+0
+0
+1
+0
+1
+1
+1
+1
+1
+0
+1
+0
+0
+1
+1
+0
+0
+0
+0
+1
+2
+4
+2
+0
+3
+3
+3
+0
+1
+3
+2
+3
+3
+7
+0
+.
+5 3 ;
+.
+2
+2
+2
+2
+0
+2
+2
+1
+.
+.
+1
+1
+1
+0
+0
+0
+0
+0
+0
+1
+0
+0
+1
+1
+0
+1
+0
+0
+1
+0
+1
+1
+1
+1
+1
+0
+1
+0
+0
+1
+1
+0
+1
+0
+0
+1
+2
+4
+2
+0
+3
+3
+3
+0
+1
+3
+3
+3
+3
+7
+0
+.
+5 3 ;
+.
+2
+2
+2
+2
+0
+2
+2
+1
+.
+.
+1
+1
+1
+0
+0
+0
+0
+0
+0
+1
+0
+0
+0
+1
+1
+1
+0
+0
+1
+0
+1
+1
+1
+1
+1
+0
+1
+0
+0
+1
+1
+0
+1
+0
+0
+1
+2
+4
+2
+1
+3
+3
+3
+0
+1
+3
+3
+3
+3
+7
+0
+.
+1 3 ;
+.
+2
+2
+2
+2
+0
+2
+2
+1
+.
+.
+1
+1
+1
+0
+0
+0
+0
+0
+0
+1
+0
+0
+1
+1
+1
+1
+0
+0
+1
+0
+1
+1
+1
+1
+1
+0
+1
+0
+0
+1
+0
+0
+1
+0
+0
+1
+2
+4
+2
+1
+3
+3
+3
+0
+1
+3
+3
+3
+2
+7
+0
+.
+6 2 ;
+.
+2
+2
+2
+2
+0
+2
+2
+1
+.
+.
+1
+1
+1
+0
+0
+0
+1
+0
+0
+1
+0
+0
+1
+1
+1
+1
+0
+0
+1
+0
+1
+1
+1
+1
+0
+0
+1
+0
+0
+1
+0
+0
+1
+0
+0
+1
+2
+4
+2
+1
+3
+3
+3
+0
+1
+3
+3
+3
+1
+7
+0
+.
+6 2 ;
+.
+2
+2
+2
+2
+3
+2
+2
+1
+.
+.
+1
+1
+1
+1
+0
+0
+1
+0
+0
+1
+0
+0
+1
+1
+1
+0
+0
+0
+1
+0
+1
+1
+1
+1
+0
+0
+1
+0
+0
+1
+0
+0
+1
+0
+0
+1
+2
+4
+2
+1
+3
+3
+3
+0
+0
+3
+3
+3
+1
+7
+0
+.
+4 3 ;
+.
+2
+2
+2
+2
+1
+2
+2
+1
+.
+.
+1
+1
+1
+1
+0
+0
+1
+0
+0
+1
+0
+0
+1
+1
+1
+0
+0
+0
+1
+0
+1
+1
+1
+1
+0
+0
+1
+0
+0
+1
+0
+0
+1
+0
+0
+1
+2
+4
+2
+1
+3
+3
+3
+0
+0
+3
+3
+3
+1
+7
+0
+.
+4 5 ;
+4 6 ;
+.
+2
+2
+2
+2
+1
+2
+2
+1
+.
+.
+1
+1
+1
+1
+0
+0
+1
+0
+0
+1
+0
+0
+1
+0
+1
+1
+0
+0
+1
+0
+1
+1
+1
+1
+0
+0
+1
+0
+0
+1
+0
+0
+1
+0
+0
+1
+2
+4
+2
+2
+3
+3
+3
+0
+0
+3
+3
+3
+1
+7
+0
+.
+1 3 ;
+.
+2
+2
+2
+2
+1
+2
+2
+1
+.
+.
+1
+1
+1
+1
+0
+0
+1
+0
+0
+1
+0
+0
+1
+0
+0
+1
+1
+0
+1
+0
+1
+1
+1
+1
+0
+0
+1
+0
+0
+1
+0
+0
+1
+0
+0
+1
+2
+4
+2
+3
+3
+3
+3
+0
+0
+3
+3
+3
+1
+7
+0
+.
+1 3 ;
+.
+2
+2
+2
+2
+1
+2
+2
+1
+.
+.
+1
+1
+1
+1
+0
+0
+1
+0
+0
+1
+0
+0
+1
+0
+0
+0
+1
+1
+1
+0
+1
+1
+1
+1
+0
+0
+1
+0
+0
+1
+0
+0
+1
+0
+0
+1
+2
+4
+2
+4
+3
+3
+3
+0
+0
+3
+3
+3
+1
+7
+0
+.
+1 3 ;
+.
+2
+2
+2
+2
+1
+2
+2
+1
+.
+.
+1
+1
+1
+1
+0
+0
+1
+0
+0
+1
+0
+0
+1
+0
+1
+0
+1
+1
+1
+0
+1
+1
+1
+1
+0
+0
+1
+0
+0
+1
+0
+0
+0
+0
+0
+1
+2
+4
+2
+4
+3
+3
+3
+0
+0
+3
+2
+3
+1
+7
+0
+.
+5 2 ;
+.
+2
+2
+2
+2
+1
+2
+2
+1
+.
+.
+1
+1
+1
+1
+0
+0
+1
+0
+1
+1
+0
+0
+1
+0
+1
+0
+1
+1
+1
+0
+1
+1
+1
+1
+0
+0
+0
+0
+0
+1
+0
+0
+0
+0
+0
+1
+2
+4
+2
+4
+3
+3
+3
+0
+0
+3
+1
+3
+1
+7
+0
+.
+5 2 ;
+.
+2
+2
+2
+2
+3
+2
+2
+1
+.
+.
+1
+1
+1
+0
+0
+0
+1
+0
+1
+1
+0
+0
+1
+0
+1
+1
+1
+1
+1
+0
+1
+1
+1
+1
+0
+0
+0
+0
+0
+1
+0
+0
+0
+0
+0
+1
+2
+4
+2
+4
+3
+3
+3
+0
+1
+3
+1
+3
+1
+7
+0
+.
+4 2 ;
+.
+2
+2
+2
+2
+1
+2
+2
+1
+.
+.
+1
+1
+1
+0
+0
+0
+1
+0
+1
+1
+0
+0
+1
+0
+1
+1
+1
+1
+1
+0
+1
+1
+1
+1
+0
+0
+0
+0
+0
+1
+0
+0
+0
+0
+0
+1
+2
+4
+2
+4
+3
+3
+3
+0
+1
+3
+1
+3
+1
+7
+0
+.
+4 5 ;
+4 6 ;
+.
+2
+2
+2
+2
+1
+2
+2
+1
+.
+.
+0
+1
+1
+1
+0
+0
+1
+0
+1
+1
+0
+0
+1
+0
+1
+1
+1
+1
+1
+0
+1
+1
+1
+1
+0
+0
+0
+0
+0
+1
+0
+0
+0
+0
+0
+1
+2
+4
+2
+4
+3
+3
+3
+1
+1
+3
+1
+3
+1
+7
+0
+.
+3 3 ;
+.
+2
+2
+2
+2
+1
+2
+2
+1
+.
+.
+0
+0
+1
+1
+1
+0
+1
+0
+1
+1
+0
+0
+1
+0
+1
+1
+1
+1
+1
+0
+1
+1
+1
+1
+0
+0
+0
+0
+0
+1
+0
+0
+0
+0
+0
+1
+2
+4
+2
+4
+3
+3
+3
+2
+1
+3
+1
+3
+1
+7
+0
+.
+3 3 ;
+.
+2
+2
+2
+2
+1
+2
+2
+1
+.
+.
+0
+0
+0
+1
+1
+1
+1
+0
+1
+1
+0
+0
+1
+0
+1
+1
+1
+1
+1
+0
+1
+1
+1
+1
+0
+0
+0
+0
+0
+1
+0
+0
+0
+0
+0
+1
+2
+4
+2
+4
+3
+3
+3
+3
+1
+3
+1
+3
+1
+7
+0
+.
+3 3 ;
+.
+2
+2
+2
+2
+1
+2
+2
+1
+.
+.
+0
+0
+1
+1
+1
+1
+1
+0
+1
+1
+0
+0
+1
+0
+1
+1
+1
+1
+1
+0
+0
+1
+1
+1
+0
+0
+0
+0
+0
+1
+0
+0
+0
+0
+0
+1
+2
+4
+2
+4
+3
+3
+3
+3
+1
+3
+0
+3
+1
+7
+0
+.
+5 2 ;
+.
+2
+2
+2
+2
+1
+2
+2
+1
+.
+.
+0
+0
+1
+1
+1
+1
+1
+0
+1
+1
+0
+0
+1
+0
+1
+1
+1
+1
+1
+0
+1
+1
+1
+0
+0
+0
+0
+0
+0
+1
+0
+0
+0
+0
+0
+1
+2
+4
+2
+4
+3
+2
+3
+3
+1
+3
+0
+3
+1
+7
+0
+.
+2 2 ;
+.
+2
+2
+2
+2
+1
+2
+2
+1
+.
+.
+0
+0
+1
+1
+1
+1
+1
+0
+1
+1
+0
+0
+1
+0
+1
+1
+1
+1
+1
+1
+1
+1
+0
+0
+0
+0
+0
+0
+0
+1
+0
+0
+0
+0
+0
+1
+2
+4
+2
+4
+3
+1
+3
+3
+1
+3
+0
+3
+1
+7
+0
+.
+2 2 ;
+.
+2
+2
+2
+2
+1
+2
+2
+1
+.
+.
+1
+0
+1
+1
+1
+1
+1
+0
+1
+1
+0
+0
+1
+0
+1
+1
+1
+1
+0
+1
+1
+1
+0
+0
+0
+0
+0
+0
+0
+1
+0
+0
+0
+0
+0
+1
+2
+4
+2
+4
+3
+1
+3
+3
+1
+3
+0
+3
+0
+7
+0
+.
+6 2 ;
+.
+2
+2
+2
+2
+1
+2
+2
+1
+.
+.
+1
+0
+1
+1
+1
+1
+1
+0
+1
+1
+0
+0
+1
+0
+1
+1
+1
+1
+1
+1
+1
+0
+0
+0
+0
+0
+0
+0
+0
+1
+0
+0
+0
+0
+0
+1
+2
+4
+2
+4
+3
+0
+3
+3
+1
+3
+0
+3
+0
+7
+0
+.
+2 2 ;
+.
+2
+2
+2
+2
+3
+2
+2
+1
+.
+.
+1
+0
+1
+1
+1
+1
+1
+0
+1
+0
+0
+0
+1
+0
+1
+1
+1
+1
+1
+1
+1
+1
+0
+0
+0
+0
+0
+0
+0
+1
+0
+0
+0
+0
+0
+1
+2
+4
+2
+4
+3
+0
+3
+3
+2
+3
+0
+3
+0
+7
+0
+.
+4 2 ;
+.
+2
+2
+2
+2
+1
+2
+2
+1
+.
+.
+1
+0
+1
+1
+1
+1
+1
+0
+1
+0
+0
+0
+1
+0
+1
+1
+1
+1
+1
+1
+1
+1
+0
+0
+0
+0
+0
+0
+0
+1
+0
+0
+0
+0
+0
+1
+2
+4
+2
+4
+3
+0
+3
+3
+2
+3
+0
+3
+0
+7
+0
+.
+4 5 ;
+4 6 ;
+.
+2
+2
+2
+2
+3
+2
+2
+1
+.
+.
+1
+0
+1
+1
+1
+1
+1
+0
+1
+0
+0
+0
+1
+0
+1
+0
+1
+1
+1
+1
+1
+1
+0
+0
+0
+0
+0
+1
+0
+1
+0
+0
+0
+0
+0
+1
+2
+4
+2
+4
+3
+0
+3
+3
+3
+3
+0
+3
+0
+7
+0
+.
+4 2 ;
+.
+2
+2
+2
+2
+1
+2
+2
+1
+.
+.
+1
+0
+1
+1
+1
+1
+1
+0
+1
+0
+0
+0
+1
+0
+1
+0
+1
+1
+1
+1
+1
+1
+0
+0
+0
+0
+0
+1
+0
+1
+0
+0
+0
+0
+0
+1
+2
+4
+2
+4
+3
+0
+3
+3
+3
+3
+0
+3
+0
+7
+0
+.
+4 5 ;
+4 6 ;
+.
+2
+2
+2
+2
+3
+2
+2
+1
+.
+.
+1
+0
+1
+1
+1
+1
+1
+0
+1
+0
+0
+0
+1
+0
+1
+0
+1
+1
+1
+1
+1
+0
+0
+0
+0
+0
+0
+1
+0
+1
+0
+0
+0
+1
+0
+1
+2
+4
+2
+4
+3
+0
+3
+3
+4
+3
+0
+3
+0
+7
+0
+.
+4 2 ;
+.
+2
+2
+2
+2
+2
+2
+2
+0
+.
+.
+1
+0
+1
+1
+1
+1
+1
+0
+1
+0
+0
+0
+1
+0
+1
+0
+1
+1
+1
+1
+1
+0
+0
+0
+0
+0
+0
+1
+0
+1
+0
+0
+0
+1
+0
+1
+2
+4
+2
+4
+3
+0
+3
+3
+4
+3
+0
+3
+0
+7
+1
+.
+4 7 ;
+7 0 ;
+.
+.

diff --git a/uppaal/2intermediateTrace.xtr b/uppaal/2intermediateTrace.xtr
new file mode 100644 (file)
index 0000000..d57420f
--- /dev/null
+++ b/uppaal/2intermediateTrace.xtr
@@ -0,0 +1,3392 @@
+1
+1
+1
+1
+1
+1
+1
+5
+1
+1
+1
+1
+1
+2
+.
+.
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+2
+0
+2
+2
+2
+4
+2
+3
+3
+2
+2
+3
+2
+3
+2
+3
+0
+2
+1
+2
+0
+2
+4
+2
+4
+0
+0
+.
+0
+1
+1
+1
+1
+1
+1
+5
+1
+1
+1
+1
+1
+2
+.
+.
+0
+0
+0
+0
+0
+1
+0
+0
+0
+0
+0
+1
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+2
+0
+2
+2
+2
+4
+2
+3
+3
+2
+2
+3
+2
+3
+2
+3
+0
+2
+1
+2
+0
+2
+4
+2
+4
+1
+0
+.
+0 1 ;
+13 2 ;
+.
+0
+0
+1
+1
+1
+1
+1
+5
+1
+1
+1
+1
+1
+2
+.
+.
+0
+0
+0
+0
+0
+1
+0
+0
+0
+0
+0
+1
+0
+0
+0
+0
+0
+1
+0
+0
+0
+0
+0
+1
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+2
+0
+2
+2
+2
+4
+2
+3
+3
+2
+2
+3
+2
+3
+2
+3
+0
+2
+1
+2
+0
+2
+4
+2
+4
+2
+0
+.
+1 1 ;
+13 2 ;
+.
+0
+0
+0
+1
+1
+1
+1
+5
+1
+1
+1
+1
+1
+2
+.
+.
+0
+0
+0
+0
+0
+1
+0
+0
+0
+0
+0
+1
+0
+0
+0
+0
+0
+1
+0
+0
+0
+0
+0
+1
+0
+0
+0
+0
+1
+1
+0
+0
+0
+0
+0
+0
+2
+0
+2
+2
+2
+4
+2
+3
+3
+2
+2
+3
+2
+3
+2
+3
+0
+2
+1
+2
+0
+2
+4
+2
+4
+3
+0
+.
+2 1 ;
+13 2 ;
+.
+0
+0
+0
+0
+1
+1
+1
+5
+1
+1
+1
+1
+1
+2
+.
+.
+0
+0
+0
+0
+0
+1
+0
+0
+0
+0
+0
+1
+0
+0
+0
+1
+1
+1
+0
+0
+0
+0
+0
+1
+0
+0
+0
+0
+1
+1
+0
+0
+0
+0
+0
+0
+2
+0
+2
+2
+2
+4
+2
+3
+3
+2
+2
+3
+2
+3
+2
+3
+0
+2
+1
+2
+0
+2
+4
+2
+4
+4
+0
+.
+3 1 ;
+13 2 ;
+.
+0
+0
+0
+0
+0
+1
+1
+5
+1
+1
+1
+1
+1
+2
+.
+.
+0
+0
+0
+0
+0
+1
+0
+0
+0
+0
+0
+1
+0
+0
+0
+1
+1
+1
+0
+0
+0
+0
+0
+1
+0
+0
+0
+0
+1
+1
+0
+0
+1
+1
+1
+0
+2
+0
+2
+2
+2
+4
+2
+3
+3
+2
+2
+3
+2
+3
+2
+3
+0
+2
+1
+2
+0
+2
+4
+2
+4
+5
+0
+.
+4 1 ;
+13 2 ;
+.
+0
+0
+0
+0
+0
+0
+1
+5
+1
+1
+1
+1
+1
+2
+.
+.
+0
+0
+0
+0
+0
+1
+0
+0
+0
+1
+1
+1
+0
+0
+0
+1
+1
+1
+0
+0
+0
+0
+0
+1
+0
+0
+0
+0
+1
+1
+0
+0
+1
+1
+1
+0
+2
+0
+2
+2
+2
+4
+2
+3
+3
+2
+2
+3
+2
+3
+2
+3
+0
+2
+1
+2
+0
+2
+4
+2
+4
+6
+0
+.
+5 1 ;
+13 2 ;
+.
+0
+0
+0
+0
+0
+0
+0
+5
+1
+1
+1
+1
+1
+2
+.
+.
+0
+0
+0
+0
+0
+1
+0
+0
+0
+1
+1
+1
+0
+0
+0
+1
+1
+1
+0
+0
+0
+0
+1
+1
+0
+0
+0
+0
+1
+1
+0
+0
+1
+1
+1
+0
+2
+0
+2
+2
+2
+4
+2
+3
+3
+2
+2
+3
+2
+3
+2
+3
+0
+2
+1
+2
+0
+2
+4
+2
+4
+7
+0
+.
+6 1 ;
+13 2 ;
+.
+0
+0
+0
+0
+0
+0
+0
+4
+1
+1
+1
+1
+1
+2
+.
+.
+0
+0
+0
+0
+0
+1
+0
+0
+0
+1
+1
+1
+0
+0
+0
+1
+1
+1
+0
+0
+0
+1
+1
+1
+0
+0
+0
+0
+1
+1
+0
+0
+1
+1
+1
+0
+2
+0
+2
+2
+2
+4
+2
+3
+3
+2
+2
+3
+2
+3
+2
+3
+0
+2
+1
+2
+0
+2
+4
+2
+4
+8
+0
+.
+7 9 ;
+13 2 ;
+.
+0
+0
+0
+0
+0
+0
+0
+4
+0
+1
+1
+1
+1
+2
+.
+.
+1
+1
+1
+0
+0
+1
+0
+0
+0
+1
+1
+1
+0
+0
+0
+1
+1
+1
+0
+0
+0
+1
+1
+1
+0
+0
+0
+0
+1
+1
+0
+0
+1
+1
+1
+0
+2
+0
+2
+2
+2
+4
+2
+3
+3
+2
+2
+3
+2
+3
+2
+3
+0
+2
+1
+2
+0
+2
+4
+2
+4
+9
+0
+.
+8 1 ;
+13 2 ;
+.
+0
+0
+0
+0
+0
+0
+0
+4
+0
+0
+1
+1
+1
+2
+.
+.
+1
+1
+1
+0
+0
+1
+1
+0
+0
+1
+1
+1
+1
+0
+0
+1
+1
+1
+0
+0
+0
+1
+1
+1
+0
+0
+0
+0
+1
+1
+0
+0
+1
+1
+1
+0
+2
+0
+2
+2
+2
+4
+2
+3
+3
+2
+2
+3
+2
+3
+2
+3
+0
+2
+1
+2
+0
+2
+4
+2
+4
+10
+0
+.
+9 1 ;
+13 2 ;
+.
+0
+0
+0
+0
+0
+0
+0
+4
+0
+0
+0
+1
+1
+2
+.
+.
+1
+1
+1
+0
+0
+1
+1
+0
+0
+1
+1
+1
+1
+0
+0
+1
+1
+1
+1
+1
+0
+1
+1
+1
+0
+0
+0
+0
+1
+1
+0
+0
+1
+1
+1
+0
+2
+0
+2
+2
+2
+4
+2
+3
+3
+2
+2
+3
+2
+3
+2
+3
+0
+2
+1
+2
+0
+2
+4
+2
+4
+11
+0
+.
+10 1 ;
+13 2 ;
+.
+0
+0
+0
+0
+0
+0
+0
+4
+0
+0
+0
+0
+1
+2
+.
+.
+1
+1
+1
+0
+0
+1
+1
+0
+0
+1
+1
+1
+1
+0
+0
+1
+1
+1
+1
+1
+0
+1
+1
+1
+0
+1
+0
+0
+1
+1
+0
+1
+1
+1
+1
+0
+2
+0
+2
+2
+2
+4
+2
+3
+3
+2
+2
+3
+2
+3
+2
+3
+0
+2
+1
+2
+0
+2
+4
+2
+4
+12
+0
+.
+11 1 ;
+13 2 ;
+.
+0
+0
+0
+0
+0
+0
+0
+4
+0
+0
+0
+0
+0
+2
+.
+.
+1
+1
+1
+0
+0
+1
+1
+0
+0
+1
+1
+1
+1
+0
+0
+1
+1
+1
+1
+1
+0
+1
+1
+1
+1
+1
+0
+0
+1
+1
+1
+1
+1
+1
+1
+0
+2
+0
+2
+2
+2
+4
+2
+3
+3
+2
+2
+3
+2
+3
+2
+3
+0
+2
+1
+2
+0
+2
+4
+2
+4
+13
+0
+.
+12 1 ;
+13 2 ;
+.
+2
+2
+2
+2
+2
+2
+2
+3
+2
+2
+2
+2
+2
+1
+.
+.
+1
+1
+1
+0
+0
+1
+1
+0
+0
+1
+1
+1
+1
+0
+0
+1
+1
+1
+1
+1
+0
+1
+1
+1
+1
+1
+0
+0
+1
+1
+1
+1
+1
+1
+1
+0
+2
+0
+2
+2
+2
+4
+2
+3
+3
+2
+2
+3
+2
+3
+2
+3
+0
+2
+1
+2
+0
+2
+4
+2
+4
+13
+0
+.
+13 1 ;
+0 0 ;
+1 0 ;
+2 0 ;
+3 0 ;
+4 0 ;
+5 0 ;
+6 0 ;
+7 8 ;
+8 0 ;
+9 0 ;
+10 0 ;
+11 0 ;
+12 0 ;
+.
+2
+2
+2
+2
+2
+2
+2
+0
+2
+2
+2
+2
+2
+1
+.
+.
+1
+1
+1
+0
+0
+1
+1
+0
+0
+1
+1
+1
+1
+0
+0
+1
+1
+1
+1
+1
+0
+1
+1
+1
+1
+1
+0
+0
+1
+1
+1
+1
+1
+1
+1
+0
+2
+0
+2
+2
+2
+4
+2
+3
+3
+2
+2
+3
+2
+3
+2
+3
+0
+2
+1
+2
+0
+2
+4
+2
+4
+13
+0
+.
+7 4 ;
+7 6 ;
+.
+2
+2
+2
+2
+2
+2
+2
+0
+2
+2
+2
+2
+2
+1
+.
+.
+1
+1
+1
+0
+0
+1
+1
+0
+0
+1
+1
+1
+1
+0
+0
+1
+1
+1
+0
+1
+1
+1
+1
+1
+1
+1
+0
+0
+1
+1
+1
+1
+1
+1
+1
+0
+2
+0
+2
+2
+2
+4
+2
+3
+3
+2
+2
+3
+2
+3
+2
+3
+0
+2
+1
+2
+1
+2
+4
+2
+4
+13
+0
+.
+10 3 ;
+.
+2
+2
+2
+2
+2
+2
+2
+0
+2
+2
+2
+2
+2
+1
+.
+.
+1
+1
+1
+0
+0
+1
+1
+0
+0
+1
+1
+1
+1
+0
+0
+1
+1
+1
+0
+1
+1
+1
+1
+1
+1
+1
+0
+1
+1
+0
+1
+1
+1
+1
+1
+0
+2
+0
+2
+2
+2
+3
+2
+3
+3
+2
+2
+3
+2
+3
+2
+3
+0
+2
+1
+2
+1
+2
+4
+2
+4
+13
+0
+.
+2 2 ;
+.
+2
+2
+2
+2
+2
+2
+2
+0
+2
+2
+2
+2
+2
+1
+.
+.
+1
+1
+1
+0
+0
+1
+1
+0
+0
+1
+1
+1
+1
+0
+0
+1
+1
+1
+0
+1
+1
+1
+1
+1
+1
+1
+1
+1
+0
+0
+1
+1
+1
+1
+1
+0
+2
+0
+2
+2
+2
+2
+2
+3
+3
+2
+2
+3
+2
+3
+2
+3
+0
+2
+1
+2
+1
+2
+4
+2
+4
+13
+0
+.
+2 2 ;
+.
+2
+2
+2
+2
+2
+2
+2
+0
+2
+2
+2
+2
+2
+1
+.
+.
+1
+1
+1
+0
+0
+1
+1
+0
+1
+1
+0
+1
+1
+0
+0
+1
+1
+1
+0
+1
+1
+1
+1
+1
+1
+1
+1
+1
+0
+0
+1
+1
+1
+1
+1
+0
+2
+0
+2
+2
+2
+2
+2
+3
+3
+2
+2
+2
+2
+3
+2
+3
+0
+2
+1
+2
+1
+2
+4
+2
+4
+13
+0
+.
+5 2 ;
+.
+2
+2
+2
+2
+2
+2
+2
+0
+2
+2
+2
+2
+2
+1
+.
+.
+1
+1
+1
+0
+0
+1
+1
+1
+1
+0
+0
+1
+1
+0
+0
+1
+1
+1
+0
+1
+1
+1
+1
+1
+1
+1
+1
+1
+0
+0
+1
+1
+1
+1
+1
+0
+2
+0
+2
+2
+2
+2
+2
+3
+3
+2
+2
+1
+2
+3
+2
+3
+0
+2
+1
+2
+1
+2
+4
+2
+4
+13
+0
+.
+5 2 ;
+.
+2
+2
+2
+2
+2
+2
+2
+0
+2
+2
+2
+2
+2
+1
+.
+.
+1
+1
+1
+0
+0
+1
+1
+1
+1
+0
+0
+1
+1
+0
+0
+1
+1
+1
+1
+1
+1
+1
+1
+1
+1
+1
+1
+1
+0
+0
+0
+1
+1
+1
+1
+0
+2
+0
+2
+2
+2
+2
+2
+3
+3
+2
+2
+1
+2
+3
+2
+3
+0
+2
+1
+2
+1
+2
+4
+2
+3
+13
+0
+.
+12 2 ;
+.
+2
+2
+2
+2
+2
+2
+2
+0
+2
+2
+2
+2
+2
+1
+.
+.
+1
+1
+1
+0
+0
+1
+1
+1
+1
+0
+0
+1
+1
+0
+0
+1
+1
+0
+1
+1
+1
+1
+1
+1
+1
+1
+1
+1
+0
+1
+0
+1
+1
+1
+1
+0
+2
+0
+2
+3
+2
+2
+2
+3
+3
+2
+2
+1
+2
+3
+2
+3
+0
+2
+1
+2
+1
+2
+4
+2
+3
+13
+0
+.
+1 3 ;
+.
+2
+2
+2
+2
+2
+2
+2
+0
+2
+2
+2
+2
+2
+1
+.
+.
+1
+1
+1
+0
+0
+1
+1
+1
+1
+0
+0
+1
+1
+0
+0
+1
+1
+0
+1
+1
+1
+1
+1
+0
+1
+1
+1
+1
+0
+1
+0
+1
+1
+1
+1
+1
+2
+0
+2
+4
+2
+2
+2
+3
+3
+2
+2
+1
+2
+3
+2
+3
+0
+2
+1
+2
+1
+2
+4
+2
+3
+13
+0
+.
+1 3 ;
+.
+2
+2
+2
+2
+2
+2
+2
+3
+2
+2
+2
+2
+2
+1
+.
+.
+1
+1
+1
+0
+0
+1
+1
+1
+1
+1
+0
+1
+1
+0
+0
+1
+1
+0
+1
+1
+1
+0
+1
+0
+1
+1
+1
+1
+0
+1
+0
+1
+1
+1
+1
+1
+2
+0
+2
+4
+2
+2
+2
+3
+3
+2
+2
+1
+2
+3
+1
+3
+0
+2
+1
+2
+1
+2
+4
+2
+3
+13
+0
+.
+7 3 ;
+.
+2
+2
+2
+2
+2
+2
+2
+1
+2
+2
+2
+2
+2
+1
+.
+.
+1
+1
+1
+0
+0
+1
+1
+1
+1
+1
+0
+1
+1
+0
+0
+1
+1
+0
+1
+1
+1
+0
+1
+0
+1
+1
+1
+1
+0
+1
+0
+1
+1
+1
+1
+1
+2
+0
+2
+4
+2
+2
+2
+3
+3
+2
+2
+1
+2
+3
+1
+3
+0
+2
+1
+2
+1
+2
+4
+2
+3
+13
+0
+.
+7 5 ;
+7 6 ;
+.
+2
+2
+2
+2
+2
+2
+2
+1
+2
+2
+2
+2
+2
+1
+.
+.
+1
+1
+1
+0
+0
+1
+1
+1
+1
+1
+0
+1
+1
+0
+0
+1
+1
+0
+1
+0
+1
+1
+1
+0
+1
+1
+1
+1
+0
+1
+0
+1
+1
+1
+1
+1
+2
+0
+2
+4
+2
+2
+2
+3
+3
+2
+2
+1
+2
+3
+1
+3
+0
+2
+1
+2
+2
+2
+4
+2
+3
+13
+0
+.
+10 3 ;
+.
+2
+2
+2
+2
+2
+2
+2
+1
+2
+2
+2
+2
+2
+1
+.
+.
+1
+1
+1
+0
+0
+1
+1
+1
+1
+1
+0
+1
+1
+0
+0
+1
+1
+0
+1
+1
+1
+1
+1
+0
+1
+1
+1
+1
+0
+1
+0
+0
+1
+1
+1
+1
+2
+0
+2
+4
+2
+2
+2
+3
+3
+2
+2
+1
+2
+3
+1
+3
+0
+2
+1
+2
+2
+2
+3
+2
+3
+13
+0
+.
+11 2 ;
+.
+2
+2
+2
+2
+2
+2
+2
+1
+2
+2
+2
+2
+2
+1
+.
+.
+1
+1
+1
+0
+0
+1
+1
+1
+1
+1
+0
+1
+1
+0
+0
+1
+1
+0
+1
+1
+1
+1
+1
+0
+1
+1
+1
+1
+0
+1
+0
+1
+1
+1
+0
+1
+2
+0
+2
+4
+2
+2
+2
+3
+3
+1
+2
+1
+2
+3
+1
+3
+0
+2
+1
+2
+2
+2
+3
+2
+3
+13
+0
+.
+4 2 ;
+.
+2
+2
+2
+2
+2
+2
+2
+1
+2
+2
+2
+2
+2
+1
+.
+.
+1
+1
+1
+0
+0
+1
+1
+1
+1
+1
+0
+1
+1
+0
+0
+1
+1
+0
+1
+1
+1
+1
+1
+0
+1
+1
+1
+1
+0
+1
+1
+1
+1
+0
+0
+1
+2
+0
+2
+4
+2
+2
+2
+3
+3
+0
+2
+1
+2
+3
+1
+3
+0
+2
+1
+2
+2
+2
+3
+2
+3
+13
+0
+.
+4 2 ;
+.
+2
+2
+2
+2
+2
+2
+2
+1
+2
+2
+2
+2
+2
+1
+.
+.
+1
+1
+1
+0
+0
+1
+1
+1
+1
+1
+0
+1
+1
+1
+0
+1
+1
+0
+1
+1
+1
+1
+1
+0
+1
+0
+1
+1
+0
+1
+1
+1
+1
+0
+0
+1
+2
+0
+2
+4
+2
+2
+2
+3
+3
+0
+2
+1
+2
+3
+1
+3
+0
+2
+1
+2
+2
+2
+2
+2
+3
+13
+0
+.
+11 2 ;
+.
+2
+2
+2
+2
+2
+2
+2
+1
+2
+2
+2
+2
+2
+1
+.
+.
+1
+1
+1
+0
+0
+1
+1
+1
+1
+1
+0
+1
+1
+1
+0
+1
+1
+0
+1
+1
+1
+1
+1
+0
+1
+1
+1
+0
+0
+1
+1
+1
+1
+0
+0
+1
+2
+0
+2
+4
+2
+1
+2
+3
+3
+0
+2
+1
+2
+3
+1
+3
+0
+2
+1
+2
+2
+2
+2
+2
+3
+13
+0
+.
+2 2 ;
+.
+2
+2
+2
+2
+2
+2
+2
+1
+2
+2
+2
+2
+2
+1
+.
+.
+1
+1
+1
+0
+0
+1
+1
+1
+1
+1
+0
+1
+1
+1
+0
+1
+1
+0
+1
+1
+1
+1
+0
+0
+1
+1
+1
+0
+0
+1
+1
+1
+1
+0
+1
+1
+2
+0
+2
+4
+2
+1
+2
+3
+3
+0
+2
+1
+2
+4
+1
+3
+0
+2
+1
+2
+2
+2
+2
+2
+3
+13
+0
+.
+6 3 ;
+.
+2
+2
+2
+2
+2
+2
+2
+1
+2
+2
+2
+2
+2
+1
+.
+.
+1
+1
+1
+0
+0
+1
+1
+1
+1
+1
+0
+1
+1
+1
+0
+1
+1
+0
+1
+1
+0
+1
+1
+0
+1
+1
+1
+0
+0
+1
+1
+1
+1
+0
+1
+1
+2
+0
+2
+4
+2
+1
+2
+3
+3
+0
+2
+1
+2
+4
+1
+3
+0
+2
+1
+2
+3
+2
+2
+2
+3
+13
+0
+.
+10 3 ;
+.
+2
+2
+2
+2
+2
+2
+2
+1
+2
+2
+2
+2
+2
+1
+.
+.
+1
+1
+1
+0
+0
+1
+1
+1
+1
+1
+0
+1
+1
+1
+0
+1
+1
+0
+1
+1
+0
+0
+1
+1
+1
+1
+1
+0
+0
+1
+1
+1
+1
+0
+1
+1
+2
+0
+2
+4
+2
+1
+2
+3
+3
+0
+2
+1
+2
+4
+1
+3
+0
+2
+1
+2
+4
+2
+2
+2
+3
+13
+0
+.
+10 3 ;
+.
+2
+2
+2
+2
+2
+2
+2
+3
+2
+2
+2
+2
+2
+1
+.
+.
+1
+1
+1
+0
+0
+1
+1
+1
+1
+0
+0
+1
+1
+1
+0
+1
+1
+0
+1
+1
+0
+1
+1
+1
+1
+1
+1
+0
+0
+1
+1
+1
+1
+0
+1
+1
+2
+0
+2
+4
+2
+1
+2
+3
+3
+0
+2
+1
+2
+4
+2
+3
+0
+2
+1
+2
+4
+2
+2
+2
+3
+13
+0
+.
+7 2 ;
+.
+2
+2
+2
+2
+2
+2
+2
+1
+2
+2
+2
+2
+2
+1
+.
+.
+1
+1
+1
+0
+0
+1
+1
+1
+1
+0
+0
+1
+1
+1
+0
+1
+1
+0
+1
+1
+0
+1
+1
+1
+1
+1
+1
+0
+0
+1
+1
+1
+1
+0
+1
+1
+2
+0
+2
+4
+2
+1
+2
+3
+3
+0
+2
+1
+2
+4
+2
+3
+0
+2
+1
+2
+4
+2
+2
+2
+3
+13
+0
+.
+7 5 ;
+7 6 ;
+.
+2
+2
+2
+2
+2
+2
+2
+3
+2
+2
+2
+2
+2
+1
+.
+.
+1
+1
+1
+0
+0
+1
+1
+1
+1
+0
+0
+1
+1
+1
+0
+0
+1
+0
+1
+1
+0
+1
+1
+1
+1
+1
+1
+1
+0
+1
+1
+1
+1
+0
+1
+1
+2
+0
+2
+4
+2
+1
+2
+3
+3
+0
+2
+1
+2
+4
+3
+3
+0
+2
+1
+2
+4
+2
+2
+2
+3
+13
+0
+.
+7 2 ;
+.
+2
+2
+2
+2
+2
+2
+2
+1
+2
+2
+2
+2
+2
+1
+.
+.
+1
+1
+1
+0
+0
+1
+1
+1
+1
+0
+0
+1
+1
+1
+0
+0
+1
+0
+1
+1
+0
+1
+1
+1
+1
+1
+1
+1
+0
+1
+1
+1
+1
+0
+1
+1
+2
+0
+2
+4
+2
+1
+2
+3
+3
+0
+2
+1
+2
+4
+3
+3
+0
+2
+1
+2
+4
+2
+2
+2
+3
+13
+0
+.
+7 5 ;
+7 6 ;
+.
+2
+2
+2
+2
+2
+2
+2
+3
+2
+2
+2
+2
+2
+1
+.
+.
+1
+1
+1
+0
+0
+1
+1
+1
+1
+0
+0
+1
+1
+1
+0
+0
+1
+0
+1
+1
+0
+0
+1
+1
+1
+1
+1
+1
+0
+1
+1
+1
+1
+1
+1
+1
+2
+0
+2
+4
+2
+1
+2
+3
+3
+0
+2
+1
+2
+4
+4
+3
+0
+2
+1
+2
+4
+2
+2
+2
+3
+13
+0
+.
+7 2 ;
+.
+2
+2
+2
+2
+2
+2
+2
+2
+2
+2
+2
+2
+2
+0
+.
+.
+1
+1
+1
+0
+0
+1
+1
+1
+1
+0
+0
+1
+1
+1
+0
+0
+1
+0
+1
+1
+0
+0
+1
+1
+1
+1
+1
+1
+0
+1
+1
+1
+1
+1
+1
+1
+2
+0
+2
+4
+2
+1
+2
+3
+3
+0
+2
+1
+2
+4
+4
+3
+0
+2
+1
+2
+4
+2
+2
+2
+3
+13
+1
+.
+7 7 ;
+13 0 ;
+.
+.

diff --git a/uppaal/2website2Trace.xtr b/uppaal/2website2Trace.xtr
new file mode 100644 (file)
index 0000000..f25ae03
--- /dev/null
+++ b/uppaal/2website2Trace.xtr
@@ -0,0 +1,7449 @@
+1
+1
+1
+1
+1
+5
+1
+1
+1
+2
+.
+.
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+2
+0
+3
+3
+3
+0
+3
+3
+2
+1
+3
+2
+3
+2
+4
+2
+4
+0
+0
+.
+0
+1
+1
+1
+1
+5
+1
+1
+1
+2
+.
+.
+1
+1
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+2
+0
+3
+3
+3
+0
+3
+3
+2
+1
+3
+2
+3
+2
+4
+2
+4
+1
+0
+.
+0 1 ;
+9 2 ;
+.
+0
+0
+1
+1
+1
+5
+1
+1
+1
+2
+.
+.
+1
+1
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+1
+1
+1
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+2
+0
+3
+3
+3
+0
+3
+3
+2
+1
+3
+2
+3
+2
+4
+2
+4
+2
+0
+.
+1 1 ;
+9 2 ;
+.
+0
+0
+0
+1
+1
+5
+1
+1
+1
+2
+.
+.
+1
+1
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+1
+1
+1
+1
+1
+1
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+2
+0
+3
+3
+3
+0
+3
+3
+2
+1
+3
+2
+3
+2
+4
+2
+4
+3
+0
+.
+2 1 ;
+9 2 ;
+.
+0
+0
+0
+0
+1
+5
+1
+1
+1
+2
+.
+.
+1
+1
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+1
+1
+1
+1
+1
+1
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+1
+1
+1
+2
+0
+3
+3
+3
+0
+3
+3
+2
+1
+3
+2
+3
+2
+4
+2
+4
+4
+0
+.
+3 1 ;
+9 2 ;
+.
+0
+0
+0
+0
+0
+5
+1
+1
+1
+2
+.
+.
+1
+1
+0
+0
+0
+0
+0
+1
+0
+0
+0
+0
+0
+1
+0
+1
+1
+1
+1
+1
+1
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+0
+1
+1
+1
+2
+0
+3
+3
+3
+0
+3
+3
+2
+1
+3
+2
+3
+2
+4
+2
+4
+5
+0
+.
+4 1 ;
+9 2 ;
+.
+0
+0
+0
+0
+0
+4
+1
+1
+1
+2
+.
+.
+1
+1
+0
+0
+0
+0
+0
+1
+0
+0
+0
+0
+0
+1
+0
+1
+1
+1
+1
+1
+1
+1
+0
+0
+0
+0
+0
+1
+0
+0
+0
+0
+0
+1
+1
+1
+2
+0
+3
+3
+3
+0
+3
+3
+2
+1
+3
+2
+3
+2
+4
+2
+4
+6
+0
+.
+5 9 ;
+9 2 ;
+.
+0
+0
+0
+0
+0
+4
+0
+1
+1
+2
+.
+.
+1
+1
+0
+0
+0
+0
+0
+1
+0
+0
+0
+0
+0
+1
+0
+1
+1
+1
+1
+1
+1
+1
+0
+1
+0
+0
+0
+1
+0
+1
+0
+0
+0
+1
+1
+1
+2
+0
+3
+3
+3
+0
+3
+3
+2
+1
+3
+2
+3
+2
+4
+2
+4
+7
+0
+.
+6 1 ;
+9 2 ;
+.
+0
+0
+0
+0
+0
+4
+0
+0
+1
+2
+.
+.
+1
+1
+0
+0
+0
+0
+0
+1
+0
+0
+0
+0
+0
+1
+0
+1
+1
+1
+1
+1
+1
+1
+0
+1
+1
+0
+0
+1
+0
+1
+1
+0
+0
+1
+1
+1
+2
+0
+3
+3
+3
+0
+3
+3
+2
+1
+3
+2
+3
+2
+4
+2
+4
+8
+0
+.
+7 1 ;
+9 2 ;
+.
+0
+0
+0
+0
+0
+4
+0
+0
+0
+2
+.
+.
+1
+1
+0
+0
+0
+0
+0
+1
+0
+0
+0
+0
+0
+1
+0
+1
+1
+1
+1
+1
+1
+1
+0
+1
+1
+0
+1
+1
+0
+1
+1
+0
+1
+1
+1
+1
+2
+0
+3
+3
+3
+0
+3
+3
+2
+1
+3
+2
+3
+2
+4
+2
+4
+9
+0
+.
+8 1 ;
+9 2 ;
+.
+2
+2
+2
+2
+2
+3
+2
+2
+2
+1
+.
+.
+1
+1
+0
+0
+0
+0
+0
+1
+0
+0
+0
+0
+0
+1
+0
+1
+1
+1
+1
+1
+1
+1
+0
+1
+1
+0
+1
+1
+0
+1
+1
+0
+1
+1
+1
+1
+2
+0
+3
+3
+3
+0
+3
+3
+2
+1
+3
+2
+3
+2
+4
+2
+4
+9
+0
+.
+9 1 ;
+0 0 ;
+1 0 ;
+2 0 ;
+3 0 ;
+4 0 ;
+5 8 ;
+6 0 ;
+7 0 ;
+8 0 ;
+.
+2
+2
+2
+2
+2
+0
+2
+2
+2
+1
+.
+.
+1
+1
+0
+0
+0
+0
+0
+1
+0
+0
+0
+0
+0
+1
+0
+1
+1
+1
+1
+1
+1
+1
+0
+1
+1
+0
+1
+1
+0
+1
+1
+0
+1
+1
+1
+1
+2
+0
+3
+3
+3
+0
+3
+3
+2
+1
+3
+2
+3
+2
+4
+2
+4
+9
+0
+.
+5 4 ;
+5 6 ;
+.
+2
+2
+2
+2
+2
+0
+2
+2
+2
+1
+.
+.
+0
+1
+1
+0
+0
+0
+0
+1
+0
+0
+0
+0
+0
+1
+0
+1
+1
+1
+1
+1
+1
+1
+0
+1
+1
+0
+1
+1
+0
+1
+1
+0
+1
+1
+1
+1
+2
+1
+3
+3
+3
+0
+3
+3
+2
+1
+3
+2
+3
+2
+4
+2
+4
+9
+0
+.
+0 3 ;
+.
+2
+2
+2
+2
+2
+0
+2
+2
+2
+1
+.
+.
+0
+0
+1
+1
+0
+0
+0
+1
+0
+0
+0
+0
+0
+1
+0
+1
+1
+1
+1
+1
+1
+1
+0
+1
+1
+0
+1
+1
+0
+1
+1
+0
+1
+1
+1
+1
+2
+2
+3
+3
+3
+0
+3
+3
+2
+1
+3
+2
+3
+2
+4
+2
+4
+9
+0
+.
+0 3 ;
+.
+2
+2
+2
+2
+2
+0
+2
+2
+2
+1
+.
+.
+0
+0
+0
+1
+1
+0
+0
+1
+0
+0
+0
+0
+0
+1
+0
+1
+1
+1
+1
+1
+1
+1
+0
+1
+1
+0
+1
+1
+0
+1
+1
+0
+1
+1
+1
+1
+2
+3
+3
+3
+3
+0
+3
+3
+2
+1
+3
+2
+3
+2
+4
+2
+4
+9
+0
+.
+0 3 ;
+.
+2
+2
+2
+2
+2
+0
+2
+2
+2
+1
+.
+.
+0
+0
+0
+0
+1
+1
+0
+1
+0
+0
+0
+0
+0
+1
+0
+1
+1
+1
+1
+1
+1
+1
+0
+1
+1
+0
+1
+1
+0
+1
+1
+0
+1
+1
+1
+1
+2
+4
+3
+3
+3
+0
+3
+3
+2
+1
+3
+2
+3
+2
+4
+2
+4
+9
+0
+.
+0 3 ;
+.
+2
+2
+2
+2
+2
+0
+2
+2
+2
+1
+.
+.
+0
+0
+0
+0
+1
+1
+0
+1
+0
+0
+0
+0
+0
+1
+1
+1
+1
+0
+1
+1
+1
+1
+0
+1
+1
+0
+1
+1
+0
+1
+1
+0
+1
+1
+1
+1
+2
+4
+3
+2
+3
+0
+3
+3
+2
+1
+3
+2
+3
+2
+4
+2
+4
+9
+0
+.
+1 2 ;
+.
+2
+2
+2
+2
+2
+0
+2
+2
+2
+1
+.
+.
+0
+1
+0
+0
+1
+1
+0
+1
+0
+0
+0
+0
+0
+0
+1
+1
+1
+0
+1
+1
+1
+1
+0
+1
+1
+0
+1
+1
+0
+1
+1
+0
+1
+1
+1
+1
+2
+4
+3
+2
+3
+0
+3
+3
+2
+0
+3
+2
+3
+2
+4
+2
+4
+9
+0
+.
+4 2 ;
+.
+2
+2
+2
+2
+2
+0
+2
+2
+2
+1
+.
+.
+0
+1
+0
+0
+1
+1
+0
+1
+0
+0
+0
+0
+0
+1
+1
+1
+0
+0
+1
+1
+1
+1
+0
+1
+1
+0
+1
+1
+0
+1
+1
+0
+1
+1
+1
+1
+2
+4
+3
+1
+3
+0
+3
+3
+2
+0
+3
+2
+3
+2
+4
+2
+4
+9
+0
+.
+1 2 ;
+.
+2
+2
+2
+2
+2
+0
+2
+2
+2
+1
+.
+.
+0
+1
+0
+0
+1
+1
+0
+1
+0
+0
+0
+0
+1
+1
+1
+0
+0
+0
+1
+1
+1
+1
+0
+1
+1
+0
+1
+1
+0
+1
+1
+0
+1
+1
+1
+1
+2
+4
+3
+0
+3
+0
+3
+3
+2
+0
+3
+2
+3
+2
+4
+2
+4
+9
+0
+.
+1 2 ;
+.
+2
+2
+2
+2
+2
+0
+2
+2
+2
+1
+.
+.
+0
+1
+0
+0
+1
+1
+0
+1
+0
+0
+0
+0
+1
+1
+1
+0
+0
+1
+1
+1
+1
+1
+0
+1
+1
+0
+1
+1
+0
+0
+1
+0
+1
+1
+1
+1
+2
+4
+3
+0
+3
+0
+3
+3
+2
+0
+3
+2
+2
+2
+4
+2
+4
+9
+0
+.
+6 2 ;
+.
+2
+2
+2
+2
+2
+0
+2
+2
+2
+1
+.
+.
+0
+1
+0
+0
+1
+1
+0
+1
+0
+0
+0
+1
+1
+1
+1
+0
+0
+1
+1
+1
+1
+1
+0
+0
+1
+0
+1
+1
+0
+0
+1
+0
+1
+1
+1
+1
+2
+4
+3
+0
+3
+0
+3
+3
+2
+0
+3
+2
+1
+2
+4
+2
+4
+9
+0
+.
+6 2 ;
+.
+2
+2
+2
+2
+2
+3
+2
+2
+2
+1
+.
+.
+0
+1
+0
+0
+1
+1
+0
+1
+0
+0
+0
+1
+1
+1
+1
+1
+0
+1
+1
+1
+1
+1
+0
+0
+1
+0
+1
+0
+0
+0
+1
+0
+1
+1
+1
+1
+2
+4
+3
+0
+3
+0
+3
+3
+2
+0
+2
+2
+1
+2
+4
+2
+4
+9
+0
+.
+5 3 ;
+.
+2
+2
+2
+2
+2
+0
+2
+2
+2
+1
+.
+.
+0
+1
+0
+0
+1
+1
+0
+1
+0
+0
+0
+1
+1
+1
+1
+1
+0
+1
+1
+1
+1
+1
+0
+0
+1
+0
+1
+0
+0
+0
+1
+0
+1
+1
+1
+1
+2
+4
+3
+0
+3
+0
+3
+3
+2
+0
+2
+2
+1
+2
+4
+2
+4
+9
+0
+.
+5 4 ;
+5 6 ;
+.
+2
+2
+2
+2
+2
+3
+2
+2
+2
+1
+.
+.
+0
+1
+0
+0
+1
+1
+0
+1
+0
+1
+0
+1
+1
+1
+1
+1
+0
+1
+1
+1
+1
+0
+0
+0
+1
+0
+1
+0
+0
+0
+1
+0
+1
+1
+1
+1
+2
+4
+3
+0
+3
+0
+3
+3
+2
+0
+1
+2
+1
+2
+4
+2
+4
+9
+0
+.
+5 3 ;
+.
+2
+2
+2
+2
+2
+0
+2
+2
+2
+1
+.
+.
+0
+1
+0
+0
+1
+1
+0
+1
+0
+1
+0
+1
+1
+1
+1
+1
+0
+1
+1
+1
+1
+0
+0
+0
+1
+0
+1
+0
+0
+0
+1
+0
+1
+1
+1
+1
+2
+4
+3
+0
+3
+0
+3
+3
+2
+0
+1
+2
+1
+2
+4
+2
+4
+9
+0
+.
+5 4 ;
+5 6 ;
+.
+2
+2
+2
+2
+2
+0
+2
+2
+2
+1
+.
+.
+0
+1
+0
+0
+1
+1
+0
+1
+0
+1
+0
+1
+1
+1
+1
+1
+0
+1
+0
+1
+1
+1
+0
+0
+1
+0
+1
+0
+0
+0
+1
+0
+1
+1
+1
+1
+2
+4
+3
+0
+3
+1
+3
+3
+2
+0
+1
+2
+1
+2
+4
+2
+4
+9
+0
+.
+2 3 ;
+.
+2
+2
+2
+2
+2
+0
+2
+2
+2
+1
+.
+.
+0
+1
+0
+0
+1
+1
+0
+1
+0
+1
+0
+1
+1
+1
+1
+1
+0
+1
+0
+0
+1
+1
+1
+0
+1
+0
+1
+0
+0
+0
+1
+0
+1
+1
+1
+1
+2
+4
+3
+0
+3
+2
+3
+3
+2
+0
+1
+2
+1
+2
+4
+2
+4
+9
+0
+.
+2 3 ;
+.
+2
+2
+2
+2
+2
+0
+2
+2
+2
+1
+.
+.
+0
+1
+0
+0
+1
+1
+0
+1
+0
+1
+0
+1
+1
+1
+1
+1
+0
+1
+0
+0
+0
+1
+1
+1
+1
+0
+1
+0
+0
+0
+1
+0
+1
+1
+1
+1
+2
+4
+3
+0
+3
+3
+3
+3
+2
+0
+1
+2
+1
+2
+4
+2
+4
+9
+0
+.
+2 3 ;
+.
+2
+2
+2
+2
+2
+0
+2
+2
+2
+1
+.
+.
+0
+1
+0
+0
+1
+1
+0
+1
+0
+1
+0
+1
+1
+1
+1
+1
+0
+1
+1
+0
+0
+1
+1
+1
+1
+0
+1
+0
+0
+0
+0
+0
+1
+1
+1
+1
+2
+4
+3
+0
+3
+3
+3
+3
+2
+0
+1
+2
+1
+2
+3
+2
+4
+9
+0
+.
+7 2 ;
+.
+2
+2
+2
+2
+2
+0
+2
+2
+2
+1
+.
+.
+0
+1
+0
+0
+1
+1
+0
+1
+0
+1
+0
+1
+1
+1
+1
+1
+0
+1
+1
+0
+1
+1
+1
+1
+1
+0
+1
+0
+0
+0
+0
+0
+0
+1
+1
+1
+2
+4
+3
+0
+3
+3
+3
+3
+2
+0
+1
+2
+1
+2
+3
+2
+3
+9
+0
+.
+8 2 ;
+.
+2
+2
+2
+2
+2
+0
+2
+2
+2
+1
+.
+.
+0
+1
+0
+0
+1
+1
+0
+1
+0
+1
+0
+1
+1
+1
+1
+1
+0
+1
+1
+0
+1
+1
+1
+1
+1
+0
+1
+0
+0
+0
+0
+0
+1
+1
+1
+0
+2
+4
+3
+0
+3
+3
+3
+2
+2
+0
+1
+2
+1
+2
+3
+2
+3
+9
+0
+.
+3 2 ;
+.
+2
+2
+2
+2
+2
+0
+2
+2
+2
+1
+.
+.
+0
+1
+0
+0
+1
+1
+0
+1
+0
+1
+0
+1
+1
+1
+1
+1
+0
+1
+1
+0
+1
+1
+1
+1
+1
+0
+1
+0
+0
+0
+0
+1
+1
+1
+0
+0
+2
+4
+3
+0
+3
+3
+3
+1
+2
+0
+1
+2
+1
+2
+3
+2
+3
+9
+0
+.
+3 2 ;
+.
+2
+2
+2
+2
+2
+0
+2
+2
+2
+1
+.
+.
+0
+1
+0
+0
+1
+1
+0
+1
+0
+1
+0
+1
+1
+1
+1
+1
+0
+1
+1
+0
+1
+1
+1
+1
+1
+0
+1
+0
+0
+0
+1
+1
+1
+0
+0
+0
+2
+4
+3
+0
+3
+3
+3
+0
+2
+0
+1
+2
+1
+2
+3
+2
+3
+9
+0
+.
+3 2 ;
+.
+2
+2
+2
+2
+2
+3
+2
+2
+2
+1
+.
+.
+0
+1
+0
+1
+1
+1
+0
+1
+0
+1
+0
+1
+1
+1
+1
+0
+0
+1
+1
+0
+1
+1
+1
+1
+1
+0
+1
+0
+0
+0
+1
+1
+1
+0
+0
+0
+2
+4
+3
+0
+3
+3
+3
+0
+2
+0
+0
+2
+1
+2
+3
+2
+3
+9
+0
+.
+5 3 ;
+.
+2
+2
+2
+2
+2
+1
+2
+2
+2
+1
+.
+.
+0
+1
+0
+1
+1
+1
+0
+1
+0
+1
+0
+1
+1
+1
+1
+0
+0
+1
+1
+0
+1
+1
+1
+1
+1
+0
+1
+0
+0
+0
+1
+1
+1
+0
+0
+0
+2
+4
+3
+0
+3
+3
+3
+0
+2
+0
+0
+2
+1
+2
+3
+2
+3
+9
+0
+.
+5 5 ;
+5 6 ;
+.
+2
+2
+2
+2
+2
+1
+2
+2
+2
+1
+.
+.
+0
+1
+0
+1
+1
+1
+0
+1
+0
+1
+0
+1
+0
+1
+1
+1
+0
+1
+1
+0
+1
+1
+1
+1
+1
+0
+1
+0
+0
+0
+1
+1
+1
+0
+0
+0
+2
+4
+3
+1
+3
+3
+3
+0
+2
+0
+0
+2
+1
+2
+3
+2
+3
+9
+0
+.
+1 3 ;
+.
+2
+2
+2
+2
+2
+1
+2
+2
+2
+1
+.
+.
+0
+1
+0
+1
+1
+1
+0
+1
+0
+1
+0
+1
+0
+0
+1
+1
+1
+1
+1
+0
+1
+1
+1
+1
+1
+0
+1
+0
+0
+0
+1
+1
+1
+0
+0
+0
+2
+4
+3
+2
+3
+3
+3
+0
+2
+0
+0
+2
+1
+2
+3
+2
+3
+9
+0
+.
+1 3 ;
+.
+2
+2
+2
+2
+2
+1
+2
+2
+2
+1
+.
+.
+0
+0
+0
+1
+1
+1
+0
+1
+0
+1
+0
+1
+0
+1
+1
+1
+1
+1
+1
+0
+1
+1
+1
+1
+1
+0
+1
+0
+0
+0
+1
+1
+1
+0
+0
+0
+2
+4
+3
+2
+3
+3
+3
+0
+2
+1
+0
+2
+1
+2
+3
+2
+3
+9
+0
+.
+4 3 ;
+.
+2
+2
+2
+2
+2
+1
+2
+2
+2
+1
+.
+.
+0
+0
+0
+1
+1
+1
+0
+0
+0
+1
+0
+1
+0
+1
+1
+1
+1
+1
+1
+1
+1
+1
+1
+1
+1
+0
+1
+0
+0
+0
+1
+1
+1
+0
+0
+0
+2
+4
+3
+2
+3
+3
+3
+0
+2
+2
+0
+2
+1
+2
+3
+2
+3
+9
+0
+.
+4 3 ;
+.
+2
+2
+2
+2
+2
+1
+2
+2
+2
+1
+.
+.
+0
+0
+0
+1
+1
+1
+0
+0
+0
+1
+0
+1
+0
+0
+1
+1
+1
+1
+1
+1
+1
+1
+1
+1
+1
+1
+1
+0
+0
+0
+1
+1
+1
+0
+0
+0
+2
+4
+3
+2
+3
+3
+3
+0
+2
+3
+0
+2
+1
+2
+3
+2
+3
+9
+0
+.
+4 3 ;
+.
+2
+2
+2
+2
+2
+1
+2
+2
+2
+1
+.
+.
+0
+0
+0
+1
+1
+1
+0
+0
+0
+1
+0
+1
+0
+1
+1
+1
+0
+1
+1
+1
+1
+1
+1
+1
+1
+1
+1
+0
+0
+0
+1
+1
+1
+0
+0
+0
+2
+4
+3
+1
+3
+3
+3
+0
+2
+3
+0
+2
+1
+2
+3
+2
+3
+9
+0
+.
+1 2 ;
+.
+2
+2
+2
+2
+2
+1
+2
+2
+2
+1
+.
+.
+0
+0
+0
+1
+1
+1
+0
+0
+0
+1
+0
+1
+1
+1
+1
+0
+0
+1
+1
+1
+1
+1
+1
+1
+1
+1
+1
+0
+0
+0
+1
+1
+1
+0
+0
+0
+2
+4
+3
+0
+3
+3
+3
+0
+2
+3
+0
+2
+1
+2
+3
+2
+3
+9
+0
+.
+1 2 ;
+.
+2
+2
+2
+2
+2
+3
+2
+2
+2
+1
+.
+.
+0
+0
+0
+0
+1
+1
+0
+0
+0
+1
+0
+1
+1
+1
+1
+1
+0
+1
+1
+1
+1
+1
+1
+1
+1
+1
+1
+0
+0
+0
+1
+1
+1
+0
+0
+0
+2
+4
+3
+0
+3
+3
+3
+0
+2
+3
+1
+2
+1
+2
+3
+2
+3
+9
+0
+.
+5 2 ;
+.
+2
+2
+2
+2
+2
+0
+2
+2
+2
+1
+.
+.
+0
+0
+0
+0
+1
+1
+0
+0
+0
+1
+0
+1
+1
+1
+1
+1
+0
+1
+1
+1
+1
+1
+1
+1
+1
+1
+1
+0
+0
+0
+1
+1
+1
+0
+0
+0
+2
+4
+3
+0
+3
+3
+3
+0
+2
+3
+1
+2
+1
+2
+3
+2
+3
+9
+0
+.
+5 4 ;
+5 6 ;
+.
+2
+2
+2
+2
+2
+0
+2
+2
+2
+1
+.
+.
+0
+0
+0
+1
+1
+0
+0
+0
+0
+1
+0
+1
+1
+1
+1
+1
+0
+1
+1
+1
+1
+1
+1
+1
+1
+1
+1
+0
+0
+0
+1
+1
+1
+0
+0
+0
+2
+3
+3
+0
+3
+3
+3
+0
+2
+3
+1
+2
+1
+2
+3
+2
+3
+9
+0
+.
+0 2 ;
+.
+2
+2
+2
+2
+2
+0
+2
+2
+2
+1
+.
+.
+0
+0
+1
+1
+0
+0
+0
+0
+0
+1
+0
+1
+1
+1
+1
+1
+0
+1
+1
+1
+1
+1
+1
+1
+1
+1
+1
+0
+0
+0
+1
+1
+1
+0
+0
+0
+2
+2
+3
+0
+3
+3
+3
+0
+2
+3
+1
+2
+1
+2
+3
+2
+3
+9
+0
+.
+0 2 ;
+.
+2
+2
+2
+2
+2
+0
+2
+2
+2
+1
+.
+.
+0
+1
+1
+0
+0
+0
+0
+0
+0
+1
+0
+1
+1
+1
+1
+1
+0
+1
+1
+1
+1
+1
+1
+1
+1
+1
+1
+0
+0
+0
+1
+1
+1
+0
+0
+0
+2
+1
+3
+0
+3
+3
+3
+0
+2
+3
+1
+2
+1
+2
+3
+2
+3
+9
+0
+.
+0 2 ;
+.
+2
+2
+2
+2
+2
+0
+2
+2
+2
+1
+.
+.
+1
+1
+0
+0
+0
+0
+0
+0
+0
+1
+0
+1
+1
+1
+1
+1
+0
+1
+1
+1
+1
+1
+1
+1
+1
+1
+1
+0
+0
+0
+1
+1
+1
+0
+0
+0
+2
+0
+3
+0
+3
+3
+3
+0
+2
+3
+1
+2
+1
+2
+3
+2
+3
+9
+0
+.
+0 2 ;
+.
+2
+2
+2
+2
+2
+0
+2
+2
+2
+1
+.
+.
+1
+1
+0
+0
+0
+1
+0
+0
+0
+1
+0
+1
+1
+1
+1
+1
+0
+0
+1
+1
+1
+1
+1
+1
+1
+1
+1
+0
+0
+0
+1
+1
+1
+0
+0
+0
+2
+0
+3
+0
+3
+3
+3
+0
+2
+3
+1
+2
+0
+2
+3
+2
+3
+9
+0
+.
+6 2 ;
+.
+2
+2
+2
+2
+2
+3
+2
+2
+2
+1
+.
+.
+1
+1
+0
+1
+0
+1
+0
+0
+0
+1
+0
+1
+1
+1
+1
+0
+0
+0
+1
+1
+1
+1
+1
+1
+1
+1
+1
+0
+0
+0
+1
+1
+1
+0
+0
+0
+2
+0
+3
+0
+3
+3
+3
+0
+2
+3
+0
+2
+0
+2
+3
+2
+3
+9
+0
+.
+5 3 ;
+.
+2
+2
+2
+2
+2
+1
+2
+2
+2
+1
+.
+.
+1
+1
+0
+1
+0
+1
+0
+0
+0
+1
+0
+1
+1
+1
+1
+0
+0
+0
+1
+1
+1
+1
+1
+1
+1
+1
+1
+0
+0
+0
+1
+1
+1
+0
+0
+0
+2
+0
+3
+0
+3
+3
+3
+0
+2
+3
+0
+2
+0
+2
+3
+2
+3
+9
+0
+.
+5 5 ;
+5 6 ;
+.
+2
+2
+2
+2
+2
+1
+2
+2
+2
+1
+.
+.
+1
+1
+0
+1
+0
+1
+0
+0
+0
+1
+0
+1
+0
+1
+1
+1
+0
+0
+1
+1
+1
+1
+1
+1
+1
+1
+1
+0
+0
+0
+1
+1
+1
+0
+0
+0
+2
+0
+3
+1
+3
+3
+3
+0
+2
+3
+0
+2
+0
+2
+3
+2
+3
+9
+0
+.
+1 3 ;
+.
+2
+2
+2
+2
+2
+1
+2
+2
+2
+1
+.
+.
+1
+1
+0
+1
+0
+1
+0
+0
+0
+1
+0
+1
+0
+0
+1
+1
+1
+0
+1
+1
+1
+1
+1
+1
+1
+1
+1
+0
+0
+0
+1
+1
+1
+0
+0
+0
+2
+0
+3
+2
+3
+3
+3
+0
+2
+3
+0
+2
+0
+2
+3
+2
+3
+9
+0
+.
+1 3 ;
+.
+2
+2
+2
+2
+2
+1
+2
+2
+2
+1
+.
+.
+1
+1
+0
+1
+0
+1
+0
+0
+0
+1
+0
+1
+0
+0
+0
+1
+1
+1
+1
+1
+1
+1
+1
+1
+1
+1
+1
+0
+0
+0
+1
+1
+1
+0
+0
+0
+2
+0
+3
+3
+3
+3
+3
+0
+2
+3
+0
+2
+0
+2
+3
+2
+3
+9
+0
+.
+1 3 ;
+.
+2
+2
+2
+2
+2
+1
+2
+2
+2
+1
+.
+.
+1
+1
+0
+1
+0
+1
+0
+0
+0
+1
+0
+1
+1
+0
+0
+1
+1
+1
+1
+1
+1
+1
+1
+1
+0
+1
+1
+0
+0
+0
+1
+1
+1
+0
+0
+0
+2
+0
+3
+3
+3
+3
+3
+0
+2
+3
+0
+2
+0
+2
+2
+2
+3
+9
+0
+.
+7 2 ;
+.
+2
+2
+2
+2
+2
+1
+2
+2
+2
+1
+.
+.
+1
+1
+0
+1
+0
+1
+1
+0
+0
+1
+0
+1
+1
+0
+0
+1
+1
+1
+0
+1
+1
+1
+1
+1
+0
+1
+1
+0
+0
+0
+1
+1
+1
+0
+0
+0
+2
+0
+3
+3
+3
+3
+3
+0
+2
+3
+0
+2
+0
+2
+1
+2
+3
+9
+0
+.
+7 2 ;
+.
+2
+2
+2
+2
+2
+1
+2
+2
+2
+1
+.
+.
+1
+1
+0
+1
+0
+1
+1
+0
+0
+1
+0
+1
+1
+0
+1
+1
+1
+1
+0
+1
+1
+1
+1
+1
+0
+1
+0
+0
+0
+0
+1
+1
+1
+0
+0
+0
+2
+0
+3
+3
+3
+3
+3
+0
+2
+3
+0
+2
+0
+2
+1
+2
+2
+9
+0
+.
+8 2 ;
+.
+2
+2
+2
+2
+2
+1
+2
+2
+2
+1
+.
+.
+1
+1
+0
+1
+0
+1
+1
+0
+1
+1
+0
+1
+1
+0
+1
+1
+1
+1
+0
+1
+0
+1
+1
+1
+0
+1
+0
+0
+0
+0
+1
+1
+1
+0
+0
+0
+2
+0
+3
+3
+3
+3
+3
+0
+2
+3
+0
+2
+0
+2
+1
+2
+1
+9
+0
+.
+8 2 ;
+.
+2
+2
+2
+2
+2
+1
+2
+2
+2
+1
+.
+.
+1
+1
+0
+1
+0
+1
+1
+0
+1
+1
+0
+1
+1
+0
+1
+1
+1
+1
+0
+1
+1
+1
+1
+0
+0
+1
+0
+0
+0
+0
+1
+1
+1
+0
+0
+0
+2
+0
+3
+3
+3
+2
+3
+0
+2
+3
+0
+2
+0
+2
+1
+2
+1
+9
+0
+.
+2 2 ;
+.
+2
+2
+2
+2
+2
+1
+2
+2
+2
+1
+.
+.
+1
+1
+1
+1
+0
+1
+1
+0
+1
+1
+0
+1
+1
+0
+0
+1
+1
+1
+0
+1
+1
+1
+1
+0
+0
+1
+0
+0
+0
+0
+1
+1
+1
+0
+0
+0
+2
+0
+3
+3
+3
+2
+3
+0
+2
+3
+0
+2
+0
+2
+1
+2
+0
+9
+0
+.
+8 2 ;
+.
+2
+2
+2
+2
+2
+1
+2
+2
+2
+1
+.
+.
+1
+1
+1
+1
+0
+1
+1
+0
+1
+1
+0
+1
+1
+0
+1
+1
+1
+0
+0
+1
+1
+1
+1
+0
+0
+1
+0
+0
+0
+0
+1
+1
+1
+0
+0
+0
+2
+0
+3
+2
+3
+2
+3
+0
+2
+3
+0
+2
+0
+2
+1
+2
+0
+9
+0
+.
+1 2 ;
+.
+2
+2
+2
+2
+2
+1
+2
+2
+2
+1
+.
+.
+1
+1
+1
+1
+0
+0
+1
+0
+1
+1
+0
+1
+1
+0
+1
+1
+1
+1
+0
+1
+1
+1
+1
+0
+0
+1
+0
+0
+0
+0
+1
+1
+1
+0
+0
+0
+2
+0
+3
+2
+3
+2
+3
+0
+2
+3
+0
+2
+1
+2
+1
+2
+0
+9
+0
+.
+6 3 ;
+.
+2
+2
+2
+2
+2
+1
+2
+2
+2
+1
+.
+.
+1
+1
+1
+1
+0
+0
+1
+0
+1
+1
+0
+0
+1
+0
+1
+1
+1
+1
+0
+1
+1
+1
+1
+1
+0
+1
+0
+0
+0
+0
+1
+1
+1
+0
+0
+0
+2
+0
+3
+2
+3
+2
+3
+0
+2
+3
+0
+2
+2
+2
+1
+2
+0
+9
+0
+.
+6 3 ;
+.
+2
+2
+2
+2
+2
+1
+2
+2
+2
+1
+.
+.
+1
+1
+1
+1
+0
+0
+1
+0
+1
+1
+0
+0
+1
+0
+1
+1
+1
+0
+0
+1
+1
+1
+1
+1
+0
+1
+0
+0
+0
+1
+1
+1
+1
+0
+0
+0
+2
+0
+3
+2
+3
+2
+3
+0
+2
+3
+0
+2
+3
+2
+1
+2
+0
+9
+0
+.
+6 3 ;
+.
+2
+2
+2
+2
+2
+1
+2
+2
+2
+1
+.
+.
+1
+1
+1
+1
+0
+0
+1
+0
+1
+1
+0
+0
+1
+0
+0
+1
+1
+1
+0
+1
+1
+1
+1
+1
+0
+1
+0
+0
+0
+1
+1
+1
+1
+0
+0
+0
+2
+0
+3
+3
+3
+2
+3
+0
+2
+3
+0
+2
+3
+2
+1
+2
+0
+9
+0
+.
+1 3 ;
+.
+2
+2
+2
+2
+2
+1
+2
+2
+2
+1
+.
+.
+1
+1
+1
+1
+0
+0
+1
+0
+1
+1
+0
+0
+1
+0
+0
+1
+1
+1
+0
+1
+1
+1
+1
+0
+0
+1
+0
+0
+0
+1
+1
+1
+1
+0
+0
+1
+2
+0
+3
+3
+3
+2
+3
+0
+2
+3
+0
+2
+4
+2
+1
+2
+0
+9
+0
+.
+6 3 ;
+.
+2
+2
+2
+2
+2
+1
+2
+2
+2
+1
+.
+.
+1
+1
+1
+1
+0
+0
+1
+0
+1
+1
+0
+0
+1
+0
+0
+1
+1
+1
+0
+1
+0
+1
+1
+1
+0
+1
+0
+0
+0
+1
+1
+1
+1
+0
+0
+1
+2
+0
+3
+3
+3
+3
+3
+0
+2
+3
+0
+2
+4
+2
+1
+2
+0
+9
+0
+.
+2 3 ;
+.
+2
+2
+2
+2
+2
+1
+2
+2
+2
+1
+.
+.
+1
+1
+0
+1
+0
+0
+1
+0
+1
+1
+0
+0
+1
+0
+1
+1
+1
+1
+0
+1
+0
+1
+1
+1
+0
+1
+0
+0
+0
+1
+1
+1
+1
+0
+0
+1
+2
+0
+3
+3
+3
+3
+3
+0
+2
+3
+0
+2
+4
+2
+1
+2
+1
+9
+0
+.
+8 3 ;
+.
+2
+2
+2
+2
+2
+1
+2
+2
+2
+1
+.
+.
+0
+1
+1
+1
+0
+0
+1
+0
+1
+1
+0
+0
+1
+0
+1
+1
+1
+1
+0
+1
+0
+1
+1
+1
+0
+1
+0
+0
+0
+1
+1
+1
+1
+0
+0
+1
+2
+1
+3
+3
+3
+3
+3
+0
+2
+3
+0
+2
+4
+2
+1
+2
+1
+9
+0
+.
+0 3 ;
+.
+2
+2
+2
+2
+2
+1
+2
+2
+2
+1
+.
+.
+1
+1
+1
+1
+0
+0
+1
+0
+1
+1
+0
+0
+0
+0
+1
+1
+1
+1
+0
+1
+0
+1
+1
+1
+0
+1
+0
+0
+0
+1
+1
+1
+1
+0
+0
+1
+2
+1
+3
+3
+3
+3
+3
+0
+2
+3
+0
+2
+4
+2
+0
+2
+1
+9
+0
+.
+7 2 ;
+.
+2
+2
+2
+2
+2
+1
+2
+2
+2
+1
+.
+.
+1
+1
+1
+1
+0
+0
+1
+0
+0
+1
+0
+0
+0
+0
+1
+1
+1
+1
+0
+1
+1
+1
+1
+1
+0
+1
+0
+0
+0
+1
+1
+1
+1
+0
+0
+1
+2
+1
+3
+3
+3
+3
+3
+0
+2
+3
+0
+2
+4
+2
+0
+2
+2
+9
+0
+.
+8 3 ;
+.
+2
+2
+2
+2
+2
+1
+2
+2
+2
+1
+.
+.
+1
+1
+1
+1
+0
+0
+1
+0
+0
+1
+0
+0
+0
+0
+0
+1
+1
+1
+0
+1
+1
+1
+1
+1
+0
+1
+1
+0
+0
+1
+1
+1
+1
+0
+0
+1
+2
+1
+3
+3
+3
+3
+3
+0
+2
+3
+0
+2
+4
+2
+0
+2
+3
+9
+0
+.
+8 3 ;
+.
+2
+2
+2
+2
+2
+1
+2
+2
+2
+1
+.
+.
+1
+1
+1
+1
+0
+0
+1
+0
+0
+1
+0
+0
+0
+0
+1
+1
+1
+0
+0
+1
+1
+1
+1
+1
+0
+1
+1
+0
+0
+1
+1
+1
+1
+0
+0
+1
+2
+1
+3
+2
+3
+3
+3
+0
+2
+3
+0
+2
+4
+2
+0
+2
+3
+9
+0
+.
+1 2 ;
+.
+2
+2
+2
+2
+2
+1
+2
+2
+2
+1
+.
+.
+1
+1
+1
+1
+0
+0
+1
+0
+0
+1
+0
+0
+0
+1
+1
+1
+0
+0
+0
+1
+1
+1
+1
+1
+0
+1
+1
+0
+0
+1
+1
+1
+1
+0
+0
+1
+2
+1
+3
+1
+3
+3
+3
+0
+2
+3
+0
+2
+4
+2
+0
+2
+3
+9
+0
+.
+1 2 ;
+.
+2
+2
+2
+2
+2
+1
+2
+2
+2
+1
+.
+.
+1
+1
+1
+1
+0
+0
+1
+0
+0
+1
+0
+0
+1
+1
+1
+0
+0
+0
+0
+1
+1
+1
+1
+1
+0
+1
+1
+0
+0
+1
+1
+1
+1
+0
+0
+1
+2
+1
+3
+0
+3
+3
+3
+0
+2
+3
+0
+2
+4
+2
+0
+2
+3
+9
+0
+.
+1 2 ;
+.
+2
+2
+2
+2
+2
+3
+2
+2
+2
+1
+.
+.
+1
+1
+1
+0
+0
+0
+1
+0
+0
+1
+0
+0
+1
+1
+1
+1
+0
+0
+0
+1
+1
+1
+1
+1
+0
+1
+1
+0
+0
+1
+1
+1
+1
+0
+0
+1
+2
+1
+3
+0
+3
+3
+3
+0
+2
+3
+1
+2
+4
+2
+0
+2
+3
+9
+0
+.
+5 2 ;
+.
+2
+2
+2
+2
+2
+0
+2
+2
+2
+1
+.
+.
+1
+1
+1
+0
+0
+0
+1
+0
+0
+1
+0
+0
+1
+1
+1
+1
+0
+0
+0
+1
+1
+1
+1
+1
+0
+1
+1
+0
+0
+1
+1
+1
+1
+0
+0
+1
+2
+1
+3
+0
+3
+3
+3
+0
+2
+3
+1
+2
+4
+2
+0
+2
+3
+9
+0
+.
+5 4 ;
+5 6 ;
+.
+2
+2
+2
+2
+2
+0
+2
+2
+2
+1
+.
+.
+1
+0
+1
+1
+0
+0
+1
+0
+0
+1
+0
+0
+1
+1
+1
+1
+0
+0
+0
+1
+1
+1
+1
+1
+0
+1
+1
+0
+0
+1
+1
+1
+1
+0
+0
+1
+2
+2
+3
+0
+3
+3
+3
+0
+2
+3
+1
+2
+4
+2
+0
+2
+3
+9
+0
+.
+0 3 ;
+.
+2
+2
+2
+2
+2
+0
+2
+2
+2
+1
+.
+.
+1
+0
+0
+1
+1
+0
+1
+0
+0
+1
+0
+0
+1
+1
+1
+1
+0
+0
+0
+1
+1
+1
+1
+1
+0
+1
+1
+0
+0
+1
+1
+1
+1
+0
+0
+1
+2
+3
+3
+0
+3
+3
+3
+0
+2
+3
+1
+2
+4
+2
+0
+2
+3
+9
+0
+.
+0 3 ;
+.
+2
+2
+2
+2
+2
+0
+2
+2
+2
+1
+.
+.
+1
+0
+0
+0
+1
+1
+1
+0
+0
+1
+0
+0
+1
+1
+1
+1
+0
+0
+0
+1
+1
+1
+1
+1
+0
+1
+1
+0
+0
+1
+1
+1
+1
+0
+0
+1
+2
+4
+3
+0
+3
+3
+3
+0
+2
+3
+1
+2
+4
+2
+0
+2
+3
+9
+0
+.
+0 3 ;
+.
+2
+2
+2
+2
+2
+3
+2
+2
+2
+1
+.
+.
+1
+0
+0
+1
+1
+1
+1
+0
+0
+1
+0
+0
+1
+1
+1
+0
+0
+0
+0
+1
+1
+1
+1
+1
+0
+1
+1
+0
+0
+1
+1
+1
+1
+0
+0
+1
+2
+4
+3
+0
+3
+3
+3
+0
+2
+3
+0
+2
+4
+2
+0
+2
+3
+9
+0
+.
+5 3 ;
+.
+2
+2
+2
+2
+2
+1
+2
+2
+2
+1
+.
+.
+1
+0
+0
+1
+1
+1
+1
+0
+0
+1
+0
+0
+1
+1
+1
+0
+0
+0
+0
+1
+1
+1
+1
+1
+0
+1
+1
+0
+0
+1
+1
+1
+1
+0
+0
+1
+2
+4
+3
+0
+3
+3
+3
+0
+2
+3
+0
+2
+4
+2
+0
+2
+3
+9
+0
+.
+5 5 ;
+5 6 ;
+.
+2
+2
+2
+2
+2
+1
+2
+2
+2
+1
+.
+.
+1
+0
+0
+1
+1
+1
+1
+0
+0
+1
+0
+0
+0
+1
+1
+1
+0
+0
+0
+1
+1
+1
+1
+1
+0
+1
+1
+0
+0
+1
+1
+1
+1
+0
+0
+1
+2
+4
+3
+1
+3
+3
+3
+0
+2
+3
+0
+2
+4
+2
+0
+2
+3
+9
+0
+.
+1 3 ;
+.
+2
+2
+2
+2
+2
+1
+2
+2
+2
+1
+.
+.
+1
+0
+0
+1
+1
+1
+1
+0
+0
+1
+0
+0
+0
+0
+1
+1
+1
+0
+0
+1
+1
+1
+1
+1
+0
+1
+1
+0
+0
+1
+1
+1
+1
+0
+0
+1
+2
+4
+3
+2
+3
+3
+3
+0
+2
+3
+0
+2
+4
+2
+0
+2
+3
+9
+0
+.
+1 3 ;
+.
+2
+2
+2
+2
+2
+1
+2
+2
+2
+1
+.
+.
+1
+0
+0
+1
+1
+1
+1
+0
+0
+1
+0
+0
+0
+0
+0
+1
+1
+1
+0
+1
+1
+1
+1
+1
+0
+1
+1
+0
+0
+1
+1
+1
+1
+0
+0
+1
+2
+4
+3
+3
+3
+3
+3
+0
+2
+3
+0
+2
+4
+2
+0
+2
+3
+9
+0
+.
+1 3 ;
+.
+2
+2
+2
+2
+2
+1
+2
+2
+2
+1
+.
+.
+1
+0
+0
+1
+1
+1
+1
+0
+0
+1
+0
+0
+0
+1
+0
+1
+1
+1
+0
+1
+1
+1
+1
+1
+0
+0
+1
+0
+0
+1
+1
+1
+1
+0
+0
+1
+2
+4
+3
+3
+3
+3
+3
+0
+2
+2
+0
+2
+4
+2
+0
+2
+3
+9
+0
+.
+4 2 ;
+.
+2
+2
+2
+2
+2
+1
+2
+2
+2
+1
+.
+.
+1
+0
+0
+1
+1
+1
+1
+1
+0
+1
+0
+0
+0
+1
+0
+1
+1
+1
+0
+0
+1
+1
+1
+1
+0
+0
+1
+0
+0
+1
+1
+1
+1
+0
+0
+1
+2
+4
+3
+3
+3
+3
+3
+0
+2
+1
+0
+2
+4
+2
+0
+2
+3
+9
+0
+.
+4 2 ;
+.
+2
+2
+2
+2
+2
+1
+2
+2
+2
+1
+.
+.
+1
+1
+0
+1
+1
+1
+1
+1
+0
+1
+0
+0
+0
+0
+0
+1
+1
+1
+0
+0
+1
+1
+1
+1
+0
+0
+1
+0
+0
+1
+1
+1
+1
+0
+0
+1
+2
+4
+3
+3
+3
+3
+3
+0
+2
+0
+0
+2
+4
+2
+0
+2
+3
+9
+0
+.
+4 2 ;
+.
+2
+2
+2
+2
+2
+1
+2
+2
+2
+1
+.
+.
+1
+1
+0
+1
+1
+1
+1
+1
+0
+1
+0
+0
+0
+0
+1
+1
+1
+1
+0
+0
+1
+1
+1
+1
+0
+0
+0
+0
+0
+1
+1
+1
+1
+0
+0
+1
+2
+4
+3
+3
+3
+3
+3
+0
+2
+0
+0
+2
+4
+2
+0
+2
+2
+9
+0
+.
+8 2 ;
+.
+2
+2
+2
+2
+2
+1
+2
+2
+2
+1
+.
+.
+1
+1
+0
+1
+1
+1
+1
+1
+1
+1
+0
+0
+0
+0
+1
+1
+1
+1
+0
+0
+0
+1
+1
+1
+0
+0
+0
+0
+0
+1
+1
+1
+1
+0
+0
+1
+2
+4
+3
+3
+3
+3
+3
+0
+2
+0
+0
+2
+4
+2
+0
+2
+1
+9
+0
+.
+8 2 ;
+.
+2
+2
+2
+2
+2
+1
+2
+2
+2
+1
+.
+.
+1
+1
+0
+1
+1
+1
+1
+1
+1
+1
+0
+0
+0
+0
+1
+1
+1
+1
+0
+0
+1
+1
+1
+0
+0
+0
+0
+0
+0
+1
+1
+1
+1
+0
+0
+1
+2
+4
+3
+3
+3
+2
+3
+0
+2
+0
+0
+2
+4
+2
+0
+2
+1
+9
+0
+.
+2 2 ;
+.
+2
+2
+2
+2
+2
+1
+2
+2
+2
+1
+.
+.
+1
+1
+0
+1
+1
+1
+1
+1
+1
+1
+0
+0
+0
+0
+1
+1
+1
+1
+0
+1
+1
+1
+0
+0
+0
+0
+0
+0
+0
+1
+1
+1
+1
+0
+0
+1
+2
+4
+3
+3
+3
+1
+3
+0
+2
+0
+0
+2
+4
+2
+0
+2
+1
+9
+0
+.
+2 2 ;
+.
+2
+2
+2
+2
+2
+1
+2
+2
+2
+1
+.
+.
+1
+1
+0
+1
+1
+1
+1
+1
+1
+1
+0
+0
+0
+0
+1
+1
+1
+1
+1
+1
+1
+0
+0
+0
+0
+0
+0
+0
+0
+1
+1
+1
+1
+0
+0
+1
+2
+4
+3
+3
+3
+0
+3
+0
+2
+0
+0
+2
+4
+2
+0
+2
+1
+9
+0
+.
+2 2 ;
+.
+2
+2
+2
+2
+2
+1
+2
+2
+2
+1
+.
+.
+1
+1
+1
+1
+1
+1
+1
+1
+1
+1
+0
+0
+0
+0
+0
+1
+1
+1
+1
+1
+1
+0
+0
+0
+0
+0
+0
+0
+0
+1
+1
+1
+1
+0
+0
+1
+2
+4
+3
+3
+3
+0
+3
+0
+2
+0
+0
+2
+4
+2
+0
+2
+0
+9
+0
+.
+8 2 ;
+.
+2
+2
+2
+2
+2
+1
+2
+2
+2
+1
+.
+.
+1
+1
+1
+1
+1
+1
+1
+1
+1
+1
+0
+0
+0
+0
+1
+1
+1
+0
+1
+1
+1
+0
+0
+0
+0
+0
+0
+0
+0
+1
+1
+1
+1
+0
+0
+1
+2
+4
+3
+2
+3
+0
+3
+0
+2
+0
+0
+2
+4
+2
+0
+2
+0
+9
+0
+.
+1 2 ;
+.
+2
+2
+2
+2
+2
+1
+2
+2
+2
+1
+.
+.
+1
+1
+1
+1
+1
+1
+1
+1
+1
+1
+0
+0
+0
+1
+1
+1
+0
+0
+1
+1
+1
+0
+0
+0
+0
+0
+0
+0
+0
+1
+1
+1
+1
+0
+0
+1
+2
+4
+3
+1
+3
+0
+3
+0
+2
+0
+0
+2
+4
+2
+0
+2
+0
+9
+0
+.
+1 2 ;
+.
+2
+2
+2
+2
+2
+1
+2
+2
+2
+1
+.
+.
+1
+1
+1
+1
+1
+1
+1
+1
+1
+1
+0
+0
+1
+1
+1
+0
+0
+0
+1
+1
+1
+0
+0
+0
+0
+0
+0
+0
+0
+1
+1
+1
+1
+0
+0
+1
+2
+4
+3
+0
+3
+0
+3
+0
+2
+0
+0
+2
+4
+2
+0
+2
+0
+9
+0
+.
+1 2 ;
+.
+2
+2
+2
+2
+2
+3
+2
+2
+2
+1
+.
+.
+1
+1
+1
+0
+1
+1
+1
+1
+1
+1
+0
+0
+1
+1
+1
+1
+0
+0
+1
+1
+1
+0
+0
+0
+0
+0
+0
+0
+0
+1
+1
+1
+1
+0
+0
+1
+2
+4
+3
+0
+3
+0
+3
+0
+2
+0
+1
+2
+4
+2
+0
+2
+0
+9
+0
+.
+5 2 ;
+.
+2
+2
+2
+2
+2
+1
+2
+2
+2
+1
+.
+.
+1
+1
+1
+0
+1
+1
+1
+1
+1
+1
+0
+0
+1
+1
+1
+1
+0
+0
+1
+1
+1
+0
+0
+0
+0
+0
+0
+0
+0
+1
+1
+1
+1
+0
+0
+1
+2
+4
+3
+0
+3
+0
+3
+0
+2
+0
+1
+2
+4
+2
+0
+2
+0
+9
+0
+.
+5 5 ;
+5 6 ;
+.
+2
+2
+2
+2
+2
+3
+2
+2
+2
+1
+.
+.
+1
+1
+1
+0
+1
+1
+1
+1
+1
+0
+0
+0
+1
+1
+1
+1
+0
+0
+1
+1
+1
+1
+0
+0
+0
+0
+0
+0
+0
+1
+1
+1
+1
+0
+0
+1
+2
+4
+3
+0
+3
+0
+3
+0
+2
+0
+2
+2
+4
+2
+0
+2
+0
+9
+0
+.
+5 2 ;
+.
+2
+2
+2
+2
+2
+1
+2
+2
+2
+1
+.
+.
+1
+1
+1
+0
+1
+1
+1
+1
+1
+0
+0
+0
+1
+1
+1
+1
+0
+0
+1
+1
+1
+1
+0
+0
+0
+0
+0
+0
+0
+1
+1
+1
+1
+0
+0
+1
+2
+4
+3
+0
+3
+0
+3
+0
+2
+0
+2
+2
+4
+2
+0
+2
+0
+9
+0
+.
+5 5 ;
+5 6 ;
+.
+2
+2
+2
+2
+2
+3
+2
+2
+2
+1
+.
+.
+1
+1
+1
+0
+1
+1
+1
+1
+1
+0
+0
+0
+1
+1
+1
+0
+0
+0
+1
+1
+1
+1
+0
+0
+0
+0
+0
+1
+0
+1
+1
+1
+1
+0
+0
+1
+2
+4
+3
+0
+3
+0
+3
+0
+2
+0
+3
+2
+4
+2
+0
+2
+0
+9
+0
+.
+5 2 ;
+.
+2
+2
+2
+2
+2
+1
+2
+2
+2
+1
+.
+.
+1
+1
+1
+0
+1
+1
+1
+1
+1
+0
+0
+0
+1
+1
+1
+0
+0
+0
+1
+1
+1
+1
+0
+0
+0
+0
+0
+1
+0
+1
+1
+1
+1
+0
+0
+1
+2
+4
+3
+0
+3
+0
+3
+0
+2
+0
+3
+2
+4
+2
+0
+2
+0
+9
+0
+.
+5 5 ;
+5 6 ;
+.
+2
+2
+2
+2
+2
+3
+2
+2
+2
+1
+.
+.
+1
+1
+1
+0
+1
+1
+1
+1
+1
+0
+0
+0
+1
+1
+1
+0
+0
+0
+1
+1
+1
+0
+0
+0
+0
+0
+0
+1
+0
+1
+1
+1
+1
+1
+0
+1
+2
+4
+3
+0
+3
+0
+3
+0
+2
+0
+4
+2
+4
+2
+0
+2
+0
+9
+0
+.
+5 2 ;
+.
+2
+2
+2
+2
+2
+2
+2
+2
+2
+0
+.
+.
+1
+1
+1
+0
+1
+1
+1
+1
+1
+0
+0
+0
+1
+1
+1
+0
+0
+0
+1
+1
+1
+0
+0
+0
+0
+0
+0
+1
+0
+1
+1
+1
+1
+1
+0
+1
+2
+4
+3
+0
+3
+0
+3
+0
+2
+0
+4
+2
+4
+2
+0
+2
+0
+9
+1
+.
+5 7 ;
+9 0 ;
+.
+.