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．

打开Safety Properties子系统。

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

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

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

中保存更新的代码编辑器选项卡上,单击保存并关闭编辑器。

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

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

例如MATLAB表达式，x > 0．

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

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

介绍了R2009b