/regression_tests/lustre_files/success/kind_fmcad08/large/TIMEOUT/microwave06.lus - Annotate - Lustrec-Tests

fa9e78e5

bourbouh

--@ ensures OK;

2

node top(KP_START: bool;

3

      KP_CLEAR: bool;

4

      KP_0: bool;

5

      KP_1: bool;

6

      KP_2: bool;

7

      KP_3: bool;

8

      KP_4: bool;

9

      KP_5: bool;

10

      KP_6: bool;

11

      KP_7: bool;

12

      KP_8: bool;

13

      KP_9: bool;

14

      DOOR_CLOSED: bool

15

) returns (OK:bool);

16

17

18

var

19

   LEFT_DIGIT: int;

20

      SETUP: bool;

21

      COOKING: bool;

22

      SUSPENDED: bool;

23

      START_PRESSED: bool;

24

      CLEAR_PRESSED: bool;

25

      MIDDLE_DIGIT: int;

26

      RIGHT_DIGIT: int;

27

      enable: bool;

28

      STEPS_TO_COOK: int;

29

30

   rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clock: bool;

31

   KP_01: bool;

32

   KP_11: bool;

33

   KP_21: bool;

34

   KP_31: bool;

35

   KP_41: bool;

36

   KP_51: bool;

37

   KP_61: bool;

38

   KP_71: bool;

39

   KP_81: bool;

40

   KP_91: bool;

41

   rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_init_step: bool;

42

   microwave_microwave_KEYPAD_PROCESSING_DISPLAY_LEFT_DIGIT_DIGIT_TO_DISPLAY: int;

43

   microwave_microwave_KEYPAD_PROCESSING_DISPLAY_MIDDLE_DIGIT_DIGIT_TO_DISPLAY: int;

44

   microwave_microwave_KEYPAD_PROCESSING_DISPLAY_RIGHT_DIGIT_DIGIT_TO_DISPLAY: int;

45

   rlt__Arrow5: int;

46

   rlt__Arrow4: int;

47

   rlt__Arrow3: int;

48

   rlt__Arrow2: int;

49

   rlt__Arrow1: int;

50

   rlt__Arrow: int;

51

   chart_microwave_mode_logic_start: int;

52

   chart_microwave_mode_logic_clear_off: int;

53

   chart_microwave_mode_logic_door_closed: int;

54

   chart_microwave_mode_logic____wakeup___: bool;

55

   rlt_eval_microwave_mode_logic_ON_rlt_fired_1: bool;

56

   rlt_eval_microwave_mode_logic_ON_rlt_state_1_states___root: int;

57

   rlt_eval_microwave_mode_logic_ON_rlt_state_2_states___root: int;

58

   rlt_eval_microwave_mode_logic_ON_rlt_fired_2: bool;

59

   rlt_eval_microwave_mode_logic_ON_rlt_complete_1: bool;

60

   rlt_eval_microwave_mode_logic_ON_rlt_state_3_states___root: int;

61

   rlt_eval_microwave_mode_logic_ON_rlt_state_3_outports_mode: int;

62

   rlt_eval_microwave_mode_logic_ON_rlt_state_4_states___root: int;

63

   rlt_eval_microwave_mode_logic_ON_rlt_state_4_outports_mode: int;

64

   rlt_eval_microwave_mode_logic_ON_rlt_fired_4: bool;

65

   rlt_eval_microwave_mode_logic_ON_rlt_complete_2: bool;

66

   rlt_eval_microwave_mode_logic_ON_rlt_state_6_states___root: int;

67

   rlt_eval_microwave_mode_logic_ON_rlt_state_6_outports_steps_remaining: int;

68

   rlt_eval_microwave_mode_logic_ON_rlt_state_7_states___root: int;

69

   rlt_eval_microwave_mode_logic_ON_rlt_fired_5: bool;

70

   rlt_eval_microwave_mode_logic_ON_rlt_state_8_outports_mode: int;

71

   rlt_eval_microwave_mode_logic_ON_rlt_state_9_states___root: int;

72

   rlt_eval_microwave_mode_logic_ON_rlt_state_10_states___root: int;

73

   rlt_eval_microwave_mode_logic_ON_rlt_fired_6: bool;

74

   rlt_eval_microwave_mode_logic_ON_rlt_state_11_states___root: int;

75

   rlt_eval_microwave_mode_logic_ON_rlt_state_11_outports_mode: int;

76

   rlt_enter_microwave_mode_logic_ON_rlt_state_1_states___root: int;

77

   rlt_enter_microwave_mode_logic_ON_rlt_fired_0: bool;

78

   rlt_enter_microwave_mode_logic_ON_rlt_fired_1: bool;

79

   rlt_enter_microwave_mode_logic_ON_rlt_state_2_states___root: int;

80

   rlt_enter_microwave_mode_logic_ON_rlt_state_2_outports_mode: int;

81

   rlt_enter_microwave_mode_logic_ON_rlt_fired_2: bool;

82

   rlt_enter_microwave_mode_logic_ON_rlt_state_4_states___root: int;

83

   rlt_eval_microwave_mode_logic_rlt_fired_0: bool;

84

   rlt_eval_microwave_mode_logic_rlt_state_1_outports_steps_remaining: int;

85

   rlt_eval_microwave_mode_logic_rlt_fired_1: bool;

86

   rlt_eval_microwave_mode_logic_rlt_state_2_states___root: int;

87

   rlt_eval_microwave_mode_logic_rlt_state_3_states___root: int;

88

   rlt_eval_microwave_mode_logic_rlt_state_3_outports_mode: int;

89

   rlt_enter_microwave_mode_logic_rlt_state_2_states___root: int;

90

   chart_microwave_mode_logic_rlt_evtInitStep: bool;

91

   chart_microwave_mode_logic_begin_state_states___root: int;

92

   chart_microwave_mode_logic_begin_state_outports_mode: int;

93

   chart_microwave_mode_logic_begin_state_outports_steps_remaining: int;

94

   chart_microwave_mode_logic_final_state_states___root: int;

95

   chart_microwave_mode_logic_mode: int;

96

   chart_microwave_mode_logic_steps_remaining: int;

97

   microwave_microwave_TIME_ON_DISPLAY_SECONDS_TO_MINUTES__QUOTIENT: int;

98

   microwave_microwave_TIME_ON_DISPLAY_SECONDS_TO_TENS__QUOTIENT: int;

99

   microwave_microwave_TIME_ON_DISPLAY_SECONDS_TO_TENS__REMAINDER: int;

100

   microwave_microwave_mode_logic_mode: int;

101

   MWI_FcnMaxI_In16: int;

102

   MWI_FcnMaxI_In15: int;

103

   MWI_FcnMaxI_In13: int;

104

   MWI_FcnMaxI_In12: int;

105

   MWI_FcnMaxI_In11: int;

106

   MWI_FcnMaxI_In1: int;

107

   p4: bool;

108

   p5: bool;

109

   p6: bool;

110

   p7: bool;

111

   p8: bool;

112

   p9: bool;

113

   p10: bool;

114

   p11: bool;

115

   p12: bool;

116

   p13: bool;

117

   p14: bool;

118

   p15: bool;

119

   p16: bool;

120

   p17: bool;

121

   p18: bool;

122

   p19: bool;

123

   p20: bool;

124

   p21: bool;

125

   p22: bool;

126

   p23: bool;

127

   p24: bool;

128

   p25: bool;

129

   p26: bool;

130

   p27: bool;

131

   p28: bool;

132

   p29: bool;

133

   p30: bool;

134

   p31: bool;

135

   p32: bool;

136

   p33: bool;

137

   p34: bool;

138

   p35: bool;

139

   p36: bool;

140

   p37: bool;

141

let

142

   rlt__Arrow5 = (639 ->

143

      (if (not (not SETUP))

144

         then

145

               (if (MWI_FcnMaxI_In13 > 0)

146

                  then MWI_FcnMaxI_In13

147

                  else 0)

148

         else 639));

