PaperModel/ 000755 000765 000024 00000000000 12647702321 013237 5 ustar 00ruth staff 000000 000000 PaperModel/.git/ 000755 000765 000024 00000000000 12647702373 014107 5 ustar 00ruth staff 000000 000000 PaperModel/README.md 000644 000765 000024 00000003450 12647702321 014520 0 ustar 00ruth staff 000000 000000 Prism Models
------------
In all models scenario 2 can be recreated by uncommenting the lines ending with //Scenario 2 and commenting the lines ending with //Scenario 1.
These lines are
const int Miss = 900; // Scenario 1
//const int Miss = 900; // Scenario 2
and
NoOfObjs : [0..3] init 3; // Scenario 1
// NoOfObjs : [0..3] init 3; // Scenario 2
uav_dtmc.prism
--------------
Contains the discrete time markov chain model of the scenario, where the transitions are chosen uniform randomly.
uav_mdp.prism
-------------
Contains the markov decision process model of the scenario. The non-determinism will return maximal and minimal results.
uav_rounded_mdp.prism
---------------------
Non-deterministic markov decision process model of the scenario, where all constants have been rounded manually.
Property Files
--------------
uav_mdp.props
-------------
Contains some properties that are of interest to the models.
uav_mdp.bounded.props
---------------------
Contains the time bound properties needed for the graphs.
Results Files
-------------
result_uav_mdp.txt
------------------
Log file from running all properties in uav_mdp.props against the model in Scenario 1 in uav_mdp.prism.
summary_result_uav_mdp.txt
--------------------------
Summary file containing just the most important information about the properties.
(The columns are; Name, Probability, Time to check, RAM needed for matrix)
Graphs
------
uav_deadline1.gra
-----------------
Prism graph file, containing information from running Scenario 1.
uav_deadline1.pdf
-----------------
Graph resulting from running Scenario 1, produced by prism.
uav_deadline2.gra
-----------------
Prism graph file, containing information from running Scenario 2.
uav_deadline2.pdf
-----------------
Graph resulting from running Scenario 2, produced by prism.
PaperModel/result_uav_mdp.txt 000644 000765 000024 00000224211 12647406661 017043 0 ustar 00ruth staff 000000 000000 PRISM
=====
Version: 4.3.beta
Date: Thu Jan 14 23:41:21 GMT 2016
Hostname: Bubbly.home
Memory limits: cudd=1g, java(heap)=910.5m
Command line: prism uav_mdp.prism -s uav_mdp.props
Parsing model file "uav_mdp.prism"...
Parsing properties file "uav_mdp.props"...
19 properties:
(1) Pmax=? [ F "MissionSuccessful" ]
(2) Pmin=? [ F "MissionSuccessful" ]
(3) Pmax=? [ F "MissionTimeUp" ]
(4) Pmin=? [ F "MissionTimeUp" ]
(5) Pmax=? [ F "Crash" ]
(6) Pmin=? [ F "Crash" ]
(7) Pmax=? [ F "AllAreaSearched" ]
(8) Pmin=? [ F "AllAreaSearched" ]
(9) Pmax=? [ F "MissionTimeUp"|"AllAreaSearched"|"Crash" ]
(10) Pmin=? [ F "MissionTimeUp"|"AllAreaSearched"|"Crash" ]
(11) filter(print, "deadlock", true)
(12) R{"drop"}max=? [ F "deadlock" ]
(13) R{"drop"}min=? [ F "deadlock" ]
(14) R{"charge"}max=? [ F "deadlock" ]
(15) R{"charge"}min=? [ F "deadlock" ]
(16) R{"time"}max=? [ F "deadlock" ]
(17) R{"time"}min=? [ F "deadlock" ]
(18) R{"success"}max=? [ F "deadlock" ]/Pmin=? [ F "MissionSuccessful" ]
(19) R{"success"}min=? [ F "deadlock" ]/Pmax=? [ F "MissionSuccessful" ]
Type: MDP
Modules: Obj Move Robot T
Variables: NoOfObjs posx posy s1 retx rety b t c
---------------------------------------------------------------------
Model checking: Pmax=? [ F "MissionSuccessful" ]
Building model...
Warning: Update 2 of command 9 of module "T" doesn't do anything ("(c'=1)", line 274, column 112)
Warning: Guard for command 10 of module "T" is never satisfied.
Warning: Update 2 of command 27 of module "T" doesn't do anything ("(c'=1)", line 297, column 108)
Warning: Guard for command 28 of module "T" is never satisfied.
Warning: Update 2 of command 47 of module "T" doesn't do anything ("(c'=1)", line 324, column 113)
Warning: Guard for command 48 of module "T" is never satisfied.
Computing reachable states...
Reachability (BFS): 166 iterations in 294.98 seconds (average 1.776994, setup 0.00)
Time for model construction: 488.044 seconds.
Warning: Deadlocks detected and fixed in 1 states
Type: MDP
States: 116191709 (1 initial)
Transitions: 290191121
Choices: 153547098
Transition matrix: 446910 nodes (133 terminal), 290191121 minterms, vars: 37r/37c/17nd
Prob0A: 81 iterations in 18.98 seconds (average 0.234321, setup 0.00)
Prob1E: 4 iterations in 0.91 seconds (average 0.226500, setup 0.00)
yes = 82818, no = 72159702, maybe = 43949189
Computing remaining probabilities...
Engine: Sparse
Building sparse matrix... [n=116191709, nc=71940167, nnz=174316066, k=2] [2.1 GB]
Creating vector for yes... [886.5 MB]
Allocating iteration vectors... [2 x 886.5 MB]
TOTAL: [4.7 GB]
Starting iterations...
Iteration 3: max relative diff=1.000000, 5.02 sec so far
Iteration 7: max relative diff=1.000000, 11.61 sec so far
Iteration 11: max relative diff=1.000000, 18.07 sec so far
Iteration 15: max relative diff=1.000000, 24.82 sec so far
Iteration 19: max relative diff=1.000000, 31.29 sec so far
Iteration 23: max relative diff=1.000000, 37.88 sec so far
Iteration 26: max relative diff=1.000000, 42.92 sec so far
Iteration 29: max relative diff=1.000000, 48.28 sec so far
Iteration 32: max relative diff=1.000000, 53.36 sec so far
Iteration 36: max relative diff=1.000000, 59.72 sec so far
Iteration 40: max relative diff=1.000000, 66.43 sec so far
Iteration 43: max relative diff=1.000000, 71.69 sec so far
Iteration 46: max relative diff=1.000000, 76.86 sec so far
Iteration 49: max relative diff=1.000000, 81.98 sec so far
Iteration 53: max relative diff=1.000000, 88.62 sec so far
Iteration 56: max relative diff=1.000000, 93.79 sec so far
Iteration 59: max relative diff=1.000000, 99.44 sec so far
Iteration 63: max relative diff=1.000000, 106.14 sec so far
Iteration 66: max relative diff=1.000000, 111.38 sec so far
Iteration 69: max relative diff=1.000000, 116.48 sec so far
Iteration 73: max relative diff=1.000000, 123.03 sec so far
Iteration 77: max relative diff=1.000000, 129.53 sec so far
Iteration 81: max relative diff=0.461494, 136.00 sec so far
Iteration 85: max relative diff=0.204179, 142.43 sec so far
Iteration 89: max relative diff=0.132162, 148.83 sec so far
Iteration 92: max relative diff=0.094611, 155.11 sec so far
Iteration 94: max relative diff=0.070982, 160.61 sec so far
Iteration 97: max relative diff=0.051260, 167.36 sec so far
Iteration 100: max relative diff=0.024506, 173.03 sec so far
Iteration 103: max relative diff=0.011646, 178.24 sec so far
Iteration 106: max relative diff=0.005073, 183.29 sec so far
Iteration 110: max relative diff=0.001386, 189.65 sec so far
Iteration 114: max relative diff=0.000336, 196.06 sec so far
Iteration 118: max relative diff=0.000063, 202.43 sec so far
Iteration 122: max relative diff=0.000008, 208.61 sec so far
Iteration 126: max relative diff=0.000001, 214.66 sec so far
Iterative method: 126 iterations in 287.76 seconds (average 1.703659, setup 73.10)
Value in the initial state: 0.7610284756344345
Time for model checking: 324.671 seconds.
Result: 0.7610284756344345 (value in the initial state)
---------------------------------------------------------------------
Model checking: Pmin=? [ F "MissionSuccessful" ]
Prob0E: 89 iterations in 23.19 seconds (average 0.260607, setup 0.00)
Prob1A: 4 iterations in 1.14 seconds (average 0.285750, setup 0.00)
yes = 82818, no = 76902300, maybe = 39206591
Computing remaining probabilities...
Engine: Sparse
Building sparse matrix... [n=116191709, nc=64081283, nnz=155549122, k=2] [1.9 GB]
Creating vector for yes... [886.5 MB]
Allocating iteration vectors... [2 x 886.5 MB]
TOTAL: [4.5 GB]
Starting iterations...
Iteration 4: max relative diff=1.000000, 5.78 sec so far
Iteration 8: max relative diff=1.000000, 11.36 sec so far
Iteration 12: max relative diff=1.000000, 16.97 sec so far
Iteration 16: max relative diff=1.000000, 22.63 sec so far
Iteration 20: max relative diff=1.000000, 28.33 sec so far
Iteration 24: max relative diff=1.000000, 34.48 sec so far
Iteration 28: max relative diff=1.000000, 40.53 sec so far
Iteration 32: max relative diff=1.000000, 46.84 sec so far
Iteration 36: max relative diff=1.000000, 52.92 sec so far
Iteration 40: max relative diff=1.000000, 59.12 sec so far
Iteration 44: max relative diff=1.000000, 65.56 sec so far
Iteration 48: max relative diff=1.000000, 71.95 sec so far
Iteration 52: max relative diff=1.000000, 78.03 sec so far
Iteration 56: max relative diff=1.000000, 84.17 sec so far
Iteration 60: max relative diff=1.000000, 90.50 sec so far
Iteration 64: max relative diff=1.000000, 97.06 sec so far
Iteration 67: max relative diff=1.000000, 102.31 sec so far
Iteration 71: max relative diff=1.000000, 108.89 sec so far
Iteration 75: max relative diff=1.000000, 115.21 sec so far
Iteration 79: max relative diff=1.000000, 121.36 sec so far
Iteration 83: max relative diff=1.000000, 127.45 sec so far
Iteration 87: max relative diff=1.000000, 133.46 sec so far
Iteration 91: max relative diff=0.509941, 139.54 sec so far
Iteration 94: max relative diff=0.344297, 145.28 sec so far
Iteration 98: max relative diff=0.302600, 151.30 sec so far
Iteration 102: max relative diff=0.126808, 157.20 sec so far
Iteration 106: max relative diff=0.068875, 163.09 sec so far
Iteration 110: max relative diff=0.027426, 168.99 sec so far
Iteration 114: max relative diff=0.013191, 174.88 sec so far
Iteration 118: max relative diff=0.004647, 180.76 sec so far
Iteration 122: max relative diff=0.000795, 186.55 sec so far
Iteration 126: max relative diff=0.000100, 192.34 sec so far
Iteration 130: max relative diff=0.000062, 198.19 sec so far
Iteration 134: max relative diff=0.000012, 203.98 sec so far
Iteration 138: max relative diff=0.000001, 209.69 sec so far
Iterative method: 139 iterations in 272.19 seconds (average 1.518734, setup 61.09)
Value in the initial state: 0.6787083686458641
Time for model checking: 301.359 seconds.
Result: 0.6787083686458641 (value in the initial state)
---------------------------------------------------------------------
Model checking: Pmax=? [ F "MissionTimeUp" ]
Prob0A: 95 iterations in 30.86 seconds (average 0.324842, setup 0.00)
Prob1E: 4 iterations in 0.38 seconds (average 0.094000, setup 0.00)
yes = 26535, no = 62542664, maybe = 53622510
Computing remaining probabilities...
Engine: Sparse
Building sparse matrix... [n=116191709, nc=88252519, nnz=216031546, k=2] [2.6 GB]
Creating vector for yes... [886.5 MB]
Allocating iteration vectors... [2 x 886.5 MB]
TOTAL: [5.2 GB]
Starting iterations...
Iteration 3: max relative diff=1.000000, 5.17 sec so far
Iteration 6: max relative diff=1.000000, 10.20 sec so far
Iteration 9: max relative diff=1.000000, 15.22 sec so far
Iteration 12: max relative diff=1.000000, 20.31 sec so far
Iteration 15: max relative diff=1.000000, 25.38 sec so far
Iteration 18: max relative diff=1.000000, 30.49 sec so far
Iteration 21: max relative diff=1.000000, 35.63 sec so far
Iteration 24: max relative diff=1.000000, 40.79 sec so far
Iteration 27: max relative diff=1.000000, 45.97 sec so far
Iteration 30: max relative diff=1.000000, 51.18 sec so far
Iteration 33: max relative diff=1.000000, 56.35 sec so far
Iteration 36: max relative diff=1.000000, 61.57 sec so far
Iteration 39: max relative diff=1.000000, 66.78 sec so far
Iteration 42: max relative diff=1.000000, 72.01 sec so far
Iteration 45: max relative diff=1.000000, 77.27 sec so far
Iteration 48: max relative diff=1.000000, 82.56 sec so far
Iteration 51: max relative diff=1.000000, 87.89 sec so far
Iteration 54: max relative diff=1.000000, 93.22 sec so far
Iteration 57: max relative diff=1.000000, 98.60 sec so far
Iteration 60: max relative diff=1.000000, 103.95 sec so far
Iteration 63: max relative diff=1.000000, 109.40 sec so far
Iteration 66: max relative diff=1.000000, 114.81 sec so far
Iteration 69: max relative diff=1.000000, 120.28 sec so far
Iteration 72: max relative diff=1.000000, 125.72 sec so far
Iteration 75: max relative diff=1.000000, 131.09 sec so far
Iteration 78: max relative diff=1.000000, 136.55 sec so far
Iteration 81: max relative diff=1.000000, 141.94 sec so far
Iteration 84: max relative diff=1.000000, 147.33 sec so far
Iteration 87: max relative diff=1.000000, 152.72 sec so far
Iteration 90: max relative diff=1.000000, 158.07 sec so far
Iteration 93: max relative diff=1.000000, 163.42 sec so far
Iteration 96: max relative diff=0.999897, 168.76 sec so far
Iteration 99: max relative diff=0.998740, 174.07 sec so far
Iteration 102: max relative diff=0.916690, 179.35 sec so far
Iteration 105: max relative diff=0.889374, 184.63 sec so far
Iteration 108: max relative diff=0.832980, 189.91 sec so far
Iteration 111: max relative diff=0.798203, 195.15 sec so far
Iteration 114: max relative diff=0.772981, 200.38 sec so far
Iteration 117: max relative diff=0.674777, 205.63 sec so far
Iteration 120: max relative diff=0.548569, 210.80 sec so far
Iteration 123: max relative diff=0.533648, 215.99 sec so far
Iteration 126: max relative diff=0.509247, 221.16 sec so far
Iteration 129: max relative diff=0.509247, 226.31 sec so far
Iteration 132: max relative diff=0.441513, 231.41 sec so far
Iteration 135: max relative diff=0.418914, 236.58 sec so far
Iteration 138: max relative diff=0.377560, 241.71 sec so far
Iteration 141: max relative diff=0.346387, 246.84 sec so far
Iteration 144: max relative diff=0.275327, 252.03 sec so far
Iteration 147: max relative diff=0.158707, 257.17 sec so far
Iteration 150: max relative diff=0.101559, 262.26 sec so far
Iteration 153: max relative diff=0.049277, 267.32 sec so far
Iteration 156: max relative diff=0.015769, 272.46 sec so far
Iteration 159: max relative diff=0.003877, 277.64 sec so far
Iteration 162: max relative diff=0.000665, 282.74 sec so far
Iteration 165: max relative diff=0.000043, 287.84 sec so far
Iterative method: 167 iterations in 374.51 seconds (average 1.743886, setup 83.28)
Value in the initial state: 5.159769973549628E-9
Time for model checking: 409.384 seconds.
Result: 5.159769973549628E-9 (value in the initial state)
---------------------------------------------------------------------
Model checking: Pmin=? [ F "MissionTimeUp" ]
Prob0E: 127 iterations in 62.36 seconds (average 0.491031, setup 0.00)
Prob1A: 4 iterations in 0.57 seconds (average 0.143500, setup 0.00)
yes = 26535, no = 62604489, maybe = 53560685
Computing remaining probabilities...
Engine: Sparse
Building sparse matrix... [n=116191709, nc=88152092, nnz=215828723, k=2] [2.6 GB]
Creating vector for yes... [886.5 MB]
Allocating iteration vectors... [2 x 886.5 MB]
TOTAL: [5.2 GB]
Starting iterations...
Iteration 3: max relative diff=1.000000, 5.19 sec so far
Iteration 7: max relative diff=1.000000, 11.84 sec so far
Iteration 10: max relative diff=1.000000, 16.88 sec so far
Iteration 14: max relative diff=1.000000, 23.56 sec so far
Iteration 17: max relative diff=1.000000, 28.60 sec so far
Iteration 20: max relative diff=1.000000, 33.66 sec so far
Iteration 23: max relative diff=1.000000, 38.73 sec so far
Iteration 26: max relative diff=1.000000, 43.83 sec so far
Iteration 29: max relative diff=1.000000, 48.98 sec so far
Iteration 32: max relative diff=1.000000, 54.09 sec so far
Iteration 35: max relative diff=1.000000, 59.23 sec so far
Iteration 38: max relative diff=1.000000, 64.33 sec so far
Iteration 41: max relative diff=1.000000, 69.41 sec so far
Iteration 44: max relative diff=1.000000, 74.57 sec so far
Iteration 47: max relative diff=1.000000, 79.70 sec so far
Iteration 50: max relative diff=1.000000, 84.82 sec so far
Iteration 53: max relative diff=1.000000, 90.04 sec so far
Iteration 56: max relative diff=1.000000, 95.35 sec so far
Iteration 59: max relative diff=1.000000, 100.54 sec so far
Iteration 62: max relative diff=1.000000, 105.78 sec so far
Iteration 65: max relative diff=1.000000, 111.06 sec so far
Iteration 68: max relative diff=1.000000, 116.36 sec so far
Iteration 71: max relative diff=1.000000, 121.65 sec so far
Iteration 74: max relative diff=1.000000, 127.00 sec so far
Iteration 77: max relative diff=1.000000, 132.29 sec so far
Iteration 80: max relative diff=1.000000, 137.58 sec so far
Iteration 83: max relative diff=1.000000, 142.89 sec so far
Iteration 86: max relative diff=1.000000, 148.20 sec so far
Iteration 89: max relative diff=1.000000, 153.53 sec so far
Iteration 92: max relative diff=1.000000, 158.89 sec so far
Iteration 95: max relative diff=1.000000, 164.26 sec so far
Iteration 98: max relative diff=1.000000, 169.59 sec so far
Iteration 101: max relative diff=1.000000, 174.97 sec so far
Iteration 104: max relative diff=1.000000, 180.28 sec so far
Iteration 107: max relative diff=1.000000, 185.63 sec so far
Iteration 110: max relative diff=1.000000, 190.91 sec so far
Iteration 113: max relative diff=1.000000, 196.19 sec so far
Iteration 116: max relative diff=1.000000, 201.43 sec so far
Iteration 119: max relative diff=1.000000, 206.67 sec so far
Iteration 122: max relative diff=1.000000, 211.94 sec so far
Iteration 125: max relative diff=1.000000, 217.18 sec so far
Iteration 128: max relative diff=0.999518, 222.37 sec so far
Iteration 131: max relative diff=0.995764, 227.54 sec so far
Iteration 134: max relative diff=0.983990, 232.68 sec so far
Iteration 137: max relative diff=0.856352, 237.82 sec so far
Iteration 140: max relative diff=0.724636, 242.95 sec so far
Iteration 143: max relative diff=0.706606, 248.08 sec so far
Iteration 146: max relative diff=0.676521, 253.22 sec so far
Iteration 149: max relative diff=0.652402, 258.31 sec so far
Iteration 152: max relative diff=0.612766, 263.43 sec so far
Iteration 155: max relative diff=0.609204, 268.53 sec so far
Iteration 158: max relative diff=0.606214, 273.67 sec so far
Iteration 161: max relative diff=0.558309, 278.82 sec so far
Iteration 164: max relative diff=0.475302, 283.92 sec so far
Iteration 167: max relative diff=0.387155, 289.03 sec so far
Iteration 170: max relative diff=0.315535, 294.10 sec so far
Iteration 173: max relative diff=0.241236, 299.19 sec so far
Iteration 176: max relative diff=0.168470, 304.27 sec so far
Iteration 179: max relative diff=0.107073, 309.36 sec so far
Iteration 182: max relative diff=0.054788, 314.37 sec so far
Iteration 185: max relative diff=0.019158, 319.41 sec so far
Iteration 188: max relative diff=0.002691, 324.47 sec so far
Iteration 191: max relative diff=0.000121, 329.49 sec so far
Iteration 194: max relative diff=0.000003, 334.58 sec so far
Iterative method: 195 iterations in 419.08 seconds (average 1.724292, setup 82.84)
Value in the initial state: 3.575324529773406E-17
Time for model checking: 485.793 seconds.
Result: 3.575324529773406E-17 (value in the initial state)
---------------------------------------------------------------------
Model checking: Pmax=? [ F "Crash" ]
Prob0A: 4 iterations in 0.62 seconds (average 0.155250, setup 0.00)
Prob1E: 239 iterations in 54.14 seconds (average 0.226536, setup 0.00)
yes = 57038651, no = 167829, maybe = 58985229
Computing remaining probabilities...
Engine: Sparse
Building sparse matrix... [n=116191709, nc=96340618, nnz=232984641, k=2] [2.8 GB]
Creating vector for yes... [886.5 MB]
Allocating iteration vectors... [2 x 886.5 MB]
TOTAL: [5.4 GB]
Starting iterations...
Iteration 3: max relative diff=1.000000, 6.11 sec so far
Iteration 6: max relative diff=0.968861, 11.98 sec so far
Iteration 9: max relative diff=0.944305, 17.89 sec so far
Iteration 12: max relative diff=0.914697, 23.73 sec so far
Iteration 15: max relative diff=0.883561, 29.57 sec so far
Iteration 18: max relative diff=0.847544, 35.41 sec so far
Iteration 21: max relative diff=0.818328, 41.32 sec so far
Iteration 24: max relative diff=0.783239, 47.16 sec so far
Iteration 27: max relative diff=0.745858, 52.98 sec so far
Iteration 30: max relative diff=0.677589, 58.80 sec so far
Iteration 33: max relative diff=0.588384, 64.54 sec so far
Iteration 36: max relative diff=0.455315, 70.35 sec so far
Iteration 39: max relative diff=0.382557, 76.06 sec so far
Iteration 42: max relative diff=0.357905, 81.80 sec so far
Iteration 45: max relative diff=0.336851, 87.62 sec so far
Iteration 48: max relative diff=0.277293, 93.27 sec so far
Iteration 51: max relative diff=0.226178, 98.95 sec so far
Iteration 54: max relative diff=0.202733, 104.61 sec so far
Iteration 57: max relative diff=0.121505, 110.25 sec so far
Iteration 60: max relative diff=0.088954, 115.91 sec so far
Iteration 63: max relative diff=0.086973, 121.50 sec so far
Iteration 66: max relative diff=0.077094, 127.10 sec so far
Iteration 69: max relative diff=0.055394, 132.71 sec so far
Iteration 72: max relative diff=0.049788, 138.32 sec so far
Iteration 75: max relative diff=0.043789, 143.89 sec so far
Iteration 78: max relative diff=0.037665, 149.48 sec so far
Iteration 81: max relative diff=0.024844, 155.10 sec so far
Iteration 84: max relative diff=0.016226, 160.67 sec so far
Iteration 87: max relative diff=0.011217, 166.25 sec so far
Iteration 90: max relative diff=0.008414, 171.74 sec so far
Iteration 93: max relative diff=0.004861, 177.25 sec so far
Iteration 96: max relative diff=0.001924, 182.74 sec so far
Iteration 99: max relative diff=0.001496, 188.19 sec so far
Iteration 102: max relative diff=0.001136, 193.63 sec so far
Iteration 105: max relative diff=0.000796, 199.05 sec so far
Iteration 108: max relative diff=0.000616, 204.43 sec so far
Iteration 111: max relative diff=0.000437, 209.82 sec so far
Iteration 114: max relative diff=0.000241, 215.19 sec so far
Iteration 117: max relative diff=0.000119, 220.56 sec so far
Iteration 120: max relative diff=0.000043, 225.90 sec so far
Iteration 123: max relative diff=0.000016, 231.25 sec so far
Iteration 126: max relative diff=0.000006, 236.60 sec so far
Iteration 129: max relative diff=0.000001, 241.87 sec so far
Iterative method: 130 iterations in 336.00 seconds (average 1.874300, setup 92.34)
Value in the initial state: 0.0627708316469184
Time for model checking: 395.261 seconds.
Result: 0.0627708316469184 (value in the initial state)
---------------------------------------------------------------------
Model checking: Pmin=? [ F "Crash" ]
Prob0E: 4 iterations in 0.55 seconds (average 0.137000, setup 0.00)
Prob1A: 52 iterations in 13.38 seconds (average 0.257327, setup 0.00)
yes = 57038651, no = 167829, maybe = 58985229
Computing remaining probabilities...
Engine: Sparse
Building sparse matrix... [n=116191709, nc=96340618, nnz=232984641, k=2] [2.8 GB]
Creating vector for yes... [886.5 MB]
Allocating iteration vectors... [2 x 886.5 MB]
TOTAL: [5.4 GB]
Starting iterations...
Iteration 3: max relative diff=1.000000, 6.02 sec so far
Iteration 6: max relative diff=0.973652, 11.92 sec so far
Iteration 9: max relative diff=0.948533, 17.80 sec so far
Iteration 12: max relative diff=0.928950, 23.62 sec so far
Iteration 15: max relative diff=0.893132, 29.47 sec so far
Iteration 18: max relative diff=0.865209, 35.39 sec so far
Iteration 21: max relative diff=0.836540, 41.23 sec so far
Iteration 24: max relative diff=0.807441, 47.09 sec so far
Iteration 27: max relative diff=0.773799, 52.90 sec so far
Iteration 30: max relative diff=0.734053, 58.69 sec so far
Iteration 33: max relative diff=0.669383, 64.53 sec so far
Iteration 36: max relative diff=0.610464, 70.25 sec so far
Iteration 39: max relative diff=0.534796, 75.99 sec so far
Iteration 42: max relative diff=0.494513, 81.75 sec so far
Iteration 45: max relative diff=0.436797, 87.42 sec so far
Iteration 48: max relative diff=0.342147, 93.13 sec so far
Iteration 51: max relative diff=0.275349, 98.78 sec so far
Iteration 54: max relative diff=0.203337, 104.44 sec so far
Iteration 57: max relative diff=0.142464, 110.08 sec so far
Iteration 60: max relative diff=0.129289, 115.74 sec so far
Iteration 63: max relative diff=0.094535, 121.41 sec so far
Iteration 66: max relative diff=0.087265, 127.06 sec so far
Iteration 69: max relative diff=0.059570, 132.63 sec so far
Iteration 72: max relative diff=0.050036, 138.26 sec so far
Iteration 75: max relative diff=0.048194, 143.85 sec so far
Iteration 78: max relative diff=0.041167, 149.50 sec so far
Iteration 81: max relative diff=0.031725, 155.12 sec so far
Iteration 84: max relative diff=0.022855, 160.73 sec so far
Iteration 87: max relative diff=0.008788, 166.38 sec so far
Iteration 90: max relative diff=0.003677, 171.98 sec so far
Iteration 93: max relative diff=0.002152, 177.84 sec so far
Iteration 96: max relative diff=0.001586, 183.54 sec so far
Iteration 99: max relative diff=0.001088, 189.11 sec so far
Iteration 102: max relative diff=0.000675, 194.64 sec so far
Iteration 105: max relative diff=0.000447, 200.10 sec so far
Iteration 108: max relative diff=0.000183, 205.53 sec so far
Iteration 111: max relative diff=0.000049, 210.93 sec so far
Iteration 114: max relative diff=0.000017, 216.27 sec so far
Iteration 117: max relative diff=0.000004, 221.61 sec so far
Iteration 120: max relative diff=0.000001, 226.99 sec so far
Iterative method: 121 iterations in 320.00 seconds (average 1.890537, setup 91.24)
Value in the initial state: 0.05518770124189629
Time for model checking: 337.509 seconds.
Result: 0.05518770124189629 (value in the initial state)
---------------------------------------------------------------------
Model checking: Pmax=? [ F "AllAreaSearched" ]
Prob0A: 57 iterations in 6.88 seconds (average 0.120772, setup 0.00)
Prob1E: 4 iterations in 0.69 seconds (average 0.171250, setup 0.00)
yes = 59303, no = 69278576, maybe = 46853830
Computing remaining probabilities...
Engine: Sparse
Building sparse matrix... [n=116191709, nc=77201846, nnz=190458435, k=2] [2.3 GB]
Creating vector for yes... [886.5 MB]
Allocating iteration vectors... [2 x 886.5 MB]
TOTAL: [4.9 GB]
Starting iterations...
Iteration 4: max relative diff=1.000000, 6.40 sec so far
Iteration 8: max relative diff=1.000000, 12.61 sec so far
Iteration 12: max relative diff=1.000000, 18.93 sec so far
Iteration 16: max relative diff=1.000000, 25.30 sec so far
Iteration 20: max relative diff=1.000000, 31.59 sec so far
Iteration 24: max relative diff=1.000000, 37.96 sec so far
Iteration 28: max relative diff=1.000000, 44.43 sec so far
Iteration 32: max relative diff=1.000000, 50.95 sec so far
Iteration 36: max relative diff=1.000000, 57.49 sec so far
Iteration 40: max relative diff=1.000000, 64.12 sec so far
Iteration 44: max relative diff=1.000000, 70.75 sec so far
Iteration 47: max relative diff=1.000000, 75.78 sec so far
Iteration 50: max relative diff=1.000000, 80.86 sec so far
Iteration 53: max relative diff=1.000000, 85.92 sec so far
Iteration 56: max relative diff=1.000000, 90.99 sec so far
Iteration 59: max relative diff=0.999936, 96.59 sec so far
Iteration 62: max relative diff=0.870211, 101.66 sec so far
Iteration 65: max relative diff=0.870113, 106.74 sec so far
Iteration 68: max relative diff=0.805022, 111.81 sec so far
Iteration 71: max relative diff=0.787720, 116.84 sec so far
Iteration 74: max relative diff=0.482653, 121.86 sec so far
Iteration 77: max relative diff=0.410929, 126.90 sec so far
Iteration 81: max relative diff=0.410929, 133.58 sec so far
Iteration 84: max relative diff=0.409982, 138.63 sec so far
Iteration 87: max relative diff=0.228665, 143.66 sec so far
Iteration 91: max relative diff=0.097644, 150.31 sec so far
Iteration 95: max relative diff=0.067910, 156.93 sec so far
Iteration 99: max relative diff=0.048517, 163.51 sec so far
Iteration 103: max relative diff=0.015545, 170.09 sec so far
Iteration 107: max relative diff=0.005709, 176.56 sec so far
Iteration 111: max relative diff=0.004004, 182.97 sec so far
Iteration 115: max relative diff=0.001271, 189.42 sec so far
Iteration 119: max relative diff=0.000512, 195.85 sec so far
Iteration 123: max relative diff=0.000315, 202.25 sec so far
Iteration 127: max relative diff=0.000156, 208.58 sec so far
Iteration 131: max relative diff=0.000049, 214.91 sec so far
Iteration 135: max relative diff=0.000030, 221.27 sec so far
Iteration 139: max relative diff=0.000005, 227.61 sec so far
Iteration 143: max relative diff=0.000001, 233.89 sec so far
Iterative method: 143 iterations in 307.53 seconds (average 1.635608, setup 73.64)
Value in the initial state: 0.2616990621972663
Time for model checking: 318.66 seconds.
Result: 0.2616990621972663 (value in the initial state)
---------------------------------------------------------------------
Model checking: Pmin=? [ F "AllAreaSearched" ]
Prob0E: 58 iterations in 9.30 seconds (average 0.160328, setup 0.00)
Prob1A: 4 iterations in 0.80 seconds (average 0.198750, setup 0.00)
yes = 59303, no = 70196712, maybe = 45935694
Computing remaining probabilities...
Engine: Sparse
Building sparse matrix... [n=116191709, nc=75490392, nnz=186605507, k=2] [2.3 GB]
Creating vector for yes... [886.5 MB]
Allocating iteration vectors... [2 x 886.5 MB]
TOTAL: [4.9 GB]
Starting iterations...
Iteration 4: max relative diff=1.000000, 6.45 sec so far
Iteration 8: max relative diff=1.000000, 12.57 sec so far
Iteration 12: max relative diff=1.000000, 18.78 sec so far
Iteration 16: max relative diff=1.000000, 24.99 sec so far
Iteration 20: max relative diff=1.000000, 31.29 sec so far
Iteration 24: max relative diff=1.000000, 37.53 sec so far
Iteration 28: max relative diff=1.000000, 43.91 sec so far
Iteration 32: max relative diff=1.000000, 50.37 sec so far
Iteration 36: max relative diff=1.000000, 56.81 sec so far
Iteration 39: max relative diff=1.000000, 63.27 sec so far
Iteration 43: max relative diff=1.000000, 69.82 sec so far
Iteration 47: max relative diff=1.000000, 76.45 sec so far
Iteration 51: max relative diff=1.000000, 83.10 sec so far
Iteration 55: max relative diff=1.000000, 89.73 sec so far
Iteration 59: max relative diff=0.999949, 96.36 sec so far
Iteration 63: max relative diff=0.829293, 103.00 sec so far
Iteration 67: max relative diff=0.828990, 109.63 sec so far
Iteration 71: max relative diff=0.781670, 116.22 sec so far
Iteration 75: max relative diff=0.480177, 122.84 sec so far
Iteration 79: max relative diff=0.464776, 129.44 sec so far
Iteration 83: max relative diff=0.447566, 136.02 sec so far
Iteration 87: max relative diff=0.444414, 142.61 sec so far
Iteration 91: max relative diff=0.139818, 149.10 sec so far
Iteration 95: max relative diff=0.116489, 155.59 sec so far
Iteration 99: max relative diff=0.091445, 162.00 sec so far
Iteration 103: max relative diff=0.032222, 168.41 sec so far
Iteration 107: max relative diff=0.002528, 174.79 sec so far
Iteration 111: max relative diff=0.000961, 181.21 sec so far
Iteration 115: max relative diff=0.000168, 187.44 sec so far
Iteration 119: max relative diff=0.000018, 193.71 sec so far
Iteration 123: max relative diff=0.000005, 199.97 sec so far
Iteration 127: max relative diff=0.000003, 206.29 sec so far
Iteration 131: max relative diff=0.000001, 212.52 sec so far
Iterative method: 131 iterations in 284.36 seconds (average 1.622321, setup 71.84)
Value in the initial state: 0.180815758831309
Time for model checking: 298.681 seconds.
Result: 0.180815758831309 (value in the initial state)
---------------------------------------------------------------------
Model checking: Pmax=? [ F "MissionTimeUp"|"AllAreaSearched"|"Crash" ]
Prob0A: 4 iterations in 0.67 seconds (average 0.168250, setup 0.00)
Prob1E: 435 iterations in 104.45 seconds (average 0.240115, setup 0.00)
yes = 76902299, no = 82819, maybe = 39206591
Computing remaining probabilities...
Engine: Sparse
Building sparse matrix... [n=116191709, nc=64081283, nnz=155549122, k=2] [1.9 GB]
Creating vector for yes... [886.5 MB]
Allocating iteration vectors... [2 x 886.5 MB]
TOTAL: [4.5 GB]
Starting iterations...
Iteration 4: max relative diff=0.999514, 6.43 sec so far
Iteration 8: max relative diff=0.997856, 12.69 sec so far
Iteration 12: max relative diff=0.995223, 18.93 sec so far
Iteration 16: max relative diff=0.991932, 25.15 sec so far
Iteration 20: max relative diff=0.987168, 31.39 sec so far
Iteration 24: max relative diff=0.980382, 37.61 sec so far
Iteration 28: max relative diff=0.974103, 43.84 sec so far
Iteration 32: max relative diff=0.961920, 49.99 sec so far
Iteration 36: max relative diff=0.945623, 56.13 sec so far
Iteration 40: max relative diff=0.923178, 62.27 sec so far
Iteration 44: max relative diff=0.900544, 68.47 sec so far
Iteration 48: max relative diff=0.860005, 74.60 sec so far
Iteration 52: max relative diff=0.601737, 80.70 sec so far
Iteration 56: max relative diff=0.565152, 86.85 sec so far
Iteration 60: max relative diff=0.486671, 93.01 sec so far
Iteration 64: max relative diff=0.449559, 99.14 sec so far
Iteration 68: max relative diff=0.369013, 105.22 sec so far
Iteration 72: max relative diff=0.291803, 111.31 sec so far
Iteration 76: max relative diff=0.183060, 117.37 sec so far
Iteration 80: max relative diff=0.162727, 123.39 sec so far
Iteration 84: max relative diff=0.146110, 129.46 sec so far
Iteration 88: max relative diff=0.082608, 135.41 sec so far
Iteration 92: max relative diff=0.053930, 141.34 sec so far
Iteration 96: max relative diff=0.035647, 147.22 sec so far
Iteration 100: max relative diff=0.017721, 153.09 sec so far
Iteration 104: max relative diff=0.002568, 158.99 sec so far
Iteration 108: max relative diff=0.000419, 164.84 sec so far
Iteration 112: max relative diff=0.000261, 170.64 sec so far
Iteration 116: max relative diff=0.000049, 176.41 sec so far
Iteration 120: max relative diff=0.000010, 182.15 sec so far
Iteration 124: max relative diff=0.000002, 187.96 sec so far
Iterative method: 126 iterations in 254.93 seconds (average 1.514508, setup 64.11)
Value in the initial state: 0.32129081972405277
Time for model checking: 363.379 seconds.
Result: 0.32129081972405277 (value in the initial state)
---------------------------------------------------------------------
Model checking: Pmin=? [ F "MissionTimeUp"|"AllAreaSearched"|"Crash" ]
Prob0E: 4 iterations in 0.65 seconds (average 0.162250, setup 0.00)
Prob1A: 81 iterations in 17.59 seconds (average 0.217160, setup 0.00)
yes = 72159701, no = 82819, maybe = 43949189
Computing remaining probabilities...
Engine: Sparse
Building sparse matrix... [n=116191709, nc=71940167, nnz=174316066, k=2] [2.1 GB]
Creating vector for yes... [886.5 MB]
Allocating iteration vectors... [2 x 886.5 MB]
TOTAL: [4.7 GB]
Starting iterations...
Iteration 3: max relative diff=1.000000, 5.06 sec so far
Iteration 7: max relative diff=0.998546, 11.70 sec so far
Iteration 11: max relative diff=0.996608, 18.32 sec so far
Iteration 15: max relative diff=0.993868, 24.96 sec so far
Iteration 18: max relative diff=0.990935, 29.97 sec so far
Iteration 22: max relative diff=0.986434, 36.58 sec so far
Iteration 26: max relative diff=0.982971, 43.21 sec so far
Iteration 30: max relative diff=0.976031, 49.84 sec so far
Iteration 34: max relative diff=0.971300, 56.46 sec so far
Iteration 38: max relative diff=0.960914, 63.02 sec so far
Iteration 42: max relative diff=0.926393, 69.55 sec so far
Iteration 46: max relative diff=0.897436, 76.04 sec so far
Iteration 50: max relative diff=0.854574, 82.58 sec so far
Iteration 54: max relative diff=0.694598, 89.09 sec so far
Iteration 58: max relative diff=0.677316, 95.57 sec so far
Iteration 62: max relative diff=0.531228, 102.09 sec so far
Iteration 66: max relative diff=0.507632, 108.71 sec so far
Iteration 70: max relative diff=0.384427, 115.24 sec so far
Iteration 74: max relative diff=0.238573, 121.66 sec so far
Iteration 78: max relative diff=0.223135, 128.12 sec so far
Iteration 82: max relative diff=0.201353, 134.54 sec so far
Iteration 86: max relative diff=0.189892, 140.91 sec so far
Iteration 90: max relative diff=0.095988, 147.30 sec so far
Iteration 94: max relative diff=0.062024, 153.63 sec so far
Iteration 98: max relative diff=0.033915, 159.96 sec so far
Iteration 102: max relative diff=0.006621, 166.17 sec so far
Iteration 106: max relative diff=0.001124, 172.38 sec so far
Iteration 110: max relative diff=0.000084, 178.51 sec so far
Iteration 114: max relative diff=0.000006, 184.66 sec so far
Iteration 118: max relative diff=0.000002, 190.76 sec so far
Iteration 122: max relative diff=0.000002, 196.78 sec so far
Iteration 126: max relative diff=0.000001, 202.85 sec so far
Iterative method: 128 iterations in 276.67 seconds (average 1.608336, setup 70.80)
Value in the initial state: 0.23897082858778257
Time for model checking: 298.315 seconds.
Result: 0.23897082858778257 (value in the initial state)
---------------------------------------------------------------------
Model checking: filter(print, "deadlock", true)
States satisfying filter true: 116191709
Satisfying states:
23957:(0,0,0,16,0,0,0,0,0)
Number of states satisfying filter(print, "deadlock", true): 1
Property satisfied in 0 of 1 initial states.
Time for model checking: 0.03 seconds.
Result: false (property not satisfied in the initial state)
---------------------------------------------------------------------
Model checking: R{"drop"}max=? [ F "deadlock" ]
Prob0E: 5 iterations in 0.95 seconds (average 0.190800, setup 0.00)
Prob1A: 1 iterations in 0.09 seconds (average 0.086000, setup 0.00)
goal = 1, inf = 0, maybe = 116191708
Computing remaining rewards...
Engine: Sparse
Building sparse matrix (transitions)... [n=116191709, nc=153547097, nnz=290191120, k=2] [4.2 GB]
Building sparse matrix (transition rewards)... [n=116191709, nc=153547097, nnz=0, k=2] [1.0 GB]
Creating vector for state rewards... [886.5 MB]
Creating vector for inf... [886.5 MB]
Allocating iteration vectors... [2 x 886.5 MB]
TOTAL: [8.7 GB]
Starting iterations...
Iteration 2: max relative diff=1.000000, 5.44 sec so far
Iteration 5: max relative diff=1.000000, 12.88 sec so far
Iteration 7: max relative diff=1.000000, 17.94 sec so far
Iteration 9: max relative diff=1.000000, 23.08 sec so far
Iteration 11: max relative diff=1.000000, 28.29 sec so far
Iteration 13: max relative diff=1.000000, 33.48 sec so far
Iteration 15: max relative diff=1.000000, 38.68 sec so far
Iteration 17: max relative diff=1.000000, 43.89 sec so far
Iteration 19: max relative diff=1.000000, 49.12 sec so far
Iteration 21: max relative diff=1.000000, 54.36 sec so far
Iteration 23: max relative diff=1.000000, 59.63 sec so far
Iteration 25: max relative diff=1.000000, 64.94 sec so far
Iteration 27: max relative diff=1.000000, 70.19 sec so far
Iteration 29: max relative diff=1.000000, 75.42 sec so far
Iteration 31: max relative diff=0.494805, 80.67 sec so far
Iteration 33: max relative diff=0.357364, 85.89 sec so far
Iteration 35: max relative diff=0.253750, 91.14 sec so far
Iteration 37: max relative diff=0.214944, 96.29 sec so far
Iteration 39: max relative diff=0.182263, 101.47 sec so far
Iteration 41: max relative diff=0.153238, 106.70 sec so far
Iteration 43: max relative diff=0.127843, 111.87 sec so far
Iteration 45: max relative diff=0.111712, 117.06 sec so far
Iteration 47: max relative diff=0.080993, 123.65 sec so far
Iteration 49: max relative diff=0.073079, 128.91 sec so far
Iteration 51: max relative diff=0.068531, 134.09 sec so far
Iteration 53: max relative diff=0.064291, 139.32 sec so far
Iteration 55: max relative diff=0.053972, 144.51 sec so far
Iteration 57: max relative diff=0.049067, 149.67 sec so far
Iteration 59: max relative diff=0.040167, 154.92 sec so far
Iteration 61: max relative diff=0.037327, 160.08 sec so far
Iteration 63: max relative diff=0.032577, 165.22 sec so far
Iteration 65: max relative diff=0.028161, 170.38 sec so far
Iteration 67: max relative diff=0.025952, 175.51 sec so far
Iteration 69: max relative diff=0.025952, 180.75 sec so far
Iteration 71: max relative diff=0.025952, 185.94 sec so far
Iteration 73: max relative diff=0.025952, 191.08 sec so far
Iteration 75: max relative diff=0.025377, 196.24 sec so far
Iteration 77: max relative diff=0.023510, 201.40 sec so far
Iteration 79: max relative diff=0.022600, 206.51 sec so far
Iteration 81: max relative diff=0.020915, 211.65 sec so far
Iteration 83: max relative diff=0.019390, 216.75 sec so far
Iteration 85: max relative diff=0.016830, 221.86 sec so far
Iteration 87: max relative diff=0.014702, 226.99 sec so far
Iteration 89: max relative diff=0.013215, 232.07 sec so far
Iteration 91: max relative diff=0.012576, 237.16 sec so far
Iteration 93: max relative diff=0.011654, 242.27 sec so far
Iteration 95: max relative diff=0.010213, 247.31 sec so far
Iteration 97: max relative diff=0.008275, 252.38 sec so far
Iteration 99: max relative diff=0.006565, 257.42 sec so far
Iteration 101: max relative diff=0.005547, 262.47 sec so far
Iteration 103: max relative diff=0.004422, 267.56 sec so far
Iteration 105: max relative diff=0.002982, 272.60 sec so far
Iteration 107: max relative diff=0.001730, 277.63 sec so far
Iteration 110: max relative diff=0.000691, 285.07 sec so far
Iteration 112: max relative diff=0.000318, 290.09 sec so far
Iteration 115: max relative diff=0.000098, 297.56 sec so far
Iteration 118: max relative diff=0.000059, 305.05 sec so far
Iteration 121: max relative diff=0.000059, 312.54 sec so far
Iteration 124: max relative diff=0.000053, 319.97 sec so far
Iteration 127: max relative diff=0.000050, 327.37 sec so far
Iteration 130: max relative diff=0.000037, 334.78 sec so far
Iteration 133: max relative diff=0.000014, 342.16 sec so far
Iteration 136: max relative diff=0.000006, 349.57 sec so far
Iteration 139: max relative diff=0.000002, 356.98 sec so far
Iterative method: 141 iterations in 500.24 seconds (average 2.566504, setup 138.36)
Value in the initial state: 0.029584782191533654
Time for model checking: 507.297 seconds.
Result: 0.029584782191533654 (value in the initial state)
---------------------------------------------------------------------
Model checking: R{"drop"}min=? [ F "deadlock" ]
Prob0A: 5 iterations in 0.28 seconds (average 0.056200, setup 0.00)
Prob1E: 6 iterations in 0.41 seconds (average 0.068167, setup 0.00)
Warning: PRISM hasn't checked for zero-reward loops.
Your minimum rewards may be too low...
goal = 1, inf = 0, maybe = 116191708
Computing remaining rewards...
Engine: Sparse
Building sparse matrix (transitions)... [n=116191709, nc=153547097, nnz=290191120, k=2] [4.2 GB]
Building sparse matrix (transition rewards)... [n=116191709, nc=153547097, nnz=0, k=2] [1.0 GB]
Creating vector for state rewards... [886.5 MB]
Creating vector for inf... [886.5 MB]
Allocating iteration vectors... [2 x 886.5 MB]
TOTAL: [8.7 GB]
Starting iterations...
Iteration 2: max relative diff=1.000000, 5.11 sec so far
Iteration 5: max relative diff=1.000000, 12.55 sec so far
Iteration 8: max relative diff=1.000000, 20.01 sec so far
Iteration 10: max relative diff=1.000000, 25.14 sec so far
Iteration 12: max relative diff=1.000000, 30.26 sec so far
Iteration 14: max relative diff=1.000000, 35.45 sec so far
Iteration 16: max relative diff=1.000000, 40.55 sec so far
Iteration 18: max relative diff=1.000000, 45.71 sec so far
Iteration 20: max relative diff=1.000000, 50.86 sec so far
Iteration 22: max relative diff=1.000000, 56.05 sec so far
Iteration 24: max relative diff=1.000000, 61.26 sec so far
Iteration 26: max relative diff=1.000000, 66.46 sec so far
Iteration 28: max relative diff=1.000000, 71.59 sec so far
Iteration 30: max relative diff=1.000000, 76.74 sec so far
Iteration 32: max relative diff=1.000000, 81.93 sec so far
Iteration 34: max relative diff=0.494157, 87.14 sec so far
Iteration 36: max relative diff=0.358616, 92.36 sec so far
Iteration 38: max relative diff=0.297563, 97.52 sec so far
Iteration 40: max relative diff=0.240903, 102.69 sec so far
Iteration 42: max relative diff=0.190151, 107.84 sec so far
Iteration 44: max relative diff=0.156932, 112.97 sec so far
Iteration 46: max relative diff=0.134848, 118.08 sec so far
Iteration 48: max relative diff=0.089611, 123.20 sec so far
Iteration 50: max relative diff=0.081706, 128.34 sec so far
Iteration 52: max relative diff=0.067159, 133.51 sec so far
Iteration 54: max relative diff=0.062288, 138.65 sec so far
Iteration 56: max relative diff=0.054117, 143.76 sec so far
Iteration 58: max relative diff=0.048223, 148.89 sec so far
Iteration 60: max relative diff=0.043041, 154.01 sec so far
Iteration 62: max relative diff=0.039472, 159.10 sec so far
Iteration 64: max relative diff=0.038157, 164.24 sec so far
Iteration 66: max relative diff=0.036155, 169.35 sec so far
Iteration 68: max relative diff=0.030877, 174.49 sec so far
Iteration 70: max relative diff=0.025637, 179.62 sec so far
Iteration 72: max relative diff=0.025257, 184.69 sec so far
Iteration 74: max relative diff=0.024890, 189.75 sec so far
Iteration 76: max relative diff=0.024463, 194.83 sec so far
Iteration 78: max relative diff=0.024463, 199.89 sec so far
Iteration 80: max relative diff=0.024463, 204.90 sec so far
Iteration 82: max relative diff=0.024463, 210.16 sec so far
Iteration 84: max relative diff=0.023457, 215.41 sec so far
Iteration 86: max relative diff=0.022359, 220.41 sec so far
Iteration 89: max relative diff=0.019795, 227.92 sec so far
Iteration 91: max relative diff=0.016901, 232.96 sec so far
Iteration 94: max relative diff=0.009665, 240.41 sec so far
Iteration 96: max relative diff=0.006280, 245.46 sec so far
Iteration 99: max relative diff=0.003408, 252.92 sec so far
Iteration 102: max relative diff=0.001367, 260.33 sec so far
Iteration 105: max relative diff=0.000341, 267.78 sec so far
Iteration 108: max relative diff=0.000097, 275.22 sec so far
Iteration 111: max relative diff=0.000026, 282.65 sec so far
Iteration 114: max relative diff=0.000008, 290.03 sec so far
Iteration 117: max relative diff=0.000002, 297.31 sec so far
Iterative method: 119 iterations in 439.93 seconds (average 2.539437, setup 137.73)
Value in the initial state: 0.026210917006325468
Time for model checking: 445.57 seconds.
Result: 0.026210917006325468 (value in the initial state)
---------------------------------------------------------------------
Model checking: R{"charge"}max=? [ F "deadlock" ]
Prob0E: 5 iterations in 0.20 seconds (average 0.039600, setup 0.00)
Prob1A: 1 iterations in 0.04 seconds (average 0.039000, setup 0.00)
goal = 1, inf = 0, maybe = 116191708
Computing remaining rewards...
Engine: Sparse
Building sparse matrix (transitions)... [n=116191709, nc=153547097, nnz=290191120, k=2] [4.2 GB]
Building sparse matrix (transition rewards)... [n=116191709, nc=153547097, nnz=2747626, k=2] [1.0 GB]
Creating vector for state rewards... [886.5 MB]
Creating vector for inf... [886.5 MB]
Allocating iteration vectors... [2 x 886.5 MB]
TOTAL: [8.7 GB]
Starting iterations...
Iteration 2: max relative diff=1.000000, 5.32 sec so far
Iteration 5: max relative diff=1.000000, 12.74 sec so far
Iteration 8: max relative diff=1.000000, 20.10 sec so far
Iteration 11: max relative diff=1.000000, 27.51 sec so far
Iteration 13: max relative diff=1.000000, 32.53 sec so far
Iteration 15: max relative diff=1.000000, 37.62 sec so far
Iteration 17: max relative diff=1.000000, 42.74 sec so far
Iteration 19: max relative diff=1.000000, 47.85 sec so far
Iteration 21: max relative diff=1.000000, 52.91 sec so far
Iteration 23: max relative diff=1.000000, 57.98 sec so far
Iteration 25: max relative diff=1.000000, 63.04 sec so far
Iteration 27: max relative diff=1.000000, 68.07 sec so far
Iteration 29: max relative diff=1.000000, 73.20 sec so far
Iteration 31: max relative diff=1.000000, 78.26 sec so far
Iteration 33: max relative diff=1.000000, 83.28 sec so far
Iteration 35: max relative diff=1.000000, 88.36 sec so far
Iteration 37: max relative diff=0.999970, 93.52 sec so far
Iteration 39: max relative diff=0.999962, 98.54 sec so far
Iteration 41: max relative diff=0.999626, 103.63 sec so far
Iteration 43: max relative diff=0.984551, 108.66 sec so far
Iteration 45: max relative diff=0.968832, 113.74 sec so far
Iteration 47: max relative diff=0.966495, 118.82 sec so far
Iteration 49: max relative diff=0.966495, 123.97 sec so far
Iteration 51: max relative diff=0.966495, 129.13 sec so far
Iteration 53: max relative diff=0.763114, 134.31 sec so far
Iteration 55: max relative diff=0.763114, 139.36 sec so far
Iteration 57: max relative diff=0.725324, 144.42 sec so far
Iteration 59: max relative diff=0.657115, 149.52 sec so far
Iteration 61: max relative diff=0.634572, 154.63 sec so far
Iteration 63: max relative diff=0.634572, 159.76 sec so far
Iteration 65: max relative diff=0.546531, 164.81 sec so far
Iteration 67: max relative diff=0.286201, 169.91 sec so far
Iteration 69: max relative diff=0.211623, 175.00 sec so far
Iteration 71: max relative diff=0.174697, 180.09 sec so far
Iteration 73: max relative diff=0.110801, 185.19 sec so far
Iteration 75: max relative diff=0.074044, 190.30 sec so far
Iteration 77: max relative diff=0.061196, 195.41 sec so far
Iteration 79: max relative diff=0.050136, 200.49 sec so far
Iteration 81: max relative diff=0.035321, 205.54 sec so far
Iteration 83: max relative diff=0.028196, 210.58 sec so far
Iteration 85: max relative diff=0.026463, 215.62 sec so far
Iteration 87: max relative diff=0.021288, 220.68 sec so far
Iteration 89: max relative diff=0.016579, 225.69 sec so far
Iteration 91: max relative diff=0.013176, 230.74 sec so far
Iteration 94: max relative diff=0.002848, 238.21 sec so far
Iteration 97: max relative diff=0.000931, 245.76 sec so far
Iteration 99: max relative diff=0.000917, 252.06 sec so far
Iteration 101: max relative diff=0.000917, 257.07 sec so far
Iteration 103: max relative diff=0.000917, 262.12 sec so far
Iteration 106: max relative diff=0.000722, 269.59 sec so far
Iteration 109: max relative diff=0.000381, 276.99 sec so far
Iteration 112: max relative diff=0.000380, 284.38 sec so far
Iteration 115: max relative diff=0.000243, 291.73 sec so far
Iteration 118: max relative diff=0.000041, 299.12 sec so far
Iteration 121: max relative diff=0.000014, 306.50 sec so far
Iteration 124: max relative diff=0.000004, 313.91 sec so far
Iteration 127: max relative diff=0.000001, 321.29 sec so far
Iterative method: 127 iterations in 459.57 seconds (average 2.529858, setup 138.28)
Value in the initial state: 0.7376191240350886
Time for model checking: 465.644 seconds.
Result: 0.7376191240350886 (value in the initial state)
---------------------------------------------------------------------
Model checking: R{"charge"}min=? [ F "deadlock" ]
Prob0A: 5 iterations in 0.18 seconds (average 0.036600, setup 0.00)
Prob1E: 6 iterations in 0.38 seconds (average 0.062833, setup 0.00)
Warning: PRISM hasn't checked for zero-reward loops.
Your minimum rewards may be too low...
goal = 1, inf = 0, maybe = 116191708
Computing remaining rewards...
Engine: Sparse
Building sparse matrix (transitions)... [n=116191709, nc=153547097, nnz=290191120, k=2] [4.2 GB]
Building sparse matrix (transition rewards)... [n=116191709, nc=153547097, nnz=2747626, k=2] [1.0 GB]
Creating vector for state rewards... [886.5 MB]
Creating vector for inf... [886.5 MB]
Allocating iteration vectors... [2 x 886.5 MB]
TOTAL: [8.7 GB]
Starting iterations...
Iteration 2: max relative diff=1.000000, 5.01 sec so far
Iteration 5: max relative diff=1.000000, 12.30 sec so far
Iteration 8: max relative diff=1.000000, 19.62 sec so far
Iteration 11: max relative diff=1.000000, 27.02 sec so far
Iteration 14: max relative diff=1.000000, 34.41 sec so far
Iteration 17: max relative diff=1.000000, 41.84 sec so far
Iteration 20: max relative diff=1.000000, 49.30 sec so far
Iteration 22: max relative diff=1.000000, 54.31 sec so far
Iteration 24: max relative diff=1.000000, 59.34 sec so far
Iteration 27: max relative diff=1.000000, 66.78 sec so far
Iteration 30: max relative diff=1.000000, 74.23 sec so far
Iteration 32: max relative diff=1.000000, 79.24 sec so far
Iteration 35: max relative diff=1.000000, 86.73 sec so far
Iteration 38: max relative diff=1.000000, 94.15 sec so far
Iteration 41: max relative diff=1.000000, 101.53 sec so far
Iteration 44: max relative diff=1.000000, 108.91 sec so far
Iteration 47: max relative diff=1.000000, 116.37 sec so far
Iteration 50: max relative diff=0.999983, 123.84 sec so far
Iteration 53: max relative diff=0.998982, 131.28 sec so far
Iteration 56: max relative diff=0.979936, 138.77 sec so far
Iteration 58: max relative diff=0.957496, 143.81 sec so far
Iteration 60: max relative diff=0.952611, 148.89 sec so far
Iteration 62: max relative diff=0.858267, 153.89 sec so far
Iteration 64: max relative diff=0.858267, 158.95 sec so far
Iteration 66: max relative diff=0.797709, 164.01 sec so far
Iteration 68: max relative diff=0.797709, 169.09 sec so far
Iteration 70: max relative diff=0.797709, 174.21 sec so far
Iteration 72: max relative diff=0.791748, 179.31 sec so far
Iteration 74: max relative diff=0.569733, 184.40 sec so far
Iteration 76: max relative diff=0.569733, 189.50 sec so far
Iteration 78: max relative diff=0.381080, 194.58 sec so far
Iteration 80: max relative diff=0.314187, 199.66 sec so far
Iteration 82: max relative diff=0.085067, 204.73 sec so far
Iteration 84: max relative diff=0.058119, 209.81 sec so far
Iteration 86: max relative diff=0.039817, 214.85 sec so far
Iteration 88: max relative diff=0.027507, 219.86 sec so far
Iteration 90: max relative diff=0.012938, 224.96 sec so far
Iteration 92: max relative diff=0.006695, 230.02 sec so far
Iteration 94: max relative diff=0.002340, 235.08 sec so far
Iteration 97: max relative diff=0.001113, 242.55 sec so far
Iteration 99: max relative diff=0.000245, 247.56 sec so far
Iteration 102: max relative diff=0.000088, 255.02 sec so far
Iteration 104: max relative diff=0.000052, 260.02 sec so far
Iteration 107: max relative diff=0.000008, 267.55 sec so far
Iteration 110: max relative diff=0.000008, 274.94 sec so far
Iteration 113: max relative diff=0.000007, 282.34 sec so far
Iteration 116: max relative diff=0.000003, 289.76 sec so far
Iteration 119: max relative diff=0.000002, 297.13 sec so far
Iteration 122: max relative diff=0.000001, 304.47 sec so far
Iterative method: 122 iterations in 441.04 seconds (average 2.495672, setup 136.57)
Value in the initial state: 0.24430484376692715
Time for model checking: 446.294 seconds.
Result: 0.24430484376692715 (value in the initial state)
---------------------------------------------------------------------
Model checking: R{"time"}max=? [ F "deadlock" ]
Prob0E: 5 iterations in 0.20 seconds (average 0.040600, setup 0.00)
Prob1A: 1 iterations in 0.03 seconds (average 0.034000, setup 0.00)
goal = 1, inf = 0, maybe = 116191708
Computing remaining rewards...
Engine: Sparse
Building sparse matrix (transitions)... [n=116191709, nc=153547097, nnz=290191120, k=2] [4.2 GB]
Building sparse matrix (transition rewards)... [n=116191709, nc=153547097, nnz=57206478, k=2] [1.6 GB]
Creating vector for state rewards... [886.5 MB]
Creating vector for inf... [886.5 MB]
Allocating iteration vectors... [2 x 886.5 MB]
TOTAL: [9.4 GB]
Starting iterations...
Iteration 2: max relative diff=1.000000, 5.76 sec so far
Iteration 4: max relative diff=1.000000, 11.05 sec so far
Iteration 6: max relative diff=0.999642, 16.29 sec so far
Iteration 8: max relative diff=0.998753, 21.55 sec so far
Iteration 10: max relative diff=0.997870, 26.75 sec so far
Iteration 12: max relative diff=0.997193, 31.96 sec so far
Iteration 14: max relative diff=0.996418, 37.17 sec so far
Iteration 16: max relative diff=0.995588, 42.55 sec so far
Iteration 18: max relative diff=0.993253, 47.86 sec so far
Iteration 20: max relative diff=0.991210, 53.10 sec so far
Iteration 22: max relative diff=0.987391, 58.26 sec so far
Iteration 24: max relative diff=0.979773, 63.43 sec so far
Iteration 26: max relative diff=0.976787, 68.54 sec so far
Iteration 28: max relative diff=0.975567, 73.73 sec so far
Iteration 30: max relative diff=0.973257, 78.88 sec so far
Iteration 32: max relative diff=0.970974, 84.05 sec so far
Iteration 34: max relative diff=0.951911, 89.23 sec so far
Iteration 36: max relative diff=0.936564, 94.40 sec so far
Iteration 38: max relative diff=0.935573, 99.50 sec so far
Iteration 40: max relative diff=0.934408, 104.67 sec so far
Iteration 42: max relative diff=0.870391, 109.80 sec so far
Iteration 44: max relative diff=0.784201, 114.92 sec so far
Iteration 46: max relative diff=0.706035, 120.04 sec so far
Iteration 48: max relative diff=0.672025, 125.14 sec so far
Iteration 50: max relative diff=0.640731, 130.27 sec so far
Iteration 52: max relative diff=0.584697, 135.38 sec so far
Iteration 54: max relative diff=0.583453, 140.44 sec so far
Iteration 56: max relative diff=0.553007, 145.53 sec so far
Iteration 58: max relative diff=0.500601, 150.63 sec so far
Iteration 60: max relative diff=0.476768, 155.69 sec so far
Iteration 62: max relative diff=0.456723, 160.78 sec so far
Iteration 64: max relative diff=0.426934, 165.92 sec so far
Iteration 66: max relative diff=0.374792, 170.99 sec so far
Iteration 68: max relative diff=0.355495, 176.06 sec so far
Iteration 70: max relative diff=0.329580, 181.10 sec so far
Iteration 72: max relative diff=0.269688, 186.16 sec so far
Iteration 74: max relative diff=0.269656, 191.20 sec so far
Iteration 76: max relative diff=0.269580, 196.24 sec so far
Iteration 78: max relative diff=0.269347, 201.24 sec so far
Iteration 80: max relative diff=0.269006, 206.28 sec so far
Iteration 83: max relative diff=0.256672, 213.76 sec so far
Iteration 86: max relative diff=0.193905, 221.26 sec so far
Iteration 89: max relative diff=0.121799, 228.71 sec so far
Iteration 92: max relative diff=0.093524, 236.19 sec so far
Iteration 94: max relative diff=0.083035, 241.20 sec so far
Iteration 97: max relative diff=0.057597, 249.14 sec so far
Iteration 99: max relative diff=0.051619, 254.16 sec so far
Iteration 102: max relative diff=0.042762, 261.57 sec so far
Iteration 105: max relative diff=0.024980, 268.95 sec so far
Iteration 108: max relative diff=0.016431, 276.31 sec so far
Iteration 111: max relative diff=0.010641, 283.71 sec so far
Iteration 114: max relative diff=0.008022, 291.02 sec so far
Iteration 117: max relative diff=0.003946, 298.31 sec so far
Iteration 120: max relative diff=0.000985, 305.62 sec so far
Iteration 123: max relative diff=0.000396, 312.92 sec so far
Iteration 126: max relative diff=0.000242, 320.22 sec so far
Iteration 129: max relative diff=0.000089, 327.49 sec so far
Iteration 132: max relative diff=0.000039, 334.73 sec so far
Iteration 135: max relative diff=0.000038, 342.01 sec so far
Iteration 138: max relative diff=0.000005, 349.33 sec so far
Iteration 141: max relative diff=0.000002, 356.74 sec so far
Iteration 144: max relative diff=0.000001, 364.04 sec so far
Iterative method: 144 iterations in 515.64 seconds (average 2.528069, setup 151.60)
Value in the initial state: 345.2910501408803
Time for model checking: 521.245 seconds.
Result: 345.2910501408803 (value in the initial state)
---------------------------------------------------------------------
Model checking: R{"time"}min=? [ F "deadlock" ]
Prob0A: 5 iterations in 0.18 seconds (average 0.036600, setup 0.00)
Prob1E: 6 iterations in 0.38 seconds (average 0.063000, setup 0.00)
Warning: PRISM hasn't checked for zero-reward loops.
Your minimum rewards may be too low...
goal = 1, inf = 0, maybe = 116191708
Computing remaining rewards...
Engine: Sparse
Building sparse matrix (transitions)... [n=116191709, nc=153547097, nnz=290191120, k=2] [4.2 GB]
Building sparse matrix (transition rewards)... [n=116191709, nc=153547097, nnz=57206478, k=2] [1.6 GB]
Creating vector for state rewards... [886.5 MB]
Creating vector for inf... [886.5 MB]
Allocating iteration vectors... [2 x 886.5 MB]
TOTAL: [9.4 GB]
Starting iterations...
Iteration 2: max relative diff=1.000000, 5.51 sec so far
Iteration 4: max relative diff=1.000000, 10.75 sec so far
Iteration 6: max relative diff=0.999642, 16.03 sec so far
Iteration 8: max relative diff=0.999107, 21.31 sec so far
Iteration 10: max relative diff=0.998397, 26.58 sec so far
Iteration 12: max relative diff=0.997725, 31.91 sec so far
Iteration 14: max relative diff=0.996817, 37.20 sec so far
Iteration 16: max relative diff=0.995958, 42.46 sec so far
Iteration 18: max relative diff=0.994130, 47.70 sec so far
Iteration 20: max relative diff=0.991520, 52.90 sec so far
Iteration 22: max relative diff=0.989238, 58.18 sec so far
Iteration 24: max relative diff=0.985816, 63.41 sec so far
Iteration 26: max relative diff=0.978874, 68.65 sec so far
Iteration 28: max relative diff=0.975732, 73.86 sec so far
Iteration 30: max relative diff=0.973996, 79.03 sec so far
Iteration 32: max relative diff=0.971953, 84.25 sec so far
Iteration 34: max relative diff=0.952124, 89.46 sec so far
Iteration 36: max relative diff=0.940135, 94.71 sec so far
Iteration 38: max relative diff=0.939467, 99.87 sec so far
Iteration 40: max relative diff=0.938336, 105.02 sec so far
Iteration 42: max relative diff=0.915802, 110.16 sec so far
Iteration 44: max relative diff=0.792751, 115.30 sec so far
Iteration 46: max relative diff=0.743996, 120.49 sec so far
Iteration 48: max relative diff=0.685987, 125.60 sec so far
Iteration 50: max relative diff=0.681631, 130.76 sec so far
Iteration 52: max relative diff=0.655314, 135.87 sec so far
Iteration 54: max relative diff=0.622846, 141.00 sec so far
Iteration 56: max relative diff=0.578115, 146.12 sec so far
Iteration 58: max relative diff=0.573843, 151.28 sec so far
Iteration 60: max relative diff=0.569786, 156.35 sec so far
Iteration 62: max relative diff=0.515384, 161.45 sec so far
Iteration 64: max relative diff=0.454366, 166.56 sec so far
Iteration 66: max relative diff=0.419002, 171.65 sec so far
Iteration 68: max relative diff=0.394574, 176.78 sec so far
Iteration 70: max relative diff=0.371360, 182.01 sec so far
Iteration 72: max relative diff=0.345916, 187.10 sec so far
Iteration 74: max relative diff=0.342440, 192.20 sec so far
Iteration 76: max relative diff=0.339098, 197.31 sec so far
Iteration 78: max relative diff=0.331611, 202.45 sec so far
Iteration 80: max relative diff=0.291262, 207.55 sec so far
Iteration 82: max relative diff=0.281872, 212.62 sec so far
Iteration 84: max relative diff=0.279072, 217.64 sec so far
Iteration 86: max relative diff=0.277100, 222.67 sec so far
Iteration 88: max relative diff=0.269660, 227.78 sec so far
Iteration 90: max relative diff=0.247187, 232.85 sec so far
Iteration 92: max relative diff=0.211617, 237.93 sec so far
Iteration 94: max relative diff=0.167728, 242.97 sec so far
Iteration 96: max relative diff=0.130035, 248.03 sec so far
Iteration 98: max relative diff=0.113286, 253.06 sec so far
Iteration 100: max relative diff=0.091236, 258.07 sec so far
Iteration 102: max relative diff=0.075264, 263.11 sec so far
Iteration 104: max relative diff=0.056751, 268.18 sec so far
Iteration 107: max relative diff=0.030163, 275.67 sec so far
Iteration 109: max relative diff=0.021274, 280.67 sec so far
Iteration 112: max relative diff=0.013287, 288.14 sec so far
Iteration 114: max relative diff=0.009026, 293.15 sec so far
Iteration 117: max relative diff=0.003222, 300.62 sec so far
Iteration 120: max relative diff=0.000564, 307.98 sec so far
Iteration 123: max relative diff=0.000175, 315.41 sec so far
Iteration 126: max relative diff=0.000067, 322.80 sec so far
Iteration 129: max relative diff=0.000032, 330.22 sec so far
Iteration 132: max relative diff=0.000017, 337.55 sec so far
Iteration 135: max relative diff=0.000006, 344.90 sec so far
Iteration 138: max relative diff=0.000003, 352.25 sec so far
Iteration 141: max relative diff=0.000001, 359.61 sec so far
Iterative method: 142 iterations in 514.90 seconds (average 2.549648, setup 152.85)
Value in the initial state: 303.52431284485687
Time for model checking: 521.412 seconds.
Result: 303.52431284485687 (value in the initial state)
---------------------------------------------------------------------
Model checking: R{"success"}max=? [ F "deadlock" ]/Pmin=? [ F "MissionSuccessful" ]
Prob0E: 5 iterations in 0.19 seconds (average 0.038800, setup 0.00)
Prob1A: 1 iterations in 0.04 seconds (average 0.040000, setup 0.00)
goal = 1, inf = 0, maybe = 116191708
Computing remaining rewards...
Engine: Sparse
Building sparse matrix (transitions)... [n=116191709, nc=153547097, nnz=290191120, k=2] [4.2 GB]
Building sparse matrix (transition rewards)... [n=116191709, nc=153547097, nnz=153667, k=2] [1.0 GB]
Creating vector for state rewards... [886.5 MB]
Creating vector for inf... [886.5 MB]
Allocating iteration vectors... [2 x 886.5 MB]
TOTAL: [8.7 GB]
Starting iterations...
Iteration 2: max relative diff=1.000000, 5.02 sec so far
Iteration 5: max relative diff=1.000000, 12.23 sec so far
Iteration 8: max relative diff=1.000000, 19.46 sec so far
Iteration 11: max relative diff=1.000000, 26.73 sec so far
Iteration 14: max relative diff=1.000000, 33.96 sec so far
Iteration 17: max relative diff=1.000000, 41.27 sec so far
Iteration 20: max relative diff=1.000000, 48.58 sec so far
Iteration 23: max relative diff=1.000000, 55.92 sec so far
Iteration 26: max relative diff=1.000000, 63.29 sec so far
Iteration 29: max relative diff=1.000000, 70.72 sec so far
Iteration 32: max relative diff=1.000000, 78.20 sec so far
Iteration 35: max relative diff=1.000000, 85.68 sec so far
Iteration 38: max relative diff=1.000000, 93.22 sec so far
Iteration 40: max relative diff=1.000000, 98.41 sec so far
Iteration 42: max relative diff=1.000000, 103.53 sec so far
Iteration 44: max relative diff=1.000000, 108.57 sec so far
Iteration 46: max relative diff=1.000000, 113.64 sec so far
Iteration 48: max relative diff=1.000000, 118.75 sec so far
Iteration 50: max relative diff=1.000000, 123.89 sec so far
Iteration 52: max relative diff=1.000000, 129.05 sec so far
Iteration 54: max relative diff=1.000000, 134.12 sec so far
Iteration 56: max relative diff=1.000000, 139.24 sec so far
Iteration 58: max relative diff=1.000000, 144.34 sec so far
Iteration 60: max relative diff=1.000000, 149.45 sec so far
Iteration 62: max relative diff=1.000000, 154.58 sec so far
Iteration 64: max relative diff=1.000000, 159.73 sec so far
Iteration 66: max relative diff=1.000000, 164.83 sec so far
Iteration 68: max relative diff=1.000000, 169.91 sec so far
Iteration 70: max relative diff=1.000000, 175.02 sec so far
Iteration 72: max relative diff=1.000000, 180.09 sec so far
Iteration 74: max relative diff=1.000000, 185.15 sec so far
Iteration 76: max relative diff=1.000000, 190.22 sec so far
Iteration 78: max relative diff=1.000000, 195.30 sec so far
Iteration 80: max relative diff=1.000000, 200.35 sec so far
Iteration 82: max relative diff=0.461494, 205.44 sec so far
Iteration 84: max relative diff=0.288580, 210.46 sec so far
Iteration 86: max relative diff=0.223577, 215.53 sec so far
Iteration 88: max relative diff=0.166178, 220.56 sec so far
Iteration 90: max relative diff=0.149519, 225.64 sec so far
Iteration 92: max relative diff=0.116884, 230.65 sec so far
Iteration 94: max relative diff=0.092061, 235.70 sec so far
Iteration 96: max relative diff=0.073919, 240.72 sec so far
Iteration 99: max relative diff=0.063596, 248.24 sec so far
Iteration 102: max relative diff=0.039480, 255.73 sec so far
Iteration 104: max relative diff=0.031217, 260.74 sec so far
Iteration 107: max relative diff=0.015909, 268.23 sec so far
Iteration 110: max relative diff=0.005857, 275.72 sec so far
Iteration 112: max relative diff=0.004334, 280.76 sec so far
Iteration 115: max relative diff=0.001671, 288.14 sec so far
Iteration 118: max relative diff=0.000649, 295.53 sec so far
Iteration 121: max relative diff=0.000218, 302.98 sec so far
Iteration 124: max relative diff=0.000056, 310.39 sec so far
Iteration 127: max relative diff=0.000013, 317.78 sec so far
Iteration 130: max relative diff=0.000005, 325.12 sec so far
Iteration 133: max relative diff=0.000002, 332.50 sec so far
Iteration 136: max relative diff=0.000001, 339.86 sec so far
Iterative method: 138 iterations in 481.15 seconds (average 2.498072, setup 136.42)
Prob0E: 89 iterations in 23.63 seconds (average 0.265528, setup 0.00)
Prob1A: 4 iterations in 0.99 seconds (average 0.248750, setup 0.00)
yes = 82818, no = 76902300, maybe = 39206591
Computing remaining probabilities...
Engine: Sparse
Building sparse matrix... [n=116191709, nc=64081283, nnz=155549122, k=2] [1.9 GB]
Creating vector for yes... [886.5 MB]
Allocating iteration vectors... [2 x 886.5 MB]
TOTAL: [4.5 GB]
Starting iterations...
Iteration 4: max relative diff=1.000000, 5.95 sec so far
Iteration 8: max relative diff=1.000000, 11.54 sec so far
Iteration 12: max relative diff=1.000000, 17.18 sec so far
Iteration 16: max relative diff=1.000000, 23.96 sec so far
Iteration 20: max relative diff=1.000000, 29.79 sec so far
Iteration 24: max relative diff=1.000000, 35.49 sec so far
Iteration 28: max relative diff=1.000000, 41.19 sec so far
Iteration 32: max relative diff=1.000000, 46.95 sec so far
Iteration 36: max relative diff=1.000000, 52.76 sec so far
Iteration 40: max relative diff=1.000000, 58.56 sec so far
Iteration 44: max relative diff=1.000000, 64.47 sec so far
Iteration 48: max relative diff=1.000000, 70.44 sec so far
Iteration 52: max relative diff=1.000000, 76.45 sec so far
Iteration 56: max relative diff=1.000000, 82.56 sec so far
Iteration 60: max relative diff=1.000000, 88.61 sec so far
Iteration 64: max relative diff=1.000000, 94.63 sec so far
Iteration 68: max relative diff=1.000000, 100.61 sec so far
Iteration 72: max relative diff=1.000000, 106.62 sec so far
Iteration 76: max relative diff=1.000000, 112.73 sec so far
Iteration 80: max relative diff=1.000000, 118.74 sec so far
Iteration 84: max relative diff=1.000000, 124.71 sec so far
Iteration 88: max relative diff=1.000000, 130.63 sec so far
Iteration 92: max relative diff=0.419422, 136.54 sec so far
Iteration 96: max relative diff=0.318358, 142.39 sec so far
Iteration 100: max relative diff=0.191568, 148.34 sec so far
Iteration 104: max relative diff=0.095506, 154.19 sec so far
Iteration 108: max relative diff=0.050126, 159.98 sec so far
Iteration 112: max relative diff=0.018273, 165.70 sec so far
Iteration 116: max relative diff=0.006704, 171.41 sec so far
Iteration 120: max relative diff=0.002252, 177.17 sec so far
Iteration 124: max relative diff=0.000285, 182.90 sec so far
Iteration 128: max relative diff=0.000098, 188.57 sec so far
Iteration 132: max relative diff=0.000027, 194.27 sec so far
Iteration 136: max relative diff=0.000004, 199.96 sec so far
Iterative method: 139 iterations in 264.80 seconds (average 1.469381, setup 60.55)
Value in the initial state: 397.5997676844599
Time for model checking: 784.71 seconds.
Result: 397.5997676844599 (value in the initial state)
---------------------------------------------------------------------
Model checking: R{"success"}min=? [ F "deadlock" ]/Pmax=? [ F "MissionSuccessful" ]
Prob0A: 5 iterations in 0.74 seconds (average 0.148400, setup 0.00)
Prob1E: 6 iterations in 0.43 seconds (average 0.072167, setup 0.00)
Warning: PRISM hasn't checked for zero-reward loops.
Your minimum rewards may be too low...
goal = 1, inf = 0, maybe = 116191708
Computing remaining rewards...
Engine: Sparse
Building sparse matrix (transitions)... [n=116191709, nc=153547097, nnz=290191120, k=2] [4.2 GB]
Building sparse matrix (transition rewards)... [n=116191709, nc=153547097, nnz=153667, k=2] [1.0 GB]
Creating vector for state rewards... [886.5 MB]
Creating vector for inf... [886.5 MB]
Allocating iteration vectors... [2 x 886.5 MB]
TOTAL: [8.7 GB]
Starting iterations...
Iteration 2: max relative diff=1.000000, 5.02 sec so far
Iteration 5: max relative diff=1.000000, 12.24 sec so far
Iteration 8: max relative diff=1.000000, 19.46 sec so far
Iteration 11: max relative diff=1.000000, 26.71 sec so far
Iteration 14: max relative diff=1.000000, 33.97 sec so far
Iteration 17: max relative diff=1.000000, 41.26 sec so far
Iteration 20: max relative diff=1.000000, 48.52 sec so far
Iteration 23: max relative diff=1.000000, 55.80 sec so far
Iteration 26: max relative diff=1.000000, 63.25 sec so far
Iteration 29: max relative diff=1.000000, 70.61 sec so far
Iteration 32: max relative diff=1.000000, 77.98 sec so far
Iteration 35: max relative diff=1.000000, 85.42 sec so far
Iteration 38: max relative diff=1.000000, 92.94 sec so far
Iteration 41: max relative diff=1.000000, 100.43 sec so far
Iteration 43: max relative diff=1.000000, 105.46 sec so far
Iteration 45: max relative diff=1.000000, 110.47 sec so far
Iteration 47: max relative diff=1.000000, 115.52 sec so far
Iteration 49: max relative diff=1.000000, 120.56 sec so far
Iteration 51: max relative diff=1.000000, 125.67 sec so far
Iteration 53: max relative diff=1.000000, 130.74 sec so far
Iteration 55: max relative diff=1.000000, 135.87 sec so far
Iteration 57: max relative diff=1.000000, 140.94 sec so far
Iteration 59: max relative diff=1.000000, 146.02 sec so far
Iteration 61: max relative diff=1.000000, 151.11 sec so far
Iteration 63: max relative diff=1.000000, 157.01 sec so far
Iteration 65: max relative diff=1.000000, 162.42 sec so far
Iteration 67: max relative diff=1.000000, 167.81 sec so far
Iteration 69: max relative diff=1.000000, 173.18 sec so far
Iteration 71: max relative diff=1.000000, 178.54 sec so far
Iteration 73: max relative diff=1.000000, 184.22 sec so far
Iteration 75: max relative diff=1.000000, 189.60 sec so far
Iteration 77: max relative diff=1.000000, 195.09 sec so far
Iteration 79: max relative diff=1.000000, 200.71 sec so far
Iteration 81: max relative diff=1.000000, 206.31 sec so far
Iteration 83: max relative diff=1.000000, 212.01 sec so far
Iteration 85: max relative diff=1.000000, 217.62 sec so far
Iteration 87: max relative diff=1.000000, 223.27 sec so far
Iteration 89: max relative diff=1.000000, 228.78 sec so far
Iteration 91: max relative diff=0.637240, 234.12 sec so far
Iteration 93: max relative diff=0.438103, 239.52 sec so far
Iteration 95: max relative diff=0.351550, 244.89 sec so far
Iteration 97: max relative diff=0.318492, 251.46 sec so far
Iteration 99: max relative diff=0.302050, 257.10 sec so far
Iteration 101: max relative diff=0.196638, 262.13 sec so far
Iteration 103: max relative diff=0.135873, 267.20 sec so far
Iteration 105: max relative diff=0.102879, 272.44 sec so far
Iteration 108: max relative diff=0.071539, 279.95 sec so far
Iteration 111: max relative diff=0.033077, 287.42 sec so far
Iteration 114: max relative diff=0.016437, 294.88 sec so far
Iteration 117: max relative diff=0.009031, 302.36 sec so far
Iteration 120: max relative diff=0.004931, 309.74 sec so far
Iteration 123: max relative diff=0.001470, 317.16 sec so far
Iteration 126: max relative diff=0.000306, 324.60 sec so far
Iteration 129: max relative diff=0.000088, 332.06 sec so far
Iteration 132: max relative diff=0.000060, 339.54 sec so far
Iteration 135: max relative diff=0.000030, 346.94 sec so far
Iteration 138: max relative diff=0.000030, 354.35 sec so far
Iteration 141: max relative diff=0.000027, 361.76 sec so far
Iteration 144: max relative diff=0.000005, 369.07 sec so far
Iteration 147: max relative diff=0.000001, 376.35 sec so far
Iterative method: 148 iterations in 514.66 seconds (average 2.559426, setup 135.86)
Prob0A: 81 iterations in 17.04 seconds (average 0.210346, setup 0.00)
Prob1E: 4 iterations in 0.87 seconds (average 0.218500, setup 0.00)
yes = 82818, no = 72159702, maybe = 43949189
Computing remaining probabilities...
Engine: Sparse
Building sparse matrix... [n=116191709, nc=71940167, nnz=174316066, k=2] [2.1 GB]
Creating vector for yes... [886.5 MB]
Allocating iteration vectors... [2 x 886.5 MB]
TOTAL: [4.7 GB]
Starting iterations...
Iteration 4: max relative diff=1.000000, 6.07 sec so far
Iteration 8: max relative diff=1.000000, 12.03 sec so far
Iteration 12: max relative diff=1.000000, 17.94 sec so far
Iteration 16: max relative diff=1.000000, 23.94 sec so far
Iteration 20: max relative diff=1.000000, 29.93 sec so far
Iteration 24: max relative diff=1.000000, 35.98 sec so far
Iteration 28: max relative diff=1.000000, 42.19 sec so far
Iteration 32: max relative diff=1.000000, 48.31 sec so far
Iteration 36: max relative diff=1.000000, 54.51 sec so far
Iteration 40: max relative diff=1.000000, 60.80 sec so far
Iteration 44: max relative diff=1.000000, 67.14 sec so far
Iteration 48: max relative diff=1.000000, 73.53 sec so far
Iteration 52: max relative diff=1.000000, 79.96 sec so far
Iteration 56: max relative diff=1.000000, 86.45 sec so far
Iteration 60: max relative diff=1.000000, 92.87 sec so far
Iteration 64: max relative diff=1.000000, 99.35 sec so far
Iteration 68: max relative diff=1.000000, 105.82 sec so far
Iteration 72: max relative diff=1.000000, 112.25 sec so far
Iteration 76: max relative diff=1.000000, 118.67 sec so far
Iteration 80: max relative diff=1.000000, 125.05 sec so far
Iteration 84: max relative diff=0.264073, 131.48 sec so far
Iteration 88: max relative diff=0.136806, 137.81 sec so far
Iteration 92: max relative diff=0.094611, 144.18 sec so far
Iteration 96: max relative diff=0.059328, 150.44 sec so far
Iteration 100: max relative diff=0.024506, 156.71 sec so far
Iteration 104: max relative diff=0.008762, 162.95 sec so far
Iteration 108: max relative diff=0.003046, 169.11 sec so far
Iteration 112: max relative diff=0.000556, 175.25 sec so far
Iteration 116: max relative diff=0.000153, 181.37 sec so far
Iteration 120: max relative diff=0.000022, 187.48 sec so far
Iteration 124: max relative diff=0.000003, 193.60 sec so far
Iterative method: 126 iterations in 263.94 seconds (average 1.560278, setup 67.34)
Value in the initial state: 293.6345515215482
Time for model checking: 813.041 seconds.
Result: 293.6345515215482 (value in the initial state)
---------------------------------------------------------------------
Note: There were 11 warnings during computation.
PaperModel/summary_result_uav_mdp.txt 000644 000765 000024 00000003365 12646112537 020620 0 ustar 00ruth staff 000000 000000 Time for model construction: 488.044 seconds.
Type: MDP
States: 116191709 (1 initial)
Transitions: 290191121
Choices: 153547098
Transition matrix: 446910 nodes (133 terminal), 290191121 minterms, vars: 37r/37c/17nd
(1) Pmax=? [ F "MissionSuccessful" ] , 0.7610284756344345 , 324.671 , 4.7 GB
(2) Pmin=? [ F "MissionSuccessful" ] , 0.6787083686458641 , 301.359 , 4.5 GB
(3) Pmax=? [ F "MissionTimeUp" ] , 5.159769973549628E-9 , 409.384 , 5.2 GB
(4) Pmin=? [ F "MissionTimeUp" ] , 3.575324529773406E-17 , 485.793 , 5.2 GB
(5) Pmax=? [ F "Crash" ] , 0.0627708316469184 , 395.261 , 5.4 GB
(6) Pmin=? [ F "Crash" ] , 0.05518770124189629 , 337.509 , 5.4 GB
(7) Pmax=? [ F "AllAreaSearched" ] , 0.2616990621972663 , 318.66 , 4.9 GB
(8) Pmin=? [ F "AllAreaSearched" ] , 0.180815758831309 , 298.681 , 4.9 GB
(9) Pmax=? [ F "MissionTimeUp"|"AllAreaSearched"|"Crash" ] , 0.32129081972405277 , 363.379 , 4.5 GB
(10) Pmin=? [ F "MissionTimeUp"|"AllAreaSearched"|"Crash" ] , 0.23897082858778257 , 298.315 , 4.7 GB
(11) filter(print, "deadlock", true) , false , 0.03 ,
(12) R{"drop"}max=? [ F "deadlock" ] ,0.029584782191533654 , 507.297 , 8.7 GB
(13) R{"drop"}min=? [ F "deadlock" ] , 0.026210917006325468 , 445.57 , 8.7 GB
(14) R{"charge"}max=? [ F "deadlock" ] , 0.7376191240350886 , 465.644 , 8.7 GB
(15) R{"charge"}min=? [ F "deadlock" ] , 0.24430484376692715 , 446.294 , 8.7 GB
(16) R{"time"}max=? [ F "deadlock" ] , 345.2910501408803 , 521.245 , 9.4 GB
(17) R{"time"}min=? [ F "deadlock" ] , 303.52431284485687 , 521.412 , 9.4 GB
(18) R{"success"}max=? [ F "deadlock" ]/Pmin=? [ F "MissionSuccessful" ] , 397.5997676844599 , 784.71 , 8.7 GB , 4.5 GB
(19) R{"success"}min=? [ F "deadlock" ]/Pmax=? [ F "MissionSuccessful" ] , 293.6345515215482 , 813.041 , 8.7 GB , 4.7 GB
PaperModel/uav_deadline1.gra 000644 000765 000024 00000010361 12647404400 016431 0 ustar 00ruth staff 000000 000000
PaperModel/uav_deadline1.pdf 000644 000765 000024 00000053005 12647404400 016433 0 ustar 00ruth staff 000000 000000 %PDF-1.3
%Äåòåë§ó ÐÄÆ
4 0 obj
<< /Length 5 0 R /Filter /FlateDecode >>
stream
xËŽ,IŽž÷ñùÙq¿¬{1À Zz1A«’zB× ZÌëëû~’æyòTz¤Sd˜›Ñx'ÍÜóŸÿöñÏ#ÿ»>çÛñãÿýŸÿø¯¿üõ·ÓÇ/¿}œò¿ß~ùøË¿€øß¾ŽýûÇåuúx>Ï÷Çýãuû¸ß>¯÷ëóÀ<ÿ8?þûãüñ¯5Ý_ÿ–§û«‹~ž
ìùÕ©n§Ûýüy9ü
I·þññ·¢õ'½NOIèÇüÉc‡YmÆ}Yü'}ðX¨Ú<Íõ؉
Ÿ>þovwúÍÂíÓõzý|>¥úøZ`oV±œ>àýõxuäçµG
]>/Ï+¿\>OG¸t=ç×ëñ¼þÛ玟Ïä_]bžÌry*#ùåöy{]æ)àûnÎü÷Á‘³âü*5óäFç/ˆ_ÉaÄwÂ>°©µáì?àåòYÛ:}ֶ¶åØs€PûüD×ÃTÇl¬Ÿ
P|ÍX»Ý>kkýà}?oٛ˯ù94ͳ;zùøÏè£":FD§ëçåúø8]^Ÿ§×Ã
ÆÉ>ïçÓÇ?ÀÜ>ïPñæöy>?2æþyqgw,êÎ#¦«GÏÛázz2pÁÐ|z}žO÷<ÁˆÀÏ~"3œŸç›OÔ<æù:…0Ö¼žOŸµæþùxÏŸ+fß°ãј×sa„_ã׫”Öl§«¹Ÿ¥èöù<¿?¿WÔíÙd@ñíw‰ë
¢š›;r½<ïrjƸ±¦ |:!àûÍ}aׄ,aìTÞÎ „}z>ÝÑûÅ©ëçéQ;iÞm„ÁžØÈ*x#ªaIz"‹ççí&çXñ‰HóÉÌ
kM‘oÓ”XÕ½ž8ÝÙÄR™EÓ`
ÿùq½œ X½Å©";”ïrü¼8£”Ýõü‚ÙHø¡?±3(iXæ¨Yµ7F®çÇçãT3œá’ðå„ñÄäwô TþõtOuü¼â‰†*øÌÞê‰q‚è*s¯±ãÏk¨dÍhÎk½ä‰ççÕ5ôZ÷'T±„ð
5pŸw£Dìæõ¨'¢,Œô¼a¢—+’gÄ
R.‡šÀK(‚ŜץT¥