Revision 23c510d0
Added by Guillaume Davy over 8 years ago
tcm_benchmarks/ALT2/ALT2_proof_inlined/ALT_2.lustrec.c  

68  68 
double r2d_Out1_603; 
69  69 

70  70 

71 
/* Asserting trans predicate: locals are [] */ 

71 
/* Asserting trans predicate: locals are [Abs_Out1_144: real, Kh_Out1_193: real, Logical_Operator_In1_197: bool, Logical_Operator_Out1_198: bool, Saturation_115_enforce_lo_lim: real, Saturation_115_s_out: real, Sum3_Out1_296: real, Sum_Out1_286: real, Switch1_In2_312: bool, Switch1_Out1_314: real, Switch_In2_303: bool, Switch_Out1_305: real, VariableLimitSaturation_144_enforce_lo_lim: real, VariableLimitSaturation_144_out: real, VariableRateLimit_139_Gain1_Out1_382: real, VariableRateLimit_139_Gain_Out1_373: real, VariableRateLimit_139_Integrator1_Out1_391: real, VariableRateLimit_139_Sum2_Out1_401: real, VariableRateLimit_139_VariableLimitSaturation_69_enforce_lo_lim: real, VariableRateLimit_139_VariableLimitSaturation_69_out: real, VariableRateLimit_139_integrator_reset_56_ir_out: real, __AltitudeControl_1: bool, __AltitudeControl_10: bool, __AltitudeControl_2: bool, __AltitudeControl_3: bool, __AltitudeControl_4: bool, __AltitudeControl_5: bool, __AltitudeControl_6: bool, __AltitudeControl_8: bool, __AltitudeControl_9: bool, k_Out1_585: real, kts2fps_Out1_594: real, r2d_Out1_603: real] */ 

72 
/*@ensures \exists real Abs_Out1_144; 

73 
\exists real Kh_Out1_193; 

74 
\exists _Bool Logical_Operator_In1_197; 

75 
\exists _Bool Logical_Operator_Out1_198; 

76 
\exists real Saturation_115_enforce_lo_lim; 

77 
\exists real Saturation_115_s_out; 

78 
\exists real Sum3_Out1_296; 

79 
\exists real Sum_Out1_286; 

80 
\exists _Bool Switch1_In2_312; 

81 
\exists real Switch1_Out1_314; 

82 
\exists _Bool Switch_In2_303; 

83 
\exists real Switch_Out1_305; 

84 
\exists real VariableLimitSaturation_144_enforce_lo_lim; 

85 
\exists real VariableLimitSaturation_144_out; 

86 
\exists real VariableRateLimit_139_Gain1_Out1_382; 

87 
\exists real VariableRateLimit_139_Gain_Out1_373; 

88 
\exists real VariableRateLimit_139_Integrator1_Out1_391; 

89 
\exists real VariableRateLimit_139_Sum2_Out1_401; 

90 
\exists real VariableRateLimit_139_VariableLimitSaturation_69_enforce_lo_lim; 

91 
\exists real VariableRateLimit_139_VariableLimitSaturation_69_out; 

92 
\exists real VariableRateLimit_139_integrator_reset_56_ir_out; 

93 
\exists _Bool __AltitudeControl_1; 

94 
\exists _Bool __AltitudeControl_10; 

95 
\exists _Bool __AltitudeControl_2; 

96 
\exists _Bool __AltitudeControl_3; 

97 
\exists _Bool __AltitudeControl_4; 

98 
\exists _Bool __AltitudeControl_5; 

99 
\exists _Bool __AltitudeControl_6; 

100 
\exists _Bool __AltitudeControl_8; 

101 
\exists _Bool __AltitudeControl_9; 

102 
\exists real k_Out1_585; 

103 
\exists real kts2fps_Out1_594; 

104 
\exists real r2d_Out1_603; 

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 
\at(*self, Here), 

114 
Abs_Out1_144, 

115 
Kh_Out1_193, 

116 
Logical_Operator_In1_197, 

117 
Logical_Operator_Out1_198, 

118 
Saturation_115_enforce_lo_lim, 

119 
Saturation_115_s_out, 

120 
Sum3_Out1_296, 

121 
Sum_Out1_286, 

122 
Switch1_In2_312, 

123 
Switch1_Out1_314, 

124 
Switch_In2_303, 

125 
Switch_Out1_305, 

126 
VariableLimitSaturation_144_enforce_lo_lim, 

127 
VariableLimitSaturation_144_out, 

128 
VariableRateLimit_139_Gain1_Out1_382, 

129 
VariableRateLimit_139_Gain_Out1_373, 

130 
VariableRateLimit_139_Integrator1_Out1_391, 

131 
VariableRateLimit_139_Sum2_Out1_401, 

132 
VariableRateLimit_139_VariableLimitSaturation_69_enforce_lo_lim, 

133 
VariableRateLimit_139_VariableLimitSaturation_69_out, 

134 
VariableRateLimit_139_integrator_reset_56_ir_out, 

135 
__AltitudeControl_1, 

136 
__AltitudeControl_10, 

137 
__AltitudeControl_2, 

138 
__AltitudeControl_3, 

139 
__AltitudeControl_4, 

140 
__AltitudeControl_5, 

141 
__AltitudeControl_6, 

142 
__AltitudeControl_8, 

143 
__AltitudeControl_9, 

144 
k_Out1_585, 

145 
kts2fps_Out1_594, 

146 
r2d_Out1_603); 

147 
assigns *altgammacmd_In1_661, *self, Abs_Out1_144, Kh_Out1_193, 

148 
Logical_Operator_In1_197, Logical_Operator_Out1_198, 

149 
Saturation_115_enforce_lo_lim, Saturation_115_s_out, Sum3_Out1_296, 

150 
Sum_Out1_286, Switch1_In2_312, Switch1_Out1_314, Switch_In2_303, 

151 
Switch_Out1_305, VariableLimitSaturation_144_enforce_lo_lim, 

152 
VariableLimitSaturation_144_out, 

153 
VariableRateLimit_139_Gain1_Out1_382, 

154 
VariableRateLimit_139_Gain_Out1_373, 

155 
VariableRateLimit_139_Integrator1_Out1_391, 

156 
VariableRateLimit_139_Sum2_Out1_401, 

157 
VariableRateLimit_139_VariableLimitSaturation_69_enforce_lo_lim, 

158 
VariableRateLimit_139_VariableLimitSaturation_69_out, 

159 
VariableRateLimit_139_integrator_reset_56_ir_out, 

160 
__AltitudeControl_1, __AltitudeControl_10, __AltitudeControl_2, 

161 
__AltitudeControl_3, __AltitudeControl_4, __AltitudeControl_5, 

162 
__AltitudeControl_6, __AltitudeControl_8, __AltitudeControl_9, 

163 
k_Out1_585, kts2fps_Out1_594, r2d_Out1_603; 

164 
*/ 

