/regression_tests/lustre_files/success/kind_fmcad08/large/TIMEOUT/microwave07.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

   p5: bool;

108

   p6: bool;

109

   p7: bool;

110

   p8: bool;

111

   p9: bool;

112

   p10: bool;

113

   p11: bool;

114

   p12: bool;

115

   p13: bool;

116

   p14: bool;

117

   p15: bool;

118

   p16: bool;

119

   p17: bool;

120

   p18: bool;

121

   p19: bool;

122

   p20: bool;

123

   p21: bool;

124

   p22: bool;

125

   p23: bool;

126

   p24: bool;

127

   p25: bool;

128

   p26: bool;

129

   p27: bool;

130

   p28: bool;

131

   p29: bool;

132

   p30: bool;

133

   p31: bool;

134

   p32: bool;

135

   p33: bool;

136

   p34: bool;

137

   p35: bool;

138

   p36: bool;

139

   p37: bool;

140

let

141

   rlt__Arrow5 = (639 ->

142

      (if (not (not SETUP))

143

         then

144

               (if (MWI_FcnMaxI_In13 > 0)

145

                  then MWI_FcnMaxI_In13

146

                  else 0)

147

         else 639));

148

149

   rlt__Arrow4 = (639 ->

150

      (if (not SUSPENDED)

151

         then

152

               (if (MWI_FcnMaxI_In12 > 0)

153

                  then MWI_FcnMaxI_In12

154

                  else 0)

155

         else 639));

156

157

   rlt__Arrow3 = (639 ->

158

      (if (not (not COOKING))

159

         then

160

               (if (MWI_FcnMaxI_In16 > 0)

161

                  then MWI_FcnMaxI_In16

162

                  else 0)

163

         else 639));

164

165

   rlt__Arrow2 = (639 ->

166

      (if (not (not SUSPENDED))

167

         then

168

               (if (MWI_FcnMaxI_In15 > 0)

169

                  then MWI_FcnMaxI_In15

170

                  else 0)

171

         else 639));

172

173

   rlt__Arrow1 = (639 ->

174

      (if (not COOKING)

175

         then

176

               (if (MWI_FcnMaxI_In11 > 0)

177

                  then MWI_FcnMaxI_In11

178

                  else 0)

179

         else 639));

180

181

   rlt__Arrow = (639 ->

182

      (if (not SETUP)

183

         then

184

               (if (MWI_FcnMaxI_In1 > 0)

185

                  then MWI_FcnMaxI_In1

186

                  else 0)

187

         else 639));

188

189

   p18 = (((not (enable and

190

      (not KP_CLEAR))) or

191

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

192

      KP_2) or

193

      KP_3) or

194

      KP_4) or

195

      KP_5) or

196

      KP_6) or

197

      KP_7) or

198

      KP_8) or

199

      KP_9) or

200

      KP_0)) or

201

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

202

      (not KP_CLEAR))) or

203

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

204

      (not (pre KP_1))) or

205

      (KP_2 and

206

      (not (pre KP_2)))) or

207

      (KP_3 and

208

      (not (pre KP_3)))) or

209

      (KP_4 and

210

      (not (pre KP_4)))) or

211

      (KP_5 and

212

      (not (pre KP_5)))) or

213

      (KP_6 and

214

      (not (pre KP_6)))) or

215

      (KP_7 and

216

      (not (pre KP_7)))) or

217

      (KP_8 and

218

      (not (pre KP_8)))) or

219

      (KP_9 and

220

      (not (pre KP_9)))) or

221

      (KP_0 and

222

      (not (pre KP_0))))) or

223

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

224

225

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

226

      (not KP_CLEAR))) or

227

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

228

      (not (pre KP_1))) or

229

      (KP_2 and

230

      (not (pre KP_2)))) or

231

      (KP_3 and

232

      (not (pre KP_3)))) or

233

      (KP_4 and

234

      (not (pre KP_4)))) or

235

      (KP_5 and

236

      (not (pre KP_5)))) or

237

      (KP_6 and

238

      (not (pre KP_6)))) or

239

      (KP_7 and

240

      (not (pre KP_7)))) or

241

      (KP_8 and

242

      (not (pre KP_8)))) or

243

      (KP_9 and

244

      (not (pre KP_9)))) or

245

      (KP_0 and

246

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

247

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

248

249

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

250

      (not KP_CLEAR))) or

251

      ((not ((KP_8 and

252

      (not (pre KP_8))) and

253

      ((not (KP_7 and

254

      (not (pre KP_7)))) and

255

      ((not (KP_6 and

256

      (not (pre KP_6)))) and

257

      ((not (KP_5 and

258

      (not (pre KP_5)))) and

259

      ((not (KP_4 and

260

      (not (pre KP_4)))) and

261

      ((not (KP_3 and

262

      (not (pre KP_3)))) and

263

      ((not (KP_2 and

264

      (not (pre KP_2)))) and

265

      ((not (KP_1 and

266

      (not (pre KP_1)))) and

267

      (not (KP_0 and

268

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

269

      (RIGHT_DIGIT = 8))));

270

271

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

272

      (not KP_CLEAR))) or

273

      ((not ((KP_6 and

274

      (not (pre KP_6))) and

275

      ((not (KP_5 and

276

      (not (pre KP_5)))) and

277

      ((not (KP_4 and

278

      (not (pre KP_4)))) and

279

      ((not (KP_3 and

280

      (not (pre KP_3)))) and

281

      ((not (KP_2 and

282

      (not (pre KP_2)))) and

283

      ((not (KP_1 and

284

      (not (pre KP_1)))) and

285

      (not (KP_0 and

286

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

287

      (RIGHT_DIGIT = 6))));

288

289

   MIDDLE_DIGIT = microwave_microwave_TIME_ON_DISPLAY_SECONDS_TO_TENS__QUOTIENT;

290

291

   RIGHT_DIGIT = microwave_microwave_TIME_ON_DISPLAY_SECONDS_TO_TENS__REMAINDER;

292

293

   p25 = (enable or

294

      (RIGHT_DIGIT = 0));

295

296

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

297

      (not KP_CLEAR))) or

298

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

299

      (not (pre KP_1))) or

300

      (KP_2 and

301

      (not (pre KP_2)))) or

302

      (KP_3 and

303

      (not (pre KP_3)))) or

304

      (KP_4 and

305

      (not (pre KP_4)))) or

306

      (KP_5 and

307

      (not (pre KP_5)))) or

308

      (KP_6 and

309

      (not (pre KP_6)))) or

310

      (KP_7 and

311

      (not (pre KP_7)))) or

312

      (KP_8 and

313

      (not (pre KP_8)))) or

314

      (KP_9 and

315

      (not (pre KP_9)))) or

316

      (KP_0 and

317

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

318

      (MIDDLE_DIGIT = (pre RIGHT_DIGIT))));

319

320

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

321

      (not KP_CLEAR))) or

