maggicl
/
soft-an04
Archived
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

grid search completed

This commit is contained in:
Claudio Maggioni 2023-05-09 16:52:07 +02:00
parent de2476e2d6
commit 2addd53076
579 changed files with 14121 additions and 359 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

15
ReversalModel/grid-search.sh Executable file
View File

@ -0,0 +1,15 @@
#!/bin/bash
set -e
SCRIPT_DIR=$(cd -- "$( dirname -- "${BASH_SOURCE[0]}" )" &> /dev/null && pwd)
time_out="time.txt"
# grid search fixed parameters
max=8
prop="seq_eq_parallel"
max_time=300
parallel --jobs 4 \
"$SCRIPT_DIR/test-property.sh" ::: "$prop" ::: "$(seq 2 10)" ::: "$(seq 3 10)" ::: "$(seq 2 10)" ::: "$SCRIPT_DIR/$time_out"

869
ReversalModel/outputs/time.txt Normal file
View File

@ -0,0 +1,869 @@
seq_eq_parallel,2,3,2,
0.12 real 0.03 user 0.02 sys
seq_eq_parallel,2,3,3,
0.12 real 0.03 user 0.03 sys
seq_eq_parallel,2,3,4,
0.12 real 0.04 user 0.02 sys
seq_eq_parallel,2,3,5,
0.14 real 0.05 user 0.03 sys
seq_eq_parallel,2,3,6,
0.14 real 0.06 user 0.02 sys
seq_eq_parallel,2,3,7,
0.16 real 0.07 user 0.02 sys
seq_eq_parallel,2,3,8,
0.18 real 0.09 user 0.03 sys
seq_eq_parallel,2,4,2,
0.12 real 0.04 user 0.02 sys
seq_eq_parallel,2,4,3,
0.14 real 0.06 user 0.02 sys
seq_eq_parallel,2,4,4,
0.18 real 0.10 user 0.03 sys
seq_eq_parallel,2,4,5,
0.26 real 0.17 user 0.03 sys
seq_eq_parallel,2,4,6,
0.37 real 0.28 user 0.03 sys
seq_eq_parallel,2,4,7,
0.58 real 0.48 user 0.04 sys
seq_eq_parallel,2,4,8,
0.82 real 0.71 user 0.05 sys
seq_eq_parallel,2,5,2,
0.15 real 0.06 user 0.03 sys
seq_eq_parallel,2,5,3,
0.26 real 0.17 user 0.03 sys
seq_eq_parallel,2,5,4,
0.56 real 0.45 user 0.04 sys
seq_eq_parallel,2,5,5,
1.21 real 1.08 user 0.07 sys
seq_eq_parallel,2,5,6,
2.68 real 2.45 user 0.16 sys
seq_eq_parallel,2,5,7,
5.27 real 4.93 user 0.27 sys
seq_eq_parallel,2,5,8,
9.00 real 8.38 user 0.44 sys
seq_eq_parallel,2,6,2,
0.34 real 0.16 user 0.03 sys
seq_eq_parallel,2,6,3,
0.92 real 0.72 user 0.05 sys
seq_eq_parallel,2,6,4,
3.01 real 2.70 user 0.16 sys
seq_eq_parallel,2,6,5,
8.75 real 8.18 user 0.42 sys
seq_eq_parallel,2,6,6,
24.91 real 23.53 user 1.20 sys
seq_eq_parallel,2,6,7,
63.94 real 60.85 user 2.89 sys
seq_eq_parallel,2,6,8,
342.41 real 160.09 user 126.62 sys
seq_eq_parallel,2,7,2,
0.83 real 0.51 user 0.05 sys
seq_eq_parallel,2,7,3,
5.13 real 4.67 user 0.31 sys
seq_eq_parallel,2,7,4,
24.95 real 23.38 user 1.38 sys
seq_eq_parallel,2,7,5,
101.42 real 95.14 user 5.84 sys
seq_eq_parallel,2,8,2,
2.14 real 1.75 user 0.11 sys
seq_eq_parallel,2,8,3,
19.55 real 18.40 user 0.98 sys
seq_eq_parallel,3,3,2,
0.30 real 0.05 user 0.06 sys
seq_eq_parallel,3,3,3,
0.33 real 0.06 user 0.07 sys
seq_eq_parallel,3,3,4,
0.44 real 0.08 user 0.07 sys
seq_eq_parallel,3,3,5,
0.52 real 0.11 user 0.09 sys
seq_eq_parallel,3,3,6,
0.75 real 0.15 user 0.08 sys
seq_eq_parallel,3,3,7,
0.77 real 0.21 user 0.08 sys
seq_eq_parallel,3,3,8,
1.00 real 0.28 user 0.10 sys
seq_eq_parallel,3,4,2,
0.41 real 0.08 user 0.07 sys
seq_eq_parallel,3,4,3,
0.70 real 0.16 user 0.08 sys
seq_eq_parallel,3,4,4,
1.06 real 0.31 user 0.10 sys
seq_eq_parallel,3,4,5,
1.71 real 0.61 user 0.13 sys
seq_eq_parallel,3,4,6,
3.81 real 1.14 user 0.31 sys
seq_eq_parallel,3,4,7,
5.40 real 1.95 user 0.47 sys
seq_eq_parallel,3,4,8,
6.31 real 2.87 user 0.49 sys
seq_eq_parallel,3,5,2,
0.90 real 0.19 user 0.08 sys
seq_eq_parallel,3,5,3,
1.82 real 0.67 user 0.18 sys
seq_eq_parallel,3,5,4,
4.27 real 1.83 user 0.33 sys
seq_eq_parallel,3,5,5,
13.23 real 4.74 user 1.46 sys
seq_eq_parallel,3,5,6,
75.60 real 14.34 user 16.88 sys
seq_eq_parallel,3,5,7,
226.55 real 34.58 user 62.64 sys
seq_eq_parallel,4,3,2,
0.43 real 0.05 user 0.06 sys
seq_eq_parallel,4,3,3,
0.39 real 0.08 user 0.07 sys
seq_eq_parallel,4,3,4,
0.41 real 0.10 user 0.05 sys
seq_eq_parallel,4,3,5,
0.38 real 0.15 user 0.06 sys
seq_eq_parallel,4,3,6,
0.48 real 0.21 user 0.08 sys
seq_eq_parallel,4,3,7,
0.63 real 0.33 user 0.10 sys
seq_eq_parallel,4,3,8,
0.67 real 0.37 user 0.10 sys
seq_eq_parallel,4,4,2,
0.44 real 0.12 user 0.07 sys
seq_eq_parallel,4,4,3,
0.58 real 0.30 user 0.06 sys
seq_eq_parallel,4,4,4,
1.19 real 0.77 user 0.14 sys
seq_eq_parallel,4,4,5,
2.61 real 1.53 user 0.31 sys
seq_eq_parallel,4,4,6,
4.05 real 2.87 user 0.55 sys
seq_eq_parallel,4,4,7,
6.40 real 4.73 user 1.03 sys
seq_eq_parallel,4,4,8,
10.47 real 7.63 user 1.96 sys
seq_eq_parallel,4,5,2,
0.99 real 0.46 user 0.11 sys
seq_eq_parallel,4,5,3,
2.40 real 1.72 user 0.28 sys
seq_eq_parallel,4,5,4,
6.93 real 5.02 user 1.14 sys
seq_eq_parallel,4,5,5,
22.23 real 13.75 user 5.59 sys
seq_eq_parallel,4,5,6,
139.63 real 39.78 user 43.62 sys
seq_eq_parallel,5,3,2,
0.44 real 0.07 user 0.07 sys
seq_eq_parallel,5,3,3,
0.38 real 0.13 user 0.07 sys
seq_eq_parallel,5,3,4,
0.51 real 0.19 user 0.09 sys
seq_eq_parallel,5,3,5,
0.58 real 0.31 user 0.08 sys
seq_eq_parallel,5,3,6,
0.65 real 0.42 user 0.07 sys
seq_eq_parallel,5,3,7,
0.82 real 0.58 user 0.08 sys
seq_eq_parallel,5,3,8,
1.28 real 0.87 user 0.14 sys
seq_eq_parallel,5,4,2,
0.53 real 0.15 user 0.08 sys
seq_eq_parallel,5,4,3,
0.80 real 0.40 user 0.09 sys
seq_eq_parallel,5,4,4,
1.29 real 0.90 user 0.14 sys
seq_eq_parallel,5,4,5,
2.67 real 1.93 user 0.28 sys
seq_eq_parallel,5,4,6,
4.68 real 3.51 user 0.60 sys
seq_eq_parallel,5,4,7,
11.94 real 6.67 user 2.18 sys
seq_eq_parallel,5,4,8,
18.38 real 10.46 user 2.77 sys
seq_eq_parallel,5,5,2,
3.16 real 1.22 user 0.20 sys
seq_eq_parallel,5,5,3,
10.96 real 5.20 user 1.10 sys
seq_eq_parallel,5,5,4,
68.06 real 18.49 user 13.30 sys
seq_eq_parallel,6,3,2,
0.46 real 0.11 user 0.08 sys
seq_eq_parallel,6,3,3,
0.60 real 0.22 user 0.09 sys
seq_eq_parallel,6,3,4,
0.79 real 0.38 user 0.09 sys
seq_eq_parallel,6,3,5,
1.48 real 0.66 user 0.13 sys
seq_eq_parallel,6,3,6,
2.33 real 1.06 user 0.21 sys
seq_eq_parallel,6,3,7,
3.64 real 1.49 user 0.23 sys
seq_eq_parallel,6,3,8,
4.19 real 2.08 user 0.31 sys
seq_eq_parallel,6,4,2,
0.74 real 0.34 user 0.08 sys
seq_eq_parallel,6,4,3,
1.84 real 0.92 user 0.13 sys
seq_eq_parallel,6,4,4,
4.65 real 2.20 user 0.33 sys
seq_eq_parallel,6,4,5,
10.27 real 4.76 user 0.92 sys
seq_eq_parallel,6,4,6,
24.70 real 9.22 user 3.10 sys
seq_eq_parallel,6,4,7,
52.76 real 16.49 user 7.90 sys
seq_eq_parallel,6,4,8,
196.66 real 36.23 user 46.28 sys
seq_eq_parallel,6,5,2,
2.60 real 1.04 user 0.16 sys
seq_eq_parallel,6,5,3,
15.11 real 4.98 user 1.93 sys
seq_eq_parallel,6,5,4,
76.82 real 18.34 user 15.81 sys
seq_eq_parallel,7,3,2,
0.52 real 0.21 user 0.07 sys
seq_eq_parallel,7,3,3,
1.12 real 0.46 user 0.11 sys
seq_eq_parallel,7,3,4,
1.97 real 0.87 user 0.14 sys
seq_eq_parallel,7,3,5,
3.74 real 1.45 user 0.23 sys
seq_eq_parallel,7,3,6,
4.36 real 2.24 user 0.31 sys
seq_eq_parallel,7,3,7,
6.82 real 3.38 user 0.53 sys
seq_eq_parallel,7,3,8,
10.21 real 4.93 user 0.93 sys
seq_eq_parallel,7,4,2,
2.00 real 0.75 user 0.14 sys
seq_eq_parallel,7,4,3,
4.59 real 2.15 user 0.34 sys
seq_eq_parallel,7,4,4,
13.71 real 5.35 user 1.20 sys
seq_eq_parallel,7,4,5,
37.15 real 11.78 user 4.54 sys
seq_eq_parallel,7,4,6,
107.50 real 25.80 user 21.47 sys
seq_eq_parallel,7,4,7,
319.25 real 55.45 user 79.14 sys
seq_eq_parallel,8,3,2,
0.94 real 0.42 user 0.10 sys
seq_eq_parallel,8,3,3,
2.75 real 1.01 user 0.18 sys
seq_eq_parallel,8,3,4,
3.50 real 1.84 user 0.24 sys
seq_eq_parallel,8,3,5,
6.42 real 3.23 user 0.46 sys
seq_eq_parallel,8,3,6,
10.36 real 5.18 user 0.87 sys
seq_eq_parallel,8,3,7,
19.11 real 8.07 user 1.93 sys
seq_eq_parallel,8,3,8,
39.00 real 12.05 user 4.40 sys
seq_eq_parallel,8,4,2,
2.94 real 1.46 user 0.16 sys
seq_eq_parallel,8,4,3,
11.56 real 5.04 user 0.81 sys
seq_eq_parallel,8,4,4,
42.06 real 13.24 user 6.15 sys
seq_eq_parallel,8,4,5,
162.17 real 34.75 user 32.92 sys
seq_eq_parallel,2,3,9,
0.20 real 0.11 user 0.02 sys
seq_eq_parallel,2,3,10,
0.28 real 0.15 user 0.03 sys
seq_eq_parallel,2,4,9,
1.32 real 1.18 user 0.08 sys
seq_eq_parallel,2,4,10,
1.98 real 1.73 user 0.10 sys
seq_eq_parallel,2,5,9,
16.92 real 15.89 user 0.83 sys
seq_eq_parallel,2,5,10,
29.69 real 27.98 user 1.45 sys
seq_eq_parallel,2,6,9,
seq_eq_parallel,2,6,10,
seq_eq_parallel,2,7,6,
seq_eq_parallel,2,7,7,
seq_eq_parallel,2,7,8,
seq_eq_parallel,2,7,9,
seq_eq_parallel,2,7,10,
seq_eq_parallel,2,8,4,
seq_eq_parallel,2,8,5,
seq_eq_parallel,2,8,6,
seq_eq_parallel,2,8,7,
seq_eq_parallel,2,8,8,
seq_eq_parallel,2,9,2,
7.57 real 6.98 user 0.43 sys
seq_eq_parallel,2,8,9,
seq_eq_parallel,2,8,10,
seq_eq_parallel,2,9,3,
seq_eq_parallel,2,9,4,
seq_eq_parallel,2,9,5,
seq_eq_parallel,2,9,6,
seq_eq_parallel,2,9,7,
seq_eq_parallel,2,9,8,
seq_eq_parallel,2,9,9,
seq_eq_parallel,2,10,2,
31.42 real 27.77 user 2.97 sys
seq_eq_parallel,2,9,10,
seq_eq_parallel,2,10,3,
seq_eq_parallel,2,10,4,
seq_eq_parallel,2,10,5,
seq_eq_parallel,2,10,6,
seq_eq_parallel,2,10,7,
seq_eq_parallel,2,10,8,
seq_eq_parallel,3,3,9,
0.56 real 0.29 user 0.07 sys
seq_eq_parallel,3,3,10,
0.58 real 0.36 user 0.07 sys
seq_eq_parallel,3,4,9,
4.93 real 4.30 user 0.40 sys
seq_eq_parallel,3,4,10,
8.09 real 6.76 user 0.69 sys
seq_eq_parallel,2,10,9,
seq_eq_parallel,2,10,10,
seq_eq_parallel,3,5,8,
37.85 real 34.34 user 2.55 sys
seq_eq_parallel,3,6,2,
0.72 real 0.51 user 0.05 sys
seq_eq_parallel,3,6,3,
3.10 real 2.77 user 0.16 sys
seq_eq_parallel,3,6,4,
11.23 real 10.45 user 0.61 sys
seq_eq_parallel,3,6,5,
242.86 real 57.49 user 118.97 sys
seq_eq_parallel,3,5,9,
seq_eq_parallel,3,5,10,
seq_eq_parallel,3,6,6,
seq_eq_parallel,3,6,7,
seq_eq_parallel,3,7,2,
2.46 real 1.94 user 0.13 sys
seq_eq_parallel,3,7,3,
17.64 real 15.46 user 0.99 sys
seq_eq_parallel,3,6,8,
seq_eq_parallel,3,6,9,
seq_eq_parallel,3,6,10,
seq_eq_parallel,3,7,4,
seq_eq_parallel,3,7,5,
seq_eq_parallel,3,7,6,
seq_eq_parallel,3,7,7,
seq_eq_parallel,3,7,8,
seq_eq_parallel,3,7,9,
seq_eq_parallel,3,8,2,
8.11 real 7.29 user 0.40 sys
seq_eq_parallel,3,7,10,
seq_eq_parallel,3,8,3,
seq_eq_parallel,3,8,4,
seq_eq_parallel,3,8,5,
seq_eq_parallel,3,8,8,
seq_eq_parallel,3,8,7,
seq_eq_parallel,3,8,6,
seq_eq_parallel,3,8,9,
seq_eq_parallel,3,9,2,
50.58 real 33.19 user 12.54 sys
seq_eq_parallel,3,9,3,
seq_eq_parallel,3,8,10,
seq_eq_parallel,3,9,4,
seq_eq_parallel,3,9,5,
seq_eq_parallel,3,9,6,
seq_eq_parallel,3,9,7,
seq_eq_parallel,3,9,8,
seq_eq_parallel,3,9,9,
seq_eq_parallel,3,9,10,
seq_eq_parallel,3,10,2,
seq_eq_parallel,3,10,3,
seq_eq_parallel,3,10,4,
seq_eq_parallel,3,10,6,
seq_eq_parallel,3,10,5,
seq_eq_parallel,3,10,7,
seq_eq_parallel,4,3,9,
1.23 real 0.50 user 0.06 sys
seq_eq_parallel,4,3,10,
0.95 real 0.66 user 0.07 sys
seq_eq_parallel,4,4,9,
11.67 real 10.72 user 0.69 sys
seq_eq_parallel,4,4,10,
24.13 real 19.75 user 2.89 sys
seq_eq_parallel,3,10,8,
seq_eq_parallel,3,10,10,
seq_eq_parallel,3,10,9,
seq_eq_parallel,4,5,7,
seq_eq_parallel,4,6,2,
2.80 real 1.66 user 0.17 sys
seq_eq_parallel,4,5,8,
seq_eq_parallel,4,6,3,
9.13 real 8.16 user 0.55 sys
seq_eq_parallel,4,6,4,
100.94 real 45.36 user 41.80 sys
seq_eq_parallel,4,5,10,
seq_eq_parallel,4,5,9,
seq_eq_parallel,4,6,5,
seq_eq_parallel,4,6,6,
seq_eq_parallel,4,6,8,
seq_eq_parallel,4,6,7,
seq_eq_parallel,4,7,2,
7.24 real 5.44 user 0.46 sys
seq_eq_parallel,4,6,9,
seq_eq_parallel,4,6,10,
seq_eq_parallel,4,7,3,
177.33 real 66.30 user 80.28 sys
seq_eq_parallel,4,7,4,
seq_eq_parallel,4,7,5,
seq_eq_parallel,4,7,6,
seq_eq_parallel,4,7,7,
seq_eq_parallel,4,8,2,
66.60 real 36.81 user 22.82 sys
seq_eq_parallel,4,7,8,
seq_eq_parallel,4,7,9,
seq_eq_parallel,4,7,10,
seq_eq_parallel,4,8,3,
seq_eq_parallel,4,8,4,
seq_eq_parallel,4,8,5,
seq_eq_parallel,4,8,6,
seq_eq_parallel,4,8,7,
seq_eq_parallel,4,8,8,
seq_eq_parallel,4,8,9,
seq_eq_parallel,4,8,10,
seq_eq_parallel,4,9,2,
seq_eq_parallel,4,9,3,
seq_eq_parallel,4,9,4,
seq_eq_parallel,4,9,5,
seq_eq_parallel,4,9,6,
seq_eq_parallel,4,9,7,
seq_eq_parallel,4,9,8,
seq_eq_parallel,4,9,9,
seq_eq_parallel,4,9,10,
seq_eq_parallel,4,10,2,
seq_eq_parallel,4,10,3,
seq_eq_parallel,4,10,4,
seq_eq_parallel,4,10,5,
seq_eq_parallel,4,10,6,
seq_eq_parallel,4,10,7,
seq_eq_parallel,5,3,9,
1.76 real 1.01 user 0.12 sys
seq_eq_parallel,5,3,10,
1.78 real 1.38 user 0.16 sys
seq_eq_parallel,5,4,9,
21.28 real 17.52 user 2.62 sys
seq_eq_parallel,5,4,10,
42.65 real 28.30 user 10.35 sys
seq_eq_parallel,4,10,8,
seq_eq_parallel,5,5,5,
114.98 real 52.80 user 46.92 sys
seq_eq_parallel,4,10,9,
seq_eq_parallel,4,10,10,
seq_eq_parallel,5,5,6,
seq_eq_parallel,5,5,7,
seq_eq_parallel,5,5,8,
seq_eq_parallel,5,6,2,
5.60 real 4.26 user 0.35 sys
seq_eq_parallel,5,6,3,
45.42 real 31.82 user 10.75 sys
seq_eq_parallel,5,5,9,
seq_eq_parallel,5,5,10,
seq_eq_parallel,5,6,4,
seq_eq_parallel,5,6,5,
seq_eq_parallel,5,6,6,
seq_eq_parallel,5,6,7,
seq_eq_parallel,5,7,2,
34.61 real 23.38 user 8.15 sys
seq_eq_parallel,5,6,8,
seq_eq_parallel,5,6,9,
seq_eq_parallel,5,6,10,
seq_eq_parallel,5,7,3,
seq_eq_parallel,5,7,4,
seq_eq_parallel,5,7,5,
seq_eq_parallel,5,7,6,
seq_eq_parallel,5,7,7,
seq_eq_parallel,5,7,8,
seq_eq_parallel,5,7,9,
seq_eq_parallel,5,7,10,
seq_eq_parallel,5,8,2,
seq_eq_parallel,5,8,3,
seq_eq_parallel,5,8,4,
seq_eq_parallel,5,8,5,
seq_eq_parallel,5,8,6,
seq_eq_parallel,5,8,7,
seq_eq_parallel,5,8,8,
seq_eq_parallel,5,8,9,
seq_eq_parallel,5,8,10,
seq_eq_parallel,5,9,2,
seq_eq_parallel,5,9,3,
seq_eq_parallel,5,9,4,
seq_eq_parallel,5,9,5,
seq_eq_parallel,5,9,6,
seq_eq_parallel,5,9,7,
seq_eq_parallel,5,9,8,
seq_eq_parallel,5,9,9,
seq_eq_parallel,5,9,10,
seq_eq_parallel,5,10,2,
seq_eq_parallel,5,10,3,
seq_eq_parallel,5,10,4,
seq_eq_parallel,5,10,5,
seq_eq_parallel,5,10,6,
seq_eq_parallel,5,10,7,
seq_eq_parallel,5,10,8,
seq_eq_parallel,5,10,9,
seq_eq_parallel,5,10,10,
seq_eq_parallel,6,3,9,
3.08 real 2.29 user 0.12 sys
seq_eq_parallel,6,3,10,
4.39 real 3.17 user 0.16 sys
seq_eq_parallel,6,5,5,
50.09 real 35.80 user 9.80 sys
seq_eq_parallel,6,6,2,
18.23 real 15.13 user 2.15 sys
seq_eq_parallel,6,5,6,
seq_eq_parallel,6,5,8,
seq_eq_parallel,6,5,7,
seq_eq_parallel,6,6,3,
seq_eq_parallel,6,6,6,
seq_eq_parallel,6,6,5,
seq_eq_parallel,6,6,4,
seq_eq_parallel,6,6,7,
seq_eq_parallel,6,6,8,
seq_eq_parallel,6,7,3,
seq_eq_parallel,6,7,2,
seq_eq_parallel,6,7,4,
seq_eq_parallel,6,7,5,
seq_eq_parallel,6,7,6,
seq_eq_parallel,6,7,7,
seq_eq_parallel,6,7,8,
seq_eq_parallel,6,8,3,
seq_eq_parallel,6,8,2,
seq_eq_parallel,6,8,4,
seq_eq_parallel,6,8,5,
seq_eq_parallel,7,4,8,
195.19 real 79.06 user 82.82 sys
seq_eq_parallel,7,5,2,
3.28 real 2.54 user 0.27 sys
seq_eq_parallel,7,5,3,
16.06 real 12.16 user 2.50 sys
seq_eq_parallel,6,8,6,
seq_eq_parallel,6,8,8,
seq_eq_parallel,6,8,7,
seq_eq_parallel,7,5,4,
34.64 real 29.88 user 3.19 sys
seq_eq_parallel,7,5,7,
seq_eq_parallel,7,5,6,
seq_eq_parallel,7,5,5,
seq_eq_parallel,7,6,2,
9.38 real 8.07 user 0.45 sys
seq_eq_parallel,7,5,8,
seq_eq_parallel,7,5,9,
seq_eq_parallel,7,5,10,
seq_eq_parallel,7,6,3,
68.59 real 47.57 user 14.02 sys
seq_eq_parallel,7,6,4,
seq_eq_parallel,7,6,5,
seq_eq_parallel,7,6,6,
seq_eq_parallel,7,6,7,
seq_eq_parallel,7,6,8,
seq_eq_parallel,7,6,9,
seq_eq_parallel,7,6,10,
seq_eq_parallel,7,7,2,
seq_eq_parallel,7,7,3,
seq_eq_parallel,7,7,4,
seq_eq_parallel,7,7,5,
seq_eq_parallel,7,7,6,
seq_eq_parallel,7,7,7,
seq_eq_parallel,7,7,8,
seq_eq_parallel,7,7,9,
seq_eq_parallel,7,7,10,
seq_eq_parallel,7,8,2,
seq_eq_parallel,7,8,3,
seq_eq_parallel,7,8,4,
seq_eq_parallel,7,8,5,
seq_eq_parallel,7,8,6,
seq_eq_parallel,7,8,7,
seq_eq_parallel,7,8,8,
seq_eq_parallel,7,8,9,
seq_eq_parallel,7,8,10,
seq_eq_parallel,6,4,9,
42.09 real 31.93 user 5.93 sys
seq_eq_parallel,6,4,10,
133.69 real 60.03 user 50.07 sys
seq_eq_parallel,6,5,9,
seq_eq_parallel,6,5,10,
seq_eq_parallel,6,6,9,
seq_eq_parallel,6,6,10,
seq_eq_parallel,6,7,9,
seq_eq_parallel,6,7,10,
seq_eq_parallel,7,3,9,
6.60 real 5.77 user 0.42 sys
seq_eq_parallel,7,3,10,
9.24 real 8.05 user 0.59 sys
seq_eq_parallel,6,8,9,
seq_eq_parallel,8,3,9,
19.05 real 15.69 user 2.10 sys
seq_eq_parallel,8,3,10,
27.61 real 22.59 user 3.72 sys
seq_eq_parallel,6,8,10,
seq_eq_parallel,8,4,6,
84.82 real 55.03 user 23.06 sys
seq_eq_parallel,7,4,9,
seq_eq_parallel,7,4,10,
seq_eq_parallel,8,4,7,
291.05 real 109.46 user 122.72 sys
seq_eq_parallel,8,5,2,
6.25 real 5.35 user 0.42 sys
seq_eq_parallel,8,5,3,
35.64 real 27.24 user 6.16 sys
seq_eq_parallel,8,4,8,
seq_eq_parallel,8,4,9,
seq_eq_parallel,8,4,10,
seq_eq_parallel,8,5,4,
231.45 real 96.33 user 93.39 sys
seq_eq_parallel,8,5,5,
seq_eq_parallel,8,5,6,
seq_eq_parallel,8,5,7,
seq_eq_parallel,8,6,2,
22.50 real 19.67 user 2.12 sys
seq_eq_parallel,8,5,8,
seq_eq_parallel,8,5,9,
seq_eq_parallel,8,5,10,
seq_eq_parallel,8,6,3,
seq_eq_parallel,8,6,4,
seq_eq_parallel,8,6,5,
seq_eq_parallel,8,6,6,
seq_eq_parallel,8,6,7,
seq_eq_parallel,8,6,8,
seq_eq_parallel,8,6,9,
seq_eq_parallel,8,7,2,
244.41 real 101.09 user 94.28 sys
seq_eq_parallel,8,6,10,
seq_eq_parallel,8,7,3,
seq_eq_parallel,8,7,4,
seq_eq_parallel,8,7,5,
seq_eq_parallel,8,7,6,
seq_eq_parallel,8,7,7,
seq_eq_parallel,8,7,8,
seq_eq_parallel,8,7,9,
seq_eq_parallel,8,7,10,
seq_eq_parallel,8,8,2,
seq_eq_parallel,8,8,3,
seq_eq_parallel,8,8,4,
seq_eq_parallel,8,8,5,
seq_eq_parallel,8,8,6,
seq_eq_parallel,8,8,7,
seq_eq_parallel,8,8,8,
seq_eq_parallel,8,8,9,
seq_eq_parallel,8,8,10,
seq_eq_parallel,6,9,2,
seq_eq_parallel,6,9,5,
seq_eq_parallel,6,9,3,
seq_eq_parallel,6,9,4,
seq_eq_parallel,6,9,6,
seq_eq_parallel,6,9,7,
seq_eq_parallel,6,9,9,
seq_eq_parallel,6,9,8,
seq_eq_parallel,6,9,10,
seq_eq_parallel,6,10,3,
seq_eq_parallel,6,10,2,
seq_eq_parallel,6,10,4,
seq_eq_parallel,6,10,5,
seq_eq_parallel,6,10,8,
seq_eq_parallel,6,10,7,
seq_eq_parallel,6,10,6,
seq_eq_parallel,6,10,9,
seq_eq_parallel,6,10,10,
seq_eq_parallel,7,9,3,
seq_eq_parallel,7,9,2,
seq_eq_parallel,7,9,4,
seq_eq_parallel,7,9,5,
seq_eq_parallel,7,9,6,
seq_eq_parallel,7,9,7,
seq_eq_parallel,7,9,10,
seq_eq_parallel,7,9,8,
seq_eq_parallel,7,9,9,
seq_eq_parallel,7,10,2,
seq_eq_parallel,7,10,3,
seq_eq_parallel,7,10,4,
seq_eq_parallel,7,10,5,
seq_eq_parallel,7,10,6,
seq_eq_parallel,7,10,7,
seq_eq_parallel,7,10,8,
seq_eq_parallel,7,10,9,
seq_eq_parallel,7,10,10,
seq_eq_parallel,8,9,2,
seq_eq_parallel,8,9,3,
seq_eq_parallel,8,9,4,
seq_eq_parallel,8,9,5,
seq_eq_parallel,8,9,6,
seq_eq_parallel,8,9,7,
seq_eq_parallel,8,9,8,
seq_eq_parallel,8,9,9,
seq_eq_parallel,8,9,10,
seq_eq_parallel,8,10,2,
seq_eq_parallel,8,10,3,
seq_eq_parallel,8,10,4,
seq_eq_parallel,8,10,5,
seq_eq_parallel,8,10,6,
seq_eq_parallel,8,10,7,
seq_eq_parallel,8,10,8,
seq_eq_parallel,8,10,9,
seq_eq_parallel,8,10,10,
seq_eq_parallel,9,10,2,
seq_eq_parallel,9,10,3,
seq_eq_parallel,9,10,4,
seq_eq_parallel,9,10,5,
seq_eq_parallel,9,10,6,
seq_eq_parallel,9,10,7,
seq_eq_parallel,9,10,8,
seq_eq_parallel,9,10,9,
seq_eq_parallel,9,10,10,
seq_eq_parallel,10,10,2,
seq_eq_parallel,10,10,3,
seq_eq_parallel,10,10,4,
seq_eq_parallel,10,10,5,
seq_eq_parallel,10,10,6,
seq_eq_parallel,10,10,7,
seq_eq_parallel,10,10,8,
seq_eq_parallel,10,10,9,
seq_eq_parallel,10,10,10,
seq_eq_parallel,9,9,2,
seq_eq_parallel,9,9,3,
seq_eq_parallel,9,9,4,
seq_eq_parallel,9,9,5,
seq_eq_parallel,9,9,6,
seq_eq_parallel,9,9,7,
seq_eq_parallel,9,9,8,
seq_eq_parallel,9,9,9,
seq_eq_parallel,9,9,10,
seq_eq_parallel,10,9,2,
seq_eq_parallel,10,9,3,
seq_eq_parallel,10,9,4,
seq_eq_parallel,10,9,5,
seq_eq_parallel,10,9,6,
seq_eq_parallel,10,9,7,
seq_eq_parallel,10,9,8,
seq_eq_parallel,10,9,9,
seq_eq_parallel,10,9,10,
seq_eq_parallel,9,3,2,
1.42 real 0.70 user 0.04 sys
seq_eq_parallel,9,3,3,
2.01 real 1.64 user 0.07 sys
seq_eq_parallel,9,3,4,
3.79 real 3.12 user 0.11 sys
seq_eq_parallel,9,3,5,
6.03 real 5.42 user 0.18 sys
seq_eq_parallel,9,3,6,
9.04 real 8.60 user 0.27 sys
seq_eq_parallel,9,3,7,
13.41 real 12.85 user 0.40 sys
seq_eq_parallel,9,4,2,
2.78 real 2.52 user 0.10 sys
seq_eq_parallel,9,3,8,
19.16 real 18.40 user 0.59 sys
seq_eq_parallel,9,4,3,
8.63 real 8.19 user 0.28 sys
seq_eq_parallel,9,3,9,
26.35 real 25.34 user 0.84 sys
seq_eq_parallel,9,4,4,
21.30 real 20.38 user 0.73 sys
seq_eq_parallel,9,3,10,
36.70 real 35.28 user 1.22 sys
seq_eq_parallel,9,4,5,
59.38 real 47.74 user 8.21 sys
seq_eq_parallel,9,4,6,
seq_eq_parallel,9,4,7,
seq_eq_parallel,9,4,8,
seq_eq_parallel,9,5,2,
12.63 real 11.65 user 0.63 sys
seq_eq_parallel,9,4,9,
seq_eq_parallel,9,5,3,
72.14 real 54.80 user 13.08 sys
seq_eq_parallel,9,4,10,
seq_eq_parallel,9,5,4,
seq_eq_parallel,9,5,5,
seq_eq_parallel,9,5,6,
seq_eq_parallel,9,5,7,
seq_eq_parallel,9,5,8,
seq_eq_parallel,9,5,9,
seq_eq_parallel,9,6,2,
75.20 real 53.30 user 15.55 sys
seq_eq_parallel,9,5,10,
seq_eq_parallel,9,6,3,
seq_eq_parallel,9,6,4,
seq_eq_parallel,9,6,5,
seq_eq_parallel,9,6,6,
seq_eq_parallel,9,6,7,
seq_eq_parallel,9,6,8,
seq_eq_parallel,9,6,9,
seq_eq_parallel,9,6,10,
seq_eq_parallel,9,7,2,
seq_eq_parallel,9,7,3,
seq_eq_parallel,9,7,4,
seq_eq_parallel,9,7,5,
seq_eq_parallel,9,7,6,
seq_eq_parallel,9,7,7,
seq_eq_parallel,9,7,8,
seq_eq_parallel,9,7,9,
seq_eq_parallel,9,7,10,
seq_eq_parallel,9,8,2,
seq_eq_parallel,9,8,3,
seq_eq_parallel,9,8,4,
seq_eq_parallel,9,8,5,
seq_eq_parallel,9,8,6,
seq_eq_parallel,9,8,7,
seq_eq_parallel,9,8,8,
seq_eq_parallel,10,3,2,
2.63 real 2.24 user 0.17 sys
seq_eq_parallel,10,3,3,
5.09 real 4.62 user 0.25 sys
seq_eq_parallel,10,3,4,
9.46 real 8.77 user 0.44 sys
seq_eq_parallel,10,3,5,
16.24 real 15.01 user 0.84 sys
seq_eq_parallel,10,3,6,
31.09 real 26.69 user 2.88 sys
seq_eq_parallel,10,3,7,
61.77 real 46.07 user 10.02 sys
seq_eq_parallel,10,3,8,
104.42 real 68.87 user 26.00 sys
seq_eq_parallel,9,8,9,
seq_eq_parallel,10,4,2,
8.92 real 7.98 user 0.58 sys
seq_eq_parallel,9,8,10,
seq_eq_parallel,10,3,9,
189.16 real 98.49 user 69.19 sys
seq_eq_parallel,10,4,3,
27.48 real 24.39 user 2.34 sys
seq_eq_parallel,10,4,4,
100.18 real 62.87 user 27.12 sys
seq_eq_parallel,10,3,10,
seq_eq_parallel,10,4,5,
seq_eq_parallel,10,4,6,
seq_eq_parallel,10,4,7,
seq_eq_parallel,10,5,2,
45.44 real 33.86 user 8.22 sys
seq_eq_parallel,10,4,8,
seq_eq_parallel,10,4,9,
seq_eq_parallel,10,4,10,
seq_eq_parallel,10,5,3,
seq_eq_parallel,10,5,4,
seq_eq_parallel,10,5,5,
seq_eq_parallel,10,5,6,
seq_eq_parallel,10,5,7,
seq_eq_parallel,10,5,8,
seq_eq_parallel,10,5,9,
seq_eq_parallel,10,5,10,
seq_eq_parallel,10,6,2,
seq_eq_parallel,10,6,3,
seq_eq_parallel,10,6,4,
seq_eq_parallel,10,6,5,
seq_eq_parallel,10,6,6,
seq_eq_parallel,10,6,7,
seq_eq_parallel,10,6,8,
seq_eq_parallel,10,6,9,
seq_eq_parallel,10,6,10,
seq_eq_parallel,10,7,2,
seq_eq_parallel,10,7,3,
seq_eq_parallel,10,7,4,
seq_eq_parallel,10,7,5,
seq_eq_parallel,10,7,6,
seq_eq_parallel,10,7,7,
seq_eq_parallel,10,7,8,
seq_eq_parallel,10,7,9,
seq_eq_parallel,10,7,10,
seq_eq_parallel,10,8,2,
seq_eq_parallel,10,8,3,
seq_eq_parallel,10,8,4,
seq_eq_parallel,10,8,5,
seq_eq_parallel,10,8,6,
seq_eq_parallel,10,8,7,
seq_eq_parallel,10,8,8,
seq_eq_parallel,10,8,9,
seq_eq_parallel,10,8,10,

