Proof Objective
Задайте цели, которые сигналы должны удовлетворять при доказывании свойств модели
Библиотека
Simulink Design Verifier
Описание
При работе в режиме проверки свойств Simulink® Design Verifier™ программного обеспечения доказывает, что свойства вашей модели удовлетворяют заданным критериям (см. «Что такое Property Proving?»). В этом режиме можно использовать блоки Proof Objective, чтобы задать цели доказательства для сигналов в вашей модели.
Параметр Values позволяет вам задать приемлемые значения для входного сигнала блока. Если значение сигналов отклоняется от допустимых значений на любом временном шаге, происходит нарушение свойства, и цель доказательства фальсифицируется. Блок применяет указанный параметр Values к своему входному сигналу, а программное обеспечение Simulink Design Verifier доказывает или опровергает, что свойства вашей модели удовлетворяют заданным критериям.
Диалоговое окно параметра блока позволяет
Включите или отключите цель.
Укажите, что блок должен отображать свой параметр Values в Редактор.
Укажите, что блок должен отображать свой выходной порт.
Примечание
Программное обеспечение Simulink и Simulink Coder™ игнорируют блок Цель Доказательства во время симуляции модели и генерации кода, соответственно. Программа Simulink Design Verifier использует блок Цель Доказательства только при доказывании свойств модели.
Определение целей доказательства
Используйте параметр Values, чтобы задать значения, которых должен достичь сигнал во время симуляции доказательства. Задайте любую комбинацию скаляров и интервалов в форме 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)- скаляр
Если для блока Цель Доказательства задано несколько скаляров и интервалов, программа Simulink Design Verifier объединяет их с помощью логической операции OR во время проверки свойства. В этом случае программное обеспечение рассматривает полную цель доказательства как удовлетворенную, если удовлетворен какой-либо один скаляр или интервал.
Поддержка типа данных
Блок Цель Доказательства принимает сигналы всех встроенных типов данных, поддерживаемых программным обеспечением Simulink. Для обсуждения типов данных, поддерживаемых программным обеспечением Simulink, смотрите Типы данных, поддерживаемые Simulink. Блок не поддерживает сложные входные сигналы.
Параметры
- Enable
Укажите, включен ли блок. Если выбран (по умолчанию), программа Simulink Design Verifier использует блок при проверке свойств модели. Удаление этой опции отключает блок, то есть заставляет программное обеспечение Simulink Design Verifier вести себя так, как если бы блок Цель Доказательства не существовал. Если эта опция не выбрана, блок появляется серым цветом в редакторе 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.
Если вы выбираете этот параметр и моделируете модель, симуляция останавливается, если оно встречается с нарушением заданного свойства.