<!DOCTYPE html>
<html lang="ja">
<head>
<meta charset="UTF-8">
<style>
c1{
color: blue;
}
c2{
color: red;
}
</style>
<title>【InventoryManagement(Alloy)】</title>
</head>
<body>
<h1 class="title">
【InventoryManagement(Alloy)の課題】
</h1>
<p>
ここでは，Alloyを用いて記述したInventoryManagementの課題について説明します．<br>
以下にInventoryManagementのモデルを示します．こちらを適宜参照しながらモデルの理解を行ってください．
</p>
<hr/>
<h2>InventoryManagementのAlloyによる記述についての説明</h2>
<h3><code><c1>sig</c1></code>:</h3>
<p>
以下のモデルでは始めに，商品を識別するためのIDを表す <code>ItemId</code> と商品名を表す <code>Name</code> を集合として宣言しています．<br>
次に，商品全体を管理する倉庫を表している <code>Inventory</code> は，<code>itemDB</code> フィールドを持っています．
このフィールドを定義している行では，<code>itemDB</code> フィールドが <code>ItemId</code> から，
商品の情報を表す <code>Item</code> との対応関係を参照していることを表しています．<br>
最後の <code>Item</code> では始めに，商品名を表す <code>name</code> を <code>Item</code> の要素と，<code>Name</code> の要素の間の関係として定義しています．
次にある，在庫数を表す <code>count</code> では在庫数を <c2><code>Int</code></c2> 型で表すように定義を行っています．<br>
</p>
<h3><code><c1>pred</c1></code>:</h3>
<p>
以下のモデルで最初に記述されている <code>init</code> は，<code>Inventory</code> の
構造を持った <code>its</code> 初期化するという操作になっています．<br>
次の，<code>itemRegistraction</code> では初めて取り扱う商品を入荷する際に，
商品名と入荷数量を <code>Inventory</code> に登録するという操作になっています．<br>
その次にある， <code>receivingOrShipping</code> では登録されている商品に対して
入荷か出荷を行った際に起こる数量の変化の操作を表しています．<br>
最後の <code>execute</code> では上記にて説明を行った，
<code>init</code> ，<code>itemRegistraction</code> ，<code>receivingOrShipping</code> を
上から順番に実行を進めるという操作になっています．<br>
そして，最後にある <c1><code>run</code></c1> では，<code>execute</code> を呼び出して実行を行っています．
この実行の際に <code><c2>100</c2></code> や <code>-<c2>50</c2></code> の数字を扱うため，
末尾に <code><c2>8</c2></code> <code><c1>Int</c1></code> という
Alloyで8bitの数字を扱うことができるようにするための記述を行っています．
</p>
<div style="padding: 10px; margin-bottom: 10px; border: 1px solid #333333; border-radius: 10px;">
<pre>
<c1>sig</c1> ItemId, Name{}
<c1>sig</c1> Inventory {
itemDB: ItemId <c1>lone</c1> -> <c1>lone</c1> Item
}
<c1>sig</c1> Item {
name : Name,
count: <c1>Int</c1>
}
<c1>pred</c1> init[its: Inventory] {
<c1>no</c1> its.itemDB
}
<c1>pred</c1> itemRegistration[its, its': Inventory, itemId: ItemId, quantity: <c1>Int</c1>, n: Name] {
<c1>some</c1> it: Item | {
<c1>no</c1> itemId2: ItemId | its.itemDB[itemId2] = it
its'.itemDB = its.itemDB + itemId -> it
it.name = n
it.count = quantity
}
}
<c1>pred</c1> receivingOrShipping[its, its': Inventory, itemId: ItemId, quantity: <c1>Int</c1>] {
<c1>some</c1> it': Item | {
<c1>no</c1> itemId2: ItemId | its.itemDB[itemId2] = it'
its'.itemDB = its.itemDB ++ itemId -> it'
it'.name = its.itemDB[itemId].name
it'.count = plus[its.itemDB[itemId].count, quantity]
}
}
<c1>pred</c1> execute[] {
<c1>some disj</c1> its, its', its'': Inventory, itemId: ItemId, n: Name | {
init[its]
itemRegistration[its, its', itemId, <c2>100</c2>, n]
receivingOrShipping[its', its'', itemId, -<c2>50</c2>]
}
}
<c1>run</c1> execute <c1>for</c1> <c2>2</c2> but <c2>3</c2> Inventory, <c2>8</c2> <c1>Int</c1>
</pre>
</div>
<hr/>
<h2>モデルの可視化</h2>
<p>
先ほどのInventoryManagementを，Alloyの可視化ツールを使用して，モデルを可視化した図が以下の通りになります．<br>
</p>
<div class="img-center">
<img src="../img/Alloy/Alloy MetaModel Ver InventoryManagement.png", class ="before-image-size"><br>
</div>
<p>
<code>Inventory</code> が，商品名を表す <code>name</code> と在庫数を表す <code>count</code> の２つのフィールドを持っている，
<code>Item</code> を管理するというモデルになっています．
</p>
<hr/>
<h2>InventoryManagementの仮想実行について</h2>
<p>
ここでは，InventoryManagementの仮想実行について説明します．InventoryManagementの仮想実行で用いるテストケースは次の通りです．<br>
<ol>
<li>Inventoryに新しく取り扱う商品を100個入荷します．</li>
<li>お客様が商品を50個購入してくれたので，在庫数が50個に減少しました．</li>
</ol>
</p>
<h3>仮想実行の可視化:</h3>
<p>
先ほどの仮想実行を可視化したものを以下に示します．<br>
</p>
<div class="img-center">
<img src="../img/Alloy/Alloy Ver InventoryManagement.png", class ="before-image-size"><br>
</div>
<p>
左下にあるInventory2($execute_its)は，始めに <code>init</code> が実行された時の状態になっているため，
まだ何の商品(Item)も登録されていない状態になっています．<br>
次に，1番上の段の左にあるInventory1($execute_its')はテストケースの１が行われた時の状態になっているため，
100個のItem1を入荷している状態になっています．<br>
そして，Inventory1の右にあるInventory0($execute_its'')ではテストケース２が行われた時の状態になっているため，
在庫数が50個に減少しています．
</p>
<hr/>
<h2>
課題概要
</h2>
<p>
本課題ではまず，上記にて説明を行ったInventoryManagementに，とある機能を追加した時のモデルと可視化の図を
実験参加者の皆様に見て頂きます．<br>
次に，その２つを見て<strong>どの様な機能が追加されたのか</strong>，また<strong>どの様なテストケースになっているのか</strong>を
考えて頂き，以下のアンケートにお答えください．
</p>
<div style="padding: 10px; margin-bottom: 10px; border: 1px solid #333333; border-radius: 10px;">
<pre>
<c1>sig</c1> ItemId, Name{}
<c1>sig</c1> Inventory {
itemDB: ItemId <c1>lone</c1> -> <c1>lone</c1> Item
}
<c1>sig</c1> Item {
name : Name,
count: <c1>Int</c1>
}
<c1>pred</c1> init[its: Inventory] {
<c1>no</c1> its.itemDB
}
<c1>pred</c1> itemRegistration[its, its': Inventory, itemId: ItemId, quantity: <c1>Int</c1>, n: Name] {
<c1>some</c1> it: Item | {
<c1>no</c1> itemId2: ItemId | its.itemDB[itemId2] = it
its'.itemDB = its.itemDB + itemId -> it
it.name = n
it.count = quantity
}
}
<c1>pred</c1> shippingOrReceiving[its, its': Inventory, itemId: ItemId, quantity: <c1>Int</c1>] {
plus[its.itemDB[itemId].count, quantity] < <c2>0</c2> <c1>implies</c1> {
<c1>all</c1> itemId': ItemId | its'.itemDB[itemId'] = its.itemDB[itemId']
}
<c1>else</c1> {
<c1>some</c1> it': Item | {
<c1>no</c1> itemId2: ItemId | its.itemDB[itemId2] = it'
its'.itemDB = its.itemDB ++ itemId -> it'
it'.name = its.itemDB[itemId].name
it'.count = plus[its.itemDB[itemId].count, quantity]
}
}
}
<c1>pred</c1> execute[] {
<c1>some disj</c1> its, its', its'', its''': Inventory, itemId: ItemId, n: Name | {
init[its]
itemRegistration[its, its', itemId, <c2>100</c2>, n]
shippingOrReceiving[its', its'', itemId, -<c2>50</c2>]
shippingOrReceiving[its'', its''', itemId, -<c2>75</c2>]
}
}
<c1>run</c1> execute <c1>for</c1> <c2>2</c2> <c1>but</c1> <c2>4</c2> Inventory, <c2>8</c2> <c1>Int</c1>
</pre>
</div>
<div class="img-center">
<img src="../img/Alloy/Alloy_Ver_InventoryManagementCheckMinus.png", class ="before-image-size"><br>
</div>
<p>
<strong>
<a href="https://docs.google.com/forms/d/e/1FAIpQLSf5rIUfHnzsLMLPZ_KWnsukn3HcEGBSLN-BxzRPzqszyrlj8g/viewform?usp=sf_link" target="_blank" rel="noopener noreferrer">
課題アンケート (別タブが開きます)
</a>
</strong>
<br>
<strong>
<a href="https://docs.google.com/forms/d/e/1FAIpQLSf8Ex1RPzMRvyUYIRkCjcIY69fI74sNXK-m4rNAoAcR6_dm4g/viewform?usp=sf_link" target="_blank" rel="noopener noreferrer">
課題終了後の評価アンケート (別タブが開きます)
</a>
</strong>
</p>
<hr>
<br>
<a href="IM_DTRAM.html">【InventoryManagement(DTRAM)】へ</a>
</body>
<style>
.title{
text-align: center;
}
.links-manual-A{
display: flex;
flex-direction: column;
}
.img-center{
display: flex;
justify-content: center;
align-items: center;
}
.before-image-size{
max-width: 100%;
height: auto;
}
.after-image-size{
max-width: 100%;
height: auto;
}
</style>
</html>
