Generating Traces

Traces are generated in three phases: Query file, Depth search, and Single step. These are executed in order, and each phase tries to add to the coverage achieved by previous phases.

The first phase looks through the currently loaded query file in the verifier for reachability queries. Each reachability query is executed and the resulting trace is used as a test case.

The second phase does a random depth first search of the specified number of steps, the resulting trace is used as a test case. This process is repeated until the newly generated trace does not add new coverage over the previous traces. In order to use this method a global integer variable named __reach__ must be initialized to zero, and must not be used throughout the model.

The third phase tries to cover any remaining edges not covered by the previous phases. This is done by making a reachability query for each uncovered edge. In large systems this can be many edges, and the query for reaching specific edges can take a long time to execute. In order to use this method a global integer variable named __single__ must be initialized to zero, and must not be used throughout the model.