【发布时间】：2014-08-29 15:46:36
【问题描述】：
我想对 HTTP 交互进行建模，即 HTTPRequest/HTTPResponse 序列，并且我试图将其建模为转换系统。 我使用以下方法在类 State 上定义了一个排序：
open util/ordering[State]
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 生成非常慢，而求解需要相当长的时间。
您对如何建模类似的过渡系统有什么建议吗？
非常感谢！
【问题讨论】：
-
原则上，您似乎没有做任何明显错误的事情。但是，如果您正在创建一系列状态，那么您的模型是否不需要服务器（或整个系统）永远不会两次处于相同状态？这似乎需要比您原本需要的更多的状态（以及让读者说“等等，HTTP 不是无状态协议吗？！”）；如果您允许重用状态，您可能会获得更好的性能。许多事情可以影响性能；您尝试过许多不同的 SAT 求解器吗？
-
感谢您的回复！今天早上，我尝试了几个 SAT 求解器，但没有得到更好的表现。特别是，事实证明，大部分分析时间都与 CNF 子句的生成有关。你说得对，我们从来没有两次处于同一状态，但这不应该成为我正在建模的案例研究中的问题。关于如何改进 CNF 生成阶段的任何建议？
-
如果没有更多细节，我无法提出任何建议（我怀疑其他人也可能）。您可能需要提供minimum complete example 来说明问题：展示性能问题的最短可能示例。生成这样一个最小示例所需的工作量可能很大，但它也可以帮助您找到解决方案。
-
关于状态重用问题——您可能是对的，您对状态的处理不会使模型无效。然而，这里的相关点是，任何需要模型拥有更多个体的东西都会减慢分析速度。允许状态重用是否可以解决您的性能问题？
-
我无法复制问题；使用您在 pastebin 中提供的模型，Alloy 报告在大约 400 毫秒内找不到模型。 （顺便说一下，许多 Stack Overflow 版主不鼓励使用 pastebin，因为如果粘贴的材料消失了，它会使问题变得不那么有用。）我非常普遍的建议是：从简单的开始，大纲有三个或五个签名，并逐步建立；不要等到有 17 个抽象签名和 60 多个具体签名才尝试实例化模型。
标签： http transitions alloy model-checking transition-systems