149

150

   rlt__Arrow4 = (639 ->

151

      (if (not SUSPENDED)

152

         then

153

               (if (MWI_FcnMaxI_In12 > 0)

154

                  then MWI_FcnMaxI_In12

155

                  else 0)

156

         else 639));

157

158

   rlt__Arrow3 = (639 ->

159

      (if (not (not COOKING))

160

         then

161

               (if (MWI_FcnMaxI_In16 > 0)

162

                  then MWI_FcnMaxI_In16

163

                  else 0)

164

         else 639));

165

166

   rlt__Arrow2 = (639 ->

167

      (if (not (not SUSPENDED))

168

         then

169

               (if (MWI_FcnMaxI_In15 > 0)

170

                  then MWI_FcnMaxI_In15

171

                  else 0)

172

         else 639));

173

174

   rlt__Arrow1 = (639 ->

175

      (if (not COOKING)

176

         then

177

               (if (MWI_FcnMaxI_In11 > 0)

178

                  then MWI_FcnMaxI_In11

179

                  else 0)

180

         else 639));

181

182

   rlt__Arrow = (639 ->

183

      (if (not SETUP)

184

         then

185

               (if (MWI_FcnMaxI_In1 > 0)

186

                  then MWI_FcnMaxI_In1

187

                  else 0)

188

         else 639));

189

190

   p18 = (((not (enable and

191

      (not KP_CLEAR))) or

192

      ((not (((((((((KP_1 or

193

      KP_2) or

194

      KP_3) or

195

      KP_4) or

196

      KP_5) or

197

      KP_6) or

198

      KP_7) or

199

      KP_8) or

200

      KP_9) or

201

      KP_0)) or

202

      (LEFT_DIGIT = ((STEPS_TO_COOK div 1) div 60)))) -> ((not (enable and

203

      (not KP_CLEAR))) or

204

      ((not ((((((((((KP_1 and

205

      (not (pre KP_1))) or

206

      (KP_2 and

207

      (not (pre KP_2)))) or

208

      (KP_3 and

209

      (not (pre KP_3)))) or

210

      (KP_4 and

211

      (not (pre KP_4)))) or

212

      (KP_5 and

213

      (not (pre KP_5)))) or

214

      (KP_6 and

215

      (not (pre KP_6)))) or

216

      (KP_7 and

217

      (not (pre KP_7)))) or

218

      (KP_8 and

219

      (not (pre KP_8)))) or

220

      (KP_9 and

221

      (not (pre KP_9)))) or

222

      (KP_0 and

223

      (not (pre KP_0))))) or

224

      (LEFT_DIGIT = ((STEPS_TO_COOK div 1) div 60)))));

225

226

   p23 = (true -> (((not (enable and

227

      (not KP_CLEAR))) or

228

      (not ((((((((((KP_1 and

229

      (not (pre KP_1))) or

230

      (KP_2 and

231

      (not (pre KP_2)))) or

232

      (KP_3 and

233

      (not (pre KP_3)))) or

234

      (KP_4 and

235

      (not (pre KP_4)))) or

236

      (KP_5 and

237

      (not (pre KP_5)))) or

238

      (KP_6 and

239

      (not (pre KP_6)))) or

240

      (KP_7 and

241

      (not (pre KP_7)))) or

242

      (KP_8 and

243

      (not (pre KP_8)))) or

244

      (KP_9 and

245

      (not (pre KP_9)))) or

246

      (KP_0 and

247

      (not (pre KP_0)))))) or

248

      (MIDDLE_DIGIT = ((STEPS_TO_COOK - (STEPS_TO_COOK div 60)*60) div 10))));

249

250

   p35 = (true -> ((not (enable and

251

      (not KP_CLEAR))) or

252

      ((not ((KP_8 and

253

      (not (pre KP_8))) and

254

      ((not (KP_7 and

255

      (not (pre KP_7)))) and

256

      ((not (KP_6 and

257

      (not (pre KP_6)))) and

258

      ((not (KP_5 and

259

      (not (pre KP_5)))) and

260

      ((not (KP_4 and

261

      (not (pre KP_4)))) and

262

      ((not (KP_3 and

263

      (not (pre KP_3)))) and

264

      ((not (KP_2 and

265

      (not (pre KP_2)))) and

266

      ((not (KP_1 and

267

      (not (pre KP_1)))) and

268

      (not (KP_0 and

269

      (not (pre KP_0))))))))))))) or

270

      (RIGHT_DIGIT = 8))));

271

272

   p33 = (true -> ((not (enable and

273

      (not KP_CLEAR))) or

274

      ((not ((KP_6 and

275

      (not (pre KP_6))) and

276

      ((not (KP_5 and

277

      (not (pre KP_5)))) and

278

      ((not (KP_4 and

279

      (not (pre KP_4)))) and

280

      ((not (KP_3 and

281

      (not (pre KP_3)))) and

282

      ((not (KP_2 and

283

      (not (pre KP_2)))) and

284

      ((not (KP_1 and

285

      (not (pre KP_1)))) and

286

      (not (KP_0 and

287

      (not (pre KP_0))))))))))) or

288

      (RIGHT_DIGIT = 6))));

289

290

   MIDDLE_DIGIT = microwave_microwave_TIME_ON_DISPLAY_SECONDS_TO_TENS__QUOTIENT;

291

292

   RIGHT_DIGIT = microwave_microwave_TIME_ON_DISPLAY_SECONDS_TO_TENS__REMAINDER;

293

294

   p25 = (enable or

295

      (RIGHT_DIGIT = 0));

296

297

   p22 = (true -> (((not (enable and

298

      (not KP_CLEAR))) or

299

      (not ((((((((((KP_1 and

300

      (not (pre KP_1))) or

301

      (KP_2 and

302

      (not (pre KP_2)))) or

303

      (KP_3 and

304

      (not (pre KP_3)))) or

305

      (KP_4 and

306

      (not (pre KP_4)))) or

307

      (KP_5 and

308

      (not (pre KP_5)))) or

309

      (KP_6 and

310

      (not (pre KP_6)))) or

311

      (KP_7 and

312

      (not (pre KP_7)))) or

313

      (KP_8 and

314

      (not (pre KP_8)))) or

315

      (KP_9 and

316

      (not (pre KP_9)))) or

317

      (KP_0 and

318

      (not (pre KP_0)))))) or

319

      (MIDDLE_DIGIT = (pre RIGHT_DIGIT))));

320

321

   p36 = (true -> ((not (enable and

322

      (not KP_CLEAR))) or

323

      ((not ((KP_9 and

324

      (not (pre KP_9))) and

325

      ((not (KP_8 and

326

      (not (pre KP_8)))) and

327

      ((not (KP_7 and

328

      (not (pre KP_7)))) and

329

      ((not (KP_6 and

330

      (not (pre KP_6)))) and

331

      ((not (KP_5 and

332

      (not (pre KP_5)))) and

333

      ((not (KP_4 and

334

      (not (pre KP_4)))) and

335

      ((not (KP_3 and

336

      (not (pre KP_3)))) and

337

      ((not (KP_2 and

338

      (not (pre KP_2)))) and

339

      ((not (KP_1 and

340

      (not (pre KP_1)))) and

341

      (not (KP_0 and

342

      (not (pre KP_0)))))))))))))) or

343

      (RIGHT_DIGIT = 9))));

344

345

   MWI_FcnMaxI_In1 = ((pre rlt__Arrow) - 1);

346

347

   CLEAR_PRESSED = (KP_CLEAR -> (KP_CLEAR and

348

      (not (pre KP_CLEAR))));

349

350

   microwave_microwave_TIME_ON_DISPLAY_SECONDS_TO_MINUTES__QUOTIENT = ((chart_microwave_mode_logic_steps_remaining div 1) div 60);