66
ReversalModel/outputs/trace_seq_eq_parallel_10_3_10.txt Normal file
View File

@ -0,0 +1,66 @@
pan: ltl formula seq_eq_parallel
Depth= 349 States= 1e+06 Transitions= 2.12e+06 Memory= 419.940 t= 4.07 R= 2e+05
Depth= 349 States= 2e+06 Transitions= 4.25e+06 Memory= 711.249 t= 8.61 R= 2e+05
Depth= 349 States= 3e+06 Transitions= 6.38e+06 Memory= 1002.558 t= 13.4 R= 2e+05
Depth= 349 States= 4e+06 Transitions= 8.5e+06 Memory= 1293.964 t= 18.4 R= 2e+05
Depth= 349 States= 5e+06 Transitions= 1.06e+07 Memory= 1585.272 t= 24.2 R= 2e+05
Depth= 349 States= 6e+06 Transitions= 1.27e+07 Memory= 1876.581 t= 30.8 R= 2e+05
Depth= 349 States= 7e+06 Transitions= 1.49e+07 Memory= 2167.987 t= 38.9 R= 2e+05
Depth= 349 States= 8e+06 Transitions= 1.7e+07 Memory= 2459.296 t= 48.3 R= 2e+05
Depth= 349 States= 9e+06 Transitions= 1.91e+07 Memory= 2750.605 t= 58.5 R= 2e+05
Depth= 349 States= 1e+07 Transitions= 2.12e+07 Memory= 3042.011 t= 70.2 R= 1e+05
Depth= 349 States= 1.1e+07 Transitions= 2.34e+07 Memory= 3333.319 t= 83.3 R= 1e+05
Depth= 349 States= 1.2e+07 Transitions= 2.55e+07 Memory= 3624.530 t= 95.7 R= 1e+05
Depth= 349 States= 1.3e+07 Transitions= 2.76e+07 Memory= 3915.839 t= 104 R= 1e+05
Depth= 349 States= 1.4e+07 Transitions= 2.98e+07 Memory= 4207.245 t= 114 R= 1e+05
Depth= 349 States= 1.5e+07 Transitions= 3.19e+07 Memory= 4498.554 t= 125 R= 1e+05
Depth= 349 States= 1.6e+07 Transitions= 3.4e+07 Memory= 4789.862 t= 132 R= 1e+05
Depth= 349 States= 1.7e+07 Transitions= 3.61e+07 Memory= 5081.269 t= 136 R= 1e+05
Depth= 349 States= 1.8e+07 Transitions= 3.82e+07 Memory= 5372.577 t= 140 R= 1e+05
Depth= 349 States= 1.9e+07 Transitions= 4.04e+07 Memory= 5663.983 t= 144 R= 1e+05
Depth= 349 States= 2e+07 Transitions= 4.25e+07 Memory= 5955.292 t= 148 R= 1e+05
Depth= 349 States= 2.1e+07 Transitions= 4.46e+07 Memory= 6246.601 t= 153 R= 1e+05
Depth= 349 States= 2.2e+07 Transitions= 4.67e+07 Memory= 6537.909 t= 167 R= 1e+05
Depth= 349 States= 2.3e+07 Transitions= 4.89e+07 Memory= 6829.218 t= 191 R= 1e+05
Depth= 349 States= 2.4e+07 Transitions= 5.1e+07 Memory= 7120.526 t= 225 R= 1e+05
Depth= 349 States= 2.5e+07 Transitions= 5.31e+07 Memory= 7411.835 t= 255 R= 1e+05
Depth= 349 States= 2.6e+07 Transitions= 5.53e+07 Memory= 7703.241 t= 296 R= 9e+04
(Spin Version 6.5.2 -- 6 December 2019)
+ Partial Order Reduction
Full statespace search for:
never claim + (seq_eq_parallel)
assertion violations + (if within scope of claim)
acceptance cycles + (fairness disabled)
invalid end states - (disabled by never claim)
State-vector 340 byte, depth reached 349, errors: 0
26050864 states, stored
29307289 states, matched
55358153 transitions (= stored+matched)
0 atomic steps
hash conflicts: 16916426 (resolved)
Stats on memory usage (in Megabytes):
9142.607 equivalent memory usage for states (stored*(State-vector + overhead))
7595.899 actual memory usage for states (compression: 83.08%)
state-vector as stored = 278 byte + 28 byte overhead
128.000 memory used for hash table (-w24)
0.534 memory used for DFS stack (-m10000)
6.350 memory lost to fragmentation
7718.085 total actual memory usage
unreached in proctype ThreadedReverser
(0 of 15 states)
unreached in init
reversal_seq_eq_parallel_10_3_10.pml:87, state 79, "seq_eq_to_parallel = 0"
reversal_seq_eq_parallel_10_3_10.pml:91, state 89, "-end-"
(2 of 89 states)
unreached in claim seq_eq_parallel
_spin_nvr.tmp:8, state 10, "-end-"
(1 of 10 states)
pan: elapsed time 299 seconds
pan: rate 87255.038 states/second

39
ReversalModel/outputs/trace_seq_eq_parallel_10_3_2.txt Normal file
View File

@ -0,0 +1,39 @@
pan: ltl formula seq_eq_parallel
(Spin Version 6.5.2 -- 6 December 2019)
+ Partial Order Reduction
Full statespace search for:
never claim + (seq_eq_parallel)
assertion violations + (if within scope of claim)
acceptance cycles + (fairness disabled)
invalid end states - (disabled by never claim)
State-vector 340 byte, depth reached 349, errors: 0
528496 states, stored
594513 states, matched
1123009 transitions (= stored+matched)
0 atomic steps
hash conflicts: 4798 (resolved)
Stats on memory usage (in Megabytes):
185.477 equivalent memory usage for states (stored*(State-vector + overhead))
154.313 actual memory usage for states (compression: 83.20%)
state-vector as stored = 278 byte + 28 byte overhead
128.000 memory used for hash table (-w24)
0.534 memory used for DFS stack (-m10000)
282.636 total actual memory usage
unreached in proctype ThreadedReverser
(0 of 15 states)
unreached in init
reversal_seq_eq_parallel_10_3_2.pml:87, state 71, "seq_eq_to_parallel = 0"
reversal_seq_eq_parallel_10_3_2.pml:91, state 81, "-end-"
(2 of 81 states)
unreached in claim seq_eq_parallel
_spin_nvr.tmp:8, state 10, "-end-"
(1 of 10 states)
pan: elapsed time 2.35 seconds
pan: rate 224891.91 states/second

40
ReversalModel/outputs/trace_seq_eq_parallel_10_3_3.txt Normal file
View File

@ -0,0 +1,40 @@
pan: ltl formula seq_eq_parallel
Depth= 349 States= 1e+06 Transitions= 2.12e+06 Memory= 419.940 t= 3.83 R= 3e+05
(Spin Version 6.5.2 -- 6 December 2019)
+ Partial Order Reduction
Full statespace search for:
never claim + (seq_eq_parallel)
assertion violations + (if within scope of claim)
acceptance cycles + (fairness disabled)
invalid end states - (disabled by never claim)
State-vector 340 byte, depth reached 349, errors: 0
1252692 states, stored
1409216 states, matched
2661908 transitions (= stored+matched)
0 atomic steps
hash conflicts: 28480 (resolved)
Stats on memory usage (in Megabytes):
439.635 equivalent memory usage for states (stored*(State-vector + overhead))
365.421 actual memory usage for states (compression: 83.12%)
state-vector as stored = 278 byte + 28 byte overhead
128.000 memory used for hash table (-w24)
0.534 memory used for DFS stack (-m10000)
493.573 total actual memory usage
unreached in proctype ThreadedReverser
(0 of 15 states)
unreached in init
reversal_seq_eq_parallel_10_3_3.pml:87, state 72, "seq_eq_to_parallel = 0"
reversal_seq_eq_parallel_10_3_3.pml:91, state 82, "-end-"
(2 of 82 states)
unreached in claim seq_eq_parallel
_spin_nvr.tmp:8, state 10, "-end-"
(1 of 10 states)
pan: elapsed time 4.78 seconds
pan: rate 262069.46 states/second

41
ReversalModel/outputs/trace_seq_eq_parallel_10_3_4.txt Normal file
View File

@ -0,0 +1,41 @@
pan: ltl formula seq_eq_parallel
Depth= 349 States= 1e+06 Transitions= 2.12e+06 Memory= 419.940 t= 3.78 R= 3e+05
Depth= 349 States= 2e+06 Transitions= 4.25e+06 Memory= 711.249 t= 7.5 R= 3e+05
(Spin Version 6.5.2 -- 6 December 2019)
+ Partial Order Reduction
Full statespace search for:
never claim + (seq_eq_parallel)
assertion violations + (if within scope of claim)
acceptance cycles + (fairness disabled)
invalid end states - (disabled by never claim)
State-vector 340 byte, depth reached 349, errors: 0
2446624 states, stored
2752375 states, matched
5198999 transitions (= stored+matched)
0 atomic steps
hash conflicts: 113220 (resolved)
Stats on memory usage (in Megabytes):
858.648 equivalent memory usage for states (stored*(State-vector + overhead))
713.558 actual memory usage for states (compression: 83.10%)
state-vector as stored = 278 byte + 28 byte overhead
128.000 memory used for hash table (-w24)
0.534 memory used for DFS stack (-m10000)
841.425 total actual memory usage
unreached in proctype ThreadedReverser
(0 of 15 states)
unreached in init
reversal_seq_eq_parallel_10_3_4.pml:87, state 73, "seq_eq_to_parallel = 0"
reversal_seq_eq_parallel_10_3_4.pml:91, state 83, "-end-"
(2 of 83 states)
unreached in claim seq_eq_parallel
_spin_nvr.tmp:8, state 10, "-end-"
(1 of 10 states)
pan: elapsed time 9.15 seconds
pan: rate 267390.6 states/second

44
ReversalModel/outputs/trace_seq_eq_parallel_10_3_5.txt Normal file
View File

@ -0,0 +1,44 @@
pan: ltl formula seq_eq_parallel
Depth= 349 States= 1e+06 Transitions= 2.12e+06 Memory= 419.940 t= 3.69 R= 3e+05
Depth= 349 States= 2e+06 Transitions= 4.25e+06 Memory= 711.249 t= 7.39 R= 3e+05
Depth= 349 States= 3e+06 Transitions= 6.38e+06 Memory= 1002.558 t= 10.9 R= 3e+05
Depth= 349 States= 4e+06 Transitions= 8.5e+06 Memory= 1293.866 t= 14.8 R= 3e+05
(Spin Version 6.5.2 -- 6 December 2019)
+ Partial Order Reduction
Full statespace search for:
never claim + (seq_eq_parallel)
assertion violations + (if within scope of claim)
acceptance cycles + (fairness disabled)
invalid end states - (disabled by never claim)
State-vector 340 byte, depth reached 349, errors: 0
4227724 states, stored
4756104 states, matched
8983828 transitions (= stored+matched)
0 atomic steps
hash conflicts: 348665 (resolved)
Stats on memory usage (in Megabytes):
1483.729 equivalent memory usage for states (stored*(State-vector + overhead))
1232.930 actual memory usage for states (compression: 83.10%)
state-vector as stored = 278 byte + 28 byte overhead
128.000 memory used for hash table (-w24)
0.534 memory used for DFS stack (-m10000)
1.095 memory lost to fragmentation
1360.370 total actual memory usage
unreached in proctype ThreadedReverser
(0 of 15 states)
unreached in init
reversal_seq_eq_parallel_10_3_5.pml:87, state 74, "seq_eq_to_parallel = 0"
reversal_seq_eq_parallel_10_3_5.pml:91, state 84, "-end-"
(2 of 84 states)
unreached in claim seq_eq_parallel
_spin_nvr.tmp:8, state 10, "-end-"
(1 of 10 states)
pan: elapsed time 15.8 seconds
pan: rate 268086.49 states/second

46
ReversalModel/outputs/trace_seq_eq_parallel_10_3_6.txt Normal file
View File

@ -0,0 +1,46 @@
pan: ltl formula seq_eq_parallel
Depth= 349 States= 1e+06 Transitions= 2.12e+06 Memory= 419.940 t= 3.6 R= 3e+05
Depth= 349 States= 2e+06 Transitions= 4.25e+06 Memory= 711.249 t= 7.06 R= 3e+05
Depth= 349 States= 3e+06 Transitions= 6.38e+06 Memory= 1002.558 t= 11.3 R= 3e+05
Depth= 349 States= 4e+06 Transitions= 8.5e+06 Memory= 1293.866 t= 15.2 R= 3e+05
Depth= 349 States= 5e+06 Transitions= 1.06e+07 Memory= 1585.272 t= 20.4 R= 2e+05
Depth= 349 States= 6e+06 Transitions= 1.27e+07 Memory= 1876.581 t= 26.4 R= 2e+05
(Spin Version 6.5.2 -- 6 December 2019)
+ Partial Order Reduction
Full statespace search for:
never claim + (seq_eq_parallel)
assertion violations + (if within scope of claim)
acceptance cycles + (fairness disabled)
invalid end states - (disabled by never claim)
State-vector 340 byte, depth reached 349, errors: 0
6713424 states, stored
7552517 states, matched
14265941 transitions (= stored+matched)
0 atomic steps
hash conflicts: 917536 (resolved)
Stats on memory usage (in Megabytes):
2356.091 equivalent memory usage for states (stored*(State-vector + overhead))
1957.648 actual memory usage for states (compression: 83.09%)
state-vector as stored = 278 byte + 28 byte overhead
128.000 memory used for hash table (-w24)
0.534 memory used for DFS stack (-m10000)
1.692 memory lost to fragmentation
2084.491 total actual memory usage
unreached in proctype ThreadedReverser
(0 of 15 states)
unreached in init
reversal_seq_eq_parallel_10_3_6.pml:87, state 75, "seq_eq_to_parallel = 0"
reversal_seq_eq_parallel_10_3_6.pml:91, state 85, "-end-"
(2 of 85 states)
unreached in claim seq_eq_parallel
_spin_nvr.tmp:8, state 10, "-end-"
(1 of 10 states)
pan: elapsed time 30.5 seconds
pan: rate 219895.97 states/second

50
ReversalModel/outputs/trace_seq_eq_parallel_10_3_7.txt Normal file
View File

@ -0,0 +1,50 @@
pan: ltl formula seq_eq_parallel
Depth= 349 States= 1e+06 Transitions= 2.12e+06 Memory= 419.940 t= 3.95 R= 3e+05
Depth= 349 States= 2e+06 Transitions= 4.25e+06 Memory= 711.249 t= 8.76 R= 2e+05
Depth= 349 States= 3e+06 Transitions= 6.38e+06 Memory= 1002.558 t= 14.1 R= 2e+05
Depth= 349 States= 4e+06 Transitions= 8.5e+06 Memory= 1293.964 t= 19.2 R= 2e+05
Depth= 349 States= 5e+06 Transitions= 1.06e+07 Memory= 1585.272 t= 23.7 R= 2e+05
Depth= 349 States= 6e+06 Transitions= 1.27e+07 Memory= 1876.581 t= 29.2 R= 2e+05
Depth= 349 States= 7e+06 Transitions= 1.49e+07 Memory= 2167.890 t= 35.4 R= 2e+05
Depth= 349 States= 8e+06 Transitions= 1.7e+07 Memory= 2459.296 t= 43.2 R= 2e+05
Depth= 349 States= 9e+06 Transitions= 1.91e+07 Memory= 2750.605 t= 51.6 R= 2e+05
Depth= 349 States= 1e+07 Transitions= 2.12e+07 Memory= 3041.913 t= 60.8 R= 2e+05
(Spin Version 6.5.2 -- 6 December 2019)
+ Partial Order Reduction
Full statespace search for:
never claim + (seq_eq_parallel)
assertion violations + (if within scope of claim)
acceptance cycles + (fairness disabled)
invalid end states - (disabled by never claim)
State-vector 340 byte, depth reached 349, errors: 0
10021156 states, stored
11273728 states, matched
21294884 transitions (= stored+matched)
0 atomic steps
hash conflicts: 2133171 (resolved)
Stats on memory usage (in Megabytes):
3516.946 equivalent memory usage for states (stored*(State-vector + overhead))
2922.115 actual memory usage for states (compression: 83.09%)
state-vector as stored = 278 byte + 28 byte overhead
128.000 memory used for hash table (-w24)
0.534 memory used for DFS stack (-m10000)
2.488 memory lost to fragmentation
3048.163 total actual memory usage
unreached in proctype ThreadedReverser
(0 of 15 states)
unreached in init
reversal_seq_eq_parallel_10_3_7.pml:87, state 76, "seq_eq_to_parallel = 0"
reversal_seq_eq_parallel_10_3_7.pml:91, state 86, "-end-"
(2 of 86 states)
unreached in claim seq_eq_parallel
_spin_nvr.tmp:8, state 10, "-end-"
(1 of 10 states)
pan: elapsed time 61 seconds
pan: rate 164254.32 states/second

54
ReversalModel/outputs/trace_seq_eq_parallel_10_3_8.txt Normal file
View File

@ -0,0 +1,54 @@
pan: ltl formula seq_eq_parallel
Depth= 349 States= 1e+06 Transitions= 2.12e+06 Memory= 419.940 t= 4.29 R= 2e+05
Depth= 349 States= 2e+06 Transitions= 4.25e+06 Memory= 711.249 t= 9 R= 2e+05
Depth= 349 States= 3e+06 Transitions= 6.38e+06 Memory= 1002.558 t= 14.1 R= 2e+05
Depth= 349 States= 4e+06 Transitions= 8.5e+06 Memory= 1293.964 t= 19.8 R= 2e+05
Depth= 349 States= 5e+06 Transitions= 1.06e+07 Memory= 1585.272 t= 26.4 R= 2e+05
Depth= 349 States= 6e+06 Transitions= 1.27e+07 Memory= 1876.581 t= 33.5 R= 2e+05
Depth= 349 States= 7e+06 Transitions= 1.49e+07 Memory= 2167.987 t= 40.5 R= 2e+05
Depth= 349 States= 8e+06 Transitions= 1.7e+07 Memory= 2459.296 t= 45.6 R= 2e+05
Depth= 349 States= 9e+06 Transitions= 1.91e+07 Memory= 2750.605 t= 51.7 R= 2e+05
Depth= 349 States= 1e+07 Transitions= 2.12e+07 Memory= 3042.011 t= 58.1 R= 2e+05
Depth= 349 States= 1.1e+07 Transitions= 2.34e+07 Memory= 3333.319 t= 65.8 R= 2e+05
Depth= 349 States= 1.2e+07 Transitions= 2.55e+07 Memory= 3624.530 t= 75.2 R= 2e+05
Depth= 349 States= 1.3e+07 Transitions= 2.76e+07 Memory= 3915.839 t= 86.4 R= 2e+05
Depth= 349 States= 1.4e+07 Transitions= 2.98e+07 Memory= 4207.245 t= 99.4 R= 1e+05
(Spin Version 6.5.2 -- 6 December 2019)
+ Partial Order Reduction
Full statespace search for:
never claim + (seq_eq_parallel)
assertion violations + (if within scope of claim)
acceptance cycles + (fairness disabled)
invalid end states - (disabled by never claim)
State-vector 340 byte, depth reached 349, errors: 0
14268352 states, stored
16051851 states, matched
30320203 transitions (= stored+matched)
0 atomic steps
hash conflicts: 4569848 (resolved)
Stats on memory usage (in Megabytes):
5007.509 equivalent memory usage for states (stored*(State-vector + overhead))
4160.443 actual memory usage for states (compression: 83.08%)
state-vector as stored = 278 byte + 28 byte overhead
128.000 memory used for hash table (-w24)
0.534 memory used for DFS stack (-m10000)
3.510 memory lost to fragmentation
4285.468 total actual memory usage
unreached in proctype ThreadedReverser
(0 of 15 states)
unreached in init
reversal_seq_eq_parallel_10_3_8.pml:87, state 77, "seq_eq_to_parallel = 0"
reversal_seq_eq_parallel_10_3_8.pml:91, state 87, "-end-"
(2 of 87 states)
unreached in claim seq_eq_parallel
_spin_nvr.tmp:8, state 10, "-end-"
(1 of 10 states)
pan: elapsed time 103 seconds
pan: rate 137951.77 states/second

59
ReversalModel/outputs/trace_seq_eq_parallel_10_3_9.txt Normal file
View File

@ -0,0 +1,59 @@
pan: ltl formula seq_eq_parallel
Depth= 349 States= 1e+06 Transitions= 2.12e+06 Memory= 419.940 t= 4.01 R= 2e+05
Depth= 349 States= 2e+06 Transitions= 4.25e+06 Memory= 711.249 t= 8.66 R= 2e+05
Depth= 349 States= 3e+06 Transitions= 6.38e+06 Memory= 1002.558 t= 13.1 R= 2e+05
Depth= 349 States= 4e+06 Transitions= 8.5e+06 Memory= 1293.964 t= 17.8 R= 2e+05
Depth= 349 States= 5e+06 Transitions= 1.06e+07 Memory= 1585.272 t= 23.2 R= 2e+05
Depth= 349 States= 6e+06 Transitions= 1.27e+07 Memory= 1876.581 t= 29.2 R= 2e+05
Depth= 349 States= 7e+06 Transitions= 1.49e+07 Memory= 2167.987 t= 35.6 R= 2e+05
Depth= 349 States= 8e+06 Transitions= 1.7e+07 Memory= 2459.296 t= 43.5 R= 2e+05
Depth= 349 States= 9e+06 Transitions= 1.91e+07 Memory= 2750.605 t= 52.4 R= 2e+05
Depth= 349 States= 1e+07 Transitions= 2.12e+07 Memory= 3042.011 t= 61.8 R= 2e+05
Depth= 349 States= 1.1e+07 Transitions= 2.34e+07 Memory= 3333.319 t= 68.4 R= 2e+05
Depth= 349 States= 1.2e+07 Transitions= 2.55e+07 Memory= 3624.530 t= 76.7 R= 2e+05
Depth= 349 States= 1.3e+07 Transitions= 2.76e+07 Memory= 3915.839 t= 86.8 R= 1e+05
Depth= 349 States= 1.4e+07 Transitions= 2.98e+07 Memory= 4207.245 t= 99.3 R= 1e+05
Depth= 349 States= 1.5e+07 Transitions= 3.19e+07 Memory= 4498.554 t= 114 R= 1e+05
Depth= 349 States= 1.6e+07 Transitions= 3.4e+07 Memory= 4789.862 t= 130 R= 1e+05
Depth= 349 States= 1.7e+07 Transitions= 3.61e+07 Memory= 5081.269 t= 149 R= 1e+05
Depth= 349 States= 1.8e+07 Transitions= 3.82e+07 Memory= 5372.577 t= 163 R= 1e+05
Depth= 349 States= 1.9e+07 Transitions= 4.04e+07 Memory= 5663.886 t= 178 R= 1e+05
(Spin Version 6.5.2 -- 6 December 2019)
+ Partial Order Reduction
Full statespace search for:
never claim + (seq_eq_parallel)
assertion violations + (if within scope of claim)
acceptance cycles + (fairness disabled)
invalid end states - (disabled by never claim)
State-vector 340 byte, depth reached 349, errors: 0
19572444 states, stored
22019000 states, matched
41591444 transitions (= stored+matched)
0 atomic steps
hash conflicts: 9056739 (resolved)
Stats on memory usage (in Megabytes):
6868.991 equivalent memory usage for states (stored*(State-vector + overhead))
5706.936 actual memory usage for states (compression: 83.08%)
state-vector as stored = 278 byte + 28 byte overhead
128.000 memory used for hash table (-w24)
0.534 memory used for DFS stack (-m10000)
4.788 memory lost to fragmentation
5830.683 total actual memory usage
unreached in proctype ThreadedReverser
(0 of 15 states)
unreached in init
reversal_seq_eq_parallel_10_3_9.pml:87, state 78, "seq_eq_to_parallel = 0"
reversal_seq_eq_parallel_10_3_9.pml:91, state 88, "-end-"
(2 of 88 states)
unreached in claim seq_eq_parallel
_spin_nvr.tmp:8, state 10, "-end-"
(1 of 10 states)
pan: elapsed time 188 seconds
pan: rate 104153.07 states/second

