Задайте опции, которые управляют тем, как Simulink® Design Verifier™ доказывает свойства для моделей, которые он анализирует.
Укажите, включены ли или отключены блоки Assertion в модели.
По умолчанию: Use local settings
Use local settingsВключает или отключает блоки Assertion зависимости от значения параметра Enable каждого блока. Если выбран Enable параметр блока, блок активируется; в противном случае блок отключен.
Enable allВключает все блоки Assertion в модели независимо от настроек их параметров Enable.
Disable allОтключает все блоки Assertion в модели независимо от настроек их параметров Enable.
Параметр: DVAssertions |
| Тип: символьный массив |
Значение: 'UseLocalSettings' | 'EnableAll' | 'DisableAll' |
По умолчанию: 'UseLocalSettings' |
Укажите, включены ли или отключены блоки Proof Assumption в модели.
По умолчанию: Use local settings
Use local settingsВключает или отключает блоки Proof Assumption зависимости от значения параметра Enable каждого блока. Если выбран Enable параметр блока, блок активируется; в противном случае блок отключен.
Enable allВключает все блоки Proof Assumption в модели независимо от настроек их параметров Enable.
Disable allОтключает все блоки Proof Assumption в модели независимо от настроек их параметров Enable.
Параметр: DVProofAssumptions |
| Тип: символьный массив |
Значение: 'UseLocalSettings' | 'EnableAll' | 'DisableAll' |
По умолчанию: 'UseLocalSettings' |
Укажите стратегию, которую Simulink Design Verifier использует при проверке свойств.
По умолчанию: Prove
ProveВыполняет проверку свойств.
FindViolationПоиск только нарушений свойств в пределах количества шагов симуляции, заданных опцией Maximum violation steps.
ProveWithViolationDetectionИщет как нарушения собственности, так и пытается доказать свойства, по которым не удалось обнаружить нарушение. Эта стратегия является относительно оптимальным балансом между ProveWithViolationDetection и FindViolation стратегии.
Выбор FindViolation или ProveWithViolationDetection включает параметр Maximum violation steps.
Параметр: DVProvingStrategy |
| Тип: символьный массив |
Значение: 'Prove' | 'FindViolation' | 'ProveWithViolationDetection' |
По умолчанию: 'Prove' |
Задайте максимальное количество шагов симуляции, на которых Simulink Design Verifier ищет нарушения свойств.
По умолчанию: 20
Программа Simulink Design Verifier не ищет больше заданного максимального количества шагов симуляции. Поэтому он не может идентифицировать нарушения, которые могут произойти позже в симуляции.
Этот параметр активируется, когда вы задаете Strategy FindViolation или ProveWithViolationDetection.
Параметр: DVMaxViolationSteps |
Тип: int32 |
| Значение: любое допустимое значение |
По умолчанию: 20 |