指定具有时间逻辑的状态机

QuickStrom使用线性时间逻辑（LTL）来指定Web应用程序。在解释它的工作原理时，我发现LTL的基础知识对新人来说是直观的。另一方面，它不明显地使用LTL指定真实系统。这就是为什么我以博客帖子的形式从过去一年分享一些学习和想法。

此帖子侧重于如何在状态机方面使用LTL指定系统。这是一个简短的概述，避免过多的细节。有关如何使用此类规范测试Web应用程序的更多信息，请参阅Quickstrom文档。

为避免可能的混淆，我想首先指出这种上下文中的状态机规范与TLA +（或类似的建模语言中的模型不同。我们没有构建模型以证明或检查属性。相反，我们在状态机转换方面定义属性，最终目标是通过检查录制的痕迹与我们的规范相匹配来测试实际系统行为（例如Web应用程序，桌面应用程序，API）。

在这篇文章中，我们将使用LTL语言。这是未来规范语言的速写。

公式（多种公式）是一种逻辑表达式，可评估为真或假。我们有常数：

==＆gt;操作员含义。到目前为止，我们有命题逻辑，但我们需要更多的东西。

在我们的语言的核心，我们有国家的概念。系统随着时间的推移而改变状态，我们希望在我们的规范中表达这一点。但是我们看到的公式迄今为止不处理时间。为此，我们使用时间运算符。

为了说明时间运算符如何工作，我将使用图表来可视化迹线（状态序列）。 黑色圆圈表示公式为真的状态，并且白色圆圈表示公式是假的状态。 所有其他州的两个公式都是假的。 公式和痕迹将如下可视化： P●────────○───────○ 请注意，在这些图中，我们假设最后一个状态永远重复。 这似乎有点奇怪，但绘制无限数量的状态是有问题的。 下一个运算符将公式作为参数作为参数，并在下一个状态下评估它。 下一个P●───○───○P○───────○ 下一个运算符相对于当前状态，而不是跟踪中的第一个状态。 这意味着我们可以嵌套接下来进入未来。

接下来（下一个p）●───────────────●──●──────○p○──────────── ●────────

好吧，时间为一个更具体的例子，我们将在整个帖子中发展。假设我们有一个公式gdproconsentisible，当gdpr同意屏幕可见时，这是真的。我们指定屏幕应在当前和下一个状态下可见：

一对连续状态称为步骤。在指定状态机时，我们使用下一个运算符来描述状态转换。状态转换公式是一个步骤的逻辑谓词。

在上面的GDPR示例中，我们表示，同意屏幕应在这两个国家保持可见。如果我们想描述同意屏幕的能见度的国家变更，我们可以说：

但有趣的状态机通常具有多于一种可能的转换，有趣的行为可能包含多个步骤。

虽然我们可以嵌套包含下一个运算符的公式，但我们将陷入困境的规格，仅描述有限次数的转换。

考虑以下内容，我们喜欢说明GDPR同意屏幕应该始终可见：

这不适用于具有周期的状态机，即可能是无限迹线，因为我们只能嵌套一个有限数量的下一个运算符。我们想要描述任何转换的状态机规范。

这是我们拿起始终运算符的地方。它将公式作为参数，如果在当前状态和所有未来状态下给定的公式，则为真实。

始终P●─────────────────────────────────────○────── ──────────────────●───

请注意第三个状态和向前Q的Q.如此，因为当前和所有未来状态都变得如此。

让我们重新审视始终可见的同意屏幕规范。我们不试着筑巢，而不是试图筑巢，而是说：

整洁的！这称为不变的属性。不变性是个人状态的断言，不变的属性表明它必须在跟踪中的每个状态。

现在，让我们来吧我们的游戏。要将系统指定为状态机，我们可以将带有差异（||）和始终运算符组合的转换。首先，我们定义单个转换公式打开并关闭：

让开放=不是gdprconsentisvisible＆amp;＆amp;下一个gdprconsentisvisible;让close = gdprconsentisvisible＆amp;＆amp;接下来（不是gdprconsentisvisible）;

我们的国家机器公式表示，它始终通过开放或关闭描述的转换：

我们有一个状态机规格！请注意，此规范仅允许同意屏幕的可见性来回转换。

到目前为止，我们只看到了安全性质的例子。这些是指定“没有发生不好的东西”的属性。但我们也想指定某种方式以某种方式进行进度。以下两个时间运算符让我们指定活力属性，即“好事最终发生。”

我们旁边使用了指定转换，始终指定不变性和状态机。但我们可能还希望在我们的规范中使用活力属性。在这种情况下，我们不是在谈论具体步骤，而是目标。

时间运算符最终将公式带为参数，如果在当前或任何未来状态下给定的公式，则为真实。

最终P○───────────────────────○最终Q●───────────────────────── ────○Q○──────○───────

例如，我们可以说同意屏幕应该最初是可见的，最终隐藏：

这并没有说它隐藏在一起。它可能再次可见，我们的规范将允许这一点。要指定它应该保持隐藏，我们最终和始终使用组合：

让我们来看看一个图表，了解时间运算符的组合更好：

最终（始终p）○────────────────────────○─ ──●───────●Q○──────●───────

如果公式最终（总是p）在任何状态下都不是真的，因为P永远不会永远终于呈现。其他公式最终（总是Q），在所有状态都是如此，因为Q在第三状态中永远变为真实。

我想讨论的最后一个时间运算符是。对于p直到q为true，p必须是真的，直到q变为真实。

p直到q●───────────────────────○○○───○─────────────────────────── ─●───○

就像最终的运营商一样，停止条件（Q）不必永远保持真实，但它至少是真的，至少一次。

直到操作员比始终和最终更具表现力，并且可以通过直到来定义。 2

无论如何，让我们回到我们的跑步之下。假设我们有另一个公式支持挑剔，当显示支持聊天按钮时，这是真的。我们希望在关闭GDPR同意屏幕之后，确保它没有显示出来：

否定使读取更难，但它相当于非正式陈述：“支持聊天按钮至少隐藏在隐藏的GDPR同意屏幕之前。”但是，它不要求支持聊天按钮可见。为此，我们说：

在该公式中，支持特征必须最终变为真实，并且在该点时必须隐藏同意屏幕。

我们可以使用直到运营商定义最终转换更明确的状态机公式。

假设我们想更加严格地指定GDPR同意屏幕。假设我们已经拥有了可能的状态转换公式：

在该公式中，我们允许任何数量的allowCollectedData或禁止脉冲Data过渡，直到最终提交导致闭合同意屏幕。

我们已经查看了LTL中的一些时间运算符，以及如何使用它们来指定状态机。我希望这篇文章给了你一些想法和灵感！

值得退房的另一个博客文章是Hillel Wayne的TLA +行动属性。它专门为TLA +编写，但大多数概念适用于LTL和Quickstrom规范。

我打算编写后续行动，涵盖原子命题，查询，行动和事件。如果您想评论，Github，Twitter和龙虾上有线程。您可能还想赞助我的工作。

谢谢Vitor Enes，Andrey Mokhov，Pascal Poizat，以及Liam O'Connor审查这篇文章的草案。

未来版本的Quickstrom将使用针对测试量身定制的LTL的不同风味，并支持满足活动属性。 ↩︎

我们可以最终定义p = true，直到p，且可能有点难以掌握，总是p =不是（true直到不是p）。或者我们总是可以说p =不是（最终不是p）。 ↩︎