Project

General

Profile

« Previous | Next » 

Revision 97602f7c

Added by Guillaume Davy over 9 years ago

Correct bug when there is no precondition and change reprensentation
of boolean in ACSL

View differences:

tcm_benchmarks/ALT2/ALT2_proof/ALT_2.lustrec.h
24 24
                                            real Signal,
25 25
                                            real lo_lim,
26 26
                                            real out,
27
                                            integer __VariableLimitSaturation_1,
28
                                            integer __VariableLimitSaturation_2,
27
                                            boolean __VariableLimitSaturation_1,
28
                                            boolean __VariableLimitSaturation_2,
29 29
                                            real enforce_lo_lim) =
30 30
       
31
       (__VariableLimitSaturation_1 == (Signal >= lo_lim)) &&
32
       (enforce_lo_lim == (__VariableLimitSaturation_1?(Signal):(lo_lim))) &&
33
       (__VariableLimitSaturation_2 == (enforce_lo_lim <= up_lim)) &&
34
       (out == (__VariableLimitSaturation_2?(enforce_lo_lim):(up_lim)));
31
       ((__VariableLimitSaturation_1?\true:\false) == ((Signal) >= (lo_lim))) &&
32
       ((enforce_lo_lim) == ((__VariableLimitSaturation_1?\true:\false)?((Signal)):((lo_lim)))) &&
33
       ((__VariableLimitSaturation_2?\true:\false) == ((enforce_lo_lim) <= (up_lim))) &&
34
       ((out) == ((__VariableLimitSaturation_2?\true:\false)?((enforce_lo_lim)):((up_lim))));
35 35
*/
36 36
/*@ predicate Ctrans_VariableLimitSaturation(real up_lim,
37 37
                                             real Signal,
38 38
                                             real lo_lim,
39 39
                                             real out) =
40
       \exists integer __VariableLimitSaturation_1;
41
       \exists integer __VariableLimitSaturation_2;
40
       \exists boolean __VariableLimitSaturation_1;
41
       \exists boolean __VariableLimitSaturation_2;
42 42
       \exists real enforce_lo_lim;
43
       trans_VariableLimitSaturation(up_lim,
44
                                     Signal,
45
                                     lo_lim,
46
                                     out,
47
                                     __VariableLimitSaturation_1,
48
                                     __VariableLimitSaturation_2,
49
                                     enforce_lo_lim);
43
       trans_VariableLimitSaturation((up_lim),
44
                                     (Signal),
45
                                     (lo_lim),
46
                                     (out),
47
                                     (__VariableLimitSaturation_1?\true:\false),
48
                                     (__VariableLimitSaturation_2?\true:\false),
49
                                     (enforce_lo_lim));
50 50
*/
51 51
/*@ requires \valid(out);
52
  ensures Ctrans_VariableLimitSaturation(up_lim,
53
                                         Signal,
54
                                         lo_lim,
55
                                         *out);
52
  ensures Ctrans_VariableLimitSaturation((up_lim),
53
                                         (Signal),
54
                                         (lo_lim),
55
                                         (*out));
56 56
  assigns *out;
57 57
  */
58 58
extern void VariableLimitSaturation_step (double up_lim, double Signal,
......
61 61
                                          );
62 62

  
63 63
/*@ predicate trans_integrator_reset(real Fx,
64
                                     integer ResetLevel,
64
                                     boolean ResetLevel,
65 65
                                     real x0,
66 66
                                     real ir_out,
67 67
                                     struct integrator_reset_mem self1,
68 68
                                     struct integrator_reset_mem self2,
69
                                     integer __integrator_reset_1) =
69
                                     boolean __integrator_reset_1) =
70 70
       
71
       (__integrator_reset_1==(self1.ni_3._reg._first?(1):(0))) && (self2.ni_3._reg._first==0) &&
72
       (ir_out == (__integrator_reset_1?(x0):((ResetLevel?(x0):(((Fx * 1.) + self1._reg.__integrator_reset_2)))))) &&
73
       (self2._reg.__integrator_reset_2 == ir_out);
71
       ((__integrator_reset_1?\true:\false)==(self1.ni_3._reg._first?(1):(0))) && (self2.ni_3._reg._first==0) &&
72
       ((ir_out) == ((__integrator_reset_1?\true:\false)?((x0)):(((ResetLevel?\true:\false)?((x0)):((((Fx) * 1.) + self1._reg.__integrator_reset_2)))))) &&
73
       (self2._reg.__integrator_reset_2 == (ir_out));
74 74
*/
75 75
/*@ predicate Ctrans_integrator_reset(real Fx,
76
                                      integer ResetLevel,
76
                                      boolean ResetLevel,
77 77
                                      real x0,
78 78
                                      real ir_out,
79 79
                                      struct integrator_reset_mem self1,
80 80
                                      struct integrator_reset_mem self2) =
81
       \exists integer __integrator_reset_1;
82
       trans_integrator_reset(Fx,
83
                              ResetLevel,
84
                              x0,
85
                              ir_out,
81
       \exists boolean __integrator_reset_1;
82
       trans_integrator_reset((Fx),
83
                              (ResetLevel?\true:\false),
84
                              (x0),
85
                              (ir_out),
86 86
                              self1,
87 87
                              self2,
88
                              __integrator_reset_1);
88
                              (__integrator_reset_1?\true:\false));
89 89
*/
90 90
/*@ predicate init_integrator_reset(struct integrator_reset_mem self) =
91 91
       
......
108 108
/*@ requires \valid(ir_out);
109 109
  requires \valid(self);
110 110
  requires \separated(ir_out, self);
111
  ensures Ctrans_integrator_reset(Fx,
112
                                  ResetLevel,
113
                                  x0,
114
                                  *ir_out,
111
  ensures Ctrans_integrator_reset((Fx),
112
                                  (ResetLevel?\true:\false),
113
                                  (x0),
114
                                  (*ir_out),
115 115
                                  \at(*self, Pre),
116 116
                                  (*self));
117 117
  assigns *ir_out, *self;
......
122 122

  
123 123
/*@ predicate trans_Saturation(real Signal,
124 124
                               real s_out,
125
                               integer __Saturation_1,
126
                               integer __Saturation_2,
125
                               boolean __Saturation_1,
126
                               boolean __Saturation_2,
127 127
                               real enforce_lo_lim) =
128 128
       
129
       (__Saturation_1 == (0.0001 >= Signal)) &&
130
       (enforce_lo_lim == (__Saturation_1?(0.0001):(Signal))) &&
131
       (__Saturation_2 == (1000. <= enforce_lo_lim)) &&
132
       (s_out == (__Saturation_2?(1000.):(enforce_lo_lim)));
129
       ((__Saturation_1?\true:\false) == (0.0001 >= (Signal))) &&
130
       ((enforce_lo_lim) == ((__Saturation_1?\true:\false)?(0.0001):((Signal)))) &&
131
       ((__Saturation_2?\true:\false) == (1000. <= (enforce_lo_lim))) &&
132
       ((s_out) == ((__Saturation_2?\true:\false)?(1000.):((enforce_lo_lim))));
133 133
*/
134 134
/*@ predicate Ctrans_Saturation(real Signal,
135 135
                                real s_out) =
136
       \exists integer __Saturation_1;
137
       \exists integer __Saturation_2;
136
       \exists boolean __Saturation_1;
137
       \exists boolean __Saturation_2;
138 138
       \exists real enforce_lo_lim;
139
       trans_Saturation(Signal,
140
                        s_out,
141
                        __Saturation_1,
142
                        __Saturation_2,
143
                        enforce_lo_lim);
139
       trans_Saturation((Signal),
140
                        (s_out),
141
                        (__Saturation_1?\true:\false),
142
                        (__Saturation_2?\true:\false),
143
                        (enforce_lo_lim));
144 144
*/
145 145
/*@ requires \valid(s_out);
146
  ensures Ctrans_Saturation(Signal,
147
                            *s_out);
146
  ensures Ctrans_Saturation((Signal),
147
                            (*s_out));
148 148
  assigns *s_out;
149 149
  */
