Fork: 0
nitta-lab / SpecificationSimulatorExperiments
Transfer to URL with SHA Find file
Newer
Older
SpecificationSimulatorExperiments / courseA / IM_DTRAM.html
okazakitakehiro on 3 Sep 8 KB IM_Alloyの修正とIM_DTRAMのプロトタイプが完成．
Raw Blame History 
  1. <!DOCTYPE html>
  2. <html lang="ja">
  3. <head>
  4. 	<meta charset="UTF-8">
  5. 	<style>
  6. 		c1{
  7. 			color: blue;
  8. 		}
  9. 		c2{
  10. 			color: red;
  11. 		}
  12.  
  13. 	</style>
  14. 	<title>【InventoryManagement(DTRAM)】</title>
  15. </head>
  16. <body>
  17. <h1 class="title">
  18. 	【InventoryManagement(DTRAM)の課題】
  19. </h1>
  20. <p>
  21. 	ここでは，DTRAMを用いて記述したInventoryManagementの課題について説明します．<br>
  22. 	以下にInventoryManagementのモデルを示します．こちらを適宜参照しながらモデルの理解を行ってください．
  23. </p>
  24. <hr/>
  25.  
  26. <h2>InventoryManagementのDTRAMによる記述についての説明</h2>
  27. <p>
  28. 	以下のモデルでは始めに，新規に取り扱う商品を入荷する時に使用されるイベントチャンネル，<code><c1>channel</c1></code> <code>ItemRegistraction</code> を宣言しています．<br>
  29. 	次にある，<code><c1>channel</c1></code> <code>ReceivingOrShipping(itemId:<c1>Str</c1>)</code> は <code>itemId</code> を用いて
  30. 	登録されている商品に対して出荷か入荷を行う時に使用されるイベントチャンネルになります．
  31. </p>
  32.  
  33. <div style="padding: 10px; margin-bottom: 10px; border: 1px solid #333333; border-radius: 10px;">
  34. 	<pre>
  35. <c1>channel</c1> ItemRegistration {
  36. 	<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})
  37. }
  38.  
  39. <c1>channel</c1> ReceivingOrShipping(itemId:<c1>Str</c1>) {
  40. 	<c1>out</c1> inventory.{itemId}.count(prev_quantity:<c1>Int</c1>, receiveOrShip(quantity:<c1>Int</c1>)) = prev_quantity + quantity
  41. }
  42. 	</pre>
  43. </div>
  44. <hr/>
  45.  
  46. <h2>モデルの可視化</h2>
  47. <p>
  48. 	先ほどのInventoryManagementを，DTRAMの可視化ツールを使用して，モデルを可視化した図が以下の通りになります．<br>
  49. </p>
  50. <div class="img-center">
  51. 	<img src="../img/DTRAM/InventoryManagement/DTRAM Ver InventoryManagement architecture Visualize.png", class ="before-image-size"><br>
  52. </div>
  53. <p>
  54. 	まず，始めに商品全体を管理する倉庫を表している <code>inventory</code> というリソースがあります．<br>
  55. 	次に，その下の階層に <code>inventory</code> リソースを親にしている，<code>inventory.{itemId}</code> という子リソースがあります．
  56. 	この子リソースは，商品を識別するためのIDを表す <code>itemId</code> という
  57. 	パスパラメータがあるので，一意なリソース(商品)を特定することができます．<br>
  58. 	そして，最後に <code>inventory.{itemId}</code> リソースを親にしている，<code>inventory.{itemId}.count</code> という子リソースがあり，特定の商品の在庫数量を表しています．
  59. </p>
  60. <hr/>
  61.  
  62. <h2>InventoryManagementの仮想実行について</h2>
  63. <p>
  64. 	ここでは，InventoryManagementの仮想実行について説明します．InventoryManagementの仮想実行で用いるテストケースは次の通りです．<br>
  65. <ol>
  66. 	<li>inventoryに新しく取り扱う商品(Asahi)を100個入荷します．</li>
  67. 	<li>お客様が商品(Asahi)を50個購入してくれたので，在庫数が50個に減少しました．</li>
  68. </ol>
  69. </p>
  70.  
  71. <h3>仮想実行の可視化:</h3>
  72. <p>
  73. 	先ほどの仮想実行を可視化したものを以下に示していきます．<br>
  74. 	まず，システムの初期状態を可視化したものが以下の図です．
  75. </p>
  76.  
  77. <div class="img-center">
  78. 	<img src="../img/DTRAM/InventoryManagement/DTRAM 1 Ver InventoryManagement.png", class ="before-image-size"><br>
  79. </div>
  80. <p>
  81. 	初期状態のため，<code>inventory</code> リソースには何の商品も登録されていないという状態になっています．<br>
  82. 	次に，テストケースの１を実行していくので，<code>inventory</code> リソースをダブルクリックします．
  83. </p>
  84.  
  85. <div class="img-center">
  86. 	<img src="../img/DTRAM/InventoryManagement/DTRAM 2 Ver InventoryManagement.png", class ="before-image-size"><br>
  87. </div>
  88. <p>
  89. 	ダブルクリックすると，<code>registerItem</code> というメッセージが選択できるので，こちらを選択します．
  90. </p>
  91.  
  92. <div class="img-center">
  93. 	<img src="../img/DTRAM/InventoryManagement/DTRAM 3 Ver InventoryManagement.png", class ="before-image-size"><br>
  94. </div>
  95. <p>
  96. 	次に，<code>inventory</code> リソースに対して，商品のIDを表す <code>itemId</code> と
  97. 	商品名を表す <code>itemName</code>，入荷数量を表す <code>quantity</code> を入力できる画面が表示されます．
  98. </p>
  99.  
  100. <div class="img-center">
  101. 	<img src="../img/DTRAM/InventoryManagement/DTRAM 4 Ver Inventory Management.png", class ="before-image-size"><br>
  102. </div>
  103. <p>
  104. 	ここでは，<code>inventory</code> リソースに対して<code>registerItem(@123, "Asahi", 100)</code>というメッセージを入力し，実行します．
  105. </p>
  106.  
  107. <div class="img-center">
  108. 	<img src="../img/DTRAM/InventoryManagement/DTRAM 5 Ver Inventory Management.png", class ="before-image-size"><br>
  109. </div>
  110. <p>
  111. 	実行した結果，次の状態に遷移することができたので，固有のID(@123)の状態を持った<code>inventory.@123</code> と
  112. 	在庫数量が100の状態を持った<code>inventory.@123.count</code>，商品名がAsahiの状態を持った <code>inventory.@123.name</code> という
  113. 	３つのリソースが表示されました．<br>
  114. 	次に，テストケースの２を実行していきますので，<code>inventory.@123.count</code>リソースをダブルクリックします．
  115. </p>
  116.  
  117. <div class="img-center">
  118. 	<img src="../img/DTRAM/InventoryManagement/DTRAM 6 Ver Inventory Management.png", class ="before-image-size"><br>
  119. </div>
  120. <p>
  121. 	ダブルクリックすると，メッセージを選択する画面が先ほどと同様に表示されますので，出荷と入荷の両方を行うことができる <code>receiveOrShip</code> を選択します．
  122. </p>
  123.  
  124. <div class="img-center">
  125. 	<img src="../img/DTRAM/InventoryManagement/DTRAM 7 Ver Inventory Management.png", class ="before-image-size"><br>
  126. </div>
  127. <p>
  128. 	次に，出荷数量，または入荷数量を入力可能な画面が表示されますので，<strong><code>receiveOrShip(-50)</code></strong> と入力して実行します．
  129. </p>
  130.  
  131. <div class="img-center">
  132. 	<img src="../img/DTRAM/InventoryManagement/DTRAM 9 Ver Inventory Management.png", class ="before-image-size"><br>
  133. </div>
  134. <p>
  135. 	次の状態に遷移したため，<code>inventory.@123.name</code> リソースの状態が50に遷移したことが確認できました．
  136. </p>
  137. <hr/>
  138.  
  139. <h2>
  140. 	課題概要
  141. </h2>
  142. <p>
  143. 	本課題ではまず，上記にて説明を行ったInventoryManagementに，とある機能を追加した時のモデルと可視化の図を
  144. 	実験参加者の皆様に見て頂きます．<br>
  145. 	次に，その２つを見て<strong>どの様な機能が追加されたのか</strong>，また<strong>どの様なシナリオになっているのか</strong>を
  146. 	考えて頂き，以下のアンケートにお答えください．
  147. </p>
  148. <div style="padding: 10px; margin-bottom: 10px; border: 1px solid #333333; border-radius: 10px;">
  149. <pre>
  150. <c1>channel</c1> ItemRegistration {
  151. 	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})
  152. }
  153.  
  154. <c1>channel</c1> Receiving(itemId:<c1>Str</c1>) {
  155. 	out inventory.{itemId}.count(prev_quantity:<c1>Int</c1>, receive(quantity:<c1>Int</c1>)) = prev_quantity + quantity
  156. }
  157.  
  158. <c1>channel</c1> Shipping(itemId:<c1>Str</c1>) {
  159. 	out inventory.{itemId}.count(prev_quantity:<c1>Int</c1>, ship(quantity:<c1>Int</c1>)) = prev_quantity - quantity
  160. }
  161.  
  162. </pre>
  163. </div>
  164.  
  165. <div class="img-center">
  166. 	<img src="../img/Alloy/Alloy_Ver_InventoryManagementCheckMinus.png", class ="before-image-size"><br>
  167. </div>
  168.  
  169. <p>
  170. 	<strong>
  171. 		<a href="https://docs.google.com/forms/d/e/1FAIpQLSf5rIUfHnzsLMLPZ_KWnsukn3HcEGBSLN-BxzRPzqszyrlj8g/viewform?usp=sf_link" target="_blank" rel="noopener noreferrer">
  172. 			課題アンケート (別タブが開きます)
  173. 		</a>
  174. 	</strong>
  175. 	<br>
  176. 	<strong>
  177. 		<a href="https://docs.google.com/forms/d/e/1FAIpQLSf8Ex1RPzMRvyUYIRkCjcIY69fI74sNXK-m4rNAoAcR6_dm4g/viewform?usp=sf_link" target="_blank" rel="noopener noreferrer">
  178. 			課題終了後の評価アンケート (別タブが開きます)
  179. 		</a>
  180. 	</strong>
  181. </p>
  182.  
  183. <hr>
  184. <br>
  185. <a href="IM_DTRAM.html">【InventoryManagement(DTRAM)】へ</a>
  186. </body>
  187.  
  188. <style>
  189. 	.title{
  190. 		text-align: center;
  191. 	}
  192. 	.links-manual-A{
  193. 		display: flex;
  194. 		flex-direction: column;
  195. 	}
  196. 	.img-center{
  197. 		display: flex;
  198. 		justify-content: center;
  199. 		align-items: center;
  200. 	}
  201. 	.before-image-size{
  202. 		max-width: 100%;
  203. 		height: auto;
  204. 	}
  205. 	.after-image-size{
  206. 		max-width: 100%;
  207. 		height: auto;
  208. 	}
  209. </style>
  210.  
  211. </html>