-
Notifications
You must be signed in to change notification settings - Fork 0
/
casestudy.profeat
371 lines (316 loc) · 20.1 KB
/
casestudy.profeat
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
mdp
// Scenario 1: Short pipeline inspection in the North Sea
const int max_visib = 10; // The maximum visibility
const int min_visib = 1; // The minimum visibility
const double current_prob = 0.6; // The probability of currents
const int inspect = 10; // The meters of pipeline that should be inspected
const double camera_block_prob = 0.05; // The probability the camera getting blocked (e.g. because of something in front of the camera)
// Scenario 2: Longer pipeline inspection in the Caribbean Sea
//const int max_visib = 20;
//const int min_visib = 3;
//const double current_prob = 0.3;
//const int inspect = 30;
//const double camera_block_prob = 0.03;
// Scenario independent parameters
const int infl_tf = 10; // The influence a thruster failure has on the path of the AUV. The bigger the value, the less influence a thruster failure has on the path (it can keep the path even in case of a thruster failure)
const double sonar_fail_prob = 0.01; // The probability of a sonar failure
const double camera_fail_prob = 0.005; // The probability of a camera failure
const double camera_unblock_prob = current_prob*0.8; // The probability of the camera getting unblocked depends on the current probability
// Formulas
formula med_visib = (max_visib-min_visib)/3;
formula high_visib = 2*(max_visib-min_visib)/3;
formula camera_unavailable = camera_failed | camera_blocked;
////////////////
// Feature Model
///////////////
root feature
all of robot;
modules auv, environment, hardware;
rewards "time"
[step] true : 1; // Every transition is a time step
endrewards
rewards "energy"
// Costs for being in a recovery state
(s=recover_very_high) : 2;
(s=recover_high) : 2;
(s=recover_med) : 2;
(s=recover_low) : 2;
(s=recover_following) : 2;
// Costs for switching altitudes
(s=search_very_high) & active(high) : 2;
(s=search_very_high) & active(med) : 4;
(s=search_very_high) & active(low) : 6;
(s=search_high) & active(very_high) : 2;
(s=search_high) & active(med) : 2;
(s=search_high) & active(low) : 4;
(s=search_med) & active(very_high) : 4;
(s=search_med) & active(high) : 2;
(s=search_med) & active(low) : 2;
(s=search_low) & active(very_high) : 6;
(s=search_low) & active(high) : 4;
(s=search_low) & active(med) : 2;
// Costs for going to low altitude when the pipeline is found
(s=found) & active(very_high) : 6;
(s=found) & active(high) : 4;
(s=found) & active(med) : 2;
// Costs for all other states
(s=start_task) : 1;
(s=start_search) : 1;
(s=search_high) & active(high) : 1;
(s=search_med) & active(med) : 1;
(s=search_low) & active(low) : 1;
(s=found) & active(low) : 1;
(s=following) : 1;
(s=lost_pipe) : 1;
// Additional costs for sonar because it takes more energy than camera
active(sonar) : 3;
endrewards
endfeature
feature robot
all of navigation, pipeline_inspection, vision;
endfeature
feature navigation
one of low, med, high, very_high;
initial constraint active(very_high); // To ensure that low is active in the beginning
endfeature
feature pipeline_inspection
one of search, follow;
initial constraint active(search); // To ensure that search is active in the beginning
endfeature
feature vision
[0..1] of sonar, camera;
initial constraint active(sonar); // To ensure that sonar is active in the beginning
endfeature
feature low endfeature
feature med endfeature
feature high endfeature
feature very_high endfeature
feature search endfeature
feature follow
constraint active(follow) => active(low);
endfeature
feature sonar endfeature
feature camera
constraint active(camera) => !active(very_high);
endfeature
/////////////////////
// States
////////////////////
const int start_search = 0;
const int search_high = 1;
const int search_med = 2;
const int search_low = 3;
const int found = 4;
const int following = 5;
const int recover_high = 6;
const int recover_med = 7;
const int recover_low = 8;
const int recover_following = 9;
const int done = 10;
const int start_task = 11;
const int lost_pipe = 12;
const int abort_mission = 13;
const int search_very_high = 14;
const int recover_very_high = 15;
////////////////////
// Environment
////////////////////
// The environment module models the changes in the water visibility
// If there is a current, then the water visibility reduces by 1, if there is not, it increases by 1 or stays the same
module environment
water_visib : [min_visib..max_visib] init round((max_visib-min_visib)/2);
[step] true -> current_prob: (water_visib'= (water_visib=min_visib? min_visib : water_visib-1))
+ (1-current_prob)/2: (water_visib'= (water_visib=max_visib? max_visib : water_visib+1))
+ (1-current_prob)/2: true;
endmodule
////////////////////
// Hardware
////////////////////
// The module hardware models models the failures of the vision components
// Every time step, the sonar and the camera fail with the respecitve failure probability, or both sensors fail.
module hardware
sonar_failed : bool init false;
camera_failed : bool init false;
camera_blocked : bool init false;
/////// Everything is working
// One of the sensors fails/gets blocked
[step] (!sonar_failed & !camera_failed & !camera_blocked) -> sonar_fail_prob: (sonar_failed' = true) + (1-sonar_fail_prob): true;
[step] (!sonar_failed & !camera_failed & !camera_blocked) -> camera_fail_prob: (camera_failed' = true) + (1-camera_fail_prob): true;
[step] (!sonar_failed & !camera_failed & !camera_blocked) -> camera_block_prob: (camera_blocked' = true) + (1-camera_block_prob): true;
// Two sensors fail/get blocked at the same time
[step] (!sonar_failed & !camera_failed & !camera_blocked) -> camera_fail_prob*sonar_fail_prob: (camera_failed' = true) & (sonar_failed' = true)
+ (1-camera_fail_prob*sonar_fail_prob): true;
[step] (!sonar_failed & !camera_blocked & !camera_blocked) -> sonar_fail_prob*camera_block_prob: (camera_blocked' = true) & (sonar_failed' = true)
+ (1-sonar_fail_prob*camera_block_prob): true;
[step] (!camera_failed & !camera_blocked & !camera_blocked) -> camera_fail_prob*camera_block_prob: (camera_blocked' = true) & (camera_failed' = true)
+ (1-camera_fail_prob*camera_block_prob): true;
// Everything fails/gets blocked at the same time
[step] (!camera_failed & !camera_blocked & !sonar_failed) -> camera_fail_prob*camera_block_prob*sonar_fail_prob: (camera_blocked' = true) & (camera_failed' = true) & (sonar_failed' = true)
+ (1-camera_fail_prob*camera_block_prob*sonar_fail_prob): true;
/////// Sonar failed
[step] (sonar_failed & !camera_failed & !camera_blocked) -> camera_fail_prob: (camera_failed' = true) + (1-camera_fail_prob): true;
[step] (sonar_failed & !camera_failed & !camera_blocked) -> camera_block_prob: (camera_blocked' = true) + (1-camera_block_prob): true;
[step] (sonar_failed & !camera_failed & !camera_blocked) -> camera_fail_prob*camera_block_prob: (camera_failed' = true) & (camera_blocked' = true)
+ (1-camera_fail_prob*camera_block_prob): true;
/////// Camera failed
[step] (camera_failed & !sonar_failed & !camera_blocked) -> sonar_fail_prob: (sonar_failed' = true) + (1-sonar_fail_prob): true;
[step] (camera_failed & !sonar_failed & !camera_blocked) -> camera_block_prob: (camera_blocked' = true) + (1-camera_block_prob): true;
[step] (camera_failed & !sonar_failed & !camera_blocked) -> sonar_fail_prob*camera_block_prob: (sonar_failed' = true) & (camera_blocked' = true)
+ (1-sonar_fail_prob*camera_block_prob): true;
/////// Camera blocked
// Sonar or camera fail or both
[step] (camera_blocked & !sonar_failed & !camera_failed) -> sonar_fail_prob: (sonar_failed' = true) + (1-sonar_fail_prob): true;
[step] (camera_blocked & !sonar_failed & !camera_failed) -> camera_fail_prob: (camera_failed' = true) + (1-camera_fail_prob): true;
[step] (camera_blocked & !sonar_failed & !camera_failed) -> sonar_fail_prob*camera_fail_prob: (sonar_failed' = true) & (camera_failed' = true)
+ (1-sonar_fail_prob*camera_fail_prob): true;
// Camera gets unblocked
[step] (camera_blocked & !sonar_failed & !camera_failed) -> camera_unblock_prob: (camera_blocked' = false) + (1-camera_unblock_prob): true;
// Camera gets unblocked and one or two sensors fail
[step] (camera_blocked & !sonar_failed & !camera_failed) -> sonar_fail_prob*camera_unblock_prob: (sonar_failed' = true) & (camera_blocked' = false)
+ (1-sonar_fail_prob*camera_unblock_prob): true;
[step] (camera_blocked & !sonar_failed & !camera_failed) -> camera_fail_prob*camera_unblock_prob: (camera_failed' = true) & (camera_blocked' = false)
+ (1-camera_fail_prob*camera_unblock_prob): true;
[step] (camera_blocked & !sonar_failed & !camera_failed) -> camera_fail_prob*sonar_fail_prob*camera_unblock_prob: (camera_failed' = true) & (sonar_failed' = true) & (camera_blocked' = false)
+ (1-camera_fail_prob*sonar_fail_prob*camera_unblock_prob): true;
/////// Sonar failed and camera blocked
[step] (camera_blocked & sonar_failed & !camera_failed) -> camera_fail_prob: (camera_failed' = true) + (1-camera_fail_prob): true;
[step] (camera_blocked & sonar_failed & !camera_failed) -> camera_unblock_prob: (camera_blocked' = false) + (1-camera_unblock_prob): true;
[step] (camera_blocked & sonar_failed & !camera_failed) -> camera_unblock_prob*camera_fail_prob: (camera_blocked' = false) & (camera_failed' = true)
+ (1-camera_unblock_prob*camera_fail_prob): true;
/////// Camera failed and camera blocked
[step] (camera_blocked & camera_failed & !sonar_failed) -> sonar_fail_prob: (sonar_failed' = true) + (1-sonar_fail_prob): true;
[step] (camera_blocked & camera_failed & !sonar_failed) -> camera_unblock_prob: (camera_blocked' = false) + (1-camera_unblock_prob): true;
[step] (camera_blocked & camera_failed & !sonar_failed) -> camera_unblock_prob*sonar_fail_prob: (camera_blocked' = false) & (sonar_failed' = true)
+ (1-camera_unblock_prob*sonar_fail_prob): true;
/////// Sonar failed and camera failed
[step] (sonar_failed & camera_failed & !camera_blocked) -> camera_block_prob: (camera_blocked' = true) + (1-camera_block_prob): true;
/////// Sonar failed and camera failed and camera blocked
[step] (camera_blocked & camera_failed & sonar_failed) -> camera_unblock_prob: (camera_blocked' = false) + (1-camera_unblock_prob): true;
endmodule
////////////////////
// Managed Subsystem
////////////////////
// The module auv implements the behaviour of the managed subystem of the AUV
// !active(camera) means that the camera is either blocked or failed
module auv
s : [0..15] init start_task;
d_insp : [0..inspect] init 0; // The meters of pipeline that are inspected (changed during runtime)
t_failed : [0..infl_tf] init 0; // The amount of times a thruster failed while following the pipeline (bounded by the influence a thruster failure has on the path of the AUV)
// To the correct task
[step] (s=start_task & active(search) & (active(camera) | active(sonar))) -> 1: (s'=start_search);
[step] (s=start_task & active(follow) & (active(camera) | active(sonar))) -> 1: (s'=following);
// From start_search to search state
[step] (s=start_search & active(very_high) & active(sonar)) -> 1: (s'=search_very_high);
[step] (s=start_search & active(high) & (active(camera) | active(sonar))) -> 1: (s'=search_high);
[step] (s=start_search & active(med) & (active(camera) | active(sonar))) -> 1: (s'=search_med);
[step] (s=start_search & active(low) & (active(camera) | active(sonar))) -> 1: (s'=search_low);
/////// From search state to another state
// Search very high
[step] (s=search_very_high & active(very_high) & active(sonar)) -> 0.66:(s'=found)
+ 0.33:(s'=search_very_high)
+ 0.01:(s'=recover_very_high);
[step] (s=search_very_high & active(high) & (active(camera) | active(sonar))) -> 1:(s'=search_high);
[step] (s=search_very_high & active(med) & (active(camera) | active(sonar))) -> 1:(s'=search_med);
[step] (s=search_very_high & active(low) & (active(camera) | active(sonar))) -> 1:(s'=search_low);
// Search high
[step] (s=search_high & active(high) & (active(camera) | active(sonar))) -> 0.59:(s'=found)
+ 0.4:(s'=search_high)
+ 0.01:(s'=recover_high);
[step] (s=search_high & active(very_high) & active(sonar)) -> 1:(s'=search_very_high);
[step] (s=search_high & active(med) & (active(camera) | active(sonar))) -> 1:(s'=search_med);
[step] (s=search_high & active(low) & (active(camera) | active(sonar))) -> 1:(s'=search_low);
// Search medium
[step] (s=search_med & active(med) & (active(camera) | active(sonar))) -> 0.48:(s'=found)
+ 0.5: (s'=search_med)
+ 0.02:(s'=recover_med);
[step] (s=search_med & active(very_high) & active(sonar)) -> 1:(s'=search_very_high);
[step] (s=search_med & active(high) & (active(camera) | active(sonar))) -> 1:(s'=search_high);
[step] (s=search_med & active(low) & (active(camera) | active(sonar))) -> 1:(s'=search_low);
// Search low
[step] (s=search_low & active(low) & (active(camera) | active(sonar))) -> 0.42:(s'=found)
+ 0.55: (s'=search_low)
+ 0.03:(s'=recover_low);
[step] (s=search_low & active(very_high) & active(sonar)) -> 1:(s'=search_very_high);
[step] (s=search_low & active(high) & (active(camera) | active(sonar))) -> 1:(s'=search_high);
[step] (s=search_low & active(med) & (active(camera) | active(sonar))) -> 1:(s'=search_med);
// Go to other task if pipeline is found
[step] (s=found) & (active(camera) | active(sonar)) -> 1:(s'=start_task);
// Following the pipeline
[step] (s=following) & (d_insp<inspect) & (t_failed=0) & (active(camera) | active(sonar))
-> 0.92: (s'=following) & (d_insp'=d_insp+1) // If the AUV didn't lose the pipeline for some time
+ 0.05: (s'=lost_pipe)
+ 0.03:(s'=recover_following) & (t_failed'=(t_failed<infl_tf? t_failed+1 : t_failed));
[step] (s=following) & (d_insp<inspect) & (t_failed>0) & (active(camera) | active(sonar))
-> 0.92*(1-t_failed/infl_tf): (s'=following) & (d_insp'=d_insp+1) & (t_failed'=t_failed-1) // If the AUV lost the pipeline in the last time steps,
+ 0.05*(1+((0.92*t_failed)/(0.05*infl_tf))): (s'=lost_pipe) // the probability of staying in following or losing the pipeline depends on the variable t_failed
+ 0.03:(s'=recover_following) & (t_failed'=(t_failed<infl_tf? t_failed+1 : t_failed));
[step] (s=following) & (d_insp=inspect) & (active(camera) | active(sonar)) -> (s'=done);
// Lost the pipeline
[step] (s=lost_pipe) & (active(camera) | active(sonar)) -> 1: (s'=start_task) & (t_failed'=0); // Reset the thruster failures (because the AUV will search for the pipeline again)
// Recovery states
[step] (s=recover_very_high) & active(sonar) -> 0.5:(s'=recover_very_high)
+ 0.5:(s'=search_very_high);
[step] (s=recover_high) & (active(camera) | active(sonar)) -> 0.5:(s'=recover_high)
+ 0.5:(s'=search_high);
[step] (s=recover_med) & (active(camera) | active(sonar)) -> 0.5:(s'=recover_med)
+ 0.5:(s'=search_med);
[step] (s=recover_low) & (active(camera) | active(sonar)) -> 0.5:(s'=recover_low)
+ 0.5:(s'=search_low);
[step] (s=recover_following) & (active(camera) | active(sonar)) -> 0.5:(s'=recover_following) & (t_failed'=(t_failed<infl_tf? t_failed+1 : t_failed))
+ 0.5:(s'=following);
// If sonar fails while in state recovery very high and the camera is active, then either keep recovering or go to search high (so camera can keep on searching)
[step] (s=recover_very_high) & !active(sonar) & active(camera) -> 0.5:(s'=recover_very_high)
+ 0.5:(s'=search_high);
// Abort mission if both sensors failed (if the mission has not been finished yet)
[step] (s!=done) & (s!=abort_mission) & (camera_failed & sonar_failed) -> 1: (s'=abort_mission);
// Wait that the camera gets unblocked if it is blocked but didn't fail and the sonar failed
[step] (s!=done) & (s!=abort_mission) & !active(sonar) & !active(camera) & !camera_failed -> 1: true;
// Self-loop for done state and abort_mission state
[step] (s=done) -> 1:(s'=done);
[step] (s=abort_mission) -> 1:(s'=abort_mission);
endmodule
/////////////////
// Feature Controller
////////////////
// The feature controller implements the adaptation logic of the managing subsystem of the AUV
controller
/////// Searching
// Prefer searching with the sonar if it is available
// Sonar should search on a very high altitude
[step] (s!=abort_mission) & (s!=found) & active(search) & !sonar_failed
-> activate(very_high) & deactivate(high) & deactivate(med) & deactivate(low) & activate(sonar) & deactivate(camera);
// Use camera if sonar is not available and camera is available (camera unavailable and sonar failed case below)
// Change altitude depending on water visibility (not possible on very high altitude)
[step] (s!=abort_mission) & (s!=found) & active(search) & sonar_failed & !camera_unavailable & water_visib<med_visib
-> activate(low) & deactivate(very_high) & deactivate(high) & deactivate(med) & activate(camera) & deactivate(sonar);
[step] (s!=abort_mission) & (s!=found) & active(search) & sonar_failed & !camera_unavailable & med_visib<=water_visib & water_visib<high_visib
-> activate(low) & deactivate(med) & deactivate(high) & deactivate(very_high) & activate(camera) & deactivate(sonar);
[step] (s!=abort_mission) & (s!=found) & active(search) & sonar_failed & !camera_unavailable & med_visib<=water_visib & water_visib<high_visib
-> activate(med) & deactivate(low) & deactivate(high) & deactivate(very_high) & activate(camera) & deactivate(sonar);
[step] (s!=abort_mission) & (s!=found) & active(search) & sonar_failed & !camera_unavailable & high_visib<=water_visib
-> activate(low) & deactivate(med) & deactivate(high) & deactivate(very_high) & activate(camera) & deactivate(sonar);
[step] (s!=abort_mission) & (s!=found) & active(search) & sonar_failed & !camera_unavailable & high_visib<=water_visib
-> activate(med) & deactivate(low) & deactivate(high) & deactivate(very_high) & activate(camera) & deactivate(sonar);
[step] (s!=abort_mission) & (s!=found) & active(search) & sonar_failed & !camera_unavailable & high_visib<=water_visib
-> activate(high) & deactivate(low) & deactivate(med) & deactivate(very_high) & activate(camera) & deactivate(sonar);
/////// Switch task from "search" to "follow"
// Prefer camera for following if it is available
[step] (s=found) & active(search) & !camera_unavailable -> deactivate(search) & activate(follow) & activate(low) & deactivate(med) & deactivate(high) & deactivate(very_high)
& activate(camera) & deactivate(sonar);
[step] (s=found) & active(search) & camera_unavailable & !sonar_failed -> deactivate(search) & activate(follow) & activate(low) & deactivate(med) & deactivate(high) & deactivate(very_high)
& activate(sonar) & deactivate(camera);
/////// Switch task from "follow" to "search"
// Prefer sonar for searching if it is available (camera unavailable and sonar failed case below)
[step] (s=lost_pipe) & active(follow) & !sonar_failed -> deactivate(follow) & activate(search) & activate(sonar) & deactivate(camera) & activate(very_high) & deactivate(high) & deactivate(med) & deactivate(low);
[step] (s=lost_pipe) & active(follow) & sonar_failed & !camera_unavailable -> deactivate(follow) & activate(search) & activate(camera) & deactivate(sonar);
/////// Follow the pipeline
// Use the camera for following/inspecting if it is available (camera unavailable and sonar failed case below)
[step] (s!=abort_mission) & (s!=lost_pipe) & active(follow) & !camera_unavailable -> activate(camera) & deactivate(sonar);
[step] (s!=abort_mission) & (s!=lost_pipe) & active(follow) & camera_unavailable & !sonar_failed -> activate(sonar) & deactivate(camera);
// Deactivate vision sensors when they are broken
[step] (s!=abort_mission) & camera_failed & sonar_failed -> deactivate(camera) & deactivate(sonar);
// Wait for camera to get unblocked if sonar failed and camera is blocked but did not fail
[step] sonar_failed & camera_blocked & !camera_failed -> 1: true;
// Avoid deadlock with broken sensors
[step] (s=abort_mission) -> 1: true;
endcontroller