165 
{ 

166 


167 
/*@ensures \exists real Kh_Out1_193; 

168 
\exists _Bool Logical_Operator_In1_197; 

169 
\exists _Bool Logical_Operator_Out1_198; 

170 
\exists real Saturation_115_enforce_lo_lim; 

171 
\exists real Saturation_115_s_out; 

172 
\exists real Sum3_Out1_296; 

173 
\exists real Sum_Out1_286; 

174 
\exists _Bool Switch1_In2_312; 

175 
\exists real Switch1_Out1_314; 

176 
\exists _Bool Switch_In2_303; 

177 
\exists real Switch_Out1_305; 

178 
\exists real VariableLimitSaturation_144_enforce_lo_lim; 

179 
\exists real VariableLimitSaturation_144_out; 

180 
\exists real VariableRateLimit_139_Gain1_Out1_382; 

181 
\exists real VariableRateLimit_139_Gain_Out1_373; 

182 
\exists real VariableRateLimit_139_Integrator1_Out1_391; 

183 
\exists real VariableRateLimit_139_Sum2_Out1_401; 

184 
\exists real VariableRateLimit_139_VariableLimitSaturation_69_enforce_lo_lim; 

185 
\exists real VariableRateLimit_139_VariableLimitSaturation_69_out; 

186 
\exists real VariableRateLimit_139_integrator_reset_56_ir_out; 

187 
\exists _Bool __AltitudeControl_1; 

188 
\exists _Bool __AltitudeControl_10; 

189 
\exists _Bool __AltitudeControl_2; 

190 
\exists _Bool __AltitudeControl_3; 

191 
\exists _Bool __AltitudeControl_4; 

192 
\exists _Bool __AltitudeControl_5; 

193 
\exists _Bool __AltitudeControl_6; 

194 
\exists _Bool __AltitudeControl_8; 

195 
\exists _Bool __AltitudeControl_9; 

196 
\exists real k_Out1_585; 

197 
\exists real kts2fps_Out1_594; 

198 
\exists real r2d_Out1_603; 

199 
trans_AltitudeControl(AntEng_Out1_19, 

200 
AltCmd_Out1_29, 

201 
Alt_Out1_39, 

202 
GsKts_Out1_49, 

203 
hdot_Out1_59, 

204 
hdotChgRate_Out1_69, 

205 
*altgammacmd_In1_661, 

206 
\at(*self, Pre), 

207 
\at(*self, Here), 

208 
Abs_Out1_144, 

209 
Kh_Out1_193, 

210 
Logical_Operator_In1_197, 

211 
Logical_Operator_Out1_198, 

212 
Saturation_115_enforce_lo_lim, 

213 
Saturation_115_s_out, 

214 
Sum3_Out1_296, 

215 
Sum_Out1_286, 

216 
Switch1_In2_312, 

217 
Switch1_Out1_314, 

218 
Switch_In2_303, 

219 
Switch_Out1_305, 

220 
VariableLimitSaturation_144_enforce_lo_lim, 

221 
VariableLimitSaturation_144_out, 

222 
VariableRateLimit_139_Gain1_Out1_382, 

223 
VariableRateLimit_139_Gain_Out1_373, 

224 
VariableRateLimit_139_Integrator1_Out1_391, 

225 
VariableRateLimit_139_Sum2_Out1_401, 

226 
VariableRateLimit_139_VariableLimitSaturation_69_enforce_lo_lim, 

227 
VariableRateLimit_139_VariableLimitSaturation_69_out, 

228 
VariableRateLimit_139_integrator_reset_56_ir_out, 

229 
__AltitudeControl_1, 

230 
__AltitudeControl_10, 

231 
__AltitudeControl_2, 

232 
__AltitudeControl_3, 

233 
__AltitudeControl_4, 

234 
__AltitudeControl_5, 

235 
__AltitudeControl_6, 

236 
__AltitudeControl_8, 

237 
__AltitudeControl_9, 

238 
k_Out1_585, 

239 
kts2fps_Out1_594, 

240 
r2d_Out1_603); 

241 
assigns *altgammacmd_In1_661, *self, Abs_Out1_144, Kh_Out1_193, 

242 
Logical_Operator_In1_197, Logical_Operator_Out1_198, 

243 
Saturation_115_enforce_lo_lim, Saturation_115_s_out, Sum3_Out1_296, 

244 
Sum_Out1_286, Switch1_In2_312, Switch1_Out1_314, Switch_In2_303, 

245 
Switch_Out1_305, VariableLimitSaturation_144_enforce_lo_lim, 

246 
VariableLimitSaturation_144_out, 

247 
VariableRateLimit_139_Gain1_Out1_382, 

248 
VariableRateLimit_139_Gain_Out1_373, 

249 
VariableRateLimit_139_Integrator1_Out1_391, 

250 
VariableRateLimit_139_Sum2_Out1_401, 

251 
VariableRateLimit_139_VariableLimitSaturation_69_enforce_lo_lim, 

252 
VariableRateLimit_139_VariableLimitSaturation_69_out, 

253 
VariableRateLimit_139_integrator_reset_56_ir_out, 

254 
__AltitudeControl_1, __AltitudeControl_10, __AltitudeControl_2, 

255 
__AltitudeControl_3, __AltitudeControl_4, __AltitudeControl_5, 

256 
__AltitudeControl_6, __AltitudeControl_8, __AltitudeControl_9, 

257 
k_Out1_585, kts2fps_Out1_594, r2d_Out1_603; 

258 
*/ 

259 
{ 

260 


261 
/*@ensures \exists _Bool Logical_Operator_In1_197; 

262 
\exists _Bool Logical_Operator_Out1_198; 

263 
\exists real Saturation_115_enforce_lo_lim; 

264 
\exists real Saturation_115_s_out; 

265 
\exists real Sum3_Out1_296; 

266 
\exists real Sum_Out1_286; 

267 
\exists _Bool Switch1_In2_312; 

268 
\exists real Switch1_Out1_314; 

269 
\exists _Bool Switch_In2_303; 

270 
\exists real Switch_Out1_305; 

271 
\exists real VariableLimitSaturation_144_enforce_lo_lim; 

272 
\exists real VariableLimitSaturation_144_out; 

273 
\exists real VariableRateLimit_139_Gain1_Out1_382; 

274 
\exists real VariableRateLimit_139_Gain_Out1_373; 

275 
\exists real VariableRateLimit_139_Integrator1_Out1_391; 

276 
\exists real VariableRateLimit_139_Sum2_Out1_401; 

277 
\exists real VariableRateLimit_139_VariableLimitSaturation_69_enforce_lo_lim; 

278 
\exists real VariableRateLimit_139_VariableLimitSaturation_69_out; 

279 
\exists real VariableRateLimit_139_integrator_reset_56_ir_out; 

280 
\exists _Bool __AltitudeControl_1; 

281 
\exists _Bool __AltitudeControl_10; 

282 
\exists _Bool __AltitudeControl_2; 

283 
\exists _Bool __AltitudeControl_3; 

284 
\exists _Bool __AltitudeControl_4; 

285 
\exists _Bool __AltitudeControl_5; 

286 
\exists _Bool __AltitudeControl_6; 

287 
\exists _Bool __AltitudeControl_8; 

288 
\exists _Bool __AltitudeControl_9; 

289 
\exists real k_Out1_585; 

290 
\exists real kts2fps_Out1_594; 

291 
\exists real r2d_Out1_603; 

292 
trans_AltitudeControl(AntEng_Out1_19, 

293 
AltCmd_Out1_29, 

294 
Alt_Out1_39, 

295 
GsKts_Out1_49, 

296 
hdot_Out1_59, 

297 
hdotChgRate_Out1_69, 

298 
*altgammacmd_In1_661, 

299 
\at(*self, Pre), 

300 
\at(*self, Here), 

301 
Abs_Out1_144, 

302 
Kh_Out1_193, 

303 
Logical_Operator_In1_197, 

304 
Logical_Operator_Out1_198, 

305 
Saturation_115_enforce_lo_lim, 

306 
Saturation_115_s_out, 

307 
Sum3_Out1_296, 

308 
Sum_Out1_286, 

309 
Switch1_In2_312, 

310 
Switch1_Out1_314, 

311 
Switch_In2_303, 

312 
Switch_Out1_305, 

313 
VariableLimitSaturation_144_enforce_lo_lim, 

314 
VariableLimitSaturation_144_out, 

315 
VariableRateLimit_139_Gain1_Out1_382, 

316 
VariableRateLimit_139_Gain_Out1_373, 

317 
VariableRateLimit_139_Integrator1_Out1_391, 

318 
VariableRateLimit_139_Sum2_Out1_401, 

319 
VariableRateLimit_139_VariableLimitSaturation_69_enforce_lo_lim, 

320 
VariableRateLimit_139_VariableLimitSaturation_69_out, 

321 
VariableRateLimit_139_integrator_reset_56_ir_out, 

322 
__AltitudeControl_1, 

323 
__AltitudeControl_10, 

324 
__AltitudeControl_2, 

325 
__AltitudeControl_3, 

326 
__AltitudeControl_4, 

327 
__AltitudeControl_5, 

328 
__AltitudeControl_6, 

329 
__AltitudeControl_8, 

330 
__AltitudeControl_9, 

331 
k_Out1_585, 

332 
kts2fps_Out1_594, 

333 
r2d_Out1_603); 

334 
assigns *altgammacmd_In1_661, *self, Abs_Out1_144, Kh_Out1_193, 

335 
Logical_Operator_In1_197, Logical_Operator_Out1_198, 

336 
Saturation_115_enforce_lo_lim, Saturation_115_s_out, Sum3_Out1_296, 

337 
Sum_Out1_286, Switch1_In2_312, Switch1_Out1_314, Switch_In2_303, 

338 
Switch_Out1_305, VariableLimitSaturation_144_enforce_lo_lim, 

339 
VariableLimitSaturation_144_out, 

340 
VariableRateLimit_139_Gain1_Out1_382, 

341 
VariableRateLimit_139_Gain_Out1_373, 

342 
VariableRateLimit_139_Integrator1_Out1_391, 

343 
VariableRateLimit_139_Sum2_Out1_401, 

344 
VariableRateLimit_139_VariableLimitSaturation_69_enforce_lo_lim, 

345 
VariableRateLimit_139_VariableLimitSaturation_69_out, 

346 
VariableRateLimit_139_integrator_reset_56_ir_out, 

347 
__AltitudeControl_1, __AltitudeControl_10, __AltitudeControl_2, 

348 
__AltitudeControl_3, __AltitudeControl_4, __AltitudeControl_5, 

349 
__AltitudeControl_6, __AltitudeControl_8, __AltitudeControl_9, 

350 
k_Out1_585, kts2fps_Out1_594, r2d_Out1_603; 

351 
*/ 

352 
{ 

353 


354 
/*@ensures \exists _Bool Logical_Operator_Out1_198; 

355 
\exists real Saturation_115_enforce_lo_lim; 

356 
\exists real Saturation_115_s_out; 

357 
\exists real Sum3_Out1_296; 

358 
\exists real Sum_Out1_286; 

359 
\exists _Bool Switch1_In2_312; 

360 
\exists real Switch1_Out1_314; 

361 
\exists _Bool Switch_In2_303; 

362 
\exists real Switch_Out1_305; 

363 
\exists real VariableLimitSaturation_144_enforce_lo_lim; 

364 
\exists real VariableLimitSaturation_144_out; 

365 
\exists real VariableRateLimit_139_Gain1_Out1_382; 

366 
\exists real VariableRateLimit_139_Gain_Out1_373; 

367 
\exists real VariableRateLimit_139_Integrator1_Out1_391; 

368 
\exists real VariableRateLimit_139_Sum2_Out1_401; 

369 
\exists real VariableRateLimit_139_VariableLimitSaturation_69_enforce_lo_lim; 

370 
\exists real VariableRateLimit_139_VariableLimitSaturation_69_out; 

371 
\exists real VariableRateLimit_139_integrator_reset_56_ir_out; 

372 
\exists _Bool __AltitudeControl_1; 

373 
\exists _Bool __AltitudeControl_10; 

374 
\exists _Bool __AltitudeControl_2; 

375 
\exists _Bool __AltitudeControl_3; 

376 
\exists _Bool __AltitudeControl_4; 

377 
\exists _Bool __AltitudeControl_5; 

378 
\exists _Bool __AltitudeControl_6; 

379 
\exists _Bool __AltitudeControl_8; 

380 
\exists _Bool __AltitudeControl_9; 

381 
\exists real k_Out1_585; 

382 
\exists real kts2fps_Out1_594; 

383 
\exists real r2d_Out1_603; 

384 
trans_AltitudeControl(AntEng_Out1_19, 

385 
AltCmd_Out1_29, 

386 
Alt_Out1_39, 

387 
GsKts_Out1_49, 

388 
hdot_Out1_59, 

389 
hdotChgRate_Out1_69, 

390 
*altgammacmd_In1_661, 

391 
\at(*self, Pre), 

392 
\at(*self, Here), 

393 
Abs_Out1_144, 

394 
Kh_Out1_193, 

395 
Logical_Operator_In1_197, 

396 
Logical_Operator_Out1_198, 

397 
Saturation_115_enforce_lo_lim, 

398 
Saturation_115_s_out, 

399 
Sum3_Out1_296, 

400 
Sum_Out1_286, 

401 
Switch1_In2_312, 

402 
Switch1_Out1_314, 

403 
Switch_In2_303, 

404 
Switch_Out1_305, 

405 
VariableLimitSaturation_144_enforce_lo_lim, 

406 
VariableLimitSaturation_144_out, 

407 
VariableRateLimit_139_Gain1_Out1_382, 

408 
VariableRateLimit_139_Gain_Out1_373, 

409 
VariableRateLimit_139_Integrator1_Out1_391, 

410 
VariableRateLimit_139_Sum2_Out1_401, 

411 
VariableRateLimit_139_VariableLimitSaturation_69_enforce_lo_lim, 

412 
VariableRateLimit_139_VariableLimitSaturation_69_out, 

413 
VariableRateLimit_139_integrator_reset_56_ir_out, 

414 
__AltitudeControl_1, 

415 
__AltitudeControl_10, 

416 
__AltitudeControl_2, 

417 
__AltitudeControl_3, 

418 
__AltitudeControl_4, 

419 
__AltitudeControl_5, 

420 
__AltitudeControl_6, 

421 
__AltitudeControl_8, 

422 
__AltitudeControl_9, 

423 
k_Out1_585, 

424 
kts2fps_Out1_594, 

425 
r2d_Out1_603); 

426 
assigns *altgammacmd_In1_661, *self, Abs_Out1_144, Kh_Out1_193, 

427 
Logical_Operator_In1_197, Logical_Operator_Out1_198, 

428 
Saturation_115_enforce_lo_lim, Saturation_115_s_out, Sum3_Out1_296, 

429 
Sum_Out1_286, Switch1_In2_312, Switch1_Out1_314, Switch_In2_303, 

430 
Switch_Out1_305, VariableLimitSaturation_144_enforce_lo_lim, 

431 
VariableLimitSaturation_144_out, 

432 
VariableRateLimit_139_Gain1_Out1_382, 

433 
VariableRateLimit_139_Gain_Out1_373, 

434 
VariableRateLimit_139_Integrator1_Out1_391, 

435 
VariableRateLimit_139_Sum2_Out1_401, 

436 
VariableRateLimit_139_VariableLimitSaturation_69_enforce_lo_lim, 

437 
VariableRateLimit_139_VariableLimitSaturation_69_out, 

438 
VariableRateLimit_139_integrator_reset_56_ir_out, 

439 
__AltitudeControl_1, __AltitudeControl_10, __AltitudeControl_2, 

440 
__AltitudeControl_3, __AltitudeControl_4, __AltitudeControl_5, 

441 
__AltitudeControl_6, __AltitudeControl_8, __AltitudeControl_9, 

442 
k_Out1_585, kts2fps_Out1_594, r2d_Out1_603; 

443 
*/ 

444 
{ 

445 


446 
/*@ensures \exists real Saturation_115_enforce_lo_lim; 

447 
\exists real Saturation_115_s_out; 

448 
\exists real Sum3_Out1_296; 

449 
\exists real Sum_Out1_286; 

450 
\exists _Bool Switch1_In2_312; 

451 
\exists real Switch1_Out1_314; 

452 
\exists _Bool Switch_In2_303; 

453 
\exists real Switch_Out1_305; 

454 
\exists real VariableLimitSaturation_144_enforce_lo_lim; 

455 
\exists real VariableLimitSaturation_144_out; 

456 
\exists real VariableRateLimit_139_Gain1_Out1_382; 

457 
\exists real VariableRateLimit_139_Gain_Out1_373; 

458 
\exists real VariableRateLimit_139_Integrator1_Out1_391; 

459 
\exists real VariableRateLimit_139_Sum2_Out1_401; 

460 
\exists real VariableRateLimit_139_VariableLimitSaturation_69_enforce_lo_lim; 

461 
\exists real VariableRateLimit_139_VariableLimitSaturation_69_out; 

462 
\exists real VariableRateLimit_139_integrator_reset_56_ir_out; 

463 
\exists _Bool __AltitudeControl_1; 

464 
\exists _Bool __AltitudeControl_10; 

465 
\exists _Bool __AltitudeControl_2; 

466 
\exists _Bool __AltitudeControl_3; 

467 
\exists _Bool __AltitudeControl_4; 

468 
\exists _Bool __AltitudeControl_5; 

469 
\exists _Bool __AltitudeControl_6; 

470 
\exists _Bool __AltitudeControl_8; 

471 
\exists _Bool __AltitudeControl_9; 

472 
\exists real k_Out1_585; 

473 
\exists real kts2fps_Out1_594; 

474 
\exists real r2d_Out1_603; 

475 
trans_AltitudeControl(AntEng_Out1_19, 

476 
AltCmd_Out1_29, 

477 
Alt_Out1_39, 

478 
GsKts_Out1_49, 

479 
hdot_Out1_59, 

480 
hdotChgRate_Out1_69, 

481 
*altgammacmd_In1_661, 

482 
\at(*self, Pre), 

483 
\at(*self, Here), 

484 
Abs_Out1_144, 

485 
Kh_Out1_193, 

486 
Logical_Operator_In1_197, 

487 
Logical_Operator_Out1_198, 

488 
Saturation_115_enforce_lo_lim, 

489 
Saturation_115_s_out, 

490 
Sum3_Out1_296, 

491 
Sum_Out1_286, 

492 
Switch1_In2_312, 

493 
Switch1_Out1_314, 

494 
Switch_In2_303, 

495 
Switch_Out1_305, 

496 
VariableLimitSaturation_144_enforce_lo_lim, 

497 
VariableLimitSaturation_144_out, 

498 
VariableRateLimit_139_Gain1_Out1_382, 

499 
VariableRateLimit_139_Gain_Out1_373, 

500 
VariableRateLimit_139_Integrator1_Out1_391, 

501 
VariableRateLimit_139_Sum2_Out1_401, 

502 
VariableRateLimit_139_VariableLimitSaturation_69_enforce_lo_lim, 

503 
VariableRateLimit_139_VariableLimitSaturation_69_out, 

504 
VariableRateLimit_139_integrator_reset_56_ir_out, 

505 
__AltitudeControl_1, 

506 
__AltitudeControl_10, 

507 
__AltitudeControl_2, 

508 
__AltitudeControl_3, 

509 
__AltitudeControl_4, 

510 
__AltitudeControl_5, 

511 
__AltitudeControl_6, 

512 
__AltitudeControl_8, 

513 
__AltitudeControl_9, 

514 
k_Out1_585, 

515 
kts2fps_Out1_594, 

516 
r2d_Out1_603); 

517 
assigns *altgammacmd_In1_661, *self, Abs_Out1_144, Kh_Out1_193, 

518 
Logical_Operator_In1_197, Logical_Operator_Out1_198, 

519 
Saturation_115_enforce_lo_lim, Saturation_115_s_out, Sum3_Out1_296, 

520 
Sum_Out1_286, Switch1_In2_312, Switch1_Out1_314, Switch_In2_303, 

521 
Switch_Out1_305, VariableLimitSaturation_144_enforce_lo_lim, 

522 
VariableLimitSaturation_144_out, 

523 
VariableRateLimit_139_Gain1_Out1_382, 

524 
VariableRateLimit_139_Gain_Out1_373, 

525 
VariableRateLimit_139_Integrator1_Out1_391, 

526 
VariableRateLimit_139_Sum2_Out1_401, 

527 
VariableRateLimit_139_VariableLimitSaturation_69_enforce_lo_lim, 

528 
VariableRateLimit_139_VariableLimitSaturation_69_out, 

529 
VariableRateLimit_139_integrator_reset_56_ir_out, 

530 
__AltitudeControl_1, __AltitudeControl_10, __AltitudeControl_2, 

531 
__AltitudeControl_3, __AltitudeControl_4, __AltitudeControl_5, 

532 
__AltitudeControl_6, __AltitudeControl_8, __AltitudeControl_9, 

533 
k_Out1_585, kts2fps_Out1_594, r2d_Out1_603; 

534 
*/ 

535 
{ 

536 


537 
/*@ensures \exists real Saturation_115_s_out; 

538 
\exists real Sum3_Out1_296; 

539 
\exists real Sum_Out1_286; 

540 
\exists _Bool Switch1_In2_312; 

541 
\exists real Switch1_Out1_314; 

542 
\exists _Bool Switch_In2_303; 

543 
\exists real Switch_Out1_305; 

544 
\exists real VariableLimitSaturation_144_enforce_lo_lim; 

545 
\exists real VariableLimitSaturation_144_out; 

546 
\exists real VariableRateLimit_139_Gain1_Out1_382; 

547 
\exists real VariableRateLimit_139_Gain_Out1_373; 

548 
\exists real VariableRateLimit_139_Integrator1_Out1_391; 

549 
\exists real VariableRateLimit_139_Sum2_Out1_401; 

550 
\exists real VariableRateLimit_139_VariableLimitSaturation_69_enforce_lo_lim; 

551 
\exists real VariableRateLimit_139_VariableLimitSaturation_69_out; 

552 
\exists real VariableRateLimit_139_integrator_reset_56_ir_out; 

553 
\exists _Bool __AltitudeControl_1; 

554 
\exists _Bool __AltitudeControl_10; 

555 
\exists _Bool __AltitudeControl_2; 

556 
\exists _Bool __AltitudeControl_3; 

557 
\exists _Bool __AltitudeControl_4; 

558 
\exists _Bool __AltitudeControl_5; 

559 
\exists _Bool __AltitudeControl_6; 

560 
\exists _Bool __AltitudeControl_8; 

561 
\exists _Bool __AltitudeControl_9; 

562 
\exists real k_Out1_585; 

563 
\exists real kts2fps_Out1_594; 

564 
\exists real r2d_Out1_603; 

565 
trans_AltitudeControl(AntEng_Out1_19, 

566 
AltCmd_Out1_29, 

567 
Alt_Out1_39, 

568 
GsKts_Out1_49, 

569 
hdot_Out1_59, 

570 
hdotChgRate_Out1_69, 

571 
*altgammacmd_In1_661, 

572 
\at(*self, Pre), 

573 
\at(*self, Here), 

574 
Abs_Out1_144, 

575 
Kh_Out1_193, 

576 
Logical_Operator_In1_197, 

577 
Logical_Operator_Out1_198, 

578 
Saturation_115_enforce_lo_lim, 

579 
Saturation_115_s_out, 

580 
Sum3_Out1_296, 

581 
Sum_Out1_286, 

582 
Switch1_In2_312, 

583 
Switch1_Out1_314, 

584 
Switch_In2_303, 

585 
Switch_Out1_305, 

586 
VariableLimitSaturation_144_enforce_lo_lim, 

587 
VariableLimitSaturation_144_out, 

588 
VariableRateLimit_139_Gain1_Out1_382, 

589 
VariableRateLimit_139_Gain_Out1_373, 

590 
VariableRateLimit_139_Integrator1_Out1_391, 

591 
VariableRateLimit_139_Sum2_Out1_401, 

592 
VariableRateLimit_139_VariableLimitSaturation_69_enforce_lo_lim, 

593 
VariableRateLimit_139_VariableLimitSaturation_69_out, 

594 
VariableRateLimit_139_integrator_reset_56_ir_out, 

595 
__AltitudeControl_1, 

596 
__AltitudeControl_10, 

597 
__AltitudeControl_2, 

598 
__AltitudeControl_3, 

599 
__AltitudeControl_4, 

600 
__AltitudeControl_5, 

601 
__AltitudeControl_6, 

602 
__AltitudeControl_8, 

603 
__AltitudeControl_9, 

604 
k_Out1_585, 

605 
kts2fps_Out1_594, 

606 
r2d_Out1_603); 

607 
assigns *altgammacmd_In1_661, *self, Abs_Out1_144, Kh_Out1_193, 

608 
Logical_Operator_In1_197, Logical_Operator_Out1_198, 

609 
Saturation_115_enforce_lo_lim, Saturation_115_s_out, Sum3_Out1_296, 

610 
Sum_Out1_286, Switch1_In2_312, Switch1_Out1_314, Switch_In2_303, 

611 
Switch_Out1_305, VariableLimitSaturation_144_enforce_lo_lim, 

612 
VariableLimitSaturation_144_out, 

613 
VariableRateLimit_139_Gain1_Out1_382, 

614 
VariableRateLimit_139_Gain_Out1_373, 

615 
VariableRateLimit_139_Integrator1_Out1_391, 

616 
VariableRateLimit_139_Sum2_Out1_401, 

617 
VariableRateLimit_139_VariableLimitSaturation_69_enforce_lo_lim, 

618 
VariableRateLimit_139_VariableLimitSaturation_69_out, 

619 
VariableRateLimit_139_integrator_reset_56_ir_out, 

620 
__AltitudeControl_1, __AltitudeControl_10, __AltitudeControl_2, 

621 
__AltitudeControl_3, __AltitudeControl_4, __AltitudeControl_5, 

622 
__AltitudeControl_6, __AltitudeControl_8, __AltitudeControl_9, 

623 
k_Out1_585, kts2fps_Out1_594, r2d_Out1_603; 

624 
*/ 

625 
{ 

626 


627 
/*@ensures \exists real Sum3_Out1_296; 

628 
\exists real Sum_Out1_286; 

629 
\exists _Bool Switch1_In2_312; 

630 
\exists real Switch1_Out1_314; 

631 
\exists _Bool Switch_In2_303; 

632 
\exists real Switch_Out1_305; 

633 
\exists real VariableLimitSaturation_144_enforce_lo_lim; 

634 
\exists real VariableLimitSaturation_144_out; 

635 
\exists real VariableRateLimit_139_Gain1_Out1_382; 

636 
\exists real VariableRateLimit_139_Gain_Out1_373; 

637 
\exists real VariableRateLimit_139_Integrator1_Out1_391; 

638 
\exists real VariableRateLimit_139_Sum2_Out1_401; 

639 
\exists real VariableRateLimit_139_VariableLimitSaturation_69_enforce_lo_lim; 

640 
\exists real VariableRateLimit_139_VariableLimitSaturation_69_out; 

641 
\exists real VariableRateLimit_139_integrator_reset_56_ir_out; 

642 
\exists _Bool __AltitudeControl_1; 

643 
\exists _Bool __AltitudeControl_10; 

644 
\exists _Bool __AltitudeControl_2; 

645 
\exists _Bool __AltitudeControl_3; 

646 
\exists _Bool __AltitudeControl_4; 

647 
\exists _Bool __AltitudeControl_5; 

648 
\exists _Bool __AltitudeControl_6; 

649 
\exists _Bool __AltitudeControl_8; 

650 
\exists _Bool __AltitudeControl_9; 

651 
\exists real k_Out1_585; 

652 
\exists real kts2fps_Out1_594; 

653 
\exists real r2d_Out1_603; 

654 
trans_AltitudeControl(AntEng_Out1_19, 

655 
AltCmd_Out1_29, 

656 
Alt_Out1_39, 

657 
GsKts_Out1_49, 

658 
hdot_Out1_59, 

659 
hdotChgRate_Out1_69, 

660 
*altgammacmd_In1_661, 

661 
\at(*self, Pre), 

662 
\at(*self, Here), 

663 
Abs_Out1_144, 

664 
Kh_Out1_193, 

665 
Logical_Operator_In1_197, 

666 
Logical_Operator_Out1_198, 

667 
Saturation_115_enforce_lo_lim, 

668 
Saturation_115_s_out, 

669 
Sum3_Out1_296, 

670 
Sum_Out1_286, 

671 
Switch1_In2_312, 

672 
Switch1_Out1_314, 

673 
Switch_In2_303, 

674 
Switch_Out1_305, 

675 
VariableLimitSaturation_144_enforce_lo_lim, 

676 
VariableLimitSaturation_144_out, 

677 
VariableRateLimit_139_Gain1_Out1_382, 

678 
VariableRateLimit_139_Gain_Out1_373, 

679 
VariableRateLimit_139_Integrator1_Out1_391, 

680 
VariableRateLimit_139_Sum2_Out1_401, 

681 
VariableRateLimit_139_VariableLimitSaturation_69_enforce_lo_lim, 

682 
VariableRateLimit_139_VariableLimitSaturation_69_out, 

683 
VariableRateLimit_139_integrator_reset_56_ir_out, 

684 
__AltitudeControl_1, 

685 
__AltitudeControl_10, 

686 
__AltitudeControl_2, 

687 
__AltitudeControl_3, 

688 
__AltitudeControl_4, 

689 
__AltitudeControl_5, 

690 
__AltitudeControl_6, 

691 
__AltitudeControl_8, 

692 
__AltitudeControl_9, 

693 
k_Out1_585, 

694 
kts2fps_Out1_594, 

695 
r2d_Out1_603); 

696 
assigns *altgammacmd_In1_661, *self, Abs_Out1_144, Kh_Out1_193, 

697 
Logical_Operator_In1_197, Logical_Operator_Out1_198, 

698 
Saturation_115_enforce_lo_lim, Saturation_115_s_out, Sum3_Out1_296, 

699 
Sum_Out1_286, Switch1_In2_312, Switch1_Out1_314, Switch_In2_303, 

700 
Switch_Out1_305, VariableLimitSaturation_144_enforce_lo_lim, 

701 
VariableLimitSaturation_144_out, 

702 
VariableRateLimit_139_Gain1_Out1_382, 

703 
VariableRateLimit_139_Gain_Out1_373, 

704 
VariableRateLimit_139_Integrator1_Out1_391, 

705 
VariableRateLimit_139_Sum2_Out1_401, 

706 
VariableRateLimit_139_VariableLimitSaturation_69_enforce_lo_lim, 

707 
VariableRateLimit_139_VariableLimitSaturation_69_out, 

708 
VariableRateLimit_139_integrator_reset_56_ir_out, 

709 
__AltitudeControl_1, __AltitudeControl_10, __AltitudeControl_2, 

710 
__AltitudeControl_3, __AltitudeControl_4, __AltitudeControl_5, 

711 
__AltitudeControl_6, __AltitudeControl_8, __AltitudeControl_9, 

712 
k_Out1_585, kts2fps_Out1_594, r2d_Out1_603; 

713 
*/ 

714 
{ 

715 


716 
/*@ensures \exists real Sum_Out1_286; 

717 
\exists _Bool Switch1_In2_312; 

718 
\exists real Switch1_Out1_314; 

719 
\exists _Bool Switch_In2_303; 

720 
\exists real Switch_Out1_305; 

721 
\exists real VariableLimitSaturation_144_enforce_lo_lim; 

722 
\exists real VariableLimitSaturation_144_out; 

723 
\exists real VariableRateLimit_139_Gain1_Out1_382; 

724 
\exists real VariableRateLimit_139_Gain_Out1_373; 

725 
\exists real VariableRateLimit_139_Integrator1_Out1_391; 

726 
\exists real VariableRateLimit_139_Sum2_Out1_401; 

727 
\exists real VariableRateLimit_139_VariableLimitSaturation_69_enforce_lo_lim; 

728 
\exists real VariableRateLimit_139_VariableLimitSaturation_69_out; 

729 
\exists real VariableRateLimit_139_integrator_reset_56_ir_out; 

730 
\exists _Bool __AltitudeControl_1; 

731 
\exists _Bool __AltitudeControl_10; 

732 
\exists _Bool __AltitudeControl_2; 

733 
\exists _Bool __AltitudeControl_3; 

734 
\exists _Bool __AltitudeControl_4; 

735 
\exists _Bool __AltitudeControl_5; 

736 
\exists _Bool __AltitudeControl_6; 

737 
\exists _Bool __AltitudeControl_8; 

738 
\exists _Bool __AltitudeControl_9; 

739 
\exists real k_Out1_585; 

740 
\exists real kts2fps_Out1_594; 

741 
\exists real r2d_Out1_603; 

742 
trans_AltitudeControl(AntEng_Out1_19, 

743 
AltCmd_Out1_29, 

744 
Alt_Out1_39, 

745 
GsKts_Out1_49, 

746 
hdot_Out1_59, 

747 
hdotChgRate_Out1_69, 

748 
*altgammacmd_In1_661, 

749 
\at(*self, Pre), 

750 
\at(*self, Here), 

751 
Abs_Out1_144, 

752 
Kh_Out1_193, 

753 
Logical_Operator_In1_197, 

754 
Logical_Operator_Out1_198, 

755 
Saturation_115_enforce_lo_lim, 

756 
Saturation_115_s_out, 

757 
Sum3_Out1_296, 

758 
Sum_Out1_286, 

759 
Switch1_In2_312, 

760 
Switch1_Out1_314, 

761 
Switch_In2_303, 

762 
Switch_Out1_305, 

763 
VariableLimitSaturation_144_enforce_lo_lim, 

764 
VariableLimitSaturation_144_out, 

765 
VariableRateLimit_139_Gain1_Out1_382, 

766 
VariableRateLimit_139_Gain_Out1_373, 

767 
VariableRateLimit_139_Integrator1_Out1_391, 

768 
VariableRateLimit_139_Sum2_Out1_401, 

769 
VariableRateLimit_139_VariableLimitSaturation_69_enforce_lo_lim, 

770 
VariableRateLimit_139_VariableLimitSaturation_69_out, 

771 
VariableRateLimit_139_integrator_reset_56_ir_out, 

772 
__AltitudeControl_1, 

773 
__AltitudeControl_10, 

774 
__AltitudeControl_2, 

775 
__AltitudeControl_3, 

776 
__AltitudeControl_4, 

777 
__AltitudeControl_5, 

778 
__AltitudeControl_6, 

779 
__AltitudeControl_8, 

780 
__AltitudeControl_9, 

781 
k_Out1_585, 

782 
kts2fps_Out1_594, 

783 
r2d_Out1_603); 

784 
assigns *altgammacmd_In1_661, *self, Abs_Out1_144, Kh_Out1_193, 

785 
Logical_Operator_In1_197, Logical_Operator_Out1_198, 

786 
Saturation_115_enforce_lo_lim, Saturation_115_s_out, Sum3_Out1_296, 

787 
Sum_Out1_286, Switch1_In2_312, Switch1_Out1_314, Switch_In2_303, 

788 
Switch_Out1_305, VariableLimitSaturation_144_enforce_lo_lim, 

789 
VariableLimitSaturation_144_out, 

790 
VariableRateLimit_139_Gain1_Out1_382, 

791 
VariableRateLimit_139_Gain_Out1_373, 

792 
VariableRateLimit_139_Integrator1_Out1_391, 

793 
VariableRateLimit_139_Sum2_Out1_401, 

794 
VariableRateLimit_139_VariableLimitSaturation_69_enforce_lo_lim, 

795 
VariableRateLimit_139_VariableLimitSaturation_69_out, 

796 
VariableRateLimit_139_integrator_reset_56_ir_out, 

797 
__AltitudeControl_1, __AltitudeControl_10, __AltitudeControl_2, 

798 
__AltitudeControl_3, __AltitudeControl_4, __AltitudeControl_5, 

799 
__AltitudeControl_6, __AltitudeControl_8, __AltitudeControl_9, 

800 
k_Out1_585, kts2fps_Out1_594, r2d_Out1_603; 

801 
*/ 

802 
{ 

803 


804 
/*@ensures \exists _Bool Switch1_In2_312; 

805 
\exists real Switch1_Out1_314; 

806 
\exists _Bool Switch_In2_303; 

807 
\exists real Switch_Out1_305; 

808 
\exists real VariableLimitSaturation_144_enforce_lo_lim; 

809 
\exists real VariableLimitSaturation_144_out; 

810 
\exists real VariableRateLimit_139_Gain1_Out1_382; 

811 
\exists real VariableRateLimit_139_Gain_Out1_373; 

812 
\exists real VariableRateLimit_139_Integrator1_Out1_391; 

813 
\exists real VariableRateLimit_139_Sum2_Out1_401; 

814 
\exists real VariableRateLimit_139_VariableLimitSaturation_69_enforce_lo_lim; 

815 
\exists real VariableRateLimit_139_VariableLimitSaturation_69_out; 

816 
\exists real VariableRateLimit_139_integrator_reset_56_ir_out; 

817 
\exists _Bool __AltitudeControl_1; 

818 
\exists _Bool __AltitudeControl_10; 

819 
\exists _Bool __AltitudeControl_2; 

820 
\exists _Bool __AltitudeControl_3; 

821 
\exists _Bool __AltitudeControl_4; 

822 
\exists _Bool __AltitudeControl_5; 

823 
\exists _Bool __AltitudeControl_6; 

824 
\exists _Bool __AltitudeControl_8; 

825 
\exists _Bool __AltitudeControl_9; 

826 
\exists real k_Out1_585; 

827 
\exists real kts2fps_Out1_594; 

828 
\exists real r2d_Out1_603; 

829 
trans_AltitudeControl(AntEng_Out1_19, 

830 
AltCmd_Out1_29, 

831 
Alt_Out1_39, 

832 
GsKts_Out1_49, 

833 
hdot_Out1_59, 

834 
hdotChgRate_Out1_69, 

835 
*altgammacmd_In1_661, 

836 
\at(*self, Pre), 

837 
\at(*self, Here), 

838 
Abs_Out1_144, 

839 
Kh_Out1_193, 

840 
Logical_Operator_In1_197, 

841 
Logical_Operator_Out1_198, 

842 
Saturation_115_enforce_lo_lim, 

843 
Saturation_115_s_out, 

844 
Sum3_Out1_296, 

845 
Sum_Out1_286, 

846 
Switch1_In2_312, 

847 
Switch1_Out1_314, 

848 
Switch_In2_303, 

849 
Switch_Out1_305, 

850 
VariableLimitSaturation_144_enforce_lo_lim, 

851 
VariableLimitSaturation_144_out, 

852 
VariableRateLimit_139_Gain1_Out1_382, 

853 
VariableRateLimit_139_Gain_Out1_373, 

854 
VariableRateLimit_139_Integrator1_Out1_391, 

855 
VariableRateLimit_139_Sum2_Out1_401, 

856 
VariableRateLimit_139_VariableLimitSaturation_69_enforce_lo_lim, 

857 
VariableRateLimit_139_VariableLimitSaturation_69_out, 

858 
VariableRateLimit_139_integrator_reset_56_ir_out, 

859 
__AltitudeControl_1, 

860 
__AltitudeControl_10, 

861 
__AltitudeControl_2, 

862 
__AltitudeControl_3, 

863 
__AltitudeControl_4, 

864 
__AltitudeControl_5, 

865 
__AltitudeControl_6, 

866 
__AltitudeControl_8, 

867 
__AltitudeControl_9, 

868 
k_Out1_585, 

869 
kts2fps_Out1_594, 

870 
r2d_Out1_603); 

871 
assigns *altgammacmd_In1_661, *self, Abs_Out1_144, Kh_Out1_193, 

872 
Logical_Operator_In1_197, Logical_Operator_Out1_198, 

873 
Saturation_115_enforce_lo_lim, Saturation_115_s_out, Sum3_Out1_296, 

874 
Sum_Out1_286, Switch1_In2_312, Switch1_Out1_314, Switch_In2_303, 

875 
Switch_Out1_305, VariableLimitSaturation_144_enforce_lo_lim, 

876 
VariableLimitSaturation_144_out, 

877 
VariableRateLimit_139_Gain1_Out1_382, 

878 
VariableRateLimit_139_Gain_Out1_373, 

879 
VariableRateLimit_139_Integrator1_Out1_391, 

880 
VariableRateLimit_139_Sum2_Out1_401, 

881 
VariableRateLimit_139_VariableLimitSaturation_69_enforce_lo_lim, 

882 
VariableRateLimit_139_VariableLimitSaturation_69_out, 

883 
VariableRateLimit_139_integrator_reset_56_ir_out, 

884 
__AltitudeControl_1, __AltitudeControl_10, __AltitudeControl_2, 

885 
__AltitudeControl_3, __AltitudeControl_4, __AltitudeControl_5, 

886 
__AltitudeControl_6, __AltitudeControl_8, __AltitudeControl_9, 

887 
k_Out1_585, kts2fps_Out1_594, r2d_Out1_603; 

888 
*/ 

889 
{ 

890 


891 
/*@ensures \exists real Switch1_Out1_314; 

892 
\exists _Bool Switch_In2_303; 

893 
\exists real Switch_Out1_305; 

894 
\exists real VariableLimitSaturation_144_enforce_lo_lim; 

895 
\exists real VariableLimitSaturation_144_out; 

896 
\exists real VariableRateLimit_139_Gain1_Out1_382; 

897 
\exists real VariableRateLimit_139_Gain_Out1_373; 

898 
\exists real VariableRateLimit_139_Integrator1_Out1_391; 

899 
\exists real VariableRateLimit_139_Sum2_Out1_401; 

900 
\exists real VariableRateLimit_139_VariableLimitSaturation_69_enforce_lo_lim; 

901 
\exists real VariableRateLimit_139_VariableLimitSaturation_69_out; 

902 
\exists real VariableRateLimit_139_integrator_reset_56_ir_out; 

903 
\exists _Bool __AltitudeControl_1; 

904 
\exists _Bool __AltitudeControl_10; 

905 
\exists _Bool __AltitudeControl_2; 

906 
\exists _Bool __AltitudeControl_3; 

907 
\exists _Bool __AltitudeControl_4; 

908 
\exists _Bool __AltitudeControl_5; 

909 
\exists _Bool __AltitudeControl_6; 

910 
\exists _Bool __AltitudeControl_8; 

911 
\exists _Bool __AltitudeControl_9; 

912 
\exists real k_Out1_585; 

913 
\exists real kts2fps_Out1_594; 

914 
\exists real r2d_Out1_603; 

915 
trans_AltitudeControl(AntEng_Out1_19, 

916 
AltCmd_Out1_29, 

917 
Alt_Out1_39, 

918 
GsKts_Out1_49, 

919 
hdot_Out1_59, 

920 
hdotChgRate_Out1_69, 

921 
*altgammacmd_In1_661, 

922 
\at(*self, Pre), 

923 
\at(*self, Here), 

924 
Abs_Out1_144, 

925 
Kh_Out1_193, 

926 
Logical_Operator_In1_197, 

927 
Logical_Operator_Out1_198, 

928 
Saturation_115_enforce_lo_lim, 

929 
Saturation_115_s_out, 

930 
Sum3_Out1_296, 

931 
Sum_Out1_286, 

932 
Switch1_In2_312, 

933 
Switch1_Out1_314, 

934 
Switch_In2_303, 

935 
Switch_Out1_305, 

936 
VariableLimitSaturation_144_enforce_lo_lim, 

937 
VariableLimitSaturation_144_out, 

938 
VariableRateLimit_139_Gain1_Out1_382, 

939 
VariableRateLimit_139_Gain_Out1_373, 

940 
VariableRateLimit_139_Integrator1_Out1_391, 

941 
VariableRateLimit_139_Sum2_Out1_401, 

942 
VariableRateLimit_139_VariableLimitSaturation_69_enforce_lo_lim, 

943 
VariableRateLimit_139_VariableLimitSaturation_69_out, 

944 
VariableRateLimit_139_integrator_reset_56_ir_out, 

945 
__AltitudeControl_1, 

946 
__AltitudeControl_10, 

947 
__AltitudeControl_2, 

948 
__AltitudeControl_3, 

949 
__AltitudeControl_4, 

950 
__AltitudeControl_5, 

951 
__AltitudeControl_6, 

952 
__AltitudeControl_8, 

953 
__AltitudeControl_9, 

954 
k_Out1_585, 

955 
kts2fps_Out1_594, 

956 
r2d_Out1_603); 

957 
assigns *altgammacmd_In1_661, *self, Abs_Out1_144, Kh_Out1_193, 

958 
Logical_Operator_In1_197, Logical_Operator_Out1_198, 

959 
Saturation_115_enforce_lo_lim, Saturation_115_s_out, Sum3_Out1_296, 

960 
Sum_Out1_286, Switch1_In2_312, Switch1_Out1_314, Switch_In2_303, 

961 
Switch_Out1_305, VariableLimitSaturation_144_enforce_lo_lim, 

962 
VariableLimitSaturation_144_out, 

963 
VariableRateLimit_139_Gain1_Out1_382, 

964 
VariableRateLimit_139_Gain_Out1_373, 

965 
VariableRateLimit_139_Integrator1_Out1_391, 

966 
VariableRateLimit_139_Sum2_Out1_401, 

967 
VariableRateLimit_139_VariableLimitSaturation_69_enforce_lo_lim, 

968 
VariableRateLimit_139_VariableLimitSaturation_69_out, 

969 
VariableRateLimit_139_integrator_reset_56_ir_out, 

970 
__AltitudeControl_1, __AltitudeControl_10, __AltitudeControl_2, 

971 
__AltitudeControl_3, __AltitudeControl_4, __AltitudeControl_5, 

972 
__AltitudeControl_6, __AltitudeControl_8, __AltitudeControl_9, 

973 
k_Out1_585, kts2fps_Out1_594, r2d_Out1_603; 

974 
*/ 

975 
{ 

976 


977 
/*@ensures \exists _Bool Switch_In2_303; 

978 
\exists real Switch_Out1_305; 

979 
\exists real VariableLimitSaturation_144_enforce_lo_lim; 

980 
\exists real VariableLimitSaturation_144_out; 

981 
\exists real VariableRateLimit_139_Gain1_Out1_382; 

982 
\exists real VariableRateLimit_139_Gain_Out1_373; 

983 
\exists real VariableRateLimit_139_Integrator1_Out1_391; 

984 
\exists real VariableRateLimit_139_Sum2_Out1_401; 

985 
\exists real VariableRateLimit_139_VariableLimitSaturation_69_enforce_lo_lim; 

986 
\exists real VariableRateLimit_139_VariableLimitSaturation_69_out; 

987 
\exists real VariableRateLimit_139_integrator_reset_56_ir_out; 

988 
\exists _Bool __AltitudeControl_1; 

989 
\exists _Bool __AltitudeControl_10; 

990 
\exists _Bool __AltitudeControl_2; 

991 
\exists _Bool __AltitudeControl_3; 

992 
\exists _Bool __AltitudeControl_4; 

993 
\exists _Bool __AltitudeControl_5; 

994 
\exists _Bool __AltitudeControl_6; 

995 
\exists _Bool __AltitudeControl_8; 

996 
\exists _Bool __AltitudeControl_9; 

997 
\exists real k_Out1_585; 

998 
\exists real kts2fps_Out1_594; 

999 
\exists real r2d_Out1_603; 

1000 
trans_AltitudeControl(AntEng_Out1_19, 

1001 
AltCmd_Out1_29, 

1002 
Alt_Out1_39, 

1003 
GsKts_Out1_49, 

1004 
hdot_Out1_59, 

1005 
hdotChgRate_Out1_69, 

1006 
*altgammacmd_In1_661, 

1007 
\at(*self, Pre), 

1008 
\at(*self, Here), 

1009 
Abs_Out1_144, 

1010 
Kh_Out1_193, 

1011 
Logical_Operator_In1_197, 

1012 
Logical_Operator_Out1_198, 

1013 
Saturation_115_enforce_lo_lim, 

1014 
Saturation_115_s_out, 

1015 
Sum3_Out1_296, 

1016 
Sum_Out1_286, 

1017 
Switch1_In2_312, 

1018 
Switch1_Out1_314, 

1019 
Switch_In2_303, 

1020 
Switch_Out1_305, 

1021 
VariableLimitSaturation_144_enforce_lo_lim, 

1022 
VariableLimitSaturation_144_out, 

1023 
VariableRateLimit_139_Gain1_Out1_382, 

1024 
VariableRateLimit_139_Gain_Out1_373, 

1025 
VariableRateLimit_139_Integrator1_Out1_391, 

1026 
VariableRateLimit_139_Sum2_Out1_401, 

1027 
VariableRateLimit_139_VariableLimitSaturation_69_enforce_lo_lim, 

1028 
VariableRateLimit_139_VariableLimitSaturation_69_out, 

1029 
VariableRateLimit_139_integrator_reset_56_ir_out, 

1030 
__AltitudeControl_1, 

1031 
__AltitudeControl_10, 

1032 
__AltitudeControl_2, 

1033 
__AltitudeControl_3, 

1034 
__AltitudeControl_4, 

1035 
__AltitudeControl_5, 

1036 
__AltitudeControl_6, 

1037 
__AltitudeControl_8, 

1038 
__AltitudeControl_9, 

1039 
k_Out1_585, 

1040 
kts2fps_Out1_594, 

1041 
r2d_Out1_603); 

1042 
assigns *altgammacmd_In1_661, *self, Abs_Out1_144, Kh_Out1_193, 

1043 
Logical_Operator_In1_197, Logical_Operator_Out1_198, 

1044 
Saturation_115_enforce_lo_lim, Saturation_115_s_out, Sum3_Out1_296, 

1045 
Sum_Out1_286, Switch1_In2_312, Switch1_Out1_314, Switch_In2_303, 

1046 
Switch_Out1_305, VariableLimitSaturation_144_enforce_lo_lim, 

1047 
VariableLimitSaturation_144_out, 

1048 
VariableRateLimit_139_Gain1_Out1_382, 

1049 
VariableRateLimit_139_Gain_Out1_373, 

1050 
VariableRateLimit_139_Integrator1_Out1_391, 

1051 
VariableRateLimit_139_Sum2_Out1_401, 

1052 
VariableRateLimit_139_VariableLimitSaturation_69_enforce_lo_lim, 

1053 
VariableRateLimit_139_VariableLimitSaturation_69_out, 

1054 
VariableRateLimit_139_integrator_reset_56_ir_out, 

1055 
__AltitudeControl_1, __AltitudeControl_10, __AltitudeControl_2, 

1056 
__AltitudeControl_3, __AltitudeControl_4, __AltitudeControl_5, 

1057 
__AltitudeControl_6, __AltitudeControl_8, __AltitudeControl_9, 

1058 
k_Out1_585, kts2fps_Out1_594, r2d_Out1_603; 

1059 
*/ 

1060 
{ 

1061 


1062 
/*@ensures \exists real Switch_Out1_305; 

1063 
\exists real VariableLimitSaturation_144_enforce_lo_lim; 

1064 
\exists real VariableLimitSaturation_144_out; 

1065 
\exists real VariableRateLimit_139_Gain1_Out1_382; 

1066 
\exists real VariableRateLimit_139_Gain_Out1_373; 

1067 
\exists real VariableRateLimit_139_Integrator1_Out1_391; 

1068 
\exists real VariableRateLimit_139_Sum2_Out1_401; 

1069 
\exists real VariableRateLimit_139_VariableLimitSaturation_69_enforce_lo_lim; 

1070 
\exists real VariableRateLimit_139_VariableLimitSaturation_69_out; 

1071 
\exists real VariableRateLimit_139_integrator_reset_56_ir_out; 

1072 
\exists _Bool __AltitudeControl_1; 

1073 
\exists _Bool __AltitudeControl_10; 

1074 
\exists _Bool __AltitudeControl_2; 

1075 
\exists _Bool __AltitudeControl_3; 

1076 
\exists _Bool __AltitudeControl_4; 

1077 
\exists _Bool __AltitudeControl_5; 

1078 
\exists _Bool __AltitudeControl_6; 

1079 
\exists _Bool __AltitudeControl_8; 

1080 
\exists _Bool __AltitudeControl_9; 

1081 
\exists real k_Out1_585; 

1082 
\exists real kts2fps_Out1_594; 

1083 
\exists real r2d_Out1_603; 

1084 
trans_AltitudeControl(AntEng_Out1_19, 

1085 
AltCmd_Out1_29, 

1086 
Alt_Out1_39, 

1087 
GsKts_Out1_49, 

1088 
hdot_Out1_59, 

1089 
hdotChgRate_Out1_69, 

1090 
*altgammacmd_In1_661, 

1091 
\at(*self, Pre), 

1092 
\at(*self, Here), 

1093 
Abs_Out1_144, 

1094 
Kh_Out1_193, 

1095 
Logical_Operator_In1_197, 

1096 
Logical_Operator_Out1_198, 

1097 
Saturation_115_enforce_lo_lim, 

1098 
Saturation_115_s_out, 

1099 
Sum3_Out1_296, 

1100 
Sum_Out1_286, 

1101 
Switch1_In2_312, 

1102 
Switch1_Out1_314, 

1103 
Switch_In2_303, 

1104 
Switch_Out1_305, 

1105 
VariableLimitSaturation_144_enforce_lo_lim, 

1106 
VariableLimitSaturation_144_out, 

1107 
VariableRateLimit_139_Gain1_Out1_382, 

1108 
VariableRateLimit_139_Gain_Out1_373, 

1109 
VariableRateLimit_139_Integrator1_Out1_391, 

1110 
VariableRateLimit_139_Sum2_Out1_401, 

1111 
VariableRateLimit_139_VariableLimitSaturation_69_enforce_lo_lim, 

1112 
VariableRateLimit_139_VariableLimitSaturation_69_out, 

1113 
VariableRateLimit_139_integrator_reset_56_ir_out, 

1114 
__AltitudeControl_1, 

1115 
__AltitudeControl_10, 

1116 
__AltitudeControl_2, 

1117 
__AltitudeControl_3, 

1118 
__AltitudeControl_4, 

1119 
__AltitudeControl_5, 

1120 
__AltitudeControl_6, 

1121 
__AltitudeControl_8, 

1122 
__AltitudeControl_9, 

1123 
k_Out1_585, 

1124 
kts2fps_Out1_594, 

1125 
r2d_Out1_603); 

1126 
assigns *altgammacmd_In1_661, *self, Abs_Out1_144, Kh_Out1_193, 

1127 
Logical_Operator_In1_197, Logical_Operator_Out1_198, 

1128 
Saturation_115_enforce_lo_lim, Saturation_115_s_out, Sum3_Out1_296, 

1129 
Sum_Out1_286, Switch1_In2_312, Switch1_Out1_314, Switch_In2_303, 

1130 
Switch_Out1_305, VariableLimitSaturation_144_enforce_lo_lim, 

1131 
VariableLimitSaturation_144_out, 

1132 
VariableRateLimit_139_Gain1_Out1_382, 

1133 
VariableRateLimit_139_Gain_Out1_373, 

1134 
VariableRateLimit_139_Integrator1_Out1_391, 

1135 
VariableRateLimit_139_Sum2_Out1_401, 

1136 
VariableRateLimit_139_VariableLimitSaturation_69_enforce_lo_lim, 

1137 
VariableRateLimit_139_VariableLimitSaturation_69_out, 

1138 
VariableRateLimit_139_integrator_reset_56_ir_out, 

1139 
__AltitudeControl_1, __AltitudeControl_10, __AltitudeControl_2, 

1140 
__AltitudeControl_3, __AltitudeControl_4, __AltitudeControl_5, 

1141 
__AltitudeControl_6, __AltitudeControl_8, __AltitudeControl_9, 

1142 
k_Out1_585, kts2fps_Out1_594, r2d_Out1_603; 

1143 
*/ 

1144 
{ 

1145 


1146 
/*@ensures \exists real VariableLimitSaturation_144_enforce_lo_lim; 

1147 
\exists real VariableLimitSaturation_144_out; 

1148 
\exists real VariableRateLimit_139_Gain1_Out1_382; 

1149 
\exists real VariableRateLimit_139_Gain_Out1_373; 

1150 
\exists real VariableRateLimit_139_Integrator1_Out1_391; 

1151 
\exists real VariableRateLimit_139_Sum2_Out1_401; 

1152 
\exists real VariableRateLimit_139_VariableLimitSaturation_69_enforce_lo_lim; 

1153 
\exists real VariableRateLimit_139_VariableLimitSaturation_69_out; 

1154 
\exists real VariableRateLimit_139_integrator_reset_56_ir_out; 

1155 
\exists _Bool __AltitudeControl_1; 

1156 
\exists _Bool __AltitudeControl_10; 

1157 
\exists _Bool __AltitudeControl_2; 

1158 
\exists _Bool __AltitudeControl_3; 

1159 
\exists _Bool __AltitudeControl_4; 

1160 
\exists _Bool __AltitudeControl_5; 

1161 
\exists _Bool __AltitudeControl_6; 

1162 
\exists _Bool __AltitudeControl_8; 

1163 
\exists _Bool __AltitudeControl_9; 

1164 
\exists real k_Out1_585; 

1165 
\exists real kts2fps_Out1_594; 

1166 
\exists real r2d_Out1_603; 

1167 
trans_AltitudeControl(AntEng_Out1_19, 

1168 
AltCmd_Out1_29, 

1169 
Alt_Out1_39, 

1170 
GsKts_Out1_49, 

1171 
hdot_Out1_59, 

1172 
hdotChgRate_Out1_69, 

1173 
*altgammacmd_In1_661, 

1174 
\at(*self, Pre), 

1175 
\at(*self, Here), 

1176 
Abs_Out1_144, 

1177 
Kh_Out1_193, 

1178 
Logical_Operator_In1_197, 

1179 
Logical_Operator_Out1_198, 

1180 
Saturation_115_enforce_lo_lim, 

1181 
Saturation_115_s_out, 

1182 
Sum3_Out1_296, 

1183 
Sum_Out1_286, 

1184 
Switch1_In2_312, 

1185 
Switch1_Out1_314, 

1186 
Switch_In2_303, 

1187 
Switch_Out1_305, 

1188 
VariableLimitSaturation_144_enforce_lo_lim, 

1189 
VariableLimitSaturation_144_out, 

1190 
VariableRateLimit_139_Gain1_Out1_382, 

1191 
VariableRateLimit_139_Gain_Out1_373, 

1192 
VariableRateLimit_139_Integrator1_Out1_391, 

1193 
VariableRateLimit_139_Sum2_Out1_401, 

1194 
VariableRateLimit_139_VariableLimitSaturation_69_enforce_lo_lim, 

1195 
VariableRateLimit_139_VariableLimitSaturation_69_out, 

1196 
VariableRateLimit_139_integrator_reset_56_ir_out, 

1197 
__AltitudeControl_1, 

1198 
__AltitudeControl_10, 

1199 
__AltitudeControl_2, 

1200 
__AltitudeControl_3, 

1201 
__AltitudeControl_4, 

1202 
__AltitudeControl_5, 

1203 
__AltitudeControl_6, 

1204 
__AltitudeControl_8, 

1205 
__AltitudeControl_9, 

1206 
k_Out1_585, 

1207 
kts2fps_Out1_594, 

1208 
r2d_Out1_603); 

1209 
assigns *altgammacmd_In1_661, *self, Abs_Out1_144, Kh_Out1_193, 

1210 
Logical_Operator_In1_197, Logical_Operator_Out1_198, 

1211 
Saturation_115_enforce_lo_lim, Saturation_115_s_out, Sum3_Out1_296, 

1212 
Sum_Out1_286, Switch1_In2_312, Switch1_Out1_314, Switch_In2_303, 

1213 
Switch_Out1_305, VariableLimitSaturation_144_enforce_lo_lim, 

1214 
VariableLimitSaturation_144_out, 

1215 
VariableRateLimit_139_Gain1_Out1_382, 

1216 
VariableRateLimit_139_Gain_Out1_373, 

1217 
VariableRateLimit_139_Integrator1_Out1_391, 

1218 
VariableRateLimit_139_Sum2_Out1_401, 

1219 
VariableRateLimit_139_VariableLimitSaturation_69_enforce_lo_lim, 

1220 
VariableRateLimit_139_VariableLimitSaturation_69_out, 

1221 
VariableRateLimit_139_integrator_reset_56_ir_out, 

1222 
__AltitudeControl_1, __AltitudeControl_10, __AltitudeControl_2, 

1223 
__AltitudeControl_3, __AltitudeControl_4, __AltitudeControl_5, 

1224 
__AltitudeControl_6, __AltitudeControl_8, __AltitudeControl_9, 

1225 
k_Out1_585, kts2fps_Out1_594, r2d_Out1_603; 

1226 
*/ 

1227 
{ 

1228 


1229 
/*@ensures \exists real VariableLimitSaturation_144_out; 

1230 
\exists real VariableRateLimit_139_Gain1_Out1_382; 

1231 
\exists real VariableRateLimit_139_Gain_Out1_373; 

1232 
\exists real VariableRateLimit_139_Integrator1_Out1_391; 

1233 
\exists real VariableRateLimit_139_Sum2_Out1_401; 

1234 
\exists real VariableRateLimit_139_VariableLimitSaturation_69_enforce_lo_lim; 

1235 
\exists real VariableRateLimit_139_VariableLimitSaturation_69_out; 

1236 
\exists real VariableRateLimit_139_integrator_reset_56_ir_out; 

1237 
\exists _Bool __AltitudeControl_1; 

1238 
\exists _Bool __AltitudeControl_10; 

1239 
\exists _Bool __AltitudeControl_2; 

1240 
\exists _Bool __AltitudeControl_3; 

1241 
\exists _Bool __AltitudeControl_4; 

1242 
\exists _Bool __AltitudeControl_5; 

1243 
\exists _Bool __AltitudeControl_6; 

1244 
\exists _Bool __AltitudeControl_8; 

1245 
\exists _Bool __AltitudeControl_9; 

1246 
\exists real k_Out1_585; 

1247 
\exists real kts2fps_Out1_594; 

1248 
\exists real r2d_Out1_603; 

1249 
trans_AltitudeControl(AntEng_Out1_19, 

1250 
AltCmd_Out1_29, 

1251 
Alt_Out1_39, 

1252 
GsKts_Out1_49, 

1253 
hdot_Out1_59, 

1254 
hdotChgRate_Out1_69, 

1255 
*altgammacmd_In1_661, 

1256 
\at(*self, Pre), 

1257 
\at(*self, Here), 

1258 
Abs_Out1_144, 

1259 
Kh_Out1_193, 

1260 
Logical_Operator_In1_197, 

1261 
Logical_Operator_Out1_198, 

1262 
Saturation_115_enforce_lo_lim, 

1263 
Saturation_115_s_out, 

1264 
Sum3_Out1_296, 

1265 
Sum_Out1_286, 

1266 
Switch1_In2_312, 

1267 
Switch1_Out1_314, 

1268 
Switch_In2_303, 

1269 
Switch_Out1_305, 

1270 
VariableLimitSaturation_144_enforce_lo_lim, 

1271 
VariableLimitSaturation_144_out, 

1272 
VariableRateLimit_139_Gain1_Out1_382, 

1273 
VariableRateLimit_139_Gain_Out1_373, 

1274 
VariableRateLimit_139_Integrator1_Out1_391, 

1275 
VariableRateLimit_139_Sum2_Out1_401, 

1276 
VariableRateLimit_139_VariableLimitSaturation_69_enforce_lo_lim, 

1277 
VariableRateLimit_139_VariableLimitSaturation_69_out, 

1278 
VariableRateLimit_139_integrator_reset_56_ir_out, 

1279 
__AltitudeControl_1, 

1280 
__AltitudeControl_10, 

1281 
__AltitudeControl_2, 

1282 
__AltitudeControl_3, 

1283 
__AltitudeControl_4, 

1284 
__AltitudeControl_5, 

1285 
__AltitudeControl_6, 

1286 
__AltitudeControl_8, 

1287 
__AltitudeControl_9, 

1288 
k_Out1_585, 

1289 
kts2fps_Out1_594, 

1290 
r2d_Out1_603); 

1291 
assigns *altgammacmd_In1_661, *self, Abs_Out1_144, Kh_Out1_193, 

1292 
Logical_Operator_In1_197, Logical_Operator_Out1_198, 

1293 
Saturation_115_enforce_lo_lim, Saturation_115_s_out, Sum3_Out1_296, 

1294 
Sum_Out1_286, Switch1_In2_312, Switch1_Out1_314, Switch_In2_303, 

1295 
Switch_Out1_305, VariableLimitSaturation_144_enforce_lo_lim, 

1296 
VariableLimitSaturation_144_out, 

1297 
VariableRateLimit_139_Gain1_Out1_382, 

1298 
VariableRateLimit_139_Gain_Out1_373, 

1299 
VariableRateLimit_139_Integrator1_Out1_391, 

1300 
VariableRateLimit_139_Sum2_Out1_401, 

1301 
VariableRateLimit_139_VariableLimitSaturation_69_enforce_lo_lim, 

1302 
VariableRateLimit_139_VariableLimitSaturation_69_out, 

1303 
VariableRateLimit_139_integrator_reset_56_ir_out, 

1304 
__AltitudeControl_1, __AltitudeControl_10, __AltitudeControl_2, 

1305 
__AltitudeControl_3, __AltitudeControl_4, __AltitudeControl_5, 

1306 
__AltitudeControl_6, __AltitudeControl_8, __AltitudeControl_9, 

1307 
k_Out1_585, kts2fps_Out1_594, r2d_Out1_603; 

1308 
*/ 

1309 
{ 

1310 


1311 
/*@ensures \exists real VariableRateLimit_139_Gain1_Out1_382; 

1312 
\exists real VariableRateLimit_139_Gain_Out1_373; 

1313 
\exists real VariableRateLimit_139_Integrator1_Out1_391; 

1314 
\exists real VariableRateLimit_139_Sum2_Out1_401; 

1315 
\exists real VariableRateLimit_139_VariableLimitSaturation_69_enforce_lo_lim; 

1316 
\exists real VariableRateLimit_139_VariableLimitSaturation_69_out; 

1317 
\exists real VariableRateLimit_139_integrator_reset_56_ir_out; 

1318 
\exists _Bool __AltitudeControl_1; 

1319 
\exists _Bool __AltitudeControl_10; 

1320 
\exists _Bool __AltitudeControl_2; 

1321 
\exists _Bool __AltitudeControl_3; 

1322 
\exists _Bool __AltitudeControl_4; 

1323 
\exists _Bool __AltitudeControl_5; 

1324 
\exists _Bool __AltitudeControl_6; 

1325 
\exists _Bool __AltitudeControl_8; 

1326 
\exists _Bool __AltitudeControl_9; 

1327 
\exists real k_Out1_585; 

1328 
\exists real kts2fps_Out1_594; 

1329 
\exists real r2d_Out1_603; 

1330 
trans_AltitudeControl(AntEng_Out1_19, 

1331 
AltCmd_Out1_29, 

1332 
Alt_Out1_39, 

1333 
GsKts_Out1_49, 

1334 
hdot_Out1_59, 

1335 
hdotChgRate_Out1_69, 

1336 
*altgammacmd_In1_661, 

1337 
\at(*self, Pre), 

1338 
\at(*self, Here), 

1339 
Abs_Out1_144, 

1340 
Kh_Out1_193, 

1341 
Logical_Operator_In1_197, 

1342 
Logical_Operator_Out1_198, 

1343 
Saturation_115_enforce_lo_lim, 

1344 
Saturation_115_s_out, 

1345 
Sum3_Out1_296, 

1346 
Sum_Out1_286, 

1347 
Switch1_In2_312, 

1348 
Switch1_Out1_314, 

1349 
Switch_In2_303, 

1350 
Switch_Out1_305, 

1351 
VariableLimitSaturation_144_enforce_lo_lim, 

1352 
VariableLimitSaturation_144_out, 

1353 
VariableRateLimit_139_Gain1_Out1_382, 

1354 
VariableRateLimit_139_Gain_Out1_373, 

1355 
VariableRateLimit_139_Integrator1_Out1_391, 

1356 
VariableRateLimit_139_Sum2_Out1_401, 

1357 
VariableRateLimit_139_VariableLimitSaturation_69_enforce_lo_lim, 

1358 
VariableRateLimit_139_VariableLimitSaturation_69_out, 

1359 
VariableRateLimit_139_integrator_reset_56_ir_out, 

1360 
__AltitudeControl_1, 

1361 
__AltitudeControl_10, 

1362 
__AltitudeControl_2, 

1363 
__AltitudeControl_3, 

1364 
__AltitudeControl_4, 

1365 
__AltitudeControl_5, 

1366 
__AltitudeControl_6, 

1367 
__AltitudeControl_8, 

1368 
__AltitudeControl_9, 

1369 
k_Out1_585, 

1370 
kts2fps_Out1_594, 

1371 
r2d_Out1_603); 

1372 
assigns *altgammacmd_In1_661, *self, Abs_Out1_144, Kh_Out1_193, 

1373 
Logical_Operator_In1_197, Logical_Operator_Out1_198, 

1374 
Saturation_115_enforce_lo_lim, Saturation_115_s_out, Sum3_Out1_296, 

1375 
Sum_Out1_286, Switch1_In2_312, Switch1_Out1_314, Switch_In2_303, 

1376 
Switch_Out1_305, VariableLimitSaturation_144_enforce_lo_lim, 

1377 
VariableLimitSaturation_144_out, 

1378 
VariableRateLimit_139_Gain1_Out1_382, 

1379 
VariableRateLimit_139_Gain_Out1_373, 

1380 
VariableRateLimit_139_Integrator1_Out1_391, 

1381 
VariableRateLimit_139_Sum2_Out1_401, 

1382 
VariableRateLimit_139_VariableLimitSaturation_69_enforce_lo_lim, 

1383 
VariableRateLimit_139_VariableLimitSaturation_69_out, 

1384 
VariableRateLimit_139_integrator_reset_56_ir_out, 

1385 
__AltitudeControl_1, __AltitudeControl_10, __AltitudeControl_2, 

1386 
__AltitudeControl_3, __AltitudeControl_4, __AltitudeControl_5, 

1387 
__AltitudeControl_6, __AltitudeControl_8, __AltitudeControl_9, 

1388 
k_Out1_585, kts2fps_Out1_594, r2d_Out1_603; 

1389 
*/ 

1390 
{ 

1391 


1392 
/*@ensures \exists real VariableRateLimit_139_Gain_Out1_373; 

1393 
\exists real VariableRateLimit_139_Integrator1_Out1_391; 

1394 
\exists real VariableRateLimit_139_Sum2_Out1_401; 

1395 
\exists real VariableRateLimit_139_VariableLimitSaturation_69_enforce_lo_lim; 

1396 
\exists real VariableRateLimit_139_VariableLimitSaturation_69_out; 

1397 
\exists real VariableRateLimit_139_integrator_reset_56_ir_out; 

1398 
\exists _Bool __AltitudeControl_1; 

1399 
\exists _Bool __AltitudeControl_10; 

1400 
\exists _Bool __AltitudeControl_2; 

1401 
\exists _Bool __AltitudeControl_3; 

1402 
\exists _Bool __AltitudeControl_4; 

1403 
\exists _Bool __AltitudeControl_5; 

1404 
\exists _Bool __AltitudeControl_6; 

1405 
\exists _Bool __AltitudeControl_8; 

1406 
\exists _Bool __AltitudeControl_9; 

1407 
\exists real k_Out1_585; 

1408 
\exists real kts2fps_Out1_594; 

1409 
\exists real r2d_Out1_603; 

1410 
trans_AltitudeControl(AntEng_Out1_19, 

1411 
AltCmd_Out1_29, 

1412 
Alt_Out1_39, 

1413 
GsKts_Out1_49, 

1414 
hdot_Out1_59, 

1415 
hdotChgRate_Out1_69, 

1416 
*altgammacmd_In1_661, 

1417 
\at(*self, Pre), 

1418 
\at(*self, Here), 

1419 
Abs_Out1_144, 

1420 
Kh_Out1_193, 

1421 
Logical_Operator_In1_197, 

1422 
Logical_Operator_Out1_198, 

1423 
Saturation_115_enforce_lo_lim, 

1424 
Saturation_115_s_out, 

1425 
Sum3_Out1_296, 

1426 
Sum_Out1_286, 

1427 
Switch1_In2_312, 

1428 
Switch1_Out1_314, 

1429 
Switch_In2_303, 

1430 
Switch_Out1_305, 

1431 
VariableLimitSaturation_144_enforce_lo_lim, 

1432 
VariableLimitSaturation_144_out, 

1433 
VariableRateLimit_139_Gain1_Out1_382, 

1434 
VariableRateLimit_139_Gain_Out1_373, 

1435 
VariableRateLimit_139_Integrator1_Out1_391, 

1436 
VariableRateLimit_139_Sum2_Out1_401, 

1437 
VariableRateLimit_139_VariableLimitSaturation_69_enforce_lo_lim, 

1438 
VariableRateLimit_139_VariableLimitSaturation_69_out, 

1439 
VariableRateLimit_139_integrator_reset_56_ir_out, 

1440 
__AltitudeControl_1, 

1441 
__AltitudeControl_10, 

1442 
__AltitudeControl_2, 

1443 
__AltitudeControl_3, 

1444 
__AltitudeControl_4, 

1445 
__AltitudeControl_5, 

1446 
__AltitudeControl_6, 

1447 
__AltitudeControl_8, 

1448 
__AltitudeControl_9, 

1449 
k_Out1_585, 

1450 
kts2fps_Out1_594, 

1451 
r2d_Out1_603); 

1452 
assigns *altgammacmd_In1_661, *self, Abs_Out1_144, Kh_Out1_193, 

1453 
Logical_Operator_In1_197, Logical_Operator_Out1_198, 

1454 
Saturation_115_enforce_lo_lim, Saturation_115_s_out, Sum3_Out1_296, 

1455 
Sum_Out1_286, Switch1_In2_312, Switch1_Out1_314, Switch_In2_303, 

1456 
Switch_Out1_305, VariableLimitSaturation_144_enforce_lo_lim, 

1457 
VariableLimitSaturation_144_out, 

1458 
VariableRateLimit_139_Gain1_Out1_382, 

1459 
VariableRateLimit_139_Gain_Out1_373, 

1460 
VariableRateLimit_139_Integrator1_Out1_391, 

1461 
VariableRateLimit_139_Sum2_Out1_401, 

1462 
VariableRateLimit_139_VariableLimitSaturation_69_enforce_lo_lim, 

1463 
VariableRateLimit_139_VariableLimitSaturation_69_out, 

1464 
VariableRateLimit_139_integrator_reset_56_ir_out, 

1465 
__AltitudeControl_1, __AltitudeControl_10, __AltitudeControl_2, 

1466 
__AltitudeControl_3, __AltitudeControl_4, __AltitudeControl_5, 

1467 
__AltitudeControl_6, __AltitudeControl_8, __AltitudeControl_9, 

1468 
k_Out1_585, kts2fps_Out1_594, r2d_Out1_603; 

1469 
*/ 

1470 
{ 

1471 


1472 
/*@ensures \exists real VariableRateLimit_139_Integrator1_Out1_391; 

1473 
\exists real VariableRateLimit_139_Sum2_Out1_401; 

1474 
\exists real VariableRateLimit_139_VariableLimitSaturation_69_enforce_lo_lim; 

1475 
\exists real VariableRateLimit_139_VariableLimitSaturation_69_out; 

1476 
\exists real VariableRateLimit_139_integrator_reset_56_ir_out; 

1477 
\exists _Bool __AltitudeControl_1; 

1478 
\exists _Bool __AltitudeControl_10; 

1479 
\exists _Bool __AltitudeControl_2; 

1480 
\exists _Bool __AltitudeControl_3; 

1481 
\exists _Bool __AltitudeControl_4; 

1482 
\exists _Bool __AltitudeControl_5; 

1483 
\exists _Bool __AltitudeControl_6; 

1484 
\exists _Bool __AltitudeControl_8; 

1485 
\exists _Bool __AltitudeControl_9; 

1486 
\exists real k_Out1_585; 

1487 
\exists real kts2fps_Out1_594; 

1488 
\exists real r2d_Out1_603; 

1489 
trans_AltitudeControl(AntEng_Out1_19, 

1490 
AltCmd_Out1_29, 

1491 
Alt_Out1_39, 

1492 
GsKts_Out1_49, 

1493 
hdot_Out1_59, 

1494 
hdotChgRate_Out1_69, 

1495 
*altgammacmd_In1_661, 

1496 
\at(*self, Pre), 

1497 
\at(*self, Here), 

1498 
Abs_Out1_144, 

1499 
Kh_Out1_193, 

1500 
Logical_Operator_In1_197, 

1501 
Logical_Operator_Out1_198, 

1502 
Saturation_115_enforce_lo_lim, 

1503 
Saturation_115_s_out, 

1504 
Sum3_Out1_296, 

1505 
Sum_Out1_286, 

1506 
Switch1_In2_312, 

1507 
Switch1_Out1_314, 

1508 
Switch_In2_303, 

1509 
Switch_Out1_305, 

1510 
VariableLimitSaturation_144_enforce_lo_lim, 

1511 
VariableLimitSaturation_144_out, 

1512 
VariableRateLimit_139_Gain1_Out1_382, 

1513 
VariableRateLimit_139_Gain_Out1_373, 

1514 
VariableRateLimit_139_Integrator1_Out1_391, 

1515 
VariableRateLimit_139_Sum2_Out1_401, 

1516 
VariableRateLimit_139_VariableLimitSaturation_69_enforce_lo_lim, 

1517 
VariableRateLimit_139_VariableLimitSaturation_69_out, 

1518 
VariableRateLimit_139_integrator_reset_56_ir_out, 

1519 
__AltitudeControl_1, 

1520 
__AltitudeControl_10, 

1521 
__AltitudeControl_2, 

1522 
__AltitudeControl_3, 

1523 
__AltitudeControl_4, 

1524 
__AltitudeControl_5, 

1525 
__AltitudeControl_6, 

1526 
__AltitudeControl_8, 

1527 
__AltitudeControl_9, 

1528 
k_Out1_585, 

1529 
kts2fps_Out1_594, 

1530 
r2d_Out1_603); 

1531 
assigns *altgammacmd_In1_661, *self, Abs_Out1_144, Kh_Out1_193, 

1532 
Logical_Operator_In1_197, Logical_Operator_Out1_198, 

1533 
Saturation_115_enforce_lo_lim, Saturation_115_s_out, Sum3_Out1_296, 

1534 
Sum_Out1_286, Switch1_In2_312, Switch1_Out1_314, Switch_In2_303, 

1535 
Switch_Out1_305, VariableLimitSaturation_144_enforce_lo_lim, 

1536 
VariableLimitSaturation_144_out, 

1537 
VariableRateLimit_139_Gain1_Out1_382, 

1538 
VariableRateLimit_139_Gain_Out1_373, 

1539 
VariableRateLimit_139_Integrator1_Out1_391, 

1540 
VariableRateLimit_139_Sum2_Out1_401, 

1541 
VariableRateLimit_139_VariableLimitSaturation_69_enforce_lo_lim, 

1542 
VariableRateLimit_139_VariableLimitSaturation_69_out, 

1543 
VariableRateLimit_139_integrator_reset_56_ir_out, 

1544 
__AltitudeControl_1, __AltitudeControl_10, __AltitudeControl_2, 

1545 
__AltitudeControl_3, __AltitudeControl_4, __AltitudeControl_5, 

1546 
__AltitudeControl_6, __AltitudeControl_8, __AltitudeControl_9, 

1547 
k_Out1_585, kts2fps_Out1_594, r2d_Out1_603; 

1548 
*/ 

1549 
{ 

1550 


1551 
/*@ensures \exists real VariableRateLimit_139_Sum2_Out1_401; 

1552 
\exists real VariableRateLimit_139_VariableLimitSaturation_69_enforce_lo_lim; 

1553 
\exists real VariableRateLimit_139_VariableLimitSaturation_69_out; 

1554 
\exists real VariableRateLimit_139_integrator_reset_56_ir_out; 

1555 
\exists _Bool __AltitudeControl_1; 

1556 
\exists _Bool __AltitudeControl_10; 
Also available in: Unified diff
Update on c backend proof