近似值在模型分析中的作用
Simulink® Design Verifier™ 软件生成输入和参数以实现目标。然而，软件需要搜索的值可能非常多。为了在分析中创建合理的限制，软件会执行近似值以简化分析。该软件将其执行的所有近似值记录在 Simulink Design Verifier HTML 报告的分析信息章节中。有关本章的描述，请参阅分析信息章节。
当软件使用近似值时，请仔细检查分析结果。评估您的模型以确定哪些模块或子系统导致软件执行近似操作。
在极少数情况下，近似值可能导致测试用例无法达到测试目标或表现出设计错误，或者反例无法证伪证明目标。例如，当软件生成一个应该通过超过阈值来实现目标的测试用例信号时，浮点舍入误差可能会阻止该信号达到阈值。有关详细信息，请参阅 Simulink Design Verifier 如何通过验证结果报告近似值。
近似类型
Simulink Design Verifier 软件在分析模型时执行以下近似计算：
浮点数到有理数的转换
在某些情况下，Simulink Design Verifier 软件通过使用无限精度有理数来近似浮点数，从而简化浮点数的线性运算。该软件发现这些值之间的逻辑关系如何影响目标。该分析使软件能够支持嵌入式控制器设计中常见的监控逻辑。有关示例，请参阅通过验证结果识别近似值的影响。
如果您的模型在信号、输入值或模块参数中包含浮点值，Simulink Design Verifier 会在执行分析之前将某些值转换为有理数。这些近似值的结果是：
不考虑舍入误差。
不考虑浮点数的上限和下限。
如果您的模型将浮点值转换为整数值，则整数表示会影响为该模型生成的测试。在极少数情况下，生成的测试可能无法满足与浮点值相关的目标。
注意
您可以使用配置参数窗口中的运行附加分析以减少有理逼近值的实例选项来减少近似实例。有关详细信息，请参阅 运行附加分析以减少有理逼近的实例。
浮点数据类型的二维查找表的线性化
当您的模型包含 2-D Lookup Table 块或 n-D Lookup Table 块（其中 n = 2）时，该软件通过将平面拟合到每个插值区间，用线性插值近似非线性二维插值，具有以下特征：
插值方法参数是线性。
插值方法参数是裁剪或线性。
输入和输出信号都具有浮点数据类型。
整数和定点数据类型的一维和二维查找表的近似值
如果您的模型包含具有以下特征的查找表，Simulink Design Verifier 会自动将原始查找表转换为由在各个相应维度上均匀分布的断点组成的新查找表，并具有以下特征：
插值方法参数是线性。
插值方法参数是 Clip。
索引搜索方法参数是线性搜索或二分搜索。
输入和输出信号均为同一类型，均为整数类型或者定点类型。
这种近似值使得 Simulink Design Verifier 能够更快地生成测试。当您的模型中存在无法满足的测试目标时，节省的时间就非常明显。
while 循环近似处理
如果模型中包含一个 while-loop，对于模型中的每个 while-loop，Simulink Design Verifier 会尝试检测执行分析所需的 while-loop 迭代次数的保守常数上界。如果软件无法找到常数边界，它有时会执行一个 while-循环近似。当软件使用 while-loop 近似值来证明目标有效或不可满足时，它会将目标报告为在近似值下有效或在近似值下不可满足。
Model 模块
如果您的模型包含引用外部模型的 Model 模块，则会针对顶级模型创建测试，并考虑其执行上下文中的每个引用模型。
如果多个 Model 模块引用同一个模型，则生成的测试将尝试满足顶级模型中各个上下文中引用模型的每个实例的测试目标。如果您有三个引用某个模型的 Model 模块，则分析会针对所有三个实例产生结果。
如果使用生成的测试用例收集覆盖率，累计覆盖率将反映同一引用模型的多个实例。仿真会为每个引用模型生成一组覆盖率结果；如果您有三个引用某个模型的 Model 模块，则仿真会为该引用模型生成一组结果。
例如，考虑一个顶层模型，其中三个 Model 模块引用同一个模型。参考模型有三个测试目标。分析顶层模型产生了九个测试目标。如果使用九个测试用例仿真模型，则该引用模型的覆盖率结果指定三个测试目标。