322

      ((not ((KP_9 and

323

      (not (pre KP_9))) and

324

      ((not (KP_8 and

325

      (not (pre KP_8)))) and

326

      ((not (KP_7 and

327

      (not (pre KP_7)))) and

328

      ((not (KP_6 and

329

      (not (pre KP_6)))) and

330

      ((not (KP_5 and

331

      (not (pre KP_5)))) and

332

      ((not (KP_4 and

333

      (not (pre KP_4)))) and

334

      ((not (KP_3 and

335

      (not (pre KP_3)))) and

336

      ((not (KP_2 and

337

      (not (pre KP_2)))) and

338

      ((not (KP_1 and

339

      (not (pre KP_1)))) and

340

      (not (KP_0 and

341

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

342

      (RIGHT_DIGIT = 9))));

343

344

   MWI_FcnMaxI_In1 = ((pre rlt__Arrow) - 1);

345

346

   CLEAR_PRESSED = (KP_CLEAR -> (KP_CLEAR and

347

      (not (pre KP_CLEAR))));

348

349

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

350

351

   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));

352

353

   SUSPENDED =

354

      (if (3 = microwave_microwave_mode_logic_mode)

355

         then true

356

         else false);

357

358

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

359

      (not KP_CLEAR))) or

360

      ((not ((KP_4 and

361

      (not (pre KP_4))) and

362

      ((not (KP_3 and

363

      (not (pre KP_3)))) and

364

      ((not (KP_2 and

365

      (not (pre KP_2)))) and

366

      ((not (KP_1 and

367

      (not (pre KP_1)))) and

368

      (not (KP_0 and

369

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

370

      (RIGHT_DIGIT = 4))));

371

372

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

373

      (not KP_CLEAR))) or

374

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

375

      (not (pre KP_1))) or

376

      (KP_2 and

377

      (not (pre KP_2)))) or

378

      (KP_3 and

379

      (not (pre KP_3)))) or

380

      (KP_4 and

381

      (not (pre KP_4)))) or

382

      (KP_5 and

383

      (not (pre KP_5)))) or

384

      (KP_6 and

385

      (not (pre KP_6)))) or

386

      (KP_7 and

387

      (not (pre KP_7)))) or

388

      (KP_8 and

389

      (not (pre KP_8)))) or

390

      (KP_9 and

391

      (not (pre KP_9)))) or

392

      (KP_0 and

393

      (not (pre KP_0)))) or

394

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

395

396

   MWI_FcnMaxI_In11 = ((pre rlt__Arrow1) - 1);

397

398

   OK = (true -> (

399

      (if (not COOKING)

400

         then

401

               (if (MWI_FcnMaxI_In11 > 0)

402

                  then MWI_FcnMaxI_In11

403

                  else 0)

404

         else 639) > 0));

405

406

   MWI_FcnMaxI_In15 = ((pre rlt__Arrow2) - 1);

407

408

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

409

      (not KP_CLEAR))) or

410

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

411

      (not (pre KP_1))) or

412

      (KP_2 and

413

      (not (pre KP_2)))) or

414

      (KP_3 and

415

      (not (pre KP_3)))) or

416

      (KP_4 and

417

      (not (pre KP_4)))) or

418

      (KP_5 and

419

      (not (pre KP_5)))) or

420

      (KP_6 and

421

      (not (pre KP_6)))) or

422

      (KP_7 and

423

      (not (pre KP_7)))) or

424

      (KP_8 and

425

      (not (pre KP_8)))) or

426

      (KP_9 and

427

      (not (pre KP_9)))) or

428

      (KP_0 and

429

      (not (pre KP_0))))) or

430

      (MIDDLE_DIGIT = (pre MIDDLE_DIGIT))));

431

432

   p20 = (enable or

433

      (MIDDLE_DIGIT = 0));

434

435

   p5 = (true -> (

436

      (if (not SUSPENDED)

437

         then

438

               (if (MWI_FcnMaxI_In12 > 0)

439

                  then MWI_FcnMaxI_In12

440

                  else 0)

441

         else 639) > 0));

442

443

   p26 = ((not (enable and

444

      KP_CLEAR)) or

445

      (RIGHT_DIGIT = 0));

446

447

   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);

448

449

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

450

      (not KP_CLEAR))) or

451

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

452

453

   MWI_FcnMaxI_In16 = ((pre rlt__Arrow3) - 1);

454

455

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

456

457

      (if (not (not SETUP))

458

         then

459

               (if (MWI_FcnMaxI_In13 > 0)

460

                  then MWI_FcnMaxI_In13

461

                  else 0)

462

         else 639) > 0)));

463

464

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

465

466

      (if (not (not SUSPENDED))

467

         then

468

               (if (MWI_FcnMaxI_In15 > 0)

469

                  then MWI_FcnMaxI_In15

470

                  else 0)

471

         else 639) > 0)));

472

473

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

474

475

      (if (not (not COOKING))

476

         then

477

               (if (MWI_FcnMaxI_In16 > 0)

478

                  then MWI_FcnMaxI_In16

479

                  else 0)

480

         else 639) > 0)));

481

482

   MWI_FcnMaxI_In12 = ((pre rlt__Arrow4) - 1);

483

484

   p16 = ((not (enable and

485

      KP_CLEAR)) or

486

      (LEFT_DIGIT = 0));

