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

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

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