150 150
extern void Saturation_step (double Signal, 
......
153 153

  
154 154
/*@ predicate trans_VariableRateLimit(real ratelim_Out1_334,
155 155
                                      real input_Out1_344,
156
                                      integer ICtrig_Out1_354,
156
                                      boolean ICtrig_Out1_354,
157 157
                                      real IC_Out1_364,
158 158
                                      real output_In1_489,
159 159
                                      struct VariableRateLimit_mem self1,
......
163 163
                                      real Integrator1_Out1_391,
164 164
                                      real Sum2_Out1_401,
165 165
                                      real Variable_Limit_Saturation_Out1_410,
166
                                      integer __VariableRateLimit_1,
166
                                      boolean __VariableRateLimit_1,
167 167
                                      real __VariableRateLimit_2) =
168 168
       
169
       (__VariableRateLimit_1==(self1.ni_2._reg._first?(1):(0))) && (self2.ni_2._reg._first==0) &&
170
       (Integrator1_Out1_391 == (__VariableRateLimit_1?(IC_Out1_364):(self1._reg.__VariableRateLimit_3))) &&
171
       (output_In1_489 == Integrator1_Out1_391) &&
172
       (Gain1_Out1_382 == (- ratelim_Out1_334)) &&
173
       (Sum2_Out1_401 == (input_Out1_344 + (- Integrator1_Out1_391))) &&
174
       (Gain_Out1_373 == (20. * Sum2_Out1_401)) &&
175
       Ctrans_VariableLimitSaturation((double) ratelim_Out1_334,
176
                                      (double) Gain_Out1_373,
177
                                      (double) Gain1_Out1_382,
178
                                      Variable_Limit_Saturation_Out1_410) &&
179
       Ctrans_integrator_reset((double) Variable_Limit_Saturation_Out1_410,
180
                               (_Bool) ICtrig_Out1_354,
181
                               (double) IC_Out1_364,
182
                               __VariableRateLimit_2,
169
       ((__VariableRateLimit_1?\true:\false)==(self1.ni_2._reg._first?(1):(0))) && (self2.ni_2._reg._first==0) &&
170
       ((Integrator1_Out1_391) == ((__VariableRateLimit_1?\true:\false)?((IC_Out1_364)):(self1._reg.__VariableRateLimit_3))) &&
171
       ((output_In1_489) == (Integrator1_Out1_391)) &&
172
       ((Gain1_Out1_382) == (- (ratelim_Out1_334))) &&
173
       ((Sum2_Out1_401) == ((input_Out1_344) + (- (Integrator1_Out1_391)))) &&
174
       ((Gain_Out1_373) == (20. * (Sum2_Out1_401))) &&
175
       Ctrans_VariableLimitSaturation((ratelim_Out1_334),
176
                                      (Gain_Out1_373),
177
                                      (Gain1_Out1_382),
178
                                      (Variable_Limit_Saturation_Out1_410)) &&
179
       Ctrans_integrator_reset((Variable_Limit_Saturation_Out1_410),
180
                               (ICtrig_Out1_354?\true:\false),
181
                               (IC_Out1_364),
182
                               (__VariableRateLimit_2),
183 183
                               self1.ni_1,
184 184
                               self2.ni_1) &&
185
       (self2._reg.__VariableRateLimit_3 == __VariableRateLimit_2);
185
       (self2._reg.__VariableRateLimit_3 == (__VariableRateLimit_2));
186 186
*/
187 187
/*@ predicate Ctrans_VariableRateLimit(real ratelim_Out1_334,
188 188
                                       real input_Out1_344,
189
                                       integer ICtrig_Out1_354,
189
                                       boolean ICtrig_Out1_354,
190 190
                                       real IC_Out1_364,
191 191
                                       real output_In1_489,
192 192
                                       struct VariableRateLimit_mem self1,
......
196 196
       \exists real Integrator1_Out1_391;
197 197
       \exists real Sum2_Out1_401;
198 198
       \exists real Variable_Limit_Saturation_Out1_410;
199
       \exists integer __VariableRateLimit_1;
199
       \exists boolean __VariableRateLimit_1;
200 200
       \exists real __VariableRateLimit_2;
201
       trans_VariableRateLimit(ratelim_Out1_334,
202
                               input_Out1_344,
203
                               ICtrig_Out1_354,
204
                               IC_Out1_364,
205
                               output_In1_489,
201
       trans_VariableRateLimit((ratelim_Out1_334),
202
                               (input_Out1_344),
203
                               (ICtrig_Out1_354?\true:\false),
204
                               (IC_Out1_364),
205
                               (output_In1_489),
206 206
                               self1,
207 207
                               self2,
208
                               Gain1_Out1_382,
209
                               Gain_Out1_373,
210
                               Integrator1_Out1_391,
211
                               Sum2_Out1_401,
212
                               Variable_Limit_Saturation_Out1_410,
213
                               __VariableRateLimit_1,
214
                               __VariableRateLimit_2);
208
                               (Gain1_Out1_382),
209
                               (Gain_Out1_373),
210
                               (Integrator1_Out1_391),
211
                               (Sum2_Out1_401),
212
                               (Variable_Limit_Saturation_Out1_410),
213
                               (__VariableRateLimit_1?\true:\false),
214
                               (__VariableRateLimit_2));
215 215
*/
216 216
/*@ predicate init_VariableRateLimit(struct VariableRateLimit_mem self) =
217 217
       
......
236 236
/*@ requires \valid(output_In1_489);
237 237
  requires \valid(self);
238 238
  requires \separated(output_In1_489, self);
239
  ensures Ctrans_VariableRateLimit(ratelim_Out1_334,
240
                                   input_Out1_344,
241
                                   ICtrig_Out1_354,
242
                                   IC_Out1_364,
243
                                   *output_In1_489,
239
  ensures Ctrans_VariableRateLimit((ratelim_Out1_334),
240
                                   (input_Out1_344),
241
                                   (ICtrig_Out1_354?\true:\false),
242
                                   (IC_Out1_364),
243
                                   (*output_In1_489),
244 244
                                   \at(*self, Pre),
245 245
                                   (*self));
246 246
  assigns *output_In1_489, *self;
......
269 269
                                    struct AltitudeControl_mem self2,
270 270
                                    real Abs_Out1_144,
271 271
                                    real Kh_Out1_193,
272
                                    integer Logical_Operator_In1_197,
273
                                    integer Logical_Operator_Out1_198,
272
                                    boolean Logical_Operator_In1_197,
273
                                    boolean Logical_Operator_Out1_198,
274 274
                                    real Saturation1_Out1_213,
275 275
                                    real Sum3_Out1_296,
276 276
                                    real Sum_Out1_286,
277
                                    integer Switch1_In2_312,
277
                                    boolean Switch1_In2_312,
278 278
                                    real Switch1_Out1_314,
279
                                    integer Switch_In2_303,
279
                                    boolean Switch_In2_303,
280 280
                                    real Switch_Out1_305,
281 281
                                    real Variable_Limit_Saturation_0_Out1_509,
282 282
                                    real Variable__Rate_Limit_Out1_324,
283
                                    integer __AltitudeControl_1,
284
                                    integer __AltitudeControl_2,
283
                                    boolean __AltitudeControl_1,
284
                                    boolean __AltitudeControl_2,
285 285
                                    real k_Out1_585,
286 286
                                    real kts2fps_Out1_594,
287 287
                                    real r2d_Out1_603) =
288 288
       
289
       (__AltitudeControl_1 == (hdot_Out1_59 < 0.)) &&
290
       (Abs_Out1_144 == (__AltitudeControl_1?((- hdot_Out1_59)):(hdot_Out1_59))) &&
291
       (Sum3_Out1_296 == (Abs_Out1_144 + 10.)) &&
292
       (k_Out1_585 == (- Sum3_Out1_296)) &&
293
       (__AltitudeControl_2 == (AntEng_Out1_19 == 0.)) &&
294
       ((!Logical_Operator_In1_197) == (!(__AltitudeControl_2?(0):(1)))) &&
295
       ((!Logical_Operator_Out1_198) == (!(!Logical_Operator_In1_197))) &&
296
       ((!Switch_In2_303) == (!(__AltitudeControl_2?(0):(1)))) &&
297
       (Sum_Out1_286 == (AltCmd_Out1_29 + (- Alt_Out1_39))) &&
298
       (Kh_Out1_193 == (0.08 * Sum_Out1_286)) &&
299
       (Switch_Out1_305 == (Switch_In2_303?(Kh_Out1_193):(0.))) &&
300
       Ctrans_VariableLimitSaturation((double) Sum3_Out1_296,
301
                                      (double) Switch_Out1_305,
302
                                      (double) k_Out1_585,
303
                                      Variable_Limit_Saturation_0_Out1_509) &&
304
       Ctrans_VariableRateLimit((double) hdotChgRate_Out1_69,
305
                                (double) Variable_Limit_Saturation_0_Out1_509,
306
                                (_Bool) Logical_Operator_Out1_198,
307
                                (double) hdot_Out1_59,
308
                                Variable__Rate_Limit_Out1_324,
289
       ((__AltitudeControl_1?\true:\false) == ((hdot_Out1_59) < 0.)) &&
290
       ((Abs_Out1_144) == ((__AltitudeControl_1?\true:\false)?((- (hdot_Out1_59))):((hdot_Out1_59)))) &&
291
       ((Sum3_Out1_296) == ((Abs_Out1_144) + 10.)) &&
292
       ((k_Out1_585) == (- (Sum3_Out1_296))) &&
293
       ((__AltitudeControl_2?\true:\false) == ((AntEng_Out1_19) == 0.)) &&
294
       ((!(Logical_Operator_In1_197?\true:\false)) == (!((__AltitudeControl_2?\true:\false)?(0):(1)))) &&
295
       ((!(Logical_Operator_Out1_198?\true:\false)) == (!(!(Logical_Operator_In1_197?\true:\false)))) &&
296
       ((!(Switch_In2_303?\true:\false)) == (!((__AltitudeControl_2?\true:\false)?(0):(1)))) &&
297
       ((Sum_Out1_286) == ((AltCmd_Out1_29) + (- (Alt_Out1_39)))) &&
298
       ((Kh_Out1_193) == (0.08 * (Sum_Out1_286))) &&
299
       ((Switch_Out1_305) == ((Switch_In2_303?\true:\false)?((Kh_Out1_193)):(0.))) &&
300
       Ctrans_VariableLimitSaturation((Sum3_Out1_296),
301
                                      (Switch_Out1_305),
302
                                      (k_Out1_585),
303
                                      (Variable_Limit_Saturation_0_Out1_509)) &&
304
       Ctrans_VariableRateLimit((hdotChgRate_Out1_69),
305
                                (Variable_Limit_Saturation_0_Out1_509),
306
                                (Logical_Operator_Out1_198?\true:\false),
307
                                (hdot_Out1_59),
308
                                (Variable__Rate_Limit_Out1_324),
309 309
                                self1.ni_0,
310 310
                                self2.ni_0) &&
311
       (r2d_Out1_603 == (57.2958 * Variable__Rate_Limit_Out1_324)) &&
312
       (kts2fps_Out1_594 == (1.6878 * GsKts_Out1_49)) &&
313
       ((!Switch1_In2_312) == (!(__AltitudeControl_2?(0):(1)))) &&
314
       (Switch1_Out1_314 == (Switch1_In2_312?(r2d_Out1_603):(0.))) &&
315
       (altgammacmd_In1_661 == Switch1_Out1_314) &&
316
       Ctrans_Saturation((double) kts2fps_Out1_594,
317
                         Saturation1_Out1_213);
311
       ((r2d_Out1_603) == (57.2958 * (Variable__Rate_Limit_Out1_324))) &&
312
       ((kts2fps_Out1_594) == (1.6878 * (GsKts_Out1_49))) &&
313
       ((!(Switch1_In2_312?\true:\false)) == (!((__AltitudeControl_2?\true:\false)?(0):(1)))) &&
314
       ((Switch1_Out1_314) == ((Switch1_In2_312?\true:\false)?((r2d_Out1_603)):(0.))) &&
315
       ((altgammacmd_In1_661) == (Switch1_Out1_314)) &&
316
       Ctrans_Saturation((kts2fps_Out1_594),
317
                         (Saturation1_Out1_213));
318 318
*/
319 319
/*@ predicate Ctrans_AltitudeControl(real AntEng_Out1_19,
320 320
                                     real AltCmd_Out1_29,
......
327 327
                                     struct AltitudeControl_mem self2) =
328 328
       \exists real Abs_Out1_144;
329 329
       \exists real Kh_Out1_193;
330
       \exists integer Logical_Operator_In1_197;
331
       \exists integer Logical_Operator_Out1_198;
330
       \exists boolean Logical_Operator_In1_197;
331
       \exists boolean Logical_Operator_Out1_198;
332 332
       \exists real Saturation1_Out1_213;
333 333
       \exists real Sum3_Out1_296;
334 334
       \exists real Sum_Out1_286;
335
       \exists integer Switch1_In2_312;
335
       \exists boolean Switch1_In2_312;
336 336
       \exists real Switch1_Out1_314;
337
       \exists integer Switch_In2_303;
337
       \exists boolean Switch_In2_303;
338 338
       \exists real Switch_Out1_305;
339 339
       \exists real Variable_Limit_Saturation_0_Out1_509;
340 340
       \exists real Variable__Rate_Limit_Out1_324;
341
       \exists integer __AltitudeControl_1;
342
       \exists integer __AltitudeControl_2;
341
       \exists boolean __AltitudeControl_1;
342
       \exists boolean __AltitudeControl_2;
343 343
       \exists real k_Out1_585;
344 344
       \exists real kts2fps_Out1_594;
345 345
       \exists real r2d_Out1_603;
346
       trans_AltitudeControl(AntEng_Out1_19,
347
                             AltCmd_Out1_29,
348
                             Alt_Out1_39,
349
                             GsKts_Out1_49,
350
                             hdot_Out1_59,
351
                             hdotChgRate_Out1_69,
352
                             altgammacmd_In1_661,
346
       trans_AltitudeControl((AntEng_Out1_19),
347
                             (AltCmd_Out1_29),
348
                             (Alt_Out1_39),
349
                             (GsKts_Out1_49),
350
                             (hdot_Out1_59),
351
                             (hdotChgRate_Out1_69),
352
                             (altgammacmd_In1_661),
353 353
                             self1,
354 354
                             self2,
355
                             Abs_Out1_144,
356
                             Kh_Out1_193,
357
                             Logical_Operator_In1_197,
358
                             Logical_Operator_Out1_198,
359
                             Saturation1_Out1_213,
360
                             Sum3_Out1_296,
361
                             Sum_Out1_286,
362
                             Switch1_In2_312,
363
                             Switch1_Out1_314,
364
                             Switch_In2_303,
365
                             Switch_Out1_305,
366
                             Variable_Limit_Saturation_0_Out1_509,
367
                             Variable__Rate_Limit_Out1_324,
368
                             __AltitudeControl_1,
369
                             __AltitudeControl_2,
370
                             k_Out1_585,
371
                             kts2fps_Out1_594,
372
                             r2d_Out1_603);
355
                             (Abs_Out1_144),
356
                             (Kh_Out1_193),
357
                             (Logical_Operator_In1_197?\true:\false),
358
                             (Logical_Operator_Out1_198?\true:\false),
359
                             (Saturation1_Out1_213),
360
                             (Sum3_Out1_296),
361
                             (Sum_Out1_286),
362
                             (Switch1_In2_312?\true:\false),
363
                             (Switch1_Out1_314),
364
                             (Switch_In2_303?\true:\false),
365
                             (Switch_Out1_305),
366
                             (Variable_Limit_Saturation_0_Out1_509),
367
                             (Variable__Rate_Limit_Out1_324),
368
                             (__AltitudeControl_1?\true:\false),
369
                             (__AltitudeControl_2?\true:\false),
370
                             (k_Out1_585),
371
                             (kts2fps_Out1_594),
372
                             (r2d_Out1_603));
373 373
*/
374 374
/*@ predicate init_AltitudeControl(struct AltitudeControl_mem self) =
375 375
       
......
378 378
/*@ predicate inv_AltitudeControl(struct AltitudeControl_mem self3) =
379 379
       (init_AltitudeControl(self3))||
380 380
       (\exists struct AltitudeControl_mem self2, real AntEng_Out1_193, real AltCmd_Out1_293, real Alt_Out1_393, real GsKts_Out1_493, real hdot_Out1_593, real hdotChgRate_Out1_693, real altgammacmd_In1_6613;
381
       Ctrans_AltitudeControl(AntEng_Out1_193,
382
                              AltCmd_Out1_293,
383
                              Alt_Out1_393,
384
                              GsKts_Out1_493,
385
                              hdot_Out1_593,
386
                              hdotChgRate_Out1_693,
387
                              altgammacmd_In1_6613,
381
       Ctrans_AltitudeControl((AntEng_Out1_193),
382
                              (AltCmd_Out1_293),
383
                              (Alt_Out1_393),
384
                              (GsKts_Out1_493),
385
                              (hdot_Out1_593),
386
                              (hdotChgRate_Out1_693),
387
                              (altgammacmd_In1_6613),
388 388
                              self2,
389 389
                              self3)&&
390
       (spec_85(AntEng_Out1_193, AltCmd_Out1_293, Alt_Out1_393, GsKts_Out1_493, hdot_Out1_593, hdotChgRate_Out1_693, altgammacmd_In1_6613, self2))&&
390
       (spec_85((AntEng_Out1_193), (AltCmd_Out1_293), (Alt_Out1_393), (GsKts_Out1_493), (hdot_Out1_593), (hdotChgRate_Out1_693), (altgammacmd_In1_6613), self2))&&
391 391
       init_AltitudeControl(self2))||
392 392
       (\exists struct AltitudeControl_mem self2, struct AltitudeControl_mem self1, real AntEng_Out1_193, real AntEng_Out1_192, real AltCmd_Out1_293, real AltCmd_Out1_292, real Alt_Out1_393, real Alt_Out1_392, real GsKts_Out1_493, real GsKts_Out1_492, real hdot_Out1_593, real hdot_Out1_592, real hdotChgRate_Out1_693, real hdotChgRate_Out1_692, real altgammacmd_In1_6613, real altgammacmd_In1_6612;
393
       Ctrans_AltitudeControl(AntEng_Out1_193,
394
                              AltCmd_Out1_293,
395
                              Alt_Out1_393,
396
                              GsKts_Out1_493,
397
                              hdot_Out1_593,
398
                              hdotChgRate_Out1_693,
399
                              altgammacmd_In1_6613,
393
       Ctrans_AltitudeControl((AntEng_Out1_193),
394
                              (AltCmd_Out1_293),
395
                              (Alt_Out1_393),
396
                              (GsKts_Out1_493),
397
                              (hdot_Out1_593),
398
                              (hdotChgRate_Out1_693),
399
                              (altgammacmd_In1_6613),
400 400
                              self2,
401 401
                              self3)&&
402
       Ctrans_AltitudeControl(AntEng_Out1_192,
403
                              AltCmd_Out1_292,
404
                              Alt_Out1_392,
405
                              GsKts_Out1_492,
406
                              hdot_Out1_592,
407
                              hdotChgRate_Out1_692,
408
                              altgammacmd_In1_6612,
402
       Ctrans_AltitudeControl((AntEng_Out1_192),
403
                              (AltCmd_Out1_292),
404
                              (Alt_Out1_392),
405
                              (GsKts_Out1_492),
406
                              (hdot_Out1_592),
407
                              (hdotChgRate_Out1_692),
408
                              (altgammacmd_In1_6612),
409 409
                              self1,
410 410
                              self2)&&
411
       (spec_85(AntEng_Out1_193, AltCmd_Out1_293, Alt_Out1_393, GsKts_Out1_493, hdot_Out1_593, hdotChgRate_Out1_693, altgammacmd_In1_6613, self2))&&
412
       (spec_85(AntEng_Out1_192, AltCmd_Out1_292, Alt_Out1_392, GsKts_Out1_492, hdot_Out1_592, hdotChgRate_Out1_692, altgammacmd_In1_6612, self1))&&
411
       (spec_85((AntEng_Out1_193), (AltCmd_Out1_293), (Alt_Out1_393), (GsKts_Out1_493), (hdot_Out1_593), (hdotChgRate_Out1_693), (altgammacmd_In1_6613), self2))&&
412
       (spec_85((AntEng_Out1_192), (AltCmd_Out1_292), (Alt_Out1_392), (GsKts_Out1_492), (hdot_Out1_592), (hdotChgRate_Out1_692), (altgammacmd_In1_6612), self1))&&
413 413
       init_AltitudeControl(self1))||
414 414
       (\exists struct AltitudeControl_mem self2, struct AltitudeControl_mem self1, struct AltitudeControl_mem self0, real AntEng_Out1_193, real AntEng_Out1_192, real AntEng_Out1_191, real AltCmd_Out1_293, real AltCmd_Out1_292, real AltCmd_Out1_291, real Alt_Out1_393, real Alt_Out1_392, real Alt_Out1_391, real GsKts_Out1_493, real GsKts_Out1_492, real GsKts_Out1_491, real hdot_Out1_593, real hdot_Out1_592, real hdot_Out1_591, real hdotChgRate_Out1_693, real hdotChgRate_Out1_692, real hdotChgRate_Out1_691, real altgammacmd_In1_6613, real altgammacmd_In1_6612, real altgammacmd_In1_6611;
415
       Ctrans_AltitudeControl(AntEng_Out1_193,
416
                              AltCmd_Out1_293,
417
                              Alt_Out1_393,
418
                              GsKts_Out1_493,
419
                              hdot_Out1_593,
420
                              hdotChgRate_Out1_693,
421
                              altgammacmd_In1_6613,
415
       Ctrans_AltitudeControl((AntEng_Out1_193),
416
                              (AltCmd_Out1_293),
417
                              (Alt_Out1_393),
418
                              (GsKts_Out1_493),
419
                              (hdot_Out1_593),
420
                              (hdotChgRate_Out1_693),
421
                              (altgammacmd_In1_6613),
422 422
                              self2,
423 423
                              self3)&&
424
       Ctrans_AltitudeControl(AntEng_Out1_192,
425
                              AltCmd_Out1_292,
426
                              Alt_Out1_392,
427
                              GsKts_Out1_492,
428
                              hdot_Out1_592,
429
                              hdotChgRate_Out1_692,
430
                              altgammacmd_In1_6612,
424
       Ctrans_AltitudeControl((AntEng_Out1_192),
425
                              (AltCmd_Out1_292),
426
                              (Alt_Out1_392),
427
                              (GsKts_Out1_492),
428
                              (hdot_Out1_592),
429
                              (hdotChgRate_Out1_692),
430
                              (altgammacmd_In1_6612),
431 431
                              self1,
432 432
                              self2)&&
433
       Ctrans_AltitudeControl(AntEng_Out1_191,
434
                              AltCmd_Out1_291,
435
                              Alt_Out1_391,
436
                              GsKts_Out1_491,
437
                              hdot_Out1_591,
438
                              hdotChgRate_Out1_691,
439
                              altgammacmd_In1_6611,
433
       Ctrans_AltitudeControl((AntEng_Out1_191),
434
                              (AltCmd_Out1_291),
435
                              (Alt_Out1_391),
436
                              (GsKts_Out1_491),
437
                              (hdot_Out1_591),
438
                              (hdotChgRate_Out1_691),
439
                              (altgammacmd_In1_6611),
440 440
                              self0,
441 441
                              self1)&&
442
       (spec_85(AntEng_Out1_193, AltCmd_Out1_293, Alt_Out1_393, GsKts_Out1_493, hdot_Out1_593, hdotChgRate_Out1_693, altgammacmd_In1_6613, self2))&&
443
       (spec_85(AntEng_Out1_192, AltCmd_Out1_292, Alt_Out1_392, GsKts_Out1_492, hdot_Out1_592, hdotChgRate_Out1_692, altgammacmd_In1_6612, self1))&&
444
       (spec_85(AntEng_Out1_191, AltCmd_Out1_291, Alt_Out1_391, GsKts_Out1_491, hdot_Out1_591, hdotChgRate_Out1_691, altgammacmd_In1_6611, self0))&&
445
       (spec_90(AntEng_Out1_193, AltCmd_Out1_293, Alt_Out1_393, GsKts_Out1_493, hdot_Out1_593, hdotChgRate_Out1_693, altgammacmd_In1_6613, self3))&&
446
       (spec_90(AntEng_Out1_192, AltCmd_Out1_292, Alt_Out1_392, GsKts_Out1_492, hdot_Out1_592, hdotChgRate_Out1_692, altgammacmd_In1_6612, self2))&&
447
       (spec_90(AntEng_Out1_191, AltCmd_Out1_291, Alt_Out1_391, GsKts_Out1_491, hdot_Out1_591, hdotChgRate_Out1_691, altgammacmd_In1_6611, self1)));
442
       (spec_85((AntEng_Out1_193), (AltCmd_Out1_293), (Alt_Out1_393), (GsKts_Out1_493), (hdot_Out1_593), (hdotChgRate_Out1_693), (altgammacmd_In1_6613), self2))&&
443
       (spec_85((AntEng_Out1_192), (AltCmd_Out1_292), (Alt_Out1_392), (GsKts_Out1_492), (hdot_Out1_592), (hdotChgRate_Out1_692), (altgammacmd_In1_6612), self1))&&
444
       (spec_85((AntEng_Out1_191), (AltCmd_Out1_291), (Alt_Out1_391), (GsKts_Out1_491), (hdot_Out1_591), (hdotChgRate_Out1_691), (altgammacmd_In1_6611), self0))&&
445
       (spec_90((AntEng_Out1_193), (AltCmd_Out1_293), (Alt_Out1_393), (GsKts_Out1_493), (hdot_Out1_593), (hdotChgRate_Out1_693), (altgammacmd_In1_6613), self3))&&
446
       (spec_90((AntEng_Out1_192), (AltCmd_Out1_292), (Alt_Out1_392), (GsKts_Out1_492), (hdot_Out1_592), (hdotChgRate_Out1_692), (altgammacmd_In1_6612), self2))&&
447
       (spec_90((AntEng_Out1_191), (AltCmd_Out1_291), (Alt_Out1_391), (GsKts_Out1_491), (hdot_Out1_591), (hdotChgRate_Out1_691), (altgammacmd_In1_6611), self1)));
448 448
*/
449 449
/*@ lemma inv_init_3_AltitudeControl : 
450 450
       \forall struct AltitudeControl_mem self3, struct AltitudeControl_mem self2, struct AltitudeControl_mem self1, struct AltitudeControl_mem self0, real AntEng_Out1_193, real AntEng_Out1_192, real AntEng_Out1_191, real AltCmd_Out1_293, real AltCmd_Out1_292, real AltCmd_Out1_291, real Alt_Out1_393, real Alt_Out1_392, real Alt_Out1_391, real GsKts_Out1_493, real GsKts_Out1_492, real GsKts_Out1_491, real hdot_Out1_593, real hdot_Out1_592, real hdot_Out1_591, real hdotChgRate_Out1_693, real hdotChgRate_Out1_692, real hdotChgRate_Out1_691, real altgammacmd_In1_6613, real altgammacmd_In1_6612, real altgammacmd_In1_6611;
451
       Ctrans_AltitudeControl(AntEng_Out1_193,
452
                              AltCmd_Out1_293,
453
                              Alt_Out1_393,
454
                              GsKts_Out1_493,
455
                              hdot_Out1_593,
456
                              hdotChgRate_Out1_693,
457
                              altgammacmd_In1_6613,
451
       Ctrans_AltitudeControl((AntEng_Out1_193),
452
                              (AltCmd_Out1_293),
453
                              (Alt_Out1_393),
454
                              (GsKts_Out1_493),
455
                              (hdot_Out1_593),
456
                              (hdotChgRate_Out1_693),
457
                              (altgammacmd_In1_6613),
458 458
                              self2,
459 459
                              self3)==>
460
       Ctrans_AltitudeControl(AntEng_Out1_192,
461
                              AltCmd_Out1_292,
462
                              Alt_Out1_392,
463
                              GsKts_Out1_492,
464
                              hdot_Out1_592,
465
                              hdotChgRate_Out1_692,
466
                              altgammacmd_In1_6612,
460
       Ctrans_AltitudeControl((AntEng_Out1_192),
461
                              (AltCmd_Out1_292),
462
                              (Alt_Out1_392),
463
                              (GsKts_Out1_492),
464
                              (hdot_Out1_592),
465
                              (hdotChgRate_Out1_692),
466
                              (altgammacmd_In1_6612),
467 467
                              self1,
468 468
                              self2)==>
469
       Ctrans_AltitudeControl(AntEng_Out1_191,
470
                              AltCmd_Out1_291,
471
                              Alt_Out1_391,
472
                              GsKts_Out1_491,
473
                              hdot_Out1_591,
474
                              hdotChgRate_Out1_691,
475
                              altgammacmd_In1_6611,
469
       Ctrans_AltitudeControl((AntEng_Out1_191),
470
                              (AltCmd_Out1_291),
471
                              (Alt_Out1_391),
472
                              (GsKts_Out1_491),
473
                              (hdot_Out1_591),
474
                              (hdotChgRate_Out1_691),
475
                              (altgammacmd_In1_6611),
476 476
                              self0,
477 477
                              self1)==>
478
       init_AltitudeControl(self0) ==> spec_85(AntEng_Out1_193, AltCmd_Out1_293, Alt_Out1_393, GsKts_Out1_493, hdot_Out1_593, hdotChgRate_Out1_693, altgammacmd_In1_6613, self2)==>
479
       spec_85(AntEng_Out1_193, AltCmd_Out1_293, Alt_Out1_393, GsKts_Out1_493, hdot_Out1_593, hdotChgRate_Out1_693, altgammacmd_In1_6613, self1)==>
480
       spec_85(AntEng_Out1_193, AltCmd_Out1_293, Alt_Out1_393, GsKts_Out1_493, hdot_Out1_593, hdotChgRate_Out1_693, altgammacmd_In1_6613, self0)==>
481
       (spec_90(AntEng_Out1_193, AltCmd_Out1_293, Alt_Out1_393, GsKts_Out1_493, hdot_Out1_593, hdotChgRate_Out1_693, altgammacmd_In1_6613, self3));
478
       init_AltitudeControl(self0) ==> spec_85((AntEng_Out1_193), (AltCmd_Out1_293), (Alt_Out1_393), (GsKts_Out1_493), (hdot_Out1_593), (hdotChgRate_Out1_693), (altgammacmd_In1_6613), self2)==>
479
       spec_85((AntEng_Out1_193), (AltCmd_Out1_293), (Alt_Out1_393), (GsKts_Out1_493), (hdot_Out1_593), (hdotChgRate_Out1_693), (altgammacmd_In1_6613), self1)==>
480
       spec_85((AntEng_Out1_193), (AltCmd_Out1_293), (Alt_Out1_393), (GsKts_Out1_493), (hdot_Out1_593), (hdotChgRate_Out1_693), (altgammacmd_In1_6613), self0)==>
481
       (spec_90((AntEng_Out1_193), (AltCmd_Out1_293), (Alt_Out1_393), (GsKts_Out1_493), (hdot_Out1_593), (hdotChgRate_Out1_693), (altgammacmd_In1_6613), self3));
482 482
*/
483 483
/*@ lemma inv_init_2_AltitudeControl : 
484 484
       \forall struct AltitudeControl_mem self3, struct AltitudeControl_mem self2, struct AltitudeControl_mem self1, real AntEng_Out1_193, real AntEng_Out1_192, real AltCmd_Out1_293, real AltCmd_Out1_292, real Alt_Out1_393, real Alt_Out1_392, real GsKts_Out1_493, real GsKts_Out1_492, real hdot_Out1_593, real hdot_Out1_592, real hdotChgRate_Out1_693, real hdotChgRate_Out1_692, real altgammacmd_In1_6613, real altgammacmd_In1_6612;
485
       Ctrans_AltitudeControl(AntEng_Out1_193,
486
                              AltCmd_Out1_293,
487
                              Alt_Out1_393,
488
                              GsKts_Out1_493,
489
                              hdot_Out1_593,
490
                              hdotChgRate_Out1_693,
491
                              altgammacmd_In1_6613,
485
       Ctrans_AltitudeControl((AntEng_Out1_193),
486
                              (AltCmd_Out1_293),
487
                              (Alt_Out1_393),
488
                              (GsKts_Out1_493),
489
                              (hdot_Out1_593),
490
                              (hdotChgRate_Out1_693),
491
                              (altgammacmd_In1_6613),
492 492
                              self2,
493 493
                              self3)==>
494
       Ctrans_AltitudeControl(AntEng_Out1_192,
495
                              AltCmd_Out1_292,
496
                              Alt_Out1_392,
497
                              GsKts_Out1_492,
498
                              hdot_Out1_592,
499
                              hdotChgRate_Out1_692,
500
                              altgammacmd_In1_6612,
494
       Ctrans_AltitudeControl((AntEng_Out1_192),
495
                              (AltCmd_Out1_292),
496
                              (Alt_Out1_392),
497
                              (GsKts_Out1_492),
498
                              (hdot_Out1_592),
499
                              (hdotChgRate_Out1_692),
500
                              (altgammacmd_In1_6612),
501 501
                              self1,
502 502
                              self2)==>
503
       init_AltitudeControl(self1) ==> spec_85(AntEng_Out1_193, AltCmd_Out1_293, Alt_Out1_393, GsKts_Out1_493, hdot_Out1_593, hdotChgRate_Out1_693, altgammacmd_In1_6613, self2)==>
504
       spec_85(AntEng_Out1_193, AltCmd_Out1_293, Alt_Out1_393, GsKts_Out1_493, hdot_Out1_593, hdotChgRate_Out1_693, altgammacmd_In1_6613, self1)==>
505
       (spec_90(AntEng_Out1_193, AltCmd_Out1_293, Alt_Out1_393, GsKts_Out1_493, hdot_Out1_593, hdotChgRate_Out1_693, altgammacmd_In1_6613, self3));
503
       init_AltitudeControl(self1) ==> spec_85((AntEng_Out1_193), (AltCmd_Out1_293), (Alt_Out1_393), (GsKts_Out1_493), (hdot_Out1_593), (hdotChgRate_Out1_693), (altgammacmd_In1_6613), self2)==>
504
       spec_85((AntEng_Out1_193), (AltCmd_Out1_293), (Alt_Out1_393), (GsKts_Out1_493), (hdot_Out1_593), (hdotChgRate_Out1_693), (altgammacmd_In1_6613), self1)==>
505
       (spec_90((AntEng_Out1_193), (AltCmd_Out1_293), (Alt_Out1_393), (GsKts_Out1_493), (hdot_Out1_593), (hdotChgRate_Out1_693), (altgammacmd_In1_6613), self3));
506 506
*/
507 507
/*@ lemma inv_init_1_AltitudeControl : 
508 508
       \forall struct AltitudeControl_mem self3, struct AltitudeControl_mem self2, real AntEng_Out1_193, real AltCmd_Out1_293, real Alt_Out1_393, real GsKts_Out1_493, real hdot_Out1_593, real hdotChgRate_Out1_693, real altgammacmd_In1_6613;
509
       Ctrans_AltitudeControl(AntEng_Out1_193,
510
                              AltCmd_Out1_293,
511
                              Alt_Out1_393,
512
                              GsKts_Out1_493,
513
                              hdot_Out1_593,
514
                              hdotChgRate_Out1_693,
515
                              altgammacmd_In1_6613,
509
       Ctrans_AltitudeControl((AntEng_Out1_193),
510
                              (AltCmd_Out1_293),
511
                              (Alt_Out1_393),
512
                              (GsKts_Out1_493),
513
                              (hdot_Out1_593),
514
                              (hdotChgRate_Out1_693),
515
                              (altgammacmd_In1_6613),
516 516
                              self2,
517 517
                              self3)==>
518
       init_AltitudeControl(self2) ==> spec_85(AntEng_Out1_193, AltCmd_Out1_293, Alt_Out1_393, GsKts_Out1_493, hdot_Out1_593, hdotChgRate_Out1_693, altgammacmd_In1_6613, self2)==>
519
       (spec_90(AntEng_Out1_193, AltCmd_Out1_293, Alt_Out1_393, GsKts_Out1_493, hdot_Out1_593, hdotChgRate_Out1_693, altgammacmd_In1_6613, self3));
518
       init_AltitudeControl(self2) ==> spec_85((AntEng_Out1_193), (AltCmd_Out1_293), (Alt_Out1_393), (GsKts_Out1_493), (hdot_Out1_593), (hdotChgRate_Out1_693), (altgammacmd_In1_6613), self2)==>
519
       (spec_90((AntEng_Out1_193), (AltCmd_Out1_293), (Alt_Out1_393), (GsKts_Out1_493), (hdot_Out1_593), (hdotChgRate_Out1_693), (altgammacmd_In1_6613), self3));
520 520
*/
521 521
/*@ lemma inv_spec_AltitudeControl : 
522 522
       \forall struct AltitudeControl_mem self1, self2, real AntEng_Out1_19, real AltCmd_Out1_29, real Alt_Out1_39, real GsKts_Out1_49, real hdot_Out1_59, real hdotChgRate_Out1_69, real altgammacmd_In1_661;
523 523
       inv_AltitudeControl(self1)==>
524
       Ctrans_AltitudeControl(AntEng_Out1_19,
525
                              AltCmd_Out1_29,
526
                              Alt_Out1_39,
527
                              GsKts_Out1_49,
528
                              hdot_Out1_59,
529
                              hdotChgRate_Out1_69,
530
                              altgammacmd_In1_661,
524
       Ctrans_AltitudeControl((AntEng_Out1_19),
525
                              (AltCmd_Out1_29),
526
                              (Alt_Out1_39),
527
                              (GsKts_Out1_49),
528
                              (hdot_Out1_59),
529
                              (hdotChgRate_Out1_69),
530
                              (altgammacmd_In1_661),
531 531
                              self1,
532 532
                              self2)==>
533
       spec_85(AntEng_Out1_19, AltCmd_Out1_29, Alt_Out1_39, GsKts_Out1_49, hdot_Out1_59, hdotChgRate_Out1_69, altgammacmd_In1_661, self1)==>
534
       spec_90(AntEng_Out1_19, AltCmd_Out1_29, Alt_Out1_39, GsKts_Out1_49, hdot_Out1_59, hdotChgRate_Out1_69, altgammacmd_In1_661, self2);
533
       spec_85((AntEng_Out1_19), (AltCmd_Out1_29), (Alt_Out1_39), (GsKts_Out1_49), (hdot_Out1_59), (hdotChgRate_Out1_69), (altgammacmd_In1_661), self1)==>
534
       spec_90((AntEng_Out1_19), (AltCmd_Out1_29), (Alt_Out1_39), (GsKts_Out1_49), (hdot_Out1_59), (hdotChgRate_Out1_69), (altgammacmd_In1_661), self2);
535 535
*/
536 536
/*@ lemma inv_inv_AltitudeControl : 
537 537
       \forall struct AltitudeControl_mem self1, self2, real AntEng_Out1_19, real AltCmd_Out1_29, real Alt_Out1_39, real GsKts_Out1_49, real hdot_Out1_59, real hdotChgRate_Out1_69, real altgammacmd_In1_661;
538 538
       inv_AltitudeControl(self1)==>
539
       Ctrans_AltitudeControl(AntEng_Out1_19,
540
                              AltCmd_Out1_29,
541
                              Alt_Out1_39,
542
                              GsKts_Out1_49,
543
                              hdot_Out1_59,
544
                              hdotChgRate_Out1_69,
545
                              altgammacmd_In1_661,
539
       Ctrans_AltitudeControl((AntEng_Out1_19),
540
                              (AltCmd_Out1_29),
541
                              (Alt_Out1_39),
542
                              (GsKts_Out1_49),
543
                              (hdot_Out1_59),
544
                              (hdotChgRate_Out1_69),
545
                              (altgammacmd_In1_661),
546 546
                              self1,
547 547
                              self2)==>
548
       spec_85(AntEng_Out1_19, AltCmd_Out1_29, Alt_Out1_39, GsKts_Out1_49, hdot_Out1_59, hdotChgRate_Out1_69, altgammacmd_In1_661, self1)==>
548
       spec_85((AntEng_Out1_19), (AltCmd_Out1_29), (Alt_Out1_39), (GsKts_Out1_49), (hdot_Out1_59), (hdotChgRate_Out1_69), (altgammacmd_In1_661), self1)==>
549 549
       inv_AltitudeControl(self2);
550 550
*/
551 551
#define AltitudeControl_DECLARE(attr, inst)\
......
566 566
/*@ requires \valid(altgammacmd_In1_661);
567 567
  requires \valid(self);
568 568
  requires \separated(altgammacmd_In1_661, self);
569
  requires spec_85(AntEng_Out1_19, AltCmd_Out1_29, Alt_Out1_39, GsKts_Out1_49, hdot_Out1_59, hdotChgRate_Out1_69, *altgammacmd_In1_661, *self);
569
  requires spec_85((AntEng_Out1_19), (AltCmd_Out1_29), (Alt_Out1_39), (GsKts_Out1_49), (hdot_Out1_59), (hdotChgRate_Out1_69), (*altgammacmd_In1_661), *self);
570 570
  requires inv_AltitudeControl(*self);
571
  ensures spec_90(AntEng_Out1_19, AltCmd_Out1_29, Alt_Out1_39, GsKts_Out1_49, hdot_Out1_59, hdotChgRate_Out1_69, *altgammacmd_In1_661, *self);
571
  ensures spec_90((AntEng_Out1_19), (AltCmd_Out1_29), (Alt_Out1_39), (GsKts_Out1_49), (hdot_Out1_59), (hdotChgRate_Out1_69), (*altgammacmd_In1_661), *self);
572 572
  ensures inv_AltitudeControl(*self);
573
  ensures Ctrans_AltitudeControl(AntEng_Out1_19,
574
                                 AltCmd_Out1_29,
575
                                 Alt_Out1_39,
576
                                 GsKts_Out1_49,
577
                                 hdot_Out1_59,
578
                                 hdotChgRate_Out1_69,
579
                                 *altgammacmd_In1_661,
573
  ensures Ctrans_AltitudeControl((AntEng_Out1_19),
574
                                 (AltCmd_Out1_29),
575
                                 (Alt_Out1_39),
576
                                 (GsKts_Out1_49),
577
                                 (hdot_Out1_59),
578
                                 (hdotChgRate_Out1_69),
579
                                 (*altgammacmd_In1_661),
580 580
                                 \at(*self, Pre),
581 581
                                 (*self));
582 582
  

Also available in: Unified diff