近似值在模型分析中的作用

Simulink^® Design Verifier™ 软件生成输入和参数以实现目标。然而，软件可以搜索的值的数量是无限的。为了在分析中创建合理的限制，软件会执行近似值以简化分析。该软件将其执行的所有近似值记录在 Simulink Design Verifier HTML 报告的分析信息章节中。有关本章的描述，请参阅分析信息章节。

当软件使用近似值时，请仔细检查分析结果。评估您的模型以确定哪些模块或子系统导致软件执行近似操作。

在极少数情况下，近似值可能导致测试用例无法达到测试目标或表现出设计错误，或者反例无法证伪证明目标。例如，假设软件生成一个测试用例信号，该信号应该通过超过阈值来实现目标，那么浮点舍入误差可能会阻止该信号达到阈值。有关更多信息，请参阅 Simulink Design Verifier 如何通过验证结果报告近似值。

近似类型

Simulink Design Verifier 软件在分析模型时执行以下近似计算：

浮点数到有理数的转换

在某些情况下，Simulink Design Verifier 软件通过使用无限精度有理数来近似浮点数，从而简化浮点数的线性运算。该软件发现这些值之间的逻辑关系如何影响目标。该分析使软件能够支持嵌入式控制器设计中常见的监控逻辑。有关示例，请参阅通过验证结果识别近似值的影响。

如果您的模型在信号、输入值或模块参数中包含浮点值，Simulink Design Verifier 会在执行分析之前将某些值转换为有理数。这些近似值的结果是：

不考虑舍入误差。
不考虑浮点数的上限和下限。
如果您的模型将浮点值转换为整数值，则整数表示会影响为该模型生成的测试。在极少数情况下，生成的测试可能无法满足与浮点值相关的目标。

注意

您可以使用配置参数窗口中的运行附加分析以减少有理逼近值的实例选项来减少近似实例。有关更多信息，请参阅运行附加分析以减少有理近似的情况。

浮点数据类型的二维查找表的线性化

Simulink Design Verifier 软件不支持浮点数据类型的非线性运算。如果您的模型包含任何 2-D Lookup Table 模块，或 n-D Lookup Table 模块（其中 n = 2），且具有以下所有特征，则该软件通过将平面拟合到每个插值区间，用线性插值近似非线性二维插值。

模块	特征
n-D Lookup Table模块, n = 2：	插值方法参数是 Linear 。插值方法参数是 Clip 或 Linear 。输入和输出信号都具有浮点数据类型。

整数和定点数据类型的一维和二维查找表的近似值

如果您的模型包含具有以下特征的查找表，Simulink Design Verifier 会自动将您原始的查找表转换为由在各自维度上均匀分布的断点组成的新查找表。

模块	特征
n-D Lookup Table模块, n = 1 或 n = 2:	插值方法参数是 Linear 。插值方法参数是 Clip 。索引搜索方法参数是线性搜索或二分搜索。输入和输出信号均为同一类型，均为整数类型或者定点类型。

这种近似值使得 Simulink Design Verifier 能够更快地生成测试。当您的模型中存在无法满足的测试目标时，节省的时间就非常明显。

如果 Simulink Design Verifier 将此类近似值应用于您的模型，则 Simulink Design Verifier 报告将包含近似值的详细信息。

While 循环

如果您的模型或模型中的 Stateflow^® 图表包含 while 循环，Simulink Design Verifier 会尝试检测允许 while 循环退出的保守常数边界。如果软件找不到常数边界，它会执行while循环近似。通过这种近似，分析不能证明目标是否有效或不可满足，也不能证明死逻辑。生成的分析报告记录了这种近似值。

while 循环近似的行为在所有分析模式下都是一致的，如下表所述。

分析模式	While 循环近似
设计错误检测	将 `while` 循环迭代次数设置为 3。不报告死逻辑或有效目标。
测试用例生成	将 `while` 循环迭代次数设置为 3。不报告无法满足的目标。
属性证明	将 `while` 循环迭代次数设置为 3。未报告有效目标。

另请参阅

Simulink Design Verifier 如何通过验证结果报告近似值 | 查看分析结果