UniTO/anno3/vpc/consegne/3/dekker_WN.2-CTL model checking of Unfolding of CPN.solution/Unfolding of CPN.net
2024-10-29 09:11:05 +01:00

953 lines
29 KiB
Text
Executable file

|0|
|
f 0 46 0 72 0 0 0
TURN_t1 1 1.0 0.8333333333333334 0.7164583333333333 1.0289583333333334 0
TURN_t2 0 1.0 1.3333333333333333 0.7164583333333333 1.5289583333333334 0
local_P 1 5.5 1.6666666666666667 5.294583333333333 1.8622916666666667 0
local_Q 1 5.5 2.1666666666666665 5.284166666666667 2.3622916666666667 0
setTrue_P 0 8.333333333333334 1.6666666666666667 8.034166666666666 1.8622916666666667 0
setTrue_Q 0 8.333333333333334 2.1666666666666665 8.028958333333334 2.3622916666666667 0
setFalse_P 0 11.0 3.8333333333333335 10.690416666666666 4.028958333333333 0
setFalse_Q 0 11.0 4.333333333333333 10.685208333333334 4.528958333333333 0
await_P 0 9.0 6.333333333333333 8.768541666666666 6.528958333333333 0
await_Q 0 9.0 6.833333333333333 8.763333333333334 7.028958333333333 0
while_P 0 14.166666666666666 3.8333333333333335 13.940416666666666 4.028958333333333 0
while_Q 0 14.166666666666666 4.333333333333333 13.935208333333334 4.528958333333333 0
setTrue_2_P 0 12.666666666666666 6.333333333333333 12.310208333333334 6.528958333333333 0
setTrue_2_Q 0 12.666666666666666 6.833333333333333 12.299791666666666 7.028958333333333 0
critical_P 0 17.666666666666668 7.833333333333333 17.388333333333332 8.028958333333334 0
critical_Q 0 17.666666666666668 8.333333333333334 17.377916666666668 8.528958333333334 0
setFalse_2_P 0 9.5 7.833333333333333 9.127916666666666 8.028958333333334 0
setFalse_2_Q 0 9.5 8.333333333333334 9.122708333333334 8.528958333333334 0
want_var_false_false 1 29.166666666666668 5.0 28.528958333333335 5.195625 0
want_var_false_true 0 29.666666666666668 5.0 29.039375000000003 5.195625 0
want_var_true_false 0 29.166666666666668 5.5 28.539375000000003 5.695625 0
want_var_true_true 0 29.666666666666668 5.5 29.049791666666668 5.695625 0
setTrue_pw_P_false_false 0 26.333333333333332 2.1666666666666665 25.534166666666668 2.3622916666666667 0
setTrue_pw_P_false_true 0 26.333333333333332 2.6666666666666665 25.544583333333335 2.8622916666666662 0
setTrue_pw_P_true_false 0 26.833333333333332 2.1666666666666665 26.044583333333335 2.3622916666666667 0
setTrue_pw_P_true_true 0 26.833333333333332 2.6666666666666665 26.055000000000003 2.8622916666666662 0
setTrue_pw_Q_false_false 0 26.333333333333332 2.6666666666666665 25.528958333333335 2.8622916666666662 0
setTrue_pw_Q_false_true 0 26.333333333333332 3.1666666666666665 25.539375000000003 3.3622916666666662 0
setTrue_pw_Q_true_false 0 26.833333333333332 2.6666666666666665 26.039375000000003 2.8622916666666662 0
setTrue_pw_Q_true_true 0 26.833333333333332 3.1666666666666665 26.049791666666668 3.3622916666666662 0
setFalse_pw_P_false_false 0 32.0 2.1666666666666665 31.190416666666668 2.3622916666666667 0
setFalse_pw_P_false_true 0 32.0 2.6666666666666665 31.200833333333335 2.8622916666666662 0
setFalse_pw_P_true_false 0 32.5 2.1666666666666665 31.700833333333335 2.3622916666666667 0
setFalse_pw_P_true_true 0 32.5 2.6666666666666665 31.711250000000003 2.8622916666666662 0
setFalse_pw_Q_false_false 0 32.0 2.6666666666666665 31.180000000000003 2.8622916666666662 0
setFalse_pw_Q_false_true 0 32.0 3.1666666666666665 31.190416666666668 3.3622916666666662 0
setFalse_pw_Q_true_false 0 32.5 2.6666666666666665 31.690416666666668 2.8622916666666662 0
setFalse_pw_Q_true_true 0 32.5 3.1666666666666665 31.700833333333335 3.3622916666666662 0
identity_pw_P_false_false 0 29.166666666666668 2.1666666666666665 28.357083333333335 2.3622916666666667 0
identity_pw_P_false_true 0 29.166666666666668 2.6666666666666665 28.372708333333335 2.8622916666666662 0
identity_pw_P_true_false 0 29.666666666666668 2.1666666666666665 28.872708333333335 2.3622916666666667 0
identity_pw_P_true_true 0 29.666666666666668 2.6666666666666665 28.883125000000003 2.8622916666666662 0
identity_pw_Q_false_false 0 29.166666666666668 2.6666666666666665 28.351875000000003 2.8622916666666662 0
identity_pw_Q_false_true 0 29.166666666666668 3.1666666666666665 28.362291666666668 3.3622916666666662 0
identity_pw_Q_true_false 0 29.666666666666668 2.6666666666666665 28.862291666666668 2.8622916666666662 0
identity_pw_Q_true_true 0 29.666666666666668 3.1666666666666665 28.872708333333335 3.3622916666666662 0
T1_p_P 1.0 0 0 1 1 6.833333333333333 1.6666666666666667 6.651041666666667 1.4739583333333333 6.916666666666667 1.734375 0
1 3 1 0
6.0625976562499995 1.6666666666666667
1
1 5 0 0
0
T1_p_Q 1.0 0 0 1 1 6.833333333333333 2.1666666666666665 6.645833333333333 1.9739583333333333 6.916666666666667 2.234375 0
1 4 1 0
6.0625976562499995 2.1666666666666665
1
1 6 0 0
0
T2_b_false_c_false_p_P 1.0 0 0 2 0 10.166666666666666 1.6666666666666667 9.463541666666666 1.4739583333333333 10.25 1.734375 0
1 5 0 0
-1 19 3 0
10.166666666666666 2.6666666666666665
10.0 2.8333333333333335
29.25 7.916666666666667
2
1 11 1 0
14.166666666666666 1.6666666666666667
-1 23 2 0
10.166666666666666 0.3333333333333333
26.333333333333332 0.3333333333333333
0
T2_b_false_c_false_p_Q 1.0 0 0 2 0 10.166666666666666 2.1666666666666665 9.458333333333334 1.9739583333333333 10.25 2.234375 0
1 6 0 0
-1 19 3 0
10.166666666666666 3.1666666666666665
10.0 3.3333333333333335
29.25 8.416666666666666
2
1 12 1 0
14.166666666666666 2.1666666666666665
-1 27 2 0
10.166666666666666 0.8333333333333334
26.333333333333332 0.8333333333333334
0
T2_b_false_c_true_p_P 1.0 0 0 2 0 10.666666666666666 1.6666666666666667 9.979166666666666 1.4739583333333333 10.75 1.734375 0
1 5 0 0
-1 20 3 0
10.666666666666666 2.6666666666666665
10.5 2.8333333333333335
29.75 7.916666666666667
2
1 11 1 0
14.666666666666666 1.6666666666666667
-1 24 2 0
10.666666666666666 0.3333333333333333
26.833333333333332 0.3333333333333333
0
T2_b_false_c_true_p_Q 1.0 0 0 2 0 10.666666666666666 2.1666666666666665 9.973958333333334 1.9739583333333333 10.75 2.234375 0
1 6 0 0
-1 20 3 0
10.666666666666666 3.1666666666666665
10.5 3.3333333333333335
29.75 8.416666666666666
2
1 12 1 0
14.666666666666666 2.1666666666666665
-1 28 2 0
10.666666666666666 0.8333333333333334
26.833333333333332 0.8333333333333334
0
T2_b_true_c_false_p_P 1.0 0 0 2 0 10.166666666666666 2.1666666666666665 9.479166666666666 1.9739583333333333 10.25 2.234375 0
1 5 0 0
-1 21 3 0
10.166666666666666 3.1666666666666665
10.0 3.3333333333333335
29.25 8.416666666666666
2
1 11 1 0
14.166666666666666 2.1666666666666665
-1 25 2 0
10.166666666666666 0.8333333333333334
26.333333333333332 0.8333333333333334
0
T2_b_true_c_false_p_Q 1.0 0 0 2 0 10.166666666666666 2.6666666666666665 9.473958333333334 2.4739583333333335 10.25 2.734375 0
1 6 0 0
-1 21 3 0
10.166666666666666 3.6666666666666665
10.0 3.8333333333333335
29.25 8.916666666666666
2
1 12 1 0
14.166666666666666 2.6666666666666665
-1 29 2 0
10.166666666666666 1.3333333333333333
26.333333333333332 1.3333333333333333
0
T2_b_true_c_true_p_P 1.0 0 0 2 0 10.666666666666666 2.1666666666666665 9.994791666666666 1.9739583333333333 10.75 2.234375 0
1 5 0 0
-1 22 3 0
10.666666666666666 3.1666666666666665
10.5 3.3333333333333335
29.75 8.416666666666666
2
1 11 1 0
14.666666666666666 2.1666666666666665
-1 26 2 0
10.666666666666666 0.8333333333333334
26.833333333333332 0.8333333333333334
0
T2_b_true_c_true_p_Q 1.0 0 0 2 0 10.666666666666666 2.6666666666666665 9.984375 2.4739583333333335 10.75 2.734375 0
1 6 0 0
-1 22 3 0
10.666666666666666 3.6666666666666665
10.5 3.8333333333333335
29.75 8.916666666666666
2
1 12 1 0
14.666666666666666 2.6666666666666665
-1 30 2 0
10.666666666666666 1.3333333333333333
26.833333333333332 1.3333333333333333
0
T7_b_false_c_false_p_P 1.0 0 0 2 1 9.0 3.8333333333333335 8.296875 3.640625 9.083333333333334 3.9010416666666665 0
1 7 0 0
-1 19 4 0
10.166666666666666 2.9166666666666665
6.25 3.5
6.416666666666667 6.833333333333333
26.5 6.583333333333333
2
-1 31 7 0
6.75 4.0
30.5 7.333333333333333
31.083333333333332 1.0833333333333333
32.75 0.5833333333333334
32.666666666666664 0.5833333333333334
31.916666666666668 1.25
32.0 1.6666666666666667
1 9 0 0
0
T7_b_false_c_false_p_Q 1.0 0 0 2 1 9.0 4.333333333333333 8.291666666666666 4.140625 9.083333333333334 4.401041666666667 0
1 8 0 0
-1 19 4 0
10.166666666666666 3.4166666666666665
6.25 4.0
6.416666666666667 7.333333333333333
26.5 7.083333333333333
2
-1 35 7 0
6.75 4.5
30.5 7.833333333333333
31.083333333333332 1.5833333333333333
32.75 1.0833333333333333
32.666666666666664 1.0833333333333333
31.916666666666668 1.75
32.0 2.1666666666666665
1 10 0 0
0
T7_b_false_c_true_p_P 1.0 0 0 2 1 9.5 3.8333333333333335 8.8125 3.640625 9.583333333333334 3.9010416666666665 0
1 7 0 0
-1 20 4 0
10.666666666666666 2.9166666666666665
6.75 3.5
6.916666666666667 6.833333333333333
27.0 6.583333333333333
2
-1 32 7 0
7.25 4.0
31.0 7.333333333333333
31.583333333333332 1.0833333333333333
33.25 0.5833333333333334
33.166666666666664 0.5833333333333334
32.416666666666664 1.25
32.5 1.6666666666666667
1 9 0 0
0
T7_b_false_c_true_p_Q 1.0 0 0 2 1 9.5 4.333333333333333 8.807291666666666 4.140625 9.583333333333334 4.401041666666667 0
1 8 0 0
-1 20 4 0
10.666666666666666 3.4166666666666665
6.75 4.0
6.916666666666667 7.333333333333333
27.0 7.083333333333333
2
-1 36 7 0
7.25 4.5
31.0 7.833333333333333
31.583333333333332 1.5833333333333333
33.25 1.0833333333333333
33.166666666666664 1.0833333333333333
32.416666666666664 1.75
32.5 2.1666666666666665
1 10 0 0
0
T7_b_true_c_false_p_P 1.0 0 0 2 1 9.0 4.333333333333333 8.3125 4.140625 9.083333333333334 4.401041666666667 0
1 7 0 0
-1 21 4 0
10.166666666666666 3.4166666666666665
6.25 4.0
6.416666666666667 7.333333333333333
26.5 7.083333333333333
2
-1 33 7 0
6.75 4.5
30.5 7.833333333333333
31.083333333333332 1.5833333333333333
32.75 1.0833333333333333
32.666666666666664 1.0833333333333333
31.916666666666668 1.75
32.0 2.1666666666666665
1 9 0 0
0
T7_b_true_c_false_p_Q 1.0 0 0 2 1 9.0 4.833333333333333 8.307291666666666 4.640625 9.083333333333334 4.901041666666667 0
1 8 0 0
-1 21 4 0
10.166666666666666 3.9166666666666665
6.25 4.5
6.416666666666667 7.833333333333333
26.5 7.583333333333333
2
-1 37 7 0
6.75 5.0
30.5 8.333333333333334
31.083333333333332 2.0833333333333335
32.75 1.5833333333333333
32.666666666666664 1.5833333333333333
31.916666666666668 2.25
32.0 2.6666666666666665
1 10 0 0
0
T7_b_true_c_true_p_P 1.0 0 0 2 1 9.5 4.333333333333333 8.828125 4.140625 9.583333333333334 4.401041666666667 0
1 7 0 0
-1 22 4 0
10.666666666666666 3.4166666666666665
6.75 4.0
6.916666666666667 7.333333333333333
27.0 7.083333333333333
2
-1 34 7 0
7.25 4.5
31.0 7.833333333333333
31.583333333333332 1.5833333333333333
33.25 1.0833333333333333
33.166666666666664 1.0833333333333333
32.416666666666664 1.75
32.5 2.1666666666666665
1 9 0 0
0
T7_b_true_c_true_p_Q 1.0 0 0 2 1 9.5 4.833333333333333 8.817708333333334 4.640625 9.583333333333334 4.901041666666667 0
1 8 0 0
-1 22 4 0
10.666666666666666 3.9166666666666665
6.75 4.5
6.916666666666667 7.833333333333333
27.0 7.583333333333333
2
-1 38 7 0
7.25 5.0
31.0 8.333333333333334
31.583333333333332 2.0833333333333335
33.25 1.5833333333333333
33.166666666666664 1.5833333333333333
32.416666666666664 2.25
32.5 2.6666666666666665
1 10 0 0
0
T9_p_P_t_t1 1.0 0 0 2 1 11.166666666666666 6.333333333333333 10.828125 6.140625 11.25 6.401041666666667 0
1 9 0 0
-1 1 3 0
10.75 6.166666666666667
10.166666666666666 7.583333333333333
5.5 7.583333333333333
2
1 13 1 0
11.75 6.333333333333333
-1 1 4 0
12.416666666666666 5.75
13.083333333333334 5.583333333333333
13.416666666666666 2.1666666666666665
9.583333333333334 2.1666666666666665
0
T9_p_Q_t_t2 1.0 0 0 2 1 11.666666666666666 6.833333333333333 11.322916666666666 6.640625 11.75 6.901041666666667 0
1 10 0 0
-1 2 3 0
11.25 6.666666666666667
10.666666666666666 8.083333333333334
6.0 8.083333333333334
2
1 14 1 0
12.25 6.833333333333333
-1 2 4 0
12.916666666666666 6.25
13.583333333333334 6.083333333333333
13.916666666666666 2.6666666666666665
10.083333333333334 2.6666666666666665
0
T12_b_false_c_false_p_P 1.0 0 0 2 1 14.166666666666666 6.333333333333333 13.4375 6.140625 14.25 6.401041666666667 0
1 13 0 0
-1 19 2 0
14.166666666666666 7.25
27.833333333333332 6.666666666666667
2
1 11 0 0
-1 23 4 0
20.5 6.25
24.0 0.75
26.5 0.3333333333333333
27.25 1.0833333333333333
0
T12_b_false_c_false_p_Q 1.0 0 0 2 1 14.166666666666666 6.833333333333333 13.432291666666666 6.640625 14.25 6.901041666666667 0
1 14 0 0
-1 19 2 0
14.166666666666666 7.75
27.833333333333332 7.166666666666667
2
1 12 0 0
-1 27 4 0
20.5 6.75
24.0 1.25
26.5 0.8333333333333334
27.25 1.5833333333333333
0
T12_b_false_c_true_p_P 1.0 0 0 2 1 14.666666666666666 6.333333333333333 13.953125 6.140625 14.75 6.401041666666667 0
1 13 0 0
-1 20 2 0
14.666666666666666 7.25
28.333333333333332 6.666666666666667
2
1 11 0 0
-1 24 4 0
21.0 6.25
24.5 0.75
27.0 0.3333333333333333
27.75 1.0833333333333333
0
T12_b_false_c_true_p_Q 1.0 0 0 2 1 14.666666666666666 6.833333333333333 13.947916666666666 6.640625 14.75 6.901041666666667 0
1 14 0 0
-1 20 2 0
14.666666666666666 7.75
28.333333333333332 7.166666666666667
2
1 12 0 0
-1 28 4 0
21.0 6.75
24.5 1.25
27.0 0.8333333333333334
27.75 1.5833333333333333
0
T12_b_true_c_false_p_P 1.0 0 0 2 1 14.166666666666666 6.833333333333333 13.453125 6.640625 14.25 6.901041666666667 0
1 13 0 0
-1 21 2 0
14.166666666666666 7.75
27.833333333333332 7.166666666666667
2
1 11 0 0
-1 25 4 0
20.5 6.75
24.0 1.25
26.5 0.8333333333333334
27.25 1.5833333333333333
0
T12_b_true_c_false_p_Q 1.0 0 0 2 1 14.166666666666666 7.333333333333333 13.447916666666666 7.140625 14.25 7.401041666666667 0
1 14 0 0
-1 21 2 0
14.166666666666666 8.25
27.833333333333332 7.666666666666667
2
1 12 0 0
-1 29 4 0
20.5 7.25
24.0 1.75
26.5 1.3333333333333333
27.25 2.0833333333333335
0
T12_b_true_c_true_p_P 1.0 0 0 2 1 14.666666666666666 6.833333333333333 13.96875 6.640625 14.75 6.901041666666667 0
1 13 0 0
-1 22 2 0
14.666666666666666 7.75
28.333333333333332 7.166666666666667
2
1 11 0 0
-1 26 4 0
21.0 6.75
24.5 1.25
27.0 0.8333333333333334
27.75 1.5833333333333333
0
T12_b_true_c_true_p_Q 1.0 0 0 2 1 14.666666666666666 7.333333333333333 13.958333333333334 7.140625 14.75 7.401041666666667 0
1 14 0 0
-1 22 2 0
14.666666666666666 8.25
28.333333333333332 7.666666666666667
2
1 12 0 0
-1 30 4 0
21.0 7.25
24.5 1.75
27.0 1.3333333333333333
27.75 2.0833333333333335
0
T15_b_false_c_false_p_P 1.0 0 0 2 1 17.666666666666668 3.5 16.9375 3.3072916666666665 17.75 3.5677083333333335 0
-1 19 7 0
16.333333333333332 3.4166666666666665
15.833333333333334 2.8333333333333335
17.666666666666668 2.25
19.5 3.75
20.083333333333332 4.5
19.833333333333332 7.25
30.083333333333332 6.166666666666667
1 11 1 0
16.583333333333332 3.8333333333333335
2
1 15 0 0
-1 39 3 0
20.666666666666668 2.9166666666666665
25.666666666666668 1.75
29.166666666666668 1.6666666666666667
0
T15_b_false_c_false_p_Q 1.0 0 0 2 1 17.666666666666668 4.0 16.932291666666668 3.8072916666666665 17.75 4.067708333333333 0
-1 19 7 0
16.333333333333332 3.9166666666666665
15.833333333333334 3.3333333333333335
17.666666666666668 2.75
19.5 4.25
20.083333333333332 5.0
19.833333333333332 7.75
30.083333333333332 6.666666666666667
1 12 1 0
16.583333333333332 4.333333333333333
2
1 16 0 0
-1 43 3 0
20.666666666666668 3.4166666666666665
25.666666666666668 2.25
29.166666666666668 2.1666666666666665
0
T15_b_false_c_true_p_Q 1.0 0 0 2 1 18.166666666666668 4.0 17.447916666666668 3.8072916666666665 18.25 4.067708333333333 0
-1 20 7 0
16.833333333333332 3.9166666666666665
16.333333333333332 3.3333333333333335
18.166666666666668 2.75
20.0 4.25
20.583333333333332 5.0
20.333333333333332 7.75
30.583333333333332 6.666666666666667
1 12 1 0
17.083333333333332 4.333333333333333
2
1 16 0 0
-1 44 3 0
21.166666666666668 3.4166666666666665
26.166666666666668 2.25
29.666666666666668 2.1666666666666665
0
T15_b_true_c_false_p_P 1.0 0 0 2 1 17.666666666666668 4.0 16.953125 3.8072916666666665 17.75 4.067708333333333 0
-1 21 7 0
16.333333333333332 3.9166666666666665
15.833333333333334 3.3333333333333335
17.666666666666668 2.75
19.5 4.25
20.083333333333332 5.0
19.833333333333332 7.75
30.083333333333332 6.666666666666667
1 11 1 0
16.583333333333332 4.333333333333333
2
1 15 0 0
-1 41 3 0
20.666666666666668 3.4166666666666665
25.666666666666668 2.25
29.166666666666668 2.1666666666666665
0
T16_p_P_t_t1 1.0 0 0 2 1 15.5 7.333333333333333 15.135416666666666 7.140625 15.583333333333334 7.401041666666667 0
1 15 0 0
-1 1 2 0
16.583333333333332 6.166666666666667
5.583333333333333 2.0
2
-1 2 0 0
1 17 0 0
0
T16_p_P_t_t2 1.0 0 0 2 1 16.0 7.333333333333333 15.635416666666666 7.140625 16.083333333333332 7.401041666666667 0
1 15 0 0
-1 2 2 0
17.083333333333332 6.166666666666667
6.083333333333333 2.0
2
-1 2 0 0
1 17 0 0
0
RESET_1_b_false_c_false_p_P 1.0 0 0 2 1 5.666666666666667 7.833333333333333 4.729166666666667 7.640625 5.75 7.901041666666667 0
1 17 0 0
-1 19 5 0
5.666666666666667 6.416666666666667
5.583333333333333 5.166666666666667
6.916666666666667 4.416666666666667
8.166666666666666 9.666666666666666
28.5 7.083333333333333
2
-1 3 2 0
4.75 7.833333333333333
4.833333333333333 1.6666666666666667
-1 31 5 0
5.666666666666667 8.833333333333334
25.916666666666668 9.166666666666666
24.916666666666668 0.3333333333333333
25.0 0.25
33.25 0.4166666666666667
0
RESET_1_b_false_c_false_p_Q 1.0 0 0 2 1 5.666666666666667 8.333333333333334 4.723958333333333 8.140625 5.75 8.401041666666666 0
1 18 0 0
-1 19 5 0
5.666666666666667 6.916666666666667
5.583333333333333 5.666666666666667
6.916666666666667 4.916666666666667
8.166666666666666 10.166666666666666
28.5 7.583333333333333
2
-1 4 2 0
4.75 8.333333333333334
4.833333333333333 2.1666666666666665
-1 35 5 0
5.666666666666667 9.333333333333334
25.916666666666668 9.666666666666666
24.916666666666668 0.8333333333333334
25.0 0.75
33.25 0.9166666666666666
0
RESET_1_b_false_c_true_p_P 1.0 0 0 2 1 6.166666666666667 7.833333333333333 5.244791666666667 7.640625 6.25 7.901041666666667 0
1 17 0 0
-1 20 5 0
6.166666666666667 6.416666666666667
6.083333333333333 5.166666666666667
7.416666666666667 4.416666666666667
8.666666666666666 9.666666666666666
29.0 7.083333333333333
2
-1 3 2 0
5.25 7.833333333333333
5.333333333333333 1.6666666666666667
-1 32 5 0
6.166666666666667 8.833333333333334
26.416666666666668 9.166666666666666
25.416666666666668 0.3333333333333333
25.5 0.25
33.75 0.4166666666666667
0
RESET_1_b_false_c_true_p_Q 1.0 0 0 2 1 6.166666666666667 8.333333333333334 5.239583333333333 8.140625 6.25 8.401041666666666 0
1 18 0 0
-1 20 5 0
6.166666666666667 6.916666666666667
6.083333333333333 5.666666666666667
7.416666666666667 4.916666666666667
8.666666666666666 10.166666666666666
29.0 7.583333333333333
2
-1 4 2 0
5.25 8.333333333333334
5.333333333333333 2.1666666666666665
-1 36 5 0
6.166666666666667 9.333333333333334
26.416666666666668 9.666666666666666
25.416666666666668 0.8333333333333334
25.5 0.75
33.75 0.9166666666666666
0
RESET_1_b_true_c_false_p_P 1.0 0 0 2 1 5.666666666666667 8.333333333333334 4.744791666666667 8.140625 5.75 8.401041666666666 0
1 17 0 0
-1 21 5 0
5.666666666666667 6.916666666666667
5.583333333333333 5.666666666666667
6.916666666666667 4.916666666666667
8.166666666666666 10.166666666666666
28.5 7.583333333333333
2
-1 3 2 0
4.75 8.333333333333334
4.833333333333333 2.1666666666666665
-1 33 5 0
5.666666666666667 9.333333333333334
25.916666666666668 9.666666666666666
24.916666666666668 0.8333333333333334
25.0 0.75
33.25 0.9166666666666666
0
RESET_1_b_true_c_false_p_Q 1.0 0 0 2 1 5.666666666666667 8.833333333333334 4.739583333333333 8.640625 5.75 8.901041666666666 0
1 18 0 0
-1 21 5 0
5.666666666666667 7.416666666666667
5.583333333333333 6.166666666666667
6.916666666666667 5.416666666666667
8.166666666666666 10.666666666666666
28.5 8.083333333333334
2
-1 4 2 0
4.75 8.833333333333334
4.833333333333333 2.6666666666666665
-1 37 5 0
5.666666666666667 9.833333333333334
25.916666666666668 10.166666666666666
24.916666666666668 1.3333333333333333
25.0 1.25
33.25 1.4166666666666667
0
RESET_1_b_true_c_true_p_P 1.0 0 0 2 1 6.166666666666667 8.333333333333334 5.260416666666667 8.140625 6.25 8.401041666666666 0
1 17 0 0
-1 22 5 0
6.166666666666667 6.916666666666667
6.083333333333333 5.666666666666667
7.416666666666667 4.916666666666667
8.666666666666666 10.166666666666666
29.0 7.583333333333333
2
-1 3 2 0
5.25 8.333333333333334
5.333333333333333 2.1666666666666665
-1 34 5 0
6.166666666666667 9.333333333333334
26.416666666666668 9.666666666666666
25.416666666666668 0.8333333333333334
25.5 0.75
33.75 0.9166666666666666
0
RESET_1_b_true_c_true_p_Q 1.0 0 0 2 1 6.166666666666667 8.833333333333334 5.255208333333333 8.640625 6.25 8.901041666666666 0
1 18 0 0
-1 22 5 0
6.166666666666667 7.416666666666667
6.083333333333333 6.166666666666667
7.416666666666667 5.416666666666667
8.666666666666666 10.666666666666666
29.0 8.083333333333334
2
-1 4 2 0
5.25 8.833333333333334
5.333333333333333 2.6666666666666665
-1 38 5 0
6.166666666666667 9.833333333333334
26.416666666666668 10.166666666666666
25.416666666666668 1.3333333333333333
25.5 1.25
33.75 1.4166666666666667
0
T5_b_false_c_false_p_P 1.0 0 0 1 0 25.5 3.3333333333333335 24.796875 3.140625 25.583333333333332 3.4010416666666665 0
1 23 0 0
1
1 21 1 0
25.5 5.0
0
T5_b_false_c_true_p_P 1.0 0 0 1 0 26.0 3.3333333333333335 25.3125 3.140625 26.083333333333332 3.4010416666666665 0
1 24 0 0
1
1 22 1 0
26.0 5.0
0
T5_b_true_c_false_p_P 1.0 0 0 1 0 25.5 3.8333333333333335 24.8125 3.640625 25.583333333333332 3.9010416666666665 0
1 25 0 0
1
1 21 1 0
25.5 5.5
0
T5_b_true_c_true_p_P 1.0 0 0 1 0 26.0 3.8333333333333335 25.328125 3.640625 26.083333333333332 3.9010416666666665 0
1 26 0 0
1
1 22 1 0
26.0 5.5
0
T8_b_false_c_false_p_Q 1.0 0 0 1 0 27.166666666666668 3.8333333333333335 26.458333333333332 3.640625 27.25 3.9010416666666665 0
1 27 0 0
1
1 20 1 0
27.166666666666668 5.5
0
T8_b_false_c_true_p_Q 1.0 0 0 1 0 27.666666666666668 3.8333333333333335 26.973958333333332 3.640625 27.75 3.9010416666666665 0
1 28 0 0
1
1 20 1 0
27.666666666666668 5.5
0
T8_b_true_c_false_p_Q 1.0 0 0 1 0 27.166666666666668 4.333333333333333 26.473958333333332 4.140625 27.25 4.401041666666667 0
1 29 0 0
1
1 22 1 0
27.166666666666668 6.0
0
T8_b_true_c_true_p_Q 1.0 0 0 1 0 27.666666666666668 4.333333333333333 26.984375 4.140625 27.75 4.401041666666667 0
1 30 0 0
1
1 22 1 0
27.666666666666668 6.0
0
T14_b_false_c_false_p_P 1.0 0 0 1 0 31.166666666666668 3.3333333333333335 30.4375 3.140625 31.25 3.4010416666666665 0
1 31 0 0
1
1 19 1 0
31.166666666666668 5.0
0
T14_b_false_c_true_p_P 1.0 0 0 1 0 31.666666666666668 3.3333333333333335 30.953125 3.140625 31.75 3.4010416666666665 0
1 32 0 0
1
1 20 1 0
31.666666666666668 5.0
0
T14_b_true_c_false_p_P 1.0 0 0 1 0 31.166666666666668 3.8333333333333335 30.453125 3.640625 31.25 3.9010416666666665 0
1 33 0 0
1
1 19 1 0
31.166666666666668 5.5
0
T14_b_true_c_true_p_P 1.0 0 0 1 0 31.666666666666668 3.8333333333333335 30.96875 3.640625 31.75 3.9010416666666665 0
1 34 0 0
1
1 20 1 0
31.666666666666668 5.5
0
T18_b_false_c_false_p_Q 1.0 0 0 1 0 32.833333333333336 3.8333333333333335 32.098958333333336 3.640625 32.916666666666664 3.9010416666666665 0
1 35 0 0
1
1 19 1 0
32.833333333333336 5.5
0
T18_b_false_c_true_p_Q 1.0 0 0 1 0 33.333333333333336 3.8333333333333335 32.614583333333336 3.640625 33.416666666666664 3.9010416666666665 0
1 36 0 0
1
1 19 1 0
33.333333333333336 5.5
0
T18_b_true_c_false_p_Q 1.0 0 0 1 0 32.833333333333336 4.333333333333333 32.114583333333336 4.140625 32.916666666666664 4.401041666666667 0
1 37 0 0
1
1 21 1 0
32.833333333333336 6.0
0
T18_b_true_c_true_p_Q 1.0 0 0 1 0 33.333333333333336 4.333333333333333 32.625 4.140625 33.416666666666664 4.401041666666667 0
1 38 0 0
1
1 21 1 0
33.333333333333336 6.0
0
T11_b_false_c_false_p_P 1.0 0 0 1 0 29.166666666666668 3.3333333333333335 28.4375 3.140625 29.25 3.4010416666666665 0
1 39 0 0
1
1 19 0 0
0
T11_b_false_c_false_p_Q 1.0 0 0 1 0 29.166666666666668 3.8333333333333335 28.432291666666668 3.640625 29.25 3.9010416666666665 0
1 43 0 0
1
1 19 0 0
0
T11_b_false_c_true_p_P 1.0 0 0 1 0 29.666666666666668 3.3333333333333335 28.953125 3.140625 29.75 3.4010416666666665 0
1 40 0 0
1
1 20 0 0
0
T11_b_false_c_true_p_Q 1.0 0 0 1 0 29.666666666666668 3.8333333333333335 28.947916666666668 3.640625 29.75 3.9010416666666665 0
1 44 0 0
1
1 20 0 0
0
T11_b_true_c_false_p_P 1.0 0 0 1 0 29.166666666666668 3.8333333333333335 28.453125 3.640625 29.25 3.9010416666666665 0
1 41 0 0
1
1 21 0 0
0
T11_b_true_c_false_p_Q 1.0 0 0 1 0 29.166666666666668 4.333333333333333 28.447916666666668 4.140625 29.25 4.401041666666667 0
1 45 0 0
1
1 21 0 0
0
T11_b_true_c_true_p_P 1.0 0 0 1 0 29.666666666666668 3.8333333333333335 28.96875 3.640625 29.75 3.9010416666666665 0
1 42 0 0
1
1 22 0 0
0
T11_b_true_c_true_p_Q 1.0 0 0 1 0 29.666666666666668 4.333333333333333 28.958333333333332 4.140625 29.75 4.401041666666667 0
1 46 0 0
1
1 22 0 0
0
T3_b_false_c_true_p_P_t_t2 1.0 0 0 3 1 13.666666666666666 3.8333333333333335 12.822916666666666 3.640625 13.75 3.9010416666666665 0
1 11 0 0
-1 20 4 0
14.666666666666666 3.25
14.75 5.25
23.333333333333332 8.833333333333334
33.833333333333336 6.25
-1 2 4 0
13.666666666666666 2.9166666666666665
12.0 2.9166666666666665
9.833333333333334 2.9166666666666665
5.0 2.6666666666666665
3
-1 40 5 0
12.916666666666666 4.75
27.583333333333332 8.416666666666666
27.666666666666668 8.5
28.666666666666668 0.9166666666666666
30.583333333333332 0.75
1 7 0 0
-1 2 3 0
14.5 4.916666666666667
14.25 5.083333333333333
3.25 3.3333333333333335
0
T3_b_true_c_false_p_Q_t_t1 1.0 0 0 3 1 12.666666666666666 4.833333333333333 11.817708333333334 4.640625 12.75 4.901041666666667 0
1 12 0 0
-1 21 4 0
13.666666666666666 4.25
13.75 6.25
22.333333333333332 9.833333333333334
32.833333333333336 7.25
-1 1 4 0
12.666666666666666 3.9166666666666665
11.0 3.9166666666666665
8.833333333333334 3.9166666666666665
4.0 3.6666666666666665
3
-1 45 5 0
11.916666666666666 5.75
26.583333333333332 9.416666666666666
26.666666666666668 9.5
27.666666666666668 1.9166666666666667
29.583333333333332 1.75
1 8 0 0
-1 1 3 0
13.5 5.916666666666667
13.25 6.083333333333333
2.25 4.333333333333333
0
T3_b_true_c_true_p_P_t_t2 1.0 0 0 3 1 13.666666666666666 4.333333333333333 12.838541666666666 4.140625 13.75 4.401041666666667 0
1 11 0 0
-1 22 4 0
14.666666666666666 3.75
14.75 5.75
23.333333333333332 9.333333333333334
33.833333333333336 6.75
-1 2 4 0
13.666666666666666 3.4166666666666665
12.0 3.4166666666666665
9.833333333333334 3.4166666666666665
5.0 3.1666666666666665
3
-1 42 5 0
12.916666666666666 5.25
27.583333333333332 8.916666666666666
27.666666666666668 9.0
28.666666666666668 1.4166666666666667
30.583333333333332 1.25
1 7 0 0
-1 2 3 0
14.5 5.416666666666667
14.25 5.583333333333333
3.25 3.8333333333333335
0
T3_b_true_c_true_p_Q_t_t1 1.0 0 0 3 1 13.166666666666666 4.833333333333333 12.333333333333334 4.640625 13.25 4.901041666666667 0
1 12 0 0
-1 22 4 0
14.166666666666666 4.25
14.25 6.25
22.833333333333332 9.833333333333334
33.333333333333336 7.25
-1 1 4 0
13.166666666666666 3.9166666666666665
11.5 3.9166666666666665
9.333333333333334 3.9166666666666665
4.5 3.6666666666666665
3
-1 46 5 0
12.416666666666666 5.75
27.083333333333332 9.416666666666666
27.166666666666668 9.5
28.166666666666668 1.9166666666666667
30.083333333333332 1.75
1 8 0 0
-1 1 3 0
14.0 5.916666666666667
13.75 6.083333333333333
2.75 4.333333333333333
0
T4_p_Q_t_t1 1.0 0 0 2 1 15.5 8.833333333333334 15.15625 8.640625 15.583333333333334 8.901041666666666 0
1 16 0 0
-1 1 6 0
16.666666666666668 9.25
18.0 9.5
19.833333333333332 9.166666666666666
20.0 9.0
19.833333333333332 7.916666666666667
3.3333333333333335 4.0
2
-1 1 3 0
14.166666666666666 9.333333333333334
5.583333333333333 10.0
4.166666666666667 7.0
1 18 0 0
0
T4_p_Q_t_t2 1.0 0 0 2 1 16.0 8.833333333333334 15.65625 8.640625 16.083333333333332 8.901041666666666 0
1 16 0 0
-1 2 6 0
17.166666666666668 9.25
18.5 9.5
20.333333333333332 9.166666666666666
20.5 9.0
20.333333333333332 7.916666666666667
3.8333333333333335 4.0
2
-1 1 3 0
14.666666666666666 9.333333333333334
6.083333333333333 10.0
4.666666666666667 7.0
1 18 0 0
0