Proof Objective
Задайте цели, которым сигналы должны удовлетворить при доказательстве свойств модели
Библиотека
Simulink Design Verifier
Описание
При работе в доказывающем свойство режиме программное обеспечение Simulink® Design Verifier™ доказывает, что свойства модели удовлетворяют заданным критериям (см. то, Что Доказывает Свойство?). В этом режиме можно использовать блоки Цели доказательства, чтобы задать цели доказательства для сигналов в модели.
Параметр Values позволяет вам задать приемлемые значения для входного сигнала блока. Если значение сигналов отклоняется от приемлемых значений в каком-либо временном шаге, нарушение свойства происходит, и цель доказательства сфальсифицирована. Блок применяет заданный параметр Values к своему входному сигналу, и программное обеспечение Simulink Design Verifier доказывает или опровергает это, свойства вашей модели удовлетворяют заданным критериям.
Диалоговое окно параметра блока позволяет вам
Включите или отключите цель.
Укажите, что блок должен отобразить свой параметр Values в Редакторе Simulink.
Укажите, что блок должен отобразить свой выходной порт.
Примечание
Программное обеспечение Simulink и Simulink Coder™ игнорирует блок Proof Objective во время симуляции модели и генерации кода, соответственно. Программное обеспечение Simulink Design Verifier использует блок Proof Objective только при доказательстве свойств модели.
Определение целей доказательства
Используйте параметр Values, чтобы задать значения, которых сигнал должен достигнуть во время симуляции доказательства. Задайте любую комбинацию скаляров и интервалов в форме массива ячеек MATLAB®. Для получения информации о массивах ячеек см. Массивы ячеек (MATLAB).
Совет
Если параметр Values задает только одно скалярное значение, вы не должны вводить его в форме массива ячеек MATLAB.
Скалярные значения каждый включает отдельную ячейку в массиве, например:
{0, 5}Закрытый интервал включает двухэлементный вектор как ячейку в массиве, где каждый элемент задает конечную точку интервала:
{[1, 2]}В качестве альтернативы можно задать скалярные значения с помощью Sldv.Point конструктор, который принимает одно значение как его аргумент. Можно задать интервалы с помощью Sldv.Interval конструктор, который требует двух входных параметров, т.е. нижней границы и верхней границы для интервала. Опционально, можно ввести одно из следующих значений как третий входной параметр, который задает включение или исключение конечных точек интервала:
'()'— Задает открытый интервал.'[]'— Задает закрытый интервал.'(]'— Задает лево-открытый интервал.'[)'— Задает правильно-открытый интервал.
Примечание
По умолчанию, Sldv.Interval полагает, что интервал закрывается, если вы не используете его третий входной параметр.
Как пример, параметр Values
{0, [1, 3]}задает:
0
— скаляр[1, 3]
— закрытый интервал
Параметр Values
{Sldv.Interval(0, 1, '[)'), Sldv.Point(1)}задает:
Sldv.Interval(0, 1, '[)')— правильно-открытый интервал [0, 1)Sldv.Point(1)— скаляр
Если вы задаете несколько скаляров и интервалов для блока Proof Objective, программное обеспечение Simulink Design Verifier комбинирует их использующий логическую операцию OR во время доказательства свойства. В этом случае программное обеспечение полагает, что целая цель доказательства удовлетворена, удовлетворяют ли какому-либо одному скаляру или интервалу.
Поддержка типов данных
Блок Proof Objective принимает сигналы всех встроенных типов данных, поддержанных программным обеспечением Simulink. Для обсуждения типов данных, поддержанных программным обеспечением Simulink, смотрите Типы данных, Поддержанные Simulink (Simulink). Блок не поддерживает комплексные входные сигналы.
Параметры
- Enable
Задайте, включен ли блок. Если выбрано (значение по умолчанию), программное обеспечение Simulink Design Verifier использует блок при доказательстве свойств модели. Очистка этой опции отключает блок, то есть, заставляет программное обеспечение Simulink Design Verifier вести себя, как будто блок Proof Objective не существовал. Если эта опция не выбрана, блок появляется grayed в Редакторе Simulink.
- Values
Задайте цель доказательства (см. Цели доказательства Определения).
- Display values
Задайте, отображает ли блок содержимое своего параметра Values в Редакторе Simulink. По умолчанию эта опция выбрана.
- Pass through style
Задайте, отображает ли блок выходной порт в Редакторе Simulink. Если выбрано (значение по умолчанию), блок отображает свой выходной порт, позволяя его входному сигналу пройти как блок выход. Если не выбранный, блок скрывает свой выходной порт и отключает входной сигнал. Следующая графика иллюстрирует внешний вид блока в каждом случае.
Pass through style: Selected
Pass through style: Deselected
- Stop simulation when the property is violated
Задайте, остановить ли симуляцию, если симуляция сталкивается с сигналом, который нарушает свойство, заданное в параметре Values.
Если вы выбираете этот параметр и симулируете модель, остановки симуляции, если это сталкивается с нарушением заданного свойства.