351

352

   microwave_microwave_TIME_ON_DISPLAY_SECONDS_TO_TENS__REMAINDER = (((chart_microwave_mode_logic_steps_remaining div 1) - (((chart_microwave_mode_logic_steps_remaining div 1) div 60) * 60)) - ((((chart_microwave_mode_logic_steps_remaining div 1) - (((chart_microwave_mode_logic_steps_remaining div 1) div 60) * 60)) div 10) * 10));

353

354

   SUSPENDED =

355

      (if (3 = microwave_microwave_mode_logic_mode)

356

         then true

357

         else false);

358

359

   p31 = (true -> ((not (enable and

360

      (not KP_CLEAR))) or

361

      ((not ((KP_4 and

362

      (not (pre KP_4))) and

363

      ((not (KP_3 and

364

      (not (pre KP_3)))) and

365

      ((not (KP_2 and

366

      (not (pre KP_2)))) and

367

      ((not (KP_1 and

368

      (not (pre KP_1)))) and

369

      (not (KP_0 and

370

      (not (pre KP_0))))))))) or

371

      (RIGHT_DIGIT = 4))));

372

373

   p37 = (true -> ((not (enable and

374

      (not KP_CLEAR))) or

375

      (((((((((((KP_1 and

376

      (not (pre KP_1))) or

377

      (KP_2 and

378

      (not (pre KP_2)))) or

379

      (KP_3 and

380

      (not (pre KP_3)))) or

381

      (KP_4 and

382

      (not (pre KP_4)))) or

383

      (KP_5 and

384

      (not (pre KP_5)))) or

385

      (KP_6 and

386

      (not (pre KP_6)))) or

387

      (KP_7 and

388

      (not (pre KP_7)))) or

389

      (KP_8 and

390

      (not (pre KP_8)))) or

391

      (KP_9 and

392

      (not (pre KP_9)))) or

393

      (KP_0 and

394

      (not (pre KP_0)))) or

395

      (RIGHT_DIGIT = (pre RIGHT_DIGIT)))));

396

397

   MWI_FcnMaxI_In11 = ((pre rlt__Arrow1) - 1);

398

399

   p4 = (true -> (

400

      (if (not COOKING)

401

         then

402

               (if (MWI_FcnMaxI_In11 > 0)

403

                  then MWI_FcnMaxI_In11

404

                  else 0)

405

         else 639) > 0));

406

407

   MWI_FcnMaxI_In15 = ((pre rlt__Arrow2) - 1);

408

409

   p24 = (true -> (((not (enable and

410

      (not KP_CLEAR))) or

411

      ((((((((((KP_1 and

412

      (not (pre KP_1))) or

413

      (KP_2 and

414

      (not (pre KP_2)))) or

415

      (KP_3 and

416

      (not (pre KP_3)))) or

417

      (KP_4 and

418

      (not (pre KP_4)))) or

419

      (KP_5 and

420

      (not (pre KP_5)))) or

421

      (KP_6 and

422

      (not (pre KP_6)))) or

423

      (KP_7 and

424

      (not (pre KP_7)))) or

425

      (KP_8 and

426

      (not (pre KP_8)))) or

427

      (KP_9 and

428

      (not (pre KP_9)))) or

429

      (KP_0 and

430

      (not (pre KP_0))))) or

431

      (MIDDLE_DIGIT = (pre MIDDLE_DIGIT))));

432

433

   p20 = (enable or

434

      (MIDDLE_DIGIT = 0));

435

436

   p5 = (true -> (

437

      (if (not SUSPENDED)

438

         then

439

               (if (MWI_FcnMaxI_In12 > 0)

440

                  then MWI_FcnMaxI_In12

441

                  else 0)

442

         else 639) > 0));

443

444

   p26 = ((not (enable and

445

      KP_CLEAR)) or

446

      (RIGHT_DIGIT = 0));

447

448

   microwave_microwave_TIME_ON_DISPLAY_SECONDS_TO_TENS__QUOTIENT = (((chart_microwave_mode_logic_steps_remaining div 1) - (((chart_microwave_mode_logic_steps_remaining div 1) div 60) * 60)) div 10);

449

450

   p14 = (true -> ((not (enable and

451

      (not KP_CLEAR))) or

452

      (STEPS_TO_COOK = (((RIGHT_DIGIT + (MIDDLE_DIGIT * 10)) + (LEFT_DIGIT * 60)) * 1))));

453

454

   MWI_FcnMaxI_In16 = ((pre rlt__Arrow3) - 1);

455

456

   p6 = (true -> ((not SETUP) or

457

458

      (if (not (not SETUP))

459

         then

460

               (if (MWI_FcnMaxI_In13 > 0)

461

                  then MWI_FcnMaxI_In13

462

                  else 0)

463

         else 639) > 0)));

464

465

   p8 = (true -> ((not SUSPENDED) or

466

467

      (if (not (not SUSPENDED))

468

         then

469

               (if (MWI_FcnMaxI_In15 > 0)

470

                  then MWI_FcnMaxI_In15

471

                  else 0)

472

         else 639) > 0)));

473

474

   p7 = (true -> ((not COOKING) or

475

476

      (if (not (not COOKING))

477

         then

478

               (if (MWI_FcnMaxI_In16 > 0)

479

                  then MWI_FcnMaxI_In16

480

                  else 0)

481

         else 639) > 0)));

482

483

   MWI_FcnMaxI_In12 = ((pre rlt__Arrow4) - 1);

484

485

   p16 = ((not (enable and

486

      KP_CLEAR)) or

487

      (LEFT_DIGIT = 0));

488

489

   p30 = (true -> ((not (enable and

490

      (not KP_CLEAR))) or

491

      ((not ((KP_3 and

492

      (not (pre KP_3))) and

493

      ((not (KP_2 and

494

      (not (pre KP_2)))) and

495

      ((not (KP_1 and

496

      (not (pre KP_1)))) and

497

      (not (KP_0 and

498

      (not (pre KP_0)))))))) or

499

      (RIGHT_DIGIT = 3))));

500

501

   COOKING =

502

      (if (2 = microwave_microwave_mode_logic_mode)

503

         then true

504

         else false);

505

506

   LEFT_DIGIT = microwave_microwave_TIME_ON_DISPLAY_SECONDS_TO_MINUTES__QUOTIENT;

507

508

   p11 = ((not KP_CLEAR) or

509

      (not COOKING));

510

511

   p9 = (true -> ((not COOKING) or

512

      DOOR_CLOSED));

513

514

   p15 = (enable or

515

      (LEFT_DIGIT = 0));

516

517

   START_PRESSED = (KP_START -> (KP_START and

518

      (not (pre KP_START))));

519

520

   chart_microwave_mode_logic_start =

521

      (if (START_PRESSED = false)

522

         then 0

523

         else 1);

524

525

   chart_microwave_mode_logic_clear_off =

526

      (if (CLEAR_PRESSED = false)

527

         then 0

528

         else 1);

529

530

   chart_microwave_mode_logic_door_closed =

531

      (if (DOOR_CLOSED = false)

532

         then 0

533

         else 1);

534

535

   chart_microwave_mode_logic____wakeup___ = true;

536

537

   chart_microwave_mode_logic_rlt_evtInitStep = (true ->

538

      (if (pre chart_microwave_mode_logic____wakeup___)

539

         then false

540

         else (pre chart_microwave_mode_logic_rlt_evtInitStep)));

541

542

   chart_microwave_mode_logic_begin_state_states___root = (0 -> (pre chart_microwave_mode_logic_final_state_states___root));

543

544

   chart_microwave_mode_logic_begin_state_outports_mode = (0 -> (pre chart_microwave_mode_logic_mode));

545

546

   chart_microwave_mode_logic_begin_state_outports_steps_remaining = (0 -> (pre chart_microwave_mode_logic_steps_remaining));