487

488

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

489

      (not KP_CLEAR))) or

490

      ((not ((KP_3 and

491

      (not (pre KP_3))) and

492

      ((not (KP_2 and

493

      (not (pre KP_2)))) and

494

      ((not (KP_1 and

495

      (not (pre KP_1)))) and

496

      (not (KP_0 and

497

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

498

      (RIGHT_DIGIT = 3))));

499

500

   COOKING =

501

      (if (2 = microwave_microwave_mode_logic_mode)

502

         then true

503

         else false);

504

505

   LEFT_DIGIT = microwave_microwave_TIME_ON_DISPLAY_SECONDS_TO_MINUTES__QUOTIENT;

506

507

   p11 = ((not KP_CLEAR) or

508

      (not COOKING));

509

510

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

511

      DOOR_CLOSED));

512

513

   p15 = (enable or

514

      (LEFT_DIGIT = 0));

515

516

   START_PRESSED = (KP_START -> (KP_START and

517

      (not (pre KP_START))));

518

519

   chart_microwave_mode_logic_start =

520

      (if (START_PRESSED = false)

521

         then 0

522

         else 1);

523

524

   chart_microwave_mode_logic_clear_off =

525

      (if (CLEAR_PRESSED = false)

526

         then 0

527

         else 1);

528

529

   chart_microwave_mode_logic_door_closed =

530

      (if (DOOR_CLOSED = false)

531

         then 0

532

         else 1);

533

534

   chart_microwave_mode_logic____wakeup___ = true;

535

536

   chart_microwave_mode_logic_rlt_evtInitStep = (true ->

537

      (if (pre chart_microwave_mode_logic____wakeup___)

538

         then false

539

         else (pre chart_microwave_mode_logic_rlt_evtInitStep)));

540

541

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

542

543

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

544

545

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

546

547

   chart_microwave_mode_logic_final_state_states___root =

548

      (if chart_microwave_mode_logic____wakeup___

549

         then

550

               (if chart_microwave_mode_logic_rlt_evtInitStep

551

                  then rlt_enter_microwave_mode_logic_rlt_state_2_states___root

552

                  else

553

               (if ((not rlt_eval_microwave_mode_logic_rlt_fired_1) and

554

555

556

                  ((rlt_eval_microwave_mode_logic_rlt_state_3_states___root >= 1) and

557

                  (rlt_eval_microwave_mode_logic_rlt_state_3_states___root <= 3)))

558

                  then

559

                        (if rlt_eval_microwave_mode_logic_ON_rlt_fired_6

560

                           then

561

                                 (if (not (rlt_eval_microwave_mode_logic_ON_rlt_state_11_states___root = 3))

562

                                    then

563

564

565

                                    else rlt_eval_microwave_mode_logic_ON_rlt_state_11_states___root)

566

                           else rlt_eval_microwave_mode_logic_ON_rlt_state_11_states___root)

567

                  else rlt_eval_microwave_mode_logic_rlt_state_3_states___root))

568

         else chart_microwave_mode_logic_begin_state_states___root);

569

570

   chart_microwave_mode_logic_mode =

571

      (if chart_microwave_mode_logic____wakeup___

572

         then

573

               (if chart_microwave_mode_logic_rlt_evtInitStep

574

                  then

575

                        (if (not (chart_microwave_mode_logic_begin_state_states___root = 4))

576

                           then 1

577

                           else chart_microwave_mode_logic_begin_state_outports_mode)

578

                  else

579

               (if ((not rlt_eval_microwave_mode_logic_rlt_fired_1) and

580

581

582

                  ((rlt_eval_microwave_mode_logic_rlt_state_3_states___root >= 1) and

583

                  (rlt_eval_microwave_mode_logic_rlt_state_3_states___root <= 3)))

584

                  then

585

                        (if rlt_eval_microwave_mode_logic_ON_rlt_fired_6

586

                           then

587

                                 (if (not (rlt_eval_microwave_mode_logic_ON_rlt_state_11_states___root = 3))

588

                                    then 3

589

                                    else rlt_eval_microwave_mode_logic_ON_rlt_state_11_outports_mode)

590

                           else rlt_eval_microwave_mode_logic_ON_rlt_state_11_outports_mode)

591

                  else rlt_eval_microwave_mode_logic_rlt_state_3_outports_mode))

592

         else chart_microwave_mode_logic_begin_state_outports_mode);

593

594

   chart_microwave_mode_logic_steps_remaining =

595

      (if chart_microwave_mode_logic____wakeup___

596

         then

597

               (if chart_microwave_mode_logic_rlt_evtInitStep

598

                  then chart_microwave_mode_logic_begin_state_outports_steps_remaining

599

                  else

600

               (if ((not rlt_eval_microwave_mode_logic_rlt_fired_1) and

601

602

603

                  ((rlt_eval_microwave_mode_logic_rlt_state_3_states___root >= 1) and

604

                  (rlt_eval_microwave_mode_logic_rlt_state_3_states___root <= 3)))

605

                  then

606

                        (if rlt_eval_microwave_mode_logic_ON_rlt_fired_5

607

                           then (rlt_eval_microwave_mode_logic_ON_rlt_state_6_outports_steps_remaining - 1)

608

                           else rlt_eval_microwave_mode_logic_ON_rlt_state_6_outports_steps_remaining)

609

                  else rlt_eval_microwave_mode_logic_rlt_state_1_outports_steps_remaining))

610

         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 =

619

      (if rlt_eval_microwave_mode_logic_rlt_fired_0

620

         then STEPS_TO_COOK

621

         else chart_microwave_mode_logic_begin_state_outports_steps_remaining);

622

623

624

   rlt_eval_microwave_mode_logic_rlt_fired_1 = (rlt_eval_microwave_mode_logic_rlt_fired_0 and

625

      ((chart_microwave_mode_logic_begin_state_states___root = 4) and

626

627

      (if (chart_microwave_mode_logic_start <> 0)

628

         then true

629

         else false) and

630

631

      (if (

632

         (if ((STEPS_TO_COOK > 0) = false)

633

            then 0

634

            else 1) <> 0)

635

         then true

636

         else false))));

   rlt_eval_microwave_mode_logic_rlt_state_2_states___root =

641

      (if rlt_eval_microwave_mode_logic_rlt_fired_1

642

         then

643

               (if (chart_microwave_mode_logic_begin_state_states___root = 4)

644

                  then

645

646

647

                  else chart_microwave_mode_logic_begin_state_states___root)

648

         else chart_microwave_mode_logic_begin_state_states___root);

   rlt_eval_microwave_mode_logic_rlt_state_3_states___root =

653

      (if rlt_eval_microwave_mode_logic_rlt_fired_1

654

         then rlt_enter_microwave_mode_logic_ON_rlt_state_4_states___root

655

         else rlt_eval_microwave_mode_logic_rlt_state_2_states___root);

   rlt_eval_microwave_mode_logic_rlt_state_3_outports_mode =

662

      (if rlt_eval_microwave_mode_logic_rlt_fired_1

663

         then

664

               (if rlt_enter_microwave_mode_logic_ON_rlt_fired_2

665

                  then

666

                        (if (not (rlt_enter_microwave_mode_logic_ON_rlt_state_2_states___root = 3))

667

                           then 3

668

                           else rlt_enter_microwave_mode_logic_ON_rlt_state_2_outports_mode)

669

                  else rlt_enter_microwave_mode_logic_ON_rlt_state_2_outports_mode)

670

         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

676

      (rlt_eval_microwave_mode_logic_rlt_state_1_outports_steps_remaining <= 0)) and

677

      (rlt_eval_microwave_mode_logic_rlt_state_3_states___root = 2));

   rlt_eval_microwave_mode_logic_ON_rlt_state_1_states___root =

682

      (if rlt_eval_microwave_mode_logic_ON_rlt_fired_1

683

         then

684

(if

685

686

                  ((rlt_eval_microwave_mode_logic_rlt_state_3_states___root >= 1) and

687

                  (rlt_eval_microwave_mode_logic_rlt_state_3_states___root <= 3))

688

                  then

689

690

691

                  else rlt_eval_microwave_mode_logic_rlt_state_3_states___root)

692

         else rlt_eval_microwave_mode_logic_rlt_state_3_states___root);

   rlt_eval_microwave_mode_logic_ON_rlt_state_2_states___root =

697

      (if rlt_eval_microwave_mode_logic_ON_rlt_fired_1

698

         then

699

               (if (not (rlt_eval_microwave_mode_logic_ON_rlt_state_1_states___root = 4))

700

                  then

701

702

703

                  else rlt_eval_microwave_mode_logic_ON_rlt_state_1_states___root)

704

         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

711

((

712

      (if (chart_microwave_mode_logic_start <> 0)

713

         then true

714

         else false) and

715

716

      (if (chart_microwave_mode_logic_door_closed <> 0)

717

         then true

718

         else false)) and

719

      (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

724

      rlt_eval_microwave_mode_logic_ON_rlt_fired_1);

   rlt_eval_microwave_mode_logic_ON_rlt_state_3_states___root =

729

      (if rlt_eval_microwave_mode_logic_ON_rlt_fired_2

730

         then

731

               (if (rlt_eval_microwave_mode_logic_ON_rlt_state_2_states___root = 3)

732

                  then

733

734

735

                  else rlt_eval_microwave_mode_logic_ON_rlt_state_2_states___root)

736

         else rlt_eval_microwave_mode_logic_ON_rlt_state_2_states___root);

   rlt_eval_microwave_mode_logic_ON_rlt_state_3_outports_mode =

741

      (if rlt_eval_microwave_mode_logic_ON_rlt_fired_1

742

         then

743

               (if (not (rlt_eval_microwave_mode_logic_ON_rlt_state_1_states___root = 4))

744

                  then 1

745

                  else rlt_eval_microwave_mode_logic_rlt_state_3_outports_mode)

746

         else rlt_eval_microwave_mode_logic_rlt_state_3_outports_mode);

   rlt_eval_microwave_mode_logic_ON_rlt_state_4_states___root =

751

      (if rlt_eval_microwave_mode_logic_ON_rlt_fired_2

752

         then

753

               (if (not (rlt_eval_microwave_mode_logic_ON_rlt_state_3_states___root = 2))

754

                  then

755

756

757

                  else rlt_eval_microwave_mode_logic_ON_rlt_state_3_states___root)

758

         else rlt_eval_microwave_mode_logic_ON_rlt_state_3_states___root);

   rlt_eval_microwave_mode_logic_ON_rlt_state_4_outports_mode =

765

      (if rlt_eval_microwave_mode_logic_ON_rlt_fired_2

766

         then

767

               (if (not (rlt_eval_microwave_mode_logic_ON_rlt_state_3_states___root = 2))

768

                  then 2

769

                  else rlt_eval_microwave_mode_logic_ON_rlt_state_3_outports_mode)

770

         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

776

777

      (if (chart_microwave_mode_logic_clear_off <> 0)

778

         then true

779

         else false) and

780

      (not rlt_eval_microwave_mode_logic_ON_rlt_complete_1))) and

781

      ((rlt_eval_microwave_mode_logic_ON_rlt_state_4_states___root = 3) and

782

      (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

787

      rlt_eval_microwave_mode_logic_ON_rlt_complete_1);

   rlt_eval_microwave_mode_logic_ON_rlt_state_6_states___root =

792

      (if rlt_eval_microwave_mode_logic_ON_rlt_fired_4

793

         then

794

(if

795

796

                  ((rlt_eval_microwave_mode_logic_ON_rlt_state_4_states___root >= 1) and

797

                  (rlt_eval_microwave_mode_logic_ON_rlt_state_4_states___root <= 3))

798

                  then

799

800

801

                  else rlt_eval_microwave_mode_logic_ON_rlt_state_4_states___root)

802

         else rlt_eval_microwave_mode_logic_ON_rlt_state_4_states___root);

   rlt_eval_microwave_mode_logic_ON_rlt_state_6_outports_steps_remaining =

807

      (if rlt_eval_microwave_mode_logic_ON_rlt_fired_4

808

         then 0

809

         else rlt_eval_microwave_mode_logic_rlt_state_1_outports_steps_remaining);

   rlt_eval_microwave_mode_logic_ON_rlt_state_7_states___root =

814

      (if rlt_eval_microwave_mode_logic_ON_rlt_fired_4

815

         then

816

               (if (not (rlt_eval_microwave_mode_logic_ON_rlt_state_6_states___root = 4))

817

                  then

818

819

820

                  else rlt_eval_microwave_mode_logic_ON_rlt_state_6_states___root)

821

         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

828

      ((rlt_eval_microwave_mode_logic_ON_rlt_state_6_outports_steps_remaining > 0) and

829

      (not rlt_eval_microwave_mode_logic_ON_rlt_complete_2)));

   rlt_eval_microwave_mode_logic_ON_rlt_state_8_outports_mode =

834

      (if rlt_eval_microwave_mode_logic_ON_rlt_fired_4

835

         then

836

               (if (not (rlt_eval_microwave_mode_logic_ON_rlt_state_6_states___root = 4))

837

                  then 1

838

                  else rlt_eval_microwave_mode_logic_ON_rlt_state_4_outports_mode)

839

         else rlt_eval_microwave_mode_logic_ON_rlt_state_4_outports_mode);

   rlt_eval_microwave_mode_logic_ON_rlt_state_9_states___root =

844

      (if rlt_eval_microwave_mode_logic_ON_rlt_fired_5

845

         then

846

               (if (rlt_eval_microwave_mode_logic_ON_rlt_state_7_states___root = 2)

847

                  then

848

849

850

                  else rlt_eval_microwave_mode_logic_ON_rlt_state_7_states___root)

851

         else rlt_eval_microwave_mode_logic_ON_rlt_state_7_states___root);

   rlt_eval_microwave_mode_logic_ON_rlt_state_10_states___root =

856

      (if rlt_eval_microwave_mode_logic_ON_rlt_fired_5

857

         then

858

               (if (not (rlt_eval_microwave_mode_logic_ON_rlt_state_9_states___root = 2))

859

                  then

860

861

862

                  else rlt_eval_microwave_mode_logic_ON_rlt_state_9_states___root)

863

         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

870

((

871

      (if (chart_microwave_mode_logic_clear_off <> 0)

872

         then true

873

         else false) or

874

      (not

875

      (if (chart_microwave_mode_logic_door_closed <> 0)

876

         then true

877

         else false))) and

878

      (not (rlt_eval_microwave_mode_logic_ON_rlt_fired_5 or

879

      rlt_eval_microwave_mode_logic_ON_rlt_complete_2))));

   rlt_eval_microwave_mode_logic_ON_rlt_state_11_states___root =

884

      (if rlt_eval_microwave_mode_logic_ON_rlt_fired_6

885

         then

886

               (if (rlt_eval_microwave_mode_logic_ON_rlt_state_10_states___root = 2)

887

                  then

888

889

890

                  else rlt_eval_microwave_mode_logic_ON_rlt_state_10_states___root)

891

         else rlt_eval_microwave_mode_logic_ON_rlt_state_10_states___root);

   rlt_eval_microwave_mode_logic_ON_rlt_state_11_outports_mode =

896

      (if rlt_eval_microwave_mode_logic_ON_rlt_fired_5

897

         then

898

               (if (not (rlt_eval_microwave_mode_logic_ON_rlt_state_9_states___root = 2))

899

                  then 2

900

                  else rlt_eval_microwave_mode_logic_ON_rlt_state_8_outports_mode)

901

         else rlt_eval_microwave_mode_logic_ON_rlt_state_8_outports_mode);

902

903

   rlt_enter_microwave_mode_logic_ON_rlt_state_1_states___root =

904

      (if (not

905

906

         ((rlt_eval_microwave_mode_logic_rlt_state_2_states___root >= 1) and

907

         (rlt_eval_microwave_mode_logic_rlt_state_2_states___root <= 3)))

908

         then

909

910

911

         else rlt_eval_microwave_mode_logic_rlt_state_2_states___root);

   rlt_enter_microwave_mode_logic_ON_rlt_fired_0 = ((not

916

917

      ((rlt_eval_microwave_mode_logic_rlt_state_2_states___root >= 1) and

918

      (rlt_eval_microwave_mode_logic_rlt_state_2_states___root <= 3))) and

919

920

921

      ((rlt_enter_microwave_mode_logic_ON_rlt_state_1_states___root >= 1) and

922

      (rlt_enter_microwave_mode_logic_ON_rlt_state_1_states___root <= 3)));

923

924

925

   rlt_enter_microwave_mode_logic_ON_rlt_fired_1 = (rlt_enter_microwave_mode_logic_ON_rlt_fired_0 and

926

927

928

      ((rlt_enter_microwave_mode_logic_ON_rlt_state_1_states___root >= 1) and

929

      (rlt_enter_microwave_mode_logic_ON_rlt_state_1_states___root <= 3)) and

930

931

      (if (chart_microwave_mode_logic_door_closed <> 0)

932

         then true

933

         else false)));

   rlt_enter_microwave_mode_logic_ON_rlt_state_2_states___root =

938

      (if rlt_enter_microwave_mode_logic_ON_rlt_fired_1

939

         then

940

               (if (not (rlt_enter_microwave_mode_logic_ON_rlt_state_1_states___root = 2))

941

                  then

942

943

944

                  else rlt_enter_microwave_mode_logic_ON_rlt_state_1_states___root)

945

         else rlt_enter_microwave_mode_logic_ON_rlt_state_1_states___root);

   rlt_enter_microwave_mode_logic_ON_rlt_state_2_outports_mode =

952

      (if rlt_enter_microwave_mode_logic_ON_rlt_fired_1

953

         then

954

               (if (not (rlt_enter_microwave_mode_logic_ON_rlt_state_1_states___root = 2))

955

                  then 2

956

                  else chart_microwave_mode_logic_begin_state_outports_mode)

957

         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

964

965

966

      ((rlt_enter_microwave_mode_logic_ON_rlt_state_2_states___root >= 1) and

967

      (rlt_enter_microwave_mode_logic_ON_rlt_state_2_states___root <= 3)) and

968

      (not rlt_enter_microwave_mode_logic_ON_rlt_fired_1)));

   rlt_enter_microwave_mode_logic_ON_rlt_state_4_states___root =

973

      (if rlt_enter_microwave_mode_logic_ON_rlt_fired_2

974

         then

975

               (if (not (rlt_enter_microwave_mode_logic_ON_rlt_state_2_states___root = 3))

976

                  then

977

978

979

                  else rlt_enter_microwave_mode_logic_ON_rlt_state_2_states___root)

980

         else rlt_enter_microwave_mode_logic_ON_rlt_state_2_states___root);

   rlt_enter_microwave_mode_logic_rlt_state_2_states___root =

987

      (if (not (chart_microwave_mode_logic_begin_state_states___root = 4))

988

         then

989

990

991

         else chart_microwave_mode_logic_begin_state_states___root);

   microwave_microwave_mode_logic_mode = chart_microwave_mode_logic_mode;

996

997

   p17 = (((not (enable and

998

      (not KP_CLEAR))) or

999

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

1000

      KP_2) or

1001

      KP_3) or

1002

      KP_4) or

