forked from IreneRosadi/UppaalModels
-
Notifications
You must be signed in to change notification settings - Fork 0
/
modelFastVerification.log
63 lines (63 loc) · 3.24 KB
/
modelFastVerification.log
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
Options for the verification:
Generating no trace
Search order is breadth first
Using conservative space optimisation
Seed is 1618771240
State space representation uses minimal constraint systems
[2K
Verifying formula 1 at /nta/queries/query[1]/formula
[2K -- Formula is satisfied.
(29 runs) Pr(<> ...) in [0,0.0981446]
with confidence 0.95.
[2K
Verifying formula 2 at /nta/queries/query[2]/formula
-- Throughput: 359 states/sec, Load: 389 runs[K
[2K -- Formula is satisfied.
(29 runs) Pr(<> ...) in [0,0.0981446]
with confidence 0.95.
[2K
Verifying formula 3 at /nta/queries/query[3]/formula
-- Throughput: 186 states/sec, Load: 389 runs[K
[2K -- Formula is satisfied.
(29 runs) Pr(<> ...) in [0.901855,1]
with confidence 0.95.
Values in [10.0022,284.051] mean=93.218 steps=2.74049: 1 0 0 2 2 0 0 0 0 1 3 0 0 1 0 0 1 0 0 1 0 0 1 0 0 0 0 0 0 0 1 2 2 0 0 1 2 0 1 0 0 1 1 0 0 0 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 0 0 0 0 0 0 0 0 0 0 0 0 0 2 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1
[2K
Verifying formula 4 at /nta/queries/query[4]/formula
-- Throughput: 178 states/sec, Load: 389 runs[K
[2K -- Formula is satisfied.
(54 runs) Pr(<> ...) in [0.000468738,0.0989152]
with confidence 0.95.
Values in [186.38,186.38] mean=186.38 steps=2.22045e-16: 1
[2K
Verifying formula 5 at /nta/queries/query[5]/formula
-- Throughput: 99 states/sec, Load: 388 runs[K
[2K -- Formula is satisfied.
(88 runs) Pr(<> ...) in [0.887691,0.987478]
with confidence 0.95.
Values in [11.4497,964.528] mean=279.295 steps=9.53078: 2 1 1 4 1 2 4 2 1 4 3 0 2 2 1 2 0 4 0 0 4 1 1 2 3 3 2 0 0 0 0 1 0 2 1 0 0 2 1 0 3 0 2 1 0 1 3 0 1 1 1 0 0 1 1 2 0 0 0 1 0 0 0 0 2 0 0 0 0 0 1 0 0 0 0 1 0 0 0 0 0 0 0 0 0 1 0 0 0 0 0 0 0 0 0 1 0 0 0 1
[2K
Verifying formula 6 at /nta/queries/query[6]/formula
-- Throughput: 80 states/sec, Load: 389 runs[K
[2K -- Formula is satisfied.
(68 runs) Pr(<> ...) in [0.897759,0.996418]
with confidence 0.95.
Values in [19.8041,999.761] mean=316.4 steps=9.79957: 2 0 1 3 1 1 1 1 2 2 1 2 2 1 0 3 1 0 2 0 0 2 1 0 3 0 4 1 2 0 0 0 2 3 4 0 1 0 0 1 1 1 0 0 0 1 2 0 1 0 0 0 0 0 0 0 0 0 1 0 1 0 0 0 1 0 1 0 0 0 0 0 0 1 0 0 0 0 0 0 1 0 0 0 0 0 0 1 0 1 0 0 0 0 1 0 0 0 0 1
[2K
Verifying formula 7 at /nta/queries/query[7]/formula
-- Throughput: 95 states/sec, Load: 389 runs[K
[2K -- Formula is satisfied.
(68 runs) Pr(<> ...) in [0.00358196,0.102241]
with confidence 0.95.
Values in [120.529,304.919] mean=212.724 steps=1.84391: 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1
[2K
Verifying formula 8 at /nta/queries/query[8]/formula
-- Throughput: 26 states/sec, Load: 389 runs[K
-- Throughput: 139276 states/sec, Load: 286 runs[K
-- Throughput: 25078 states/sec, Load: 213 runs[K
-- Throughput: 136701 states/sec, Load: 118 runs[K
-- Throughput: 24353 states/sec, Load: 49 runs[K
[2K -- Formula is satisfied.
(394 runs) Pr(<> ...) in [0.379491,0.479453]
with confidence 0.95.
Values in [21.9778,998.735] mean=551.001 steps=9.76757: 1 1 0 0 1 0 1 1 1 2 0 3 2 0 2 2 4 0 0 1 1 2 2 3 1 0 1 3 8 2 0 3 1 2 0 1 1 0 0 0 3 2 2 0 0 4 1 2 4 1 3 4 3 3 1 1 1 2 4 1 1 3 2 2 1 2 2 1 5 2 2 0 3 2 1 4 1 2 2 3 1 1 1 2 1 1 1 1 1 0 2 1 2 1 3 0 5 4 3 2