2

我想对 HTTP 交互进行建模，即一系列 HTTPRequest/HTTPResponse，并且我试图将其建模为转换系统。我使用以下方法在类 State 上定义了一个排序：

open util/ordering[State]

其中状态只是一组消息：

sig State { 
    msgSet: set Message
}

每对 (HTTPRequest->HTTPResponse) 和 (HTTPResponse->HTTPRequest) 在我的转换系统中都表示为一条规则。这些规则在 Alloy 中表示为谓词，可以让一个状态从一种状态移动到另一种状态。

例如，这是在收到特定 HTTPRequest 后生成 HTTPResponse 的规则：

pred rsp1 [s, s': State] {
    one msg: Request, msg':Response | (

       // Preconditions (previous Request)
    msg.method=get &&
    msg.address.url=sample_com &&

       // Postconditions (next Response)
    msg'.status=OK_200 &&

       // previous Request has to be in previous state
    msg in s.msgSet &&
       // Response generated is added to next state
    s'.msgSet = s.msgSet + msg' 
}

不幸的是，创建的模型似乎太复杂了：我们有十几个规则（比上面的更复杂，但遵循相同的模式）并且执行速度非常慢。

编辑：特别是，CNF 生成非常慢，而求解需要相当长的时间。

您对如何模拟类似的过渡系统有什么建议吗？

非常感谢！

4

1 回答 1

1

这是一个具有令人印象深刻的细节水平的模型；感谢您的分享！

各种形式的honestActionby 本身都不需要超过两三分钟才能找到一个实例（或者在某些情况下找不到任何实例），除了rsp8，它本身需要相当长的时间（它运行了十五分钟左右在我停止之前）。

因此，您观察到的长 CNF 准备时间显然是由（a）rsp8导致您的时间问题的honestAction谓词，或（b）谓词中析取的大小，或（c）两者造成的。

我怀疑但尚未证明时间问题是由填充模型所需的个体数量和模型中的约束数量的组合爆炸引起的。

我的第一直觉（仅此而已）是减少模型中的细节级别，特别是实例化您的抽象签名的大量单例签名。这些似乎（我可能是错的）存在于簿记目的（因此您可以确定哪些规则许可从一个状态到另一个状态的转换），或者因为建模者不信任 Alloy 生成签名的具体实例，如用户名，密码、代码等

就像现在的模型一样，看起来您正在做很多工作来定义特定示例中涉及的所有个人，而不是定义约束并让 Alloy 来完成查找示例的工作。（使用 Alloy 来检查特定的具体示例的属性可能很有用，但还有其他方法可以做到这一点。）

由于模型中的许多具体签名都受限于单例基数，我实际上并不知道定义它们会使查找模型的任务变得更加复杂。据我所知，它使它更简单。但我的直觉是认为，无论涉及哪些主机、用户和 URI，知道状态转换通常具有特定属性（并且可能更容易让 Alloy 建立）比知道更有用该属性rsp1适用于主机被命名examplecom并且地址URI是example_url_https等等的所有情况。

我推测减少其存在和属性被规定的个体数量，以及对哪些个体可以参与哪些状态转换的约束，将减少 CNF 生成时间。

如果您的长期目标是测试长序列的状态转换以测试从给定起点是否可能或不可能到达特定状态（或某种状态），您可能需要重新考虑启用的方法更短的状态转换序列来完成这项工作。

第二个猜想将涉及较少的模型重组。由于我认为我不完全理解的原因，有时量化one似乎会伤害而不是帮助性能，例如在这个例子中，明确量化一些变量some而不是one结果使问题变得易于处理而不是难以处理。

该问题涉及谓词中的量化，而不是整体模型中的量化，并且量化one并不是首先要考虑的，因此在这里可能不相关。但是我们可以one用一种简单的方式来测试关键字对这个模型的影响：我注释掉了honestActionexcept中的所有内容，rsp8并在 8 范围内运行谓词first != last，一次是大部分出现的注释都被one注释掉，一次是这些关键字完好无损。one注释掉关键字后，Analyzer 在 24 秒左右运行问题；使用one关键字，到目前为止，它运行了 500 秒，然后我决定提出并终止它。

因此，我会尝试one从特定于实例的个人的所有签名中删除关键字，仅将其保留在 get、post、OK_200 等和 appData 上。我也会尝试不使用 Key、SessionID、URL、Host、UserName 和 Password 的各种子类型，或者至少在run命令中限制它们的基数。

于 2014-09-07T15:22:45.623 回答