近似值对目标状态的影响

该软件为分析过程中因近似而受到影响的目标提供了测试用例或反例。这些目标被报告为测试生成分析的测试用例目标未定和属性证明分析的目标未定，有反例。

该软件将由于近似值而受到影响的目标确认为死逻辑、有效或不可满足。下表总结了所有分析模式的这些目标。

在以下情况下，软件无法通过验证结果来确认目标状态：

下表总结了前述案例的目标状况。为了确认目标的状态，您必须运行测试用例或反例的额外仿真。

通过验证结果识别近似值的影响

这个例子显示了近似值如何影响Switch模块的目标状态。在sldvApproximationsExample模型中，Constant模块中的计算1./3和2./3在分析时得出浮点数到有理数的转换的结果。

对于输入端口 In2 等于 -1，在仿真中，Switch模块的输入 2 不等于 0。因此，Switch 不会选择输入端口 In3 作为输出。对于测试生成和属性证明分析，由于分析过程中近似的影响，Switch模块的目标logical trigger input false(output is from 3rd input port) 尚未确定。

1.打开模型sldvApproximationsExample:

open_system('sldvApproximationsExample');