Merge branch 'master' of gitlab.science.ru.nl:mlubbers/mc1516the

[mc1516the.git] / uppaal / 2website2Trace.xtr

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