22
ReversalModel/outputs/trace_seq_eq_parallel_10_4_10.txt Normal file
View File

@ -0,0 +1,22 @@
pan: ltl formula seq_eq_parallel
Depth= 369 States= 1e+06 Transitions= 2.13e+06 Memory= 428.827 t= 3.92 R= 3e+05
Depth= 369 States= 2e+06 Transitions= 4.25e+06 Memory= 729.120 t= 7.71 R= 3e+05
Depth= 369 States= 3e+06 Transitions= 6.37e+06 Memory= 1029.413 t= 11.8 R= 3e+05
Depth= 369 States= 4e+06 Transitions= 8.5e+06 Memory= 1329.706 t= 16.4 R= 2e+05
Depth= 369 States= 5e+06 Transitions= 1.06e+07 Memory= 1629.901 t= 20.9 R= 2e+05
Depth= 369 States= 6e+06 Transitions= 1.28e+07 Memory= 1930.194 t= 26.2 R= 2e+05
Depth= 369 States= 7e+06 Transitions= 1.49e+07 Memory= 2230.487 t= 32.2 R= 2e+05
Depth= 369 States= 8e+06 Transitions= 1.7e+07 Memory= 2530.780 t= 38.8 R= 2e+05
Depth= 369 States= 9e+06 Transitions= 1.91e+07 Memory= 2830.976 t= 46.5 R= 2e+05
Depth= 369 States= 1e+07 Transitions= 2.13e+07 Memory= 3131.269 t= 55.8 R= 2e+05
Depth= 369 States= 1.1e+07 Transitions= 2.34e+07 Memory= 3431.562 t= 66.7 R= 2e+05
Depth= 369 States= 1.2e+07 Transitions= 2.55e+07 Memory= 3731.757 t= 79.3 R= 2e+05
Depth= 369 States= 1.3e+07 Transitions= 2.76e+07 Memory= 4032.050 t= 93 R= 1e+05
Depth= 369 States= 1.4e+07 Transitions= 2.98e+07 Memory= 4332.343 t= 105 R= 1e+05
Depth= 369 States= 1.5e+07 Transitions= 3.19e+07 Memory= 4632.636 t= 120 R= 1e+05
Depth= 369 States= 1.6e+07 Transitions= 3.4e+07 Memory= 4932.831 t= 137 R= 1e+05
Depth= 369 States= 1.7e+07 Transitions= 3.61e+07 Memory= 5233.124 t= 153 R= 1e+05
Depth= 369 States= 1.8e+07 Transitions= 3.83e+07 Memory= 5533.417 t= 171 R= 1e+05
Depth= 369 States= 1.9e+07 Transitions= 4.04e+07 Memory= 5833.710 t= 190 R= 1e+05
Depth= 369 States= 2e+07 Transitions= 4.25e+07 Memory= 6133.905 t= 218 R= 9e+04
Depth= 369 States= 2.1e+07 Transitions= 4.46e+07 Memory= 6434.101 t= 373 R= 6e+04

40
ReversalModel/outputs/trace_seq_eq_parallel_10_4_2.txt Normal file
View File

@ -0,0 +1,40 @@
pan: ltl formula seq_eq_parallel
Depth= 369 States= 1e+06 Transitions= 2.13e+06 Memory= 428.827 t= 4.25 R= 2e+05
(Spin Version 6.5.2 -- 6 December 2019)
+ Partial Order Reduction
Full statespace search for:
never claim + (seq_eq_parallel)
assertion violations + (if within scope of claim)
acceptance cycles + (fairness disabled)
invalid end states - (disabled by never claim)
State-vector 356 byte, depth reached 369, errors: 0
1917106 states, stored
2156787 states, matched
4073893 transitions (= stored+matched)
0 atomic steps
hash conflicts: 67855 (resolved)
Stats on memory usage (in Megabytes):
702.065 equivalent memory usage for states (stored*(State-vector + overhead))
576.005 actual memory usage for states (compression: 82.04%)
state-vector as stored = 287 byte + 28 byte overhead
128.000 memory used for hash table (-w24)
0.534 memory used for DFS stack (-m10000)
704.315 total actual memory usage
unreached in proctype ThreadedReverser
(0 of 15 states)
unreached in init
reversal_seq_eq_parallel_10_4_2.pml:87, state 71, "seq_eq_to_parallel = 0"
reversal_seq_eq_parallel_10_4_2.pml:91, state 81, "-end-"
(2 of 81 states)
unreached in claim seq_eq_parallel
_spin_nvr.tmp:8, state 10, "-end-"
(1 of 10 states)
pan: elapsed time 8.53 seconds
pan: rate 224748.65 states/second

45
ReversalModel/outputs/trace_seq_eq_parallel_10_4_3.txt Normal file
View File

@ -0,0 +1,45 @@
pan: ltl formula seq_eq_parallel
Depth= 369 States= 1e+06 Transitions= 2.13e+06 Memory= 428.827 t= 4.58 R= 2e+05
Depth= 369 States= 2e+06 Transitions= 4.25e+06 Memory= 729.120 t= 9.53 R= 2e+05
Depth= 369 States= 3e+06 Transitions= 6.37e+06 Memory= 1029.413 t= 14.7 R= 2e+05
Depth= 369 States= 4e+06 Transitions= 8.5e+06 Memory= 1329.706 t= 19.5 R= 2e+05
Depth= 369 States= 5e+06 Transitions= 1.06e+07 Memory= 1629.901 t= 23.2 R= 2e+05
Depth= 369 States= 6e+06 Transitions= 1.28e+07 Memory= 1930.194 t= 26.8 R= 2e+05
(Spin Version 6.5.2 -- 6 December 2019)
+ Partial Order Reduction
Full statespace search for:
never claim + (seq_eq_parallel)
assertion violations + (if within scope of claim)
acceptance cycles + (fairness disabled)
invalid end states - (disabled by never claim)
State-vector 356 byte, depth reached 369, errors: 0
6058836 states, stored
6816512 states, matched
12875348 transitions (= stored+matched)
0 atomic steps
hash conflicts: 734465 (resolved)
Stats on memory usage (in Megabytes):
2218.812 equivalent memory usage for states (stored*(State-vector + overhead))
1819.857 actual memory usage for states (compression: 82.02%)
state-vector as stored = 287 byte + 28 byte overhead
128.000 memory used for hash table (-w24)
0.534 memory used for DFS stack (-m10000)
1947.870 total actual memory usage
unreached in proctype ThreadedReverser
(0 of 15 states)
unreached in init
reversal_seq_eq_parallel_10_4_3.pml:87, state 72, "seq_eq_to_parallel = 0"
reversal_seq_eq_parallel_10_4_3.pml:91, state 82, "-end-"
(2 of 82 states)
unreached in claim seq_eq_parallel
_spin_nvr.tmp:8, state 10, "-end-"
(1 of 10 states)
pan: elapsed time 27 seconds
pan: rate 224567.68 states/second

54
ReversalModel/outputs/trace_seq_eq_parallel_10_4_4.txt Normal file
View File

@ -0,0 +1,54 @@
pan: ltl formula seq_eq_parallel
Depth= 369 States= 1e+06 Transitions= 2.13e+06 Memory= 428.827 t= 3.48 R= 3e+05
Depth= 369 States= 2e+06 Transitions= 4.25e+06 Memory= 729.120 t= 6.82 R= 3e+05
Depth= 369 States= 3e+06 Transitions= 6.37e+06 Memory= 1029.413 t= 10.2 R= 3e+05
Depth= 369 States= 4e+06 Transitions= 8.5e+06 Memory= 1329.706 t= 13.6 R= 3e+05
Depth= 369 States= 5e+06 Transitions= 1.06e+07 Memory= 1629.901 t= 17 R= 3e+05
Depth= 369 States= 6e+06 Transitions= 1.28e+07 Memory= 1930.194 t= 20.5 R= 3e+05
Depth= 369 States= 7e+06 Transitions= 1.49e+07 Memory= 2230.487 t= 24.5 R= 3e+05
Depth= 369 States= 8e+06 Transitions= 1.7e+07 Memory= 2530.683 t= 28.6 R= 3e+05
Depth= 369 States= 9e+06 Transitions= 1.91e+07 Memory= 2830.976 t= 36.3 R= 2e+05
Depth= 369 States= 1e+07 Transitions= 2.13e+07 Memory= 3131.269 t= 44 R= 2e+05
Depth= 369 States= 1.1e+07 Transitions= 2.34e+07 Memory= 3431.464 t= 52.4 R= 2e+05
Depth= 369 States= 1.2e+07 Transitions= 2.55e+07 Memory= 3731.757 t= 62.3 R= 2e+05
Depth= 369 States= 1.3e+07 Transitions= 2.76e+07 Memory= 4031.952 t= 74.1 R= 2e+05
Depth= 369 States= 1.4e+07 Transitions= 2.98e+07 Memory= 4332.245 t= 87.3 R= 2e+05
(Spin Version 6.5.2 -- 6 December 2019)
+ Partial Order Reduction
Full statespace search for:
never claim + (seq_eq_parallel)
assertion violations + (if within scope of claim)
acceptance cycles + (fairness disabled)
invalid end states - (disabled by never claim)
State-vector 356 byte, depth reached 369, errors: 0
14791874 states, stored
16641875 states, matched
31433749 transitions (= stored+matched)
0 atomic steps
hash conflicts: 4909886 (resolved)
Stats on memory usage (in Megabytes):
5416.946 equivalent memory usage for states (stored*(State-vector + overhead))
4442.660 actual memory usage for states (compression: 82.01%)
state-vector as stored = 287 byte + 28 byte overhead
128.000 memory used for hash table (-w24)
0.534 memory used for DFS stack (-m10000)
1.157 memory lost to fragmentation
4570.038 total actual memory usage
unreached in proctype ThreadedReverser
(0 of 15 states)
unreached in init
reversal_seq_eq_parallel_10_4_4.pml:87, state 73, "seq_eq_to_parallel = 0"
reversal_seq_eq_parallel_10_4_4.pml:91, state 83, "-end-"
(2 of 83 states)
unreached in claim seq_eq_parallel
_spin_nvr.tmp:8, state 10, "-end-"
(1 of 10 states)
pan: elapsed time 99.2 seconds
pan: rate 149156.74 states/second

24
ReversalModel/outputs/trace_seq_eq_parallel_10_4_5.txt Normal file
View File

@ -0,0 +1,24 @@
pan: ltl formula seq_eq_parallel
Depth= 369 States= 1e+06 Transitions= 2.13e+06 Memory= 428.827 t= 3.33 R= 3e+05
Depth= 369 States= 2e+06 Transitions= 4.25e+06 Memory= 729.120 t= 6.74 R= 3e+05
Depth= 369 States= 3e+06 Transitions= 6.37e+06 Memory= 1029.413 t= 10.2 R= 3e+05
Depth= 369 States= 4e+06 Transitions= 8.5e+06 Memory= 1329.706 t= 13.6 R= 3e+05
Depth= 369 States= 5e+06 Transitions= 1.06e+07 Memory= 1629.901 t= 17 R= 3e+05
Depth= 369 States= 6e+06 Transitions= 1.28e+07 Memory= 1930.194 t= 20.5 R= 3e+05
Depth= 369 States= 7e+06 Transitions= 1.49e+07 Memory= 2230.487 t= 24.7 R= 3e+05
Depth= 369 States= 8e+06 Transitions= 1.7e+07 Memory= 2530.683 t= 30.4 R= 3e+05
Depth= 369 States= 9e+06 Transitions= 1.91e+07 Memory= 2830.976 t= 37.7 R= 2e+05
Depth= 369 States= 1e+07 Transitions= 2.13e+07 Memory= 3131.269 t= 45.1 R= 2e+05
Depth= 369 States= 1.1e+07 Transitions= 2.34e+07 Memory= 3431.562 t= 53.8 R= 2e+05
Depth= 369 States= 1.2e+07 Transitions= 2.55e+07 Memory= 3731.757 t= 64.1 R= 2e+05
Depth= 369 States= 1.3e+07 Transitions= 2.76e+07 Memory= 4031.952 t= 75.7 R= 2e+05
Depth= 369 States= 1.4e+07 Transitions= 2.98e+07 Memory= 4332.245 t= 89 R= 2e+05
Depth= 369 States= 1.5e+07 Transitions= 3.19e+07 Memory= 4632.538 t= 101 R= 1e+05
Depth= 369 States= 1.6e+07 Transitions= 3.4e+07 Memory= 4932.831 t= 113 R= 1e+05
Depth= 369 States= 1.7e+07 Transitions= 3.61e+07 Memory= 5233.026 t= 128 R= 1e+05
Depth= 369 States= 1.8e+07 Transitions= 3.83e+07 Memory= 5533.319 t= 146 R= 1e+05
Depth= 369 States= 1.9e+07 Transitions= 4.04e+07 Memory= 5833.612 t= 167 R= 1e+05
Depth= 369 States= 2e+07 Transitions= 4.25e+07 Memory= 6133.808 t= 185 R= 1e+05
Depth= 369 States= 2.1e+07 Transitions= 4.46e+07 Memory= 6434.101 t= 210 R= 1e+05
Depth= 369 States= 2.2e+07 Transitions= 4.68e+07 Memory= 6734.394 t= 240 R= 9e+04
Depth= 369 States= 2.3e+07 Transitions= 4.89e+07 Memory= 7034.687 t= 275 R= 8e+04

24
ReversalModel/outputs/trace_seq_eq_parallel_10_4_6.txt Normal file
View File

@ -0,0 +1,24 @@
pan: ltl formula seq_eq_parallel
Depth= 369 States= 1e+06 Transitions= 2.13e+06 Memory= 428.827 t= 3.37 R= 3e+05
Depth= 369 States= 2e+06 Transitions= 4.25e+06 Memory= 729.120 t= 6.77 R= 3e+05
Depth= 369 States= 3e+06 Transitions= 6.37e+06 Memory= 1029.413 t= 10.2 R= 3e+05
Depth= 369 States= 4e+06 Transitions= 8.5e+06 Memory= 1329.706 t= 13.6 R= 3e+05
Depth= 369 States= 5e+06 Transitions= 1.06e+07 Memory= 1629.901 t= 17.7 R= 3e+05
Depth= 369 States= 6e+06 Transitions= 1.28e+07 Memory= 1930.194 t= 23.4 R= 3e+05
Depth= 369 States= 7e+06 Transitions= 1.49e+07 Memory= 2230.487 t= 29.5 R= 2e+05
Depth= 369 States= 8e+06 Transitions= 1.7e+07 Memory= 2530.683 t= 36.1 R= 2e+05
Depth= 369 States= 9e+06 Transitions= 1.91e+07 Memory= 2830.976 t= 43 R= 2e+05
Depth= 369 States= 1e+07 Transitions= 2.13e+07 Memory= 3131.269 t= 51 R= 2e+05
Depth= 369 States= 1.1e+07 Transitions= 2.34e+07 Memory= 3431.562 t= 61 R= 2e+05
Depth= 369 States= 1.2e+07 Transitions= 2.55e+07 Memory= 3731.757 t= 71.5 R= 2e+05
Depth= 369 States= 1.3e+07 Transitions= 2.76e+07 Memory= 4032.050 t= 83.7 R= 2e+05
Depth= 369 States= 1.4e+07 Transitions= 2.98e+07 Memory= 4332.245 t= 94.4 R= 1e+05
Depth= 369 States= 1.5e+07 Transitions= 3.19e+07 Memory= 4632.538 t= 105 R= 1e+05
Depth= 369 States= 1.6e+07 Transitions= 3.4e+07 Memory= 4932.831 t= 118 R= 1e+05
Depth= 369 States= 1.7e+07 Transitions= 3.61e+07 Memory= 5233.026 t= 134 R= 1e+05
Depth= 369 States= 1.8e+07 Transitions= 3.83e+07 Memory= 5533.319 t= 154 R= 1e+05
Depth= 369 States= 1.9e+07 Transitions= 4.04e+07 Memory= 5833.612 t= 171 R= 1e+05
Depth= 369 States= 2e+07 Transitions= 4.25e+07 Memory= 6133.808 t= 191 R= 1e+05
Depth= 369 States= 2.1e+07 Transitions= 4.46e+07 Memory= 6434.101 t= 218 R= 1e+05
Depth= 369 States= 2.2e+07 Transitions= 4.68e+07 Memory= 6734.394 t= 248 R= 9e+04
Depth= 369 States= 2.3e+07 Transitions= 4.89e+07 Memory= 7034.687 t= 286 R= 8e+04

23
ReversalModel/outputs/trace_seq_eq_parallel_10_4_7.txt Normal file
View File

@ -0,0 +1,23 @@
pan: ltl formula seq_eq_parallel
Depth= 369 States= 1e+06 Transitions= 2.13e+06 Memory= 428.827 t= 3.42 R= 3e+05
Depth= 369 States= 2e+06 Transitions= 4.25e+06 Memory= 729.120 t= 8.07 R= 2e+05
Depth= 369 States= 3e+06 Transitions= 6.37e+06 Memory= 1029.413 t= 13.2 R= 2e+05
Depth= 369 States= 4e+06 Transitions= 8.5e+06 Memory= 1329.706 t= 18.4 R= 2e+05
Depth= 369 States= 5e+06 Transitions= 1.06e+07 Memory= 1629.901 t= 24.4 R= 2e+05
Depth= 369 States= 6e+06 Transitions= 1.28e+07 Memory= 1930.194 t= 31 R= 2e+05
Depth= 369 States= 7e+06 Transitions= 1.49e+07 Memory= 2230.487 t= 38.5 R= 2e+05
Depth= 369 States= 8e+06 Transitions= 1.7e+07 Memory= 2530.683 t= 47.3 R= 2e+05
Depth= 369 States= 9e+06 Transitions= 1.91e+07 Memory= 2830.976 t= 58.3 R= 2e+05
Depth= 369 States= 1e+07 Transitions= 2.13e+07 Memory= 3131.269 t= 70.1 R= 1e+05
Depth= 369 States= 1.1e+07 Transitions= 2.34e+07 Memory= 3431.562 t= 77.5 R= 1e+05
Depth= 369 States= 1.2e+07 Transitions= 2.55e+07 Memory= 3731.757 t= 85.1 R= 1e+05
Depth= 369 States= 1.3e+07 Transitions= 2.76e+07 Memory= 4032.050 t= 94.8 R= 1e+05
Depth= 369 States= 1.4e+07 Transitions= 2.98e+07 Memory= 4332.343 t= 106 R= 1e+05
Depth= 369 States= 1.5e+07 Transitions= 3.19e+07 Memory= 4632.636 t= 122 R= 1e+05
Depth= 369 States= 1.6e+07 Transitions= 3.4e+07 Memory= 4932.831 t= 138 R= 1e+05
Depth= 369 States= 1.7e+07 Transitions= 3.61e+07 Memory= 5233.026 t= 158 R= 1e+05
Depth= 369 States= 1.8e+07 Transitions= 3.83e+07 Memory= 5533.319 t= 179 R= 1e+05
Depth= 369 States= 1.9e+07 Transitions= 4.04e+07 Memory= 5833.612 t= 203 R= 9e+04
Depth= 369 States= 2e+07 Transitions= 4.25e+07 Memory= 6133.808 t= 217 R= 9e+04
Depth= 369 States= 2.1e+07 Transitions= 4.46e+07 Memory= 6434.101 t= 236 R= 9e+04
Depth= 369 States= 2.2e+07 Transitions= 4.68e+07 Memory= 6734.394 t= 267 R= 8e+04

23
ReversalModel/outputs/trace_seq_eq_parallel_10_4_8.txt Normal file
View File

@ -0,0 +1,23 @@
pan: ltl formula seq_eq_parallel
Depth= 369 States= 1e+06 Transitions= 2.13e+06 Memory= 428.827 t= 3.37 R= 3e+05
Depth= 369 States= 2e+06 Transitions= 4.25e+06 Memory= 729.120 t= 7.31 R= 3e+05
Depth= 369 States= 3e+06 Transitions= 6.37e+06 Memory= 1029.413 t= 12.1 R= 2e+05
Depth= 369 States= 4e+06 Transitions= 8.5e+06 Memory= 1329.706 t= 17 R= 2e+05
Depth= 369 States= 5e+06 Transitions= 1.06e+07 Memory= 1629.901 t= 22.5 R= 2e+05
Depth= 369 States= 6e+06 Transitions= 1.28e+07 Memory= 1930.194 t= 28.6 R= 2e+05
Depth= 369 States= 7e+06 Transitions= 1.49e+07 Memory= 2230.487 t= 36.1 R= 2e+05
Depth= 369 States= 8e+06 Transitions= 1.7e+07 Memory= 2530.683 t= 45.7 R= 2e+05
Depth= 369 States= 9e+06 Transitions= 1.91e+07 Memory= 2830.976 t= 56.2 R= 2e+05
Depth= 369 States= 1e+07 Transitions= 2.13e+07 Memory= 3131.269 t= 67.5 R= 1e+05
Depth= 369 States= 1.1e+07 Transitions= 2.34e+07 Memory= 3431.562 t= 80.9 R= 1e+05
Depth= 369 States= 1.2e+07 Transitions= 2.55e+07 Memory= 3731.757 t= 93.7 R= 1e+05
Depth= 369 States= 1.3e+07 Transitions= 2.76e+07 Memory= 4032.050 t= 109 R= 1e+05
Depth= 369 States= 1.4e+07 Transitions= 2.98e+07 Memory= 4332.343 t= 126 R= 1e+05
Depth= 369 States= 1.5e+07 Transitions= 3.19e+07 Memory= 4632.636 t= 136 R= 1e+05
Depth= 369 States= 1.6e+07 Transitions= 3.4e+07 Memory= 4932.831 t= 143 R= 1e+05
Depth= 369 States= 1.7e+07 Transitions= 3.61e+07 Memory= 5233.026 t= 153 R= 1e+05
Depth= 369 States= 1.8e+07 Transitions= 3.83e+07 Memory= 5533.319 t= 167 R= 1e+05
Depth= 369 States= 1.9e+07 Transitions= 4.04e+07 Memory= 5833.612 t= 185 R= 1e+05
Depth= 369 States= 2e+07 Transitions= 4.25e+07 Memory= 6133.808 t= 209 R= 1e+05
Depth= 369 States= 2.1e+07 Transitions= 4.46e+07 Memory= 6434.101 t= 234 R= 9e+04
Depth= 369 States= 2.2e+07 Transitions= 4.68e+07 Memory= 6734.394 t= 269 R= 8e+04

22
ReversalModel/outputs/trace_seq_eq_parallel_10_4_9.txt Normal file
View File

@ -0,0 +1,22 @@
pan: ltl formula seq_eq_parallel
Depth= 369 States= 1e+06 Transitions= 2.13e+06 Memory= 428.827 t= 4.44 R= 2e+05
Depth= 369 States= 2e+06 Transitions= 4.25e+06 Memory= 729.120 t= 8.48 R= 2e+05
Depth= 369 States= 3e+06 Transitions= 6.37e+06 Memory= 1029.413 t= 12.4 R= 2e+05
Depth= 369 States= 4e+06 Transitions= 8.5e+06 Memory= 1329.706 t= 16.1 R= 2e+05
Depth= 369 States= 5e+06 Transitions= 1.06e+07 Memory= 1629.901 t= 20.6 R= 2e+05
Depth= 369 States= 6e+06 Transitions= 1.28e+07 Memory= 1930.194 t= 25.1 R= 2e+05
Depth= 369 States= 7e+06 Transitions= 1.49e+07 Memory= 2230.487 t= 30.3 R= 2e+05
Depth= 369 States= 8e+06 Transitions= 1.7e+07 Memory= 2530.683 t= 36.6 R= 2e+05
Depth= 369 States= 9e+06 Transitions= 1.91e+07 Memory= 2830.976 t= 43.4 R= 2e+05
Depth= 369 States= 1e+07 Transitions= 2.13e+07 Memory= 3131.269 t= 51.4 R= 2e+05
Depth= 369 States= 1.1e+07 Transitions= 2.34e+07 Memory= 3431.562 t= 61.2 R= 2e+05
Depth= 369 States= 1.2e+07 Transitions= 2.55e+07 Memory= 3731.757 t= 72.8 R= 2e+05
Depth= 369 States= 1.3e+07 Transitions= 2.76e+07 Memory= 4032.050 t= 86.1 R= 2e+05
Depth= 369 States= 1.4e+07 Transitions= 2.98e+07 Memory= 4332.343 t= 100 R= 1e+05
Depth= 369 States= 1.5e+07 Transitions= 3.19e+07 Memory= 4632.636 t= 113 R= 1e+05
Depth= 369 States= 1.6e+07 Transitions= 3.4e+07 Memory= 4932.831 t= 130 R= 1e+05
Depth= 369 States= 1.7e+07 Transitions= 3.61e+07 Memory= 5233.026 t= 148 R= 1e+05
Depth= 369 States= 1.8e+07 Transitions= 3.83e+07 Memory= 5533.319 t= 167 R= 1e+05
Depth= 369 States= 1.9e+07 Transitions= 4.04e+07 Memory= 5833.612 t= 184 R= 1e+05
Depth= 369 States= 2e+07 Transitions= 4.25e+07 Memory= 6133.808 t= 211 R= 9e+04
Depth= 369 States= 2.1e+07 Transitions= 4.46e+07 Memory= 6434.101 t= 282 R= 7e+04

20
ReversalModel/outputs/trace_seq_eq_parallel_10_5_10.txt Normal file
View File

@ -0,0 +1,20 @@
pan: ltl formula seq_eq_parallel
Depth= 389 States= 1e+06 Transitions= 2.12e+06 Memory= 445.233 t= 4.5 R= 2e+05
Depth= 389 States= 2e+06 Transitions= 4.25e+06 Memory= 761.737 t= 8.61 R= 2e+05
Depth= 389 States= 3e+06 Transitions= 6.38e+06 Memory= 1078.339 t= 14 R= 2e+05
Depth= 389 States= 4e+06 Transitions= 8.5e+06 Memory= 1394.940 t= 19.4 R= 2e+05
Depth= 389 States= 5e+06 Transitions= 1.06e+07 Memory= 1711.444 t= 27.4 R= 2e+05
Depth= 389 States= 6e+06 Transitions= 1.28e+07 Memory= 2028.046 t= 35.1 R= 2e+05
Depth= 389 States= 7e+06 Transitions= 1.49e+07 Memory= 2344.647 t= 43.7 R= 2e+05
Depth= 389 States= 8e+06 Transitions= 1.7e+07 Memory= 2661.249 t= 54 R= 1e+05
Depth= 389 States= 9e+06 Transitions= 1.91e+07 Memory= 2977.753 t= 67.2 R= 1e+05
Depth= 389 States= 1e+07 Transitions= 2.13e+07 Memory= 3294.355 t= 82.6 R= 1e+05
Depth= 389 States= 1.1e+07 Transitions= 2.34e+07 Memory= 3610.956 t= 98.9 R= 1e+05
Depth= 389 States= 1.2e+07 Transitions= 2.55e+07 Memory= 3927.558 t= 118 R= 1e+05
Depth= 389 States= 1.3e+07 Transitions= 2.76e+07 Memory= 4244.159 t= 140 R= 9e+04
Depth= 389 States= 1.4e+07 Transitions= 2.98e+07 Memory= 4560.761 t= 155 R= 9e+04
Depth= 389 States= 1.5e+07 Transitions= 3.19e+07 Memory= 4877.265 t= 172 R= 9e+04
Depth= 389 States= 1.6e+07 Transitions= 3.4e+07 Memory= 5193.866 t= 189 R= 8e+04
Depth= 389 States= 1.7e+07 Transitions= 3.61e+07 Memory= 5510.468 t= 212 R= 8e+04
Depth= 389 States= 1.8e+07 Transitions= 3.83e+07 Memory= 5827.069 t= 243 R= 7e+04
Depth= 389 States= 1.9e+07 Transitions= 4.04e+07 Memory= 6143.671 t= 275 R= 7e+04

46
ReversalModel/outputs/trace_seq_eq_parallel_10_5_2.txt Normal file
View File

@ -0,0 +1,46 @@
pan: ltl formula seq_eq_parallel
Depth= 389 States= 1e+06 Transitions= 2.12e+06 Memory= 445.233 t= 4.79 R= 2e+05
Depth= 389 States= 2e+06 Transitions= 4.25e+06 Memory= 761.737 t= 10.4 R= 2e+05
Depth= 389 States= 3e+06 Transitions= 6.37e+06 Memory= 1078.339 t= 16.1 R= 2e+05
Depth= 389 States= 4e+06 Transitions= 8.5e+06 Memory= 1394.843 t= 22.9 R= 2e+05
Depth= 389 States= 5e+06 Transitions= 1.06e+07 Memory= 1711.444 t= 29.7 R= 2e+05
Depth= 389 States= 6e+06 Transitions= 1.28e+07 Memory= 2027.948 t= 38.3 R= 2e+05
(Spin Version 6.5.2 -- 6 December 2019)
+ Partial Order Reduction
Full statespace search for:
never claim + (seq_eq_parallel)
assertion violations + (if within scope of claim)
acceptance cycles + (fairness disabled)
invalid end states - (disabled by never claim)
State-vector 364 byte, depth reached 389, errors: 0
6746164 states, stored
7590105 states, matched
14336269 transitions (= stored+matched)
0 atomic steps
hash conflicts: 913206 (resolved)
Stats on memory usage (in Megabytes):
2521.988 equivalent memory usage for states (stored*(State-vector + overhead))
2140.809 actual memory usage for states (compression: 84.89%)
state-vector as stored = 305 byte + 28 byte overhead
128.000 memory used for hash table (-w24)
0.534 memory used for DFS stack (-m10000)
5.068 memory lost to fragmentation
2264.276 total actual memory usage
unreached in proctype ThreadedReverser
(0 of 15 states)
unreached in init
reversal_seq_eq_parallel_10_5_2.pml:87, state 71, "seq_eq_to_parallel = 0"
reversal_seq_eq_parallel_10_5_2.pml:91, state 81, "-end-"
(2 of 81 states)
unreached in claim seq_eq_parallel
_spin_nvr.tmp:8, state 10, "-end-"
(1 of 10 states)
pan: elapsed time 44.7 seconds
pan: rate 150819.67 states/second

20
ReversalModel/outputs/trace_seq_eq_parallel_10_5_3.txt Normal file
View File