547

548

   chart_microwave_mode_logic_final_state_states___root =

549

      (if chart_microwave_mode_logic____wakeup___

550

         then

551

               (if chart_microwave_mode_logic_rlt_evtInitStep

552

                  then rlt_enter_microwave_mode_logic_rlt_state_2_states___root

553

                  else

554

               (if ((not rlt_eval_microwave_mode_logic_rlt_fired_1) and

555

556

557

                  ((rlt_eval_microwave_mode_logic_rlt_state_3_states___root >= 1) and

558

                  (rlt_eval_microwave_mode_logic_rlt_state_3_states___root <= 3)))

559

                  then

560

                        (if rlt_eval_microwave_mode_logic_ON_rlt_fired_6

561

                           then

562

                                 (if (not (rlt_eval_microwave_mode_logic_ON_rlt_state_11_states___root = 3))

563

                                    then

564

565

566

                                    else rlt_eval_microwave_mode_logic_ON_rlt_state_11_states___root)

567

                           else rlt_eval_microwave_mode_logic_ON_rlt_state_11_states___root)

568

                  else rlt_eval_microwave_mode_logic_rlt_state_3_states___root))

569

         else chart_microwave_mode_logic_begin_state_states___root);

570

571

   chart_microwave_mode_logic_mode =

572

      (if chart_microwave_mode_logic____wakeup___

573

         then

574

               (if chart_microwave_mode_logic_rlt_evtInitStep

575

                  then

576

                        (if (not (chart_microwave_mode_logic_begin_state_states___root = 4))

577

                           then 1

578

                           else chart_microwave_mode_logic_begin_state_outports_mode)

579

                  else

580

               (if ((not rlt_eval_microwave_mode_logic_rlt_fired_1) and

581

582

583

                  ((rlt_eval_microwave_mode_logic_rlt_state_3_states___root >= 1) and

584

                  (rlt_eval_microwave_mode_logic_rlt_state_3_states___root <= 3)))

585

                  then

586

                        (if rlt_eval_microwave_mode_logic_ON_rlt_fired_6

587

                           then

588

                                 (if (not (rlt_eval_microwave_mode_logic_ON_rlt_state_11_states___root = 3))

589

                                    then 3

590

                                    else rlt_eval_microwave_mode_logic_ON_rlt_state_11_outports_mode)

591

                           else rlt_eval_microwave_mode_logic_ON_rlt_state_11_outports_mode)

592

                  else rlt_eval_microwave_mode_logic_rlt_state_3_outports_mode))

593

         else chart_microwave_mode_logic_begin_state_outports_mode);

594

595

   chart_microwave_mode_logic_steps_remaining =

596

      (if chart_microwave_mode_logic____wakeup___

597

         then

598

               (if chart_microwave_mode_logic_rlt_evtInitStep

599

                  then chart_microwave_mode_logic_begin_state_outports_steps_remaining

600

                  else

601

               (if ((not rlt_eval_microwave_mode_logic_rlt_fired_1) and

602

603

604

                  ((rlt_eval_microwave_mode_logic_rlt_state_3_states___root >= 1) and

605

                  (rlt_eval_microwave_mode_logic_rlt_state_3_states___root <= 3)))

606

                  then

607

                        (if rlt_eval_microwave_mode_logic_ON_rlt_fired_5

608

                           then (rlt_eval_microwave_mode_logic_ON_rlt_state_6_outports_steps_remaining - 1)

609

                           else rlt_eval_microwave_mode_logic_ON_rlt_state_6_outports_steps_remaining)

610

                  else rlt_eval_microwave_mode_logic_rlt_state_1_outports_steps_remaining))

611

         else chart_microwave_mode_logic_begin_state_outports_steps_remaining);

   rlt_eval_microwave_mode_logic_rlt_fired_0 = (chart_microwave_mode_logic_begin_state_states___root = 4);

   rlt_eval_microwave_mode_logic_rlt_state_1_outports_steps_remaining =

620

      (if rlt_eval_microwave_mode_logic_rlt_fired_0

621

         then STEPS_TO_COOK

622

         else chart_microwave_mode_logic_begin_state_outports_steps_remaining);

623

624

625

   rlt_eval_microwave_mode_logic_rlt_fired_1 = (rlt_eval_microwave_mode_logic_rlt_fired_0 and

626

      ((chart_microwave_mode_logic_begin_state_states___root = 4) and

627

628

      (if (chart_microwave_mode_logic_start <> 0)

629

         then true

630

         else false) and

631

632

      (if (

633

         (if ((STEPS_TO_COOK > 0) = false)

634

            then 0

635

            else 1) <> 0)

636

         then true

637

         else false))));

   rlt_eval_microwave_mode_logic_rlt_state_2_states___root =

642

      (if rlt_eval_microwave_mode_logic_rlt_fired_1

643

         then

644

               (if (chart_microwave_mode_logic_begin_state_states___root = 4)

645

                  then

646

647

648

                  else chart_microwave_mode_logic_begin_state_states___root)

649

         else chart_microwave_mode_logic_begin_state_states___root);

   rlt_eval_microwave_mode_logic_rlt_state_3_states___root =

654

      (if rlt_eval_microwave_mode_logic_rlt_fired_1

655

         then rlt_enter_microwave_mode_logic_ON_rlt_state_4_states___root

656

         else rlt_eval_microwave_mode_logic_rlt_state_2_states___root);

   rlt_eval_microwave_mode_logic_rlt_state_3_outports_mode =

663

      (if rlt_eval_microwave_mode_logic_rlt_fired_1

664

         then

665

               (if rlt_enter_microwave_mode_logic_ON_rlt_fired_2

666

                  then

667

                        (if (not (rlt_enter_microwave_mode_logic_ON_rlt_state_2_states___root = 3))

668

                           then 3

669

                           else rlt_enter_microwave_mode_logic_ON_rlt_state_2_outports_mode)

670

                  else rlt_enter_microwave_mode_logic_ON_rlt_state_2_outports_mode)

671

         else chart_microwave_mode_logic_begin_state_outports_mode);

   rlt_eval_microwave_mode_logic_ON_rlt_fired_1 = (((rlt_eval_microwave_mode_logic_rlt_state_3_states___root = 2) and

677

      (rlt_eval_microwave_mode_logic_rlt_state_1_outports_steps_remaining <= 0)) and

678

      (rlt_eval_microwave_mode_logic_rlt_state_3_states___root = 2));

   rlt_eval_microwave_mode_logic_ON_rlt_state_1_states___root =

683

      (if rlt_eval_microwave_mode_logic_ON_rlt_fired_1

684

         then

685

(if

686

687

                  ((rlt_eval_microwave_mode_logic_rlt_state_3_states___root >= 1) and

688

                  (rlt_eval_microwave_mode_logic_rlt_state_3_states___root <= 3))

689

                  then

690

691

692

                  else rlt_eval_microwave_mode_logic_rlt_state_3_states___root)

693

         else rlt_eval_microwave_mode_logic_rlt_state_3_states___root);

   rlt_eval_microwave_mode_logic_ON_rlt_state_2_states___root =

698

      (if rlt_eval_microwave_mode_logic_ON_rlt_fired_1

699

         then

700

               (if (not (rlt_eval_microwave_mode_logic_ON_rlt_state_1_states___root = 4))

701

                  then

702

703

704

                  else rlt_eval_microwave_mode_logic_ON_rlt_state_1_states___root)

705

         else rlt_eval_microwave_mode_logic_ON_rlt_state_1_states___root);

   rlt_eval_microwave_mode_logic_ON_rlt_fired_2 = ((rlt_eval_microwave_mode_logic_ON_rlt_state_2_states___root = 3) and

712

((

713

      (if (chart_microwave_mode_logic_start <> 0)

714

         then true

715

         else false) and

716

717

      (if (chart_microwave_mode_logic_door_closed <> 0)

718

         then true

719

         else false)) and

720

      (not rlt_eval_microwave_mode_logic_ON_rlt_fired_1)));

   rlt_eval_microwave_mode_logic_ON_rlt_complete_1 = (rlt_eval_microwave_mode_logic_ON_rlt_fired_2 or

725

      rlt_eval_microwave_mode_logic_ON_rlt_fired_1);

   rlt_eval_microwave_mode_logic_ON_rlt_state_3_states___root =

