昔はよく当たりのある自動販売機が街角にあった。ジュースを買うとルーレットがまわり、当たるともう１本もらえるというものである。今回はそれを単純化しモデリングする。 channel coin, juice VMB(n) = coin -> juice -> ( VMB(n-1) |~| juice -> VMB(n-2)…

購入者、自動販売機をそれぞれCSPでモデリングし、正しく動作するシステムを検証しながら設計してみよう。まず、下記のような購入者3人と自動販売機をモデリングする。購入者の動作はコインを入れ、ジュースのボタンを押す。 channel coin, juice PERSON = c…