使用 Requirements Table 模块创建正式需求

自 R2022a 起

使用Requirements Table模块来模型形式化需求。您可以使用布尔公式来建立形式化需求，以检查所需的模型行为是否在仿真中发生。当您在 Requirements Table模块中创建需求时，您也会在需求编辑器中创建一个等效需求。请参阅配置正式需求的属性。

定义正式需求

正式需求是一组明确的规范，可以用数学方式表达，并通过仿真来执行。如果在指定的时间内至少一个条件为真，则执行每个正式需求。当需求执行时，该模块会验证指定的仿真行为并生成额外的仿真数据。

为了定义形式化需求，请向您的模型添加一个Requirements Table模块。

This is the appearance of the Requirements Table block.

打开一个新的Requirements Table模块会显示一个空白的需求。默认情况下，该模块在需求选项卡上打开。表格的每一行代表一个需求。这些列指定了用于评估每个需求的信息。这些列是：

索引 - 每个需求的唯一标识符。此列是只读的。
摘要 - 基于文本的需求摘要。此列中的条目不会影响模块行为。此列为选填。
预条件 - 在评估其余需求之前，必须在指定的时间内为真。
持续时间 - 以秒为单位的时间，在评估其余需求之前，先决条件必须为真。此列为选填。如果留空，则表示需求没有持续时间。您必须指定先决条件才能使用此列。请参阅使用持续时间列。
后条件 - 如果相关先决条件在指定持续时间内为真，则该布尔表达式必须为真。如果不包括先决条件，则模块会在每个时间步检查后条件。
操作 - 如果相关先决条件在指定持续时间内为真，模块执行的操作。您可以使用动作来定义模块输出或调用函数。如果不包括先决条件，则模块会在每个时间步执行该操作。

This shows the inside of a new Requirements Table block. It contains one blank requirement.

您可以创建多个需求、预条件、后条件和操作。要管理列和需求，请使用表选项卡中提供的选项。您还可以通过右键点击需求索引或列标题单元格来使用上下文菜单访问其他选项。

您还可以在假设选项卡中指定定义系统物理约束的假设。请参阅将假设添加到需求中。

创建形式需求的表达式

您可以使用表达式定义预条件、后条件和动作。使用布尔表达式表示前提预条件和后条件，并使用单个等号 = 来定义动作。每个预条件和后条件单元中的表达式必须计算为标量逻辑。

在表达式中使用数据来管理信息，例如信号值、工作区变量或常量值。表达式还可以包括数值和函数。例如，预条件 u >= 0 检查数据 u 是否大于或等于 0，而动作 y = 0 将数据 y 设置为等于 0。

您可以通过在需求单元格中明确列出每个完整表达式，或者在列标题中列出表达式的左侧并在需求中定义表达式的右侧来定义预条件、后条件和操作。要编写使用预条件和 后条件列中的标题的布尔表达式，请使用感兴趣的布尔关系运算符，将左侧留空，然后输入感兴趣的值。要编写使用标题的操作，请在单元格中输入操作的值。

例如，在此表中，第一个后条件指定标题中的数据 y1，第二个后条件指定需求单元格中的数据 y2，而操作将 y3 设置为等于值向量。

This image shows a Requirements Table block that uses both header and non header syntaxes. The expressions evaluate the same content.

您还可以检查标量头是否等于预条件和 后条件列中的单个值、多个值或一系列值。使用这些语法来指定检查的值：

语法	描述
`value`	检查标题数据是否等于 `value`。
`value1,value2,value3,`...`,valueN`	检查标题数据是否等于逗号分隔的值之一。
`[value1,value2]`	检查头数据是否大于或等于 `value1` 且小于或等于 `value2`。
`(value1,value2)`	检查标题数据是否大于 `value1` 且小于 `value2`。
`[value1,value2)`	检查标题数据是否大于或等于 `value1` 且小于 `value2`。
`(value1,value2]`	检查头数据是否大于 `value1` 且小于或等于 `value2`。

在此表中，预条件检查 u 是否等于 1、2 或 3。后条件使用相同的布尔表达式但不同的符号来评估数据 y1 和 y2。第一个后条件使用带有区间符号的标题数据，第二个后条件使用不带标题数据的显式布尔运算符。

This image shows a requirements table that uses both header and non header syntaxes with interval notation. The expressions evaluate the same expression using different notation.

要根据多个间隔评估标题数据，请将它们与逻辑 OR 运算符相结合。例如，[0.3, 0.5] || (0.1, 0.2) 是有效的。除了实数之外，您还可以在区间中使用 Inf 来评估趋向无穷大的界限。包括 Inf 在内的间隔必须位于括号之前或之后。如果单元格仅包含一个区间，则可以简化包括 Inf 在内的间隔。例如，(0.3, Inf) 相当于 > 0.3。

要指定标题数据不应等于表达式，请使用逻辑 NOT 运算符，即在单元格值的左侧输入 ~= 或 ~。您可以将此运算符应用于单个值、逗号分隔的值或间隔。例如，如果您不希望标题数据 u 落在区间[0.3, 0.5] 内，则输入 ~[0.3, 0.5] 或 ~=[0.3, 0.5]。对于逗号分隔的值，仅使用 ~。

如果您的需求单元格包含大量内容，则单元格大小可能会阻碍表达。要查看全部内容，您可以调整单元格的大小或添加新行。要添加新行，请用 ... 完成第一行，然后按 Alt+Enter。

使用 `X` 占位符

