Grcov report - tests.rs

1

// This file will not be overwritten if codegen is rerun

2

3

//----------------------------------------------------------------

4

//  This file illustrates three types of HAMR unit (thread application code)

5

//  testing:

6

//    - manual tests

7

//    - manual GUMBOX tests

8

//    - automated randomized GUMBOX tests (property-based testing)

9

//

10

//  See explanations for the mechanics and purpose of each type of test

11

//  in the header sections below.

12

//----------------------------------------------------------------

13

14

15

//================================================================

16

//++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++

17

//

18

//  M a n u a l l y - w r i t t e n    U n i t    T e s t s

19

//

20

//  These examples illustrate how to use the basic APIs auto-generated

21

//  by HAMR to support unit testing for a HAMR thread component.

22

//  The test APIs are found in src/test/util/test_apis.rs and are

23

//  re-generated each time HAMR code generation is run (e.g., after

24

//  changes are made to model structures or model contracts).

25

//

26

//  In manually written tests, code is written to

27

//   - construct a set of component inputs,

28

//  i.e., a "test vector" that provides a value

29

//  for each input port (and optionally, each GUMBO-specified component

30

//  variable (GSV))

31

//   - put the test vector values into the component's inputs via `put_`

32

//     API calls

33

//   - invoke a component entry point (e.g., the compute entry point)

34

//     to run component application code (which will leave values in

35

//     output ports and update GSVs)

36

//   - get values of component output ports and GSVs via `get_` APIs.

37

//   - compare output values with expected values via `assert!(..)`

38

//

39

//++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++

40

//================================================================

41

42

43

mod tests {

44

  // NOTE: need to run tests sequentially to prevent race conditions

45

  //       on the app and the testing apis which are static

46

  use serial_test::serial;

47

48

  use crate::test::util::*;

49

  use data::*;

50

  use data::Isolette_Data_Model::*; // Add for easier reference of data types

51

52

  // auto-generated example test for initialize entry point

53

  #[test]

54

  #[serial]

55

2