@ -0,0 +1,20 @@
pan: ltl formula seq_eq_parallel
Depth= 389 States= 1e+06 Transitions= 2.12e+06 Memory= 445.233 t= 4.75 R= 2e+05
Depth= 389 States= 2e+06 Transitions= 4.25e+06 Memory= 761.737 t= 10.5 R= 2e+05
Depth= 389 States= 3e+06 Transitions= 6.37e+06 Memory= 1078.339 t= 17 R= 2e+05
Depth= 389 States= 4e+06 Transitions= 8.5e+06 Memory= 1394.843 t= 24.4 R= 2e+05
Depth= 389 States= 5e+06 Transitions= 1.06e+07 Memory= 1711.444 t= 29.6 R= 2e+05
Depth= 389 States= 6e+06 Transitions= 1.28e+07 Memory= 2028.046 t= 34.7 R= 2e+05
Depth= 389 States= 7e+06 Transitions= 1.49e+07 Memory= 2344.550 t= 41.4 R= 2e+05
Depth= 389 States= 8e+06 Transitions= 1.7e+07 Memory= 2661.151 t= 48.8 R= 2e+05
Depth= 389 States= 9e+06 Transitions= 1.91e+07 Memory= 2977.753 t= 57.8 R= 2e+05
Depth= 389 States= 1e+07 Transitions= 2.13e+07 Memory= 3294.355 t= 70.9 R= 1e+05
Depth= 389 States= 1.1e+07 Transitions= 2.34e+07 Memory= 3610.858 t= 122 R= 9e+04
Depth= 389 States= 1.2e+07 Transitions= 2.55e+07 Memory= 3927.460 t= 224 R= 5e+04
Depth= 389 States= 1.3e+07 Transitions= 2.76e+07 Memory= 4244.062 t= 325 R= 4e+04
Depth= 389 States= 1.4e+07 Transitions= 2.98e+07 Memory= 4560.663 t= 338 R= 4e+04
Depth= 389 States= 1.5e+07 Transitions= 3.19e+07 Memory= 4877.167 t= 353 R= 4e+04
Depth= 389 States= 1.6e+07 Transitions= 3.4e+07 Memory= 5193.769 t= 374 R= 4e+04
Depth= 389 States= 1.7e+07 Transitions= 3.61e+07 Memory= 5510.370 t= 399 R= 4e+04
Depth= 389 States= 1.8e+07 Transitions= 3.83e+07 Memory= 5826.972 t= 424 R= 4e+04
Depth= 389 States= 1.9e+07 Transitions= 4.04e+07 Memory= 6143.573 t= 454 R= 4e+04

20
ReversalModel/outputs/trace_seq_eq_parallel_10_5_4.txt Normal file
View File

@ -0,0 +1,20 @@
pan: ltl formula seq_eq_parallel
Depth= 389 States= 1e+06 Transitions= 2.12e+06 Memory= 445.233 t= 3.98 R= 3e+05
Depth= 389 States= 2e+06 Transitions= 4.25e+06 Memory= 761.737 t= 8.91 R= 2e+05
Depth= 389 States= 3e+06 Transitions= 6.37e+06 Memory= 1078.339 t= 14.4 R= 2e+05
Depth= 389 States= 4e+06 Transitions= 8.5e+06 Memory= 1394.843 t= 20.1 R= 2e+05
Depth= 389 States= 5e+06 Transitions= 1.06e+07 Memory= 1711.444 t= 26.7 R= 2e+05
Depth= 389 States= 6e+06 Transitions= 1.28e+07 Memory= 2028.046 t= 35.6 R= 2e+05
Depth= 389 States= 7e+06 Transitions= 1.49e+07 Memory= 2344.647 t= 44.6 R= 2e+05
Depth= 389 States= 8e+06 Transitions= 1.7e+07 Memory= 2661.151 t= 86.9 R= 9e+04
Depth= 389 States= 9e+06 Transitions= 1.91e+07 Memory= 2977.753 t= 112 R= 8e+04
Depth= 389 States= 1e+07 Transitions= 2.13e+07 Memory= 3294.355 t= 223 R= 4e+04
Depth= 389 States= 1.1e+07 Transitions= 2.34e+07 Memory= 3610.956 t= 303 R= 4e+04
Depth= 389 States= 1.2e+07 Transitions= 2.55e+07 Memory= 3927.460 t= 314 R= 4e+04
Depth= 389 States= 1.3e+07 Transitions= 2.76e+07 Memory= 4244.062 t= 325 R= 4e+04
Depth= 389 States= 1.4e+07 Transitions= 2.98e+07 Memory= 4560.663 t= 343 R= 4e+04
Depth= 389 States= 1.5e+07 Transitions= 3.19e+07 Memory= 4877.265 t= 359 R= 4e+04
Depth= 389 States= 1.6e+07 Transitions= 3.4e+07 Memory= 5193.866 t= 378 R= 4e+04
Depth= 389 States= 1.7e+07 Transitions= 3.61e+07 Memory= 5510.370 t= 397 R= 4e+04
Depth= 389 States= 1.8e+07 Transitions= 3.83e+07 Memory= 5826.972 t= 420 R= 4e+04
Depth= 389 States= 1.9e+07 Transitions= 4.04e+07 Memory= 6143.573 t= 442 R= 4e+04

15
ReversalModel/outputs/trace_seq_eq_parallel_10_5_5.txt Normal file
View File

@ -0,0 +1,15 @@
pan: ltl formula seq_eq_parallel
Depth= 389 States= 1e+06 Transitions= 2.12e+06 Memory= 445.233 t= 5.51 R= 2e+05
Depth= 389 States= 2e+06 Transitions= 4.25e+06 Memory= 761.737 t= 9.95 R= 2e+05
Depth= 389 States= 3e+06 Transitions= 6.37e+06 Memory= 1078.339 t= 17.2 R= 2e+05
Depth= 389 States= 4e+06 Transitions= 8.5e+06 Memory= 1394.843 t= 27.8 R= 1e+05
Depth= 389 States= 5e+06 Transitions= 1.06e+07 Memory= 1711.444 t= 43.1 R= 1e+05
Depth= 389 States= 6e+06 Transitions= 1.28e+07 Memory= 2028.046 t= 58.1 R= 1e+05
Depth= 389 States= 7e+06 Transitions= 1.49e+07 Memory= 2344.647 t= 76.9 R= 9e+04
Depth= 389 States= 8e+06 Transitions= 1.7e+07 Memory= 2661.151 t= 96.2 R= 8e+04
Depth= 389 States= 9e+06 Transitions= 1.91e+07 Memory= 2977.753 t= 120 R= 7e+04
Depth= 389 States= 1e+07 Transitions= 2.13e+07 Memory= 3294.355 t= 144 R= 7e+04
Depth= 389 States= 1.1e+07 Transitions= 2.34e+07 Memory= 3610.956 t= 166 R= 7e+04
Depth= 389 States= 1.2e+07 Transitions= 2.55e+07 Memory= 3927.558 t= 184 R= 7e+04
Depth= 389 States= 1.3e+07 Transitions= 2.76e+07 Memory= 4244.062 t= 218 R= 6e+04
Depth= 389 States= 1.4e+07 Transitions= 2.98e+07 Memory= 4560.663 t= 257 R= 5e+04

24
ReversalModel/outputs/trace_seq_eq_parallel_10_5_6.txt Normal file
View File

@ -0,0 +1,24 @@
pan: ltl formula seq_eq_parallel
Depth= 389 States= 1e+06 Transitions= 2.12e+06 Memory= 445.233 t= 4.14 R= 2e+05
Depth= 389 States= 2e+06 Transitions= 4.25e+06 Memory= 761.737 t= 8.46 R= 2e+05
Depth= 389 States= 3e+06 Transitions= 6.38e+06 Memory= 1078.339 t= 13.1 R= 2e+05
Depth= 389 States= 4e+06 Transitions= 8.5e+06 Memory= 1394.940 t= 18.1 R= 2e+05
Depth= 389 States= 5e+06 Transitions= 1.06e+07 Memory= 1711.444 t= 23.2 R= 2e+05
Depth= 389 States= 6e+06 Transitions= 1.28e+07 Memory= 2028.046 t= 28.5 R= 2e+05
Depth= 389 States= 7e+06 Transitions= 1.49e+07 Memory= 2344.647 t= 36.5 R= 2e+05
Depth= 389 States= 8e+06 Transitions= 1.7e+07 Memory= 2661.249 t= 45 R= 2e+05
Depth= 389 States= 9e+06 Transitions= 1.91e+07 Memory= 2977.753 t= 52.5 R= 2e+05
Depth= 389 States= 1e+07 Transitions= 2.13e+07 Memory= 3294.355 t= 60.5 R= 2e+05
Depth= 389 States= 1.1e+07 Transitions= 2.34e+07 Memory= 3610.956 t= 71.3 R= 2e+05
Depth= 389 States= 1.2e+07 Transitions= 2.55e+07 Memory= 3927.558 t= 82.1 R= 1e+05
Depth= 389 States= 1.3e+07 Transitions= 2.76e+07 Memory= 4244.062 t= 93.5 R= 1e+05
Depth= 389 States= 1.4e+07 Transitions= 2.98e+07 Memory= 4560.663 t= 108 R= 1e+05
Depth= 389 States= 1.5e+07 Transitions= 3.19e+07 Memory= 4877.265 t= 124 R= 1e+05
Depth= 389 States= 1.6e+07 Transitions= 3.4e+07 Memory= 5193.866 t= 140 R= 1e+05
Depth= 389 States= 1.7e+07 Transitions= 3.61e+07 Memory= 5510.468 t= 155 R= 1e+05
Depth= 389 States= 1.8e+07 Transitions= 3.83e+07 Memory= 5826.972 t= 172 R= 1e+05
Depth= 389 States= 1.9e+07 Transitions= 4.04e+07 Memory= 6143.573 t= 185 R= 1e+05
Depth= 389 States= 2e+07 Transitions= 4.25e+07 Memory= 6460.175 t= 208 R= 1e+05
Depth= 389 States= 2.1e+07 Transitions= 4.46e+07 Memory= 6776.776 t= 231 R= 9e+04
Depth= 389 States= 2.2e+07 Transitions= 4.68e+07 Memory= 7093.378 t= 258 R= 9e+04
Depth= 389 States= 2.3e+07 Transitions= 4.89e+07 Memory= 7409.882 t= 292 R= 8e+04

22
ReversalModel/outputs/trace_seq_eq_parallel_10_5_7.txt Normal file
View File

@ -0,0 +1,22 @@
pan: ltl formula seq_eq_parallel
Depth= 389 States= 1e+06 Transitions= 2.12e+06 Memory= 445.233 t= 5.05 R= 2e+05
Depth= 389 States= 2e+06 Transitions= 4.25e+06 Memory= 761.737 t= 10.7 R= 2e+05
Depth= 389 States= 3e+06 Transitions= 6.38e+06 Memory= 1078.339 t= 17.1 R= 2e+05
Depth= 389 States= 4e+06 Transitions= 8.5e+06 Memory= 1394.940 t= 24.1 R= 2e+05
Depth= 389 States= 5e+06 Transitions= 1.06e+07 Memory= 1711.444 t= 30.4 R= 2e+05
Depth= 389 States= 6e+06 Transitions= 1.28e+07 Memory= 2028.046 t= 35.6 R= 2e+05
Depth= 389 States= 7e+06 Transitions= 1.49e+07 Memory= 2344.647 t= 40.8 R= 2e+05
Depth= 389 States= 8e+06 Transitions= 1.7e+07 Memory= 2661.249 t= 47.2 R= 2e+05
Depth= 389 States= 9e+06 Transitions= 1.91e+07 Memory= 2977.753 t= 54.4 R= 2e+05
Depth= 389 States= 1e+07 Transitions= 2.13e+07 Memory= 3294.355 t= 64.7 R= 2e+05
Depth= 389 States= 1.1e+07 Transitions= 2.34e+07 Memory= 3610.956 t= 76.4 R= 1e+05
Depth= 389 States= 1.2e+07 Transitions= 2.55e+07 Memory= 3927.558 t= 87 R= 1e+05
Depth= 389 States= 1.3e+07 Transitions= 2.76e+07 Memory= 4244.159 t= 99.1 R= 1e+05
Depth= 389 States= 1.4e+07 Transitions= 2.98e+07 Memory= 4560.663 t= 113 R= 1e+05
Depth= 389 States= 1.5e+07 Transitions= 3.19e+07 Memory= 4877.265 t= 131 R= 1e+05
Depth= 389 States= 1.6e+07 Transitions= 3.4e+07 Memory= 5193.866 t= 148 R= 1e+05
Depth= 389 States= 1.7e+07 Transitions= 3.61e+07 Memory= 5510.468 t= 163 R= 1e+05
Depth= 389 States= 1.8e+07 Transitions= 3.83e+07 Memory= 5827.069 t= 178 R= 1e+05
Depth= 389 States= 1.9e+07 Transitions= 4.04e+07 Memory= 6143.573 t= 205 R= 9e+04
Depth= 389 States= 2e+07 Transitions= 4.25e+07 Memory= 6460.175 t= 241 R= 8e+04
Depth= 389 States= 2.1e+07 Transitions= 4.46e+07 Memory= 6776.776 t= 293 R= 7e+04

21
ReversalModel/outputs/trace_seq_eq_parallel_10_5_8.txt Normal file
View File

@ -0,0 +1,21 @@
pan: ltl formula seq_eq_parallel
Depth= 389 States= 1e+06 Transitions= 2.12e+06 Memory= 445.233 t= 4.97 R= 2e+05
Depth= 389 States= 2e+06 Transitions= 4.25e+06 Memory= 761.737 t= 9.61 R= 2e+05
Depth= 389 States= 3e+06 Transitions= 6.38e+06 Memory= 1078.339 t= 14.6 R= 2e+05
Depth= 389 States= 4e+06 Transitions= 8.5e+06 Memory= 1394.940 t= 20.6 R= 2e+05
Depth= 389 States= 5e+06 Transitions= 1.06e+07 Memory= 1711.444 t= 26.6 R= 2e+05
Depth= 389 States= 6e+06 Transitions= 1.28e+07 Memory= 2028.046 t= 34.5 R= 2e+05
Depth= 389 States= 7e+06 Transitions= 1.49e+07 Memory= 2344.647 t= 43.7 R= 2e+05
Depth= 389 States= 8e+06 Transitions= 1.7e+07 Memory= 2661.249 t= 52.2 R= 2e+05
Depth= 389 States= 9e+06 Transitions= 1.91e+07 Memory= 2977.753 t= 60.9 R= 1e+05
Depth= 389 States= 1e+07 Transitions= 2.13e+07 Memory= 3294.355 t= 70.9 R= 1e+05
Depth= 389 States= 1.1e+07 Transitions= 2.34e+07 Memory= 3610.956 t= 82.1 R= 1e+05
Depth= 389 States= 1.2e+07 Transitions= 2.55e+07 Memory= 3927.558 t= 96.5 R= 1e+05
Depth= 389 States= 1.3e+07 Transitions= 2.76e+07 Memory= 4244.159 t= 112 R= 1e+05
Depth= 389 States= 1.4e+07 Transitions= 2.98e+07 Memory= 4560.663 t= 126 R= 1e+05
Depth= 389 States= 1.5e+07 Transitions= 3.19e+07 Memory= 4877.265 t= 138 R= 1e+05
Depth= 389 States= 1.6e+07 Transitions= 3.4e+07 Memory= 5193.866 t= 150 R= 1e+05
Depth= 389 States= 1.7e+07 Transitions= 3.61e+07 Memory= 5510.468 t= 171 R= 1e+05
Depth= 389 States= 1.8e+07 Transitions= 3.83e+07 Memory= 5827.069 t= 197 R= 9e+04
Depth= 389 States= 1.9e+07 Transitions= 4.04e+07 Memory= 6143.573 t= 229 R= 8e+04
Depth= 389 States= 2e+07 Transitions= 4.25e+07 Memory= 6460.175 t= 275 R= 7e+04

20
ReversalModel/outputs/trace_seq_eq_parallel_10_5_9.txt Normal file
View File

@ -0,0 +1,20 @@
pan: ltl formula seq_eq_parallel
Depth= 389 States= 1e+06 Transitions= 2.12e+06 Memory= 445.233 t= 5.14 R= 2e+05
Depth= 389 States= 2e+06 Transitions= 4.25e+06 Memory= 761.737 t= 9.95 R= 2e+05
Depth= 389 States= 3e+06 Transitions= 6.38e+06 Memory= 1078.339 t= 14.1 R= 2e+05
Depth= 389 States= 4e+06 Transitions= 8.5e+06 Memory= 1394.940 t= 19.2 R= 2e+05
Depth= 389 States= 5e+06 Transitions= 1.06e+07 Memory= 1711.444 t= 24.6 R= 2e+05
Depth= 389 States= 6e+06 Transitions= 1.28e+07 Memory= 2028.046 t= 32.7 R= 2e+05
Depth= 389 States= 7e+06 Transitions= 1.49e+07 Memory= 2344.647 t= 40.7 R= 2e+05
Depth= 389 States= 8e+06 Transitions= 1.7e+07 Memory= 2661.249 t= 50.1 R= 2e+05
Depth= 389 States= 9e+06 Transitions= 1.91e+07 Memory= 2977.753 t= 61.4 R= 1e+05
Depth= 389 States= 1e+07 Transitions= 2.13e+07 Memory= 3294.355 t= 76.2 R= 1e+05
Depth= 389 States= 1.1e+07 Transitions= 2.34e+07 Memory= 3610.956 t= 91.8 R= 1e+05
Depth= 389 States= 1.2e+07 Transitions= 2.55e+07 Memory= 3927.558 t= 109 R= 1e+05
Depth= 389 States= 1.3e+07 Transitions= 2.76e+07 Memory= 4244.159 t= 131 R= 1e+05
Depth= 389 States= 1.4e+07 Transitions= 2.98e+07 Memory= 4560.663 t= 151 R= 9e+04
Depth= 389 States= 1.5e+07 Transitions= 3.19e+07 Memory= 4877.265 t= 170 R= 9e+04
Depth= 389 States= 1.6e+07 Transitions= 3.4e+07 Memory= 5193.866 t= 186 R= 9e+04
Depth= 389 States= 1.7e+07 Transitions= 3.61e+07 Memory= 5510.468 t= 208 R= 8e+04
Depth= 389 States= 1.8e+07 Transitions= 3.83e+07 Memory= 5827.069 t= 238 R= 8e+04
Depth= 389 States= 1.9e+07 Transitions= 4.04e+07 Memory= 6143.671 t= 274 R= 7e+04

20
ReversalModel/outputs/trace_seq_eq_parallel_10_6_10.txt Normal file
View File

@ -0,0 +1,20 @@
pan: ltl formula seq_eq_parallel
Depth= 409 States= 1e+06 Transitions= 2.12e+06 Memory= 453.632 t= 5.04 R= 2e+05
Depth= 409 States= 2e+06 Transitions= 4.25e+06 Memory= 778.730 t= 11.1 R= 2e+05
Depth= 409 States= 3e+06 Transitions= 6.38e+06 Memory= 1103.632 t= 20.2 R= 1e+05
Depth= 409 States= 4e+06 Transitions= 8.5e+06 Memory= 1428.730 t= 27.5 R= 1e+05
Depth= 409 States= 5e+06 Transitions= 1.06e+07 Memory= 1753.827 t= 34.2 R= 1e+05
Depth= 409 States= 6e+06 Transitions= 1.28e+07 Memory= 2078.730 t= 41.5 R= 1e+05
Depth= 409 States= 7e+06 Transitions= 1.49e+07 Memory= 2403.827 t= 49.8 R= 1e+05
Depth= 409 States= 8e+06 Transitions= 1.7e+07 Memory= 2728.730 t= 59.3 R= 1e+05
Depth= 409 States= 9e+06 Transitions= 1.91e+07 Memory= 3053.827 t= 70.7 R= 1e+05
Depth= 409 States= 1e+07 Transitions= 2.13e+07 Memory= 3378.925 t= 82.2 R= 1e+05
Depth= 409 States= 1.1e+07 Transitions= 2.34e+07 Memory= 3703.827 t= 98.2 R= 1e+05
Depth= 409 States= 1.2e+07 Transitions= 2.55e+07 Memory= 4028.925 t= 115 R= 1e+05
Depth= 409 States= 1.3e+07 Transitions= 2.76e+07 Memory= 4353.925 t= 136 R= 1e+05
Depth= 409 States= 1.4e+07 Transitions= 2.98e+07 Memory= 4678.925 t= 154 R= 9e+04
Depth= 409 States= 1.5e+07 Transitions= 3.19e+07 Memory= 5004.022 t= 167 R= 9e+04
Depth= 409 States= 1.6e+07 Transitions= 3.4e+07 Memory= 5328.925 t= 184 R= 9e+04
Depth= 409 States= 1.7e+07 Transitions= 3.61e+07 Memory= 5654.022 t= 214 R= 8e+04
Depth= 409 States= 1.8e+07 Transitions= 3.83e+07 Memory= 5979.022 t= 248 R= 7e+04
Depth= 409 States= 1.9e+07 Transitions= 4.04e+07 Memory= 6304.022 t= 289 R= 7e+04

20
ReversalModel/outputs/trace_seq_eq_parallel_10_6_2.txt Normal file
View File

@ -0,0 +1,20 @@
pan: ltl formula seq_eq_parallel
Depth= 409 States= 1e+06 Transitions= 2.12e+06 Memory= 453.632 t= 5.78 R= 2e+05
Depth= 409 States= 2e+06 Transitions= 4.25e+06 Memory= 778.730 t= 11.7 R= 2e+05
Depth= 409 States= 3e+06 Transitions= 6.38e+06 Memory= 1103.632 t= 18.8 R= 2e+05
Depth= 409 States= 4e+06 Transitions= 8.5e+06 Memory= 1428.730 t= 27 R= 1e+05
Depth= 409 States= 5e+06 Transitions= 1.06e+07 Memory= 1753.730 t= 33 R= 2e+05
Depth= 409 States= 6e+06 Transitions= 1.28e+07 Memory= 2078.730 t= 38.8 R= 2e+05
Depth= 409 States= 7e+06 Transitions= 1.49e+07 Memory= 2403.730 t= 46.1 R= 2e+05
Depth= 409 States= 8e+06 Transitions= 1.7e+07 Memory= 2728.730 t= 54 R= 1e+05
Depth= 409 States= 9e+06 Transitions= 1.91e+07 Memory= 3053.730 t= 63 R= 1e+05
Depth= 409 States= 1e+07 Transitions= 2.13e+07 Memory= 3378.827 t= 75.3 R= 1e+05
Depth= 409 States= 1.1e+07 Transitions= 2.34e+07 Memory= 3703.730 t= 88.8 R= 1e+05
Depth= 409 States= 1.2e+07 Transitions= 2.55e+07 Memory= 4028.827 t= 107 R= 1e+05
Depth= 409 States= 1.3e+07 Transitions= 2.76e+07 Memory= 4353.827 t= 124 R= 1e+05
Depth= 409 States= 1.4e+07 Transitions= 2.98e+07 Memory= 4678.827 t= 143 R= 1e+05
Depth= 409 States= 1.5e+07 Transitions= 3.19e+07 Memory= 5003.925 t= 159 R= 9e+04
Depth= 409 States= 1.6e+07 Transitions= 3.4e+07 Memory= 5328.827 t= 174 R= 9e+04
Depth= 409 States= 1.7e+07 Transitions= 3.61e+07 Memory= 5653.925 t= 197 R= 9e+04
Depth= 409 States= 1.8e+07 Transitions= 3.83e+07 Memory= 5978.925 t= 224 R= 8e+04
Depth= 409 States= 1.9e+07 Transitions= 4.04e+07 Memory= 6303.925 t= 260 R= 7e+04

20
ReversalModel/outputs/trace_seq_eq_parallel_10_6_3.txt Normal file
View File

@ -0,0 +1,20 @@
pan: ltl formula seq_eq_parallel
Depth= 409 States= 1e+06 Transitions= 2.12e+06 Memory= 453.632 t= 5.2 R= 2e+05
Depth= 409 States= 2e+06 Transitions= 4.25e+06 Memory= 778.730 t= 10.2 R= 2e+05
Depth= 409 States= 3e+06 Transitions= 6.38e+06 Memory= 1103.632 t= 16.2 R= 2e+05
Depth= 409 States= 4e+06 Transitions= 8.5e+06 Memory= 1428.730 t= 22.2 R= 2e+05
Depth= 409 States= 5e+06 Transitions= 1.06e+07 Memory= 1753.730 t= 29 R= 2e+05
Depth= 409 States= 6e+06 Transitions= 1.28e+07 Memory= 2078.730 t= 37.1 R= 2e+05
Depth= 409 States= 7e+06 Transitions= 1.49e+07 Memory= 2403.827 t= 46.5 R= 2e+05
Depth= 409 States= 8e+06 Transitions= 1.7e+07 Memory= 2728.730 t= 57 R= 1e+05
Depth= 409 States= 9e+06 Transitions= 1.91e+07 Memory= 3053.827 t= 70.9 R= 1e+05
Depth= 409 States= 1e+07 Transitions= 2.13e+07 Memory= 3378.827 t= 85.7 R= 1e+05
Depth= 409 States= 1.1e+07 Transitions= 2.34e+07 Memory= 3703.827 t= 101 R= 1e+05
Depth= 409 States= 1.2e+07 Transitions= 2.55e+07 Memory= 4028.827 t= 118 R= 1e+05
Depth= 409 States= 1.3e+07 Transitions= 2.76e+07 Memory= 4353.827 t= 131 R= 1e+05
Depth= 409 States= 1.4e+07 Transitions= 2.98e+07 Memory= 4678.925 t= 142 R= 1e+05
Depth= 409 States= 1.5e+07 Transitions= 3.19e+07 Memory= 5003.925 t= 157 R= 1e+05
Depth= 409 States= 1.6e+07 Transitions= 3.4e+07 Memory= 5328.925 t= 178 R= 9e+04
Depth= 409 States= 1.7e+07 Transitions= 3.61e+07 Memory= 5653.925 t= 201 R= 8e+04
Depth= 409 States= 1.8e+07 Transitions= 3.83e+07 Memory= 5978.925 t= 234 R= 8e+04
Depth= 409 States= 1.9e+07 Transitions= 4.04e+07 Memory= 6304.022 t= 274 R= 7e+04

21
ReversalModel/outputs/trace_seq_eq_parallel_10_6_4.txt Normal file
View File

@ -0,0 +1,21 @@
pan: ltl formula seq_eq_parallel
Depth= 409 States= 1e+06 Transitions= 2.12e+06 Memory= 453.632 t= 4.7 R= 2e+05
Depth= 409 States= 2e+06 Transitions= 4.25e+06 Memory= 778.730 t= 9.48 R= 2e+05
Depth= 409 States= 3e+06 Transitions= 6.38e+06 Memory= 1103.632 t= 14.4 R= 2e+05
Depth= 409 States= 4e+06 Transitions= 8.5e+06 Memory= 1428.730 t= 19.9 R= 2e+05
Depth= 409 States= 5e+06 Transitions= 1.06e+07 Memory= 1753.730 t= 25.6 R= 2e+05
Depth= 409 States= 6e+06 Transitions= 1.28e+07 Memory= 2078.730 t= 33.6 R= 2e+05
Depth= 409 States= 7e+06 Transitions= 1.49e+07 Memory= 2403.827 t= 41.9 R= 2e+05
Depth= 409 States= 8e+06 Transitions= 1.7e+07 Memory= 2728.730 t= 49.7 R= 2e+05
Depth= 409 States= 9e+06 Transitions= 1.91e+07 Memory= 3053.827 t= 59.8 R= 2e+05
Depth= 409 States= 1e+07 Transitions= 2.13e+07 Memory= 3378.827 t= 71.5 R= 1e+05
Depth= 409 States= 1.1e+07 Transitions= 2.34e+07 Memory= 3703.827 t= 86 R= 1e+05
Depth= 409 States= 1.2e+07 Transitions= 2.55e+07 Memory= 4028.925 t= 103 R= 1e+05
Depth= 409 States= 1.3e+07 Transitions= 2.76e+07 Memory= 4353.827 t= 122 R= 1e+05
Depth= 409 States= 1.4e+07 Transitions= 2.98e+07 Memory= 4678.925 t= 146 R= 1e+05
Depth= 409 States= 1.5e+07 Transitions= 3.19e+07 Memory= 5003.925 t= 164 R= 9e+04
Depth= 409 States= 1.6e+07 Transitions= 3.4e+07 Memory= 5328.925 t= 182 R= 9e+04
Depth= 409 States= 1.7e+07 Transitions= 3.61e+07 Memory= 5654.022 t= 205 R= 8e+04
Depth= 409 States= 1.8e+07 Transitions= 3.83e+07 Memory= 5978.925 t= 237 R= 8e+04
Depth= 409 States= 1.9e+07 Transitions= 4.04e+07 Memory= 6304.022 t= 264 R= 7e+04
Depth= 409 States= 2e+07 Transitions= 4.25e+07 Memory= 6629.022 t= 298 R= 7e+04

21
ReversalModel/outputs/trace_seq_eq_parallel_10_6_5.txt Normal file
View File

@ -0,0 +1,21 @@
pan: ltl formula seq_eq_parallel
Depth= 409 States= 1e+06 Transitions= 2.12e+06 Memory= 453.632 t= 4.9 R= 2e+05
Depth= 409 States= 2e+06 Transitions= 4.25e+06 Memory= 778.730 t= 9.87 R= 2e+05
Depth= 409 States= 3e+06 Transitions= 6.38e+06 Memory= 1103.632 t= 15.4 R= 2e+05
Depth= 409 States= 4e+06 Transitions= 8.5e+06 Memory= 1428.730 t= 21 R= 2e+05
Depth= 409 States= 5e+06 Transitions= 1.06e+07 Memory= 1753.827 t= 28.9 R= 2e+05
Depth= 409 States= 6e+06 Transitions= 1.28e+07 Memory= 2078.730 t= 36.4 R= 2e+05
Depth= 409 States= 7e+06 Transitions= 1.49e+07 Memory= 2403.827 t= 43.6 R= 2e+05
Depth= 409 States= 8e+06 Transitions= 1.7e+07 Memory= 2728.730 t= 52.9 R= 2e+05
Depth= 409 States= 9e+06 Transitions= 1.91e+07 Memory= 3053.827 t= 63.8 R= 1e+05
Depth= 409 States= 1e+07 Transitions= 2.13e+07 Memory= 3378.925 t= 76.9 R= 1e+05
Depth= 409 States= 1.1e+07 Transitions= 2.34e+07 Memory= 3703.827 t= 93 R= 1e+05
Depth= 409 States= 1.2e+07 Transitions= 2.55e+07 Memory= 4028.925 t= 110 R= 1e+05
Depth= 409 States= 1.3e+07 Transitions= 2.76e+07 Memory= 4353.827 t= 130 R= 1e+05
Depth= 409 States= 1.4e+07 Transitions= 2.98e+07 Memory= 4678.925 t= 151 R= 9e+04
Depth= 409 States= 1.5e+07 Transitions= 3.19e+07 Memory= 5004.022 t= 169 R= 9e+04
Depth= 409 States= 1.6e+07 Transitions= 3.4e+07 Memory= 5328.925 t= 186 R= 9e+04
Depth= 409 States= 1.7e+07 Transitions= 3.61e+07 Memory= 5654.022 t= 210 R= 8e+04
Depth= 409 States= 1.8e+07 Transitions= 3.83e+07 Memory= 5979.022 t= 240 R= 8e+04
Depth= 409 States= 1.9e+07 Transitions= 4.04e+07 Memory= 6304.022 t= 267 R= 7e+04
Depth= 409 States= 2e+07 Transitions= 4.25e+07 Memory= 6629.120 t= 298 R= 7e+04

