证明假设
在证明模型属性时约束信号值
图书馆
金宝app仿真软件设计验证器
描述
当运行在属性证明模式时，金宝app®设计验证器™软件证明您的模型的特性满足指定的标准(见什么是财产证明?）.在这种模式下，您可以使用Proof Assumption模块来为模型中的信号定义假设。的值参数允许您在属性证明期间指定对信号值的约束。块应用指定的值参数设置为其输入信号，而金宝app仿真软件设计验证器软件证明或不证明您的模型的属性满足指定的标准。
块的参数对话框还允许您:
启用或禁用假设。
指定该块应该显示其值参数。金宝app
指定该块应该显示其输出端口。
请注意
仿真软件金宝app和金宝app仿真软件编码器™软件在模型仿真和代码生成过程中分别忽略了Proof Assumption模块。的金宝app仿真软件设计验证器软件只在证明模型属性时使用Proof Assumption模块。
指定验证假设
使用值参数来约束属性证明中的信号值。以MATLAB的形式指定任意标量和区间的组合®单元阵列。有关单元格阵列的信息，请参见细胞数组．
提示
如果值参数只指定一个标量值，不需要以MATLAB单元数组的形式输入。
每个标量值组成数组中的一个单元格，例如:
{0, 5}
一个封闭的间隔包含一个二元向量作为数组中的单元格，其中每个元素指定一个间隔端点:
{[1, 2]}
属性指定标量值Sldv。点构造函数，它接受一个值作为其参数。可以使用Sldv。时间间隔构造函数，它需要两个输入参数，即区间的下界和上界。可选地，您可以提供以下值之一作为指定包含或排除间隔端点的第三个输入参数:
“()”-定义开放间隔。“[]”—定义关闭时间间隔。“()”-定义左开间隔。“()”—定义右开间隔。
请注意
默认情况下,Sldv。时间间隔如果忽略了它的第三个输入参数，则认为它是关闭的。
举个例子值参数
{0, [1,3]}
指定:
0——一个标量(1、3)-一个封闭的间隔
的值参数
{Sldv。Interval(0,1， '[)')， Sldv.Point(1)}
指定:
Sldv。时间间隔(0,1,“()”)-右开间隔[0,1)Sldv.Point (1)——一个标量
如果你为一个证明假设块指定多个标量和间隔，则金宝app仿真软件设计验证器软件在财产证明过程中使用逻辑或操作将它们组合起来。在这种情况下，如果满足任何单个标量或区间，软件认为满足整个假设。
数据类型支持金宝app
Proof Assumption模块接受Simulink软件支持的所有内置数据类型的信号。金宝app金宝app有关Simulink软件支持的数据类型的讨论，请参见金宝app金宝appSimulink支持的金宝app数据类型金宝app．该块不支持复杂的输入信号。金宝app
参数
- 启用
-
指定该块是否启用。如果选中(默认)，则金宝app仿真软件设计验证器软件在证明一个模型的属性时使用块。清除此选项将禁用该块，即导致金宝app仿真软件设计验证器软件的行为，好像证明假设块不存在。如果未选择此选项，则该块在Simulink编辑器中显示为灰色。金宝app
- 类型
-
指定块的行为是证明假设块还是测试条件块。选择
测试条件将证明假设块转换为测试条件块。 - 值
-
指定证明假设(参见指定验证假设）.
- 显示值
-
指定该块是否显示其内容值参数。金宝app默认情况下，选择此选项。
- 传递样式(显示Outport)
-
指定该块是否在Simulink编辑器中显示输出端口。金宝app如果选中(默认)，块将显示其输出端口，允许其输入信号作为块输出通过。如果未被选中，该块将隐藏其输出端口并终止输入信号。下面的图形说明了每一种情况下块的外观。
传递样式(显示输出):选中
传递样式(show Outport):取消选中
你也可以从以下列表中选择一个网站:
