Fork: 0
nitta-lab / SpecificationSimulatorExperiments
Transfer to URL with SHA Find file
Newer
Older
SpecificationSimulatorExperiments / courseA / IM_DTRAM.html
okazakitakehiro on 4 Sep 9 KB IM_DTRAMのプロトタイプが完成．
Raw Blame History 
<!DOCTYPE html>
<html lang="ja">
<head>
	<meta charset="UTF-8">
	<style>
		c1{
			color: blue;
		}
		c2{
			color: red;
		}

	</style>
	<title>【InventoryManagement(DTRAM)】</title>
</head>
<body>
<h1 class="title">
	【InventoryManagement(DTRAM)の課題】
</h1>
<p>
	ここでは，InventoryManagementのDTRAMによる仕様記述に関する課題に取り組んでいただきます．<br>
	以下にDTRAMで記述されたInventoryManagementのモデルを示します．こちらを適宜参照しながらモデルの理解を行ってください．
</p>
<hr/>

<h2>InventoryManagementのDTRAMによる記述についての説明</h2>
<p>
	以下のモデルでは始めに，新規商品登録用のイベントチャンネル，<code><c1>channel</c1></code> <code>ItemRegistraction</code> を宣言しています．<br>
	次の <code><c1>channel</c1></code> <code>ReceivingOrShipping(itemId:<c1>Str</c1>)</code> は，<code>itemId</code> で登録されている商品に対して入荷か出荷を行う用のイベントチャンネルとして宣言しています．
</p>

<div style="padding: 10px; margin-bottom: 10px; border: 1px solid #333333; border-radius: 10px;">
	<pre>
<c1>channel</c1> ItemRegistration {
	<c1>out</c1> inventory(itemDB:<c1>Map</c1>, registerItem(itemId:<c1>Str</c1>, itemName:<c1>Str</c1>, quantity:<c1>Int</c1>)) = insert(itemDB, itemId, {"count": quantity, "name": itemName})
}

<c1>channel</c1> ReceivingOrShipping(itemId:<c1>Str</c1>) {
	<c1>out</c1> inventory.{itemId}.count(prev_quantity:<c1>Int</c1>, receiveOrShip(quantity:<c1>Int</c1>)) = prev_quantity + quantity
}
	</pre>
</div>
<hr/>

<h2>モデルの可視化</h2>
<p>
	先ほどのInventoryManagementのモデルのリソースとチャンネルを，DTRAMのモデリングツールを使用して可視化したものを以下の図に示します．<br>
</p>
<div class="img-center">
	<img src="../img/DTRAM/InventoryManagement/DTRAM Ver InventoryManagement architecture Visualize.png", class ="before-image-size"><br>
</div>
<p>
	この図がモデルの実行に依らない，リソースを表していることに注意して下さい．<br>
	始めに，図の中央にある <code>inventory</code> リソースは商品全体を保管する倉庫を表しており，
	<code><c1>channel</c1> ItemRegistration</code> を流れるメッセージ( <code>registerItem</code> )を受け取ります．<br>
	次に，<code>inventory</code> リソースの子リソースとして，<code>inventory.{itemId}</code> リソースが表示されています．<br>
	このリソースは，商品IDを表す <code>itemId</code> というパスパラメータを持っているため，一意なリソース(商品)の特定を可能にしています．<br>
	最後に，<code>inventory.{itemId}</code> リソースの子リソースとして，<code>itemId</code> で示された商品の在庫数を表す <code>inventory.{itemId}.count</code> リソースが表示されており，
	<code><c1>channel</c1> ReceivingOrShipping(itemId:<c1>Str</c1>)</code> を流れるメッセージ( <code>receiveOrShip</code> )を受け取ります．
</p>
<hr/>

<h2>InventoryManagementモデルの仮想実行について</h2>
<p>
	ここでは，InventoryManagementモデルの仮想実行について説明します．この仮想実行で用いるテストケースは次の通りです．<br>
<ol>
	<li>inventoryに新しく取り扱う商品(Asahi)を初期数量100で登録します．</li>
	<li>登録した商品(Asahi)を50個出荷します．</li>
</ol>
</p>

<h3>仮想実行の可視化:</h3>
<p>
	仮想実行を，シミュレーションツールを使用して可視化したものを以下に示していきます．<br>
	まず，システムの初期状態を可視化したものが以下の図です．
</p>

<div class="img-center">
	<img src="../img/DTRAM/InventoryManagement/DTRAM 1 Ver InventoryManagement.png", class ="before-image-size"><br>
</div>
<p>
	初期状態のため，<code>inventory</code> リソースには何の商品も登録されていない状態になっています．<br>
	次に，新商品(Asahi)を登録するので，<code>inventory</code> リソースをダブルクリックします．
