sldv.assume

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

折叠所有页面

语法

sldv.assume (expr)

sldv.assume (expr）指定expr在证明属性时，对每一个求值都成立。使用任意有效的布尔表达式expr．

除了评估的间接副作用外，该函数没有输出，也没有对其养育函数的影响expr．如果你在MATLAB中给出这个函数^®命令行中，该函数没有任何作用。

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

的证明假设选项中的财产证明窗格应用于表示的证明假设sldv.assume函数和证明假设块。

中指定属性证明目标和证明假设sldvdemo_sbr_verification通过使用MATLAB函数块。

打开sldvdemo_sbr_verification建模并另存为ex_sldvdemo_sbr_verification．

打开安全属性子系统。

打开MATLAB的财产Block是aMATLAB函数块。

在最后check_reminder函数定义，添加sldv.assume(输入。Key =0 | 1);函数定义的最后两行是:

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

若要保存更新后的代码，请使用编辑器选项卡上,单击保存并关闭编辑器。

为了证明安全性，在Simulink中万博1manbetx^®编辑器，选择安全属性子系统。在设计验证器选项卡上,单击证明属性．

或者，在Simulink编辑器中，您可以右键万博1manbetx单击安全属性子系统并选择设计验证器>证明子系统属性．

以MATLAB表达式为例X > 0．

而不是使用sldv.assume函数，可以插入证明假设块在你的模型中。使用sldv.assume而不是Proof Assumption块提供了几个好处，在什么是财产证明?．

在使用MATLAB进行代码生成证明模型时，还可以约束信号值而不使用sldv.assume函数。使用sldv.assume无需直接使用MATLAB进行代码生成，无需:

在R2009b中引入