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

There are two methods to generate test cases. Either by specifying the search criteria on the command line or by providing 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.

-p CLPFD
        flag to enable the CLPFD constraint solver to search the state space
-p TIME_OUT
        time out in milliseconds to abort the exploration of each possible trace

Example: To generate test cases that cover the event increase leading to a state where count = MAX-1 and do not have a depth of more than 5 we would specify this as follows

./probcli.sh simeplecounter.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 in 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>

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>

Example: 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