Определение предположений доказательства

Используйте параметр Values, чтобы ограничить значения сигналов в доказательствах свойства. Задайте любую комбинацию скаляров и интервалов в форме массива ячеек MATLAB^®. Для получения информации о массивах ячеек см. Массивы ячеек.

Скалярные значения каждый включает отдельную ячейку в массиве, например:

{0, 5}

Закрытый интервал включает двухэлементный вектор как ячейку в массиве, где каждый элемент задает конечную точку интервала:

{[1, 2]}

В качестве альтернативы можно задать скалярные значения с помощью Sldv.Point конструктор, который принимает одно значение как его аргумент. Можно задать интервалы с помощью Sldv.Interval конструктор, который требует двух входных параметров, i.e., нижняя граница и верхняя граница для интервала. Опционально, можно ввести одно из следующих значений как третий входной параметр, который задает включение или исключение конечных точек интервала:

Как пример, параметр Values

{0, [1, 3]}

задает:

Параметр Values

{Sldv.Interval(0, 1, '[)'), Sldv.Point(1)}

задает:

Если вы задаете несколько скаляров и интервалов для блока Proof Assumption, программное обеспечение Simulink Design Verifier комбинирует их использующий логическую операцию OR во время доказательства свойства. В этом случае программное обеспечение полагает, что целое предположение удовлетворено, удовлетворяют ли какому-либо одному скаляру или интервалу.