730

      (if rlt_eval_microwave_mode_logic_ON_rlt_fired_2

731

         then

732

               (if (rlt_eval_microwave_mode_logic_ON_rlt_state_2_states___root = 3)

733

                  then

734

735

736

                  else rlt_eval_microwave_mode_logic_ON_rlt_state_2_states___root)

737

         else rlt_eval_microwave_mode_logic_ON_rlt_state_2_states___root);

   rlt_eval_microwave_mode_logic_ON_rlt_state_3_outports_mode =

742

      (if rlt_eval_microwave_mode_logic_ON_rlt_fired_1

743

         then

744

               (if (not (rlt_eval_microwave_mode_logic_ON_rlt_state_1_states___root = 4))

745

                  then 1

746

                  else rlt_eval_microwave_mode_logic_rlt_state_3_outports_mode)

747

         else rlt_eval_microwave_mode_logic_rlt_state_3_outports_mode);

   rlt_eval_microwave_mode_logic_ON_rlt_state_4_states___root =

752

      (if rlt_eval_microwave_mode_logic_ON_rlt_fired_2

753

         then

754

               (if (not (rlt_eval_microwave_mode_logic_ON_rlt_state_3_states___root = 2))

755

                  then

756

757

758

                  else rlt_eval_microwave_mode_logic_ON_rlt_state_3_states___root)

759

         else rlt_eval_microwave_mode_logic_ON_rlt_state_3_states___root);

   rlt_eval_microwave_mode_logic_ON_rlt_state_4_outports_mode =

766

      (if rlt_eval_microwave_mode_logic_ON_rlt_fired_2

767

         then

768

               (if (not (rlt_eval_microwave_mode_logic_ON_rlt_state_3_states___root = 2))

769

                  then 2

770

                  else rlt_eval_microwave_mode_logic_ON_rlt_state_3_outports_mode)

771

         else rlt_eval_microwave_mode_logic_ON_rlt_state_3_outports_mode);

   rlt_eval_microwave_mode_logic_ON_rlt_fired_4 = (((rlt_eval_microwave_mode_logic_ON_rlt_state_4_states___root = 3) and

777

778

      (if (chart_microwave_mode_logic_clear_off <> 0)

779

         then true

780

         else false) and

781

      (not rlt_eval_microwave_mode_logic_ON_rlt_complete_1))) and

782

      ((rlt_eval_microwave_mode_logic_ON_rlt_state_4_states___root = 3) and

783

      (not rlt_eval_microwave_mode_logic_ON_rlt_complete_1)));

   rlt_eval_microwave_mode_logic_ON_rlt_complete_2 = (rlt_eval_microwave_mode_logic_ON_rlt_fired_4 or

788

      rlt_eval_microwave_mode_logic_ON_rlt_complete_1);

   rlt_eval_microwave_mode_logic_ON_rlt_state_6_states___root =

793

      (if rlt_eval_microwave_mode_logic_ON_rlt_fired_4

794

         then

795

(if

796

797

                  ((rlt_eval_microwave_mode_logic_ON_rlt_state_4_states___root >= 1) and

798

                  (rlt_eval_microwave_mode_logic_ON_rlt_state_4_states___root <= 3))

799

                  then

800

801

802

                  else rlt_eval_microwave_mode_logic_ON_rlt_state_4_states___root)

803

         else rlt_eval_microwave_mode_logic_ON_rlt_state_4_states___root);

   rlt_eval_microwave_mode_logic_ON_rlt_state_6_outports_steps_remaining =

808

      (if rlt_eval_microwave_mode_logic_ON_rlt_fired_4

809

         then 0

810

         else rlt_eval_microwave_mode_logic_rlt_state_1_outports_steps_remaining);

   rlt_eval_microwave_mode_logic_ON_rlt_state_7_states___root =

815

      (if rlt_eval_microwave_mode_logic_ON_rlt_fired_4

816

         then

817

               (if (not (rlt_eval_microwave_mode_logic_ON_rlt_state_6_states___root = 4))

818

                  then

819

820

821

                  else rlt_eval_microwave_mode_logic_ON_rlt_state_6_states___root)

822

         else rlt_eval_microwave_mode_logic_ON_rlt_state_6_states___root);

   rlt_eval_microwave_mode_logic_ON_rlt_fired_5 = ((rlt_eval_microwave_mode_logic_ON_rlt_state_7_states___root = 2) and

829

      ((rlt_eval_microwave_mode_logic_ON_rlt_state_6_outports_steps_remaining > 0) and

830

      (not rlt_eval_microwave_mode_logic_ON_rlt_complete_2)));

   rlt_eval_microwave_mode_logic_ON_rlt_state_8_outports_mode =

835

      (if rlt_eval_microwave_mode_logic_ON_rlt_fired_4

836

         then

837

               (if (not (rlt_eval_microwave_mode_logic_ON_rlt_state_6_states___root = 4))

838

                  then 1

839

                  else rlt_eval_microwave_mode_logic_ON_rlt_state_4_outports_mode)

840

         else rlt_eval_microwave_mode_logic_ON_rlt_state_4_outports_mode);

   rlt_eval_microwave_mode_logic_ON_rlt_state_9_states___root =

845

      (if rlt_eval_microwave_mode_logic_ON_rlt_fired_5

846

         then

847

               (if (rlt_eval_microwave_mode_logic_ON_rlt_state_7_states___root = 2)

848

                  then

849

850

851

                  else rlt_eval_microwave_mode_logic_ON_rlt_state_7_states___root)

852

         else rlt_eval_microwave_mode_logic_ON_rlt_state_7_states___root);

   rlt_eval_microwave_mode_logic_ON_rlt_state_10_states___root =

857

      (if rlt_eval_microwave_mode_logic_ON_rlt_fired_5

858

         then

859

               (if (not (rlt_eval_microwave_mode_logic_ON_rlt_state_9_states___root = 2))

860

                  then

861

862

863

                  else rlt_eval_microwave_mode_logic_ON_rlt_state_9_states___root)

864

         else rlt_eval_microwave_mode_logic_ON_rlt_state_9_states___root);

   rlt_eval_microwave_mode_logic_ON_rlt_fired_6 = ((rlt_eval_microwave_mode_logic_ON_rlt_state_10_states___root = 2) and

871

((

872

      (if (chart_microwave_mode_logic_clear_off <> 0)

873

         then true

874

         else false) or

875

      (not

876

      (if (chart_microwave_mode_logic_door_closed <> 0)

877

         then true

878

         else false))) and

879

      (not (rlt_eval_microwave_mode_logic_ON_rlt_fired_5 or

880

      rlt_eval_microwave_mode_logic_ON_rlt_complete_2))));

   rlt_eval_microwave_mode_logic_ON_rlt_state_11_states___root =

885

      (if rlt_eval_microwave_mode_logic_ON_rlt_fired_6

886

         then

887

               (if (rlt_eval_microwave_mode_logic_ON_rlt_state_10_states___root = 2)

888

                  then

889

890

891

                  else rlt_eval_microwave_mode_logic_ON_rlt_state_10_states___root)

892

         else rlt_eval_microwave_mode_logic_ON_rlt_state_10_states___root);

   rlt_eval_microwave_mode_logic_ON_rlt_state_11_outports_mode =

