Ограничьте значения сигналов при доказательстве образцовых свойств
Simulink Design Verifier
При работе в доказывающем свойство режиме программное обеспечение Simulink® Design Verifier™ доказывает, что свойства модели удовлетворяют заданные критерии (см. то, Что Доказывает Свойство?). В этом режиме можно использовать блоки Предположения Доказательства, чтобы задать предположения для сигналов в модели. Параметр Values позволяет вам задать ограничения на значения сигналов во время доказательства свойства. Блок применяет заданный параметр Values к своему входному сигналу, и программное обеспечение Simulink Design Verifier доказывает или опровергает это, свойства вашей модели удовлетворяют заданные критерии.
Диалоговое окно параметра блока также позволяет вам:
Включите или отключите предположение.
Укажите, что блок должен отобразить свой параметр Values в Редакторе Simulink.
Укажите, что блок должен отобразить свой выходной порт.
Программное обеспечение Simulink и Simulink Coder™ игнорирует блок Proof Assumption во время симуляции модели и генерации кода, соответственно. Программное обеспечение Simulink Design Verifier использует блок Proof Assumption только при доказательстве образцовых свойств.
Используйте параметр 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 Assumption, программное обеспечение Simulink Design Verifier комбинирует их использующий логическую операцию OR во время доказательства свойства. В этом случае программное обеспечение полагает, что целое предположение удовлетворено, удовлетворены ли какой-либо один скаляр или интервал.
Блок Proof Assumption принимает сигналы всех встроенных типов данных, поддержанных программным обеспечением Simulink. Для обсуждения типов данных, поддержанных программным обеспечением Simulink, смотрите Типы данных, Поддержанные Simulink (Simulink).
Задайте, включен ли блок. Если выбрано (значение по умолчанию), программное обеспечение Simulink Design Verifier использует блок при доказательстве свойств модели. Очистка этой опции отключает блок, то есть, заставляет программное обеспечение Simulink Design Verifier вести себя, как будто блок Proof Assumption не существовал. Если эта опция не выбрана, блок появляется grayed в Редакторе Simulink.
Задайте, ведет ли блок себя как блок Proof Assumption или Test Condition. Выберите Test Condition, чтобы преобразовать блок Proof Assumption в блок Test Condition.
Задайте предположение доказательства (см. Предположения Доказательства Определения).
Задайте, отображает ли блок содержимое своего параметра Values в Редакторе Simulink. По умолчанию эта опция выбрана.
Задайте, отображает ли блок выходной порт в Редакторе Simulink. Если выбрано (значение по умолчанию), блок отображает свой выходной порт, позволяя его входному сигналу пройти как блок вывод. Если не выбранный, блок скрывает свой выходной порт и отключает входной сигнал. Следующая графика иллюстрирует внешний вид блока в каждом случае.
Pass through style (show Outport): Selected
Pass through style (show Outport): Deselected
