Project

General

Profile

Download (32.6 KB) Statistics
| Branch: | Tag: | Revision:
1
/* C code generated by main_lustre_compiler.native
2
   SVN version number 355
3
   Code is C99 compliant */
4
   
5
#ifndef _ALT_2_LUSTREC
6
#define _ALT_2_LUSTREC
7

    
8
/* Imports standard library */
9
#include "/home/davyg/local_proofcompilation//include/lustrec/arrow.h"
10

    
11

    
12
/* Types definitions */
13

    
14
/*@ lemma missing: \forall _Bool x; (x != 0) <==> (((int) x) != 0);*/
15
/* Global constant (declarations, definitions are in C file) */
16

    
17
/* Struct declarations */
18
struct integrator_reset_mem {struct integrator_reset_reg {double __integrator_reset_2;} _reg; struct _arrow_mem ni_3; };
19
struct VariableRateLimit_mem {struct VariableRateLimit_reg {double __VariableRateLimit_3;} _reg; struct _arrow_mem ni_2; struct integrator_reset_mem ni_1; };
20
struct AltitudeControl_mem {struct AltitudeControl_reg {int dummy;} _reg; struct VariableRateLimit_mem ni_0; };
21

    
22
/* Nodes declarations */
23
/*@ predicate trans_VariableLimitSaturation(real up_lim,
24
                                            real Signal,
25
                                            real lo_lim,
26
                                            real out,
27
                                            boolean __VariableLimitSaturation_1,
28
                                            boolean __VariableLimitSaturation_2,
29
                                            real enforce_lo_lim) =
30
       
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
*/
36
/*@ predicate Ctrans_VariableLimitSaturation(real up_lim,
37
                                             real Signal,
38
                                             real lo_lim,
39
                                             real out) =
40
       \exists boolean __VariableLimitSaturation_1;
41
       \exists boolean __VariableLimitSaturation_2;
42
       \exists real 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
*/
51
/*@ requires \valid(out);
52
  ensures Ctrans_VariableLimitSaturation((up_lim),
53
                                         (Signal),
54
                                         (lo_lim),
55
                                         (*out));
56
  assigns *out;
57
  */
58
extern void VariableLimitSaturation_step (double up_lim, double Signal,
59
                                          double lo_lim, 
60
                                          double (*out)
61
                                          );
62

    
63
/*@ predicate trans_integrator_reset(real Fx,
64
                                     boolean ResetLevel,
65
                                     real x0,
66
                                     real ir_out,
67
                                     struct integrator_reset_mem self1,
68
                                     struct integrator_reset_mem self2,
69
                                     boolean __integrator_reset_1) =
70
       
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
*/
75
/*@ predicate Ctrans_integrator_reset(real Fx,
76
                                      boolean ResetLevel,
77
                                      real x0,
78
                                      real ir_out,
79
                                      struct integrator_reset_mem self1,
80
                                      struct integrator_reset_mem self2) =
81
       \exists boolean __integrator_reset_1;
82
       trans_integrator_reset((Fx),
83
                              (ResetLevel?\true:\false),
84
                              (x0),
85
                              (ir_out),
86
                              self1,
87
                              self2,
88
                              (__integrator_reset_1?\true:\false));
89
*/
90
/*@ predicate init_integrator_reset(struct integrator_reset_mem self) =
91
       
92
       (self.ni_3._reg._first==1);
93
*/
94
#define integrator_reset_DECLARE(attr, inst)\
95
  attr struct integrator_reset_mem inst;\
