Using Queries

This tutorial assumes you have understood using variables.

The system model

This tutorial uses the same Up/Down model as in the section using variables. Open the updown/updown.xml file in Uppaal.

Editing the Queries

Sometimes it is desirable to generate test cases for specific purposes. This can be done by creating a verification query for the purpose, and use that to generate a test trace.

In the Verifier tab you can enter queries. The Test Cases generator is able to search for traces satisfying reachability queries (that is queries which start with E<>. The query entered in this tutorial should be E<> System.Max, which asks the verifier to find a trace where the System process is in the location Max.

Generating test traces from queries

To generate test cases go to the Test Cases tab and activate the Query mode, and hit Add.

This will generate a trace from the query file that leads to the Max location. You can inspect in the trace statistics that that location is infact now covered. By default, a test trace will be generated per query for all queries in the query file. In the drop-down selector you can chosse a specific query to generate and add.

Further, you can double click the trace and go to the Simulator tab and verify that this trace does indeed lead to the Max location. From the Off location this requires doing up ten successive times.

Generating tests using the combined methodology

As recommended, start by adding test cases for the test purposes (queries), then optimize coverage by the auto-depth mode, and finally single-step mode. This results in the three sections listed the test traces output panel.