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
 count: 1..MAX
  Increase(y) = PRE y: 1..(MAX-count) THEN
     count := count+y
  Reset = BEGIN count := 1 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 four relevant settings to configure the test case generation

-cb_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

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

        flag to enable the CLPFD constraint solver to search the state space, which is highly recommended.
        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.

Test Generation Description

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

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

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

  <target>count = MAX - 1</target>
    <!-- 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"/>

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