21
ReversalModel/outputs/trace_seq_eq_parallel_10_6_6.txt Normal file
View File

@ -0,0 +1,21 @@
pan: ltl formula seq_eq_parallel
Depth= 409 States= 1e+06 Transitions= 2.12e+06 Memory= 453.632 t= 5.78 R= 2e+05
Depth= 409 States= 2e+06 Transitions= 4.25e+06 Memory= 778.730 t= 11.9 R= 2e+05
Depth= 409 States= 3e+06 Transitions= 6.38e+06 Memory= 1103.632 t= 18.6 R= 2e+05
Depth= 409 States= 4e+06 Transitions= 8.5e+06 Memory= 1428.730 t= 25.8 R= 2e+05
Depth= 409 States= 5e+06 Transitions= 1.06e+07 Memory= 1753.827 t= 31.1 R= 2e+05
Depth= 409 States= 6e+06 Transitions= 1.28e+07 Memory= 2078.730 t= 37.3 R= 2e+05
Depth= 409 States= 7e+06 Transitions= 1.49e+07 Memory= 2403.827 t= 45.3 R= 2e+05
Depth= 409 States= 8e+06 Transitions= 1.7e+07 Memory= 2728.730 t= 53.3 R= 2e+05
Depth= 409 States= 9e+06 Transitions= 1.91e+07 Memory= 3053.827 t= 64.1 R= 1e+05
Depth= 409 States= 1e+07 Transitions= 2.13e+07 Memory= 3378.925 t= 78.6 R= 1e+05
Depth= 409 States= 1.1e+07 Transitions= 2.34e+07 Memory= 3703.827 t= 92.9 R= 1e+05
Depth= 409 States= 1.2e+07 Transitions= 2.55e+07 Memory= 4028.925 t= 106 R= 1e+05
Depth= 409 States= 1.3e+07 Transitions= 2.76e+07 Memory= 4353.827 t= 120 R= 1e+05
Depth= 409 States= 1.4e+07 Transitions= 2.98e+07 Memory= 4678.925 t= 136 R= 1e+05
Depth= 409 States= 1.5e+07 Transitions= 3.19e+07 Memory= 5004.022 t= 153 R= 1e+05
Depth= 409 States= 1.6e+07 Transitions= 3.4e+07 Memory= 5328.925 t= 165 R= 1e+05
Depth= 409 States= 1.7e+07 Transitions= 3.61e+07 Memory= 5654.022 t= 175 R= 1e+05
Depth= 409 States= 1.8e+07 Transitions= 3.83e+07 Memory= 5979.022 t= 194 R= 9e+04
Depth= 409 States= 1.9e+07 Transitions= 4.04e+07 Memory= 6304.022 t= 219 R= 9e+04
Depth= 409 States= 2e+07 Transitions= 4.25e+07 Memory= 6629.120 t= 259 R= 8e+04

21
ReversalModel/outputs/trace_seq_eq_parallel_10_6_7.txt Normal file
View File

@ -0,0 +1,21 @@
pan: ltl formula seq_eq_parallel
Depth= 409 States= 1e+06 Transitions= 2.12e+06 Memory= 453.632 t= 4.63 R= 2e+05
Depth= 409 States= 2e+06 Transitions= 4.25e+06 Memory= 778.730 t= 9.7 R= 2e+05
Depth= 409 States= 3e+06 Transitions= 6.38e+06 Memory= 1103.632 t= 16 R= 2e+05
Depth= 409 States= 4e+06 Transitions= 8.5e+06 Memory= 1428.730 t= 21.9 R= 2e+05
Depth= 409 States= 5e+06 Transitions= 1.06e+07 Memory= 1753.827 t= 28.6 R= 2e+05
Depth= 409 States= 6e+06 Transitions= 1.28e+07 Memory= 2078.730 t= 37.3 R= 2e+05
Depth= 409 States= 7e+06 Transitions= 1.49e+07 Memory= 2403.827 t= 48.1 R= 1e+05
Depth= 409 States= 8e+06 Transitions= 1.7e+07 Memory= 2728.730 t= 61.3 R= 1e+05
Depth= 409 States= 9e+06 Transitions= 1.91e+07 Memory= 3053.827 t= 71.7 R= 1e+05
Depth= 409 States= 1e+07 Transitions= 2.13e+07 Memory= 3378.925 t= 83 R= 1e+05
Depth= 409 States= 1.1e+07 Transitions= 2.34e+07 Memory= 3703.827 t= 95.9 R= 1e+05
Depth= 409 States= 1.2e+07 Transitions= 2.55e+07 Memory= 4028.925 t= 110 R= 1e+05
Depth= 409 States= 1.3e+07 Transitions= 2.76e+07 Memory= 4353.827 t= 126 R= 1e+05
Depth= 409 States= 1.4e+07 Transitions= 2.98e+07 Memory= 4678.925 t= 135 R= 1e+05
Depth= 409 States= 1.5e+07 Transitions= 3.19e+07 Memory= 5004.022 t= 143 R= 1e+05
Depth= 409 States= 1.6e+07 Transitions= 3.4e+07 Memory= 5328.925 t= 153 R= 1e+05
Depth= 409 States= 1.7e+07 Transitions= 3.61e+07 Memory= 5654.022 t= 170 R= 1e+05
Depth= 409 States= 1.8e+07 Transitions= 3.83e+07 Memory= 5979.022 t= 191 R= 9e+04
Depth= 409 States= 1.9e+07 Transitions= 4.04e+07 Memory= 6304.022 t= 222 R= 9e+04
Depth= 409 States= 2e+07 Transitions= 4.25e+07 Memory= 6629.120 t= 270 R= 7e+04

20
ReversalModel/outputs/trace_seq_eq_parallel_10_6_8.txt Normal file
View File

@ -0,0 +1,20 @@
pan: ltl formula seq_eq_parallel
Depth= 409 States= 1e+06 Transitions= 2.12e+06 Memory= 453.632 t= 4.81 R= 2e+05
Depth= 409 States= 2e+06 Transitions= 4.25e+06 Memory= 778.730 t= 9.01 R= 2e+05
Depth= 409 States= 3e+06 Transitions= 6.38e+06 Memory= 1103.632 t= 12.9 R= 2e+05
Depth= 409 States= 4e+06 Transitions= 8.5e+06 Memory= 1428.730 t= 17.2 R= 2e+05
Depth= 409 States= 5e+06 Transitions= 1.06e+07 Memory= 1753.827 t= 22 R= 2e+05
Depth= 409 States= 6e+06 Transitions= 1.28e+07 Memory= 2078.730 t= 26.8 R= 2e+05
Depth= 409 States= 7e+06 Transitions= 1.49e+07 Memory= 2403.827 t= 32.8 R= 2e+05
Depth= 409 States= 8e+06 Transitions= 1.7e+07 Memory= 2728.730 t= 39.6 R= 2e+05
Depth= 409 States= 9e+06 Transitions= 1.91e+07 Memory= 3053.827 t= 47.4 R= 2e+05
Depth= 409 States= 1e+07 Transitions= 2.13e+07 Memory= 3378.925 t= 56.6 R= 2e+05
Depth= 409 States= 1.1e+07 Transitions= 2.34e+07 Memory= 3703.827 t= 67.8 R= 2e+05
Depth= 409 States= 1.2e+07 Transitions= 2.55e+07 Memory= 4028.925 t= 84.1 R= 1e+05
Depth= 409 States= 1.3e+07 Transitions= 2.76e+07 Memory= 4353.827 t= 105 R= 1e+05
Depth= 409 States= 1.4e+07 Transitions= 2.98e+07 Memory= 4678.925 t= 128 R= 1e+05
Depth= 409 States= 1.5e+07 Transitions= 3.19e+07 Memory= 5004.022 t= 153 R= 1e+05
Depth= 409 States= 1.6e+07 Transitions= 3.4e+07 Memory= 5328.925 t= 175 R= 9e+04
Depth= 409 States= 1.7e+07 Transitions= 3.61e+07 Memory= 5654.022 t= 197 R= 9e+04
Depth= 409 States= 1.8e+07 Transitions= 3.83e+07 Memory= 5979.022 t= 225 R= 8e+04
Depth= 409 States= 1.9e+07 Transitions= 4.04e+07 Memory= 6304.022 t= 258 R= 7e+04

20
ReversalModel/outputs/trace_seq_eq_parallel_10_6_9.txt Normal file
View File

@ -0,0 +1,20 @@
pan: ltl formula seq_eq_parallel
Depth= 409 States= 1e+06 Transitions= 2.12e+06 Memory= 453.632 t= 4 R= 2e+05
Depth= 409 States= 2e+06 Transitions= 4.25e+06 Memory= 778.730 t= 7.81 R= 3e+05
Depth= 409 States= 3e+06 Transitions= 6.38e+06 Memory= 1103.632 t= 12.1 R= 2e+05
Depth= 409 States= 4e+06 Transitions= 8.5e+06 Memory= 1428.730 t= 16.8 R= 2e+05
Depth= 409 States= 5e+06 Transitions= 1.06e+07 Memory= 1753.827 t= 21.5 R= 2e+05
Depth= 409 States= 6e+06 Transitions= 1.28e+07 Memory= 2078.730 t= 27 R= 2e+05
Depth= 409 States= 7e+06 Transitions= 1.49e+07 Memory= 2403.827 t= 33.3 R= 2e+05
Depth= 409 States= 8e+06 Transitions= 1.7e+07 Memory= 2728.730 t= 40.5 R= 2e+05
Depth= 409 States= 9e+06 Transitions= 1.91e+07 Memory= 3053.827 t= 48.7 R= 2e+05
Depth= 409 States= 1e+07 Transitions= 2.13e+07 Memory= 3378.925 t= 58.3 R= 2e+05
Depth= 409 States= 1.1e+07 Transitions= 2.34e+07 Memory= 3703.827 t= 72.7 R= 2e+05
Depth= 409 States= 1.2e+07 Transitions= 2.55e+07 Memory= 4028.925 t= 89.7 R= 1e+05
Depth= 409 States= 1.3e+07 Transitions= 2.76e+07 Memory= 4353.925 t= 111 R= 1e+05
Depth= 409 States= 1.4e+07 Transitions= 2.98e+07 Memory= 4678.925 t= 137 R= 1e+05
Depth= 409 States= 1.5e+07 Transitions= 3.19e+07 Memory= 5004.022 t= 156 R= 1e+05
Depth= 409 States= 1.6e+07 Transitions= 3.4e+07 Memory= 5328.925 t= 177 R= 9e+04
Depth= 409 States= 1.7e+07 Transitions= 3.61e+07 Memory= 5654.022 t= 200 R= 9e+04
Depth= 409 States= 1.8e+07 Transitions= 3.83e+07 Memory= 5979.022 t= 227 R= 8e+04
Depth= 409 States= 1.9e+07 Transitions= 4.04e+07 Memory= 6304.022 t= 261 R= 7e+04

20
ReversalModel/outputs/trace_seq_eq_parallel_10_7_10.txt Normal file
View File

@ -0,0 +1,20 @@
pan: ltl formula seq_eq_parallel
Depth= 429 States= 1e+06 Transitions= 2.12e+06 Memory= 468.964 t= 5.23 R= 2e+05
Depth= 429 States= 2e+06 Transitions= 4.25e+06 Memory= 809.198 t= 11.2 R= 2e+05
Depth= 429 States= 3e+06 Transitions= 6.38e+06 Memory= 1149.433 t= 16.7 R= 2e+05
Depth= 429 States= 4e+06 Transitions= 8.5e+06 Memory= 1489.667 t= 23 R= 2e+05
Depth= 429 States= 5e+06 Transitions= 1.06e+07 Memory= 1829.999 t= 30.1 R= 2e+05
Depth= 429 States= 6e+06 Transitions= 1.28e+07 Memory= 2170.331 t= 37.6 R= 2e+05
Depth= 429 States= 7e+06 Transitions= 1.49e+07 Memory= 2510.565 t= 47.2 R= 1e+05
Depth= 429 States= 8e+06 Transitions= 1.7e+07 Memory= 2850.897 t= 57.6 R= 1e+05
Depth= 429 States= 9e+06 Transitions= 1.91e+07 Memory= 3191.132 t= 69.6 R= 1e+05
Depth= 429 States= 1e+07 Transitions= 2.13e+07 Memory= 3531.366 t= 83 R= 1e+05
Depth= 429 States= 1.1e+07 Transitions= 2.34e+07 Memory= 3871.796 t= 99.2 R= 1e+05
Depth= 429 States= 1.2e+07 Transitions= 2.55e+07 Memory= 4212.030 t= 117 R= 1e+05
Depth= 429 States= 1.3e+07 Transitions= 2.76e+07 Memory= 4552.265 t= 133 R= 1e+05
Depth= 429 States= 1.4e+07 Transitions= 2.98e+07 Memory= 4892.499 t= 145 R= 1e+05
Depth= 429 States= 1.5e+07 Transitions= 3.19e+07 Memory= 5232.831 t= 163 R= 9e+04
Depth= 429 States= 1.6e+07 Transitions= 3.4e+07 Memory= 5573.065 t= 191 R= 8e+04
Depth= 429 States= 1.7e+07 Transitions= 3.61e+07 Memory= 5913.397 t= 212 R= 8e+04
Depth= 429 States= 1.8e+07 Transitions= 3.83e+07 Memory= 6253.730 t= 245 R= 7e+04
Depth= 429 States= 1.9e+07 Transitions= 4.04e+07 Memory= 6593.964 t= 279 R= 7e+04

19
ReversalModel/outputs/trace_seq_eq_parallel_10_7_2.txt Normal file
View File

@ -0,0 +1,19 @@
pan: ltl formula seq_eq_parallel
Depth= 429 States= 1e+06 Transitions= 2.12e+06 Memory= 468.964 t= 5.31 R= 2e+05
Depth= 429 States= 2e+06 Transitions= 4.25e+06 Memory= 809.198 t= 11.6 R= 2e+05
Depth= 429 States= 3e+06 Transitions= 6.38e+06 Memory= 1149.433 t= 17.7 R= 2e+05
Depth= 429 States= 4e+06 Transitions= 8.5e+06 Memory= 1489.667 t= 24.1 R= 2e+05
Depth= 429 States= 5e+06 Transitions= 1.06e+07 Memory= 1829.901 t= 31.6 R= 2e+05
Depth= 429 States= 6e+06 Transitions= 1.28e+07 Memory= 2170.331 t= 41.1 R= 1e+05
Depth= 429 States= 7e+06 Transitions= 1.49e+07 Memory= 2510.565 t= 51 R= 1e+05
Depth= 429 States= 8e+06 Transitions= 1.7e+07 Memory= 2850.800 t= 63.3 R= 1e+05
Depth= 429 States= 9e+06 Transitions= 1.91e+07 Memory= 3191.034 t= 77.9 R= 1e+05
Depth= 429 States= 1e+07 Transitions= 2.13e+07 Memory= 3531.269 t= 94.2 R= 1e+05
Depth= 429 States= 1.1e+07 Transitions= 2.34e+07 Memory= 3871.698 t= 113 R= 1e+05
Depth= 429 States= 1.2e+07 Transitions= 2.55e+07 Memory= 4211.933 t= 129 R= 9e+04
Depth= 429 States= 1.3e+07 Transitions= 2.76e+07 Memory= 4552.167 t= 139 R= 9e+04
Depth= 429 States= 1.4e+07 Transitions= 2.98e+07 Memory= 4892.401 t= 153 R= 9e+04
Depth= 429 States= 1.5e+07 Transitions= 3.19e+07 Memory= 5232.733 t= 174 R= 9e+04
Depth= 429 States= 1.6e+07 Transitions= 3.4e+07 Memory= 5572.968 t= 204 R= 8e+04
Depth= 429 States= 1.7e+07 Transitions= 3.61e+07 Memory= 5913.300 t= 238 R= 7e+04
Depth= 429 States= 1.8e+07 Transitions= 3.83e+07 Memory= 6253.534 t= 278 R= 6e+04

19
ReversalModel/outputs/trace_seq_eq_parallel_10_7_3.txt Normal file
View File

@ -0,0 +1,19 @@
pan: ltl formula seq_eq_parallel
Depth= 429 States= 1e+06 Transitions= 2.12e+06 Memory= 468.964 t= 4.68 R= 2e+05
Depth= 429 States= 2e+06 Transitions= 4.25e+06 Memory= 809.198 t= 9.17 R= 2e+05
Depth= 429 States= 3e+06 Transitions= 6.38e+06 Memory= 1149.433 t= 14.3 R= 2e+05
Depth= 429 States= 4e+06 Transitions= 8.5e+06 Memory= 1489.667 t= 19.9 R= 2e+05
Depth= 429 States= 5e+06 Transitions= 1.06e+07 Memory= 1829.901 t= 26.6 R= 2e+05
Depth= 429 States= 6e+06 Transitions= 1.28e+07 Memory= 2170.331 t= 34 R= 2e+05
Depth= 429 States= 7e+06 Transitions= 1.49e+07 Memory= 2510.565 t= 42.6 R= 2e+05
Depth= 429 States= 8e+06 Transitions= 1.7e+07 Memory= 2850.800 t= 58 R= 1e+05
Depth= 429 States= 9e+06 Transitions= 1.91e+07 Memory= 3191.132 t= 74.3 R= 1e+05
Depth= 429 States= 1e+07 Transitions= 2.13e+07 Memory= 3531.366 t= 89 R= 1e+05
Depth= 429 States= 1.1e+07 Transitions= 2.34e+07 Memory= 3871.698 t= 107 R= 1e+05
Depth= 429 States= 1.2e+07 Transitions= 2.55e+07 Memory= 4211.933 t= 127 R= 9e+04
Depth= 429 States= 1.3e+07 Transitions= 2.76e+07 Memory= 4552.265 t= 151 R= 9e+04
Depth= 429 States= 1.4e+07 Transitions= 2.98e+07 Memory= 4892.499 t= 167 R= 8e+04
Depth= 429 States= 1.5e+07 Transitions= 3.19e+07 Memory= 5232.733 t= 184 R= 8e+04
Depth= 429 States= 1.6e+07 Transitions= 3.4e+07 Memory= 5572.968 t= 205 R= 8e+04
Depth= 429 States= 1.7e+07 Transitions= 3.61e+07 Memory= 5913.397 t= 233 R= 7e+04
Depth= 429 States= 1.8e+07 Transitions= 3.83e+07 Memory= 6253.632 t= 266 R= 7e+04

19
ReversalModel/outputs/trace_seq_eq_parallel_10_7_4.txt Normal file
View File

@ -0,0 +1,19 @@
pan: ltl formula seq_eq_parallel
Depth= 429 States= 1e+06 Transitions= 2.12e+06 Memory= 468.964 t= 4.56 R= 2e+05
Depth= 429 States= 2e+06 Transitions= 4.25e+06 Memory= 809.198 t= 9.45 R= 2e+05
Depth= 429 States= 3e+06 Transitions= 6.38e+06 Memory= 1149.433 t= 14.9 R= 2e+05
Depth= 429 States= 4e+06 Transitions= 8.5e+06 Memory= 1489.667 t= 21.4 R= 2e+05
Depth= 429 States= 5e+06 Transitions= 1.06e+07 Memory= 1829.999 t= 28.1 R= 2e+05
Depth= 429 States= 6e+06 Transitions= 1.28e+07 Memory= 2170.331 t= 35.7 R= 2e+05
Depth= 429 States= 7e+06 Transitions= 1.49e+07 Memory= 2510.565 t= 49.5 R= 1e+05
Depth= 429 States= 8e+06 Transitions= 1.7e+07 Memory= 2850.800 t= 64 R= 1e+05
Depth= 429 States= 9e+06 Transitions= 1.91e+07 Memory= 3191.132 t= 77.6 R= 1e+05
Depth= 429 States= 1e+07 Transitions= 2.13e+07 Memory= 3531.366 t= 93.7 R= 1e+05
Depth= 429 States= 1.1e+07 Transitions= 2.34e+07 Memory= 3871.698 t= 113 R= 1e+05
Depth= 429 States= 1.2e+07 Transitions= 2.55e+07 Memory= 4212.030 t= 133 R= 9e+04
Depth= 429 States= 1.3e+07 Transitions= 2.76e+07 Memory= 4552.265 t= 152 R= 9e+04
Depth= 429 States= 1.4e+07 Transitions= 2.98e+07 Memory= 4892.499 t= 169 R= 8e+04
Depth= 429 States= 1.5e+07 Transitions= 3.19e+07 Memory= 5232.733 t= 184 R= 8e+04
Depth= 429 States= 1.6e+07 Transitions= 3.4e+07 Memory= 5572.968 t= 205 R= 8e+04
Depth= 429 States= 1.7e+07 Transitions= 3.61e+07 Memory= 5913.397 t= 233 R= 7e+04
Depth= 429 States= 1.8e+07 Transitions= 3.83e+07 Memory= 6253.632 t= 265 R= 7e+04

19
ReversalModel/outputs/trace_seq_eq_parallel_10_7_5.txt Normal file
View File

@ -0,0 +1,19 @@
pan: ltl formula seq_eq_parallel
Depth= 429 States= 1e+06 Transitions= 2.12e+06 Memory= 468.964 t= 5.26 R= 2e+05
Depth= 429 States= 2e+06 Transitions= 4.25e+06 Memory= 809.198 t= 11.3 R= 2e+05
Depth= 429 States= 3e+06 Transitions= 6.38e+06 Memory= 1149.433 t= 17.5 R= 2e+05
Depth= 429 States= 4e+06 Transitions= 8.5e+06 Memory= 1489.667 t= 24.7 R= 2e+05
Depth= 429 States= 5e+06 Transitions= 1.06e+07 Memory= 1829.999 t= 30.9 R= 2e+05
Depth= 429 States= 6e+06 Transitions= 1.28e+07 Memory= 2170.331 t= 36.6 R= 2e+05
Depth= 429 States= 7e+06 Transitions= 1.49e+07 Memory= 2510.565 t= 43.8 R= 2e+05
Depth= 429 States= 8e+06 Transitions= 1.7e+07 Memory= 2850.897 t= 52.8 R= 2e+05
Depth= 429 States= 9e+06 Transitions= 1.91e+07 Memory= 3191.132 t= 63.2 R= 1e+05
Depth= 429 States= 1e+07 Transitions= 2.13e+07 Memory= 3531.366 t= 76 R= 1e+05
Depth= 429 States= 1.1e+07 Transitions= 2.34e+07 Memory= 3871.796 t= 90.4 R= 1e+05
Depth= 429 States= 1.2e+07 Transitions= 2.55e+07 Memory= 4212.030 t= 107 R= 1e+05
Depth= 429 States= 1.3e+07 Transitions= 2.76e+07 Memory= 4552.265 t= 127 R= 1e+05
Depth= 429 States= 1.4e+07 Transitions= 2.98e+07 Memory= 4892.499 t= 151 R= 9e+04
Depth= 429 States= 1.5e+07 Transitions= 3.19e+07 Memory= 5232.733 t= 169 R= 9e+04
Depth= 429 States= 1.6e+07 Transitions= 3.4e+07 Memory= 5573.065 t= 195 R= 8e+04
Depth= 429 States= 1.7e+07 Transitions= 3.61e+07 Memory= 5913.397 t= 231 R= 7e+04
Depth= 429 States= 1.8e+07 Transitions= 3.83e+07 Memory= 6253.632 t= 266 R= 7e+04

19
ReversalModel/outputs/trace_seq_eq_parallel_10_7_6.txt Normal file
View File

@ -0,0 +1,19 @@
pan: ltl formula seq_eq_parallel
Depth= 429 States= 1e+06 Transitions= 2.12e+06 Memory= 468.964 t= 5.18 R= 2e+05
Depth= 429 States= 2e+06 Transitions= 4.25e+06 Memory= 809.198 t= 10.1 R= 2e+05
Depth= 429 States= 3e+06 Transitions= 6.38e+06 Memory= 1149.433 t= 15.8 R= 2e+05
Depth= 429 States= 4e+06 Transitions= 8.5e+06 Memory= 1489.667 t= 22 R= 2e+05
Depth= 429 States= 5e+06 Transitions= 1.06e+07 Memory= 1829.999 t= 29.1 R= 2e+05
Depth= 429 States= 6e+06 Transitions= 1.28e+07 Memory= 2170.331 t= 37.5 R= 2e+05
Depth= 429 States= 7e+06 Transitions= 1.49e+07 Memory= 2510.565 t= 47.8 R= 1e+05
Depth= 429 States= 8e+06 Transitions= 1.7e+07 Memory= 2850.897 t= 59.7 R= 1e+05
Depth= 429 States= 9e+06 Transitions= 1.91e+07 Memory= 3191.132 t= 71.5 R= 1e+05
Depth= 429 States= 1e+07 Transitions= 2.13e+07 Memory= 3531.366 t= 88.1 R= 1e+05
Depth= 429 States= 1.1e+07 Transitions= 2.34e+07 Memory= 3871.796 t= 106 R= 1e+05
Depth= 429 States= 1.2e+07 Transitions= 2.55e+07 Memory= 4212.030 t= 126 R= 1e+05
Depth= 429 States= 1.3e+07 Transitions= 2.76e+07 Memory= 4552.265 t= 140 R= 9e+04
Depth= 429 States= 1.4e+07 Transitions= 2.98e+07 Memory= 4892.499 t= 156 R= 9e+04
Depth= 429 States= 1.5e+07 Transitions= 3.19e+07 Memory= 5232.831 t= 182 R= 8e+04
Depth= 429 States= 1.6e+07 Transitions= 3.4e+07 Memory= 5573.065 t= 210 R= 8e+04
Depth= 429 States= 1.7e+07 Transitions= 3.61e+07 Memory= 5913.397 t= 239 R= 7e+04
Depth= 429 States= 1.8e+07 Transitions= 3.83e+07 Memory= 6253.632 t= 275 R= 7e+04

20
ReversalModel/outputs/trace_seq_eq_parallel_10_7_7.txt Normal file
View File

@ -0,0 +1,20 @@
pan: ltl formula seq_eq_parallel
Depth= 429 States= 1e+06 Transitions= 2.12e+06 Memory= 468.964 t= 5.86 R= 2e+05
Depth= 429 States= 2e+06 Transitions= 4.25e+06 Memory= 809.198 t= 11.2 R= 2e+05
Depth= 429 States= 3e+06 Transitions= 6.38e+06 Memory= 1149.433 t= 17.4 R= 2e+05
Depth= 429 States= 4e+06 Transitions= 8.5e+06 Memory= 1489.667 t= 23.5 R= 2e+05
Depth= 429 States= 5e+06 Transitions= 1.06e+07 Memory= 1829.999 t= 31.1 R= 2e+05
Depth= 429 States= 6e+06 Transitions= 1.28e+07 Memory= 2170.331 t= 41 R= 1e+05
Depth= 429 States= 7e+06 Transitions= 1.49e+07 Memory= 2510.565 t= 51.2 R= 1e+05
Depth= 429 States= 8e+06 Transitions= 1.7e+07 Memory= 2850.897 t= 64.1 R= 1e+05
Depth= 429 States= 9e+06 Transitions= 1.91e+07 Memory= 3191.132 t= 77.5 R= 1e+05
Depth= 429 States= 1e+07 Transitions= 2.13e+07 Memory= 3531.366 t= 92.7 R= 1e+05
Depth= 429 States= 1.1e+07 Transitions= 2.34e+07 Memory= 3871.796 t= 108 R= 1e+05
Depth= 429 States= 1.2e+07 Transitions= 2.55e+07 Memory= 4212.030 t= 125 R= 1e+05
Depth= 429 States= 1.3e+07 Transitions= 2.76e+07 Memory= 4552.265 t= 146 R= 9e+04
Depth= 429 States= 1.4e+07 Transitions= 2.98e+07 Memory= 4892.499 t= 160 R= 9e+04
Depth= 429 States= 1.5e+07 Transitions= 3.19e+07 Memory= 5232.733 t= 177 R= 8e+04
Depth= 429 States= 1.6e+07 Transitions= 3.4e+07 Memory= 5573.065 t= 195 R= 8e+04
Depth= 429 States= 1.7e+07 Transitions= 3.61e+07 Memory= 5913.397 t= 220 R= 8e+04
Depth= 429 States= 1.8e+07 Transitions= 3.83e+07 Memory= 6253.632 t= 249 R= 7e+04
Depth= 429 States= 1.9e+07 Transitions= 4.04e+07 Memory= 6593.964 t= 286 R= 7e+04

20
ReversalModel/outputs/trace_seq_eq_parallel_10_7_8.txt Normal file
View File

@ -0,0 +1,20 @@
pan: ltl formula seq_eq_parallel
Depth= 429 States= 1e+06 Transitions= 2.12e+06 Memory= 468.964 t= 5.28 R= 2e+05
Depth= 429 States= 2e+06 Transitions= 4.25e+06 Memory= 809.198 t= 10.8 R= 2e+05
Depth= 429 States= 3e+06 Transitions= 6.38e+06 Memory= 1149.433 t= 17.1 R= 2e+05
Depth= 429 States= 4e+06 Transitions= 8.5e+06 Memory= 1489.667 t= 23.2 R= 2e+05
Depth= 429 States= 5e+06 Transitions= 1.06e+07 Memory= 1829.999 t= 31.3 R= 2e+05
Depth= 429 States= 6e+06 Transitions= 1.28e+07 Memory= 2170.331 t= 41.4 R= 1e+05
Depth= 429 States= 7e+06 Transitions= 1.49e+07 Memory= 2510.565 t= 51.7 R= 1e+05
Depth= 429 States= 8e+06 Transitions= 1.7e+07 Memory= 2850.897 t= 65.4 R= 1e+05
Depth= 429 States= 9e+06 Transitions= 1.91e+07 Memory= 3191.132 t= 78.2 R= 1e+05
Depth= 429 States= 1e+07 Transitions= 2.13e+07 Memory= 3531.366 t= 92.6 R= 1e+05
Depth= 429 States= 1.1e+07 Transitions= 2.34e+07 Memory= 3871.796 t= 108 R= 1e+05
Depth= 429 States= 1.2e+07 Transitions= 2.55e+07 Memory= 4212.030 t= 126 R= 1e+05
Depth= 429 States= 1.3e+07 Transitions= 2.76e+07 Memory= 4552.265 t= 145 R= 9e+04
Depth= 429 States= 1.4e+07 Transitions= 2.98e+07 Memory= 4892.499 t= 160 R= 9e+04
Depth= 429 States= 1.5e+07 Transitions= 3.19e+07 Memory= 5232.831 t= 176 R= 9e+04
Depth= 429 States= 1.6e+07 Transitions= 3.4e+07 Memory= 5573.065 t= 194 R= 8e+04
Depth= 429 States= 1.7e+07 Transitions= 3.61e+07 Memory= 5913.397 t= 219 R= 8e+04
Depth= 429 States= 1.8e+07 Transitions= 3.83e+07 Memory= 6253.730 t= 247 R= 7e+04
Depth= 429 States= 1.9e+07 Transitions= 4.04e+07 Memory= 6593.964 t= 284 R= 7e+04

