突出显示模型结果

本页采用了机器翻译。点击此处可查看英文原文。

通过模型突出显示进行结果审查

当您使用 Simulink^® Design Verifier™ 分析模型时，已分析的模型对象会自动以以下颜色之一突出显示：

绿色
红色
橙色
灰色的

您可以通过查看 Simulink 编辑器中突出显示的对象一目了然地查看分析结果。

Simulink Design Verifier 结果检查器

当模型突出显示时，您可以点击分析记录结果的对象。然后，Simulink Design Verifier 结果检查器会显示该对象的详细分析结果。

自动突出显示模型上的结果

在分析过程中，当目标状态更新时，Simulink Design Verifier 会自动突出显示模型对象。默认情况下，自动突出显示是启用的。要禁用突出显示，点击“结果摘要”窗口中的“禁用突出显示”。

在 Simulink 编辑器中，模型上会突出显示结果。启用突出显示后，结果检查器将打开并显示分析目标的状态摘要。

注意

Simulink Design Verifier 没有突出显示 Stateflow^® 状态转换表。Simulink Design Verifier 报告、数据文件和日志文件包含状态转换表的分析数据。使用该报告，您可以导航到状态转换表。

模型上以绿色突出显示

以绿色突出显示的对象对于每种分析类型具有以下含义。

分析模式	绿色突出显示
设计错误检测	分析没有发现溢出或除以零的错误。分析未发现死逻辑。分析未发现超出用户指定的最小和最大约束范围的中间信号或输出信号。分析没有发现超出范围的数组访问错误。
测试生成	分析发现了满足测试目标的测试用例。
属性证明	分析发现所有证明目标均有效。

模型上的红色突出显示

根据分析类型，以红色突出显示的对象具有以下含义。

分析模式	红色突出显示
设计错误检测	分析发现至少有一个测试用例会导致溢出或除以零的错误。分析发现，逻辑无效。分析发现中间信号或输出信号超出了用户指定的最小和最大约束范围。分析发现至少有一个测试用例导致超出边界的数组访问错误。
测试生成	该分析未能满足某些测试目标。
属性证明	该分析推翻了证明目标，并生成了证伪该目标的反例。

如果您的模型至少包含一个以红色突出显示的对象，则模型中可能还存在Simulink Design Verifier未以红色突出显示的其他设计错误。如果设计中的对象导致运行时错误，Simulink Design Verifier 可能无法确定导致运行时错误的对象下游的对象的进一步错误或依赖于该对象的结果。解决导致最初红色突出显示的错误并重新运行分析以确定 Simulink Design Verifier 是否将模型中的其他对象突出显示为红色。

模型上的橙色高亮显示

根据分析类型，以橙色突出显示的对象具有以下含义。

分析模式	橙色突出显示
设计错误检测	对于突出显示的模型对象，该分析未确定至少一个设计错误检测目标。这种情况可能发生在以下情况：分析仍在进行中。分析超时。由于除以零或非线性算术，分析无法决定设计错误检测目标。由于存在桩件，软件无法决定设计错误检测目标。有关更多信息，请参阅使用自动桩件处理不兼容性。由于分析引擎的限制，软件无法决定设计错误检测目标。例如，如果分析遇到无界的 while 循环，它会执行近似值。有关更多信息，请参阅近似值在模型分析中的作用。分析发现了近似值可能影响的死逻辑。有关更多信息，请参阅 Simulink Design Verifier 如何通过验证结果报告近似值。分析发现了近似值可以影响的有效目标。有关更多信息，请参阅 Simulink Design Verifier 如何通过验证结果报告近似值。
测试生成	对于突出显示的模型对象，该分析未能确定至少一个测试目标。这种情况可能发生在以下情况：分析仍在进行中。分析超时。由于除以零或非线性算术，分析无法确定测试目标。由于桩件的存在，软件无法决定测试目标。有关更多信息，请参阅使用自动桩件处理不兼容性。由于分析引擎的限制，软件无法确定测试目标。例如，如果分析遇到无界的 while 循环，它会执行近似值。有关更多信息，请参阅近似值在模型分析中的作用。分析发现近似值可能会影响无法满足的目标。有关更多信息，请参阅 Simulink Design Verifier 如何通过验证结果报告近似值。该分析无法通过验证结果来确认是否满足要求。有关更多信息，请参阅目标满足 - 需求仿真。
属性证明	对于突出显示的模型对象，分析没有确定至少一个证明目标。这种情况可能发生在以下情况：分析仍在进行中。分析超时。证明目标存在于软件无法控制其值的信号上，例如 Constant模块。由于除以零或非线性算术，分析无法确定证明目标。由于存在桩件，软件无法确定证明目标。有关更多信息，请参阅使用自动桩件处理不兼容性。由于分析引擎的限制，软件无法确定证明目标。例如，如果分析遇到无界的 while 循环，它会执行近似值。有关更多信息，请参阅近似值在模型分析中的作用。分析发现了近似值可以影响的有效目标。有关更多信息，请参阅 Simulink Design Verifier 如何通过验证结果报告近似值。该软件无法通过验证结果来确认伪造状态。有关更多信息，请参阅目标被证伪——需要仿真。

