Proof Assumption
在证明模型属性时约束信号值
库:
Simulink Design Verifier /
Objectives and Constraints
描述
在属性证明模式下运行时，Simulink® Design Verifier™ 软件会证明您的模型的属性满足指定的准则（请参阅 使用 Simulink Design Verifier 证明模型属性）。在这种模式下，您可以使用 Proof Assumption 模块来定义模型中信号的假设。值参数允许您在属性证明期间指定对信号值的约束。该模块将指定的值参数应用于其输入信号，并且 Simulink Design Verifier 软件证明或反驳您的模型的属性是否满足指定的准则。
该模块的参数对话框还允许您：
启用或禁用假设。
指定该模块应在 Simulink 编辑器中显示其值参数。
指定该模块应显示其输出端口。
注意
Simulink 和 Simulink Coder™ 软件分别在模型仿真和代码生成期间忽略 Proof Assumption 模块。Simulink Design Verifier 软件仅在证明模型属性时使用 Proof Assumption 模块。
您可以使用值参数来约束属性证明中的信号值。有关详细信息，请参阅 使用参数配置文件设置参数。
示例
使用 Assumption 模块进行属性证明
此示例说明如何使用 Proof Assumption 模块执行 Simulink® Design Verifier™ 属性证明。它尝试证明，在当前输入值与之前的六个输入值之和大于 6 时，输出等于 2。该模型包含一个 Proof Assumption 模块，该模块将输入限制为 0 或 1。Simulink Design Verifier 搜索 20 个或更少的时间步内是否存在违规。由于该属性在假设下有效，因此无法找到违规。
端口
输入
输出
参数
指定该模块是否启用。如果选中（默认），Simulink Design Verifier 软件在证明模型的属性时使用该模块。清除此选项将禁用该模块，也就是说，导致 Simulink Design Verifier 软件的行为就像 Proof Assumption 模块不存在一样。如果未选择此选项，则该模块将在 Simulink 编辑器中显示为灰色。
指定该模块是否表现为 Proof Assumption 或 Test Condition 模块。选择测试条件将 Proof Assumption 模块转换为 Test Condition 模块。
使用值参数来约束测试用例中的信号值。以 MATLAB® 元胞数组的形式指定标量和区间的任意组合。有关详细信息，请参阅 使用参数配置文件设置参数。
指定模块是否在 Simulink 编辑器中显示其值参数的内容。
如果选中，该模块将显示其输出端口，这允许输入信号传递到模块输出。如果未选择，该模块将隐藏其输出端口并终止输入信号。
示例: 下图说明了每种情况下模块的外观。
直通样式（显示输出端口）：已选择
直通样式（显示输出端口）：取消选定
版本历史记录
在 R2007a 中推出
