From: pimjager Date: Thu, 16 Jun 2016 11:22:14 +0000 (+0200) Subject: working exercise2 X-Git-Url: https://git.martlubbers.net/?a=commitdiff_plain;h=9fb20990d15588f3042851886b4dd4b6b662d0d4;p=mc1516the.git working exercise2 --- diff --git a/uppaal/2.xml b/uppaal/2.xml index 25de23c..0f68e2c 100644 --- 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 //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; */ - + +//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; +*/ E<> Player.done == 1 diff --git a/uppaal/2hardTrace.xtr b/uppaal/2hardTrace.xtr new file mode 100644 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 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 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 ; +. +.