分析模式

橙色突出显示

设计错误检测

对于突出显示的模型对象，

该分析未确定至少一个设计错误检测目标。这种情况可能发生在以下情况：
- 分析仍在进行中。
- 分析超时。
- 由于除以零或非线性算术，分析无法决定设计错误检测目标。
- 由于存在桩件，软件无法决定设计错误检测目标。有关更多信息，请参阅使用自动桩件处理不兼容性。
- 由于分析引擎的限制，软件无法决定设计错误检测目标。例如，如果分析遇到无界的 while 循环，它会执行近似值。有关更多信息，请参阅近似值在模型分析中的作用。

分析发现了近似值可能影响的死逻辑。有关更多信息，请参阅 Simulink Design Verifier 如何通过验证结果报告近似值。
分析发现了近似值可以影响的有效目标。有关更多信息，请参阅 Simulink Design Verifier 如何通过验证结果报告近似值。

测试生成

对于突出显示的模型对象，

该分析未能确定至少一个测试目标。这种情况可能发生在以下情况：
- 分析仍在进行中。
- 分析超时。
- 由于除以零或非线性算术，分析无法确定测试目标。
- 由于桩件的存在，软件无法决定测试目标。有关更多信息，请参阅使用自动桩件处理不兼容性。
- 由于分析引擎的限制，软件无法确定测试目标。例如，如果分析遇到无界的 while 循环，它会执行近似值。有关更多信息，请参阅近似值在模型分析中的作用。

分析发现近似值可能会影响无法满足的目标。有关更多信息，请参阅 Simulink Design Verifier 如何通过验证结果报告近似值。
该分析无法通过验证结果来确认是否满足要求。有关更多信息，请参阅目标满足 - 需求仿真。

属性证明

对于突出显示的模型对象，

分析没有确定至少一个证明目标。这种情况可能发生在以下情况：
- 分析仍在进行中。
- 分析超时。
- 证明目标存在于软件无法控制其值的信号上，例如 Constant模块。
- 由于除以零或非线性算术，分析无法确定证明目标。
- 由于存在桩件，软件无法确定证明目标。有关更多信息，请参阅使用自动桩件处理不兼容性。
- 由于分析引擎的限制，软件无法确定证明目标。例如，如果分析遇到无界的 while 循环，它会执行近似值。有关更多信息，请参阅近似值在模型分析中的作用。

分析发现了近似值可以影响的有效目标。有关更多信息，请参阅 Simulink Design Verifier 如何通过验证结果报告近似值。
该软件无法通过验证结果来确认伪造状态。有关更多信息，请参阅目标被证伪——需要仿真。

模型上的灰色突出显示

以灰色突出显示的对象具有以下含义。

分析模式	灰色突出显示
设计错误检测测试生成属性证明	模型对象不是分析的一部分。