Resolve Undecided Objective Status Due to Analysis Approximations

Issue

For some undecided objectives, the analysis is unable to determine an outcome due to approximations involved.

  • Undecided with Testcases and Undecided with Counterexamples — These objective statuses both indicate that approximations have prevented the analysis from reaching a conclusive result. Simulink® Design Verifier™ uses mathematical approximations to simplify the analysis of complex models. These approximations may include abstracting certain model behaviors, ignoring specific numerical effects, or limiting the exploration of state spaces.

    The Undecided with Testcases objective status occurs during test generation analysis when the use of approximations prevents Simulink Design Verifier from conclusively determining whether a suitable test case exists for a particular objective. As a result, Simulink Design Verifier analysis may generate some test cases, but cannot guarantee that these test cases fully satisfy the objective.

    The Undecided with Counterexamples objective status occurs during design error detection or property proving analysis. Here, approximations may hinder the tool from conclusively proving or disproving a property, or from identifying a definitive counterexample.

  • Undecided Possibly Due to Long Counterexamples — Some design errors, such as overflows, may occur only after a very long sequence of operations or very long test cases. Such a test case may not be feasible to construct or to simulate. If Simulink Design Verifier detects that the counterexample for a design error check is infeasibly long, it returns the status Undecided Possibly Due to Long Counterexample and gives the minimum length of that counterexample without returning such a counterexample.

Possible Solutions

Depending on the type of model and analysis, try one of these solutions.

View Diagnostic Viewer and Analysis Report

Manually investigate the objective. Check the Simulink Design Verifier log file or report, or the Diagnostic Viewer for hints on specific blocks or functions that exceeded time limits or solver capabilities.

Inspect the Test Case

The test case may not achieve the objective due to model approximations. However, you can review the test case to determine if modifications could enable it to satisfy the objective, as it is likely close to meeting the required conditions.

Justify the Counterexample

In the Results Summary window, click Justify. Simulink Design Verifier then attempts to justify the counterexample for the analysis. For an example, see Review and Address Long Counterexample Objective Status on how to justify the counterexample in case when the objective status is Undecided Possibly Due to Long Counterexample after the analysis.

Ensure Analysis to Reduce Rational Approximation

If you select the Run additional analysis to reduce instances of rational approximations model configuration parameter, the analysis continues until the maximum timeout or the objective status is Unsatisfiable or Satisfied. You can find this option in the Advanced parameters section of the Design Verifier pane in the Configuration Parameters dialog box. For more information, see Understanding Result Approximations.

See Also

Topics