Определение доказательных допущений

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

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

{0, 5}

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

{[1, 2]}

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

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

{0, [1, 3]}

задает:

Параметр Values

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

задает:

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