Функция подтверждения допущений для диаграмм статофлоу и функциональных блоков MATLAB
Эта функция не имеет выхода и не влияет на ее родительскую функцию, кроме каких-либо косвенных побочных эффектов оценки expr. При выполнении этой функции из командной строки MATLAB ® эта функция не действует.
Вкрапить sldv.assume подтверждение допущений в коде MATLAB или разделение допущений на сценарий проверки.
Опция «Подтверждение допущений» на панели «Подтверждение свойств» применяется к подтверждающим допущениям, представленным sldv.assume и блоком Proof Absulation.
Укажите цель доказательства свойства и допущение доказательства в sldvdemo_sbr_verification с использованием функционального блока MATLAB.
Откройте окно sldvdemo_sbr_verification модель и сохраните ее как ex_sldvdemo_sbr_verification.
Откройте подсистему свойств безопасности.
Откройте блок свойств MATLAB, который является блоком функций MATLAB.
В конце check_reminder определение функции, добавление sldv.assume(Inputs.KEY==0 | 1); чтобы последние две строки определения функции были:
sldv.prove(implies(activeCond, SeatBeltIcon)); sldv.assume(Inputs.KEY==0 | 1);
Чтобы сохранить обновленный код, на вкладке «Редактор» нажмите кнопку «Сохранить» и закройте редактор.
Для подтверждения свойств безопасности в редакторе Simulink ® выберите подсистему свойств безопасности. На вкладке Design Verifier щелкните Доказать свойства .
Либо в редакторе Simulink можно щелкнуть правой кнопкой мыши подсистему свойств безопасности и выбрать Design Verifier > Доказать свойства подсистемы.
Вместо использования sldv.assume можно вставить в модель блок Proof Summission. Используя sldv.assume вместо блока Proof Absulation предлагает несколько преимуществ, описанных в разделе Что такое проверка свойств?.
При проверке моделей с помощью MATLAB для генерации кода можно также ограничить значения сигналов без использования sldv.assume функция. Используя sldv.assume вместо непосредственного использования MATLAB для генерации кода устраняет необходимость:
Выражайте предположение с помощью блока Simulink.
Явное подключение вывода предположения к блоку Simulink.
Допущение доказательства | Цель доказательства | sldv.condition | sldv.prove | sldv.test | Условие испытания | Цель тестирования