合金を使用して自動販売機プログラムをモデル化しようとしています。私はいくらかのお金を入れてマシンにアイテムの選択オプションを提供できるモデルを作成したいと思っています。ここでは、入力としてボタンと一緒にコインを入力しようとしています。値を指定すると、自動販売機から目的のアイテムが返されます。各項目に割り当てられた金額が入力として提供されます。したがって、ここでは、ボタン a には 10 個の R が必要であり、ボタン b には 5 個の rs が必要であり、c には 1 が必要であり、d には 2 が必要です。op インスタンスは、必要な金額が投入されると返されるアイテムです。opc は、返されるコインの残高です。ip は入力ボタン、x はお金の入力です。入力として複数のコインを取り込むようなインスタンスを提供するにはどうすればよいですか。また、金額がアイテムのコストよりも大きい場合は、コインの数を返す必要があります。私が助けを得ることができれば、それは大歓迎です。
質問する
208 次
2 に答える
1
モジュール vending_machines
open util /ordering[イベント]
fun fst:Event{順序付け/最初}
fun 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:イベント | let pfx=upto[e] | #(製品&pfx)<=#(コイン&pfx)
于 2013-04-09T03:30:12.520 に答える