Project

General

Profile

« Previous | Next » 

Revision bff13707

Added by Guillaume Davy over 9 years ago

ALT_2 working with modification made by hand

View differences:

tcm_benchmarks/ALT2/ALT2_proof/ALT_2.lustrec.h
114 114
                                  x0,
115 115
                                  *ir_out,
116 116
                                  \at(*self, Pre),
117
                                  \at(*self, Here));
117
                                  (*self));
118 118
  assigns *ir_out, *self;
119 119
  */
120 120
extern void integrator_reset_step (double Fx, _Bool ResetLevel, double x0, 
......
178 178
                                      (double) Gain1_Out1_382,
179 179
                                      Variable_Limit_Saturation_Out1_410) &&
180 180
       Ctrans_integrator_reset((double) Variable_Limit_Saturation_Out1_410,
181
                               (_Bool) ((ICtrig_Out1_354)?1:0),
181
                               ICtrig_Out1_354,
182 182
                               (double) IC_Out1_364,
183 183
                               __VariableRateLimit_2,
184 184
                               self1.ni_2,
......
243 243
                                   IC_Out1_364,
244 244
                                   *output_In1_489,
245 245
                                   \at(*self, Pre),
246
                                   \at(*self, Here));
246
                                   (*self));
247 247
  assigns *output_In1_489, *self;
248 248
  */
249 249
extern void VariableRateLimit_step (double ratelim_Out1_334,
......
579 579
                                 hdotChgRate_Out1_69,
580 580
                                 *altgammacmd_In1_661,
581 581
                                 \at(*self, Pre),
582
                                 \at(*self, Here));
582
                                 (*self));
583 583
  
584 584
  assigns *altgammacmd_In1_661, *self;
585 585
  
......
667 667
                     hdotChgRate,
668 668
                     *obs,
669 669
                     \at(*self, Pre),
670
                     \at(*self, Here));
670
                     (*self));
671 671
  assigns *obs, *self;
672 672
  */
673 673
extern void top_step (_Bool AltEng, double AltCmd, double Altitude,

Also available in: Unified diff