Interactive version:
.
.
Working with Schedulers¶
In non-deterministic models the notion of a scheduler (or policy) is important. The scheduler determines which action to take at each state.
For a given reachability property, Storm can return the scheduler realizing the resulting probability.
Examining Schedulers for MDPs¶
As in Getting Started, we import some required modules and build a model from the example files:
[1]:
>>> import stormpy
>>> import stormpy.examples
>>> import stormpy.examples.files
>>> path = stormpy.examples.files.prism_mdp_coin_2_2
>>> formula_str = "Pmin=? [F \"finished\" & \"all_coins_equal_1\"]"
>>> program = stormpy.parse_prism_program(path)
>>> formulas = stormpy.parse_properties(formula_str, program)
>>> model = stormpy.build_model(program, formulas)
Next we check the model and make sure to extract the scheduler:
[2]:
>>> result = stormpy.model_checking(model, formulas[0], extract_scheduler=True)
The result then contains the scheduler we want:
[3]:
>>> assert result.has_scheduler
>>> scheduler = result.scheduler
>>> assert scheduler.memoryless
>>> assert scheduler.deterministic
>>> print(scheduler)
___________________________________________________________________
Fully defined memoryless deterministic scheduler:
model state: choice(s)
0 0
1 0
2 1
3 0
4 0
5 0
6 0
7 0
8 0
9 1
10 0
11 0
12 0
13 0
14 0
15 0
16 0
17 0
18 0
19 0
20 0
21 1
22 1
23 0
24 1
25 0
26 0
27 0
28 0
29 0
30 1
31 0
32 0
33 0
34 0
35 0
36 0
37 1
38 1
39 0
40 0
41 0
42 0
43 0
44 0
45 1
46 0
47 0
48 0
49 0
50 0
51 0
52 0
53 1
54 0
55 1
56 1
57 0
58 0
59 0
60 0
61 1
62 0
63 1
64 0
65 0
66 0
67 0
68 0
69 1
70 1
71 0
72 0
73 0
74 0
75 0
76 0
77 1
78 0
79 0
80 0
81 0
82 0
83 1
84 0
85 0
86 0
87 0
88 0
89 0
90 1
91 1
92 0
93 0
94 0
95 1
96 0
97 1
98 0
99 0
100 0
101 1
102 1
103 0
104 0
105 0
106 0
107 0
108 0
109 1
110 0
111 0
112 0
113 0
114 0
115 0
116 1
117 1
118 0
119 0
120 0
121 0
122 0
123 0
124 0
125 0
126 1
127 0
128 0
129 0
130 0
131 1
132 0
133 0
134 0
135 0
136 0
137 0
138 0
139 0
140 0
141 0
142 0
143 0
144 0
145 0
146 0
147 0
148 0
149 0
150 0
151 0
152 0
153 0
154 0
155 0
156 0
157 0
158 0
159 0
160 0
161 0
162 0
163 0
164 0
165 0
166 0
167 0
168 0
169 0
170 0
171 0
172 0
173 0
174 0
175 0
176 0
177 0
178 0
179 0
180 0
181 0
182 0
183 0
184 0
185 0
186 0
187 0
188 0
189 0
190 0
191 0
192 0
193 0
194 0
195 0
196 0
197 0
198 0
199 0
200 0
201 0
202 0
203 0
204 0
205 0
206 0
207 0
208 0
209 0
210 0
211 0
212 0
213 0
214 0
215 0
216 0
217 0
218 0
219 0
220 0
221 0
222 0
223 0
224 0
225 0
226 0
227 0
228 0
229 0
230 0
231 0
232 0
233 0
234 0
235 0
236 0
237 0
238 0
239 0
240 0
241 0
242 0
243 0
244 0
245 0
246 0
247 0
248 0
249 0
250 0
251 0
252 0
253 0
254 0
255 0
256 0
257 0
258 0
259 0
260 0
261 0
262 0
263 0
264 0
265 0
266 0
267 0
268 0
269 0
270 0
271 0
___________________________________________________________________
To get the information which action the scheduler chooses in which state, we can simply iterate over the states:
[4]:
>>> for state in model.states:
... choice = scheduler.get_choice(state)
... action = choice.get_deterministic_choice()
... print("In state {} choose action {}".format(state, action))
In state 0 choose action 0
In state 1 choose action 0
In state 2 choose action 1
In state 3 choose action 0
In state 4 choose action 0
In state 5 choose action 0
In state 6 choose action 0
In state 7 choose action 0
In state 8 choose action 0
In state 9 choose action 1
In state 10 choose action 0
In state 11 choose action 0
In state 12 choose action 0
In state 13 choose action 0
In state 14 choose action 0
In state 15 choose action 0
In state 16 choose action 0
In state 17 choose action 0
In state 18 choose action 0
In state 19 choose action 0
In state 20 choose action 0
In state 21 choose action 1
In state 22 choose action 1
In state 23 choose action 0
In state 24 choose action 1
In state 25 choose action 0
In state 26 choose action 0
In state 27 choose action 0
In state 28 choose action 0
In state 29 choose action 0
In state 30 choose action 1
In state 31 choose action 0
In state 32 choose action 0
In state 33 choose action 0
In state 34 choose action 0
In state 35 choose action 0
In state 36 choose action 0
In state 37 choose action 1
In state 38 choose action 1
In state 39 choose action 0
In state 40 choose action 0
In state 41 choose action 0
In state 42 choose action 0
In state 43 choose action 0
In state 44 choose action 0
In state 45 choose action 1
In state 46 choose action 0
In state 47 choose action 0
In state 48 choose action 0
In state 49 choose action 0
In state 50 choose action 0
In state 51 choose action 0
In state 52 choose action 0
In state 53 choose action 1
In state 54 choose action 0
In state 55 choose action 1
In state 56 choose action 1
In state 57 choose action 0
In state 58 choose action 0
In state 59 choose action 0
In state 60 choose action 0
In state 61 choose action 1
In state 62 choose action 0
In state 63 choose action 1
In state 64 choose action 0
In state 65 choose action 0
In state 66 choose action 0
In state 67 choose action 0
In state 68 choose action 0
In state 69 choose action 1
In state 70 choose action 1
In state 71 choose action 0
In state 72 choose action 0
In state 73 choose action 0
In state 74 choose action 0
In state 75 choose action 0
In state 76 choose action 0
In state 77 choose action 1
In state 78 choose action 0
In state 79 choose action 0
In state 80 choose action 0
In state 81 choose action 0
In state 82 choose action 0
In state 83 choose action 1
In state 84 choose action 0
In state 85 choose action 0
In state 86 choose action 0
In state 87 choose action 0
In state 88 choose action 0
In state 89 choose action 0
In state 90 choose action 1
In state 91 choose action 1
In state 92 choose action 0
In state 93 choose action 0
In state 94 choose action 0
In state 95 choose action 1
In state 96 choose action 0
In state 97 choose action 1
In state 98 choose action 0
In state 99 choose action 0
In state 100 choose action 0
In state 101 choose action 1
In state 102 choose action 1
In state 103 choose action 0
In state 104 choose action 0
In state 105 choose action 0
In state 106 choose action 0
In state 107 choose action 0
In state 108 choose action 0
In state 109 choose action 1
In state 110 choose action 0
In state 111 choose action 0
In state 112 choose action 0
In state 113 choose action 0
In state 114 choose action 0
In state 115 choose action 0
In state 116 choose action 1
In state 117 choose action 1
In state 118 choose action 0
In state 119 choose action 0
In state 120 choose action 0
In state 121 choose action 0
In state 122 choose action 0
In state 123 choose action 0
In state 124 choose action 0
In state 125 choose action 0
In state 126 choose action 1
In state 127 choose action 0
In state 128 choose action 0
In state 129 choose action 0
In state 130 choose action 0
In state 131 choose action 1
In state 132 choose action 0
In state 133 choose action 0
In state 134 choose action 0
In state 135 choose action 0
In state 136 choose action 0
In state 137 choose action 0
In state 138 choose action 0
In state 139 choose action 0
In state 140 choose action 0
In state 141 choose action 0
In state 142 choose action 0
In state 143 choose action 0
In state 144 choose action 0
In state 145 choose action 0
In state 146 choose action 0
In state 147 choose action 0
In state 148 choose action 0
In state 149 choose action 0
In state 150 choose action 0
In state 151 choose action 0
In state 152 choose action 0
In state 153 choose action 0
In state 154 choose action 0
In state 155 choose action 0
In state 156 choose action 0
In state 157 choose action 0
In state 158 choose action 0
In state 159 choose action 0
In state 160 choose action 0
In state 161 choose action 0
In state 162 choose action 0
In state 163 choose action 0
In state 164 choose action 0
In state 165 choose action 0
In state 166 choose action 0
In state 167 choose action 0
In state 168 choose action 0
In state 169 choose action 0
In state 170 choose action 0
In state 171 choose action 0
In state 172 choose action 0
In state 173 choose action 0
In state 174 choose action 0
In state 175 choose action 0
In state 176 choose action 0
In state 177 choose action 0
In state 178 choose action 0
In state 179 choose action 0
In state 180 choose action 0
In state 181 choose action 0
In state 182 choose action 0
In state 183 choose action 0
In state 184 choose action 0
In state 185 choose action 0
In state 186 choose action 0
In state 187 choose action 0
In state 188 choose action 0
In state 189 choose action 0
In state 190 choose action 0
In state 191 choose action 0
In state 192 choose action 0
In state 193 choose action 0
In state 194 choose action 0
In state 195 choose action 0
In state 196 choose action 0
In state 197 choose action 0
In state 198 choose action 0
In state 199 choose action 0
In state 200 choose action 0
In state 201 choose action 0
In state 202 choose action 0
In state 203 choose action 0
In state 204 choose action 0
In state 205 choose action 0
In state 206 choose action 0
In state 207 choose action 0
In state 208 choose action 0
In state 209 choose action 0
In state 210 choose action 0
In state 211 choose action 0
In state 212 choose action 0
In state 213 choose action 0
In state 214 choose action 0
In state 215 choose action 0
In state 216 choose action 0
In state 217 choose action 0
In state 218 choose action 0
In state 219 choose action 0
In state 220 choose action 0
In state 221 choose action 0
In state 222 choose action 0
In state 223 choose action 0
In state 224 choose action 0
In state 225 choose action 0
In state 226 choose action 0
In state 227 choose action 0
In state 228 choose action 0
In state 229 choose action 0
In state 230 choose action 0
In state 231 choose action 0
In state 232 choose action 0
In state 233 choose action 0
In state 234 choose action 0
In state 235 choose action 0
In state 236 choose action 0
In state 237 choose action 0
In state 238 choose action 0
In state 239 choose action 0
In state 240 choose action 0
In state 241 choose action 0
In state 242 choose action 0
In state 243 choose action 0
In state 244 choose action 0
In state 245 choose action 0
In state 246 choose action 0
In state 247 choose action 0
In state 248 choose action 0
In state 249 choose action 0
In state 250 choose action 0
In state 251 choose action 0
In state 252 choose action 0
In state 253 choose action 0
In state 254 choose action 0
In state 255 choose action 0
In state 256 choose action 0
In state 257 choose action 0
In state 258 choose action 0
In state 259 choose action 0
In state 260 choose action 0
In state 261 choose action 0
In state 262 choose action 0
In state 263 choose action 0
In state 264 choose action 0
In state 265 choose action 0
In state 266 choose action 0
In state 267 choose action 0
In state 268 choose action 0
In state 269 choose action 0
In state 270 choose action 0
In state 271 choose action 0
Examining Schedulers for Markov automata¶
Currently there is no support yet for scheduler extraction on MAs. However, if the timing information is not relevant for the property, we can circumvent this lack by first transforming the MA to an MDP.
We build the model as before:
[5]:
>>> path = stormpy.examples.files.prism_ma_simple
>>> formula_str = "Tmin=? [ F s=4 ]"
>>> program = stormpy.parse_prism_program(path, False, True)
>>> formulas = stormpy.parse_properties_for_prism_program(formula_str, program)
>>> ma = stormpy.build_model(program, formulas)
Next we transform the continuous-time model into a discrete-time model. Note that all timing information is lost at this point:
[6]:
>>> mdp, mdp_formulas = stormpy.transform_to_discrete_time_model(ma, formulas)
>>> assert mdp.model_type == stormpy.ModelType.MDP
After the transformation we have obtained an MDP where we can extract the scheduler as shown before:
[7]:
>>> result = stormpy.model_checking(mdp, mdp_formulas[0], extract_scheduler=True)
>>> scheduler = result.scheduler
>>> print(scheduler)
___________________________________________________________________
Fully defined memoryless deterministic scheduler:
model state: choice(s)
0 1
1 0
2 0
3 0
4 0
___________________________________________________________________