sldv.assume
Функция доказывания допущения для диаграмм и Блоков MATLAB function Stateflow
Синтаксис
Описание
Эта функция не имеет выхода и никакого влияния на ее родительскую функцию, кроме любых косвенных побочных эффектов оценки expr. Если вы выпускаете эту функцию из MATLAB® командная строка, функция не имеет эффекта.
Интерсперсные sldv.assume доказательство допущений в коде MATLAB или разделите допущения на скрипты верификации.
Опция Proof assumptions на панели Property proving применяется к доказательствам, представленным sldv.assume функцию и блоком Proof Assumption.
Примеры
Задайте Property Цель Доказательства и доказательство допущения
Задайте цель доказательства свойства и доказательство допущения в sldvdemo_sbr_verification моделировать при помощи блока MATLAB Function.
Откройте sldvdemo_sbr_verification моделировать и сохранить как ex_sldvdemo_sbr_verification.
Откройте подсистему Свойства.
Откройте блок MATLAB Property, который является блоком MATLAB Function.
В конце check_reminder определение функции, добавление sldv.assume(Inputs.KEY==0 | 1); так что последние две линии определения функции:
sldv.prove(implies(activeCond, SeatBeltIcon)); sldv.assume(Inputs.KEY==0 | 1);
Чтобы сохранить обновленный код, на вкладке Editor нажмите Save и закройте редактор.
Чтобы доказать свойства безопасности, в Simulink® Редактор, выберите Подсистему свойств безопасности. На вкладке Design Verifier нажмите Prove Properties.
Кроме того, в редакторе Simulink можно щелкнуть правой кнопкой мыши Подсистему свойств безопасности и выбрать Design Verifier > Prove Subsystem Properties.
Входные параметры
Альтернативы
Вместо использования sldv.assume функция, можно вставить Proof Assumption блок в модель. Использование sldv.assume вместо блока Proof Assumption предлагает несколько преимуществ, описанных в «Что такое Property Proving?».
При доказывании моделей с помощью MATLAB для генерации кода можно также ограничивать значения сигналов, не используя sldv.assume функция. Использование sldv.assume вместо непосредственного использования MATLAB для генерации кода устраняет необходимость:
Выразите предположение при помощи блока Simulink.
Явным образом соедините выход допущения с блоком Simulink.
См. также
Proof Assumption | Proof Objective | sldv.condition | sldv.prove | sldv.test | Test Condition | Test Objective