96
  _arrow_DECLARE(attr, inst ## _ni_3);
97
  
98

    
99
#define integrator_reset_ALLOC(attr,inst)\
100
  integrator_reset_DECLARE(attr,inst);
101

    
102

    
103
/*@requires \valid(self);
104
ensures init_integrator_reset(\at(*self, Here));
105
assigns *self;*/
106
extern void integrator_reset_reset (struct integrator_reset_mem *self);
107

    
108
/*@ requires \valid(ir_out);
109
  requires \valid(self);
110
  requires \separated(ir_out, self);
111
  ensures Ctrans_integrator_reset((Fx),
112
                                  (ResetLevel?\true:\false),
113
                                  (x0),
114
                                  (*ir_out),
115
                                  \at(*self, Pre),
116
                                  (*self));
117
  assigns *ir_out, *self;
118
  */
119
extern void integrator_reset_step (double Fx, _Bool ResetLevel, double x0, 
120
                                   double (*ir_out),
121
                                   struct integrator_reset_mem *self);
122

    
123
/*@ predicate trans_Saturation(real Signal,
124
                               real s_out,
125
                               boolean __Saturation_1,
126
                               boolean __Saturation_2,
127
                               real enforce_lo_lim) =
128
       
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
*/
134
/*@ predicate Ctrans_Saturation(real Signal,
135
                                real s_out) =
136
       \exists boolean __Saturation_1;
137
       \exists boolean __Saturation_2;
138
       \exists real 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
*/
145
/*@ requires \valid(s_out);
146
  ensures Ctrans_Saturation((Signal),
147
                            (*s_out));
148
  assigns *s_out;
149
  */
150
extern void Saturation_step (double Signal, 
151
                             double (*s_out)
152
                             );
153

    
154
/*@ predicate trans_VariableRateLimit(real ratelim_Out1_334,
155
                                      real input_Out1_344,
156
                                      boolean ICtrig_Out1_354,
157
                                      real IC_Out1_364,
158
                                      real output_In1_489,
159
                                      struct VariableRateLimit_mem self1,
160
                                      struct VariableRateLimit_mem self2,
161
                                      real Gain1_Out1_382,
162
                                      real Gain_Out1_373,
163
                                      real Integrator1_Out1_391,
164
                                      real Sum2_Out1_401,
165
                                      real Variable_Limit_Saturation_Out1_410,
166
                                      boolean __VariableRateLimit_1,
167
                                      real __VariableRateLimit_2) =
168
       
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
                               self1.ni_1,
184
                               self2.ni_1) &&
185
       (self2._reg.__VariableRateLimit_3 == (__VariableRateLimit_2));
186
*/
187
/*@ predicate Ctrans_VariableRateLimit(real ratelim_Out1_334,
188
                                       real input_Out1_344,
189
                                       boolean ICtrig_Out1_354,
190
                                       real IC_Out1_364,
191
                                       real output_In1_489,
192
                                       struct VariableRateLimit_mem self1,
193
                                       struct VariableRateLimit_mem self2) =
194
       \exists real Gain1_Out1_382;
195
       \exists real Gain_Out1_373;
196
       \exists real Integrator1_Out1_391;
197
       \exists real Sum2_Out1_401;
198
       \exists real Variable_Limit_Saturation_Out1_410;
199
       \exists boolean __VariableRateLimit_1;
200
       \exists real __VariableRateLimit_2;
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
                               self1,
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?\true:\false),
214
                               (__VariableRateLimit_2));
215
*/
216
/*@ predicate init_VariableRateLimit(struct VariableRateLimit_mem self) =
217
       
218
       (self.ni_2._reg._first==1) &&
219
       init_integrator_reset(self.ni_1);
220
*/
221
#define VariableRateLimit_DECLARE(attr, inst)\
222
  attr struct VariableRateLimit_mem inst;\
223
  _arrow_DECLARE(attr, inst ## _ni_2);\
224
  integrator_reset_DECLARE(attr, inst ## _ni_1);
225
  
226

    
227
#define VariableRateLimit_ALLOC(attr,inst)\
228
  VariableRateLimit_DECLARE(attr,inst);
229

    
230

    
231
/*@requires \valid(self);
232
ensures init_VariableRateLimit(\at(*self, Here));
233
assigns *self;*/
234
extern void VariableRateLimit_reset (struct VariableRateLimit_mem *self);
235

    
236
/*@ requires \valid(output_In1_489);
237
  requires \valid(self);
238
  requires \separated(output_In1_489, self);
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
                                   \at(*self, Pre),
245
                                   (*self));
246
  assigns *output_In1_489, *self;
247
  */
248
extern void VariableRateLimit_step (double ratelim_Out1_334,
249
                                    double input_Out1_344,
250
                                    _Bool ICtrig_Out1_354,
251
                                    double IC_Out1_364, 
252
                                    double (*output_In1_489),
253
                                    struct VariableRateLimit_mem *self);
254

    
255
/*@ predicate spec_85(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, struct AltitudeControl_mem self) =
256
       (AntEng_Out1_19 == 0.);
257
*/
258
/*@ predicate spec_90(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, struct AltitudeControl_mem self) =
259
       (altgammacmd_In1_661 == 0.);
260
*/
261
/*@ predicate trans_AltitudeControl(real AntEng_Out1_19,
262
                                    real AltCmd_Out1_29,
263
                                    real Alt_Out1_39,
264
                                    real GsKts_Out1_49,
265
                                    real hdot_Out1_59,
266
                                    real hdotChgRate_Out1_69,
267
                                    real altgammacmd_In1_661,
268
                                    struct AltitudeControl_mem self1,
269
                                    struct AltitudeControl_mem self2,
270
                                    real Abs_Out1_144,
271
                                    real Kh_Out1_193,
272
                                    boolean Logical_Operator_In1_197,
273
                                    boolean Logical_Operator_Out1_198,
274
                                    real Saturation1_Out1_213,
275
                                    real Sum3_Out1_296,
276
                                    real Sum_Out1_286,
277
                                    boolean Switch1_In2_312,
278
                                    real Switch1_Out1_314,
279
                                    boolean Switch_In2_303,
280
                                    real Switch_Out1_305,
281
                                    real Variable_Limit_Saturation_0_Out1_509,
282
                                    real Variable__Rate_Limit_Out1_324,
283
                                    boolean __AltitudeControl_1,
284
                                    boolean __AltitudeControl_2,
285
                                    real k_Out1_585,
286
                                    real kts2fps_Out1_594,
287
                                    real r2d_Out1_603) =
288
       
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
                                self1.ni_0,
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?\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
*/
319
/*@ predicate Ctrans_AltitudeControl(real AntEng_Out1_19,
320
                                     real AltCmd_Out1_29,
321
                                     real Alt_Out1_39,
322
                                     real GsKts_Out1_49,
323
                                     real hdot_Out1_59,
324
                                     real hdotChgRate_Out1_69,
325
                                     real altgammacmd_In1_661,
326
                                     struct AltitudeControl_mem self1,
327
                                     struct AltitudeControl_mem self2) =
328
       \exists real Abs_Out1_144;
329
       \exists real Kh_Out1_193;
330
       \exists boolean Logical_Operator_In1_197;
331
       \exists boolean Logical_Operator_Out1_198;
332
       \exists real Saturation1_Out1_213;
333
       \exists real Sum3_Out1_296;
334
       \exists real Sum_Out1_286;
335
       \exists boolean Switch1_In2_312;
336
       \exists real Switch1_Out1_314;
337
       \exists boolean Switch_In2_303;
338
       \exists real Switch_Out1_305;
339
       \exists real Variable_Limit_Saturation_0_Out1_509;
340
       \exists real Variable__Rate_Limit_Out1_324;
341
       \exists boolean __AltitudeControl_1;
342
       \exists boolean __AltitudeControl_2;
343
       \exists real k_Out1_585;
344
       \exists real kts2fps_Out1_594;
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),
353
                             self1,
354
                             self2,
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
*/
374
/*@ predicate init_AltitudeControl(struct AltitudeControl_mem self) =
375
       
376
       init_VariableRateLimit(self.ni_0);
377
*/
378
/*@ predicate inv_AltitudeControl(struct AltitudeControl_mem self3) =
379
       (init_AltitudeControl(self3))||
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),
388
                              self2,
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))&&
391
       init_AltitudeControl(self2))||
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),
400
                              self2,
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),
409
                              self1,
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))&&
413
       init_AltitudeControl(self1))||
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),
422
                              self2,
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),
431
                              self1,
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),
440
                              self0,
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)));
448
*/
449
/*@ lemma inv_init_3_AltitudeControl : 
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),
458
                              self2,
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),
467
                              self1,
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),
476
                              self0,
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));
482
*/
483
/*@ lemma inv_init_2_AltitudeControl : 
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),
492
                              self2,
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),
501
                              self1,
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));
506
*/
507
/*@ lemma inv_init_1_AltitudeControl : 
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),
516
                              self2,
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));
520
*/
521
/*@ lemma inv_spec_AltitudeControl : 
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
       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),
531
                              self1,
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);
535
*/
536
/*@ lemma inv_inv_AltitudeControl : 
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
       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),
546
                              self1,
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)==>
549
       inv_AltitudeControl(self2);
550
*/
551
#define AltitudeControl_DECLARE(attr, inst)\
552
  attr struct AltitudeControl_mem inst;\
553
  VariableRateLimit_DECLARE(attr, inst ## _ni_0);
554
  
555

    
556
#define AltitudeControl_ALLOC(attr,inst)\
557
  AltitudeControl_DECLARE(attr,inst);
558

    
559

    
560
/*@requires \valid(self);
561
ensures init_AltitudeControl(\at(*self, Here));
562
ensures inv_AltitudeControl(*self);
563
assigns *self;*/
564
extern void AltitudeControl_reset (struct AltitudeControl_mem *self);
565

    
566
/*@ requires \valid(altgammacmd_In1_661);
567
  requires \valid(self);
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);
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);
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),
580
                                 \at(*self, Pre),
581
                                 (*self));
582
  
583
  assigns *altgammacmd_In1_661, *self;
584
  
585
*/
586
extern void AltitudeControl_step (double AntEng_Out1_19,
587
                                  double AltCmd_Out1_29, double Alt_Out1_39,
588
                                  double GsKts_Out1_49, double hdot_Out1_59,
589
                                  double hdotChgRate_Out1_69, 
590
                                  double (*altgammacmd_In1_661),
591
                                  struct AltitudeControl_mem *self);
592

    
593

    
594
#endif
595

    
(3-3/4)