我正在尝试使用alloy 对自动售货机程序进行建模。我希望创建一个模型，我可以在其中插入一些钱并为机器提供一个项目的选择选项，它会为我提供相同的功能，如果提供的钱少，则不会提供任何东西。在这里，我尝试输入一个硬币和一个按钮作为输入，它应该从自动售货机返回所需的物品，提供值即。分配给每个项目的金额作为输入提供。所以这里按钮 a 应该需要 10 个 Rs，按钮 b 需要 5 个 rs， c 需要 1 并且 d 需要 2 。op 实例是插入所需资金后返回的项目。opc 是要退回的硬币余额。ip 是输入按钮，x 是钱输入。我如何提供一个实例，使其接收多个硬币作为输入，并且如果金额大于项目成本，那么它应该返回一个硬币数量。如果我能得到一些帮助，将不胜感激。
问问题
208 次
2 回答
2
如果我是你，我会问自己我关心什么样的实体；你已经做到了（硬币和物品的签名——你还需要一些客户的概念吗？）。
接下来，我会问自己什么构成了系统的合法状态——有时通过询问什么构成非法或不可接受的状态来回想它会有所帮助。
然后我会尝试将操作定义为从系统的一种合法状态到下一种合法状态的转换——您已经提到过插入货币和选择物品。
在每个阶段，我都会使用分析器来检查模型的实例，看看我到目前为止所做的是否有意义。Daniel Jackson 的Software Abstractions的 Whirlwind Tour 章节给出了这种按顺序定义实体、状态和状态转换的模式的一个示例——如果您可以访问该书，您会发现复习该章节很有帮助。
祝你好运！
于 2013-04-08T19:53:59.537 回答
1
模块 vending_machines
打开 util /ordering[事件]
有趣的 fst:Event{ordering/first}
有趣的 nxt:Event->Event{ordering/next}
fun upto[e:Event]:set Event{prevs[e]+e}
抽象信号事件{}
sig Coin 扩展事件{}
pred no_vendor_loss[product:set (Event-Coin)] {
所有 e:Event | 让 pfx=upto[e] | #(产品&pfx)<=#(硬币&pfx)
于 2013-04-09T03:30:12.520 回答