-
Notifications
You must be signed in to change notification settings - Fork 0
/
casestudy.fprops
69 lines (56 loc) · 3.79 KB
/
casestudy.fprops
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
//////////////////////
// General Properties
/////////////////////
// The minimum and maximum probability of finishing the pipeline inspection
Pmin=? [F ${s=done}];
Pmax=? [F ${s=done}];
// The minimum and maximum probability of aborting the mission. Note that
// Pmin(F s=abort_mission) = 1 - Pmax(F s=done)
// Pmax(F s=abort_mission) = 1 - Pmin(F s=done)
Pmin=? [F ${s=abort_mission}];
Pmax=? [F ${s=abort_mission}];
//////////////////////
// Sensor failures
/////////////////////
// The minimum and maximum probability that the sonar doesn't fail until the pipeline inspection is finished
Pmin=? [${!sonar_failed} U ${s=done}];
Pmax=? [${!sonar_failed} U ${s=done}];
// The minimum and maximum probability that the camera doesn't fail until the pipeline inspection is finished
Pmin=? [${!camera_failed} U ${s=done}];
Pmax=? [${!camera_failed} U ${s=done}];
// The minimum and maximum probability that the camera doesn't get blocked until the pipeline inspection is finished
Pmin=? [${!camera_blocked} U ${s=done}];
Pmax=? [${!camera_blocked} U ${s=done}];
//////////////////////
// Correctness of the adaptation logic
/////////////////////
// The features camera and sonar are deactivated if the respective sensor failed
P>=1.0 [G (${camera_failed} => (F G ${!active(camera)}))];
P>=1.0 [G (${sonar_failed} => (F G ${!active(sonar)}))];
// The feature camera is deactivated if the camera is blocked (unless the camera got unblocked again)
P>=1.0 [G (${camera_blocked} => (F (${!active(camera)} | ${!camera_blocked})) )];
// If the camera is blocked, it will eventually be unblocked
P>=1.0 [G (${camera_blocked} => (F ${!camera_blocked}))];
// When using the camera for searching, the managing subsystem will eventually choose a correct altitude according to the wv (unless the pipeline was found, the mission was aborted or the wv changed again)
P>=1.0 [G ((${active(camera)} & ${active(search)} & ${water_visib<med_visib}) => (F (${active(low)} | ${water_visib>=med_visib})))];
P>=1.0 [G ((${active(camera)} & ${active(search)} & ${water_visib>=med_visib} & ${water_visib<high_visib}) => (F (${active(med)} | ${active(low)} | ${water_visib>=high_visib})))];
// If the wv is high, there is no check necessary as all three altitudes can be chosen (depending on the managing subsystem strategy)
// The sonar is used for searching for the pipeline if it did not fail
P>=1.0 [G ((${active(search)} & ${!sonar_failed}) => (F (${active(sonar)} | ${sonar_failed})))];
// The camera is used for following the pipeline if it did not fail and is not blocked
P>=1.0 [G ((${active(follow)} & ${!camera_unavailable}) => (F (${active(camera)} | ${camera_unavailable})))];
//////////////////////
// Reward properties
//////////////////////
R{"energy"}min=? [F ${s=done}]; // The expected minimal energy costs to finish the pipeline inspection
R{"energy"}max=? [F ${s=done}]; // The expected maximal energy costs to finish the pipeline inspection
R{"time"}min=? [F ${s=done}]; // The expected minimal time to finish the pipeline inspection
R{"time"}max=? [F ${s=done}]; // The expected maximal time to finish the pipeline inspection
//////////////////////
// Unsafe states
//////////////////////
label "thruster_failure" = s=recover_very_high | s=recover_high | s=recover_med | s=recover_low | s=recover_following;
label "safe" = s=lost_pipe | s=start_task | s=start_search | s=search_very_high| s=search_high | s=search_med | s=search_low | s=found | s=following | s=done;
label "unsafe" = s=abort_mission | s=recover_very_high | s=recover_high | s=recover_med | s=recover_low | s=recover_following;
Pmin=? [G "safe"]; // The minimum probability of reaching state "done" with passing only safe states
Pmax=? [F "unsafe"]; // The maximum probability of eventually reaching an unsafe state