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