20
ReversalModel/outputs/trace_seq_eq_parallel_10_7_9.txt Normal file
View File

@ -0,0 +1,20 @@
pan: ltl formula seq_eq_parallel
Depth= 429 States= 1e+06 Transitions= 2.12e+06 Memory= 468.964 t= 4.82 R= 2e+05
Depth= 429 States= 2e+06 Transitions= 4.25e+06 Memory= 809.198 t= 10.6 R= 2e+05
Depth= 429 States= 3e+06 Transitions= 6.38e+06 Memory= 1149.433 t= 17.2 R= 2e+05
Depth= 429 States= 4e+06 Transitions= 8.5e+06 Memory= 1489.667 t= 24.2 R= 2e+05
Depth= 429 States= 5e+06 Transitions= 1.06e+07 Memory= 1829.999 t= 30.5 R= 2e+05
Depth= 429 States= 6e+06 Transitions= 1.28e+07 Memory= 2170.331 t= 38.5 R= 2e+05
Depth= 429 States= 7e+06 Transitions= 1.49e+07 Memory= 2510.565 t= 46.2 R= 2e+05
Depth= 429 States= 8e+06 Transitions= 1.7e+07 Memory= 2850.897 t= 54.4 R= 1e+05
Depth= 429 States= 9e+06 Transitions= 1.91e+07 Memory= 3191.132 t= 64.4 R= 1e+05
Depth= 429 States= 1e+07 Transitions= 2.13e+07 Memory= 3531.366 t= 76.7 R= 1e+05
Depth= 429 States= 1.1e+07 Transitions= 2.34e+07 Memory= 3871.796 t= 89.7 R= 1e+05
Depth= 429 States= 1.2e+07 Transitions= 2.55e+07 Memory= 4212.030 t= 104 R= 1e+05
Depth= 429 States= 1.3e+07 Transitions= 2.76e+07 Memory= 4552.265 t= 123 R= 1e+05
Depth= 429 States= 1.4e+07 Transitions= 2.98e+07 Memory= 4892.499 t= 144 R= 1e+05
Depth= 429 States= 1.5e+07 Transitions= 3.19e+07 Memory= 5232.831 t= 162 R= 9e+04
Depth= 429 States= 1.6e+07 Transitions= 3.4e+07 Memory= 5573.065 t= 178 R= 9e+04
Depth= 429 States= 1.7e+07 Transitions= 3.61e+07 Memory= 5913.397 t= 211 R= 8e+04
Depth= 429 States= 1.8e+07 Transitions= 3.83e+07 Memory= 6253.730 t= 238 R= 8e+04
Depth= 429 States= 1.9e+07 Transitions= 4.04e+07 Memory= 6593.964 t= 277 R= 7e+04

32
ReversalModel/outputs/trace_seq_eq_parallel_10_8_10.txt Normal file
View File

@ -0,0 +1,32 @@
pan: ltl formula seq_eq_parallel
Depth= 449 States= 1e+06 Transitions= 2.12e+06 Memory= 476.972 t= 5.31 R= 2e+05
Depth= 449 States= 2e+06 Transitions= 4.25e+06 Memory= 825.312 t= 9.23 R= 2e+05
Depth= 449 States= 3e+06 Transitions= 6.38e+06 Memory= 1173.651 t= 12.9 R= 2e+05
Depth= 449 States= 4e+06 Transitions= 8.5e+06 Memory= 1521.894 t= 17.1 R= 2e+05
Depth= 449 States= 5e+06 Transitions= 1.06e+07 Memory= 1870.233 t= 22.7 R= 2e+05
Depth= 449 States= 6e+06 Transitions= 1.28e+07 Memory= 2218.573 t= 28.2 R= 2e+05
Depth= 449 States= 7e+06 Transitions= 1.49e+07 Memory= 2566.913 t= 34.4 R= 2e+05
Depth= 449 States= 8e+06 Transitions= 1.7e+07 Memory= 2915.155 t= 42.1 R= 2e+05
Depth= 449 States= 9e+06 Transitions= 1.91e+07 Memory= 3263.495 t= 50.6 R= 2e+05
Depth= 449 States= 1e+07 Transitions= 2.13e+07 Memory= 3611.835 t= 60 R= 2e+05
Depth= 449 States= 1.1e+07 Transitions= 2.34e+07 Memory= 3960.175 t= 70.7 R= 2e+05
Depth= 449 States= 1.2e+07 Transitions= 2.55e+07 Memory= 4308.417 t= 83.3 R= 1e+05
Depth= 449 States= 1.3e+07 Transitions= 2.76e+07 Memory= 4656.757 t= 95.7 R= 1e+05
Depth= 449 States= 1.4e+07 Transitions= 2.98e+07 Memory= 5005.097 t= 109 R= 1e+05
Depth= 449 States= 1.5e+07 Transitions= 3.19e+07 Memory= 5353.437 t= 219 R= 7e+04
Depth= 449 States= 1.6e+07 Transitions= 3.4e+07 Memory= 5701.679 t= 323 R= 5e+04
Depth= 449 States= 1.7e+07 Transitions= 3.61e+07 Memory= 6050.019 t= 333 R= 5e+04
Depth= 449 States= 1.8e+07 Transitions= 3.83e+07 Memory= 6398.358 t= 362 R= 5e+04
Depth= 449 States= 1.9e+07 Transitions= 4.04e+07 Memory= 6746.698 t= 367 R= 5e+04
Depth= 449 States= 2e+07 Transitions= 4.25e+07 Memory= 7094.940 t= 371 R= 5e+04
Depth= 449 States= 2.1e+07 Transitions= 4.46e+07 Memory= 7443.280 t= 376 R= 6e+04
Depth= 449 States= 2.2e+07 Transitions= 4.68e+07 Memory= 7791.620 t= 382 R= 6e+04
Depth= 449 States= 2.3e+07 Transitions= 4.89e+07 Memory= 8139.960 t= 387 R= 6e+04
Depth= 449 States= 2.4e+07 Transitions= 5.1e+07 Memory= 8488.202 t= 392 R= 6e+04
Depth= 449 States= 2.5e+07 Transitions= 5.31e+07 Memory= 8836.542 t= 398 R= 6e+04
Depth= 449 States= 2.6e+07 Transitions= 5.53e+07 Memory= 9184.882 t= 406 R= 6e+04
Depth= 449 States= 2.7e+07 Transitions= 5.74e+07 Memory= 9533.222 t= 412 R= 7e+04
Depth= 449 States= 2.8e+07 Transitions= 5.95e+07 Memory= 9881.464 t= 418 R= 7e+04
Depth= 449 States= 2.9e+07 Transitions= 6.16e+07 Memory= 10229.804 t= 426 R= 7e+04
Depth= 449 States= 3e+07 Transitions= 6.38e+07 Memory= 10578.144 t= 435 R= 7e+04
Depth= 449 States= 3.1e+07 Transitions= 6.59e+07 Memory= 10926.483 t= 444 R= 7e+04

20
ReversalModel/outputs/trace_seq_eq_parallel_10_8_2.txt Normal file
View File

@ -0,0 +1,20 @@
pan: ltl formula seq_eq_parallel
Depth= 449 States= 1e+06 Transitions= 2.12e+06 Memory= 476.972 t= 4.58 R= 2e+05
Depth= 449 States= 2e+06 Transitions= 4.25e+06 Memory= 825.312 t= 10.2 R= 2e+05
Depth= 449 States= 3e+06 Transitions= 6.38e+06 Memory= 1173.554 t= 15.4 R= 2e+05
Depth= 449 States= 4e+06 Transitions= 8.5e+06 Memory= 1521.894 t= 21 R= 2e+05
Depth= 449 States= 5e+06 Transitions= 1.06e+07 Memory= 1870.233 t= 26.9 R= 2e+05
Depth= 449 States= 6e+06 Transitions= 1.28e+07 Memory= 2218.476 t= 36.5 R= 2e+05
Depth= 449 States= 7e+06 Transitions= 1.49e+07 Memory= 2566.815 t= 48.9 R= 1e+05
Depth= 449 States= 8e+06 Transitions= 1.7e+07 Memory= 2915.155 t= 61 R= 1e+05
Depth= 449 States= 9e+06 Transitions= 1.91e+07 Memory= 3263.495 t= 71.2 R= 1e+05
Depth= 449 States= 1e+07 Transitions= 2.13e+07 Memory= 3611.737 t= 82.3 R= 1e+05
Depth= 449 States= 1.1e+07 Transitions= 2.34e+07 Memory= 3960.077 t= 99.2 R= 1e+05
Depth= 449 States= 1.2e+07 Transitions= 2.55e+07 Memory= 4308.319 t= 118 R= 1e+05
Depth= 449 States= 1.3e+07 Transitions= 2.76e+07 Memory= 4656.659 t= 137 R= 9e+04
Depth= 449 States= 1.4e+07 Transitions= 2.98e+07 Memory= 5004.999 t= 155 R= 9e+04
Depth= 449 States= 1.5e+07 Transitions= 3.19e+07 Memory= 5353.339 t= 173 R= 9e+04
Depth= 449 States= 1.6e+07 Transitions= 3.4e+07 Memory= 5701.581 t= 190 R= 8e+04
Depth= 449 States= 1.7e+07 Transitions= 3.61e+07 Memory= 6049.921 t= 213 R= 8e+04
Depth= 449 States= 1.8e+07 Transitions= 3.83e+07 Memory= 6398.261 t= 240 R= 7e+04
Depth= 449 States= 1.9e+07 Transitions= 4.04e+07 Memory= 6746.503 t= 271 R= 7e+04

20
ReversalModel/outputs/trace_seq_eq_parallel_10_8_3.txt Normal file
View File

@ -0,0 +1,20 @@
pan: ltl formula seq_eq_parallel
Depth= 449 States= 1e+06 Transitions= 2.12e+06 Memory= 476.972 t= 5.6 R= 2e+05
Depth= 449 States= 2e+06 Transitions= 4.25e+06 Memory= 825.312 t= 10.6 R= 2e+05
Depth= 449 States= 3e+06 Transitions= 6.38e+06 Memory= 1173.651 t= 16.2 R= 2e+05
Depth= 449 States= 4e+06 Transitions= 8.5e+06 Memory= 1521.894 t= 21.6 R= 2e+05
Depth= 449 States= 5e+06 Transitions= 1.06e+07 Memory= 1870.233 t= 29.1 R= 2e+05
Depth= 449 States= 6e+06 Transitions= 1.28e+07 Memory= 2218.573 t= 39.8 R= 2e+05
Depth= 449 States= 7e+06 Transitions= 1.49e+07 Memory= 2566.815 t= 52.7 R= 1e+05
Depth= 449 States= 8e+06 Transitions= 1.7e+07 Memory= 2915.155 t= 62.9 R= 1e+05
Depth= 449 States= 9e+06 Transitions= 1.91e+07 Memory= 3263.495 t= 72.8 R= 1e+05
Depth= 449 States= 1e+07 Transitions= 2.13e+07 Memory= 3611.737 t= 85.2 R= 1e+05
Depth= 449 States= 1.1e+07 Transitions= 2.34e+07 Memory= 3960.077 t= 102 R= 1e+05
Depth= 449 States= 1.2e+07 Transitions= 2.55e+07 Memory= 4308.417 t= 121 R= 1e+05
Depth= 449 States= 1.3e+07 Transitions= 2.76e+07 Memory= 4656.659 t= 143 R= 9e+04
Depth= 449 States= 1.4e+07 Transitions= 2.98e+07 Memory= 5004.999 t= 157 R= 9e+04
Depth= 449 States= 1.5e+07 Transitions= 3.19e+07 Memory= 5353.339 t= 175 R= 9e+04
Depth= 449 States= 1.6e+07 Transitions= 3.4e+07 Memory= 5701.679 t= 192 R= 8e+04
Depth= 449 States= 1.7e+07 Transitions= 3.61e+07 Memory= 6049.921 t= 216 R= 8e+04
Depth= 449 States= 1.8e+07 Transitions= 3.83e+07 Memory= 6398.261 t= 242 R= 7e+04
Depth= 449 States= 1.9e+07 Transitions= 4.04e+07 Memory= 6746.601 t= 275 R= 7e+04

20
ReversalModel/outputs/trace_seq_eq_parallel_10_8_4.txt Normal file
View File

@ -0,0 +1,20 @@
pan: ltl formula seq_eq_parallel
Depth= 449 States= 1e+06 Transitions= 2.12e+06 Memory= 476.972 t= 4.48 R= 2e+05
Depth= 449 States= 2e+06 Transitions= 4.25e+06 Memory= 825.312 t= 10.2 R= 2e+05
Depth= 449 States= 3e+06 Transitions= 6.38e+06 Memory= 1173.651 t= 16.8 R= 2e+05
Depth= 449 States= 4e+06 Transitions= 8.5e+06 Memory= 1521.894 t= 24.8 R= 2e+05
Depth= 449 States= 5e+06 Transitions= 1.06e+07 Memory= 1870.233 t= 30.8 R= 2e+05
Depth= 449 States= 6e+06 Transitions= 1.28e+07 Memory= 2218.573 t= 36.7 R= 2e+05
Depth= 449 States= 7e+06 Transitions= 1.49e+07 Memory= 2566.815 t= 42.8 R= 2e+05
Depth= 449 States= 8e+06 Transitions= 1.7e+07 Memory= 2915.155 t= 50.7 R= 2e+05
Depth= 449 States= 9e+06 Transitions= 1.91e+07 Memory= 3263.495 t= 60.3 R= 1e+05
Depth= 449 States= 1e+07 Transitions= 2.13e+07 Memory= 3611.835 t= 71.9 R= 1e+05
Depth= 449 States= 1.1e+07 Transitions= 2.34e+07 Memory= 3960.077 t= 83.8 R= 1e+05
Depth= 449 States= 1.2e+07 Transitions= 2.55e+07 Memory= 4308.417 t= 97 R= 1e+05
Depth= 449 States= 1.3e+07 Transitions= 2.76e+07 Memory= 4656.757 t= 112 R= 1e+05
Depth= 449 States= 1.4e+07 Transitions= 2.98e+07 Memory= 5005.097 t= 132 R= 1e+05
Depth= 449 States= 1.5e+07 Transitions= 3.19e+07 Memory= 5353.339 t= 159 R= 9e+04
Depth= 449 States= 1.6e+07 Transitions= 3.4e+07 Memory= 5701.679 t= 176 R= 9e+04
Depth= 449 States= 1.7e+07 Transitions= 3.61e+07 Memory= 6050.019 t= 202 R= 8e+04
Depth= 449 States= 1.8e+07 Transitions= 3.83e+07 Memory= 6398.261 t= 244 R= 7e+04
Depth= 449 States= 1.9e+07 Transitions= 4.04e+07 Memory= 6746.601 t= 281 R= 7e+04

20
ReversalModel/outputs/trace_seq_eq_parallel_10_8_5.txt Normal file
View File

@ -0,0 +1,20 @@
pan: ltl formula seq_eq_parallel
Depth= 449 States= 1e+06 Transitions= 2.12e+06 Memory= 476.972 t= 5.13 R= 2e+05
Depth= 449 States= 2e+06 Transitions= 4.25e+06 Memory= 825.312 t= 10.2 R= 2e+05
Depth= 449 States= 3e+06 Transitions= 6.38e+06 Memory= 1173.651 t= 14.9 R= 2e+05
Depth= 449 States= 4e+06 Transitions= 8.5e+06 Memory= 1521.894 t= 20.8 R= 2e+05
Depth= 449 States= 5e+06 Transitions= 1.06e+07 Memory= 1870.233 t= 27.9 R= 2e+05
Depth= 449 States= 6e+06 Transitions= 1.28e+07 Memory= 2218.573 t= 35.7 R= 2e+05
Depth= 449 States= 7e+06 Transitions= 1.49e+07 Memory= 2566.913 t= 45.1 R= 2e+05
Depth= 449 States= 8e+06 Transitions= 1.7e+07 Memory= 2915.155 t= 54.9 R= 1e+05
Depth= 449 States= 9e+06 Transitions= 1.91e+07 Memory= 3263.495 t= 65.6 R= 1e+05
Depth= 449 States= 1e+07 Transitions= 2.13e+07 Memory= 3611.835 t= 77.5 R= 1e+05
Depth= 449 States= 1.1e+07 Transitions= 2.34e+07 Memory= 3960.077 t= 91.7 R= 1e+05
Depth= 449 States= 1.2e+07 Transitions= 2.55e+07 Memory= 4308.417 t= 112 R= 1e+05
Depth= 449 States= 1.3e+07 Transitions= 2.76e+07 Memory= 4656.757 t= 133 R= 1e+05
Depth= 449 States= 1.4e+07 Transitions= 2.98e+07 Memory= 5005.097 t= 146 R= 1e+05
Depth= 449 States= 1.5e+07 Transitions= 3.19e+07 Memory= 5353.339 t= 164 R= 9e+04
Depth= 449 States= 1.6e+07 Transitions= 3.4e+07 Memory= 5701.679 t= 194 R= 8e+04
Depth= 449 States= 1.7e+07 Transitions= 3.61e+07 Memory= 6050.019 t= 226 R= 8e+04
Depth= 449 States= 1.8e+07 Transitions= 3.83e+07 Memory= 6398.358 t= 257 R= 7e+04
Depth= 449 States= 1.9e+07 Transitions= 4.04e+07 Memory= 6746.601 t= 294 R= 6e+04

20
ReversalModel/outputs/trace_seq_eq_parallel_10_8_6.txt Normal file
View File

@ -0,0 +1,20 @@
pan: ltl formula seq_eq_parallel
Depth= 449 States= 1e+06 Transitions= 2.12e+06 Memory= 476.972 t= 5.32 R= 2e+05
Depth= 449 States= 2e+06 Transitions= 4.25e+06 Memory= 825.312 t= 10.3 R= 2e+05
Depth= 449 States= 3e+06 Transitions= 6.38e+06 Memory= 1173.651 t= 16.1 R= 2e+05
Depth= 449 States= 4e+06 Transitions= 8.5e+06 Memory= 1521.894 t= 22.4 R= 2e+05
Depth= 449 States= 5e+06 Transitions= 1.06e+07 Memory= 1870.233 t= 28.3 R= 2e+05
Depth= 449 States= 6e+06 Transitions= 1.28e+07 Memory= 2218.573 t= 36.4 R= 2e+05
Depth= 449 States= 7e+06 Transitions= 1.49e+07 Memory= 2566.913 t= 46.9 R= 1e+05
Depth= 449 States= 8e+06 Transitions= 1.7e+07 Memory= 2915.155 t= 64.6 R= 1e+05
Depth= 449 States= 9e+06 Transitions= 1.91e+07 Memory= 3263.495 t= 82.8 R= 1e+05
Depth= 449 States= 1e+07 Transitions= 2.13e+07 Memory= 3611.835 t= 97 R= 1e+05
Depth= 449 States= 1.1e+07 Transitions= 2.34e+07 Memory= 3960.175 t= 113 R= 1e+05
Depth= 449 States= 1.2e+07 Transitions= 2.55e+07 Memory= 4308.417 t= 129 R= 9e+04
Depth= 449 States= 1.3e+07 Transitions= 2.76e+07 Memory= 4656.757 t= 151 R= 9e+04
Depth= 449 States= 1.4e+07 Transitions= 2.98e+07 Memory= 5005.097 t= 166 R= 8e+04
Depth= 449 States= 1.5e+07 Transitions= 3.19e+07 Memory= 5353.339 t= 179 R= 8e+04
Depth= 449 States= 1.6e+07 Transitions= 3.4e+07 Memory= 5701.679 t= 198 R= 8e+04
Depth= 449 States= 1.7e+07 Transitions= 3.61e+07 Memory= 6050.019 t= 225 R= 8e+04
Depth= 449 States= 1.8e+07 Transitions= 3.83e+07 Memory= 6398.358 t= 257 R= 7e+04
Depth= 449 States= 1.9e+07 Transitions= 4.04e+07 Memory= 6746.601 t= 293 R= 6e+04

20
ReversalModel/outputs/trace_seq_eq_parallel_10_8_7.txt Normal file
View File

@ -0,0 +1,20 @@
pan: ltl formula seq_eq_parallel
Depth= 449 States= 1e+06 Transitions= 2.12e+06 Memory= 476.972 t= 5.37 R= 2e+05
Depth= 449 States= 2e+06 Transitions= 4.25e+06 Memory= 825.312 t= 10.3 R= 2e+05
Depth= 449 States= 3e+06 Transitions= 6.38e+06 Memory= 1173.651 t= 16.4 R= 2e+05
Depth= 449 States= 4e+06 Transitions= 8.5e+06 Memory= 1521.894 t= 22.7 R= 2e+05
Depth= 449 States= 5e+06 Transitions= 1.06e+07 Memory= 1870.233 t= 28.8 R= 2e+05
Depth= 449 States= 6e+06 Transitions= 1.28e+07 Memory= 2218.573 t= 37.2 R= 2e+05
Depth= 449 States= 7e+06 Transitions= 1.49e+07 Memory= 2566.913 t= 48.7 R= 1e+05
Depth= 449 States= 8e+06 Transitions= 1.7e+07 Memory= 2915.155 t= 66.9 R= 1e+05
Depth= 449 States= 9e+06 Transitions= 1.91e+07 Memory= 3263.495 t= 84.4 R= 1e+05
Depth= 449 States= 1e+07 Transitions= 2.13e+07 Memory= 3611.835 t= 98.7 R= 1e+05
Depth= 449 States= 1.1e+07 Transitions= 2.34e+07 Memory= 3960.175 t= 114 R= 1e+05
Depth= 449 States= 1.2e+07 Transitions= 2.55e+07 Memory= 4308.417 t= 132 R= 9e+04
Depth= 449 States= 1.3e+07 Transitions= 2.76e+07 Memory= 4656.757 t= 152 R= 9e+04
Depth= 449 States= 1.4e+07 Transitions= 2.98e+07 Memory= 5005.097 t= 167 R= 8e+04
Depth= 449 States= 1.5e+07 Transitions= 3.19e+07 Memory= 5353.339 t= 180 R= 8e+04
Depth= 449 States= 1.6e+07 Transitions= 3.4e+07 Memory= 5701.679 t= 200 R= 8e+04
Depth= 449 States= 1.7e+07 Transitions= 3.61e+07 Memory= 6050.019 t= 227 R= 8e+04
Depth= 449 States= 1.8e+07 Transitions= 3.83e+07 Memory= 6398.358 t= 258 R= 7e+04
Depth= 449 States= 1.9e+07 Transitions= 4.04e+07 Memory= 6746.601 t= 295 R= 6e+04

21
ReversalModel/outputs/trace_seq_eq_parallel_10_8_8.txt Normal file
View File

@ -0,0 +1,21 @@
pan: ltl formula seq_eq_parallel
Depth= 449 States= 1e+06 Transitions= 2.12e+06 Memory= 476.972 t= 4.82 R= 2e+05
Depth= 449 States= 2e+06 Transitions= 4.25e+06 Memory= 825.312 t= 10.1 R= 2e+05
Depth= 449 States= 3e+06 Transitions= 6.38e+06 Memory= 1173.651 t= 16.4 R= 2e+05
Depth= 449 States= 4e+06 Transitions= 8.5e+06 Memory= 1521.894 t= 23.4 R= 2e+05
Depth= 449 States= 5e+06 Transitions= 1.06e+07 Memory= 1870.233 t= 28.6 R= 2e+05
Depth= 449 States= 6e+06 Transitions= 1.28e+07 Memory= 2218.573 t= 33.9 R= 2e+05
Depth= 449 States= 7e+06 Transitions= 1.49e+07 Memory= 2566.913 t= 41.4 R= 2e+05
Depth= 449 States= 8e+06 Transitions= 1.7e+07 Memory= 2915.155 t= 49.6 R= 2e+05
Depth= 449 States= 9e+06 Transitions= 1.91e+07 Memory= 3263.495 t= 60.5 R= 1e+05
Depth= 449 States= 1e+07 Transitions= 2.13e+07 Memory= 3611.835 t= 72.9 R= 1e+05
Depth= 449 States= 1.1e+07 Transitions= 2.34e+07 Memory= 3960.175 t= 89.3 R= 1e+05
Depth= 449 States= 1.2e+07 Transitions= 2.55e+07 Memory= 4308.417 t= 105 R= 1e+05
Depth= 449 States= 1.3e+07 Transitions= 2.76e+07 Memory= 4656.757 t= 124 R= 1e+05
Depth= 449 States= 1.4e+07 Transitions= 2.98e+07 Memory= 5005.097 t= 144 R= 1e+05
Depth= 449 States= 1.5e+07 Transitions= 3.19e+07 Memory= 5353.437 t= 163 R= 9e+04
Depth= 449 States= 1.6e+07 Transitions= 3.4e+07 Memory= 5701.679 t= 173 R= 9e+04
Depth= 449 States= 1.7e+07 Transitions= 3.61e+07 Memory= 6050.019 t= 190 R= 9e+04
Depth= 449 States= 1.8e+07 Transitions= 3.83e+07 Memory= 6398.358 t= 213 R= 8e+04
Depth= 449 States= 1.9e+07 Transitions= 4.04e+07 Memory= 6746.601 t= 240 R= 8e+04
Depth= 449 States= 2e+07 Transitions= 4.25e+07 Memory= 7094.940 t= 267 R= 7e+04

21
ReversalModel/outputs/trace_seq_eq_parallel_10_8_9.txt Normal file
View File

@ -0,0 +1,21 @@
pan: ltl formula seq_eq_parallel
Depth= 449 States= 1e+06 Transitions= 2.12e+06 Memory= 476.972 t= 4.11 R= 2e+05
Depth= 449 States= 2e+06 Transitions= 4.25e+06 Memory= 825.312 t= 9.11 R= 2e+05
Depth= 449 States= 3e+06 Transitions= 6.38e+06 Memory= 1173.651 t= 15 R= 2e+05
Depth= 449 States= 4e+06 Transitions= 8.5e+06 Memory= 1521.894 t= 20.8 R= 2e+05
Depth= 449 States= 5e+06 Transitions= 1.06e+07 Memory= 1870.233 t= 29.2 R= 2e+05
Depth= 449 States= 6e+06 Transitions= 1.28e+07 Memory= 2218.573 t= 37.2 R= 2e+05
Depth= 449 States= 7e+06 Transitions= 1.49e+07 Memory= 2566.913 t= 48 R= 1e+05
Depth= 449 States= 8e+06 Transitions= 1.7e+07 Memory= 2915.155 t= 60.9 R= 1e+05
Depth= 449 States= 9e+06 Transitions= 1.91e+07 Memory= 3263.495 t= 73.8 R= 1e+05
Depth= 449 States= 1e+07 Transitions= 2.13e+07 Memory= 3611.835 t= 89.2 R= 1e+05
Depth= 449 States= 1.1e+07 Transitions= 2.34e+07 Memory= 3960.175 t= 105 R= 1e+05
Depth= 449 States= 1.2e+07 Transitions= 2.55e+07 Memory= 4308.417 t= 123 R= 1e+05
Depth= 449 States= 1.3e+07 Transitions= 2.76e+07 Memory= 4656.757 t= 137 R= 1e+05
Depth= 449 States= 1.4e+07 Transitions= 2.98e+07 Memory= 5005.097 t= 144 R= 1e+05
Depth= 449 States= 1.5e+07 Transitions= 3.19e+07 Memory= 5353.437 t= 156 R= 1e+05
Depth= 449 States= 1.6e+07 Transitions= 3.4e+07 Memory= 5701.679 t= 171 R= 9e+04
Depth= 449 States= 1.7e+07 Transitions= 3.61e+07 Memory= 6050.019 t= 189 R= 9e+04
Depth= 449 States= 1.8e+07 Transitions= 3.83e+07 Memory= 6398.358 t= 212 R= 9e+04
Depth= 449 States= 1.9e+07 Transitions= 4.04e+07 Memory= 6746.698 t= 234 R= 8e+04
Depth= 449 States= 2e+07 Transitions= 4.25e+07 Memory= 7094.940 t= 368 R= 5e+04

35
ReversalModel/outputs/trace_seq_eq_parallel_2_10_10.txt Normal file
View File

