Skip to content

adjusted the command line options for the pid controller case study #300

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 1 commit into from
Apr 3, 2017
Merged

adjusted the command line options for the pid controller case study #300

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
16 changes: 10 additions & 6 deletions doc/html-manual/cover.shtml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -149,7 +149,7 @@ To demonstrate the automatic test suite generation in CBMC,
we call the following command and we are going to explain the command line options one by one.
</p>

<pre><code>cbmc pid.c --cover mcdc --unwind 6 --trace --xml-ui
<pre><code>cbmc pid.c --cover mcdc --unwind 6 --xml-ui
</code></pre>

<p class="justified">
Expand All @@ -173,18 +173,22 @@ pprz >= (float)0 && pprz <= (float)(16 * 600) id="climb_pid_run.coverage.3"

<p class="justified">
The "id" of each coverage goal is automatically assigned by CBMC. For every
coverage goal, a trace (if there exists) of the program execution that
satisfies such a goal is printed out in XML format, as the parameters
<code>--trace --xml-ui</code> are given. Multiple coverage goals can share a
trace, when the corresponding execution of the program satisfies all these
goals at the same time. Each trace corresponds to a test case.
coverage goal, a test suite (if there exists) that <!-- the program execution that-->
satisfies such a goal is printed out in XML format, as the parameter
<code>--xml-ui</code> is given. Multiple coverage goals can share a
test suite, when the corresponding execution of the program satisfies all these
goals at the same time. <!--Each trace corresponds to a test case.-->
</p>

<p class="justified">
In the end, the following test suites are automatically generated for testing the PID controller.
A test suite consists of a sequence of input parameters that are
passed to the PID function <code>climb_pid_run</code> at each loop iteration.
For example, Test 1 covers the MC/DC goal with id="climb_pid_run.coverage.1".
The complete output from CBMC is in
<a href="pid_test_suites.xml">pid_test_suites.xml</a>, where every test suite and the coverage goals it is for
are clearly described.

<pre><code>Test suite:
Test 1.
(iteration 1) desired_climb=-1.000000f, estimator_z_dot=1.000000f
Expand Down
Loading