Задайте опции, которые управляют, как 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 |