@ -0,0 +1,35 @@
pan: ltl formula seq_eq_parallel
Depth= 281 States= 1e+06 Transitions= 1.14e+06 Memory= 343.573 t= 1.41 R= 7e+05
Depth= 281 States= 2e+06 Transitions= 2.28e+06 Memory= 558.515 t= 2.81 R= 7e+05
Depth= 281 States= 3e+06 Transitions= 3.42e+06 Memory= 773.358 t= 4.3 R= 7e+05
Depth= 281 States= 4e+06 Transitions= 4.56e+06 Memory= 988.300 t= 5.83 R= 7e+05
Depth= 281 States= 5e+06 Transitions= 5.7e+06 Memory= 1203.144 t= 7.33 R= 7e+05
Depth= 281 States= 6e+06 Transitions= 6.84e+06 Memory= 1418.085 t= 8.81 R= 7e+05
Depth= 281 States= 7e+06 Transitions= 7.98e+06 Memory= 1632.929 t= 10.4 R= 7e+05
Depth= 281 States= 8e+06 Transitions= 9.12e+06 Memory= 1847.870 t= 11.9 R= 7e+05
Depth= 281 States= 9e+06 Transitions= 1.03e+07 Memory= 2062.812 t= 13.9 R= 6e+05
Depth= 281 States= 1e+07 Transitions= 1.14e+07 Memory= 2277.655 t= 16.1 R= 6e+05
Depth= 281 States= 1.1e+07 Transitions= 1.25e+07 Memory= 2492.597 t= 18.7 R= 6e+05
Depth= 281 States= 1.2e+07 Transitions= 1.37e+07 Memory= 2707.440 t= 20.8 R= 6e+05
Depth= 281 States= 1.3e+07 Transitions= 1.48e+07 Memory= 2922.382 t= 23 R= 6e+05
Depth= 281 States= 1.4e+07 Transitions= 1.6e+07 Memory= 3137.226 t= 26.6 R= 5e+05
Depth= 281 States= 1.5e+07 Transitions= 1.71e+07 Memory= 3352.167 t= 30.4 R= 5e+05
Depth= 281 States= 1.6e+07 Transitions= 1.82e+07 Memory= 3567.011 t= 33.9 R= 5e+05
Depth= 281 States= 1.7e+07 Transitions= 1.94e+07 Memory= 3781.952 t= 37.3 R= 5e+05
Depth= 281 States= 1.8e+07 Transitions= 2.05e+07 Memory= 3996.894 t= 41.8 R= 4e+05
Depth= 281 States= 1.9e+07 Transitions= 2.17e+07 Memory= 4211.737 t= 46.1 R= 4e+05
Depth= 281 States= 2e+07 Transitions= 2.28e+07 Memory= 4426.679 t= 51.1 R= 4e+05
Depth= 281 States= 2.1e+07 Transitions= 2.39e+07 Memory= 4641.522 t= 56.8 R= 4e+05
Depth= 281 States= 2.2e+07 Transitions= 2.51e+07 Memory= 4856.464 t= 64.2 R= 3e+05
Depth= 281 States= 2.3e+07 Transitions= 2.62e+07 Memory= 5071.308 t= 72.9 R= 3e+05
Depth= 281 States= 2.4e+07 Transitions= 2.74e+07 Memory= 5286.249 t= 82.1 R= 3e+05
Depth= 281 States= 2.5e+07 Transitions= 2.85e+07 Memory= 5501.190 t= 91.8 R= 3e+05
Depth= 281 States= 2.6e+07 Transitions= 2.96e+07 Memory= 5716.034 t= 103 R= 3e+05
Depth= 281 States= 2.7e+07 Transitions= 3.08e+07 Memory= 5930.976 t= 117 R= 2e+05
Depth= 281 States= 2.8e+07 Transitions= 3.19e+07 Memory= 6145.819 t= 131 R= 2e+05
Depth= 281 States= 2.9e+07 Transitions= 3.31e+07 Memory= 6360.761 t= 145 R= 2e+05
Depth= 281 States= 3e+07 Transitions= 3.42e+07 Memory= 6575.605 t= 162 R= 2e+05
Depth= 281 States= 3.1e+07 Transitions= 3.54e+07 Memory= 6790.546 t= 180 R= 2e+05
Depth= 281 States= 3.2e+07 Transitions= 3.65e+07 Memory= 7005.487 t= 199 R= 2e+05
Depth= 281 States= 3.3e+07 Transitions= 3.76e+07 Memory= 7220.331 t= 219 R= 2e+05
Depth= 281 States= 3.4e+07 Transitions= 3.88e+07 Memory= 7435.272 t= 242 R= 1e+05

58
ReversalModel/outputs/trace_seq_eq_parallel_2_10_2.txt Normal file
View File

@ -0,0 +1,58 @@
pan: ltl formula seq_eq_parallel
Depth= 281 States= 1e+06 Transitions= 1.14e+06 Memory= 343.476 t= 1.52 R= 7e+05
Depth= 281 States= 2e+06 Transitions= 2.28e+06 Memory= 558.222 t= 2.95 R= 7e+05
Depth= 281 States= 3e+06 Transitions= 3.42e+06 Memory= 773.065 t= 4.51 R= 7e+05
Depth= 281 States= 4e+06 Transitions= 4.56e+06 Memory= 987.812 t= 6.05 R= 7e+05
Depth= 281 States= 5e+06 Transitions= 5.7e+06 Memory= 1202.558 t= 7.67 R= 7e+05
Depth= 281 States= 6e+06 Transitions= 6.84e+06 Memory= 1417.401 t= 9.67 R= 6e+05
Depth= 281 States= 7e+06 Transitions= 7.98e+06 Memory= 1632.147 t= 11.7 R= 6e+05
Depth= 281 States= 8e+06 Transitions= 9.12e+06 Memory= 1846.991 t= 13.8 R= 6e+05
Depth= 281 States= 9e+06 Transitions= 1.03e+07 Memory= 2061.737 t= 15.8 R= 6e+05
Depth= 281 States= 1e+07 Transitions= 1.14e+07 Memory= 2276.483 t= 17.9 R= 6e+05
Depth= 281 States= 1.1e+07 Transitions= 1.25e+07 Memory= 2491.327 t= 19.7 R= 6e+05
Depth= 281 States= 1.2e+07 Transitions= 1.37e+07 Memory= 2706.073 t= 21.3 R= 6e+05
Depth= 281 States= 1.3e+07 Transitions= 1.48e+07 Memory= 2920.917 t= 22.8 R= 6e+05
Depth= 281 States= 1.4e+07 Transitions= 1.6e+07 Memory= 3135.663 t= 24.3 R= 6e+05
Depth= 281 States= 1.5e+07 Transitions= 1.71e+07 Memory= 3350.409 t= 25.8 R= 6e+05
Depth= 281 States= 1.6e+07 Transitions= 1.82e+07 Memory= 3565.253 t= 27.4 R= 6e+05
Depth= 281 States= 1.7e+07 Transitions= 1.94e+07 Memory= 3779.999 t= 28.9 R= 6e+05
Depth= 281 States= 1.8e+07 Transitions= 2.05e+07 Memory= 3994.843 t= 30.4 R= 6e+05
(Spin Version 6.5.2 -- 6 December 2019)
+ Partial Order Reduction
Full statespace search for:
never claim + (seq_eq_parallel)
assertion violations + (if within scope of claim)
acceptance cycles + (fairness disabled)
invalid end states - (disabled by never claim)
State-vector 228 byte, depth reached 281, errors: 0
18187090 states, stored
2539107 states, matched
20726197 transitions (= stored+matched)
0 atomic steps
hash conflicts: 1509186 (resolved)
Stats on memory usage (in Megabytes):
4440.208 equivalent memory usage for states (stored*(State-vector + overhead))
3910.528 actual memory usage for states (compression: 88.07%)
state-vector as stored = 197 byte + 28 byte overhead
128.000 memory used for hash table (-w24)
0.534 memory used for DFS stack (-m10000)
4.083 memory lost to fragmentation
4034.980 total actual memory usage
unreached in proctype ThreadedReverser
(0 of 15 states)
unreached in init
reversal_seq_eq_parallel_2_10_2.pml:87, state 71, "seq_eq_to_parallel = 0"
reversal_seq_eq_parallel_2_10_2.pml:91, state 81, "-end-"
(2 of 81 states)
unreached in claim seq_eq_parallel
_spin_nvr.tmp:8, state 10, "-end-"
(1 of 10 states)
pan: elapsed time 30.8 seconds
pan: rate 591450.08 states/second

35
ReversalModel/outputs/trace_seq_eq_parallel_2_10_3.txt Normal file
View File

@ -0,0 +1,35 @@
pan: ltl formula seq_eq_parallel
Depth= 281 States= 1e+06 Transitions= 1.14e+06 Memory= 343.476 t= 1.39 R= 7e+05
Depth= 281 States= 2e+06 Transitions= 2.28e+06 Memory= 558.319 t= 2.75 R= 7e+05
Depth= 281 States= 3e+06 Transitions= 3.42e+06 Memory= 773.163 t= 4.11 R= 7e+05
Depth= 281 States= 4e+06 Transitions= 4.56e+06 Memory= 988.007 t= 5.48 R= 7e+05
Depth= 281 States= 5e+06 Transitions= 5.7e+06 Memory= 1202.851 t= 6.86 R= 7e+05
Depth= 281 States= 6e+06 Transitions= 6.84e+06 Memory= 1417.694 t= 8.27 R= 7e+05
Depth= 281 States= 7e+06 Transitions= 7.98e+06 Memory= 1632.538 t= 9.72 R= 7e+05
Depth= 281 States= 8e+06 Transitions= 9.12e+06 Memory= 1847.382 t= 11.3 R= 7e+05
Depth= 281 States= 9e+06 Transitions= 1.03e+07 Memory= 2062.226 t= 12.7 R= 7e+05
Depth= 281 States= 1e+07 Transitions= 1.14e+07 Memory= 2277.069 t= 14.2 R= 7e+05
Depth= 281 States= 1.1e+07 Transitions= 1.25e+07 Memory= 2491.913 t= 15.6 R= 7e+05
Depth= 281 States= 1.2e+07 Transitions= 1.37e+07 Memory= 2706.757 t= 17.1 R= 7e+05
Depth= 281 States= 1.3e+07 Transitions= 1.48e+07 Memory= 2921.601 t= 18.6 R= 7e+05
Depth= 281 States= 1.4e+07 Transitions= 1.6e+07 Memory= 3136.347 t= 20.1 R= 7e+05
Depth= 281 States= 1.5e+07 Transitions= 1.71e+07 Memory= 3351.190 t= 21.8 R= 7e+05
Depth= 281 States= 1.6e+07 Transitions= 1.82e+07 Memory= 3566.034 t= 23.9 R= 7e+05
Depth= 281 States= 1.7e+07 Transitions= 1.94e+07 Memory= 3780.878 t= 26.7 R= 6e+05
Depth= 281 States= 1.8e+07 Transitions= 2.05e+07 Memory= 3995.722 t= 30.4 R= 6e+05
Depth= 281 States= 1.9e+07 Transitions= 2.17e+07 Memory= 4210.565 t= 34.2 R= 6e+05
Depth= 281 States= 2e+07 Transitions= 2.28e+07 Memory= 4425.409 t= 40.4 R= 5e+05
Depth= 281 States= 2.1e+07 Transitions= 2.39e+07 Memory= 4640.253 t= 46.9 R= 4e+05
Depth= 281 States= 2.2e+07 Transitions= 2.51e+07 Memory= 4855.097 t= 55 R= 4e+05
Depth= 281 States= 2.3e+07 Transitions= 2.62e+07 Memory= 5069.940 t= 65.3 R= 4e+05
Depth= 281 States= 2.4e+07 Transitions= 2.74e+07 Memory= 5284.784 t= 76.5 R= 3e+05
Depth= 281 States= 2.5e+07 Transitions= 2.85e+07 Memory= 5499.628 t= 89 R= 3e+05
Depth= 281 States= 2.6e+07 Transitions= 2.96e+07 Memory= 5714.374 t= 103 R= 3e+05
Depth= 281 States= 2.7e+07 Transitions= 3.08e+07 Memory= 5929.218 t= 117 R= 2e+05
Depth= 281 States= 2.8e+07 Transitions= 3.19e+07 Memory= 6144.062 t= 133 R= 2e+05
Depth= 281 States= 2.9e+07 Transitions= 3.31e+07 Memory= 6358.905 t= 149 R= 2e+05
Depth= 281 States= 3e+07 Transitions= 3.42e+07 Memory= 6573.749 t= 167 R= 2e+05
Depth= 281 States= 3.1e+07 Transitions= 3.53e+07 Memory= 6788.593 t= 188 R= 2e+05
Depth= 281 States= 3.2e+07 Transitions= 3.65e+07 Memory= 7003.437 t= 208 R= 2e+05
Depth= 281 States= 3.3e+07 Transitions= 3.76e+07 Memory= 7218.280 t= 230 R= 1e+05
Depth= 281 States= 3.4e+07 Transitions= 3.88e+07 Memory= 7433.124 t= 255 R= 1e+05

35
ReversalModel/outputs/trace_seq_eq_parallel_2_10_4.txt Normal file
View File

@ -0,0 +1,35 @@
pan: ltl formula seq_eq_parallel
Depth= 281 States= 1e+06 Transitions= 1.14e+06 Memory= 343.573 t= 1.38 R= 7e+05
Depth= 281 States= 2e+06 Transitions= 2.28e+06 Memory= 558.417 t= 2.73 R= 7e+05
Depth= 281 States= 3e+06 Transitions= 3.42e+06 Memory= 773.261 t= 4.09 R= 7e+05
Depth= 281 States= 4e+06 Transitions= 4.56e+06 Memory= 988.105 t= 5.47 R= 7e+05
Depth= 281 States= 5e+06 Transitions= 5.7e+06 Memory= 1202.948 t= 6.87 R= 7e+05
Depth= 281 States= 6e+06 Transitions= 6.84e+06 Memory= 1417.792 t= 8.33 R= 7e+05
Depth= 281 States= 7e+06 Transitions= 7.98e+06 Memory= 1632.636 t= 10.1 R= 7e+05
Depth= 281 States= 8e+06 Transitions= 9.12e+06 Memory= 1847.480 t= 11.9 R= 7e+05
Depth= 281 States= 9e+06 Transitions= 1.03e+07 Memory= 2062.421 t= 14.2 R= 6e+05
Depth= 281 States= 1e+07 Transitions= 1.14e+07 Memory= 2277.265 t= 16.7 R= 6e+05
Depth= 281 States= 1.1e+07 Transitions= 1.25e+07 Memory= 2492.108 t= 19 R= 6e+05
Depth= 281 States= 1.2e+07 Transitions= 1.37e+07 Memory= 2706.952 t= 21.4 R= 6e+05
Depth= 281 States= 1.3e+07 Transitions= 1.48e+07 Memory= 2921.796 t= 24.6 R= 5e+05
Depth= 281 States= 1.4e+07 Transitions= 1.6e+07 Memory= 3136.640 t= 28 R= 5e+05
Depth= 281 States= 1.5e+07 Transitions= 1.71e+07 Memory= 3351.483 t= 30.8 R= 5e+05
Depth= 281 States= 1.6e+07 Transitions= 1.82e+07 Memory= 3566.327 t= 34.3 R= 5e+05
Depth= 281 States= 1.7e+07 Transitions= 1.94e+07 Memory= 3781.171 t= 37.7 R= 5e+05
Depth= 281 States= 1.8e+07 Transitions= 2.05e+07 Memory= 3996.015 t= 41.5 R= 4e+05
Depth= 281 States= 1.9e+07 Transitions= 2.17e+07 Memory= 4210.956 t= 45.6 R= 4e+05
Depth= 281 States= 2e+07 Transitions= 2.28e+07 Memory= 4425.800 t= 50.7 R= 4e+05
Depth= 281 States= 2.1e+07 Transitions= 2.39e+07 Memory= 4640.644 t= 56.2 R= 4e+05
Depth= 281 States= 2.2e+07 Transitions= 2.51e+07 Memory= 4855.487 t= 62.2 R= 4e+05
Depth= 281 States= 2.3e+07 Transitions= 2.62e+07 Memory= 5070.331 t= 69.2 R= 3e+05
Depth= 281 States= 2.4e+07 Transitions= 2.74e+07 Memory= 5285.175 t= 77.1 R= 3e+05
Depth= 281 States= 2.5e+07 Transitions= 2.85e+07 Memory= 5500.019 t= 86.4 R= 3e+05
Depth= 281 States= 2.6e+07 Transitions= 2.96e+07 Memory= 5714.862 t= 96.7 R= 3e+05
Depth= 281 States= 2.7e+07 Transitions= 3.08e+07 Memory= 5929.804 t= 109 R= 2e+05
Depth= 281 States= 2.8e+07 Transitions= 3.19e+07 Memory= 6144.647 t= 122 R= 2e+05
Depth= 281 States= 2.9e+07 Transitions= 3.31e+07 Memory= 6359.491 t= 136 R= 2e+05
Depth= 281 States= 3e+07 Transitions= 3.42e+07 Memory= 6574.335 t= 153 R= 2e+05
Depth= 281 States= 3.1e+07 Transitions= 3.53e+07 Memory= 6789.179 t= 173 R= 2e+05
Depth= 281 States= 3.2e+07 Transitions= 3.65e+07 Memory= 7004.022 t= 192 R= 2e+05
Depth= 281 States= 3.3e+07 Transitions= 3.76e+07 Memory= 7218.866 t= 213 R= 2e+05
Depth= 281 States= 3.4e+07 Transitions= 3.88e+07 Memory= 7433.710 t= 235 R= 1e+05

35
ReversalModel/outputs/trace_seq_eq_parallel_2_10_5.txt Normal file
View File

@ -0,0 +1,35 @@
pan: ltl formula seq_eq_parallel
Depth= 281 States= 1e+06 Transitions= 1.14e+06 Memory= 343.573 t= 1.85 R= 5e+05
Depth= 281 States= 2e+06 Transitions= 2.28e+06 Memory= 558.417 t= 3.75 R= 5e+05
Depth= 281 States= 3e+06 Transitions= 3.42e+06 Memory= 773.261 t= 5.59 R= 5e+05
Depth= 281 States= 4e+06 Transitions= 4.56e+06 Memory= 988.202 t= 7.63 R= 5e+05
Depth= 281 States= 5e+06 Transitions= 5.7e+06 Memory= 1203.046 t= 9.7 R= 5e+05
Depth= 281 States= 6e+06 Transitions= 6.84e+06 Memory= 1417.890 t= 11.7 R= 5e+05
Depth= 281 States= 7e+06 Transitions= 7.98e+06 Memory= 1632.733 t= 13.9 R= 5e+05
Depth= 281 States= 8e+06 Transitions= 9.12e+06 Memory= 1847.675 t= 16.1 R= 5e+05
Depth= 281 States= 9e+06 Transitions= 1.03e+07 Memory= 2062.519 t= 18.5 R= 5e+05
Depth= 281 States= 1e+07 Transitions= 1.14e+07 Memory= 2277.362 t= 21.2 R= 5e+05
Depth= 281 States= 1.1e+07 Transitions= 1.25e+07 Memory= 2492.206 t= 23.9 R= 5e+05
Depth= 281 States= 1.2e+07 Transitions= 1.37e+07 Memory= 2707.147 t= 26.6 R= 5e+05
Depth= 281 States= 1.3e+07 Transitions= 1.48e+07 Memory= 2921.991 t= 29.8 R= 4e+05
Depth= 281 States= 1.4e+07 Transitions= 1.6e+07 Memory= 3136.835 t= 32.7 R= 4e+05
Depth= 281 States= 1.5e+07 Transitions= 1.71e+07 Memory= 3351.679 t= 34.8 R= 4e+05
Depth= 281 States= 1.6e+07 Transitions= 1.82e+07 Memory= 3566.620 t= 36.7 R= 4e+05
Depth= 281 States= 1.7e+07 Transitions= 1.94e+07 Memory= 3781.464 t= 38.5 R= 4e+05
Depth= 281 States= 1.8e+07 Transitions= 2.05e+07 Memory= 3996.308 t= 40.5 R= 4e+05
Depth= 281 States= 1.9e+07 Transitions= 2.17e+07 Memory= 4211.151 t= 42.8 R= 4e+05
Depth= 281 States= 2e+07 Transitions= 2.28e+07 Memory= 4426.093 t= 44.8 R= 4e+05
Depth= 281 States= 2.1e+07 Transitions= 2.39e+07 Memory= 4640.937 t= 46.5 R= 5e+05
Depth= 281 States= 2.2e+07 Transitions= 2.51e+07 Memory= 4855.780 t= 48.1 R= 5e+05
Depth= 281 States= 2.3e+07 Transitions= 2.62e+07 Memory= 5070.624 t= 49.6 R= 5e+05
Depth= 281 States= 2.4e+07 Transitions= 2.74e+07 Memory= 5285.565 t= 51.2 R= 5e+05
Depth= 281 States= 2.5e+07 Transitions= 2.85e+07 Memory= 5500.409 t= 52.8 R= 5e+05
Depth= 281 States= 2.6e+07 Transitions= 2.96e+07 Memory= 5715.253 t= 54.3 R= 5e+05
Depth= 281 States= 2.7e+07 Transitions= 3.08e+07 Memory= 5930.097 t= 56 R= 5e+05
Depth= 281 States= 2.8e+07 Transitions= 3.19e+07 Memory= 6145.038 t= 58.2 R= 5e+05
Depth= 281 States= 2.9e+07 Transitions= 3.31e+07 Memory= 6359.882 t= 60.5 R= 5e+05
Depth= 281 States= 3e+07 Transitions= 3.42e+07 Memory= 6574.726 t= 66 R= 5e+05
Depth= 281 States= 3.1e+07 Transitions= 3.53e+07 Memory= 6789.569 t= 80.6 R= 4e+05
Depth= 281 States= 3.2e+07 Transitions= 3.65e+07 Memory= 7004.511 t= 104 R= 3e+05
Depth= 281 States= 3.3e+07 Transitions= 3.76e+07 Memory= 7219.355 t= 131 R= 3e+05
Depth= 281 States= 3.4e+07 Transitions= 3.88e+07 Memory= 7434.198 t= 158 R= 2e+05

35
ReversalModel/outputs/trace_seq_eq_parallel_2_10_6.txt Normal file
View File

@ -0,0 +1,35 @@
pan: ltl formula seq_eq_parallel
Depth= 281 States= 1e+06 Transitions= 1.14e+06 Memory= 343.573 t= 1.6 R= 6e+05
Depth= 281 States= 2e+06 Transitions= 2.28e+06 Memory= 558.417 t= 3.2 R= 6e+05
Depth= 281 States= 3e+06 Transitions= 3.42e+06 Memory= 773.358 t= 4.77 R= 6e+05
Depth= 281 States= 4e+06 Transitions= 4.56e+06 Memory= 988.202 t= 6.42 R= 6e+05
Depth= 281 States= 5e+06 Transitions= 5.7e+06 Memory= 1203.046 t= 8.23 R= 6e+05
Depth= 281 States= 6e+06 Transitions= 6.84e+06 Memory= 1417.987 t= 10.2 R= 6e+05
Depth= 281 States= 7e+06 Transitions= 7.98e+06 Memory= 1632.831 t= 11.6 R= 6e+05
Depth= 281 States= 8e+06 Transitions= 9.12e+06 Memory= 1847.772 t= 13.1 R= 6e+05
Depth= 281 States= 9e+06 Transitions= 1.03e+07 Memory= 2062.616 t= 14.6 R= 6e+05
Depth= 281 States= 1e+07 Transitions= 1.14e+07 Memory= 2277.460 t= 15.9 R= 6e+05
Depth= 281 States= 1.1e+07 Transitions= 1.25e+07 Memory= 2492.401 t= 17.4 R= 6e+05
Depth= 281 States= 1.2e+07 Transitions= 1.37e+07 Memory= 2707.245 t= 18.9 R= 6e+05
Depth= 281 States= 1.3e+07 Transitions= 1.48e+07 Memory= 2922.089 t= 20.3 R= 6e+05
Depth= 281 States= 1.4e+07 Transitions= 1.6e+07 Memory= 3137.030 t= 21.9 R= 6e+05
Depth= 281 States= 1.5e+07 Transitions= 1.71e+07 Memory= 3351.874 t= 23.8 R= 6e+05
Depth= 281 States= 1.6e+07 Transitions= 1.82e+07 Memory= 3566.815 t= 25.6 R= 6e+05
Depth= 281 States= 1.7e+07 Transitions= 1.94e+07 Memory= 3781.659 t= 28.1 R= 6e+05
Depth= 281 States= 1.8e+07 Transitions= 2.05e+07 Memory= 3996.503 t= 31.8 R= 6e+05
Depth= 281 States= 1.9e+07 Transitions= 2.17e+07 Memory= 4211.444 t= 35.9 R= 5e+05
Depth= 281 States= 2e+07 Transitions= 2.28e+07 Memory= 4426.288 t= 42.4 R= 5e+05
Depth= 281 States= 2.1e+07 Transitions= 2.39e+07 Memory= 4641.132 t= 49.8 R= 4e+05
Depth= 281 States= 2.2e+07 Transitions= 2.51e+07 Memory= 4856.073 t= 58.3 R= 4e+05
Depth= 281 States= 2.3e+07 Transitions= 2.62e+07 Memory= 5070.917 t= 68.6 R= 3e+05
Depth= 281 States= 2.4e+07 Transitions= 2.74e+07 Memory= 5285.858 t= 80.2 R= 3e+05
Depth= 281 States= 2.5e+07 Transitions= 2.85e+07 Memory= 5500.702 t= 92.9 R= 3e+05
Depth= 281 States= 2.6e+07 Transitions= 2.96e+07 Memory= 5715.546 t= 106 R= 2e+05
Depth= 281 States= 2.7e+07 Transitions= 3.08e+07 Memory= 5930.487 t= 121 R= 2e+05
Depth= 281 States= 2.8e+07 Transitions= 3.19e+07 Memory= 6145.331 t= 137 R= 2e+05
Depth= 281 States= 2.9e+07 Transitions= 3.31e+07 Memory= 6360.272 t= 156 R= 2e+05
Depth= 281 States= 3e+07 Transitions= 3.42e+07 Memory= 6575.116 t= 174 R= 2e+05
Depth= 281 States= 3.1e+07 Transitions= 3.53e+07 Memory= 6789.960 t= 195 R= 2e+05
Depth= 281 States= 3.2e+07 Transitions= 3.65e+07 Memory= 7004.901 t= 218 R= 1e+05
Depth= 281 States= 3.3e+07 Transitions= 3.76e+07 Memory= 7219.745 t= 240 R= 1e+05
Depth= 281 States= 3.4e+07 Transitions= 3.88e+07 Memory= 7434.589 t= 267 R= 1e+05

35
ReversalModel/outputs/trace_seq_eq_parallel_2_10_7.txt Normal file
View File

@ -0,0 +1,35 @@
pan: ltl formula seq_eq_parallel
Depth= 281 States= 1e+06 Transitions= 1.14e+06 Memory= 343.573 t= 1.36 R= 7e+05
Depth= 281 States= 2e+06 Transitions= 2.28e+06 Memory= 558.417 t= 2.73 R= 7e+05
Depth= 281 States= 3e+06 Transitions= 3.42e+06 Memory= 773.358 t= 4.05 R= 7e+05
Depth= 281 States= 4e+06 Transitions= 4.56e+06 Memory= 988.202 t= 5.41 R= 7e+05
Depth= 281 States= 5e+06 Transitions= 5.7e+06 Memory= 1203.144 t= 6.8 R= 7e+05
Depth= 281 States= 6e+06 Transitions= 6.84e+06 Memory= 1417.987 t= 8.21 R= 7e+05
Depth= 281 States= 7e+06 Transitions= 7.98e+06 Memory= 1632.929 t= 9.62 R= 7e+05
Depth= 281 States= 8e+06 Transitions= 9.12e+06 Memory= 1847.772 t= 11.1 R= 7e+05
Depth= 281 States= 9e+06 Transitions= 1.03e+07 Memory= 2062.714 t= 13.1 R= 7e+05
Depth= 281 States= 1e+07 Transitions= 1.14e+07 Memory= 2277.558 t= 14.9 R= 7e+05
Depth= 281 States= 1.1e+07 Transitions= 1.25e+07 Memory= 2492.499 t= 17.4 R= 6e+05
Depth= 281 States= 1.2e+07 Transitions= 1.37e+07 Memory= 2707.343 t= 19.8 R= 6e+05
Depth= 281 States= 1.3e+07 Transitions= 1.48e+07 Memory= 2922.284 t= 22 R= 6e+05
Depth= 281 States= 1.4e+07 Transitions= 1.6e+07 Memory= 3137.128 t= 24.5 R= 6e+05
Depth= 281 States= 1.5e+07 Transitions= 1.71e+07 Memory= 3352.069 t= 28.2 R= 5e+05
Depth= 281 States= 1.6e+07 Transitions= 1.82e+07 Memory= 3566.913 t= 31.6 R= 5e+05
Depth= 281 States= 1.7e+07 Transitions= 1.94e+07 Memory= 3781.855 t= 34.8 R= 5e+05
Depth= 281 States= 1.8e+07 Transitions= 2.05e+07 Memory= 3996.698 t= 38.7 R= 5e+05
Depth= 281 States= 1.9e+07 Transitions= 2.17e+07 Memory= 4211.640 t= 42.6 R= 4e+05
Depth= 281 States= 2e+07 Transitions= 2.28e+07 Memory= 4426.483 t= 46.6 R= 4e+05
Depth= 281 States= 2.1e+07 Transitions= 2.39e+07 Memory= 4641.425 t= 51.6 R= 4e+05
Depth= 281 States= 2.2e+07 Transitions= 2.51e+07 Memory= 4856.269 t= 57 R= 4e+05
Depth= 281 States= 2.3e+07 Transitions= 2.62e+07 Memory= 5071.210 t= 63.5 R= 4e+05
Depth= 281 States= 2.4e+07 Transitions= 2.74e+07 Memory= 5286.054 t= 71 R= 3e+05
Depth= 281 States= 2.5e+07 Transitions= 2.85e+07 Memory= 5500.995 t= 80 R= 3e+05
Depth= 281 States= 2.6e+07 Transitions= 2.96e+07 Memory= 5715.839 t= 90.4 R= 3e+05
Depth= 281 States= 2.7e+07 Transitions= 3.08e+07 Memory= 5930.780 t= 102 R= 3e+05
Depth= 281 States= 2.8e+07 Transitions= 3.19e+07 Memory= 6145.624 t= 116 R= 2e+05
Depth= 281 States= 2.9e+07 Transitions= 3.31e+07 Memory= 6360.565 t= 131 R= 2e+05
Depth= 281 States= 3e+07 Transitions= 3.42e+07 Memory= 6575.409 t= 151 R= 2e+05
Depth= 281 States= 3.1e+07 Transitions= 3.53e+07 Memory= 6790.351 t= 170 R= 2e+05
Depth= 281 States= 3.2e+07 Transitions= 3.65e+07 Memory= 7005.194 t= 191 R= 2e+05
Depth= 281 States= 3.3e+07 Transitions= 3.76e+07 Memory= 7220.136 t= 215 R= 2e+05
Depth= 281 States= 3.4e+07 Transitions= 3.88e+07 Memory= 7434.980 t= 238 R= 1e+05

35
ReversalModel/outputs/trace_seq_eq_parallel_2_10_8.txt Normal file
View File

