Панель верификатора проекта: доказательство свойства

Свойство, доказывающее обзор панели

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

Смотрите также

Для просмотра документации необходимо авторизоваться на сайте