Fork: 0
nitta-lab / SpecificationSimulatorExperiments
Transfer to URL with SHA Find file
Newer
Older
SpecificationSimulatorExperiments / courseC / IM_DTRAM_C.html
Naoya Nitta on 12 Sep 12 KB Alloy と 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. 	ここでは，InventoryManagement の DTRAM による仕様記述に関する課題に取り組んでいただきます．<br>
  22. 	以下に DTRAM で記述された InventoryManagement のモデルを示します．こちらを適宜参照しながら課題を進めてください．
  23. </p>
  24. <hr/>
  25.  
  26. <h2>InventoryManagement の DTRAM による記述についての説明</h2>
  27. <p>
  28. 	DTRAMでは，InventoryManagement の仕様を以下のような階層化されたリソースで表します．<br>
  29. 	<ul>
  30. 		<li><code>inventory</code>：全商品を保管する倉庫</li>
  31. 		<li><code>inventory.{itemId}</code>：<code>itemId</code> で登録されている商品</li>
  32. 		<li><code>inventory.{itemId}.count</code>：<code>itemId</code> で登録されている商品の在庫数</li>
  33. 		<li><code>inventory.{itemId}.name</code>：<code>itemId</code> で登録されている商品の商品名</li>
  34. 	</ul>
  35.  
  36. 	DTRAM では，InventoryManagement のモデルを以下のようなチャンネル単位で記述していきます．<br>
  37. 	商品登録用のイベントチャンネルを <code>ItemRegistration</code> ，<code>itemId</code> で登録されている商品に対して入荷か出荷を行うためのイベントチャンネルを <code>ReceivingOrShipping(itemId:<c1>Str</c1>)</code> として宣言しています．<br>
  38. </p>
  39. <p>
  40. 	<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>
  41. 	ここで，関数 <code>insert(x, y, z)</code> は，写像 <code>x</code> に対し，キー <code>y</code> と値 <code>z</code> の対応を追加した結果得られる写像を返す関数です．<br>
  42. 	また <code>{"count": quantity, "name": itemName}</code> は，<code>"count"</code> と <code>"name"</code> をキーに持つ JSON オブジェクトを表しています．<br>
  43. </p>
  44. <p>
  45. 	<code>ReceivingOrShipping(itemId:<c1>Str</c1>)</code> チャンネルでは <code>inventory.{itemId}.count</code> リソースがメッセージ <code>receiveOrShip(quantity)</code> を受け取ると，
  46. 	遷移前の状態 <code>prev_quantity</code> が <code>prev_quantity + quantity</code> に変わることを示しています．<br>
  47. </p>
  48.  
  49. <div style="padding: 10px; margin-bottom: 10px; border: 1px solid #333333; border-radius: 10px;">
  50. 	<pre>
  51. <c1>channel</c1> ItemRegistration {
  52. 	<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})
  53. }
  54.  
  55. <c1>channel</c1> ReceivingOrShipping(itemId:<c1>Str</c1>) {
  56. 	<c1>out</c1> inventory.{itemId}.count(prev_quantity:<c1>Int</c1>, receiveOrShip(quantity:<c1>Int</c1>)) = prev_quantity + quantity
  57. }
  58. 	</pre>
  59. </div>
  60. <hr/>
  61.  
  62. <h2>モデルの可視化</h2>
  63. <p>
  64. 	先ほどの InventoryManagement のモデルのリソースとチャンネルを，DTRAM のモデリングツールを使用して可視化したものを以下の図に示します．<br>
  65. </p>
  66. <div class="img-center">
  67. 	<img src="../img/DTRAM/InventoryManagement/DTRAM Ver InventoryManagement architecture Visualize.png", class ="before-image-size"><br>
  68. </div>
  69. <p>
  70. 	この図がモデルの実行に依らない，リソースとチャンネルの関係を表していることに注意して下さい．<br>
  71. 	図の中央にある <code>inventory</code> リソースは <code>ItemRegistration</code> チャンネルから商品を登録するメッセージを受け取ります．<br>
  72. 	<code>inventory</code> リソースの子リソースである，<code>inventory.{itemId}</code> リソースは商品を表しています．<br>
  73. 	このリソース名に含まれる <code>itemId</code> は商品idを表すパスパラメータで，一意な商品の特定を可能にしています．<br>
  74. 	<code>inventory.{itemId}</code> リソースの子リソースである <code>inventory.{itemId}.count</code> リソースは <code>inventory.{itemId}</code> の在庫数を表しており，
  75. 	<code>ReceivingOrShipping</code> チャンネルから入荷もしくは出荷を行うメッセージを受け取ります．
  76. </p>
  77. <hr/>
  78.  
  79. <h2>InventoryManagement モデルの仮想実行について</h2>
  80. <p>
  81. 	ここでは，InventoryManagement モデルの仮想実行について説明します．この仮想実行で用いるテストケースは次の通りです．<br>
  82. <ol>
  83. 	<li>inventory に新しく取り扱う商品(Asahi)を初期数量100で登録します．</li>
  84. 	<li>登録した商品(Asahi)を50個出荷します．</li>
  85. </ol>
  86. </p>
  87.  
  88. <h3>仮想実行の可視化:</h3>
  89. <p>
  90. 	シミュレーションツールを使用すると与えられたモデルに対して，任意の仮想実行を行うことができます．<br>
  91. 	ここでは上で示したテストケースに従って行った仮想実行を可視化したものを示していきます．まず，システムの初期状態を可視化したものが以下の図です．
  92. </p>
  93.  
  94. <div class="img-center">
  95. 	<img src="../img/DTRAM/InventoryManagement/DTRAM 1 Ver InventoryManagement.png", class ="before-image-size"><br>
  96. </div>
  97. <p>
  98. 	初期状態では，<code>inventory</code> リソースには何の商品も登録されていない状態になっています．<code>nil</code> は空のマップやリストを表しています．<br>
  99. 	次に，<code>inventory</code> に商品(Asahi)を登録するため，<code>inventory</code> リソースをダブルクリックします．
  100. </p>
  101.  
  102. <div class="img-center">
  103. 	<img src="../img/DTRAM/InventoryManagement/DTRAM 2 Ver InventoryManagement.png", class ="before-image-size"><br>
  104. </div>
  105. <p>
  106. 	<strong><code>registerItem</code></strong> という商品を登録するためのメッセージを選択します．
  107. </p>
  108.  
  109. <div class="img-center">
  110. 	<img src="../img/DTRAM/InventoryManagement/DTRAM 3 Ver InventoryManagement.png", class ="before-image-size"><br>
  111. </div>
  112. <p>
  113. 	<code>registerItem</code> メッセージのシグニチャが表示されます．<br>
  114. 	<code>itemId</code> は商品id，<code>itemName</code> は商品名 ，<code>quantity</code> は初期数量を表します．
  115. </p>
  116.  
  117. <div class="img-center">
  118. 	<img src="../img/DTRAM/InventoryManagement/DTRAM 4 Ver Inventory Management.png", class ="before-image-size"><br>
  119. </div>
  120. <p>
  121. 	ここでは，<code>registerItem("@123", "Asahi", 100)</code> を入力します．
  122. </p>
  123.  
  124. <div class="img-center">
  125. 	<img src="../img/DTRAM/InventoryManagement/DTRAM 5 Ver Inventory Management.png", class ="before-image-size"><br>
  126. </div>
  127. <p>
  128. 	次の状態に遷移し，遷移後の状態が表示されます．@123というidを持つ商品 <code>inventory.@123</code> が <code>inventory</code> の子リソースとして生成されていることがわかります．<br>
  129. 	<code>inventory.@123</code> の在庫数量 <code>inventory.@123.count</code> が100，商品名 <code>inventory.@123.name</code> がAsahiとなっていることを確認できます．<br>
  130. 	次に，登録した商品 <code>inventory.@123</code> を50個出荷したいので，<code>inventory.@123.count</code> リソースをダブルクリックします．
  131. </p>
  132.  
  133. <div class="img-center">
  134. 	<img src="../img/DTRAM/InventoryManagement/DTRAM 6 Ver Inventory Management.png", class ="before-image-size"><br>
  135. </div>
  136. <p>
  137. 	メッセージを選択する画面が同様に表示されますので，入荷か出荷を行う <strong><code>receiveOrShip</code></strong> というメッセージを選択します．
  138. </p>
  139.  
  140. <div class="img-center">
  141. 	<img src="../img/DTRAM/InventoryManagement/DTRAM 7 Ver Inventory Management.png", class ="before-image-size"><br>
  142. </div>
  143. <p>
  144. 	入荷数量，または出荷数量の入力が可能な画面が表示されますので，ここでは <code>receiveOrShip(-50)</code> と入力して実行します．<br>
  145. 	ここで quantity が正の値のときは入荷，負の値のときは出荷が行われます．
  146. </p>
  147.  
  148. <div class="img-center">
  149. 	<img src="../img/DTRAM/InventoryManagement/DTRAM 9 Ver Inventory Management.png", class ="before-image-size"><br>
  150. </div>
  151. <p>
  152. 	次の状態に遷移したため，<code>inventory.@123.count</code> リソースの状態が50に遷移したことが確認できました．
  153. </p>
  154. <hr/>
  155.  
  156. <h2>
  157. 	課題概要
  158. </h2>
  159. <p>
  160. 	ここからが課題です．<br>
  161. 	本課題ではまず，上記にて説明を行った <code>InventoryManagement</code> の仕様に，ある機能を追加した仕様を考えます．<br>
  162. 	その仕様のモデルを以下に示します．また，そのモデルの仮想実行を可視化したものをその下に示します．これらの図を見ていただいた上で，２つの設問にお答えいただきます．<br>
  163. 	なお，以下のモデル中にある関数 <code>if(x, y, z)</code> は，<code>x</code> が <code>true</code> のときは <code>y</code> を返し，<code>false</code> のときは <code>z</code> を返します．<br>
  164. 	設問にお答えいただく際は，必ず設問１，設問２の順番でご解答下さい．以下の図と同じものが設問のページにも記載されているのでこのまま設問のページに飛んでいただいてもかまいません．
  165. </p>
  166. <div style="padding: 10px; margin-bottom: 10px; border: 1px solid #333333; border-radius: 10px;">
  167. <pre>
  168. <c1>channel</c1> ItemRegistration {
  169. 	<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})
  170. }
  171.  
  172. <c1>channel</c1> ReceivingOrShipping(itemId:<c1>Str</c1>) {
  173. 	<div style="background-color:#EDF7FF;">	<c1>out</c1> inventory.{itemId}.count(prev_quantity:<c1>Int</c1>, receiveOrShip(quantity:<c1>Int</c1>)) = if(prev_quantity + quantity >= 0, prev_quantity + quantity, prev_quantity)</div>
  174. }
  175. </pre>
  176. </div>
  177.  
  178. <h3>1:</h3>
  179. <div class="img-center">
  180. 	<img src="../img/DTRAM/InventoryManagement/DTRAM 1 Ver InventoryManagement.png", class ="before-image-size"><br>
  181. </div>
  182. <h3>2:</h3>
  183. <div class="img-center">
  184. 	<img src="../img/DTRAM/InventoryManagement/DTRAM 4 Ver Inventory Management.png" , class ="before-image-size"><br>
  185. </div>
  186. <h3>3:</h3>
  187. <div class="img-center">
  188. 	<img src="../img/DTRAM/InventoryManagement/DTRAM 5 Ver Inventory Management.png", class ="before-image-size"><br>
  189. </div>
  190. <h3>4:</h3>
  191. <div class="img-center">
  192. 	<img src="../img/DTRAM/InventoryManagement/CheckMinus/DTRAM_kadai4_Ver_InventoryManagement.png" , class ="before-image-size"><br>
  193. </div>
  194. <h3>5:</h3>
  195. <div class="img-center">
  196. 	<img src="../img/DTRAM/InventoryManagement/DTRAM 9 Ver Inventory Management.png", class ="before-image-size"><br>
  197. </div>
  198. <h3>6:</h3>
  199. <div class="img-center">
  200. 	<img src="../img/DTRAM/InventoryManagement/CheckMinus/DTRAM_kadai6_Ver_InventoryManagement.png" , class ="before-image-size"><br>
  201. </div>
  202. <h3>7:</h3>
  203. <div class="img-center">
  204. 	<img src="../img/DTRAM/InventoryManagement/DTRAM 9 Ver Inventory Management.png", class ="before-image-size"><br>
  205. </div>
  206.  
  207. <p>
  208. 	<strong>
  209. 		<a href="https://docs.google.com/forms/d/e/1FAIpQLScOaQl6oVFSc6Ygxa89YCtzgL5Bv5XJyGkJLp3gq24seZ91YA/viewform" target="_blank" rel="noopener noreferrer">
  210. 			設問１ (別タブが開きます)
  211. 		</a>
  212. 	</strong>
  213. 	<br>
  214. 	<strong>
  215. 		<a href="https://docs.google.com/forms/d/e/1FAIpQLSfgK_6VWFym_qBugyf5Rr1VsPwTR6BTVecxg9BhFxliRyCnlw/viewform" target="_blank" rel="noopener noreferrer">
  216. 			設問２ (別タブが開きます)
  217. 		</a>
  218. 	</strong>
  219. 	<br>
  220. 	<strong>
  221. 		<a href="https://docs.google.com/forms/d/e/1FAIpQLScjxIDaCeqBxYq3-YduI1PXxH58MqFYeek8nxXftcz-UAeNfA/viewform" target="_blank" rel="noopener noreferrer">
  222. 			課題評価アンケート (別タブが開きます)
  223. 		</a>
  224. 	</strong>
  225. </p>
  226.  
  227. <hr>
  228. <br>
  229. <a href="Alloy.html">【Alloy の概要説明】へ</a>
  230. </body>
  231.  
  232. <style>
  233. 	.title{
  234. 		text-align: center;
  235. 	}
  236. 	.links-manual-A{
  237. 		display: flex;
  238. 		flex-direction: column;
  239. 	}
  240. 	.img-center{
  241. 		display: flex;
  242. 		justify-content: center;
  243. 		align-items: center;
  244. 	}
  245. 	.before-image-size{
  246. 		max-width: 100%;
  247. 		height: auto;
  248. 	}
  249. 	.after-image-size{
  250. 		max-width: 100%;
  251. 		height: auto;
  252. 	}
  253. </style>
  254.  
  255. </html>