1003

      KP_5) or

1004

      KP_6) or

1005

      KP_7) or

1006

      KP_8) or

1007

      KP_9) or

1008

      KP_0)) or

1009

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

1010

      (not KP_CLEAR))) or

1011

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

1012

      (not (pre KP_1))) or

1013

      (KP_2 and

1014

      (not (pre KP_2)))) or

1015

      (KP_3 and

1016

      (not (pre KP_3)))) or

1017

      (KP_4 and

1018

      (not (pre KP_4)))) or

1019

      (KP_5 and

1020

      (not (pre KP_5)))) or

1021

      (KP_6 and

1022

      (not (pre KP_6)))) or

1023

      (KP_7 and

1024

      (not (pre KP_7)))) or

1025

      (KP_8 and

1026

      (not (pre KP_8)))) or

1027

      (KP_9 and

1028

      (not (pre KP_9)))) or

1029

      (KP_0 and

1030

      (not (pre KP_0))))) or

1031

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

1032

1033

   MWI_FcnMaxI_In13 = ((pre rlt__Arrow5) - 1);

1034

1035

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

1036

1037

      (if (not (not COOKING))

1038

         then

1039

               (if (MWI_FcnMaxI_In16 > 0)

1040

                  then MWI_FcnMaxI_In16

1041

                  else 0)

1042

         else 639) > 0)));

