http - 在Alloy中建模HTTP转换系统

Question

我想建模一个http交互，也就是一个httprequest/httpresponse序列，我试图将其建模为一个转换系统。
我在类状态上定义了一个顺序，方法是：

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的生成速度非常慢，而求解需要相当长的时间。
你对如何建立一个类似的过渡体系有什么建议吗？
非常感谢！

Answer 1

这是一个模型，有一个令人印象深刻的细节水平，谢谢你分享它！
各种形式的honestAction本身都不需要超过两三分钟就可以找到一个实例（或者在某些情况下找不到任何实例），除了rsp8本身需要相当长的时间（在我停止它之前它运行了大约十五分钟）。
因此，你观察到的长cnf准备时间显然是由（a）导致你时间问题的just predicatersp8或者（b）谓词中析取的大小，或者（c）两者都造成的。
我怀疑但还没有证明时间问题是由填充模型所需的个体数量和模型中的约束数量的组合爆炸引起的。
我的第一个直觉（不超过这个）是减少模型中的细节层次，特别是大量实例化抽象签名的单例签名。这些似乎（我可能错了）是出于记账目的而出现的（这样您就可以确定哪个规则允许从一个状态转换到另一个状态），或者是因为建模者不信任alloy来生成签名的具体实例，如用户名、密码、代码等。
就像现在的模型一样，您似乎正在做大量的工作来定义特定示例中涉及的所有个人，而不是定义约束并让alloy完成查找示例的工作。（使用alloy检查特定具体示例的属性可能很有用，但有其他方法可以做到这一点。）
由于模型中的许多具体签名都被限制在单点基数上，我实际上不知道定义它们会使查找模型的任务变得更复杂；据我所知，这会使它更简单。但我的直觉是，知道（也可能更容易让alloy建立）状态转换通常有一个特定的属性（不管涉及到什么主机、用户和uri）比知道属性honestAction适用于主机名为rsp1且地址uri为examplecom的所有情况更有用。什么都没有。
我猜想，减少个体的存在和性能规定的数量，以及个人可以参与哪些状态转换的约束，将减少CNF生成时间。
如果您的长期目标是测试状态转换的长序列，以测试从给定的起点是否有可能或不可能到达特定的状态（或某种状态），则可能需要重新考虑使较短的状态转换序列能够完成工作的方法。
第二个猜想将涉及较少的模型重组。由于我认为我不完全理解的原因，有时用example_url_https量化似乎伤害了性能，而不是帮助性能，如在this example中，用one而不是some显式量化一些变量，结果是使问题变得可处理而不是难以处理。
这个问题涉及到谓词中的量化，而不是整个模型中的量化，而且one的量化一开始并不是有意的，所以这里可能不相关。但是，我们可以用一种简单的方法来测试one关键字对这个模型的影响：我在one中注释掉了除honestAction之外的所有内容，并在8的范围内运行谓词rsp8，一次注释掉了大多数first != last的出现，一次注释完这些关键字。注释掉one关键字后，分析器在24秒左右运行问题；one关键字就位后，它运行了500秒，直到我确定该点并终止它。
因此，我将尝试从具有实例特定个体的所有签名中删除关键字one，只在get、post、ok_200等和appdata上保留它。我还尝试不使用key、sessionid、url、host、username和password的各种子类型，或者至少在one命令中约束它们的基数。