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

