Design Verifier 窗格：属性证明
属性证明窗格概述
指定控制 Simulink® Design Verifier™ 如何证明其所分析模型的属性的选项。
另请参阅
Assertion 模块
指定模型中的 Assertion 模块是否启用或禁用。
设置
默认值：使用局部设置
- 使用局部设置
根据每个模块的启用参数的值启用或禁用 Assertion 模块。如果选择了模块的启用参数，则启用该模块；否则，禁用该模块。
- 全部启用
启用模型中的所有 Assertion 模块，无论其启用参数的设置如何。
- 全部禁用
禁用模型中的所有 Assertion 模块，无论其启用参数的设置如何。
命令行信息
参数：DVAssertions |
| 类型：字符数组 |
值：'UseLocalSettings' | 'EnableAll' | 'DisableAll' |
默认值： 'UseLocalSettings' |
另请参阅
证明假设
指定模型中的 Proof Assumption 模块是否启用或禁用。
设置
默认值：使用局部设置
- 使用局部设置
根据每个模块的启用参数的值启用或禁用 Proof Assumption 模块。如果选择了模块的启用参数，则启用该模块；否则，禁用该模块。
- 全部启用
启用模型中的所有 Proof Assumption 模块，无论其启用参数的设置如何。
- 全部禁用
禁用模型中的所有 Proof Assumption 模块，无论其启用参数的设置如何。
命令行信息
参数：DVProofAssumptions |
| 类型：字符数组 |
值：'UseLocalSettings' | 'EnableAll' | 'DisableAll' |
默认值： 'UseLocalSettings' |
另请参阅
策略
指定 Simulink Design Verifier 在证明属性时使用的策略。
设置
默认值：证明
- 证明
进行属性证明。
- FindViolation
仅搜索最大违规步数选项指定的仿真步骤数内的属性违规。
- ProveWithViolationDetection
搜寻属性违规行为，并尝试证明未能检测到违规行为的属性。该策略是 Prove 和 FindViolation 策略之间的相对最佳平衡。
依赖关系
选择 FindViolation 或 ProveWithViolationDetection 可启用最大违规步数参数。
命令行信息
参数：DVProvingStrategy |
| 类型：字符数组 |
值：'Prove' | 'FindViolation' | 'ProveWithViolationDetection' |
默认值： 'Prove' |
另请参阅
最大违规步数
指定 Simulink Design Verifier 搜索属性违规的最大仿真步数。
设置
默认值： 20
Simulink Design Verifier 软件不会搜索超出您指定的最大仿真步骤数。因此，它无法识别在仿真后期可能发生的违规行为。
依赖关系
当将策略设置为 FindViolation 或 ProveWithViolationDetection 时，此参数启用。
命令行信息
参数：DVMaxViolationSteps |
类型：int32 |
| 值：任何有效值 |
默认值： 20 |