1043

1044

   p27 = (((not (enable and

1045

      (not KP_CLEAR))) or

1046

      ((not KP_0) or

1047

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

1048

      (not KP_CLEAR))) or

1049

      ((not (KP_0 and

1050

      (not (pre KP_0)))) or

1051

      (RIGHT_DIGIT = 0))));

1052

1053

   rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clock = enable;

1054

1055

   KP_01 = KP_0;

1056

1057

   KP_11 = KP_1;

1058

1059

   KP_21 = KP_2;

1060

1061

   KP_31 = KP_3;

1062

1063

   KP_41 = KP_4;

1064

1065

   KP_51 = KP_5;

1066

1067

   KP_61 = KP_6;

1068

1069

   KP_71 = KP_7;

1070

1071

   KP_81 = KP_8;

1072

1073

   KP_91 = KP_9;

1074

1075

   microwave_microwave_KEYPAD_PROCESSING_DISPLAY_LEFT_DIGIT_DIGIT_TO_DISPLAY = (0 ->

1076

      (if rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clock

1077

         then

1078

               (if rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_init_step

1079

                  then 0

1080

                  else

1081

               (if KP_CLEAR

1082

                  then 0

1083

                  else

1084

(if

1085

                  (if (

1086

                     (if (KP_01 and

1087

                        (not (pre KP_01)))

1088

                        then 0

1089

                        else

1090

                     (if (KP_11 and

1091

                        (not (pre KP_11)))

1092

                        then 1

1093

                        else

1094

                     (if (KP_21 and

1095

                        (not (pre KP_21)))

1096

                        then 2

1097

                        else

1098

                     (if (KP_31 and

1099

                        (not (pre KP_31)))

1100

                        then 3

1101

                        else

1102

                     (if (KP_41 and

1103

                        (not (pre KP_41)))

1104

                        then 4

1105

                        else

1106

                     (if (KP_51 and

1107

                        (not (pre KP_51)))

1108

                        then 5

1109

                        else

1110

                     (if (KP_61 and

1111

                        (not (pre KP_61)))

1112

                        then 6

1113

                        else

1114

                     (if (KP_71 and

1115

                        (not (pre KP_71)))

1116

                        then 7

1117

                        else

1118

                     (if (KP_81 and

1119

                        (not (pre KP_81)))

1120

                        then 8

1121

                        else

1122

                     (if (KP_91 and

1123

                        (not (pre KP_91)))

1124

                        then 9

1125

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

1126

                     then true

1127

                     else false)

1128

                  then (pre microwave_microwave_KEYPAD_PROCESSING_DISPLAY_MIDDLE_DIGIT_DIGIT_TO_DISPLAY)

1129

                  else (pre microwave_microwave_KEYPAD_PROCESSING_DISPLAY_LEFT_DIGIT_DIGIT_TO_DISPLAY))))

1130

         else (pre microwave_microwave_KEYPAD_PROCESSING_DISPLAY_LEFT_DIGIT_DIGIT_TO_DISPLAY)));

1131

1132

   microwave_microwave_KEYPAD_PROCESSING_DISPLAY_MIDDLE_DIGIT_DIGIT_TO_DISPLAY = (0 ->

1133

      (if rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clock

1134

         then

1135

               (if rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_init_step

1136

                  then 0

1137

                  else

1138

               (if KP_CLEAR

1139

                  then 0

1140

                  else

1141

(if

1142

                  (if (

1143

                     (if (KP_01 and

1144

                        (not (pre KP_01)))

1145

                        then 0

1146

                        else

1147

                     (if (KP_11 and

1148

                        (not (pre KP_11)))

1149

                        then 1

1150

                        else

1151

                     (if (KP_21 and

1152

                        (not (pre KP_21)))

1153

                        then 2

1154

                        else

1155

                     (if (KP_31 and

1156

                        (not (pre KP_31)))

1157

                        then 3

1158

                        else

1159

                     (if (KP_41 and

1160

                        (not (pre KP_41)))

1161

                        then 4

1162

                        else

1163

                     (if (KP_51 and

1164

                        (not (pre KP_51)))

1165

                        then 5

1166

                        else

1167

                     (if (KP_61 and

1168

                        (not (pre KP_61)))

1169

                        then 6

1170

                        else

1171

                     (if (KP_71 and

1172

                        (not (pre KP_71)))

1173

                        then 7

1174

                        else

1175

                     (if (KP_81 and

1176

                        (not (pre KP_81)))

1177

                        then 8

1178

                        else

1179

                     (if (KP_91 and

1180

                        (not (pre KP_91)))

1181

                        then 9

1182

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

1183

                     then true

1184

                     else false)

1185

                  then (pre microwave_microwave_KEYPAD_PROCESSING_DISPLAY_RIGHT_DIGIT_DIGIT_TO_DISPLAY)

1186

                  else (pre microwave_microwave_KEYPAD_PROCESSING_DISPLAY_MIDDLE_DIGIT_DIGIT_TO_DISPLAY))))

1187

         else (pre microwave_microwave_KEYPAD_PROCESSING_DISPLAY_MIDDLE_DIGIT_DIGIT_TO_DISPLAY)));

1188

1189

   microwave_microwave_KEYPAD_PROCESSING_DISPLAY_RIGHT_DIGIT_DIGIT_TO_DISPLAY = (

1190

      (if KP_CLEAR

1191

         then 0

1192

         else

1193

(if

1194

         (if (

1195

            (if KP_01

1196

               then 0

1197

               else

1198

            (if KP_11

1199

               then 1

1200

               else

1201

            (if KP_21

1202

               then 2

1203

               else

1204

            (if KP_31

1205

               then 3

1206

               else

1207

            (if KP_41

1208

               then 4

1209

               else

1210

            (if KP_51

1211

               then 5

1212

               else

1213

            (if KP_61

1214

               then 6

1215

               else

1216

            (if KP_71

1217

               then 7

1218

               else

1219

            (if KP_81

1220

               then 8

1221

               else

1222

            (if KP_91

1223

               then 9

1224

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

1225

            then true

1226

            else false)

1227

         then

1228

               (if KP_01

1229

                  then 0

1230

                  else

1231

               (if KP_11

1232

                  then 1

1233

                  else

1234

               (if KP_21

1235

                  then 2

1236

                  else

1237

               (if KP_31

1238

                  then 3

1239

                  else

1240

               (if KP_41

1241

                  then 4

1242

                  else

1243

               (if KP_51

1244

                  then 5

1245

                  else

1246

               (if KP_61

1247

                  then 6

1248

                  else

1249

               (if KP_71

1250

                  then 7

1251

                  else

1252

               (if KP_81

1253

                  then 8

1254

                  else

1255

               (if KP_91

1256

                  then 9

1257

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

1258

         else 0)) ->

1259

      (if rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clock

1260

         then

1261

               (if rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_init_step

1262

                  then

1263

                        (if KP_CLEAR

1264

                           then 0

1265

                           else

1266

(if

1267

                           (if (

1268

                              (if KP_01

1269

                                 then 0

1270

                                 else

1271

                              (if KP_11

1272

                                 then 1

1273

                                 else

1274

                              (if KP_21

1275

                                 then 2

1276

                                 else

1277

                              (if KP_31

1278

                                 then 3

1279

                                 else

1280

                              (if KP_41

1281

                                 then 4

1282

                                 else

1283

                              (if KP_51

1284

                                 then 5

1285

                                 else

1286

                              (if KP_61

1287

                                 then 6

1288

                                 else

1289

                              (if KP_71

1290

                                 then 7

1291

                                 else

1292

                              (if KP_81

1293

                                 then 8

1294

                                 else

1295

                              (if KP_91

1296

                                 then 9

1297

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

1298

                              then true

1299

                              else false)

1300

                           then

1301

                                 (if KP_01

1302

                                    then 0

1303

                                    else

1304

                                 (if KP_11

1305

                                    then 1

1306

                                    else

1307

                                 (if KP_21

1308

                                    then 2

1309

                                    else

1310

                                 (if KP_31

1311

                                    then 3

1312

                                    else

1313

                                 (if KP_41

1314

                                    then 4

1315

                                    else

1316

                                 (if KP_51

1317

                                    then 5

1318

                                    else

1319

                                 (if KP_61

1320

                                    then 6

1321

                                    else

1322

                                 (if KP_71

1323

                                    then 7

1324

                                    else

1325

                                 (if KP_81

1326

                                    then 8

1327

                                    else

1328

                                 (if KP_91

1329

                                    then 9

1330

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

1331

                           else 0))

1332

                  else

1333

               (if KP_CLEAR

1334

                  then 0

1335

                  else

1336

(if

1337

                  (if (

1338

                     (if (KP_01 and

1339

                        (not (pre KP_01)))

1340

                        then 0

1341

                        else

1342

                     (if (KP_11 and

1343

                        (not (pre KP_11)))

1344

                        then 1

1345

                        else

1346

                     (if (KP_21 and

1347

                        (not (pre KP_21)))

1348

                        then 2

1349

                        else

1350

                     (if (KP_31 and

1351

                        (not (pre KP_31)))

1352

                        then 3

1353

                        else

1354

                     (if (KP_41 and

1355

                        (not (pre KP_41)))

1356

                        then 4

1357

                        else

1358

                     (if (KP_51 and

1359

                        (not (pre KP_51)))

1360

                        then 5

1361

                        else

1362

                     (if (KP_61 and

1363

                        (not (pre KP_61)))

1364

                        then 6

1365

                        else

1366

                     (if (KP_71 and

1367

                        (not (pre KP_71)))

1368

                        then 7

1369

                        else

1370

                     (if (KP_81 and

1371

                        (not (pre KP_81)))

1372

                        then 8

1373

                        else

1374

                     (if (KP_91 and

1375

                        (not (pre KP_91)))

1376

                        then 9

1377

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

1378

                     then true

1379

                     else false)

1380

                  then

1381

                        (if (KP_01 and

1382

                           (not (pre KP_01)))

1383

                           then 0

1384

                           else

1385

                        (if (KP_11 and

1386

                           (not (pre KP_11)))

1387

                           then 1

1388

                           else

1389

                        (if (KP_21 and

1390

                           (not (pre KP_21)))

1391

                           then 2

1392

                           else

1393

                        (if (KP_31 and

1394

                           (not (pre KP_31)))

1395

                           then 3

1396

                           else

1397

                        (if (KP_41 and

1398

                           (not (pre KP_41)))

1399

                           then 4

1400

                           else

1401

                        (if (KP_51 and

1402

                           (not (pre KP_51)))

1403

                           then 5

1404

                           else

1405

                        (if (KP_61 and

1406

                           (not (pre KP_61)))

1407

                           then 6

1408

                           else

1409

                        (if (KP_71 and

1410

                           (not (pre KP_71)))

1411

                           then 7

1412

                           else

1413

                        (if (KP_81 and

1414

                           (not (pre KP_81)))

1415

                           then 8

1416

                           else

1417

                        (if (KP_91 and

1418

                           (not (pre KP_91)))

1419

                           then 9

1420

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

1421

                  else (pre microwave_microwave_KEYPAD_PROCESSING_DISPLAY_RIGHT_DIGIT_DIGIT_TO_DISPLAY))))

1422

         else (pre microwave_microwave_KEYPAD_PROCESSING_DISPLAY_RIGHT_DIGIT_DIGIT_TO_DISPLAY)));

1423

1424

   STEPS_TO_COOK = (

1425

      (if (rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_init_step and

1426

         (not rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clock))

1427

         then 0

1428

         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)) ->

1429

      (if (rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_init_step and

1430

         (not rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clock))

1431

         then 0

1432

         else

1433

      (if rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clock

1434

         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)

1435

         else (pre STEPS_TO_COOK))));

1436

1437

   rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_init_step = (true ->

1438

      (if (not rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clock)

1439

         then true

1440

         else

1441

      (if (pre rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clock)

1442

         then false

1443

         else (pre rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_init_step))));

1444

1445

   SETUP =

1446

      (if (1 = microwave_microwave_mode_logic_mode)

1447

         then true

1448

         else false);

1449

1450

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

1451

      (not KP_CLEAR))) or

1452

      ((not ((KP_5 and

1453

      (not (pre KP_5))) and

1454

      ((not (KP_4 and

1455

      (not (pre KP_4)))) and

1456

      ((not (KP_3 and

1457

      (not (pre KP_3)))) and

1458

      ((not (KP_2 and

1459

      (not (pre KP_2)))) and

1460

      ((not (KP_1 and

1461

      (not (pre KP_1)))) and

1462

      (not (KP_0 and

1463

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

1464

      (RIGHT_DIGIT = 5))));

1465

1466

   enable = (true ->

1467

      (if (1 = (pre microwave_microwave_mode_logic_mode))

1468

         then true

1469

         else false));

1470

1471

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

1472

      (not KP_CLEAR))) or

1473

      ((not ((KP_1 and

1474

      (not (pre KP_1))) and

1475

      (not (KP_0 and

1476

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

1477

      (RIGHT_DIGIT = 1))));

1478

1479

   p13 = ((not (enable and

1480

      KP_CLEAR)) or

1481

      (STEPS_TO_COOK = 0));

1482

1483

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

1484

      (not KP_CLEAR))) or

1485

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

1486

      (not (pre KP_1))) or

1487

      (KP_2 and

1488

      (not (pre KP_2)))) or

1489

      (KP_3 and

1490

      (not (pre KP_3)))) or

1491

      (KP_4 and

1492

      (not (pre KP_4)))) or

1493

      (KP_5 and

1494

      (not (pre KP_5)))) or

1495

      (KP_6 and

1496

      (not (pre KP_6)))) or

1497

      (KP_7 and

1498

      (not (pre KP_7)))) or

1499

      (KP_8 and

1500

      (not (pre KP_8)))) or

1501

      (KP_9 and

1502

      (not (pre KP_9)))) or

1503

      (KP_0 and

1504

      (not (pre KP_0)))) or

1505

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

1506

1507

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

1508

      (not KP_CLEAR))) or

1509

      ((not ((KP_2 and

1510

      (not (pre KP_2))) and

1511

      ((not (KP_1 and

1512

      (not (pre KP_1)))) and

1513

      (not (KP_0 and

1514

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

1515

      (RIGHT_DIGIT = 2))));

1516

1517

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

1518

      (not KP_CLEAR))) or

1519

      ((not ((KP_7 and

1520

      (not (pre KP_7))) and

1521

      ((not (KP_6 and

1522

      (not (pre KP_6)))) and

1523

      ((not (KP_5 and

1524

      (not (pre KP_5)))) and

1525

      ((not (KP_4 and

1526

      (not (pre KP_4)))) and

1527

      ((not (KP_3 and

1528

      (not (pre KP_3)))) and

1529

      ((not (KP_2 and

1530

      (not (pre KP_2)))) and

1531

      ((not (KP_1 and

1532

      (not (pre KP_1)))) and

1533

      (not (KP_0 and

1534

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

1535

      (RIGHT_DIGIT = 7))));

1536

1537

   p12 = (enable or

1538

      (STEPS_TO_COOK = 0));

1539

1540

   p21 = ((not (enable and

1541

      KP_CLEAR)) or

1542

      (MIDDLE_DIGIT = 0));

1543

1544

  --%PROPERTY OK=true;

1545

  --%MAIN;

1546

1547

tel

Project

General

Profile

CristalCaveGem » LustreC » Lustrec-Tests

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