@ -0,0 +1,35 @@
pan: ltl formula seq_eq_parallel
Depth= 281 States= 1e+06 Transitions= 1.14e+06 Memory= 343.573 t= 1.36 R= 7e+05
Depth= 281 States= 2e+06 Transitions= 2.28e+06 Memory= 558.515 t= 2.72 R= 7e+05
Depth= 281 States= 3e+06 Transitions= 3.42e+06 Memory= 773.358 t= 4.12 R= 7e+05
Depth= 281 States= 4e+06 Transitions= 4.56e+06 Memory= 988.300 t= 5.87 R= 7e+05
Depth= 281 States= 5e+06 Transitions= 5.7e+06 Memory= 1203.144 t= 7.72 R= 6e+05
Depth= 281 States= 6e+06 Transitions= 6.84e+06 Memory= 1418.085 t= 9.72 R= 6e+05
Depth= 281 States= 7e+06 Transitions= 7.98e+06 Memory= 1632.929 t= 11.8 R= 6e+05
Depth= 281 States= 8e+06 Transitions= 9.12e+06 Memory= 1847.870 t= 13.8 R= 6e+05
Depth= 281 States= 9e+06 Transitions= 1.03e+07 Memory= 2062.714 t= 15.9 R= 6e+05
Depth= 281 States= 1e+07 Transitions= 1.14e+07 Memory= 2277.655 t= 18.1 R= 6e+05
Depth= 281 States= 1.1e+07 Transitions= 1.25e+07 Memory= 2492.597 t= 20.8 R= 5e+05
Depth= 281 States= 1.2e+07 Transitions= 1.37e+07 Memory= 2707.440 t= 23.6 R= 5e+05
Depth= 281 States= 1.3e+07 Transitions= 1.48e+07 Memory= 2922.382 t= 27.1 R= 5e+05
Depth= 281 States= 1.4e+07 Transitions= 1.6e+07 Memory= 3137.226 t= 30.8 R= 5e+05
Depth= 281 States= 1.5e+07 Transitions= 1.71e+07 Memory= 3352.167 t= 33.5 R= 4e+05
Depth= 281 States= 1.6e+07 Transitions= 1.82e+07 Memory= 3567.011 t= 35.7 R= 4e+05
Depth= 281 States= 1.7e+07 Transitions= 1.94e+07 Memory= 3781.952 t= 37.5 R= 5e+05
Depth= 281 States= 1.8e+07 Transitions= 2.05e+07 Memory= 3996.796 t= 39.3 R= 5e+05
Depth= 281 States= 1.9e+07 Transitions= 2.17e+07 Memory= 4211.737 t= 41.4 R= 5e+05
Depth= 281 States= 2e+07 Transitions= 2.28e+07 Memory= 4426.581 t= 43.7 R= 5e+05
Depth= 281 States= 2.1e+07 Transitions= 2.39e+07 Memory= 4641.522 t= 45.4 R= 5e+05
Depth= 281 States= 2.2e+07 Transitions= 2.51e+07 Memory= 4856.464 t= 47.1 R= 5e+05
Depth= 281 States= 2.3e+07 Transitions= 2.62e+07 Memory= 5071.308 t= 48.7 R= 5e+05
Depth= 281 States= 2.4e+07 Transitions= 2.74e+07 Memory= 5286.249 t= 50.4 R= 5e+05
Depth= 281 States= 2.5e+07 Transitions= 2.85e+07 Memory= 5501.093 t= 52.1 R= 5e+05
Depth= 281 States= 2.6e+07 Transitions= 2.96e+07 Memory= 5716.034 t= 53.7 R= 5e+05
Depth= 281 States= 2.7e+07 Transitions= 3.08e+07 Memory= 5930.878 t= 55.4 R= 5e+05
Depth= 281 States= 2.8e+07 Transitions= 3.19e+07 Memory= 6145.819 t= 57.5 R= 5e+05
Depth= 281 States= 2.9e+07 Transitions= 3.31e+07 Memory= 6360.663 t= 59.8 R= 5e+05
Depth= 281 States= 3e+07 Transitions= 3.42e+07 Memory= 6575.605 t= 64.5 R= 5e+05
Depth= 281 States= 3.1e+07 Transitions= 3.53e+07 Memory= 6790.546 t= 77.7 R= 4e+05
Depth= 281 States= 3.2e+07 Transitions= 3.65e+07 Memory= 7005.390 t= 105 R= 3e+05
Depth= 281 States= 3.3e+07 Transitions= 3.76e+07 Memory= 7220.331 t= 136 R= 2e+05
Depth= 281 States= 3.4e+07 Transitions= 3.88e+07 Memory= 7435.175 t= 166 R= 2e+05

35
ReversalModel/outputs/trace_seq_eq_parallel_2_10_9.txt Normal file
View File

@ -0,0 +1,35 @@
pan: ltl formula seq_eq_parallel
Depth= 281 States= 1e+06 Transitions= 1.14e+06 Memory= 343.573 t= 1.64 R= 6e+05
Depth= 281 States= 2e+06 Transitions= 2.28e+06 Memory= 558.515 t= 3.13 R= 6e+05
Depth= 281 States= 3e+06 Transitions= 3.42e+06 Memory= 773.358 t= 4.62 R= 6e+05
Depth= 281 States= 4e+06 Transitions= 4.56e+06 Memory= 988.300 t= 6.23 R= 6e+05
Depth= 281 States= 5e+06 Transitions= 5.7e+06 Memory= 1203.144 t= 8.02 R= 6e+05
Depth= 281 States= 6e+06 Transitions= 6.84e+06 Memory= 1418.085 t= 9.97 R= 6e+05
Depth= 281 States= 7e+06 Transitions= 7.98e+06 Memory= 1633.026 t= 11.4 R= 6e+05
Depth= 281 States= 8e+06 Transitions= 9.12e+06 Memory= 1847.870 t= 12.9 R= 6e+05
Depth= 281 States= 9e+06 Transitions= 1.03e+07 Memory= 2062.812 t= 14.4 R= 6e+05
Depth= 281 States= 1e+07 Transitions= 1.14e+07 Memory= 2277.655 t= 15.9 R= 6e+05
Depth= 281 States= 1.1e+07 Transitions= 1.25e+07 Memory= 2492.597 t= 17.5 R= 6e+05
Depth= 281 States= 1.2e+07 Transitions= 1.37e+07 Memory= 2707.538 t= 19 R= 6e+05
Depth= 281 States= 1.3e+07 Transitions= 1.48e+07 Memory= 2922.382 t= 20.6 R= 6e+05
Depth= 281 States= 1.4e+07 Transitions= 1.6e+07 Memory= 3137.323 t= 22.1 R= 6e+05
Depth= 281 States= 1.5e+07 Transitions= 1.71e+07 Memory= 3352.167 t= 24.1 R= 6e+05
Depth= 281 States= 1.6e+07 Transitions= 1.82e+07 Memory= 3567.108 t= 26.1 R= 6e+05
Depth= 281 States= 1.7e+07 Transitions= 1.94e+07 Memory= 3782.050 t= 29 R= 6e+05
Depth= 281 States= 1.8e+07 Transitions= 2.05e+07 Memory= 3996.894 t= 32.5 R= 6e+05
Depth= 281 States= 1.9e+07 Transitions= 2.17e+07 Memory= 4211.835 t= 37.8 R= 5e+05
Depth= 281 States= 2e+07 Transitions= 2.28e+07 Memory= 4426.679 t= 44.2 R= 5e+05
Depth= 281 States= 2.1e+07 Transitions= 2.39e+07 Memory= 4641.620 t= 52 R= 4e+05
Depth= 281 States= 2.2e+07 Transitions= 2.51e+07 Memory= 4856.562 t= 61.2 R= 4e+05
Depth= 281 States= 2.3e+07 Transitions= 2.62e+07 Memory= 5071.405 t= 72.3 R= 3e+05
Depth= 281 States= 2.4e+07 Transitions= 2.74e+07 Memory= 5286.347 t= 85.5 R= 3e+05
Depth= 281 States= 2.5e+07 Transitions= 2.85e+07 Memory= 5501.190 t= 98.7 R= 3e+05
Depth= 281 States= 2.6e+07 Transitions= 2.96e+07 Memory= 5716.132 t= 112 R= 2e+05
Depth= 281 States= 2.7e+07 Transitions= 3.08e+07 Memory= 5930.976 t= 128 R= 2e+05
Depth= 281 States= 2.8e+07 Transitions= 3.19e+07 Memory= 6145.917 t= 144 R= 2e+05
Depth= 281 States= 2.9e+07 Transitions= 3.31e+07 Memory= 6360.858 t= 160 R= 2e+05
Depth= 281 States= 3e+07 Transitions= 3.42e+07 Memory= 6575.702 t= 177 R= 2e+05
Depth= 281 States= 3.1e+07 Transitions= 3.53e+07 Memory= 6790.644 t= 195 R= 2e+05
Depth= 281 States= 3.2e+07 Transitions= 3.65e+07 Memory= 7005.487 t= 215 R= 1e+05
Depth= 281 States= 3.3e+07 Transitions= 3.76e+07 Memory= 7220.429 t= 236 R= 1e+05
Depth= 281 States= 3.4e+07 Transitions= 3.88e+07 Memory= 7435.370 t= 259 R= 1e+05

39
ReversalModel/outputs/trace_seq_eq_parallel_2_3_10.txt Normal file
View File

@ -0,0 +1,39 @@
pan: ltl formula seq_eq_parallel
(Spin Version 6.5.2 -- 6 December 2019)
+ Partial Order Reduction
Full statespace search for:
never claim + (seq_eq_parallel)
assertion violations + (if within scope of claim)
acceptance cycles + (fairness disabled)
invalid end states - (disabled by never claim)
State-vector 140 byte, depth reached 141, errors: 0
136294 states, stored
13310 states, matched
149604 transitions (= stored+matched)
0 atomic steps
hash conflicts: 10 (resolved)
Stats on memory usage (in Megabytes):
21.837 equivalent memory usage for states (stored*(State-vector + overhead))
18.066 actual memory usage for states (compression: 82.73%)
state-vector as stored = 111 byte + 28 byte overhead
128.000 memory used for hash table (-w24)
0.534 memory used for DFS stack (-m10000)
146.503 total actual memory usage
unreached in proctype ThreadedReverser
(0 of 15 states)
unreached in init
reversal_seq_eq_parallel_2_3_10.pml:87, state 79, "seq_eq_to_parallel = 0"
reversal_seq_eq_parallel_2_3_10.pml:91, state 89, "-end-"
(2 of 89 states)
unreached in claim seq_eq_parallel
_spin_nvr.tmp:8, state 10, "-end-"
(1 of 10 states)
pan: elapsed time 0.12 seconds
pan: rate 1135783.3 states/second

0
ReversalModel/trace_seq_eq_parallel_2_3_2.txt → ReversalModel/outputs/trace_seq_eq_parallel_2_3_2.txt
View File

0
ReversalModel/trace_seq_eq_parallel_2_3_3.txt → ReversalModel/outputs/trace_seq_eq_parallel_2_3_3.txt
View File

0
ReversalModel/trace_seq_eq_parallel_2_3_4.txt → ReversalModel/outputs/trace_seq_eq_parallel_2_3_4.txt
View File

0
ReversalModel/trace_seq_eq_parallel_2_3_5.txt → ReversalModel/outputs/trace_seq_eq_parallel_2_3_5.txt
View File

0
ReversalModel/trace_seq_eq_parallel_2_3_6.txt → ReversalModel/outputs/trace_seq_eq_parallel_2_3_6.txt
View File

0
ReversalModel/trace_seq_eq_parallel_2_3_7.txt → ReversalModel/outputs/trace_seq_eq_parallel_2_3_7.txt
View File

0
ReversalModel/trace_seq_eq_parallel_2_3_8.txt → ReversalModel/outputs/trace_seq_eq_parallel_2_3_8.txt
View File

39
ReversalModel/outputs/trace_seq_eq_parallel_2_3_9.txt Normal file
View File

@ -0,0 +1,39 @@
pan: ltl formula seq_eq_parallel
(Spin Version 6.5.2 -- 6 December 2019)
+ Partial Order Reduction
Full statespace search for:
never claim + (seq_eq_parallel)
assertion violations + (if within scope of claim)
acceptance cycles + (fairness disabled)
invalid end states - (disabled by never claim)
State-vector 140 byte, depth reached 141, errors: 0
102444 states, stored
10000 states, matched
112444 transitions (= stored+matched)
0 atomic steps
hash conflicts: 4 (resolved)
Stats on memory usage (in Megabytes):
16.413 equivalent memory usage for states (stored*(State-vector + overhead))
13.668 actual memory usage for states (compression: 83.27%)
state-vector as stored = 112 byte + 28 byte overhead
128.000 memory used for hash table (-w24)
0.534 memory used for DFS stack (-m10000)
142.108 total actual memory usage
unreached in proctype ThreadedReverser
(0 of 15 states)
unreached in init
reversal_seq_eq_parallel_2_3_9.pml:87, state 78, "seq_eq_to_parallel = 0"
reversal_seq_eq_parallel_2_3_9.pml:91, state 88, "-end-"
(2 of 88 states)
unreached in claim seq_eq_parallel
_spin_nvr.tmp:8, state 10, "-end-"
(1 of 10 states)
pan: elapsed time 0.09 seconds
pan: rate 1138266.7 states/second

40
ReversalModel/outputs/trace_seq_eq_parallel_2_4_10.txt Normal file
View File

@ -0,0 +1,40 @@
pan: ltl formula seq_eq_parallel
Depth= 161 States= 1e+06 Transitions= 1.11e+06 Memory= 270.624 t= 0.98 R= 1e+06
(Spin Version 6.5.2 -- 6 December 2019)
+ Partial Order Reduction
Full statespace search for:
never claim + (seq_eq_parallel)
assertion violations + (if within scope of claim)
acceptance cycles + (fairness disabled)
invalid end states - (disabled by never claim)
State-vector 156 byte, depth reached 161, errors: 0
1806699 states, stored
190333 states, matched
1997032 transitions (= stored+matched)
0 atomic steps
hash conflicts: 5222 (resolved)
Stats on memory usage (in Megabytes):
317.032 equivalent memory usage for states (stored*(State-vector + overhead))
256.905 actual memory usage for states (compression: 81.03%)
state-vector as stored = 121 byte + 28 byte overhead
128.000 memory used for hash table (-w24)
0.534 memory used for DFS stack (-m10000)
385.175 total actual memory usage
unreached in proctype ThreadedReverser
(0 of 15 states)
unreached in init
reversal_seq_eq_parallel_2_4_10.pml:87, state 79, "seq_eq_to_parallel = 0"
reversal_seq_eq_parallel_2_4_10.pml:91, state 89, "-end-"
(2 of 89 states)
unreached in claim seq_eq_parallel
_spin_nvr.tmp:8, state 10, "-end-"
(1 of 10 states)
pan: elapsed time 1.77 seconds
pan: rate 1020733.9 states/second

0
ReversalModel/trace_seq_eq_parallel_2_4_2.txt → ReversalModel/outputs/trace_seq_eq_parallel_2_4_2.txt
View File

0
ReversalModel/trace_seq_eq_parallel_2_4_3.txt → ReversalModel/outputs/trace_seq_eq_parallel_2_4_3.txt
View File

0
ReversalModel/trace_seq_eq_parallel_2_4_4.txt → ReversalModel/outputs/trace_seq_eq_parallel_2_4_4.txt
View File

0
ReversalModel/trace_seq_eq_parallel_2_4_5.txt → ReversalModel/outputs/trace_seq_eq_parallel_2_4_5.txt
View File

0
ReversalModel/trace_seq_eq_parallel_2_4_6.txt → ReversalModel/outputs/trace_seq_eq_parallel_2_4_6.txt
View File

0
ReversalModel/trace_seq_eq_parallel_2_4_7.txt → ReversalModel/outputs/trace_seq_eq_parallel_2_4_7.txt
View File

0
ReversalModel/trace_seq_eq_parallel_2_4_8.txt → ReversalModel/outputs/trace_seq_eq_parallel_2_4_8.txt
View File

40
ReversalModel/outputs/trace_seq_eq_parallel_2_4_9.txt Normal file
View File

@ -0,0 +1,40 @@
pan: ltl formula seq_eq_parallel
Depth= 161 States= 1e+06 Transitions= 1.11e+06 Memory= 270.624 t= 0.98 R= 1e+06
(Spin Version 6.5.2 -- 6 December 2019)
+ Partial Order Reduction
Full statespace search for:
never claim + (seq_eq_parallel)
assertion violations + (if within scope of claim)
acceptance cycles + (fairness disabled)
invalid end states - (disabled by never claim)
State-vector 156 byte, depth reached 161, errors: 0
1234444 states, stored
130000 states, matched
1364444 transitions (= stored+matched)
0 atomic steps
hash conflicts: 2123 (resolved)
Stats on memory usage (in Megabytes):
216.615 equivalent memory usage for states (stored*(State-vector + overhead))
175.590 actual memory usage for states (compression: 81.06%)
state-vector as stored = 121 byte + 28 byte overhead
128.000 memory used for hash table (-w24)
0.534 memory used for DFS stack (-m10000)
303.925 total actual memory usage
unreached in proctype ThreadedReverser
(0 of 15 states)
unreached in init
reversal_seq_eq_parallel_2_4_9.pml:87, state 78, "seq_eq_to_parallel = 0"
reversal_seq_eq_parallel_2_4_9.pml:91, state 88, "-end-"
(2 of 88 states)
unreached in claim seq_eq_parallel
_spin_nvr.tmp:8, state 10, "-end-"
(1 of 10 states)
pan: elapsed time 1.19 seconds
pan: rate 1037347.9 states/second

63
ReversalModel/outputs/trace_seq_eq_parallel_2_5_10.txt Normal file
View File

@ -0,0 +1,63 @@
pan: ltl formula seq_eq_parallel
Depth= 181 States= 1e+06 Transitions= 1.11e+06 Memory= 285.077 t= 1.09 R= 9e+05
Depth= 181 States= 2e+06 Transitions= 2.23e+06 Memory= 441.522 t= 2.17 R= 9e+05
Depth= 181 States= 3e+06 Transitions= 3.34e+06 Memory= 597.968 t= 3.36 R= 9e+05
Depth= 181 States= 4e+06 Transitions= 4.46e+06 Memory= 754.413 t= 4.45 R= 9e+05
Depth= 181 States= 5e+06 Transitions= 5.57e+06 Memory= 910.761 t= 5.53 R= 9e+05
Depth= 181 States= 6e+06 Transitions= 6.69e+06 Memory= 1067.206 t= 6.61 R= 9e+05
Depth= 181 States= 7e+06 Transitions= 7.8e+06 Memory= 1223.651 t= 7.69 R= 9e+05
Depth= 181 States= 8e+06 Transitions= 8.92e+06 Memory= 1380.097 t= 8.79 R= 9e+05
Depth= 181 States= 9e+06 Transitions= 1e+07 Memory= 1536.444 t= 9.89 R= 9e+05
Depth= 181 States= 1e+07 Transitions= 1.11e+07 Memory= 1692.890 t= 11 R= 9e+05
Depth= 181 States= 1.1e+07 Transitions= 1.23e+07 Memory= 1849.335 t= 12.2 R= 9e+05
Depth= 181 States= 1.2e+07 Transitions= 1.34e+07 Memory= 2005.780 t= 13.4 R= 9e+05
Depth= 181 States= 1.3e+07 Transitions= 1.45e+07 Memory= 2162.128 t= 14.7 R= 9e+05
Depth= 181 States= 1.4e+07 Transitions= 1.56e+07 Memory= 2318.573 t= 16 R= 9e+05
Depth= 181 States= 1.5e+07 Transitions= 1.67e+07 Memory= 2475.019 t= 17.2 R= 9e+05
Depth= 181 States= 1.6e+07 Transitions= 1.78e+07 Memory= 2631.464 t= 18.5 R= 9e+05
Depth= 181 States= 1.7e+07 Transitions= 1.89e+07 Memory= 2787.909 t= 19.7 R= 9e+05
Depth= 181 States= 1.8e+07 Transitions= 2.01e+07 Memory= 2944.257 t= 20.9 R= 9e+05
Depth= 181 States= 1.9e+07 Transitions= 2.12e+07 Memory= 3100.702 t= 22.2 R= 9e+05
Depth= 181 States= 2e+07 Transitions= 2.23e+07 Memory= 3257.147 t= 23.5 R= 9e+05
Depth= 181 States= 2.1e+07 Transitions= 2.34e+07 Memory= 3413.593 t= 25.1 R= 8e+05
Depth= 181 States= 2.2e+07 Transitions= 2.45e+07 Memory= 3569.940 t= 26.6 R= 8e+05
Depth= 181 States= 2.3e+07 Transitions= 2.56e+07 Memory= 3726.386 t= 28 R= 8e+05
(Spin Version 6.5.2 -- 6 December 2019)
+ Partial Order Reduction
Full statespace search for:
never claim + (seq_eq_parallel)
assertion violations + (if within scope of claim)
acceptance cycles + (fairness disabled)
invalid end states - (disabled by never claim)
State-vector 164 byte, depth reached 181, errors: 0
23899968 states, stored
2737867 states, matched
26637835 transitions (= stored+matched)
0 atomic steps
hash conflicts: 3497703 (resolved)
Stats on memory usage (in Megabytes):
4376.215 equivalent memory usage for states (stored*(State-vector + overhead))
3740.948 actual memory usage for states (compression: 85.48%)
state-vector as stored = 136 byte + 28 byte overhead
128.000 memory used for hash table (-w24)
0.534 memory used for DFS stack (-m10000)
2.276 memory lost to fragmentation
3867.206 total actual memory usage
unreached in proctype ThreadedReverser
(0 of 15 states)
unreached in init
reversal_seq_eq_parallel_2_5_10.pml:87, state 79, "seq_eq_to_parallel = 0"
reversal_seq_eq_parallel_2_5_10.pml:91, state 89, "-end-"
(2 of 89 states)
unreached in claim seq_eq_parallel
_spin_nvr.tmp:8, state 10, "-end-"
(1 of 10 states)
pan: elapsed time 29.2 seconds
pan: rate 817372.37 states/second

0
ReversalModel/trace_seq_eq_parallel_2_5_2.txt → ReversalModel/outputs/trace_seq_eq_parallel_2_5_2.txt
View File

0
ReversalModel/trace_seq_eq_parallel_2_5_3.txt → ReversalModel/outputs/trace_seq_eq_parallel_2_5_3.txt
View File

0
ReversalModel/trace_seq_eq_parallel_2_5_4.txt → ReversalModel/outputs/trace_seq_eq_parallel_2_5_4.txt
View File

0
ReversalModel/trace_seq_eq_parallel_2_5_5.txt → ReversalModel/outputs/trace_seq_eq_parallel_2_5_5.txt
View File

0
ReversalModel/trace_seq_eq_parallel_2_5_6.txt → ReversalModel/outputs/trace_seq_eq_parallel_2_5_6.txt
View File

0
ReversalModel/trace_seq_eq_parallel_2_5_7.txt → ReversalModel/outputs/trace_seq_eq_parallel_2_5_7.txt
View File

0
ReversalModel/trace_seq_eq_parallel_2_5_8.txt → ReversalModel/outputs/trace_seq_eq_parallel_2_5_8.txt
View File

54
ReversalModel/outputs/trace_seq_eq_parallel_2_5_9.txt Normal file
View File

@ -0,0 +1,54 @@
pan: ltl formula seq_eq_parallel
Depth= 181 States= 1e+06 Transitions= 1.11e+06 Memory= 285.077 t= 1.01 R= 1e+06
Depth= 181 States= 2e+06 Transitions= 2.23e+06 Memory= 441.522 t= 2.08 R= 1e+06
Depth= 181 States= 3e+06 Transitions= 3.34e+06 Memory= 597.870 t= 3.15 R= 1e+06
Depth= 181 States= 4e+06 Transitions= 4.46e+06 Memory= 754.315 t= 4.33 R= 9e+05
Depth= 181 States= 5e+06 Transitions= 5.57e+06 Memory= 910.663 t= 5.39 R= 9e+05
Depth= 181 States= 6e+06 Transitions= 6.69e+06 Memory= 1067.108 t= 6.47 R= 9e+05
Depth= 181 States= 7e+06 Transitions= 7.8e+06 Memory= 1223.554 t= 7.53 R= 9e+05
Depth= 181 States= 8e+06 Transitions= 8.92e+06 Memory= 1379.901 t= 8.6 R= 9e+05
Depth= 181 States= 9e+06 Transitions= 1e+07 Memory= 1536.347 t= 9.69 R= 9e+05
Depth= 181 States= 1e+07 Transitions= 1.11e+07 Memory= 1692.694 t= 10.8 R= 9e+05
Depth= 181 States= 1.1e+07 Transitions= 1.23e+07 Memory= 1849.140 t= 11.9 R= 9e+05
Depth= 181 States= 1.2e+07 Transitions= 1.34e+07 Memory= 2005.585 t= 13.1 R= 9e+05
Depth= 181 States= 1.3e+07 Transitions= 1.45e+07 Memory= 2161.933 t= 14.2 R= 9e+05
Depth= 181 States= 1.4e+07 Transitions= 1.56e+07 Memory= 2318.378 t= 15.6 R= 9e+05
(Spin Version 6.5.2 -- 6 December 2019)
+ Partial Order Reduction
Full statespace search for:
never claim + (seq_eq_parallel)
assertion violations + (if within scope of claim)
acceptance cycles + (fairness disabled)
invalid end states - (disabled by never claim)
State-vector 164 byte, depth reached 181, errors: 0
14844444 states, stored
1700000 states, matched
16544444 transitions (= stored+matched)
0 atomic steps
hash conflicts: 1017569 (resolved)
Stats on memory usage (in Megabytes):
2718.099 equivalent memory usage for states (stored*(State-vector + overhead))
2323.205 actual memory usage for states (compression: 85.47%)
state-vector as stored = 136 byte + 28 byte overhead
128.000 memory used for hash table (-w24)
0.534 memory used for DFS stack (-m10000)
1.330 memory lost to fragmentation
2450.409 total actual memory usage
unreached in proctype ThreadedReverser
(0 of 15 states)
unreached in init
reversal_seq_eq_parallel_2_5_9.pml:87, state 78, "seq_eq_to_parallel = 0"
reversal_seq_eq_parallel_2_5_9.pml:91, state 88, "-end-"
(2 of 88 states)
unreached in claim seq_eq_parallel
_spin_nvr.tmp:8, state 10, "-end-"
(1 of 10 states)
pan: elapsed time 16.6 seconds
pan: rate 894243.61 states/second

35
ReversalModel/outputs/trace_seq_eq_parallel_2_6_10.txt Normal file
View File

@ -0,0 +1,35 @@
pan: ltl formula seq_eq_parallel
Depth= 201 States= 1e+06 Transitions= 1.12e+06 Memory= 295.429 t= 1.19 R= 8e+05
Depth= 201 States= 2e+06 Transitions= 2.24e+06 Memory= 462.128 t= 2.38 R= 8e+05
Depth= 201 States= 3e+06 Transitions= 3.36e+06 Memory= 628.925 t= 3.53 R= 8e+05
Depth= 201 States= 4e+06 Transitions= 4.48e+06 Memory= 795.624 t= 4.7 R= 9e+05
Depth= 201 States= 5e+06 Transitions= 5.6e+06 Memory= 962.323 t= 5.91 R= 8e+05
Depth= 201 States= 6e+06 Transitions= 6.72e+06 Memory= 1129.120 t= 7.3 R= 8e+05
Depth= 201 States= 7e+06 Transitions= 7.84e+06 Memory= 1295.819 t= 8.83 R= 8e+05
Depth= 201 States= 8e+06 Transitions= 8.96e+06 Memory= 1462.616 t= 10.3 R= 8e+05
Depth= 201 States= 9e+06 Transitions= 1.01e+07 Memory= 1629.315 t= 11.7 R= 8e+05
Depth= 201 States= 1e+07 Transitions= 1.12e+07 Memory= 1796.015 t= 13.1 R= 8e+05
Depth= 201 States= 1.1e+07 Transitions= 1.23e+07 Memory= 1962.812 t= 14.3 R= 8e+05
Depth= 201 States= 1.2e+07 Transitions= 1.34e+07 Memory= 2129.511 t= 15.7 R= 8e+05
Depth= 201 States= 1.3e+07 Transitions= 1.46e+07 Memory= 2296.308 t= 17 R= 8e+05
Depth= 201 States= 1.4e+07 Transitions= 1.57e+07 Memory= 2463.007 t= 18.3 R= 8e+05
Depth= 201 States= 1.5e+07 Transitions= 1.68e+07 Memory= 2629.804 t= 19.6 R= 8e+05
Depth= 201 States= 1.6e+07 Transitions= 1.79e+07 Memory= 2796.503 t= 21 R= 8e+05
Depth= 201 States= 1.7e+07 Transitions= 1.9e+07 Memory= 2963.202 t= 22.3 R= 8e+05
Depth= 201 States= 1.8e+07 Transitions= 2.02e+07 Memory= 3129.999 t= 23.7 R= 8e+05
Depth= 201 States= 1.9e+07 Transitions= 2.13e+07 Memory= 3296.698 t= 25.3 R= 8e+05
Depth= 201 States= 2e+07 Transitions= 2.24e+07 Memory= 3463.495 t= 27.1 R= 7e+05
Depth= 201 States= 2.1e+07 Transitions= 2.35e+07 Memory= 3630.194 t= 30 R= 7e+05
Depth= 201 States= 2.2e+07 Transitions= 2.46e+07 Memory= 3796.894 t= 32.2 R= 7e+05
Depth= 201 States= 2.3e+07 Transitions= 2.58e+07 Memory= 3963.690 t= 34.1 R= 7e+05
Depth= 201 States= 2.4e+07 Transitions= 2.69e+07 Memory= 4130.390 t= 37.9 R= 6e+05
Depth= 201 States= 2.5e+07 Transitions= 2.8e+07 Memory= 4297.187 t= 42.9 R= 6e+05
Depth= 201 States= 2.6e+07 Transitions= 2.91e+07 Memory= 4463.886 t= 49.3 R= 5e+05
Depth= 201 States= 2.7e+07 Transitions= 3.03e+07 Memory= 4630.585 t= 58.3 R= 5e+05
Depth= 201 States= 2.8e+07 Transitions= 3.14e+07 Memory= 4797.382 t= 71.7 R= 4e+05
Depth= 201 States= 2.9e+07 Transitions= 3.25e+07 Memory= 4964.081 t= 85.2 R= 3e+05
Depth= 201 States= 3e+07 Transitions= 3.36e+07 Memory= 5130.878 t= 102 R= 3e+05
Depth= 201 States= 3.1e+07 Transitions= 3.47e+07 Memory= 5297.577 t= 118 R= 3e+05
Depth= 201 States= 3.2e+07 Transitions= 3.59e+07 Memory= 5464.276 t= 134 R= 2e+05
Depth= 201 States= 3.3e+07 Transitions= 3.7e+07 Memory= 5631.073 t= 152 R= 2e+05
Depth= 201 States= 3.4e+07 Transitions= 3.81e+07 Memory= 5797.772 t= 171 R= 2e+05

0
ReversalModel/trace_seq_eq_parallel_2_6_2.txt → ReversalModel/outputs/trace_seq_eq_parallel_2_6_2.txt
View File

0
ReversalModel/trace_seq_eq_parallel_2_6_3.txt → ReversalModel/outputs/trace_seq_eq_parallel_2_6_3.txt
View File

0
ReversalModel/trace_seq_eq_parallel_2_6_4.txt → ReversalModel/outputs/trace_seq_eq_parallel_2_6_4.txt
View File

0
ReversalModel/trace_seq_eq_parallel_2_6_5.txt → ReversalModel/outputs/trace_seq_eq_parallel_2_6_5.txt
View File

0
ReversalModel/trace_seq_eq_parallel_2_6_6.txt → ReversalModel/outputs/trace_seq_eq_parallel_2_6_6.txt
View File

0
ReversalModel/trace_seq_eq_parallel_2_6_7.txt → ReversalModel/outputs/trace_seq_eq_parallel_2_6_7.txt
View File

0
ReversalModel/trace_seq_eq_parallel_2_6_8.txt → ReversalModel/outputs/trace_seq_eq_parallel_2_6_8.txt
View File

Some files were not shown because too many files have changed in this diff Show More