我想为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的生成非常缓慢，而求解需要相当长的时间。
你对如何建立类似的过渡系统有什么建议吗？
非常感谢！
这是一个具有令人印象深刻的细节级别的模型；感谢您的分享！
honestAction的各种形式本身都不需要超过两三分钟才能找到一个实例（或者在某些情况下找不到任何实例），除了rsp8，它本身需要相当长的时间（在我停止它之前，它运行了大约十五分钟）。
因此，您观察到的长CNF准备时间显然是由（a）导致时间问题的谓词rsp8，或（b）honestAction谓词中析取的大小，或（c）两者都造成的。
我怀疑但尚未证明时间问题是由填充模型所需的个体数量和模型中约束的数量的组合爆炸引起的。
我的第一直觉（仅此而已）是减少模型中的细节级别，特别是实例化抽象签名的大量单例签名。这些似乎（我可能错了）要么是出于记账目的（这样你就可以确定哪条规则允许从一个状态转换到另一个状态），要么是因为建模者不信任Alloy生成签名的具体实例，如用户名、密码、代码等。
按照现在的模型，看起来你正在做大量的工作来定义特定示例中涉及的所有个人，而不是定义约束并让Alloy来寻找示例。（使用Alloy来检查性能——一个特定的具体例子可能很有用，但还有其他方法可以做到这一点。）
由于模型中的许多具体签名都被限制为单例基数，我实际上不知道定义它们会使查找模型的任务变得更加复杂；据我所知，它让事情变得更简单。但我的直觉是，知道（Alloy可能更容易建立）状态转换通常具有特定的属性，无论涉及什么主机、用户和URI，比知道属性rsp1适用于主机名为examplecom、地址URI为example_url_https等等的所有情况更有用。
I猜想减少其存在性和性质被规定的个体的数量，以及对哪些个体可以参与哪些状态转换的约束，将减少CNF的生成时间。
如果你的长期目标是测试长序列的状态转换，以测试从给定的起点是否有可能或不可能达到特定的状态（或某种状态），那么你可能需要重新思考实现较短序列的状态过渡的方法。
第二个猜想将涉及较少的模型重组。由于我不完全理解的原因，有时用one量化似乎会伤害而不是帮助性能，比如在本例中，用some而不是one显式量化一些变量，结果证明问题是可处理的，而不是棘手的。
这个问题涉及谓词的量化，而不是整个模型的量化，而且one的量化一开始就不是有意的，所以它在这里可能不相关。但我们可以用一种简单的方式来测试one关键字对该模型的影响：我注释掉了honestAction中除rsp8之外的所有内容，并在8的范围内运行谓词first != last，一次注释掉了大多数one的出现，一次这些关键字保持不变。one关键字被注释掉后，Analyser在24秒内左右运行了问题；有了one关键字，它运行了500秒，直到我决定要点并终止它
因此，我会尝试从所有具有实例特定个人的签名中删除关键字one，只在get、post、OK_200等和appData中保留它。我也会尝试不使用Key、SessionID、URL、Host、UserName和Password的各种子类型，或者至少在run命令中约束它们的基数。