的“结果摘要”窗口中ex_property_proving_example_basic分析,点击突出模型的分析结果．

的客观的证据块用红色突出显示，这表明证明目标被反例证伪了。

的仿真软件设计验证器结果窗口。

当您单击模型中的对象时，此窗口将更改为显示该对象的详细分析结果。

点击高亮显示的客观的证据块。

的仿真软件设计验证器结果窗口表明，从比较到零的输出信号不是1的证明目标被反例推翻。

在仿真软件设计验证器“结果汇总”窗口，单击生成详细分析报告．

HTML报告在浏览器窗口中打开。

该报告包括以下内容表的内容．单击超链接导航到报告中的特定部分。

在表的内容,点击总结．

摘要提供了分析结果的概述，它指出仿真软件设计验证器确定了一个反例，它伪造了模型中的一个目标。

在表的内容,点击证明目标状态．

反例证伪目标表列出了证明目标仿真软件设计验证器用它产生的反例予以反驳。您可以通过单击在您的模型窗口中定位目标客观的证据；软件突出显示模型窗口中相应的Proof Objective块。

在反例证伪目标表中，在反例列,单击1．

本节展示关于证明目标1的信息，并提供反例的详细信息仿真软件设计验证器是为了推翻这个目标。在这个反例中，99的信号值对使用Proof objective块指定的目标进行伪证。也就是说，99不小于或等于0，这将导致Compare to Zero块返回0 (false)而不是1 (true)。

在仿真软件设计验证器日志窗口中,单击创建利用模型．

该软件创建了一个名为ex_property_proving_example_basic_harness．

harness模型包含以下项目:

双击input块。

输入信号1导致Compare to Zero块的输出为0。这个反例违反了指定Compare to Zero块的输出为1的证明目标。

打开ex_property_proving_example_basic模型。

在模拟选项卡上,单击库浏览器．

从sink库中，复制一个范围块进入您的线束模型窗口。Scope块允许您查看模型中Compare to Zero块输出的信号值。

在您的线束模型窗口中，将Test Unit子系统的输出信号连接到Scope块。

要模拟您的脊甲模型，请在模拟选项卡上,单击运行．

Simulink软件对线束模型进行了仿真。

在您的线束模型窗口中，双击Scope块以打开它的显示窗口。

Scope块显示模型中Compare To Zero块输出的信号值。在本例中，Compare To Zero块在整个模拟过程中返回0 (false)，从而证明了Compare To Zero块的输出为1 (true)的证明目标是错误的。反例是信号生成器块供应伪造证明目标。

点击突出模型的分析结果．

证明目标现在用绿色突出显示。

单击客观的证据块。

的仿真软件设计验证器结果窗口显示证明目标的状态，信号为1是有效的。

点击生成详细分析报告．

在表的内容,点击总结．

摘要一章说明了这一点仿真软件设计验证器证明了模型中的一个证明目标。

Constraints部分列出了您在Proof Assumption块中指定的分析约束。

滚动回浏览器窗口的顶部。在表的内容,点击证明目标状态．

已证明有效的目标表列出了证明目标仿真软件设计验证器被证明是有效的。

向下滚动以查看“属性”一章，或转到浏览器窗口的顶部和表的内容,点击属性．

证明目标总结表明仿真软件设计验证器证明你在模型中指定的目标。的证明假设Block将输入信号的域限制在区间[- 1,0]。因此，软件证明该区间不包含大于零的值，从而满足证明目标。