Skip to content

Commit cf085a8

Browse files
committed
Added the test suite for unwinding the loop 6 times in PID case study.
1 parent 3267568 commit cf085a8

File tree

1 file changed

+8
-0
lines changed

1 file changed

+8
-0
lines changed

doc/html-manual/cover.shtml

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -192,6 +192,14 @@ the loop must be unwound sufficient enough times.
192192
For example, the PID function <code>climb_pid_run</code> needs to be called at
193193
least six times for evaluating the condition
194194
<code>climb_sum_err>MAX_CLIMB_SUM_ERR</code> in line 48 to <em>true</em>.
195+
This corresponds to the test suite below.
196+
<pre><code>(desired_climb=-1.000000f, estimator_z_dot=1.000000f);
197+
(desired_climb=-1.000000f, estimator_z_dot=0.000000f);
198+
(desired_climb=-1.000000f, estimator_z_dot=1.000000f);
199+
(desired_climb=-1.000000f, estimator_z_dot=1.000000f);
200+
(desired_climb=-1.000000f, estimator_z_dot=1.000000f);
201+
(desired_climb=-1.000000f, estimator_z_dot=1.000000f).
202+
</code></pre>
195203
An introduction to the use of loop unwinding can be found
196204
in <a href="cbmc-loops.shtml">Understanding Loop Unwinding</a>.
197205
</p>

0 commit comments

Comments
 (0)