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

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

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