Analyze and Resolve Undecided Objective Statuses
When you analyze a model using Simulink® Design Verifier™, the tool creates objectives, which are specific conditions or checkpoints within your model. The analysis then attempts to determine if these objectives can be satisfied, violated, or proven. If Simulink Design Verifier analysis cannot conclusively determine outcomes for the objectives, it produces incomplete results. In the results summary, these incomplete results show that the objectives are undecided objectives, which often arise from model complexity, unsupported features, or analysis limitations.
Common Causes of Incomplete Result
Simulink Design Verifier analysis on a model may result in undecided objectives due to these factors.
Model Complexity
Some characteristics of Simulink models can increase the complexity of analysis, including input complexity, computational complexity, and state-space complexity.
Input complexity includes:
Large number of inputs, which can vary depending on the individual model complexity
Input datatypes that take a large number of possible values, such as floating-point and wide integer types
Complex arithmetic or algorithms.
Computational complexity can arise from nonlinear operations such as trigonometric functions, exponentials, or divisions that further increase the complexity of the analysis. Simulink Design Verifier may abstract or ignore certain behaviors, which can lead to incomplete results.
State space complexity comes from the number and type of model states that Simulink Design Verifier needs to analyze. As the number of states increases due to computations, data types, or logic branches, the number of possible execution paths grows. Simulink Design Verifier needs to explore more states, which can lead to longer analysis times. In large models, Simulink Design Verifier might not be able to exhaustively analyze all possible behaviors, potentially resulting in incomplete results. For more information, see Perform Analysis on Large and Complex Models.
Timers and Delays
Simulink Design Verifier analysis finds input values for the state space that leads to satisfying an objective. Each counter value or timer step corresponds to a different state, so the presence of long timers or counters can significantly increase the size of the state representation.
Models that contain time delays complicate the analysis by forcing the search for inputs to span a large number of states. You may see similar effects when systems use extensive averaging and filtering to delay the response to a change in inputs. Any aspect of the design that delays the response causes the test sequences to contain more timer steps, resulting in longer test cases that are more difficult to identify and incomplete results. For more information, see Analyze Models with Counters and Timers.
Analysis Limitations
Some Simulink blocks or custom S-functions may not be supported and abstracted out by Simulink Design Verifier, leading to incomplete results. For more information, see Unsupported Simulink Blocks in Analysis and Limitations of Simulink Design Verifier for Simulink Software Features.
Undecided Objectives Due to Incomplete Analysis
Objectives may show an undecided status if the analysis is either incomplete due to reaching the maximum allowed time or you aborted the analysis.
Undecided
This status can occur if either the Simulink Design Verifier analysis exceeded its analysis time limit specified using Maximum analysis time parameter or you aborted the analysis before it completed processing these objectives. To troubleshoot this objective status, see Resolve Undecided Objectives When Analysis Is Interrupted or Times Out.
Undecided Objectives Due to Model Complexities
If your model is complex, these objective statuses that indicate incomplete results can occur.
Undecided Due to Stubbing
This objective status results from the stubbing of unsupported blocks introduced in the upstream logic of your model. The stubbing could be introduced as a part of computing model representation or as a substep of Simulink Design Verifier analysis. For more information, see Handle Model Complexities with Automatic Stubbing.
Undecided Due to Nonlinearities
This status occurs when Simulink Design Verifier cannot determine the result because the model contains nonlinear arithmetic that the analysis cannot handle precisely.
To resolve these objective statuses, see Resolve Undecided Objective Statuses Resulting from Model Complexity.
Undecided Objectives Due to Possible Modeling Errors
If your model contains run-time errors, you might receive these undecided objective statuses.
Undecided Due to Runtime Error
For proof objectives and test objectives, this status occurs when Simulink Design Verifier finds a test case or counterexample that causes a run-time error during simulation.
Undecided Due to Division by Zero
This objective results from division-by-zero errors in the associated model items. In Simulink Design Verifier, the test case hits a division by zero during simulation which would cause a run-time error.
Undecided Due to Array Out of Bounds
This status occurs when the test case causes an out-of-bounds array access. For more information, see Detect Out of Bound Array Access Errors.
To resolve these objectives, see Resolve Undecided Objective Statuses Caused by Possible Modeling Errors.
Undecided Objectives Due to Approximations During Analysis
Simulink Design Verifier performs approximations during analysis, identifies the presence of approximations, and reports them as objective status. For more information on role of approximations, see Approximations During Model Analysis.
Undecided with Testcase
Simulink Design Verifier generates a test case for an objective that cannot be satisfied because of approximation effects. The analysis returns the Undecided with Testcase status to help you investigate ways to satisfy the objective.
Undecided with Counterexamples
A counterexample is a specific input scenario or sequence that demonstrates violation of an objective. Simulink Design Verifier analysis provides counterexamples when it finds that an objective does not hold. The design error detection and property proving analysis returns the Objectives Undecided with Counterexamples status due to the impact of approximation during analysis.
Undecided Possibly Due to Long Counterexample
Some design errors, such as integer overflows, may be detected only when the model is run with very long test cases. Such a test case may not be feasible to construct or to simulate. If Simulink Design Verifier analysis 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.
To resolve these objective status, see Resolve Undecided Objective Status Due to Analysis Approximations.
Troubleshoot Undecided Objective Statuses
Understanding why these objective statuses occur and how to address them is necessary for a complete analysis results when you generate tests, detect design errors, or prove properties. The approach to resolve undecided objectives can vary based on the goal:
| Goal | Impact of undecided objectives |
|---|---|
| Maximize test coverage | Missed coverage, incomplete testing |
| Model correctness | Potentially missed errors |
| Prove critical properties hold | Unproven safety, regulatory issues |
| Debug and improve model | Unclear model behavior |
Use these troubleshooting techniques if your analysis is incomplete and the results show undecided objectives:
Note
Simulink Design Verifier analysis shows these same objective status for test case generation, design error detection, and property proving analyses.
Undecided
Undecided due to Stubbing
Undecided due to Nonlinearities
Undecided Due to Division-by-Zero
Undecided Due to Array of bounds
For instance, statuses such as Undecided with Testcase or Undecided Due to Runtime Error commonly occur in both analysis modes.
See Also
Review Results from Analysis Report | Handle Model Complexities with Automatic Stubbing | Perform Analysis on Large and Complex Models
