Project

General

Profile

Download (25.2 KB) Statistics
| Branch: | Tag: | Revision:
1
#include <stdlib.h>
2
#include <assert.h>
3
#include "ALT_2.lustrec.h"
4

    
5
/* C code generated by main_lustre_compiler.native
6
   SVN version number 355
7
   Code is C99 compliant */
8
   
9
/* Imported nodes declarations */
10

    
11
/* Global constants (definitions) */
12

    
13
void AltitudeControl_reset (struct AltitudeControl_mem *self) {
14
  /*@
15
  ensures init_VariableRateLimit((*self).ni_0);
16
  assigns (*self).ni_0;
17
  */
18
  {
19
  VariableRateLimit_reset(&self->ni_0);
20
  }
21
  return;
22
}
23

    
24
void AltitudeControl_step (double AntEng_Out1_19, double AltCmd_Out1_29,
25
                           double Alt_Out1_39, double GsKts_Out1_49,
26
                           double hdot_Out1_59, double hdotChgRate_Out1_69, 
27
                           double (*altgammacmd_In1_661),
28
                           struct AltitudeControl_mem *self) {
29
  /*@ensures Ctrans_AltitudeControl((AntEng_Out1_19),
30
                                    (AltCmd_Out1_29),
31
                                    (Alt_Out1_39),
32
                                    (GsKts_Out1_49),
33
                                    (hdot_Out1_59),
34
                                    (hdotChgRate_Out1_69),
35
                                    (*altgammacmd_In1_661),
36
                                    \at(*self, Pre),
37
                                    (*self));
38
  assigns *altgammacmd_In1_661, *self;
39
  */
40
  {
41
  
42
  double Abs_Out1_144;
43
  double Kh_Out1_193;
44
  _Bool Logical_Operator_In1_197;
45
  _Bool Logical_Operator_Out1_198;
46
  double Saturation1_Out1_213;
47
  double Sum3_Out1_296;
48
  double Sum_Out1_286;
49
  _Bool Switch1_In2_312;
50
  double Switch1_Out1_314;
51
  _Bool Switch_In2_303;
52
  double Switch_Out1_305;
53
  double Variable_Limit_Saturation_0_Out1_509;
54
  double Variable__Rate_Limit_Out1_324;
55
  _Bool __AltitudeControl_1;
56
  _Bool __AltitudeControl_2;
57
  double k_Out1_585;
58
  double kts2fps_Out1_594;
59
  double r2d_Out1_603;
60
  
61
  
62
  /* Asserting trans predicate: locals are [Saturation1_Out1_213: real, Variable_Limit_Saturation_0_Out1_509: real, Variable__Rate_Limit_Out1_324: real] */
63
  /*@ensures \exists real Saturation1_Out1_213;
64
  \exists real Variable_Limit_Saturation_0_Out1_509;
65
  \exists real Variable__Rate_Limit_Out1_324;
66
  trans_AltitudeControl((AntEng_Out1_19),
67
                        (AltCmd_Out1_29),
68
                        (Alt_Out1_39),
69
                        (GsKts_Out1_49),
70
                        (hdot_Out1_59),
71
                        (hdotChgRate_Out1_69),
72
                        (*altgammacmd_In1_661),
73
                        \at(*self, Pre),
74
                        (*self),
75
                        (Abs_Out1_144),
76
                        (Kh_Out1_193),
77
                        (Logical_Operator_In1_197?\true:\false),
78
                        (Logical_Operator_Out1_198?\true:\false),
79
                        (Saturation1_Out1_213),
80
                        (Sum3_Out1_296),
81
                        (Sum_Out1_286),
82
                        (Switch1_In2_312?\true:\false),
83
                        (Switch1_Out1_314),
84
                        (Switch_In2_303?\true:\false),
85
                        (Switch_Out1_305),
86
                        (Variable_Limit_Saturation_0_Out1_509),
87
                        (Variable__Rate_Limit_Out1_324),
88
                        (__AltitudeControl_1?\true:\false),
89
                        (__AltitudeControl_2?\true:\false),
90
                        (k_Out1_585),
91
                        (kts2fps_Out1_594),
92
                        (r2d_Out1_603));
93
  assigns *altgammacmd_In1_661, *self, Abs_Out1_144, Kh_Out1_193,
94
          Logical_Operator_In1_197, Logical_Operator_Out1_198,
95
          Saturation1_Out1_213, Sum3_Out1_296, Sum_Out1_286, Switch1_In2_312,
96
          Switch1_Out1_314, Switch_In2_303, Switch_Out1_305,
97
          Variable_Limit_Saturation_0_Out1_509,
98
          Variable__Rate_Limit_Out1_324, __AltitudeControl_1,
99
          __AltitudeControl_2, k_Out1_585, kts2fps_Out1_594, r2d_Out1_603;
100
  */
101
  {
102
  
103
  /*@ensures \exists real Variable_Limit_Saturation_0_Out1_509;
104
  \exists real Variable__Rate_Limit_Out1_324;
105
  trans_AltitudeControl((AntEng_Out1_19),
106
                        (AltCmd_Out1_29),
107
                        (Alt_Out1_39),
108
                        (GsKts_Out1_49),
109
                        (hdot_Out1_59),
110
                        (hdotChgRate_Out1_69),
111
                        (*altgammacmd_In1_661),
112
                        \at(*self, Pre),
113
                        (*self),
114
                        (Abs_Out1_144),
115
                        (Kh_Out1_193),
116
                        (Logical_Operator_In1_197?\true:\false),
117
                        (Logical_Operator_Out1_198?\true:\false),
118
                        (Saturation1_Out1_213),
119
                        (Sum3_Out1_296),
120
                        (Sum_Out1_286),
121
                        (Switch1_In2_312?\true:\false),
122
                        (Switch1_Out1_314),
123
                        (Switch_In2_303?\true:\false),
124
                        (Switch_Out1_305),
125
                        (Variable_Limit_Saturation_0_Out1_509),
126
                        (Variable__Rate_Limit_Out1_324),
127
                        (__AltitudeControl_1?\true:\false),
128
                        (__AltitudeControl_2?\true:\false),
129
                        (k_Out1_585),
130
                        (kts2fps_Out1_594),
131
                        (r2d_Out1_603));
132
  assigns *altgammacmd_In1_661, *self, Abs_Out1_144, Kh_Out1_193,
133
          Logical_Operator_In1_197, Logical_Operator_Out1_198,
134
          Saturation1_Out1_213, Sum3_Out1_296, Sum_Out1_286, Switch1_In2_312,
135
          Switch1_Out1_314, Switch_In2_303, Switch_Out1_305,
136
          Variable_Limit_Saturation_0_Out1_509,
137
          Variable__Rate_Limit_Out1_324, __AltitudeControl_1,
138
          __AltitudeControl_2, k_Out1_585, kts2fps_Out1_594, r2d_Out1_603;
139
  */
140
  {
141
  
142
  /*@ensures \exists real Variable__Rate_Limit_Out1_324;
143
  trans_AltitudeControl((AntEng_Out1_19),
144
                        (AltCmd_Out1_29),
145
                        (Alt_Out1_39),
146
                        (GsKts_Out1_49),
147
                        (hdot_Out1_59),
148
                        (hdotChgRate_Out1_69),
149
                        (*altgammacmd_In1_661),
150
                        \at(*self, Pre),
151
                        (*self),
152
                        (Abs_Out1_144),
153
                        (Kh_Out1_193),
154
                        (Logical_Operator_In1_197?\true:\false),
155
                        (Logical_Operator_Out1_198?\true:\false),
156
                        (Saturation1_Out1_213),
157
                        (Sum3_Out1_296),
158
                        (Sum_Out1_286),
159
                        (Switch1_In2_312?\true:\false),
160
                        (Switch1_Out1_314),
161
                        (Switch_In2_303?\true:\false),
162
                        (Switch_Out1_305),
163
                        (Variable_Limit_Saturation_0_Out1_509),
164
                        (Variable__Rate_Limit_Out1_324),
165
                        (__AltitudeControl_1?\true:\false),
166
                        (__AltitudeControl_2?\true:\false),
167
                        (k_Out1_585),
168
                        (kts2fps_Out1_594),
169
                        (r2d_Out1_603));
170
  assigns *altgammacmd_In1_661, *self, Abs_Out1_144, Kh_Out1_193,
171
          Logical_Operator_In1_197, Logical_Operator_Out1_198,
172
          Saturation1_Out1_213, Sum3_Out1_296, Sum_Out1_286, Switch1_In2_312,
173
          Switch1_Out1_314, Switch_In2_303, Switch_Out1_305,
174
          Variable_Limit_Saturation_0_Out1_509,
175
          Variable__Rate_Limit_Out1_324, __AltitudeControl_1,
176
          __AltitudeControl_2, k_Out1_585, kts2fps_Out1_594, r2d_Out1_603;
177
  */
178
  {
179
  
180
  /*@ensures trans_AltitudeControl((AntEng_Out1_19),
181
                                   (AltCmd_Out1_29),
182
                                   (Alt_Out1_39),
183
                                   (GsKts_Out1_49),
184
                                   (hdot_Out1_59),
185
                                   (hdotChgRate_Out1_69),
186
                                   (*altgammacmd_In1_661),
187
                                   \at(*self, Pre),
188
                                   (*self),
189
                                   (Abs_Out1_144),
190
                                   (Kh_Out1_193),
191
                                   (Logical_Operator_In1_197?\true:\false),
192
                                   (Logical_Operator_Out1_198?\true:\false),
193
                                   (Saturation1_Out1_213),
194
                                   (Sum3_Out1_296),
195
                                   (Sum_Out1_286),
196
                                   (Switch1_In2_312?\true:\false),
197
                                   (Switch1_Out1_314),
198
                                   (Switch_In2_303?\true:\false),
199
                                   (Switch_Out1_305),
200
                                   (Variable_Limit_Saturation_0_Out1_509),
201
                                   (Variable__Rate_Limit_Out1_324),
202
                                   (__AltitudeControl_1?\true:\false),
203
                                   (__AltitudeControl_2?\true:\false),
204
                                   (k_Out1_585),
205
                                   (kts2fps_Out1_594),
206
                                   (r2d_Out1_603));
207
  assigns *altgammacmd_In1_661, *self, Abs_Out1_144, Kh_Out1_193,
208
          Logical_Operator_In1_197, Logical_Operator_Out1_198,
209
          Saturation1_Out1_213, Sum3_Out1_296, Sum_Out1_286, Switch1_In2_312,
210
          Switch1_Out1_314, Switch_In2_303, Switch_Out1_305,
211
          Variable_Limit_Saturation_0_Out1_509,
212
          Variable__Rate_Limit_Out1_324, __AltitudeControl_1,
213
          __AltitudeControl_2, k_Out1_585, kts2fps_Out1_594, r2d_Out1_603;
214
  */
215
  {
216
  
217
  
218
  /*@
219
  ensures ((__AltitudeControl_1?\true:\false) == ((hdot_Out1_59) < 0.));
220
  assigns __AltitudeControl_1;
221
  */
222
  {
223
  __AltitudeControl_1 = (hdot_Out1_59 < 0.);
224
  }
225
  /*@
226
  ensures ((Abs_Out1_144) == ((__AltitudeControl_1?\true:\false)?((- (hdot_Out1_59))):((hdot_Out1_59))));
227
  assigns Abs_Out1_144;
228
  */
229
  {
230
  Abs_Out1_144 = (__AltitudeControl_1?((- hdot_Out1_59)):(hdot_Out1_59));
231
  }
232
  /*@
233
  ensures ((Sum3_Out1_296) == ((Abs_Out1_144) + 10.));
234
  assigns Sum3_Out1_296;
235
  */
236
  {
237
  Sum3_Out1_296 = (Abs_Out1_144 + 10.);
238
  }
239
  /*@
240
  ensures ((k_Out1_585) == (- (Sum3_Out1_296)));
241
  assigns k_Out1_585;
242
  */
243
  {
244
  k_Out1_585 = (- Sum3_Out1_296);
245
  }
246
  /*@
247
  ensures ((__AltitudeControl_2?\true:\false) == ((AntEng_Out1_19) == 0.));
248
  assigns __AltitudeControl_2;
249
  */
250
  {
251
  __AltitudeControl_2 = (AntEng_Out1_19 == 0.);
252
  }
253
  /*@
254
  ensures ((!(Logical_Operator_In1_197?\true:\false)) == (!((__AltitudeControl_2?\true:\false)?(0):(1))));
255
  assigns Logical_Operator_In1_197;
256
  */
257
  {
258
  Logical_Operator_In1_197 = (__AltitudeControl_2?(0):(1));
259
  }
260
  /*@
261
  ensures ((!(Logical_Operator_Out1_198?\true:\false)) == (!(!(Logical_Operator_In1_197?\true:\false))));
262
  assigns Logical_Operator_Out1_198;
263
  */
264
  {
265
  Logical_Operator_Out1_198 = (!Logical_Operator_In1_197);
266
  }
267
  /*@
268
  ensures ((!(Switch_In2_303?\true:\false)) == (!((__AltitudeControl_2?\true:\false)?(0):(1))));
269
  assigns Switch_In2_303;
270
  */
271
  {
272
  Switch_In2_303 = (__AltitudeControl_2?(0):(1));
273
  }
274
  /*@
275
  ensures ((Sum_Out1_286) == ((AltCmd_Out1_29) + (- (Alt_Out1_39))));
276
  assigns Sum_Out1_286;
277
  */
278
  {
279
  Sum_Out1_286 = (AltCmd_Out1_29 + (- Alt_Out1_39));
280
  }
281
  /*@
282
  ensures ((Kh_Out1_193) == (0.08 * (Sum_Out1_286)));
283
  assigns Kh_Out1_193;
284
  */
285
  {
286
  Kh_Out1_193 = (0.08 * Sum_Out1_286);
287
  }
288
  /*@
289
  ensures ((Switch_Out1_305) == ((Switch_In2_303?\true:\false)?((Kh_Out1_193)):(0.)));
290
  assigns Switch_Out1_305;
291
  */
292
  {
293
  Switch_Out1_305 = (Switch_In2_303?(Kh_Out1_193):(0.));
294
  }
295
  /*@
296
  ensures Ctrans_VariableLimitSaturation((Sum3_Out1_296),
297
                                         (Switch_Out1_305),
298
                                         (k_Out1_585),
299
                                         (Variable_Limit_Saturation_0_Out1_509));
300
  assigns Variable_Limit_Saturation_0_Out1_509;
301
  */
302
  {
303
  VariableLimitSaturation_step (Sum3_Out1_296, Switch_Out1_305, k_Out1_585, &Variable_Limit_Saturation_0_Out1_509);
304
  }
305
  /*@
306
  ensures Ctrans_VariableRateLimit((hdotChgRate_Out1_69),
307
                                   (Variable_Limit_Saturation_0_Out1_509),
308
                                   (Logical_Operator_Out1_198?\true:\false),
309
                                   (hdot_Out1_59),
310
                                   (Variable__Rate_Limit_Out1_324),
311
                                   \at(*self, Pre).ni_0,
312
                                   (*self).ni_0);
313
  assigns Variable__Rate_Limit_Out1_324, \at(*self, Pre).ni_0, (*self).ni_0;
314
  */
315
  {
316
  VariableRateLimit_step (hdotChgRate_Out1_69, Variable_Limit_Saturation_0_Out1_509, Logical_Operator_Out1_198, hdot_Out1_59, &Variable__Rate_Limit_Out1_324, &self->ni_0);
317
  }
318
  /*@
319
  ensures ((r2d_Out1_603) == (57.2958 * (Variable__Rate_Limit_Out1_324)));
320
  assigns r2d_Out1_603;
321
  */
322
  {
323
  r2d_Out1_603 = (57.2958 * Variable__Rate_Limit_Out1_324);
324
  }
325
  /*@
326
  ensures ((kts2fps_Out1_594) == (1.6878 * (GsKts_Out1_49)));
327
  assigns kts2fps_Out1_594;
328
  */
329
  {
330
  kts2fps_Out1_594 = (1.6878 * GsKts_Out1_49);
331
  }
332
  /*@
333
  ensures ((!(Switch1_In2_312?\true:\false)) == (!((__AltitudeControl_2?\true:\false)?(0):(1))));
334
  assigns Switch1_In2_312;
335
  */
336
  {
337
  Switch1_In2_312 = (__AltitudeControl_2?(0):(1));
338
  }
339
  /*@
340
  ensures ((Switch1_Out1_314) == ((Switch1_In2_312?\true:\false)?((r2d_Out1_603)):(0.)));
341
  assigns Switch1_Out1_314;
342
  */
343
  {
344
  Switch1_Out1_314 = (Switch1_In2_312?(r2d_Out1_603):(0.));
345
  }
346
  /*@
347
  ensures ((*altgammacmd_In1_661) == (Switch1_Out1_314));
348
  assigns *altgammacmd_In1_661;
349
  */
350
  {
351
  *altgammacmd_In1_661 = Switch1_Out1_314;
352
  }
353
  /*@
354
  ensures Ctrans_Saturation((kts2fps_Out1_594),
355
                            (Saturation1_Out1_213));
356
  assigns Saturation1_Out1_213;
357
  */
358
  {
359
  Saturation_step (kts2fps_Out1_594, &Saturation1_Out1_213);
360
  }
361
  }}}}}return;
362
}
363

    
364
void VariableRateLimit_reset (struct VariableRateLimit_mem *self) {
365
  /*@
366
  ensures ((*self).ni_2._reg._first==1);
367
  assigns (*self).ni_2;
368
  */
369
  {
370
  _arrow_reset(&self->ni_2);
371
  }
372
  /*@
373
  ensures init_integrator_reset((*self).ni_1);
374
  assigns (*self).ni_1;
375
  */
376
  {
377
  integrator_reset_reset(&self->ni_1);
378
  }
379
  return;
380
}
381

    
382
void VariableRateLimit_step (double ratelim_Out1_334, double input_Out1_344,
383
                             _Bool ICtrig_Out1_354, double IC_Out1_364, 
384
                             double (*output_In1_489),
385
                             struct VariableRateLimit_mem *self) {
386
  /*@ensures Ctrans_VariableRateLimit((ratelim_Out1_334),
387
                                      (input_Out1_344),
388
                                      (ICtrig_Out1_354?\true:\false),
389
                                      (IC_Out1_364),
390
                                      (*output_In1_489),
391
                                      \at(*self, Pre),
392
                                      (*self));
393
  assigns *output_In1_489, *self;
394
  */
395
  {
396
  
397
  double Gain1_Out1_382;
398
  double Gain_Out1_373;
399
  double Integrator1_Out1_391;
400
  double Sum2_Out1_401;
401
  double Variable_Limit_Saturation_Out1_410;
402
  _Bool __VariableRateLimit_1;
403
  double __VariableRateLimit_2;
404
  
405
  
406
  /* Asserting trans predicate: locals are [Variable_Limit_Saturation_Out1_410: real, __VariableRateLimit_2: real] */
407
  /*@ensures \exists real Variable_Limit_Saturation_Out1_410;
408
  \exists real __VariableRateLimit_2;
409
  trans_VariableRateLimit((ratelim_Out1_334),
410
                          (input_Out1_344),
411
                          (ICtrig_Out1_354?\true:\false),
412
                          (IC_Out1_364),
413
                          (*output_In1_489),
414
                          \at(*self, Pre),
415
                          (*self),
416
                          (Gain1_Out1_382),
417
                          (Gain_Out1_373),
418
                          (Integrator1_Out1_391),
419
                          (Sum2_Out1_401),
420
                          (Variable_Limit_Saturation_Out1_410),
421
                          (__VariableRateLimit_1?\true:\false),
422
                          (__VariableRateLimit_2));
423
  assigns *output_In1_489, *self, Gain1_Out1_382, Gain_Out1_373,
424
          Integrator1_Out1_391, Sum2_Out1_401,
425
          Variable_Limit_Saturation_Out1_410, __VariableRateLimit_1,
426
          __VariableRateLimit_2;
427
  */
428
  {
429
  
430
  /*@ensures \exists real __VariableRateLimit_2;
431
  trans_VariableRateLimit((ratelim_Out1_334),
432
                          (input_Out1_344),
433
                          (ICtrig_Out1_354?\true:\false),
434
                          (IC_Out1_364),
435
                          (*output_In1_489),
436
                          \at(*self, Pre),
437
                          (*self),
438
                          (Gain1_Out1_382),
439
                          (Gain_Out1_373),
440
                          (Integrator1_Out1_391),
441
                          (Sum2_Out1_401),
442
                          (Variable_Limit_Saturation_Out1_410),
443
                          (__VariableRateLimit_1?\true:\false),
444
                          (__VariableRateLimit_2));
445
  assigns *output_In1_489, *self, Gain1_Out1_382, Gain_Out1_373,
446
          Integrator1_Out1_391, Sum2_Out1_401,
447
          Variable_Limit_Saturation_Out1_410, __VariableRateLimit_1,
448
          __VariableRateLimit_2;
449
  */
450
  {
451
  
452
  /*@ensures trans_VariableRateLimit((ratelim_Out1_334),
453
                                     (input_Out1_344),
454
                                     (ICtrig_Out1_354?\true:\false),
455
                                     (IC_Out1_364),
456
                                     (*output_In1_489),
457
                                     \at(*self, Pre),
458
                                     (*self),
459
                                     (Gain1_Out1_382),
460
                                     (Gain_Out1_373),
461
                                     (Integrator1_Out1_391),
462
                                     (Sum2_Out1_401),
463
                                     (Variable_Limit_Saturation_Out1_410),
464
                                     (__VariableRateLimit_1?\true:\false),
465
                                     (__VariableRateLimit_2));
466
  assigns *output_In1_489, *self, Gain1_Out1_382, Gain_Out1_373,
467
          Integrator1_Out1_391, Sum2_Out1_401,
468
          Variable_Limit_Saturation_Out1_410, __VariableRateLimit_1,
469
          __VariableRateLimit_2;
470
  */
471
  {
472
  
473
  
474
  /*@
475
  ensures ((__VariableRateLimit_1?\true:\false)==(\at(*self, Pre).ni_2._reg._first?(1):(0))) && ((*self).ni_2._reg._first==0);
476
  assigns __VariableRateLimit_1, (*self).ni_2;
477
  */
478
  {
479
  _arrow_step (1, 0, &__VariableRateLimit_1, &self->ni_2);
480
  }
481
  /*@
482
  ensures ((Integrator1_Out1_391) == ((__VariableRateLimit_1?\true:\false)?((IC_Out1_364)):(\at(*self, Pre)._reg.__VariableRateLimit_3)));
483
  assigns Integrator1_Out1_391;
484
  */
485
  {
486
  Integrator1_Out1_391 = (__VariableRateLimit_1?(IC_Out1_364):(self->_reg.__VariableRateLimit_3));
487
  }
488
  /*@
489
  ensures ((*output_In1_489) == (Integrator1_Out1_391));
490
  assigns *output_In1_489;
491
  */
492
  {
493
  *output_In1_489 = Integrator1_Out1_391;
494
  }
495
  /*@
496
  ensures ((Gain1_Out1_382) == (- (ratelim_Out1_334)));
497
  assigns Gain1_Out1_382;
498
  */
499
  {
500
  Gain1_Out1_382 = (- ratelim_Out1_334);
501
  }
502
  /*@
503
  ensures ((Sum2_Out1_401) == ((input_Out1_344) + (- (Integrator1_Out1_391))));
504
  assigns Sum2_Out1_401;
505
  */
506
  {
507
  Sum2_Out1_401 = (input_Out1_344 + (- Integrator1_Out1_391));
508
  }
509
  /*@
510
  ensures ((Gain_Out1_373) == (20. * (Sum2_Out1_401)));
511
  assigns Gain_Out1_373;
512
  */
513
  {
514
  Gain_Out1_373 = (20. * Sum2_Out1_401);
515
  }
516
  /*@
517
  ensures Ctrans_VariableLimitSaturation((ratelim_Out1_334),
518
                                         (Gain_Out1_373),
519
                                         (Gain1_Out1_382),
520
                                         (Variable_Limit_Saturation_Out1_410));
521
  assigns Variable_Limit_Saturation_Out1_410;
522
  */
523
  {
524
  VariableLimitSaturation_step (ratelim_Out1_334, Gain_Out1_373, Gain1_Out1_382, &Variable_Limit_Saturation_Out1_410);
525
  }
526
  /*@
527
  ensures Ctrans_integrator_reset((Variable_Limit_Saturation_Out1_410),
528
                                  (ICtrig_Out1_354?\true:\false),
529
                                  (IC_Out1_364),
530
                                  (__VariableRateLimit_2),
531
                                  \at(*self, Pre).ni_1,
532
                                  (*self).ni_1);
533
  assigns __VariableRateLimit_2, \at(*self, Pre).ni_1, (*self).ni_1;
534
  */
535
  {
536
  integrator_reset_step (Variable_Limit_Saturation_Out1_410, ICtrig_Out1_354, IC_Out1_364, &__VariableRateLimit_2, &self->ni_1);
537
  }
538
  /*@
539
  ensures ((*self)._reg.__VariableRateLimit_3 == (__VariableRateLimit_2));
540
  assigns (*self)._reg.__VariableRateLimit_3;
541
  */
542
  {
543
  self->_reg.__VariableRateLimit_3 = __VariableRateLimit_2;
544
  }
545
  }}}}return;
546
}
547

    
548
void Saturation_step (double Signal, 
549
                      double (*s_out)
550
                      ) {
551
  /*@ensures Ctrans_Saturation((Signal),
552
                               (*s_out));
553
  assigns *s_out;
554
  */
555
  {
556
  
557
  _Bool __Saturation_1;
558
  _Bool __Saturation_2;
559
  double enforce_lo_lim;
560
  
561
  
562
  /* Asserting trans predicate: locals are [] */
563
  /*@ensures trans_Saturation((Signal),
564
                              (*s_out),
565
                              (__Saturation_1?\true:\false),
566
                              (__Saturation_2?\true:\false),
567
                              (enforce_lo_lim));
568
  assigns *s_out, __Saturation_1, __Saturation_2, enforce_lo_lim;
569
  */
570
  {
571
  
572
  /*@
573
  ensures ((__Saturation_1?\true:\false) == (0.0001 >= (Signal)));
574
  assigns __Saturation_1;
575
  */
576
  {
577
  __Saturation_1 = (0.0001 >= Signal);
578
  }
579
  /*@
580
  ensures ((enforce_lo_lim) == ((__Saturation_1?\true:\false)?(0.0001):((Signal))));
581
  assigns enforce_lo_lim;
582
  */
583
  {
584
  enforce_lo_lim = (__Saturation_1?(0.0001):(Signal));
585
  }
586
  /*@
587
  ensures ((__Saturation_2?\true:\false) == (1000. <= (enforce_lo_lim)));
588
  assigns __Saturation_2;
589
  */
590
  {
591
  __Saturation_2 = (1000. <= enforce_lo_lim);
592
  }
593
  /*@
594
  ensures ((*s_out) == ((__Saturation_2?\true:\false)?(1000.):((enforce_lo_lim))));
595
  assigns *s_out;
596
  */
597
  {
598
  *s_out = (__Saturation_2?(1000.):(enforce_lo_lim));
599
  }
600
  }}return;
601
}
602

    
603
void integrator_reset_reset (struct integrator_reset_mem *self) {
604
  /*@
605
  ensures ((*self).ni_3._reg._first==1);
606
  assigns (*self).ni_3;
607
  */
608
  {
609
  _arrow_reset(&self->ni_3);
610
  }
611
  return;
612
}
613

    
614
void integrator_reset_step (double Fx, _Bool ResetLevel, double x0, 
615
                            double (*ir_out),
616
                            struct integrator_reset_mem *self) {
617
  /*@ensures Ctrans_integrator_reset((Fx),
618
                                     (ResetLevel?\true:\false),
619
                                     (x0),
620
                                     (*ir_out),
621
                                     \at(*self, Pre),
622
                                     (*self));
623
  assigns *ir_out, *self;
624
  */
625
  {
626
  
627
  _Bool __integrator_reset_1;
628
  
629
  
630
  /* Asserting trans predicate: locals are [] */
631
  /*@ensures trans_integrator_reset((Fx),
632
                                    (ResetLevel?\true:\false),
633
                                    (x0),
634
                                    (*ir_out),
635
                                    \at(*self, Pre),
636
                                    (*self),
637
                                    (__integrator_reset_1?\true:\false));
638
  assigns *ir_out, *self, __integrator_reset_1;
639
  */
640
  {
641
  
642
  
643
  /*@
644
  ensures ((__integrator_reset_1?\true:\false)==(\at(*self, Pre).ni_3._reg._first?(1):(0))) && ((*self).ni_3._reg._first==0);
645
  assigns __integrator_reset_1, (*self).ni_3;
646
  */
647
  {
648
  _arrow_step (1, 0, &__integrator_reset_1, &self->ni_3);
649
  }
650
  /*@
651
  ensures ((*ir_out) == ((__integrator_reset_1?\true:\false)?((x0)):(((ResetLevel?\true:\false)?((x0)):((((Fx) * 1.) + \at(*self, Pre)._reg.__integrator_reset_2))))));
652
  assigns *ir_out;
653
  */
654
  {
655
  *ir_out = (__integrator_reset_1?(x0):((ResetLevel?(x0):(((Fx * 1.) + self->_reg.__integrator_reset_2)))));
656
  }
657
  /*@
658
  ensures ((*self)._reg.__integrator_reset_2 == (*ir_out));
659
  assigns (*self)._reg.__integrator_reset_2;
660
  */
661
  {
662
  self->_reg.__integrator_reset_2 = *ir_out;
663
  }
664
  }}return;
665
}
666

    
667
void VariableLimitSaturation_step (double up_lim, double Signal,
668
                                   double lo_lim, 
669
                                   double (*out)
670
                                   ) {
671
  /*@ensures Ctrans_VariableLimitSaturation((up_lim),
672
                                            (Signal),
673
                                            (lo_lim),
674
                                            (*out));
675
  assigns *out;
676
  */
677
  {
678
  
679
  _Bool __VariableLimitSaturation_1;
680
  _Bool __VariableLimitSaturation_2;
681
  double enforce_lo_lim;
682
  
683
  
684
  /* Asserting trans predicate: locals are [] */
685
  /*@ensures trans_VariableLimitSaturation((up_lim),
686
                                           (Signal),
687
                                           (lo_lim),
688
                                           (*out),
689
                                           (__VariableLimitSaturation_1?\true:\false),
690
                                           (__VariableLimitSaturation_2?\true:\false),
691
                                           (enforce_lo_lim));
692
  assigns *out, __VariableLimitSaturation_1, __VariableLimitSaturation_2,
693
          enforce_lo_lim;
694
  */
695
  {
696
  
697
  /*@
698
  ensures ((__VariableLimitSaturation_1?\true:\false) == ((Signal) >= (lo_lim)));
699
  assigns __VariableLimitSaturation_1;
700
  */
701
  {
702
  __VariableLimitSaturation_1 = (Signal >= lo_lim);
703
  }
704
  /*@
705
  ensures ((enforce_lo_lim) == ((__VariableLimitSaturation_1?\true:\false)?((Signal)):((lo_lim))));
706
  assigns enforce_lo_lim;
707
  */
708
  {
709
  enforce_lo_lim = (__VariableLimitSaturation_1?(Signal):(lo_lim));
710
  }
711
  /*@
712
  ensures ((__VariableLimitSaturation_2?\true:\false) == ((enforce_lo_lim) <= (up_lim)));
713
  assigns __VariableLimitSaturation_2;
714
  */
715
  {
716
  __VariableLimitSaturation_2 = (enforce_lo_lim <= up_lim);
717
  }
718
  /*@
719
  ensures ((*out) == ((__VariableLimitSaturation_2?\true:\false)?((enforce_lo_lim)):((up_lim))));
720
  assigns *out;
721
  */
722
  {
723
  *out = (__VariableLimitSaturation_2?(enforce_lo_lim):(up_lim));
724
  }
725
  }}return;
726
}
727

    
(1-1/4)