Review and Address Long Counterexample Objective Status

This model in this example counts the number of times a boolean input is true in a variable of the type uint32. An integer overflow is possible, but only after the number of steps is larger than the maximum unit32 value.

Open the Model

Open the model counterexample:

open_system('counter');

Perform Design Error Detection Analysis

1. The model is preconfigured with the Integer overflow option enabled. On the Design Verifier tab, click Detect Design Errors.

2. The software analyzes the model for integer overflow errors. After the analysis completes, the Results Summary window for the add blocks displays the status of the block as Undecided Possibly due to Long Counterexample.

Along with the status, the minimum length of the counterexample is reported as 4294967295 simulation steps.

Review Analysis Results

In the report, you can see a new section Objectives Undecided Possibly Due to Long Counterexample. This section lists all objectives that may have infeasibly long counterexamples and gives the minimum length of a counterexample as the number of simulation steps. 

Click Justify in the Results Summary window. Simulink® Design Verifier™ attempts to justify a counterexample by proving that a counterexample is not actually possible in the real system, typically because of additional constraints or environment assumptions that were not modeled during the initial analysis.