sldv.assume

用于 Stateflow 图和 MATLAB Function 模块的证明假设函数

语法

sldv.assume(expr)

sldv.assume(expr) 指定在证明属性时，expr 在每次计算时都为 true。可以对 expr 使用任何有效的布尔表达式。

此函数没有输出，也不会对其父函数产生任何影响，但会对计算 expr 产生间接副作用。如果从 MATLAB^® 命令行发出该函数，则该函数无效。

可以在 MATLAB 代码中穿插使用 sldv.assume 证明假设，也可以将假设单独放在验证脚本中。

属性证明窗格中的证明假设选项适用于由 sldv.assume 函数和 Proof Assumption 模块表示的证明假设。

使用 MATLAB Function 模块在 sldvdemo_sbr_verification 模型中指定属性证明目标和证明假设。

下面的命令会打开一个关联了 sldvdemo_sbr_verification 模型的示例。打开模型。

openExample('sldv/SldvexCCallerBlockExample')

将模型另存为 ex_sldvdemo_sbr_verification。

打开 Safety Properties 子系统。

打开 MATLAB Property 模块，它是一个 MATLAB Function 模块。

在 check_reminder 函数定义的末尾添加 sldv.assume(Inputs.KEY==0 | 1);，这样函数定义的最后两行为：

sldv.prove(implies(activeCond, SeatBeltIcon));
sldv.assume(Inputs.KEY==0 | 1);

要保存更新的代码，请在编辑器选项卡中点击保存并关闭编辑器。

要证明安全属性，请在 Simulink^® 编辑器中选择 Safety Properties 子系统。在 Design Verifier 选项卡上点击证明属性。

或者，在 Simulink 编辑器中，您可以右键点击 Safety Properties 子系统，然后依次选择 Design Verifier > 证明子系统属性。

MATLAB 表达式，例如 x > 0。

除了使用 sldv.assume 函数外，您还可以在模型中插入 Proof Assumption 模块。使用 sldv.assume 而不使用 Proof Assumption 模块有几个优点，如使用 Simulink Design Verifier 证明模型属性中所述。

通过使用 MATLAB 生成代码来证明模型时，您也可以在不使用 sldv.assume 函数的情况下约束信号值。使用 sldv.assume 而不是直接使用 MATLAB 生成代码可以省去以下操作：

在 R2009b 中推出