</p>

<div class="img-center">
	<img src="../img/DTRAM/InventoryManagement/DTRAM 2 Ver InventoryManagement.png", class ="before-image-size"><br>
</div>
<p>
	<code>inventory</code> リソースに対して，<strong><code>registerItem</code></strong> という商品を登録するためのメッセージが選択できるので，こちらを選択します．
</p>

<div class="img-center">
	<img src="../img/DTRAM/InventoryManagement/DTRAM 3 Ver InventoryManagement.png", class ="before-image-size"><br>
</div>
<p>
	商品IDを表す <code>itemId</code> と商品名を表す <code>itemName</code> ，初期数量を表す <code>quantity</code> を入力できる画面が表示されます．
</p>

<div class="img-center">
	<img src="../img/DTRAM/InventoryManagement/DTRAM 4 Ver Inventory Management.png", class ="before-image-size"><br>
</div>
<p>
	ここでは，<code>registerItem("@123", "Asahi", 100)</code> を入力します．
</p>

<div class="img-center">
	<img src="../img/DTRAM/InventoryManagement/DTRAM 5 Ver Inventory Management.png", class ="before-image-size"><br>
</div>
<p>
	次の状態に遷移したので，商品IDが@123という状態の <code>inventory.@123</code> と
	在庫数量が100という状態の <code>inventory.@123.count</code> ，商品名がAsahiという状態の <code>inventory.@123.name</code> の３つのリソースが表示されました．<br>
	次に，登録した商品(Asahi)を50個出荷したいので，<code>inventory.@123.count</code> リソースをダブルクリックします．
</p>

<div class="img-center">
	<img src="../img/DTRAM/InventoryManagement/DTRAM 6 Ver Inventory Management.png", class ="before-image-size"><br>
</div>
<p>
	メッセージを選択する画面が同様に表示されますので，入荷か出荷を行う <strong><code>receiveOrShip</code></strong> というメッセージを選択します．
</p>

<div class="img-center">
	<img src="../img/DTRAM/InventoryManagement/DTRAM 7 Ver Inventory Management.png", class ="before-image-size"><br>
</div>
<p>
	入荷数量，または出荷数量の入力が可能な画面が表示されますので，ここでは <code>receiveOrShip(-50)</code> と入力して実行します．<br>
	ここで quantity が正の値のときは入荷，負の値のときは出荷が行われます．
</p>

<div class="img-center">
	<img src="../img/DTRAM/InventoryManagement/DTRAM 9 Ver Inventory Management.png", class ="before-image-size"><br>
</div>
<p>
	次の状態に遷移したため，<code>inventory.@123.count</code> リソースの状態が50に遷移したことが確認できました．
</p>
<hr/>

<h2>
	課題概要
</h2>
<p>
	本課題ではまず，上記にて説明を行ったInventoryManagementの仕様に，ある機能を追加した仕様を考えます．<br>
	その仕様のモデルと，仮想実行の流れを可視化した以下の図を見ていただいた上で，２つの設問にお答えいただきます．<br>
	設問にお答えいただく際は，必ず設問１，設問２の順番でご解答下さい．以下の図と同じものが設問のページにも記載されているのでこのまま設問のページに飛んでいただいてもかまいません．
</p>
<div style="padding: 10px; margin-bottom: 10px; border: 1px solid #333333; border-radius: 10px;">
<pre>
<c1>channel</c1> ItemRegistration {
	out inventory(itemDB:<c1>Map</c1>, registerItem(itemId:<c1>Str</c1>, itemName:<c1>Str</c1>, quantity:<c1>Int</c1>)) = insert(itemDB, itemId, {"count": quantity, "name": itemName})
}

<c1>channel</c1> Receiving(itemId:<c1>Str</c1>) {
	out inventory.{itemId}.count(prev_quantity:<c1>Int</c1>, receive(quantity:<c1>Int</c1>)) = prev_quantity + quantity
}

<c1>channel</c1> Shipping(itemId:<c1>Str</c1>) {
	out inventory.{itemId}.count(prev_quantity:<c1>Int</c1>, ship(quantity:<c1>Int</c1>)) = prev_quantity - quantity
}

</pre>
</div>

<h3>1:</h3>
<div class="img-center">
	<img src="../img/DTRAM/InventoryManagement/ShippingReceiving/DTRAM_1_Ver_InventoryManagement_ShippingReceiving.png", class ="before-image-size"><br>
</div>
<h3>2:</h3>
<div class="img-center">
	<img src="../img/DTRAM/InventoryManagement/ShippingReceiving/DTRAM_2_Ver_InventoryManagement_ShippingReceiving.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>