Home Articles

合金和webpro

Asked
Viewed 509 times
-4

我是合金的新人,我有一个与Alloy有关的任务 .

我必须用合金建模协议,该协议是一个网络协议 .

我有一个发送者,接收者和一个中间实体 .

我在这些实体上写了签名,但我不知道如何运行这个模型 .

我试图理解电子邮件客户端的地址簿示例,但是当我执行该示例时,它会生成一个简单书籍的大量实例,这些书籍将名称映射到一个地址 .

我认为模型中有3个签名是Book,Name和Addr . 如果我们运行此模型以运行3但是第1册,则该示例将生成多少个实例? 9? 18?或者更多?

请指导我如何使合金工作!


我想在ALLOY中 Build 一个Web协议,并且用于通信的基本实体是三个 . 三个entites发送消息和接收消息,每个消息都粘贴到特定时间,如消息o到time0,消息1到time1 .

我在通过Alloy进行协议建模时面临很多困难,特别是消息序列制作和处理其他消息序列 .

怎么解决?

1 Answer

  • 2

    毫无疑问,您可以在Alloy中指定您的Web协议 .

    Alloy允许您通过运行谓词生成可满足的实例,或允许通过检查断言来查找计数器示例 .

    此实例生成实际上将帮助您验证模型的某些属性,并且如果不满足某些预期属性,将允许您更正模型 . (由于实例生成,您可以逐步改进模型) .

    生成的实例数将取决于您的范围构成的域中存在的可满足实例的数量 .

    请在您的问题中添加更多详细信息,以便我们更具体地回答 .

Related