897

      (if rlt_eval_microwave_mode_logic_ON_rlt_fired_5

898

         then

899

               (if (not (rlt_eval_microwave_mode_logic_ON_rlt_state_9_states___root = 2))

900

                  then 2

901

                  else rlt_eval_microwave_mode_logic_ON_rlt_state_8_outports_mode)

902

         else rlt_eval_microwave_mode_logic_ON_rlt_state_8_outports_mode);

903

904

   rlt_enter_microwave_mode_logic_ON_rlt_state_1_states___root =

905

      (if (not

906

907

         ((rlt_eval_microwave_mode_logic_rlt_state_2_states___root >= 1) and

908

         (rlt_eval_microwave_mode_logic_rlt_state_2_states___root <= 3)))

909

         then

910

911

912

         else rlt_eval_microwave_mode_logic_rlt_state_2_states___root);

   rlt_enter_microwave_mode_logic_ON_rlt_fired_0 = ((not

917

918

      ((rlt_eval_microwave_mode_logic_rlt_state_2_states___root >= 1) and

919

      (rlt_eval_microwave_mode_logic_rlt_state_2_states___root <= 3))) and

920

921

922

      ((rlt_enter_microwave_mode_logic_ON_rlt_state_1_states___root >= 1) and

923

      (rlt_enter_microwave_mode_logic_ON_rlt_state_1_states___root <= 3)));

924

925

926

   rlt_enter_microwave_mode_logic_ON_rlt_fired_1 = (rlt_enter_microwave_mode_logic_ON_rlt_fired_0 and

927

928

929

      ((rlt_enter_microwave_mode_logic_ON_rlt_state_1_states___root >= 1) and

930

      (rlt_enter_microwave_mode_logic_ON_rlt_state_1_states___root <= 3)) and

931

932

      (if (chart_microwave_mode_logic_door_closed <> 0)

933

         then true

934

         else false)));

   rlt_enter_microwave_mode_logic_ON_rlt_state_2_states___root =

939

      (if rlt_enter_microwave_mode_logic_ON_rlt_fired_1

940

         then

941

               (if (not (rlt_enter_microwave_mode_logic_ON_rlt_state_1_states___root = 2))

942

                  then

943

944

945

                  else rlt_enter_microwave_mode_logic_ON_rlt_state_1_states___root)

946

         else rlt_enter_microwave_mode_logic_ON_rlt_state_1_states___root);

   rlt_enter_microwave_mode_logic_ON_rlt_state_2_outports_mode =

953

      (if rlt_enter_microwave_mode_logic_ON_rlt_fired_1

954

         then

955

               (if (not (rlt_enter_microwave_mode_logic_ON_rlt_state_1_states___root = 2))

956

                  then 2

957

                  else chart_microwave_mode_logic_begin_state_outports_mode)

958

         else chart_microwave_mode_logic_begin_state_outports_mode);

   rlt_enter_microwave_mode_logic_ON_rlt_fired_2 = (rlt_enter_microwave_mode_logic_ON_rlt_fired_0 and

965

966

967

      ((rlt_enter_microwave_mode_logic_ON_rlt_state_2_states___root >= 1) and

968

      (rlt_enter_microwave_mode_logic_ON_rlt_state_2_states___root <= 3)) and

969

      (not rlt_enter_microwave_mode_logic_ON_rlt_fired_1)));

   rlt_enter_microwave_mode_logic_ON_rlt_state_4_states___root =

974

      (if rlt_enter_microwave_mode_logic_ON_rlt_fired_2

975

         then

976

               (if (not (rlt_enter_microwave_mode_logic_ON_rlt_state_2_states___root = 3))

977

                  then

978

979

980

                  else rlt_enter_microwave_mode_logic_ON_rlt_state_2_states___root)

981

         else rlt_enter_microwave_mode_logic_ON_rlt_state_2_states___root);

   rlt_enter_microwave_mode_logic_rlt_state_2_states___root =

988

      (if (not (chart_microwave_mode_logic_begin_state_states___root = 4))

989

         then

990

991

992

         else chart_microwave_mode_logic_begin_state_states___root);

   microwave_microwave_mode_logic_mode = chart_microwave_mode_logic_mode;

997

998

   p17 = (((not (enable and

999

      (not KP_CLEAR))) or

1000

      ((not (((((((((KP_1 or

1001

      KP_2) or

1002

      KP_3) or

1003

      KP_4) or

1004

      KP_5) or

1005

      KP_6) or

1006

      KP_7) or

1007

      KP_8) or

1008

      KP_9) or

1009

      KP_0)) or

1010

      (LEFT_DIGIT = 0))) -> ((not (enable and

1011

      (not KP_CLEAR))) or

1012

      ((not ((((((((((KP_1 and

1013

      (not (pre KP_1))) or

1014

      (KP_2 and

1015

      (not (pre KP_2)))) or

1016

      (KP_3 and

1017

      (not (pre KP_3)))) or

1018

      (KP_4 and

1019

      (not (pre KP_4)))) or

1020

      (KP_5 and

1021

      (not (pre KP_5)))) or

1022

      (KP_6 and

1023

      (not (pre KP_6)))) or

1024

      (KP_7 and

1025

      (not (pre KP_7)))) or

1026

      (KP_8 and

1027

      (not (pre KP_8)))) or

1028

      (KP_9 and

1029

      (not (pre KP_9)))) or

1030

      (KP_0 and

1031

      (not (pre KP_0))))) or

1032

      (LEFT_DIGIT = (pre MIDDLE_DIGIT)))));

1033

1034

   MWI_FcnMaxI_In13 = ((pre rlt__Arrow5) - 1);

1035

1036

   p10 = (true -> ((not COOKING) or

1037

1038

      (if (not (not COOKING))

1039

         then

1040

               (if (MWI_FcnMaxI_In16 > 0)

1041

                  then MWI_FcnMaxI_In16

1042

                  else 0)

1043

         else 639) > 0)));

1044

1045

   p27 = (((not (enable and

1046

      (not KP_CLEAR))) or

1047

      ((not KP_0) or

1048

      (RIGHT_DIGIT = 0))) -> ((not (enable and

1049

      (not KP_CLEAR))) or

1050

      ((not (KP_0 and

1051

      (not (pre KP_0)))) or

1052

      (RIGHT_DIGIT = 0))));

1053

1054

   rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clock = enable;

1055

1056

   KP_01 = KP_0;

1057

1058

   KP_11 = KP_1;

1059

1060

   KP_21 = KP_2;

1061

1062

   KP_31 = KP_3;

1063

1064

   KP_41 = KP_4;

1065

1066

   KP_51 = KP_5;

1067

1068

   KP_61 = KP_6;

1069

1070

   KP_71 = KP_7;

1071

1072

   KP_81 = KP_8;

1073

1074

   KP_91 = KP_9;

1075

1076

   microwave_microwave_KEYPAD_PROCESSING_DISPLAY_LEFT_DIGIT_DIGIT_TO_DISPLAY = (0 ->

1077

      (if rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clock

1078

         then

1079

               (if rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_init_step

1080

                  then 0

1081

                  else

1082

               (if KP_CLEAR

1083

                  then 0

1084

                  else

1085

(if

1086

                  (if (

1087

                     (if (KP_01 and

1088

                        (not (pre KP_01)))

1089

                        then 0

1090

                        else

1091

                     (if (KP_11 and

1092

                        (not (pre KP_11)))

1093

                        then 1

1094

                        else

1095

                     (if (KP_21 and

1096

                        (not (pre KP_21)))

1097

                        then 2

1098

                        else

1099

                     (if (KP_31 and

1100

                        (not (pre KP_31)))

1101

                        then 3

1102

                        else

1103

                     (if (KP_41 and

1104

                        (not (pre KP_41)))

1105

                        then 4

1106

                        else

1107

                     (if (KP_51 and

1108

                        (not (pre KP_51)))

1109

                        then 5

1110

                        else

1111

                     (if (KP_61 and

1112

                        (not (pre KP_61)))

1113

                        then 6

1114

                        else

1115

                     (if (KP_71 and

1116

                        (not (pre KP_71)))

1117

                        then 7

1118

                        else

1119

                     (if (KP_81 and

1120

                        (not (pre KP_81)))

1121

                        then 8

1122

                        else

1123

                     (if (KP_91 and

1124

                        (not (pre KP_91)))

1125

                        then 9

1126

                        else 10)))))))))) <= 9)

1127

                     then true

1128

                     else false)

1129

                  then (pre microwave_microwave_KEYPAD_PROCESSING_DISPLAY_MIDDLE_DIGIT_DIGIT_TO_DISPLAY)

1130

                  else (pre microwave_microwave_KEYPAD_PROCESSING_DISPLAY_LEFT_DIGIT_DIGIT_TO_DISPLAY))))

1131

         else (pre microwave_microwave_KEYPAD_PROCESSING_DISPLAY_LEFT_DIGIT_DIGIT_TO_DISPLAY)));

