Merge pull request #300 from theyoucheng/case-study

adjusted the command line options for the pid controller case study

Author: Daniel Kroening

doc/html-manual/cover.shtml

@@ -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">
@@ -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