在标题中输入表达式时，请不要在该列的单元格中重复使用标题表达式。例如，如果标题包含数据 u，请不要在关联的列单元格中输入表达式 u >= 0.5 && u <= 0.3。相反，使用 X 作为标题的占位符。例如，在先决条件中，表达式 X >= 0.5 && X <= 0.3 如果标题中包含 u，则等效于 u >= 0.5 && u <= 0.3 如果标题中不包含 u。

This image shows a requirement with header data u and the placeholder X in the expression.

当标题较长时，使用 X 占位符可以提高可读性。

检查预条件和后条件中的数组数据

如果在预条件和后条件中使用数组数据，则模块将检查数据的每个元素是否满足逻辑表达式并生成一个逻辑数组。要检查先决条件或后条件是否满足值数组，请使用计算标量逻辑的函数，例如 isequal 或 all 函数。例如，如果 y1 是一个 1×4 数组，并且您想要检查它是否等于 [1 2 3 4]，请在元胞中输入 isequal(y1,[1 2 3 4]) 或 all(y1 == [1 2 3 4])。

在 Requirements Table 模块中使用函数

您可以在需求单元格或列标题中的 Requirements Table 模块中使用函数和运算符。将数据作为参量输入到函数或运算符中，就像对 MATLAB^® 中的变量进行操作一样。在此表中，单元格 u1 + u2 == 2 和标题 u3 + u4 下方的单元格都检查两个输入数据的总和是否等于 2。

This image shows a requirement that checks if the sum of the data is greater than 0 using the header and non-header notations.

Requirements Table模块不支持标题中写入全局变量或内部状态的函数。例如，您不能在标题中使用 rand 函数，因为 rand 每次生成数字时都会写入内部状态。

定义模块数据

为了使用模块中的数据，您必须在您的需求中输入它们并在符号窗格中定义它们。要打开符号窗格，请打开Requirements Table模块。在建模选项卡的设计数据部分中，点击符号窗格。

在符号窗格中，类型列中的图标表示您的数据范围。您可以将数据范围设置为输入、输出、局部、常量或参数。您还可以更改名称、初始数据值和端口号。要修改其他属性，请右键点击数据名称并选择检查以打开属性检查器。有关更多信息，请参阅在 Requirements Table 模块中定义数据。

This image shows the Symbols pane with the name of an input data u and an output data y, along with the data names, data types, and port numbers.

当您编辑需求时，Requirements Table模块会检测未定义的数据，并在符号窗格中使用未定义符号图标标记它们。未解析的数据可能会导致编译期间出现错误。要解析数据，点击解析未定义符号按钮。

观测或生成模型行为

您可以使用 Requirements Table模块通过观测模型行为或生成可与模型行为进行比较的行为来检查模型需求。

观测模型行为

此示例使用:

打开模型

您可以使用 Requirements Table 模块来观测模型行为，而无需执行操作。如果模型行为不满足先决条件，模块不会检查相关的后条件。如果在满足先决条件时模型行为不满足需求的后条件，则 Requirements Table 模块会在诊断查看器中发出警告。要使用 Requirements Table 模块来观测需求，请使用预条件来指定模型输入行为，并使用后条件来指定模型输出行为。为了区分模型输入和输出，请在属性检查器中为后条件中指定的数据启用将其作为设计模型输出进行分析属性。请参阅视为设计模型输出进行分析。

该模型包含一个 Requirements Table 模块，用于测试具有两个输入和输出两个值的基本子系统。Requirements Table 模块通过使用预条件和后条件的逻辑定义来检查子系统的输入和输出是否满足指定的需求。

打开 Requirements Table 模块来查看子系统输入和输出的指定需求。这些需求指定了对每个子系统输入的子系统输出的逻辑约束。Requirements Table 模块使用数据 u1 和 u2 捕获子系统输入，并使用数据 y1 和 y2 捕获子系统输出。该模块将数据定义为输入数据，这允许该模块捕获子系统信号作为模块输入。

当运行模型时，Requirements Table 模块会检查 Subsystem模块是否满足预条件。如果满足预条件，Requirements Table 模块会检查 Subsystem 模块的输出是否满足后条件。

此示例 Subsystem模块满足预条件和后条件。要生成警告，请将第一个需求的后条件设置为y1 < 0，然后再次运行仿真。诊断查看器显示一条警告消息。

生成模型行为

此示例使用:

打开模型

您还可以使用 Requirements Table 模块在模型满足相应预条件时执行操作。您可以使用操作列指定每个需求的操作。

该模型包含一个 Requirements Table 模块，用于测试接受两个输入并创建两个输出的子系统。如果满足预条件，Requirements Table 模块将接受子系统输入并输出一组值。每个 Requirements Table 模块输出对应子系统的一个输出。如果子系统的输出不等于 Requirements Table 模块相应的输出信号，则 Assertion 模块将停止仿真并产生错误。

打开 Requirements Table 模块来查看为子系统输入指定的两个需求。这些需求指定了对输入的逻辑约束。该模块将数据u1和u2定义为输入数据，这使得该模块可以捕获子系统输入作为模块输入。该模块将数据y1和y2定义为输出数据。

当运行模型时，Requirements Table 模块会检查 Subsystem模块的输入是否满足预条件，并将输出信号分配给 Action 列中指定的值。然后，模型将来自 Subsystem模块的输出与来自 Requirements Table 模块的输出信号进行比较。在此示例中，输出相等并且断言通过。