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