-
Notifications
You must be signed in to change notification settings - Fork 67
/
Copy pathrobot.aadl
167 lines (136 loc) · 5.46 KB
/
robot.aadl
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
package robot
public
with EMV2;
with Base_Types;
with Data_Model;
system error_probabilities
features
p_d1 : out event port;
p_ed1 : out event port;
p_d2 : out event port;
p_ed2 : out event port;
p_d3 : out event port;
p_ed3 : out event port;
p_false_neg : out event port;
see_mine : out event port;
explode : out event port;
end error_probabilities;
system implementation error_probabilities.i
end error_probabilities.i;
system robot_error
features
defuse_fail : in event port;
timeout : in event port;
annex EMV2 {**
use behavior robot_behavior_emv2_behavior::normal;
component error behavior
transitions
t1 : operational -[ defuse_fail ]-> blown;
t2 : operational -[ overrun ]-> timeout;
end component;
**};
end robot_error;
system implementation robot_error.i
end robot_error.i;
system robot_behavior
features
timeout_keyword_ba : out event port;
blown : out event port;
see_mine : in event port;
explode : in event port;
p_d1 : in event port;
p_ed1 : in event port;
p_d2 : in event port;
p_ed2 : in event port;
p_d3 : in event port;
p_ed3 : in event port;
p_false_neg : in event port;
end robot_behavior;
system implementation robot_behavior.i
subcomponents
time_counter: data Base_Types::Integer {Data_Model::Initial_Value => ("0");};
timeout_val : data Base_Types::Integer {Data_Model::Initial_Value => ("100");};
current_cell: data Base_Types::Integer {Data_Model::Initial_Value => ("0");};
ncells : data Base_Types::Integer {Data_Model::Initial_Value => ("100");};
failures : data Base_Types::Integer {Data_Model::Initial_Value => ("0");};
t_sense : data Base_Types::Integer {Data_Model::Initial_Value => ("10");};
t_defuse1 : data Base_Types::Integer {Data_Model::Initial_Value => ("10");};
t_defuse2 : data Base_Types::Integer {Data_Model::Initial_Value => ("10");};
t_defuse3 : data Base_Types::Integer {Data_Model::Initial_Value => ("10");};
t_mark : data Base_Types::Integer {Data_Model::Initial_Value => ("10");};
annex behavior_specification
{**
states
init : initial final state ;
detect_mine : state;
defuse1 : state;
defuse2 : state;
defuse3 : state;
mark : state;
goto_next : state;
goto_next_cell: state;
not_detected : state;
done : final state;
transitions
-- From init
init -[current_cell < ncells]-> detect_mine {current_cell := current_cell + 1 ; time_counter := t_sense};
init -[current_cell >= ncells]-> done;
-- From detect_mine
detect_mine -[time_counter >= timeout_val]-> done;
detect_mine -[(time_counter < timeout_val) and see_mine?]-> defuse1 {time_counter := time_counter + t_defuse1};
detect_mine -[(time_counter < timeout_val) and explode?]-> done {blown!};
detect_mine -[(time_counter < timeout_val) and ( not explode'fresh) and (not see_mine'fresh)]-> not_detected;
-- From defuse1
defuse1 -[time_counter >= timeout_val]-> done {timeout_keyword_ba!};
defuse1 -[(time_counter < timeout_val) and (p_d1'fresh) and (not p_ed1'fresh)]-> goto_next;
defuse1 -[(time_counter < timeout_val) and (not p_d1'fresh) and (p_ed1'fresh)]-> done {blown!};
defuse1 -[(time_counter < timeout_val) and (not p_d1'fresh) and (not p_ed1'fresh)]-> defuse2 {time_counter := time_counter + t_defuse2};
-- From defuse2
-- TODO: defuse2 -[time_counter >= timeout_val]-> done {timeout_keyword_ba!};
defuse2 -[(time_counter < timeout_val) and (p_d2'fresh) and (not p_ed2'fresh)]-> goto_next;
defuse2 -[(time_counter < timeout_val) and (not p_d2'fresh) and (p_ed2'fresh)]-> done {blown!};
defuse2 -[(time_counter < timeout_val) and (not p_d2'fresh) and (not p_ed2'fresh)]-> defuse3 {time_counter := time_counter + t_defuse3};
--defuse2 -[time_counter < timeout_val]
-- From defuse3
defuse3 -[time_counter >= timeout_val]-> done {timeout_keyword_ba!};
defuse3 -[(time_counter < timeout_val) and (p_d3'fresh) and (not p_ed3'fresh)]-> goto_next;
defuse3 -[(time_counter < timeout_val) and (not p_d3'fresh) and (p_ed3'fresh)]-> done {blown!};
defuse3 -[(time_counter < timeout_val) and (not p_d3'fresh) and (not p_ed3'fresh)]-> mark {time_counter := time_counter + t_mark};
-- From mark
mark -[time_counter >= timeout_val]-> done {timeout_keyword_ba!};
mark -[time_counter < timeout_val]-> goto_next;
-- From not_detected
not_detected -[ p_false_neg'fresh ]-> goto_next_cell {failures := failures + 1};
not_detected -[ not p_false_neg'fresh ]-> init;
-- From goto_next
-- Later, we can add some potential faults depending on the robot behavior
goto_next -[]-> init;
**};
end robot_behavior.i;
system robot
end robot;
system implementation robot.i
subcomponents
prob : system error_probabilities.i;
error : system robot_error.i;
behavior : system robot_behavior.i;
connections
c1:port prob.p_d1 -> behavior.p_d1;
c2:port prob.p_ed1 -> behavior.p_ed1;
c3:port prob.p_d2 -> behavior.p_d2;
c4:port prob.p_ed2 -> behavior.p_ed2;
c5:port prob.p_d3 -> behavior.p_d3;
c6:port prob.p_ed3 -> behavior.p_ed3;
c7:port prob.p_false_neg -> behavior.p_false_neg;
c8:port prob.see_mine -> behavior.see_mine;
c9:port prob.explode -> behavior.explode;
cb1:port behavior.timeout_keyword_ba -> error.timeout;
cb2:port behavior.blown -> error.defuse_fail;
end robot.i;
system s
end s;
system implementation s.i
subcomponents
r1 : system robot.i;
end s.i;
end robot;