Test Case Generation

Constraint based test case generation allows to explore the state space for a machine and generate traces of operations that cover certain user defined operations and meet a given condition to end the search.

We will use the following B Machine as an example, which is stored in a file called simplecounter.mch.

MACHINE SimpleCounter
DEFINITIONS MAX==4
VARIABLES count
INVARIANT
 count: 1..MAX
INITIALISATION count := 1
OPERATIONS
  Increase(y) = PRE y: 1..(MAX-count) THEN
     count := count+y
  END;
  Reset = BEGIN count := 1 END
END

How To run

To start the test case generation there are two alternatives. We can either provide all settings as command line arguments or in a test description file.

From the command line

From the command line there are six relevant settings to configure the test case generation

-cbc_tests Depth EndPredicate File
        generate test cases by constraint solving with maximum
        length Depth, the last state satisfies EndPredicate
        and the test cases are written to File

-cbc_cover Operation
        when generating CBC test cases, Operation should be covered. Each
        operation to be covered needs to be specified separately.

-cbc_cover_match PartialOpName
        just like -cbc_cover but for all operations whose name contains "PartialOpName"

-cbc_cover_final
        specifies that the events specified above should only be used as final events in test-cases.
        This option can lead to a considerable reduction in running time of the algorithm.

-p CLPFD TRUE
        flag to enable the CLPFD constraint solver to search the state space, which is highly recommended.
-p TIME_OUT x
        time out in milliseconds to abort the exploration of each possible trace

Example: To generate test cases that cover the event Increase in the machine above, leading to a state where count = MAX-1 is true and the explored paths do not have a depth of more than 5 operations we would specify this as follows, where we use CLPFD and have a timeout of 2000 ms. for each explored trace:

./probcli.sh simplecounter.mch -cb_tests 5 count=MAX-1 test_results.xml -cb_cover Increase -p CLPFD true -p TIME_OUT 2000

The generated test cases are stored in a file called test_results.xml. You can provide the empty filename

''

; in this case no file is generated.

Test Generation Description

The configuration for the test case generation can also be provided as an XML file. The format is shown below:

<test-generation-description>
  <output-file>OUTPUT FILE NAME</output-file>
  <event-coverage>
    <event>EVENT 1</event>
    <event>EVENT 2</event>
  </event-coverage>
  <target>TARGET PREDICATE</target>
  <!-- the parameters section contains parameters that are very ProB-specific -->
  <parameters>
    <!-- the maximum depth is the maximum length of a trace of operations/event,
         the algorithm might stop earlier when all events are covered -->
    <maximum-depth>N</maximum-depth>
    <!-- any ProB preference can be set that is listed when calling "probcli -help -v" -->
    <!-- other probably interesting preferences are MININT, MAXINT and TIME_OUT -->
  </parameters>
</test-generation-description>

Example: For our example the description file would look as follows.

<test-generation-description>
  <output-file>test_results.xml</output-file>
  <event-coverage>
    <event>Increase</event>
  </event-coverage>
  <target>count = MAX - 1</target>
  <parameters>
    <maximum-depth>5</maximum-depth>
    <!-- Please note: TIME_OUT (in milliseconds) is not a global time out, it is per trace -->
    <preference name="CLPFD" value="true"/>
    <!-- Please note: TIME_OUT (in milliseconds) is not a global time out, it is per trace -->
    <preference name="TIME_OUT" value="2000"/>
  </parameters>
</test-generation-description>

Assuming the test description above is stored in file named simple_counter_test_description.xml, we start the test case generation with the following call.

./probcli.sh simplecounter.mch -test_description simple_counter_test_description.xml