Панель верификатора проекта: доказательство свойства
Свойство, доказывающее обзор панели
Задайте опции, которые управляют, как 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Поисковые запросы сначала нарушений свойства в количестве шагов симуляции заданы опцией Maximum violation steps; затем это пытается доказать свойства, для которых этому не удалось обнаружить нарушение. Эта стратегия является комбинацией
ProveиFindViolationстратегии.
Зависимость
Выбор FindViolation или ProveWithViolationDetection включает параметр Maximum violation steps.
Информация о командной строке
Параметр: DVProvingStrategy |
| Ввод: массив символов |
Значение: 'Prove' | 'FindViolation' | 'ProveWithViolationDetection' |
Значение по умолчанию: 'Prove' |
Смотрите также
Максимальные шаги нарушения
Задайте максимальное количество шагов симуляции, по которым Simulink Design Verifier ищет нарушения свойства.
Настройки
Значение по умолчанию: 20
Программное обеспечение Simulink Design Verifier не ищет вне максимального количества шагов симуляции, которые вы задаете. Поэтому это не может идентифицировать нарушения, которые могут произойти позже в симуляции.
Зависимость
Этот параметр включен, когда вы устанавливаете Strategy на FindViolation или ProveWithViolationDetection.
Информация о командной строке
Параметр: DVMaxViolationSteps |
Ввод: int32 |
| Значение: любое допустимое значение |
Значение по умолчанию: 20 |