PRISM
=====
Version: 4.4.dev
Date: Mon Dec 10 22:46:40 CET 2018
Hostname: qcomp2019
Memory limits: cudd=1g, java(heap)=1g
Command line: prism --javamaxmem 11g speed-ind.prism speed-ind.props --property change_state -const T=2100 -sparse
Parsing model file "speed-ind.prism"...
Parsing properties file "speed-ind.props"...
1 property:
(1) "change_state": P=? [ F<=T ((S2>80)&(S3<20)) ]
Type: CTMC
Modules: S1_def S2_def S3_def S4_def Y_def Z_def CC_def XX_def
Variables: S1 S2 S3 S4 Y Z CC XX
---------------------------------------------------------------------
Model checking: "change_state": P=? [ F<=T ((S2>80)&(S3<20)) ]
Property constants: T=2100
Building model...
Computing reachable states...
Reachability (BFS): 38 iterations in 1.16 seconds (average 0.030553, setup 0.00)
Time for model construction: 32.95 seconds.
Type: CTMC
States: 743424 (1 initial)
Transitions: 9518080
Rate matrix: 33024 nodes (187 terminal), 9518080 minterms, vars: 58r/58c
Computing probabilities...
Engine: Sparse
Number of non-absorbing states: 718848 of 743424 (96.7%)
Building sparse matrix... [n=743424, nnz=9219072, compact] [35.9 MB]
Creating vector for diagonals... [5.7 MB]
Allocating iteration vectors... [3 x 5.7 MB]
TOTAL: [58.6 MB]
Uniformisation: q.t = 2.797911 x 2100.000000 = 5875.612619
Fox-Glynn: left = 5336, right = 6527
Starting iterations...
Iteration 169 (of 6527): max relative diff=0.067337, 5.01 sec so far
Iteration 338 (of 6527): max relative diff=0.028572, 10.03 sec so far
Iteration 507 (of 6527): max relative diff=0.015573, 15.06 sec so far
Iteration 676 (of 6527): max relative diff=0.009276, 20.08 sec so far
Iteration 845 (of 6527): max relative diff=0.005811, 25.11 sec so far
Iteration 1014 (of 6527): max relative diff=0.003935, 30.13 sec so far
Iteration 1183 (of 6527): max relative diff=0.002993, 35.14 sec so far
Iteration 1352 (of 6527): max relative diff=0.002348, 40.17 sec so far
Iteration 1521 (of 6527): max relative diff=0.001889, 45.20 sec so far
Iteration 1690 (of 6527): max relative diff=0.001551, 50.22 sec so far
Iteration 1859 (of 6527): max relative diff=0.001298, 55.25 sec so far
Iteration 2028 (of 6527): max relative diff=0.001103, 60.27 sec so far
Iteration 2194 (of 6527): max relative diff=0.000954, 65.30 sec so far
Iteration 2363 (of 6527): max relative diff=0.000834, 70.32 sec so far
Iteration 2532 (of 6527): max relative diff=0.000738, 75.34 sec so far
Iteration 2701 (of 6527): max relative diff=0.000660, 80.37 sec so far
Iteration 2870 (of 6527): max relative diff=0.000596, 85.39 sec so far
Iteration 3039 (of 6527): max relative diff=0.000542, 90.42 sec so far
Iteration 3208 (of 6527): max relative diff=0.000497, 95.45 sec so far
Iteration 3376 (of 6527): max relative diff=0.000458, 100.45 sec so far
Iteration 3545 (of 6527): max relative diff=0.000425, 105.46 sec so far
Iteration 3714 (of 6527): max relative diff=0.000396, 110.48 sec so far
Iteration 3881 (of 6527): max relative diff=0.000371, 115.49 sec so far
Iteration 4050 (of 6527): max relative diff=0.000349, 120.52 sec so far
Iteration 4219 (of 6527): max relative diff=0.000329, 125.54 sec so far
Iteration 4388 (of 6527): max relative diff=0.000311, 130.55 sec so far
Iteration 4557 (of 6527): max relative diff=0.000295, 135.57 sec so far
Iteration 4726 (of 6527): max relative diff=0.000281, 140.59 sec so far
Iteration 4895 (of 6527): max relative diff=0.000268, 145.60 sec so far
Iteration 5063 (of 6527): max relative diff=0.000256, 150.62 sec so far
Iteration 5228 (of 6527): max relative diff=0.000245, 155.64 sec so far
Iteration 5394 (of 6527): max relative diff=0.000235, 160.66 sec so far
Iteration 5557 (of 6527): max relative diff=0.000226, 165.69 sec so far
Iteration 5720 (of 6527): max relative diff=0.000218, 170.70 sec so far
Iteration 5883 (of 6527): max relative diff=0.000210, 175.73 sec so far
Iteration 6046 (of 6527): max relative diff=0.000203, 180.76 sec so far
Iteration 6208 (of 6527): max relative diff=0.000196, 185.76 sec so far
Iteration 6370 (of 6527): max relative diff=0.000190, 190.77 sec so far
Iterative method: 6527 iterations in 206.12 seconds (average 0.029992, setup 10.36)
Value in the initial state: 0.042294497978464705
Time for model checking: 206.292 seconds.
Result: 0.042294497978464705 (value in the initial state)
Overall running time: 239.875 seconds.