1132

1133

   microwave_microwave_KEYPAD_PROCESSING_DISPLAY_MIDDLE_DIGIT_DIGIT_TO_DISPLAY = (0 ->

1134

      (if rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clock

1135

         then

1136

               (if rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_init_step

1137

                  then 0

1138

                  else

1139

               (if KP_CLEAR

1140

                  then 0

1141

                  else

1142

(if

1143

                  (if (

1144

                     (if (KP_01 and

1145

                        (not (pre KP_01)))

1146

                        then 0

1147

                        else

1148

                     (if (KP_11 and

1149

                        (not (pre KP_11)))

1150

                        then 1

1151

                        else

1152

                     (if (KP_21 and

1153

                        (not (pre KP_21)))

1154

                        then 2

1155

                        else

1156

                     (if (KP_31 and

1157

                        (not (pre KP_31)))

1158

                        then 3

1159

                        else

1160

                     (if (KP_41 and

1161

                        (not (pre KP_41)))

1162

                        then 4

1163

                        else

1164

                     (if (KP_51 and

1165

                        (not (pre KP_51)))

1166

                        then 5

1167

                        else

1168

                     (if (KP_61 and

1169

                        (not (pre KP_61)))

1170

                        then 6

1171

                        else

1172

                     (if (KP_71 and

1173

                        (not (pre KP_71)))

1174

                        then 7

1175

                        else

1176

                     (if (KP_81 and

1177

                        (not (pre KP_81)))

1178

                        then 8

1179

                        else

1180

                     (if (KP_91 and

1181

                        (not (pre KP_91)))

1182

                        then 9

1183

                        else 10)))))))))) <= 9)

1184

                     then true

1185

                     else false)

1186

                  then (pre microwave_microwave_KEYPAD_PROCESSING_DISPLAY_RIGHT_DIGIT_DIGIT_TO_DISPLAY)

1187

                  else (pre microwave_microwave_KEYPAD_PROCESSING_DISPLAY_MIDDLE_DIGIT_DIGIT_TO_DISPLAY))))

1188

         else (pre microwave_microwave_KEYPAD_PROCESSING_DISPLAY_MIDDLE_DIGIT_DIGIT_TO_DISPLAY)));

1189

1190

   microwave_microwave_KEYPAD_PROCESSING_DISPLAY_RIGHT_DIGIT_DIGIT_TO_DISPLAY = (

1191

      (if KP_CLEAR

1192

         then 0

1193

         else

1194

(if

1195

         (if (

1196

            (if KP_01

1197

               then 0

1198

               else

1199

            (if KP_11

1200

               then 1

1201

               else

1202

            (if KP_21

1203

               then 2

1204

               else

1205

            (if KP_31

1206

               then 3

1207

               else

1208

            (if KP_41

1209

               then 4

1210

               else

1211

            (if KP_51

1212

               then 5

1213

               else

1214

            (if KP_61

1215

               then 6

1216

               else

1217

            (if KP_71

1218

               then 7

1219

               else

1220

            (if KP_81

1221

               then 8

1222

               else

1223

            (if KP_91

1224

               then 9

1225

               else 10)))))))))) <= 9)

1226

            then true

1227

            else false)

1228

         then

1229

               (if KP_01

1230

                  then 0

1231

                  else

1232

               (if KP_11

1233

                  then 1

1234

                  else

1235

               (if KP_21

1236

                  then 2

1237

                  else

1238

               (if KP_31

1239

                  then 3

1240

                  else

1241

               (if KP_41

1242

                  then 4

1243

                  else

1244

               (if KP_51

1245

                  then 5

1246

                  else

1247

               (if KP_61

1248

                  then 6

1249

                  else

1250

               (if KP_71

1251

                  then 7

1252

                  else

1253

               (if KP_81

1254

                  then 8

1255

                  else

1256

               (if KP_91

1257

                  then 9

1258

                  else 10))))))))))

1259

         else 0)) ->

1260

      (if rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clock

1261

         then

1262

               (if rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_init_step

1263

                  then

1264

                        (if KP_CLEAR

1265

                           then 0

1266

                           else

1267

(if

1268

                           (if (

1269

                              (if KP_01

1270

                                 then 0

1271

                                 else

1272

                              (if KP_11

1273

                                 then 1

1274

                                 else

1275

                              (if KP_21

1276

                                 then 2

1277

                                 else

1278

                              (if KP_31

1279

                                 then 3

1280

                                 else

1281

                              (if KP_41

1282

                                 then 4

1283

                                 else

1284

                              (if KP_51

1285

                                 then 5

1286

                                 else

1287

                              (if KP_61

1288

                                 then 6

1289

                                 else

1290

                              (if KP_71

1291

                                 then 7

1292

                                 else

1293

                              (if KP_81

1294

                                 then 8

1295

                                 else

1296

                              (if KP_91

1297

                                 then 9

1298

                                 else 10)))))))))) <= 9)

1299

                              then true

1300

                              else false)

1301

                           then

1302

                                 (if KP_01

1303

                                    then 0

1304

                                    else

1305

                                 (if KP_11

1306

                                    then 1

1307

                                    else

1308

                                 (if KP_21

1309

                                    then 2

1310

                                    else

1311

                                 (if KP_31

1312

                                    then 3

1313

                                    else

1314

                                 (if KP_41

1315

                                    then 4

1316

                                    else

1317

                                 (if KP_51

1318

                                    then 5

1319

                                    else

1320

                                 (if KP_61

1321

                                    then 6

1322

                                    else

1323

                                 (if KP_71

1324

                                    then 7

1325

                                    else

1326

                                 (if KP_81

1327

                                    then 8

1328

                                    else

1329

                                 (if KP_91

1330

                                    then 9

1331

                                    else 10))))))))))

1332

                           else 0))

1333

                  else

1334

               (if KP_CLEAR

1335

                  then 0

1336

                  else

1337

(if

1338

                  (if (

1339

                     (if (KP_01 and

1340

                        (not (pre KP_01)))

1341

                        then 0

1342

                        else

1343

                     (if (KP_11 and

1344

                        (not (pre KP_11)))

1345

                        then 1

1346

                        else

1347

                     (if (KP_21 and

1348

                        (not (pre KP_21)))

1349

                        then 2

1350

                        else

1351

                     (if (KP_31 and

1352

                        (not (pre KP_31)))

1353

                        then 3

1354

                        else

1355

                     (if (KP_41 and

1356

                        (not (pre KP_41)))

1357

                        then 4

1358

                        else

1359

                     (if (KP_51 and

1360

                        (not (pre KP_51)))

1361

                        then 5

1362

                        else

1363

                     (if (KP_61 and

1364

                        (not (pre KP_61)))

1365

                        then 6

1366

                        else

1367

                     (if (KP_71 and

1368

                        (not (pre KP_71)))

1369

                        then 7

1370

                        else

1371

                     (if (KP_81 and

1372

                        (not (pre KP_81)))

1373

                        then 8

1374

                        else

1375

                     (if (KP_91 and

1376

                        (not (pre KP_91)))

1377

                        then 9

1378

                        else 10)))))))))) <= 9)

1379

                     then true

1380

                     else false)

1381

                  then

1382

                        (if (KP_01 and

1383

                           (not (pre KP_01)))

1384

                           then 0

1385

                           else

1386

                        (if (KP_11 and

1387

                           (not (pre KP_11)))

1388

                           then 1

1389

                           else

1390

                        (if (KP_21 and

1391

                           (not (pre KP_21)))

1392

                           then 2

1393

                           else

1394

                        (if (KP_31 and

1395

                           (not (pre KP_31)))

1396

                           then 3

1397

                           else

1398

                        (if (KP_41 and

1399

                           (not (pre KP_41)))

1400

                           then 4

1401

                           else

1402

                        (if (KP_51 and

1403

                           (not (pre KP_51)))

1404

                           then 5

1405

                           else

1406

                        (if (KP_61 and

1407

                           (not (pre KP_61)))

1408

                           then 6

1409

                           else

1410

                        (if (KP_71 and

1411

                           (not (pre KP_71)))

1412

                           then 7

1413

                           else

1414

                        (if (KP_81 and

1415

                           (not (pre KP_81)))

1416

                           then 8

1417

                           else

1418

                        (if (KP_91 and

1419

                           (not (pre KP_91)))

1420

                           then 9

1421

                           else 10))))))))))

1422

                  else (pre microwave_microwave_KEYPAD_PROCESSING_DISPLAY_RIGHT_DIGIT_DIGIT_TO_DISPLAY))))

1423

         else (pre microwave_microwave_KEYPAD_PROCESSING_DISPLAY_RIGHT_DIGIT_DIGIT_TO_DISPLAY)));

