sldv.assume

Stateflow 图表和 MATLAB 函数模块的证明假设函数

语法

sldv.assume(expr)

sldv.assume(expr) 指定在证明属性时，expr 对于每次评估都为真。对 expr 使用任何有效的布尔表达式。

除了评估 expr 的任何间接副作用外，此函数没有输出，并且对其父函数也没有影响。如果从 MATLAB^® 命令行发出此功能，则该功能无效。

将 sldv.assume 证明假设散布在 MATLAB 代码中或将假设分离到验证脚本中。

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

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

下面的命令打开一个附加了sldvdemo_sbr_verification模型的示例。打开模型。

openExample('sldv/SldvexCCallerBlockExample')

将模型保存为 ex_sldvdemo_sbr_verification 。

打开安全属性子系统。

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

在check_reminder函数定义的最后添加sldv.assume(Inputs.KEY==0 | 1);，使得函数定义的最后两行是：

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

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

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

或者，在 Simulink 编辑器中，您可以右键单击安全属性子系统并选择 Design Verifier > 证明子系统属性 。

MATLAB 表达式，例如 x > 0 。

您可以插入Proof Assumption模块，而不是使用sldv.assume模型。使用 sldv.assume 而不是 Proof Assumption模块有几个好处，如什么是财产证明？中所述。

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

在 R2009b 中推出