|
1
|
/* C code generated by lustrec
|
|
2
|
SVN version number 342
|
|
3
|
Code is C99 compliant */
|
|
4
|
|
|
5
|
#ifndef _ALT_2_LUSTREC
|
|
6
|
#define _ALT_2_LUSTREC
|
|
7
|
|
|
8
|
/* Imports standard library */
|
|
9
|
#include "/usr/local/include/lustrec/arrow.h"
|
|
10
|
|
|
11
|
|
|
12
|
/* Types definitions */
|
|
13
|
|
|
14
|
/* Global constant (declarations, definitions are in C file) */
|
|
15
|
|
|
16
|
/* Struct declarations */
|
|
17
|
struct integrator_reset_mem {struct integrator_reset_reg {double __integrator_reset_2;} _reg; struct _arrow_mem ni_4; };
|
|
18
|
struct VariableRateLimit_mem {struct VariableRateLimit_reg {double __VariableRateLimit_3;} _reg; struct _arrow_mem ni_3; struct integrator_reset_mem ni_2; };
|
|
19
|
struct AltitudeControl_mem {struct AltitudeControl_reg {int dummy;} _reg; struct VariableRateLimit_mem ni_1; };
|
|
20
|
struct top_mem {struct top_reg {int dummy;} _reg; struct AltitudeControl_mem ni_0; };
|
|
21
|
|
|
22
|
/* Nodes declarations */
|
|
23
|
/*@ requires \valid(out);
|
|
24
|
assigns *out;
|
|
25
|
*/
|
|
26
|
extern void VariableLimitSaturation_step (double up_lim, double Signal,
|
|
27
|
double lo_lim,
|
|
28
|
double (*out)
|
|
29
|
);
|
|
30
|
|
|
31
|
#define integrator_reset_DECLARE(attr, inst)\
|
|
32
|
attr struct integrator_reset_mem inst;\
|
|
33
|
_arrow_DECLARE(attr, inst ## _ni_4);
|
|
34
|
|
|
35
|
|
|
36
|
#define integrator_reset_ALLOC(attr,inst)\
|
|
37
|
integrator_reset_DECLARE(attr,inst);
|
|
38
|
|
|
39
|
|
|
40
|
/*@requires \valid(self);
|
|
41
|
assigns *self;*/
|
|
42
|
extern void integrator_reset_reset (struct integrator_reset_mem *self);
|
|
43
|
|
|
44
|
/*@ requires \valid(ir_out);
|
|
45
|
requires \valid(self);
|
|
46
|
requires \separated(ir_out, self);
|
|
47
|
assigns *ir_out, *self;
|
|
48
|
*/
|
|
49
|
extern void integrator_reset_step (double Fx, _Bool ResetLevel, double x0,
|
|
50
|
double (*ir_out),
|
|
51
|
struct integrator_reset_mem *self);
|
|
52
|
|
|
53
|
/*@ requires \valid(s_out);
|
|
54
|
assigns *s_out;
|
|
55
|
*/
|
|
56
|
extern void Saturation_step (double Signal,
|
|
57
|
double (*s_out)
|
|
58
|
);
|
|
59
|
|
|
60
|
#define VariableRateLimit_DECLARE(attr, inst)\
|
|
61
|
attr struct VariableRateLimit_mem inst;\
|
|
62
|
_arrow_DECLARE(attr, inst ## _ni_3);\
|
|
63
|
integrator_reset_DECLARE(attr, inst ## _ni_2);
|
|
64
|
|
|
65
|
|
|
66
|
#define VariableRateLimit_ALLOC(attr,inst)\
|
|
67
|
VariableRateLimit_DECLARE(attr,inst);
|
|
68
|
|
|
69
|
|
|
70
|
/*@requires \valid(self);
|
|
71
|
assigns *self;*/
|
|
72
|
extern void VariableRateLimit_reset (struct VariableRateLimit_mem *self);
|
|
73
|
|
|
74
|
/*@ requires \valid(output_In1_489);
|
|
75
|
requires \valid(self);
|
|
76
|
requires \separated(output_In1_489, self);
|
|
77
|
assigns *output_In1_489, *self;
|
|
78
|
*/
|
|
79
|
extern void VariableRateLimit_step (double ratelim_Out1_334,
|
|
80
|
double input_Out1_344,
|
|
81
|
_Bool ICtrig_Out1_354,
|
|
82
|
double IC_Out1_364,
|
|
83
|
double (*output_In1_489),
|
|
84
|
struct VariableRateLimit_mem *self);
|
|
85
|
|
|
86
|
/*@ 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) =
|
|
87
|
(AntEng_Out1_19 == 0.);
|
|
88
|
*/
|
|
89
|
/*@ 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) =
|
|
90
|
(altgammacmd_In1_661 == 0.);
|
|
91
|
*/
|
|
92
|
#define AltitudeControl_DECLARE(attr, inst)\
|
|
93
|
attr struct AltitudeControl_mem inst;\
|
|
94
|
VariableRateLimit_DECLARE(attr, inst ## _ni_1);
|
|
95
|
|
|
96
|
|
|
97
|
#define AltitudeControl_ALLOC(attr,inst)\
|
|
98
|
AltitudeControl_DECLARE(attr,inst);
|
|
99
|
|
|
100
|
|
|
101
|
/*@requires \valid(self);
|
|
102
|
assigns *self;*/
|
|
103
|
extern void AltitudeControl_reset (struct AltitudeControl_mem *self);
|
|
104
|
|
|
105
|
/*@ requires \valid(altgammacmd_In1_661);
|
|
106
|
requires \valid(self);
|
|
107
|
requires \separated(altgammacmd_In1_661, self);
|
|
108
|
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);
|
|
109
|
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);
|
|
110
|
|
|
111
|
assigns *altgammacmd_In1_661, *self;
|
|
112
|
|
|
113
|
*/
|
|
114
|
extern void AltitudeControl_step (double AntEng_Out1_19,
|
|
115
|
double AltCmd_Out1_29, double Alt_Out1_39,
|
|
116
|
double GsKts_Out1_49, double hdot_Out1_59,
|
|
117
|
double hdotChgRate_Out1_69,
|
|
118
|
double (*altgammacmd_In1_661),
|
|
119
|
struct AltitudeControl_mem *self);
|
|
120
|
|
|
121
|
#define top_DECLARE(attr, inst)\
|
|
122
|
attr struct top_mem inst;\
|
|
123
|
AltitudeControl_DECLARE(attr, inst ## _ni_0);
|
|
124
|
|
|
125
|
|
|
126
|
#define top_ALLOC(attr,inst)\
|
|
127
|
top_DECLARE(attr,inst);
|
|
128
|
|
|
129
|
|
|
130
|
/*@requires \valid(self);
|
|
131
|
assigns *self;*/
|
|
132
|
extern void top_reset (struct top_mem *self);
|
|
133
|
|
|
134
|
/*@ requires \valid(obs);
|
|
135
|
requires \valid(self);
|
|
136
|
requires \separated(obs, self);
|
|
137
|
assigns *obs, *self;
|
|
138
|
*/
|
|
139
|
extern void top_step (_Bool AltEng, double AltCmd, double Altitude,
|
|
140
|
double gskts, double hdot, double hdotChgRate,
|
|
141
|
_Bool (*obs),
|
|
142
|
struct top_mem *self);
|
|
143
|
|
|
144
|
|
|
145
|
#endif
|
|
146
|
|