1424

1425

   STEPS_TO_COOK = (

1426

      (if (rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_init_step and

1427

         (not rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clock))

1428

         then 0

1429

         else ((((microwave_microwave_KEYPAD_PROCESSING_DISPLAY_RIGHT_DIGIT_DIGIT_TO_DISPLAY * 1) + (microwave_microwave_KEYPAD_PROCESSING_DISPLAY_MIDDLE_DIGIT_DIGIT_TO_DISPLAY * 10)) + (microwave_microwave_KEYPAD_PROCESSING_DISPLAY_LEFT_DIGIT_DIGIT_TO_DISPLAY * 60)) * 1)) ->

1430

      (if (rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_init_step and

1431

         (not rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clock))

1432

         then 0

1433

         else

1434

      (if rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clock

1435

         then ((((microwave_microwave_KEYPAD_PROCESSING_DISPLAY_RIGHT_DIGIT_DIGIT_TO_DISPLAY * 1) + (microwave_microwave_KEYPAD_PROCESSING_DISPLAY_MIDDLE_DIGIT_DIGIT_TO_DISPLAY * 10)) + (microwave_microwave_KEYPAD_PROCESSING_DISPLAY_LEFT_DIGIT_DIGIT_TO_DISPLAY * 60)) * 1)

1436

         else (pre STEPS_TO_COOK))));

1437

1438

   rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_init_step = (true ->

1439

      (if (not rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clock)

1440

         then true

1441

         else

1442

      (if (pre rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clock)

1443

         then false

1444

         else (pre rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_init_step))));

1445

1446

   SETUP =

1447

      (if (1 = microwave_microwave_mode_logic_mode)

1448

         then true

1449

         else false);

1450

1451

   p32 = (true -> ((not (enable and

1452

      (not KP_CLEAR))) or

1453

      ((not ((KP_5 and

1454

      (not (pre KP_5))) and

1455

      ((not (KP_4 and

1456

      (not (pre KP_4)))) and

1457

      ((not (KP_3 and

1458

      (not (pre KP_3)))) and

1459

      ((not (KP_2 and

1460

      (not (pre KP_2)))) and

1461

      ((not (KP_1 and

1462

      (not (pre KP_1)))) and

1463

      (not (KP_0 and

1464

      (not (pre KP_0)))))))))) or

1465

      (RIGHT_DIGIT = 5))));

1466

1467

   enable = (true ->

1468

      (if (1 = (pre microwave_microwave_mode_logic_mode))

1469

         then true

1470

         else false));

1471

1472

   OK = (true -> (

1473

      (if (not SETUP)

1474

         then

1475

               (if (MWI_FcnMaxI_In1 > 0)

1476

                  then MWI_FcnMaxI_In1

1477

                  else 0)

1478

         else 639) > 0));

1479

1480

   p28 = (true -> ((not (enable and

1481

      (not KP_CLEAR))) or

1482

      ((not ((KP_1 and

1483

      (not (pre KP_1))) and

1484

      (not (KP_0 and

1485

      (not (pre KP_0)))))) or

1486

      (RIGHT_DIGIT = 1))));

1487

1488

   p13 = ((not (enable and

1489

      KP_CLEAR)) or

1490

      (STEPS_TO_COOK = 0));

1491

1492

   p19 = (true -> ((not (enable and

1493

      (not KP_CLEAR))) or

1494

      (((((((((((KP_1 and

1495

      (not (pre KP_1))) or

1496

      (KP_2 and

1497

      (not (pre KP_2)))) or

1498

      (KP_3 and

1499

      (not (pre KP_3)))) or

1500

      (KP_4 and

1501

      (not (pre KP_4)))) or

1502

      (KP_5 and

1503

      (not (pre KP_5)))) or

1504

      (KP_6 and

1505

      (not (pre KP_6)))) or

1506

      (KP_7 and

1507

      (not (pre KP_7)))) or

1508

      (KP_8 and

1509

      (not (pre KP_8)))) or

1510

      (KP_9 and

1511

      (not (pre KP_9)))) or

1512

      (KP_0 and

1513

      (not (pre KP_0)))) or

1514

      (LEFT_DIGIT = (pre LEFT_DIGIT)))));

1515

1516

   p29 = (true -> ((not (enable and

1517

      (not KP_CLEAR))) or

1518

      ((not ((KP_2 and

1519

      (not (pre KP_2))) and

1520

      ((not (KP_1 and

1521

      (not (pre KP_1)))) and

1522

      (not (KP_0 and

1523

      (not (pre KP_0))))))) or

1524

      (RIGHT_DIGIT = 2))));

1525

1526

   p34 = (true -> ((not (enable and

1527

      (not KP_CLEAR))) or

1528

      ((not ((KP_7 and

1529

      (not (pre KP_7))) and

1530

      ((not (KP_6 and

1531

      (not (pre KP_6)))) and

1532

      ((not (KP_5 and

1533

      (not (pre KP_5)))) and

1534

      ((not (KP_4 and

1535

      (not (pre KP_4)))) and

1536

      ((not (KP_3 and

1537

      (not (pre KP_3)))) and

1538

      ((not (KP_2 and

1539

      (not (pre KP_2)))) and

1540

      ((not (KP_1 and

1541

      (not (pre KP_1)))) and

1542

      (not (KP_0 and

1543

      (not (pre KP_0)))))))))))) or

1544

      (RIGHT_DIGIT = 7))));

1545

1546

   p12 = (enable or

1547

      (STEPS_TO_COOK = 0));

1548

1549

   p21 = ((not (enable and

1550

      KP_CLEAR)) or

1551

      (MIDDLE_DIGIT = 0));

1552

1553

  --%PROPERTY OK=true;

1554

  --%MAIN;

1555

1556

tel

Project

General

Profile

CristalCaveGem » LustreC » Lustrec-Tests

lustrec-tests / regression_tests / lustre_files / success / kind_fmcad08 / large / TIMEOUT / microwave06.lus @ b8dc00eb