| |
|---|
| | DTRAM では，InventoryManagement のモデルを以下のようなチャンネル単位で記述していきます．<br> |
|---|
| | 商品登録用のイベントチャンネルを <code>ItemRegistration</code> ，<code>itemId</code> で登録されている商品に対して入荷か出荷を行うためのイベントチャンネルを <code>ReceivingOrShipping(itemId:<c1>Str</c1>)</code> として宣言しています．<br> |
|---|
| | <code>ItemRegistration</code> チャンネルでは <code>inventory</code> リソースが，メッセージ <code>registerItem(itemId, itemName, quantity)</code> を受け取ると， リソースの状態が <code>itemDB</code> から <code>insert(itemDB, itemId, {"count": quantity, "name": itemName})</code> に変わることを示しています．<br> |
|---|
| | ここで，<code>insert()</code> 関数は，第1引数に渡された写像に対し，第2引数と第3引数の対応を追加した結果得られる写像を返す関数です．<br> |
|---|
| | また <code>{"count": quantity, "name": itemName}</code> は，<code>"count"</code> と <code>"name"</code> をキーに持つ JSON オブジェクトを表しています．<br> |
|---|
| | また <code>{"count": quantity, "name": itemName}</code> は，<code>"count"</code> と <code>"name"</code> をキーに持つ JSON オブジェクトを表しています．<br> |
|---|
| | <code>ReceivingOrShipping(itemId:<c1>Str</c1>)</code> チャンネルでは <code>inventory.{itemId}.count</code> リソースがメッセージ <code>receiveOrShip(quantity)</code> を受け取ると， |
|---|
| | 遷移前の状態 <code>prev_quantity</code> が <code>prev_quantity + quantity</code> に変わることを示しています．<br> |
|---|
| | </p> |
|---|
| | |
|---|
| |
|---|
| | |
