Clarified the inputs for the PID case study. #244
Conversation
theyoucheng
commented
Sep 30, 2016
theyoucheng
commented
- specify input parameters for the PID function more clearly
- non-deterministically assign input values at each loop iteration
|
The test suite seems to only need to feed inputs twice into the controller; why are 6 unwindings needed? What are the inputs used in the remaining 4 iterations? |
|
Added the test suite for unwinding the loop six times. |
| 22: // Vertical speed of the UAV detected by GPS sensor | ||
| 23: float estimator_z_dot; | ||
| 24: | ||
| 25: /** PID funciton OUTPUTS */ |
| 26: float desired_gaz; | ||
| 27: float desired_pitch; | ||
| 28: | ||
| 29: /** Accumulated error in the control */ |
There was a problem hiding this comment.
Please say that this is a state variable
| 64: __CPROVER_assume(estimator_z_dot>=-MAX_CLIMB && estimator_z_dot<=MAX_CLIMB); | ||
| 65: | ||
| 66: climb_pid_run(); | ||
| 67: |
There was a problem hiding this comment.
Add a __CPROVER_output for the output
| Subsequently, the <code>__CPROVER_assume</code> statement in lines 60 and 61 guarantees that | ||
| their values are bounded within a range. | ||
| which repeatedly invokes the function <code>climb_pid_run</code> (line 66). | ||
| In the beginning of each loop iteration, the values of the desired speed <code>desired_climb</code> |
| </p> | ||
|
|
||
| <p class="justified"> | ||
| To demonstrate the automatic test suite generation in CBMC, | ||
| we call the following command | ||
| </p> | ||
|
|
||
| <pre><code>cbmc pid.c --cover mcdc --unwind 25 --trace --xml-ui | ||
| <pre><code>cbmc pid.c --cover mcdc --unwind 6 --trace --xml-ui |
There was a problem hiding this comment.
I am not told why "6" is the right number
| (goal id: climb_pid_run.coverage.2) | ||
| T3: desired_climb=0.000000f, estimator_z_dot=0.000000f | ||
| (goal id: climb_pid_run.coverage.3) | ||
| T1: (desired_climb=-1.000000f, estimator_z_dot=-1.000000f) |
There was a problem hiding this comment.
This test suite does not tell me which numbers to feed in in which iteration
| 62: /** Range of input values */ | ||
| 63: __CPROVER_assume(desired_climb>=-MAX_CLIMB && desired_climb<=MAX_CLIMB); | ||
| 64: __CPROVER_assume(estimator_z_dot>=-MAX_CLIMB && estimator_z_dot<=MAX_CLIMB); | ||
| 65: |
There was a problem hiding this comment.
There should be two __CPROVER_input commands to record these.
|
|
||
| /** Range of initial values of variables */ | ||
| __CPROVER_assume(desired_climb>=-MAX_CLIMB && desired_climb<=MAX_CLIMB); | ||
| __CPROVER_assume(estimator_z_dot>=-MAX_CLIMB && estimator_z_dot<=MAX_CLIMB); | ||
|
|
There was a problem hiding this comment.
climd_sum_err should be initialized explicitly
|
Thanks Daniel. For now the test suites are manually linked to its coverage goals in this manual. I am going to add an extra script for this later. |
Fix issue #244 - add_axioms_for_set_length
LVSA EVS tests
Fixup Makefile for PR#242 "Make exprt::is_zero() support bitfields"
