Revision bff13707
Added by Guillaume Davy over 10 years ago
| tcm_benchmarks/ALT2/ALT2_proof/ALT_2.lustrec.c | ||
|---|---|---|
| 27 | 27 |
hdotChgRate, |
| 28 | 28 |
*obs, |
| 29 | 29 |
\at(*self, Pre), |
| 30 |
\at(*self, Here));
|
|
| 30 |
(*self));
|
|
| 31 | 31 |
assigns *obs, *self; |
| 32 | 32 |
*/ |
| 33 | 33 |
{
|
| ... | ... | |
| 46 | 46 |
hdotChgRate, |
| 47 | 47 |
*obs, |
| 48 | 48 |
\at(*self, Pre), |
| 49 |
\at(*self, Here),
|
|
| 49 |
(*self),
|
|
| 50 | 50 |
altgammaCmd, |
| 51 | 51 |
tempAlt); |
| 52 | 52 |
assigns *obs, *self, altgammaCmd, tempAlt; |
| ... | ... | |
| 61 | 61 |
hdotChgRate, |
| 62 | 62 |
*obs, |
| 63 | 63 |
\at(*self, Pre), |
| 64 |
\at(*self, Here),
|
|
| 64 |
(*self),
|
|
| 65 | 65 |
altgammaCmd, |
| 66 | 66 |
tempAlt); |
| 67 | 67 |
assigns *obs, *self, altgammaCmd, tempAlt; |
| ... | ... | |
| 105 | 105 |
hdotChgRate_Out1_69, |
| 106 | 106 |
*altgammacmd_In1_661, |
| 107 | 107 |
\at(*self, Pre), |
| 108 |
\at(*self, Here));
|
|
| 108 |
(*self));
|
|
| 109 | 109 |
assigns *altgammacmd_In1_661, *self; |
| 110 | 110 |
*/ |
| 111 | 111 |
{
|
| ... | ... | |
| 142 | 142 |
hdotChgRate_Out1_69, |
| 143 | 143 |
*altgammacmd_In1_661, |
| 144 | 144 |
\at(*self, Pre), |
| 145 |
\at(*self, Here),
|
|
| 145 |
(*self),
|
|
| 146 | 146 |
Abs_Out1_144, |
| 147 | 147 |
Kh_Out1_193, |
| 148 | 148 |
Logical_Operator_In1_197, |
| ... | ... | |
| 181 | 181 |
hdotChgRate_Out1_69, |
| 182 | 182 |
*altgammacmd_In1_661, |
| 183 | 183 |
\at(*self, Pre), |
| 184 |
\at(*self, Here),
|
|
| 184 |
(*self),
|
|
| 185 | 185 |
Abs_Out1_144, |
| 186 | 186 |
Kh_Out1_193, |
| 187 | 187 |
Logical_Operator_In1_197, |
| ... | ... | |
| 219 | 219 |
hdotChgRate_Out1_69, |
| 220 | 220 |
*altgammacmd_In1_661, |
| 221 | 221 |
\at(*self, Pre), |
| 222 |
\at(*self, Here),
|
|
| 222 |
(*self),
|
|
| 223 | 223 |
Abs_Out1_144, |
| 224 | 224 |
Kh_Out1_193, |
| 225 | 225 |
Logical_Operator_In1_197, |
| ... | ... | |
| 256 | 256 |
hdotChgRate_Out1_69, |
| 257 | 257 |
*altgammacmd_In1_661, |
| 258 | 258 |
\at(*self, Pre), |
| 259 |
\at(*self, Here),
|
|
| 259 |
(*self),
|
|
| 260 | 260 |
Abs_Out1_144, |
| 261 | 261 |
Kh_Out1_193, |
| 262 | 262 |
Logical_Operator_In1_197, |
| ... | ... | |
| 333 | 333 |
Sum_Out1_286 = (AltCmd_Out1_29 + (- Alt_Out1_39)); |
| 334 | 334 |
Kh_Out1_193 = (0.08 * Sum_Out1_286); |
| 335 | 335 |
Switch_Out1_305 = (Switch_In2_303?(Kh_Out1_193):(0.)); |
| 336 |
/*@ |
|
| 337 |
ensures Ctrans_VariableLimitSaturation((double) Sum3_Out1_296, |
|
| 338 |
(double) Switch_Out1_305, |
|
| 339 |
(double) k_Out1_585, |
|
| 340 |
Variable_Limit_Saturation_0_Out1_509); |
|
| 341 |
assigns Variable_Limit_Saturation_0_Out1_509; |
|
| 342 |
*/ {
|
|
| 336 | 343 |
VariableLimitSaturation_step (Sum3_Out1_296, Switch_Out1_305, k_Out1_585, &Variable_Limit_Saturation_0_Out1_509); |
| 344 |
} |
|
| 345 |
/*@ |
|
| 346 |
ensures Ctrans_VariableRateLimit((double) hdotChgRate_Out1_69, |
|
| 347 |
(double) Variable_Limit_Saturation_0_Out1_509, |
|
| 348 |
(_Bool) ((Logical_Operator_Out1_198)?1:0), |
|
| 349 |
(double) hdot_Out1_59, |
|
| 350 |
Variable__Rate_Limit_Out1_324, |
|
| 351 |
\at(*self, Pre).ni_1, |
|
| 352 |
(*self).ni_1); |
|
| 353 |
assigns Variable__Rate_Limit_Out1_324, self->ni_1; |
|
| 354 |
*/ {
|
|
| 337 | 355 |
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_1); |
| 356 |
} |
|
| 338 | 357 |
r2d_Out1_603 = (57.2958 * Variable__Rate_Limit_Out1_324); |
| 339 | 358 |
kts2fps_Out1_594 = (1.6878 * GsKts_Out1_49); |
| 340 | 359 |
Switch1_In2_312 = (__AltitudeControl_2?(0):(1)); |
| ... | ... | |
| 360 | 379 |
IC_Out1_364, |
| 361 | 380 |
*output_In1_489, |
| 362 | 381 |
\at(*self, Pre), |
| 363 |
\at(*self, Here));
|
|
| 382 |
(*self));
|
|
| 364 | 383 |
assigns *output_In1_489, *self; |
| 365 | 384 |
*/ |
| 366 | 385 |
{
|
| ... | ... | |
| 383 | 402 |
IC_Out1_364, |
| 384 | 403 |
*output_In1_489, |
| 385 | 404 |
\at(*self, Pre), |
| 386 |
\at(*self, Here),
|
|
| 405 |
(*self),
|
|
| 387 | 406 |
Gain1_Out1_382, |
| 388 | 407 |
Gain_Out1_373, |
| 389 | 408 |
Integrator1_Out1_391, |
| ... | ... | |
| 405 | 424 |
IC_Out1_364, |
| 406 | 425 |
*output_In1_489, |
| 407 | 426 |
\at(*self, Pre), |
| 408 |
\at(*self, Here),
|
|
| 427 |
(*self),
|
|
| 409 | 428 |
Gain1_Out1_382, |
| 410 | 429 |
Gain_Out1_373, |
| 411 | 430 |
Integrator1_Out1_391, |
| ... | ... | |
| 426 | 445 |
IC_Out1_364, |
| 427 | 446 |
*output_In1_489, |
| 428 | 447 |
\at(*self, Pre), |
| 429 |
\at(*self, Here),
|
|
| 448 |
(*self),
|
|
| 430 | 449 |
Gain1_Out1_382, |
| 431 | 450 |
Gain_Out1_373, |
| 432 | 451 |
Integrator1_Out1_391, |
| ... | ... | |
| 440 | 459 |
__VariableRateLimit_2; |
| 441 | 460 |
*/ |
| 442 | 461 |
{
|
| 443 |
/*@ ensures (__VariableRateLimit_1==(\at(*self, Pre).ni_3._reg._first?(1):(0))) && ((*self).ni_3._reg._first==0); |
|
| 462 |
/*@ ensures (__VariableRateLimit_1==(\at(*self, Pre).ni_3._reg._first?(1):(0))); |
|
| 463 |
ensures ((*self).ni_3._reg._first==0); |
|
| 444 | 464 |
ensures (Integrator1_Out1_391 == (__VariableRateLimit_1?(IC_Out1_364):(\at(*self, Pre)._reg.__VariableRateLimit_3))); |
| 445 | 465 |
ensures (*output_In1_489 == Integrator1_Out1_391); |
| 446 | 466 |
ensures (Gain1_Out1_382 == (- ratelim_Out1_334)); |
| ... | ... | |
| 451 | 471 |
(double) Gain1_Out1_382, |
| 452 | 472 |
Variable_Limit_Saturation_Out1_410); |
| 453 | 473 |
ensures Ctrans_integrator_reset((double) Variable_Limit_Saturation_Out1_410, |
| 454 |
(_Bool) ((ICtrig_Out1_354)?1:0),
|
|
| 474 |
ICtrig_Out1_354,
|
|
| 455 | 475 |
(double) IC_Out1_364, |
| 456 | 476 |
__VariableRateLimit_2, |
| 457 | 477 |
\at(*self, Pre).ni_2, |
| ... | ... | |
| 465 | 485 |
|
| 466 | 486 |
_arrow_step (1, 0, &__VariableRateLimit_1, &self->ni_3); |
| 467 | 487 |
Integrator1_Out1_391 = (__VariableRateLimit_1?(IC_Out1_364):(self->_reg.__VariableRateLimit_3)); |
| 488 |
/*@ |
|
| 489 |
ensures (*output_In1_489 == Integrator1_Out1_391); |
|
| 490 |
assigns *output_In1_489; */ |
|
| 491 |
{
|
|
| 468 | 492 |
*output_In1_489 = Integrator1_Out1_391; |
| 493 |
} |
|
| 469 | 494 |
Gain1_Out1_382 = (- ratelim_Out1_334); |
| 470 | 495 |
Sum2_Out1_401 = (input_Out1_344 + (- Integrator1_Out1_391)); |
| 471 | 496 |
Gain_Out1_373 = (20. * Sum2_Out1_401); |
| 497 |
/*@ |
|
| 498 |
ensures Ctrans_VariableLimitSaturation((double) ratelim_Out1_334, |
|
| 499 |
(double) Gain_Out1_373, |
|
| 500 |
(double) Gain1_Out1_382, |
|
| 501 |
Variable_Limit_Saturation_Out1_410); |
|
| 502 |
assigns Variable_Limit_Saturation_Out1_410; */ |
|
| 503 |
{
|
|
| 472 | 504 |
VariableLimitSaturation_step (ratelim_Out1_334, Gain_Out1_373, Gain1_Out1_382, &Variable_Limit_Saturation_Out1_410); |
| 505 |
} |
|
| 506 |
/*@ |
|
| 507 |
ensures Ctrans_integrator_reset((double) Variable_Limit_Saturation_Out1_410, |
|
| 508 |
(_Bool) ((ICtrig_Out1_354)), |
|
| 509 |
(double) IC_Out1_364, |
|
| 510 |
__VariableRateLimit_2, |
|
| 511 |
\at(*self, Pre).ni_2, |
|
| 512 |
(*self).ni_2); |
|
| 513 |
assigns __VariableRateLimit_2, self->ni_2; */ |
|
| 514 |
{
|
|
| 473 | 515 |
integrator_reset_step (Variable_Limit_Saturation_Out1_410, ICtrig_Out1_354, IC_Out1_364, &__VariableRateLimit_2, &self->ni_2); |
| 516 |
} |
|
| 474 | 517 |
self->_reg.__VariableRateLimit_3 = __VariableRateLimit_2; |
| 475 | 518 |
}}}}}return; |
| 476 | 519 |
} |
| ... | ... | |
| 524 | 567 |
x0, |
| 525 | 568 |
*ir_out, |
| 526 | 569 |
\at(*self, Pre), |
| 527 |
\at(*self, Here));
|
|
| 570 |
(*self));
|
|
| 528 | 571 |
assigns *ir_out, *self; |
| 529 | 572 |
*/ |
| 530 | 573 |
{
|
| ... | ... | |
| 538 | 581 |
x0, |
| 539 | 582 |
*ir_out, |
| 540 | 583 |
\at(*self, Pre), |
| 541 |
\at(*self, Here),
|
|
| 584 |
(*self),
|
|
| 542 | 585 |
__integrator_reset_1); |
| 543 | 586 |
assigns *ir_out, *self, __integrator_reset_1; |
| 544 | 587 |
*/ |
Also available in: Unified diff
ALT_2 working with modification made by hand