  fn test_initialization() {

56

2

    // invoke initialize entry point

57

2

    crate::thermostat_thermostat_initialize();

58

59

    // use auto-generated test APIs to retrieve values of

60

    // output ports and GUMBO-defined local state as illustrated below

61

62

    // let heat_control: On_Off = test_apis::get_heat_control();

63

    // let post_lastCmd : On_Off = test_apis::get_lastCmd();

64

65

    // ..compare outputs to expected results..

66

    // assert!(..)

67

68

69

  #[test]

70

  #[serial]

71

2

  fn test_initialization_REQ_THERM_1() {

72

2

    // invoke initialize entry point

73

2

    crate::thermostat_thermostat_initialize();

74

2

75

2

    // use auto-generated test APIs to retrieve values of

76

2

    // output ports and GUMBO-defined local state

77

2

    let heat_control: On_Off = test_apis::get_heat_control(); // output port

78

2

    let post_lastCmd : On_Off = test_apis::get_lastCmd(); // GUMBO defined local state (post-state value)

79

2

80

2

    // ..compare outputs to expected results..

81

2

    // REQ_THERM_1

82

2

    //  - The Heat Control command shall be initially Off

83

2

    assert!(heat_control == On_Off::Off);

84

2

    assert!(post_lastCmd == On_Off::Off);

85

86

87

  // auto-generated example test for `compute` entry point

88

  #[test]

89

  #[serial]

90

2

  fn test_compute() {

91

2

    // initialize entry point should always be called to initialize

92

2

    // output ports and local state

93

2

    crate::thermostat_thermostat_initialize();

94

2

95

2

    // implement input of "test vector"

96

2

    // ..set values for input data ports

97

2

    test_apis::put_current_temp(Isolette_Data_Model::Temp::default());

98

2

    test_apis::put_desired_temp(Isolette_Data_Model::Set_Points::default());

99

2

    // ..[optional] set values for GUMBO-declared local state variables

100

2

    test_apis::put_lastCmd(Isolette_Data_Model::On_Off::default());

101

2

102

2

    // invoke initialize entry point

103

2

    crate::thermostat_thermostat_timeTriggered();

104

105

    // use auto-generated test APIs to retrieve values of

106

    // output ports and GUMBO-defined local state as illustrated below

107

108

    // let heat_control: On_Off = test_apis::get_heat_control();

109

    // let post_lastCmd : On_Off = test_apis::get_lastCmd();

110

111

    // ..compare outputs to expected results..

112

    // assert!(..)

113

114

115

116

  //========================================================================

117

  //  REQ-THERM-2: If Current Temperature is less than the Lower Desired Temperature,

118

  //  the Heat Control shall be set to On.

119

  //========================================================================

120

121

/*

122

       Inputs:

123

         current_temp:  95f

124

         lower_desired_temp: 98f

125

         upper_desired_temp: *irrelevant to requirement* (use 100f)

126

127

       Expected Outputs:

128

         heat_control: On

129

         last_cmd (post): On

130

*/

131

  #[test]

132

  #[serial]

133

2

  fn test_compute_REQ_THERM_2() {

134

2

    // [InvokeEntryPoint]: invoke the entry point test method

135

2

    crate::thermostat_thermostat_initialize();

136

2

137

2

    // generate values for the incoming data ports

138

2

    let current_temp = Temp { degrees: 95 };

139

2

    let lower_desired_temp = Temp { degrees: 98 };

140

2

    let upper_desired_temp = Temp { degrees: 100 };

141

2

    let desired_temp = Set_Points {lower: lower_desired_temp, upper: upper_desired_temp};

142

2

143

2

    // [PutInPorts]: put values on the input ports

144

2

    test_apis::put_current_temp(current_temp);

145

2

    test_apis::put_desired_temp(desired_temp);

146

2

147

2

    // [InvokeEntryPoint]: Invoke the entry point

148

2

    crate::thermostat_thermostat_timeTriggered();

149

2

150

2

    // get result values from output ports

151

2

    let api_heat_control = test_apis::get_heat_control();

152

2

    let lastCmd = test_apis::get_lastCmd();

153

2

154

2

    assert!(api_heat_control == On_Off::Onn);

155

2

    assert!(lastCmd == On_Off::Onn);

156

157

158

  #[test]

159

  #[serial]

160

2

  fn test_compute_REQ_THERM_2_container() { // Alternate version: Illustrate "container"-based APIs

161

2

    // [InvokeEntryPoint]: invoke the entry point test method

162

2

    crate::thermostat_thermostat_initialize();

163

2

164

2

    // Inputs can be "bundled" into a container and put "all at once".

165

2

    // There are two versions Pre-State-Container: one without inputs

166

2

    // for GUMBO state variables (GSV) and one that includes them.  Below

167

2

    // illustrates the version without.   In this case, GSVs retain

168

2

    // whatever value they have at the time of the Compute entry point

169

2

    // (timeTriggered method) invocation.

170

2

    let preStateContainer = test_apis::PreStateContainer {

171

2

      api_current_temp : Temp { degrees: 95},

172

2

      api_desired_temp : Set_Points {

173

2

        lower: Temp { degrees:  98 },

174

2

        upper: Temp { degrees: 100 }

175

2

176

2

};

177

2

178

2

    // [PutInPorts]: put values on the input ports

179

2

    test_apis::put_concrete_inputs_container(preStateContainer);

180

2

181

2

    // [InvokeEntryPoint]: Invoke the entry point

182

2

    crate::thermostat_thermostat_timeTriggered();

183

2

184

2

    // get result values from output ports

185

2

    let api_heat_control = test_apis::get_heat_control();

186

2

    let lastCmd = test_apis::get_lastCmd();

187

2

188

2

    assert!(api_heat_control == On_Off::Onn);

189

2

    assert!(lastCmd == On_Off::Onn);

190

191

192

  //. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

193

  //  Illustrate use of helper functions for repeated patterns

194

  //. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

195

196

2

  fn test_compute_THERM_helper(

197

2

    // container

198

2

    inputs: test_apis::PreStateContainer,

199

2

    // expected result

200

2

    expected_ouput: On_Off)

201

2

202

2

    // [InvokeEntryPoint]: invoke the entry point test method

203

2

    crate::thermostat_thermostat_initialize();

204

2

205

2

    // [PutInPorts]: put values on the input ports

206

2

    test_apis::put_concrete_inputs_container(inputs);

207

2

208

2

    // [InvokeEntryPoint]: Invoke the entry point

209

2

    crate::thermostat_thermostat_timeTriggered();

210

2

211

2

    // get result values from output ports

212

2

    let api_heat_control = test_apis::get_heat_control();

213

2

    let lastCmd = test_apis::get_lastCmd();

214

2

215

2

    assert!(api_heat_control == expected_ouput);

216

2

    assert!(lastCmd == expected_ouput);

217

2

218

219

  #[test]

220

  #[serial]

221

2

  fn test_compute_REQ_THERM_3_container() { // Alternate version: Illustrate "container"-based APIs

222

2

    // [InvokeEntryPoint]: invoke the entry point test method

223

2

    crate::thermostat_thermostat_initialize();

224

2

225

2

    let preStateContainer = test_apis::PreStateContainer {

226

2

      api_current_temp : Temp { degrees: 101},

227

2

      api_desired_temp : Set_Points {

228

2

        lower: Temp { degrees:  98 },

229

2

        upper: Temp { degrees: 100 }

230

2

231

2

};

232

2

233

2

    // [PutInPorts]: put values on the input ports

234

2

    test_apis::put_concrete_inputs_container(preStateContainer);

235

2

236

2

    // [InvokeEntryPoint]: Invoke the entry point

237

2

    crate::thermostat_thermostat_timeTriggered();

238

2

239

2

    // get result values from output ports

240

2

    let api_heat_control = test_apis::get_heat_control();

241

2

    let lastCmd = test_apis::get_lastCmd();

242

2

243

2

    assert!(api_heat_control == On_Off::Off);

244

2

    assert!(lastCmd == On_Off::Off);

245

246

247

  #[test]

248

  #[serial]

249

2

  fn test_compute_REQ_THERM_2_helper() { // Alternate version: Illustrate "container"-based helpers

250

2

     test_compute_THERM_helper(

251

2

     test_apis::PreStateContainer {

252

2

        api_current_temp : Temp { degrees: 95},

253

2

        api_desired_temp : Set_Points {

254

2

          lower: Temp { degrees:  98 },

255

2

          upper: Temp { degrees: 100 }

256

2

257

2

},

258

2

    On_Off::Onn

259

);

260

261

262

263

  // EXERCISES:

264

  //  - construct a test for REQ-THERM-3, making direct use of APIs

265

  //    without a container

266

  //  - construct an alternate test for REQ-THERM-3, using a container structure

267

  //    and the method `put_concrete_inputs_container`

268

  //  - construct an alternate test for REQ-THERM-3 that uses the

269

  //    helper method `test_compute_THERM_helper`

270

271

272

   //========================================================================

273

 //  REQ-THERM-4: If the Current Temperature is greater than or equal

274

 //  to the Lower Desired Temperature and less than or equal to the

275

 //  Upper Desired Temperature, the value of the Heat Control shall not be changed.":

276

 //========================================================================

277

278

  // Test design notes:

279

  // the "shall not be changed" requires reasoning about the internal

280

  // state of the component (saved heat control value) or about the value

281

  // of the heat control output on the previous activation.  To test the requirement above,

282

  // we create a sequence of activations and assertions that capture the requirement

283

  // in terms of values on previous activations.  An alternative approach is to

284

  // modify the internal state of the component directly -- that approach is

285

  // illustrated in the REQ-THERM-4-alt tests.

286

287

  //. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

288

  //  Illustrate "inheriting" values of last_cmd from previous iterations

289

  //. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

290

291

  #[test]

292

  #[serial]

293

2

  fn test_compute_REQ_THERM_4() {

294

2

    // [InvokeEntryPoint]: invoke the entry point test method

295

2

    crate::thermostat_thermostat_initialize();

296

2

297

2

    // Activation 1: Cause heat control to be On

298

2

299

2

/*

300

2

      Inputs:

301

2

        current_tempWstatus  95f

302

2

        lower_desired_temp: (use 98f)

303

2

        upper_desired_temp: (use 100f)

304

2

305

2

      Expected Outputs:

306

2

        heat_control: On

307

2

        last_cmd: On

308

2

*/

309

2

310

2

    // generate values for the incoming data ports

311

2

    let current_temp = Temp { degrees: 95 };

312

2

    let lower_desired_temp = Temp { degrees: 98 };

313

2

    let upper_desired_temp = Temp { degrees: 100 };

314

2

    let desired_temp = Set_Points {lower: lower_desired_temp, upper: upper_desired_temp};

315

2

316

2

    // [PutInPorts]: put values on the input ports

317

2

    test_apis::put_current_temp(current_temp);

318

2

    test_apis::put_desired_temp(desired_temp);

319

2

320

2

    // [InvokeEntryPoint]: Invoke the entry point

321

2

    crate::thermostat_thermostat_timeTriggered();

322

2

323

2

    // get result values from output ports

324

2

    let api_heat_control = test_apis::get_heat_control();

325

2

    let lastCmd = test_apis::get_lastCmd();

326

2

327

2

    assert!(api_heat_control == On_Off::Onn);

328

2

    assert!(lastCmd == On_Off::Onn);

329

330

    // Activation 1-a: Current temp lies within set points (closed interval)

331

    //   in this case current temp is equal to lower bound,

332

    //   so heat control should still be on

333

/*

334

       Inputs:

335

         current_tempWstatus  98f

336

         lower_desired_temp: (use 98f)

337

         upper_desired_temp: (use 100f)

338

         regulator_mode: Normal

339

340

       Expected Outputs:

341

         heat_control: On

342

         last_cmd: On

343

*/

344

345

    // generate values for the incoming data ports

346

2

    let current_temp = Temp { degrees: 98 };

347

2

    let lower_desired_temp = Temp { degrees: 98 };

348

2

    let upper_desired_temp = Temp { degrees: 100 };

349

2

    let desired_temp = Set_Points {lower: lower_desired_temp, upper: upper_desired_temp};

350

2

351

2

    // [PutInPorts]: put values on the input ports

352

2

    test_apis::put_current_temp(current_temp);

353

2

    test_apis::put_desired_temp(desired_temp);

354

2

355

2

    // [InvokeEntryPoint]: Invoke the entry point

356

2

    crate::thermostat_thermostat_timeTriggered();

357

2

358

2

    // get result values from output ports

359

2

    let api_heat_control = test_apis::get_heat_control();

360

2

    let lastCmd = test_apis::get_lastCmd();

361

2

362

2

    assert!(api_heat_control == On_Off::Onn);

363

2

    assert!(lastCmd == On_Off::Onn);

364

365

    // Activation 1-b: Current temp lies within set points (closed interval)

366

    //   in this case current temp is between lower bound and upper bound,

367

    //   so heat control should still be on

368

/*

369

       Inputs:

370

         current_tempWstatus  99f

371

         lower_desired_temp: (use 98f)

372

         upper_desired_temp: (use 100f)

373

         regulator_mode: Normal

374

375

       Expected Outputs:

376

         heat_control: On

377

         last_cmd: On

378

*/

379

380

   // generate values for the incoming data ports

381

2

    let current_temp = Temp { degrees: 99 };

382

2

    let lower_desired_temp = Temp { degrees: 98 };

383

2

    let upper_desired_temp = Temp { degrees: 100 };

384

2

    let desired_temp = Set_Points {lower: lower_desired_temp, upper: upper_desired_temp};

385

2

386

2

    // [PutInPorts]: put values on the input ports

387

2

    test_apis::put_current_temp(current_temp);

388

2

    test_apis::put_desired_temp(desired_temp);

389

2

390

2

    // [InvokeEntryPoint]: Invoke the entry point

391

2

    crate::thermostat_thermostat_timeTriggered();

392

2

393

2

    // get result values from output ports

394

2

    let api_heat_control = test_apis::get_heat_control();

395

2

    let lastCmd = test_apis::get_lastCmd();

396

2

397

2

    assert!(api_heat_control == On_Off::Onn);

398

2

    assert!(lastCmd == On_Off::Onn);

399

400

    // Activation 1-c: Current temp lies within set points (closed interval)

401

    //   in this case current temp is equal to upper bound,

402

    //   so heat control should still be on

403

404

/*

405

       Inputs:

406

         current_tempWstatus  100f

407

         lower_desired_temp: (use 98f)

408

         upper_desired_temp: (use 100f)

409

         regulator_mode: Normal

410

411

       Expected Outputs:

412

         heat_control: On

413

         last_cmd: On

414

*/

415

416

    // generate values for the incoming data ports

417

2

    let current_temp = Temp { degrees: 100 };

418

2

    let lower_desired_temp = Temp { degrees: 98 };

419

2

    let upper_desired_temp = Temp { degrees: 100 };

420

2

    let desired_temp = Set_Points {lower: lower_desired_temp, upper: upper_desired_temp};

421

2

422

2

    // [PutInPorts]: put values on the input ports

423

2

    test_apis::put_current_temp(current_temp);

424

2

    test_apis::put_desired_temp(desired_temp);

425

2

426

2

    // [InvokeEntryPoint]: Invoke the entry point

427

2

    crate::thermostat_thermostat_timeTriggered();

428

2

429

2

    // get result values from output ports

430

2

    let api_heat_control = test_apis::get_heat_control();

431

2

    let lastCmd = test_apis::get_lastCmd();

432

2

433

2

    assert!(api_heat_control == On_Off::Onn);

434

2

    assert!(lastCmd == On_Off::Onn);

435

436

    // Activation 2:   Cause the heat control to be off

437

    //   Current temp lies above set points

438

    //   in this case current temp is greater than upper bound,

439

    //   so heat control should be off

440

/*

441

       Inputs:

442

         current_tempWstatus  101f

443

         lower_desired_temp: (use 98f)

444

         upper_desired_temp: (use 100f)

445

         regulator_mode: Normal

446

447

       Expected Outputs:

448

         heat_control: Off

449

         last_cmd: Off

450

*/

451

452

    // generate values for the incoming data ports

453

2

    let current_temp = Temp { degrees: 101 };

454

2

    let lower_desired_temp = Temp { degrees: 98 };

455

2

    let upper_desired_temp = Temp { degrees: 100 };

456

2

    let desired_temp = Set_Points {lower: lower_desired_temp, upper: upper_desired_temp};

457

2

458

2

    // [PutInPorts]: put values on the input ports

459

2

    test_apis::put_current_temp(current_temp);

460

2

    test_apis::put_desired_temp(desired_temp);

461

2

462

2

    // [InvokeEntryPoint]: Invoke the entry point

463

2

    crate::thermostat_thermostat_timeTriggered();

464

2

465

2

    // get result values from output ports

466

2

    let api_heat_control = test_apis::get_heat_control();

467

2

    let lastCmd = test_apis::get_lastCmd();

468

2

469

2

    assert!(api_heat_control == On_Off::Off);

470

2

    assert!(lastCmd == On_Off::Off);

471

472

    // Activation 2-a:

473

    //   Current temp lies within set points (closed interval)

474

    //   in this case current temp is equal to upper bound,

475

    //   so heat control should still be off

476

477

/*

478

       Inputs:

479

         current_tempWstatus  100f

480

         lower_desired_temp: (use 98f)

481

         upper_desired_temp: (use 100f)

482

         regulator_mode: Normal

483

484

       Expected Outputs:

485

         heat_control: Off

486

         last_cmd: Off

487

*/

488

489

    // generate values for the incoming data ports

490

2

    let current_temp = Temp { degrees: 100 };

491

2

    let lower_desired_temp = Temp { degrees: 98 };

492

2

    let upper_desired_temp = Temp { degrees: 100 };

493

2

    let desired_temp = Set_Points {lower: lower_desired_temp, upper: upper_desired_temp};

494

2

495

2

    // [PutInPorts]: put values on the input ports

496

2

    test_apis::put_current_temp(current_temp);

497

2

    test_apis::put_desired_temp(desired_temp);

498

2

499

2

    // [InvokeEntryPoint]: Invoke the entry point

500

2

    crate::thermostat_thermostat_timeTriggered();

501

2

502

2

    // get result values from output ports

503

2

    let api_heat_control = test_apis::get_heat_control();

504

2

    let lastCmd = test_apis::get_lastCmd();

505

2

506

2

    assert!(api_heat_control == On_Off::Off);

507

2

    assert!(lastCmd == On_Off::Off);

508

509

    // Activation 2-b:

510

    //   Current temp lies within set points (closed interval)

511

    //   in this case current temp is between lower and upper bound,

512

    //   so heat control should still be off

513

514

/*

515

       Inputs:

516

         current_tempWstatus  99f

517

         lower_desired_temp: (use 98f)

518

         upper_desired_temp: (use 100f)

519

         regulator_mode: Normal

520

521

       Expected Outputs:

522

         heat_control: Off

523

         last_cmd: Off

524

*/

525

526

    // generate values for the incoming data ports

527

2

    let current_temp = Temp { degrees: 99 };

528

2

    let lower_desired_temp = Temp { degrees: 98 };

529

2

    let upper_desired_temp = Temp { degrees: 100 };

530

2

    let desired_temp = Set_Points {lower: lower_desired_temp, upper: upper_desired_temp};

531

2

532

2

    // [PutInPorts]: put values on the input ports

533

2

    test_apis::put_current_temp(current_temp);

534

2

    test_apis::put_desired_temp(desired_temp);

535

2

536

2

    // [InvokeEntryPoint]: Invoke the entry point

537

2

    crate::thermostat_thermostat_timeTriggered();

538

2

539

2

    // get result values from output ports

540

2

    let api_heat_control = test_apis::get_heat_control();

541

2

    let lastCmd = test_apis::get_lastCmd();

542

2

543

2

    assert!(api_heat_control == On_Off::Off);

544

2

    assert!(lastCmd == On_Off::Off);

545

546

    // Activation 2-c:

547

    //   Current temp lies within set points (closed interval)

548

    //   in this case current temp is equal to lower bound,

549

    //   so heat control should still be off

550

/*

551

       Inputs:

552

         current_tempWstatus  98f

553

         lower_desired_temp: (use 98f)

554

         upper_desired_temp: (use 100f)

555

         regulator_mode: Normal

556

557

       Expected Outputs:

558

         heat_control: Off

559

         last_cmd: Off

560

*/

561

562

    // generate values for the incoming data ports

563

2

    let current_temp = Temp { degrees: 98 };

564

2

    let lower_desired_temp = Temp { degrees: 98 };

565

2

    let upper_desired_temp = Temp { degrees: 100 };

566

2

    let desired_temp = Set_Points {lower: lower_desired_temp, upper: upper_desired_temp};

567

2

568

2

    // [PutInPorts]: put values on the input ports

569

2

    test_apis::put_current_temp(current_temp);

570

2

    test_apis::put_desired_temp(desired_temp);

571

2

572

2

    // [InvokeEntryPoint]: Invoke the entry point

573

2

    crate::thermostat_thermostat_timeTriggered();

574

2

575

2

    // get result values from output ports

576

2

    let api_heat_control = test_apis::get_heat_control();

577

2

    let lastCmd = test_apis::get_lastCmd();

578

2

579

2

    assert!(api_heat_control == On_Off::Off);

580

2

    assert!(lastCmd == On_Off::Off);

581

582

583

584

  //. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

585

  //  Illustrate explicit setting of last_cmd

586

  //. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

587

588

  // Activation 1-a: Current temp lies within set points (closed interval)

589

  //   in this case current temp is equal to lower bound,

590

  //   so heat control should still be on

591

/*

592

     Inputs:

593

      current_tempWstatus  98

594

      lower_desired_temp: (use 98)

595

      upper_desired_temp: (use 100)

596

597

    ** force previous heat_control lastCmd to ON **

598

599

     Expected Outputs:

600

      heat_control: On

601

      last_cmd: On

602

*/

603

604

  #[test]

605

  #[serial]

606

2

  fn test_compute_REQ_THERM_4_alt_1_a() {

607

2

    // [InvokeEntryPoint]: invoke the entry point test method

608

2

    crate::thermostat_thermostat_initialize();

609

2

610

2

    // generate values for the incoming data ports

611

2

    let current_temp = Temp { degrees: 98 };

612

2

    let lower_desired_temp = Temp { degrees: 98 };

613

2

    let upper_desired_temp = Temp { degrees: 100 };

614

2

    let desired_temp = Set_Points {lower: lower_desired_temp, upper: upper_desired_temp};

615

2

616

2

    // [PutInPorts]: put values on the input ports

617

2

    test_apis::put_current_temp(current_temp);

618

2

    test_apis::put_desired_temp(desired_temp);

619

2

620

2

    // set component internal state (last_cmd) to Onn

621

2

    test_apis::put_lastCmd(On_Off::Onn);

622

2

623

2

    // [InvokeEntryPoint]: Invoke the entry point

624

2

    crate::thermostat_thermostat_timeTriggered();

625

2

626

2

    // get result values from output ports

627

2

    let api_heat_control = test_apis::get_heat_control();

628

2

    let lastCmd = test_apis::get_lastCmd();

629

2

630

2

    assert!(api_heat_control == On_Off::Onn);

631

2

    assert!(lastCmd == On_Off::Onn);

632

633

634

  // Activation 1-b: Current temp lies within set points (closed interval)

635

  //   in this case current temp is between lower bound and upper bound,

636

  //   so heat control should still be on

637

/*

638

     Inputs:

639

       current_tempWstatus  99f

640

       lower_desired_temp: (use 98f)

641

       upper_desired_temp: (use 100f)

642

       regulator_mode: Normal

643

644

       ** force previous heat_control lastCmd to ON **

645

646

     Expected Outputs:

647

       heat_control: On

648

       last_cmd: On

649

*/

650

651

  #[test]

652

  #[serial]

653

2

  fn test_compute_REQ_THERM_4_alt_1_b() {

654

2

    // [InvokeEntryPoint]: invoke the entry point test method

655

2

    crate::thermostat_thermostat_initialize();

656

2

657

2

    // generate values for the incoming data ports

658

2

    let current_temp = Temp { degrees: 99 };

659

2

    let lower_desired_temp = Temp { degrees: 98 };

660

2

    let upper_desired_temp = Temp { degrees: 100 };

661

2

    let desired_temp = Set_Points {lower: lower_desired_temp, upper: upper_desired_temp};

662

2

663

2

    // [PutInPorts]: put values on the input ports

664

2

    test_apis::put_current_temp(current_temp);

665

2

    test_apis::put_desired_temp(desired_temp);

666

2

667

2

    // set component internal state (last_cmd) to Onn

668

2

    test_apis::put_lastCmd(On_Off::Onn);

669

2

670

2

    // [InvokeEntryPoint]: Invoke the entry point

671

2

    crate::thermostat_thermostat_timeTriggered();

672

2

673

2

    // get result values from output ports

674

2

    let api_heat_control = test_apis::get_heat_control();

675

2

    let lastCmd = test_apis::get_lastCmd();

676

2

677

2

    assert!(api_heat_control == On_Off::Onn);

678

2

    assert!(lastCmd == On_Off::Onn);

679

680

681

  // Activation 1-c: Current temp lies within set points (closed interval)

682

  //   in this case current temp is equal to upper bound,

683

  //   so heat control should still be on

684

685

/*

686

     Inputs:

687

       current_tempWstatus  100f

688

       lower_desired_temp: (use 98f)

689

       upper_desired_temp: (use 100f)

690

       regulator_mode: Normal

691

692

       ** force previous heat_control lastCmd to ON **

693

694

     Expected Outputs:

695

      heat_control: On

696

      last_cmd: On

697

*/

698

699

  #[test]

700

  #[serial]

701

2

  fn test_compute_REQ_THERM_4_alt_1_c() {

702

2

    // [InvokeEntryPoint]: invoke the entry point test method

703

2

    crate::thermostat_thermostat_initialize();

704

2

705

2

    // generate values for the incoming data ports

706

2

    let current_temp = Temp { degrees: 100 };

707

2

    let lower_desired_temp = Temp { degrees: 98 };

708

2

    let upper_desired_temp = Temp { degrees: 100 };

709

2

    let desired_temp = Set_Points {lower: lower_desired_temp, upper: upper_desired_temp};

710

2

711

2

    // [PutInPorts]: put values on the input ports

712

2

    test_apis::put_current_temp(current_temp);

713

2

    test_apis::put_desired_temp(desired_temp);

714

2

715

2

    // set component internal state (last_cmd) to Onn

716

2

    test_apis::put_lastCmd(On_Off::Onn);

717

2

718

2

    // [InvokeEntryPoint]: Invoke the entry point

719

2

    crate::thermostat_thermostat_timeTriggered();

720

2

721

2

    // get result values from output ports

722

2

    let api_heat_control = test_apis::get_heat_control();

723

2

    let lastCmd = test_apis::get_lastCmd();

724

2

725

2

    assert!(api_heat_control == On_Off::Onn);

726

2

    assert!(lastCmd == On_Off::Onn);

727

728

729

  //. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

730

  //  Illustrate use of helper functions for repeated patterns

731

  //. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

732

733

6

  fn test_compute_THERM_helper_wGSV(

734

6

    // container with GUMBO local state

735

6

    inputs: test_apis::PreStateContainer_wGSV,

736

6

    // expected result

737

6

    expected_ouput: On_Off)

738

6

739

6

    // [InvokeEntryPoint]: invoke the entry point test method

740

6

    crate::thermostat_thermostat_initialize();

741

6

742

6

    // [PutInPorts]: put values on the input ports and set GUMBO state variables

743

6

    test_apis::put_concrete_inputs_container_wGSV(inputs);

744

6

745

6

    // [InvokeEntryPoint]: Invoke the entry point

746

6

    crate::thermostat_thermostat_timeTriggered();

747

6

748

6

    // get result values from output ports

749

6

    let api_heat_control = test_apis::get_heat_control();

750

6

    let lastCmd = test_apis::get_lastCmd();

751

6

752

6

    assert!(api_heat_control == expected_ouput);

753

6

    assert!(lastCmd == expected_ouput);

754

6

755

756

  // Activation 2-a:

757

  //   Current temp lies within set points (closed interval)

758

  //   in this case current temp is equal to upper bound,

759

  //   so heat control should still be off

760

761

/*

762

     Inputs:

763

       current_tempWstatus  100f  (validity: don't care (use Valid))

764

       lower_desired_temp: (use 98f)

765

       upper_desired_temp: (use 100f)

766

       regulator_mode: Normal

767

768

     ** force previous heat_control lastCmd to OFF **

769

770

     Expected Outputs:

771

        heat_control: Off

772

        last_cmd: Off

773

*/

774

775

  #[test]

776

  #[serial]

777

2

  fn test_compute_REQ_THERM_4_alt_2_a() {

778

2

    test_compute_THERM_helper_wGSV(

779

2

      test_apis::PreStateContainer_wGSV {

780

2

        In_lastCmd: On_Off::Off,

781

2

        api_current_temp : Temp { degrees: 100},

782

2

        api_desired_temp : Set_Points {

783

2

          lower: Temp { degrees:  98 },

784

2

          upper: Temp { degrees: 100 }

785

2

786

2

},

787

2

      On_Off::Off);  // expected

788

789

790

  // Activation 2-b:

791

  //   Current temp lies within set points (closed interval)

792

  //   in this case current temp is between lower and upper bound,

793

  //   so heat control should still be off

794

795

/*

796

     Inputs:

797

       current_tempWstatus  99f  (validity: don't care (use Valid))

798

       lower_desired_temp: (use 98f)

799

       upper_desired_temp: (use 100f)

800

       regulator_mode: Normal

801

802

    ** force previous heat_control lastCmd to OFF **

803

804

     Expected Outputs:

805

       heat_control: Off

806

*/

807

808

  #[test]

809

  #[serial]

810

2

  fn test_compute_REQ_THERM_4_alt_2_b() {

811

2

    test_compute_THERM_helper_wGSV(

812

2

      test_apis::PreStateContainer_wGSV {

813

2

        In_lastCmd: On_Off::Off,

814

2

        api_current_temp : Temp { degrees: 99},

815

2

        api_desired_temp : Set_Points {

816

2

          lower: Temp { degrees:  98 },

817

2

          upper: Temp { degrees: 100 }

818

2

819

2

},

820

2

      On_Off::Off); // expected

821

822

823

  // Activation 2-c:

824

  //   Current temp lies within set points (closed interval)

825

  //   in this case current temp is equal to lower bound,

826

  //   so heat control should still be off

827

/*

828

     Inputs:

829

       current_tempWstatus  98f

830

       lower_desired_temp: (use 98f)

831

       upper_desired_temp: (use 100f)

832

       regulator_mode: Normal

833

834

    ** force previous heat_control lastCmd to OFF **

835

836

     Expected Outputs:

837

       heat_control: Off

838

*/

839

840

  #[test]

841

  #[serial]

842

2

  fn test_compute_REQ_THERM_4_alt_2_c() {

843

2

    test_compute_THERM_helper_wGSV(

844

2

      test_apis::PreStateContainer_wGSV {

845

2

        In_lastCmd: On_Off::Off,

846

2

        api_current_temp : Temp { degrees: 98},

847

2

        api_desired_temp : Set_Points {

848

2

          lower: Temp { degrees:  98 },

849

2

          upper: Temp { degrees: 100 }

850

2

851

2

},

852

2

      On_Off::Off); // expected

853

854

855

856

857

//================================================================

858

//++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++

859

//

860

//  M a n u a l l y - w r i t t e n    G U M B O X  (contract-based)  T e s t s

861

//

862

//  These examples illustrate how to use the GUMBOX APIs auto-generated

863

//  by HAMR to support contract-based unit testing for a HAMR thread component.

864

//  The test APIs are found in src/test/util/cb_apis.rs and are

865

//  re-generated each time HAMR code generation is run (e.g., after

866

//  changes are made to model structures or model contracts).

867

//

868

//  When HAMR code generation is run, if a thread component has GUMBO

869

//  contracts declared for it, in addition to generating "logical"

870

//  Verus contracts for the application entry point methods, e.g.,

871

//  in `component/thermostat_process_thermostat_app.rs` to be verified

872

//  by Verus SMT-based verification, HAMR will generate "executable" versions

873

//  of the contracts as Rust boolean functions that can be called to

874

//  support unit testing and run-time monitoring.  These boolean functions

875

//  can be found in the `bridge/<component_instance_name>_GUMBOX.rs` file

876

//  for a component.

877

//

878

//  There are two styles of unit testing supported:

879

//   - manual GUMBOX tests - in which the developer directly constructs

880

//     an input test vector,

881

//   - automated property-based testing - in which HAMR generates infrastructure

882

//     to automatically generate random test vectors for testing the component.

883

//

884

//  In manual GUMBOX tests, code is written to

885

//   - construct a set of component inputs,

886

//  i.e., a "test vector" that provides a value

887

//  for each input port (and optionally, each GUMBO-specified component

888

//  variable (GSV))

889

//   - call the HAMR-generated `cb_apis::testComputeCB` method.

890

//     This method

891

//       - checks that the supplied test vector satisfies the pre-condition,

892

//       - puts the values of the test vector into the component input ports

893

//       - invokes the compute entry point

894

//       - gets the values in the output ports of the test vector

895

//       - checks that the compute entry point post-condition on the

896

//         output port values and input test vector values

897

//         (recall that the post-condition, in addition to establishing

898

//          constraints on output values, may also specify how output values

899

//          are related to input values)

900

//       - returns a HarnessResult value, which has three alteratives

901

//             RejectedPrecondition - the input test vector does not satisfy

902

//                 the precondition

903

//             FailedPostcondition(TestCaseError),

904

//               - the input test vector satisfies the precondition, but the

905

//                 result of running the entry point DOES NOT satisfy the post condition

906

//             Passed

907

//               - both the pre- and post-condition are satisfied

908

//     In manual GUMBOX tests, one usually asserts that the HarnessResult

909

//       is Passed

910

//

911

//++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++

912

//================================================================

913

914

mod GUMBOX_manual_tests {

915

  use serial_test::serial;

916

917

  use crate::test::util::*;

918

  use data::Isolette_Data_Model::*;

919

920

   //========================================================================

921

  //  REQ-THERM-2: If Current Temperature is less than the Lower Desired Temperature,

922

  //  the Heat Control shall be set to On.

923

  //========================================================================

924

925

/*

926

       Inputs:

927

         current_temp:  95f

928

         lower_desired_temp: 98f

929

         upper_desired_temp: *irrelevant to requirement* (use 100f)

930

*/

931

932

  #[test]

933

  #[serial]

934

2

  fn test_compute_GUMBOX_manual_REQ_THERM_2() {

935

2

    // generate values for the incoming data ports

936

2

    let current_temp = Temp { degrees: 95 };

937

2

    let lower_desired_temp = Temp { degrees: 98 };

938

2

    let upper_desired_temp = Temp { degrees: 100 };

939

2

    let desired_temp = Set_Points {lower: lower_desired_temp, upper: upper_desired_temp};

940

2

941

2

    let harness_result =

942

2

       cb_apis::testComputeCB(current_temp, desired_temp);

943

2

944

2

    // ToDo: Jason: should we use #[derive(PartialEq)] for  HarnessResult

945

2

    // assert!(harness_result == cb_apis::HarnessResult::Passed);

946

2

    assert!(matches!(harness_result, cb_apis::HarnessResult::Passed));

947

948

949

  // There are also "container-based" variants (both without and with GUMBO

950

  // state variables) of the contract-based testing APIs as illustrated below.

951

  #[test]

952

  #[serial]

953

2

  fn test_compute_GUMBOX_manual_REQ_THERM_2_container() { // Alternate version: Illustrate "container"-based APIs

954

2

    // [InvokeEntryPoint]: invoke the entry point test method

955

2

    crate::thermostat_thermostat_initialize();

956

2

957

2

    // Inputs can be "bundled" into a container.

958

2

    let preStateContainer = test_apis::PreStateContainer {

959

2

      api_current_temp : Temp { degrees: 95},

960

2

      api_desired_temp : Set_Points {

961

2

        lower: Temp { degrees:  98 },

962

2

        upper: Temp { degrees: 100 }

963

2

964

2

};

965

2

966

2

    let harness_result =

967

2

       cb_apis::testComputeCB_container(preStateContainer);

968

2

    assert!(matches!(harness_result, cb_apis::HarnessResult::Passed));

969

970

971

  // Developers will occasionally supply a test vector that doesn't satsify

972

  // the pre-condition.  This is represents a failed development process step:

973

  // the developer has not followed the methodology to design

974

  // an appropriate test input OR the pre-condition has not been specified

975

  // appropriately.

976

//

977

  // The test below represents this type of error.

978

979

/*

980

  #[test]

981

  #[serial]

982

  fn test_compute_GUMBOX_manual_REQ_THERM_2_failed_pre() {

983

    // generate values for the incoming data ports

984

    let current_temp = Temp { degrees: 95 };

985

    let lower_desired_temp = Temp { degrees: 102 }; // wrong: lower value shoud be LEQ to upper

986

    let upper_desired_temp = Temp { degrees: 100 };

987

    let desired_temp = Set_Points {lower: lower_desired_temp, upper: upper_desired_temp};

988

989

    let harness_result =

990

       cb_apis::testComputeCB(current_temp, desired_temp);

991

992

    // HarnessResult::RejectedPrecondition is returned to harness_result,

993

    // which causes the assertion below to fail.

994

    assert!(matches!(harness_result, cb_apis::HarnessResult::Passed));

995

996

*/

997

998

 // EXERCISES:

999

 //  - construct a GUMBOX manual test for REQ-THERM-3, making direct use of APIs

1000

 //    without a container

1001

 //  - construct an alternate GUMBOX manual test for REQ-THERM-3,

1002

 //    using a container structure

1003

1004

1005

 //========================================================================

1006

 //  REQ-THERM-4: If the Current Temperature is greater than or equal

1007

 //  to the Lower Desired Temperature and less than or equal to the

1008

 //  Upper Desired Temperature, the value of the Heat Control shall not be changed.":

1009

 //========================================================================

1010

1011

  // Test design notes:

1012

  // The _CB based tests re-initialize the internal state of the component

1013

  // (including the GUMBO state variables) during each call.  Therefore,

1014

  // we cannot use them to implement the testing approach in which we

1015

  // "inherit" the values of GSV from previous invocations.  Instead,

1016

  // we following the approach in which we explicitly force the GSV pre-state

1017

  // variable values to specific values on each test invocation.

1018

//

1019

1020

  // Activation 1-a: Current temp lies within set points (closed interval)

1021

  //   in this case current temp is equal to lower bound,

1022

  //   so heat control should still be on

1023

/*

1024

     Inputs:

1025

      current_tempWstatus  98

1026

      lower_desired_temp: (use 98)

1027

      upper_desired_temp: (use 100)

1028

1029

    ** force previous heat_control lastCmd to ON **

1030

1031

     Expected Outputs:

1032

      heat_control: On

1033

      last_cmd: On

1034

*/

1035

1036

  #[test]

1037

  #[serial]

1038

2

  fn test_compute_GUMBOX_manual_1_a() {

1039

2

    // [InvokeEntryPoint]: invoke the entry point test method

1040

2

    crate::thermostat_thermostat_initialize();

1041

2

1042

2

    // generate values for the incoming data ports

1043

2

    let current_temp = Temp { degrees: 98 };

1044

2

    let lower_desired_temp = Temp { degrees: 98 };

1045

2

    let upper_desired_temp = Temp { degrees: 100 };

1046

2

    let desired_temp = Set_Points {lower: lower_desired_temp, upper: upper_desired_temp};

1047

2

    let last_cmd = On_Off::Onn;

1048

2

1049

2

    let harness_result =

1050

2

       cb_apis::testComputeCBwGSV(last_cmd, current_temp, desired_temp);

1051

2

1052

2

    assert!(matches!(harness_result, cb_apis::HarnessResult::Passed));

1053

1054

1055

  // Exercise

1056

//

1057

  //  Complete the remaining manual GUMBOX tests for REQ-THERM-4

1058

  //  corresponding to original manual tests given previously.

1059

1060

1061

1062

1063

//================================================================

1064

//++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++

1065

//

1066

//  A u t o m a t e d    G U M B O X  (contract-based)  T e s t s

1067

//  (property-based testing)

1068

1069

//  These examples illustrate how to use the GUMBOX APIs auto-generated

1070

//  by HAMR to support automated property-based contract-based unit testing

1071

//  for a HAMR thread component.

1072

//

1073

//  The test APIs are found in src/test/util/cb_apis.rs and are

1074

//  re-generated each time HAMR code generation is run (e.g., after

1075

//  changes are made to model structures or model contracts).

1076

//

1077

//  The auto-generated file includes macros for

1078

//  automated property-based testing - in which HAMR uses the

1079

//  Rust prop test libraries (https://altsysrq.github.io/proptest-book/)

1080

//  to automatically generate random test vectors for testing the component.

1081

//

1082

//  In automated GUMBOX tests, code is written to

1083

//   - configure the control of random value generation and

1084

//     test running.  This includes aspects such as

1085

//     indicating the desired number of tests.

1086

//   - specifying the random value generators to be used for

1087

//     each input value (input port and GUMBO-specified variable).

1088

//     HAMR generates default generators for each data type used

1089

//     in inputs in the `test/util/generators.rs` file.

1090

//

1091

//  The auto-generated artifacts for the framework can be used immediately

1092

//  by developers for automated testing that complements contract-based

1093

//  verification with Verus.

1094

//

1095

//  However, The overall objective in this assurance approarch is to

1096

//  configure the input generation framework in a manner that yields

1097

//  desired coverage of both entry point code and entry point contracts.

1098

//

1099

//  Thus effective use of the framework that goes beyond simple "tire kicking"

1100

//  requires that developers know how to...

1101

//   .. obtain and read coverage information for both code and contracts

1102

//   .. configurate the generation frameworo.

1103

//

1104

//++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++

1105

//================================================================

1106

1107

mod GUMBOX_tests {

1108

  use serial_test::serial;

1109

1110

  // import the proptest libraries used for random value generation

1111

  //  and broader property-based testing concepts

1112

  use proptest::prelude::*;

1113

1114

  // import HAMR-generated utilities for applying property-based testing

1115

  // for testing component entry points with "properties" phrased as GUMBOX contracts.

1116

  use crate::test::util::*;

1117

  use crate::testInitializeCB_macro;

1118

  use crate::testComputeCB_macro;

1119

  use crate::testComputeCBwGSV_macro;

1120

1121

  // number of valid (i.e., non-rejected) test cases that must be executed for the compute method.

1122

  const numValidComputeTestCases: u32 = 100;

1123

1124

  // how many total test cases (valid + rejected) that may be attempted.

1125

  //   0 means all inputs must satisfy the precondition (if present),

1126

  //   5 means at most 5 rejected inputs are allowed per valid test case

1127

  const computeRejectRatio: u32 = 5;

1128

1129

  const verbosity: u32 = 2;

1130

1131

  testInitializeCB_macro! {

1132

    prop_testInitializeCB_macro, // test name

1133

    config: ProptestConfig { // proptest configuration, built by overriding fields from default config

1134

      cases: numValidComputeTestCases,

1135

      max_global_rejects: numValidComputeTestCases * computeRejectRatio,

1136

      verbose: verbosity,

1137

      ..ProptestConfig::default()

1138

1139

1140

1141

  // testComputeCB_macro! {

1142

  //   prop_testComputeCB_macro, // test name

1143

  //   config: ProptestConfig { // proptest configuration, built by overriding fields from default config

1144

  //     cases: numValidComputeTestCases,

1145

  //     max_global_rejects: numValidComputeTestCases * computeRejectRatio,

1146

  //     verbose: verbosity,

1147

  //     ..ProptestConfig::default()

1148

  //   },

1149

  //   // strategies for generating each component input

1150

  //   api_current_temp: generators::Isolette_Data_Model_Temp_strategy_default(),

1151

  //   api_desired_temp: generators::Isolette_Data_Model_Set_Points_strategy_default()

1152

  // }

1153

1154

  // testComputeCBwGSV_macro! {

1155

  //   prop_testComputeCBwGSV_macro, // test name

1156

  //   config: ProptestConfig { // proptest configuration, built by overriding fields from default config

1157

  //     cases: numValidComputeTestCases,

1158

  //     max_global_rejects: numValidComputeTestCases * computeRejectRatio,

1159

  //     verbose: verbosity,

1160

  //     ..ProptestConfig::default()

1161

  //   },

1162

  //   // strategies for generating each component input

1163

  //   In_lastCmd: generators::Isolette_Data_Model_On_Off_strategy_default(),

1164

  //   api_current_temp: generators::Isolette_Data_Model_Temp_strategy_default(),

1165

  //   api_desired_temp: generators::Isolette_Data_Model_Set_Points_strategy_default()

1166

  // }

1167

1168

  testComputeCBwGSV_macro! {

1169

    prop_testComputeCBwGSV_REQ2thru4, // test name

1170

    config: ProptestConfig { // proptest configuration, built by overriding fields from default config

1171

      cases: numValidComputeTestCases,

1172

      max_global_rejects: numValidComputeTestCases * computeRejectRatio,

1173

      verbose: verbosity,

1174

      ..ProptestConfig::default()

1175

},

1176

    // Replace the default strategies with strategies for custom ranges

1177

    In_lastCmd: generators::Isolette_Data_Model_On_Off_strategy_default(),

1178

    api_current_temp: generators::Isolette_Data_Model_Temp_strategy_cust(94..=105),

1179

    api_desired_temp: generators::Isolette_Data_Model_Set_Points_strategy_cust(

1180

      generators::Isolette_Data_Model_Temp_strategy_cust(94..=103),

1181

      generators::Isolette_Data_Model_Temp_strategy_cust(97..=105)

1182

1183

1184