Fork: 0
nitta-lab / SpecificationSimulatorExperiments
Transfer to URL with SHA Find file
Newer
Older
SpecificationSimulatorExperiments / courseA / ST_DTRAM.html
okazakitakehiro on 9 Sep 10 KB IM_DTRAMの修正とST_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>【SimpleTwitter(DTRAM)】</title>
  15. </head>
  16. <body>
  17. <h1 class="title">
  18. 	【SimpleTwitter(DTRAM)の課題】
  19. </h1>
  20. <p>
  21. 	ここでは，SimpleTwitterのDTRAMによる仕様記述に関する課題に取り組んでいただきます．<br>
  22. 	以下にDTRAMで記述されたSimpleTwitterのモデルを示します．こちらを適宜参照しながらモデルの理解を行ってください．
  23. </p>
  24. <hr/>
  25.  
  26. <h2>SimpleTwitterのDTRAMによる記述についての説明</h2>
  27. <p>
  28. 	DTRAMでは，SimpleTwitter の仕様を以下のような階層化されたリソースで表します．<br>
  29. <ul>
  30. 	<li><code>accounts</code>: アカウント全体を管理</li>
  31. 	<li><code>accounts.{accountId}</code>: <code>accountId</code> で登録されているアカウント</li>
  32. 	<li><code>accounts.{accountId}.name</code>: <code>accountId</code> で示されたアカウント名</li>
  33. 	<li><code>accounts.{accountId}.tweets</code>: <code>accountId</code> で示されたアカウントのツイートリスト</li>
  34. 	<li><code>accounts.{accountId}.tweets.{tid}</code>: <code>accountId</code> で示されたアカウントが持つツイートリストに <code>tid</code> で登録されているツイート</li>
  35. </ul>
  36.  
  37. DTRAMでは，SimpleTwitterのモデルを以下のようなチャンネル単位で記述していきます．<br>
  38. ここでは，アカウント登録用のイベントチャンネルを <code>Signup</code> ，<code>accountId</code> で登録されているアカウントに対してツイートを行うためのイベントチャンネルを <code>Tweet(accountId:<c1>Str</c1>)</code> として宣言しています．<br>
  39. <code>Signup</code> チャンネルでは <code>accounts</code> リソースが，メッセージ <code>signup(accountId, name)</code> を受け取ると， リソースの状態 <code>accountDB</code> が <code>insert(accountDB, accountId, {"name": itemName, "tweets": nil})</code> に変わることを示しています．<code>nil</code> は空のマップやリストを表しています．<br>
  40. ここで，<code>insert()</code> 関数は，第1引数に渡された写像に対し，第2引数と第3引数の対応を追加した結果得られる写像を返す関数です．<br>
  41. <code>Tweet(accountId:<c1>Str</c1>)</code> チャンネルでは <code>accounts.{accountId}.tweets</code> リソースがメッセージ <code>tweet(contents)</code> を受け取ると，
  42. 遷移前の状態 <code>tweetList</code> が <code>append(tweetList, contents)</code> に変わることを示しています．<br>
  43. ここで，<code>append()</code> 関数は，第1引数に渡された写像に対し，第2引数の対応を追加した結果得られる写像を返す関数です．<br>
  44. </p>
  45.  
  46. <div style="padding: 10px; margin-bottom: 10px; border: 1px solid #333333; border-radius: 10px;">
  47. 	<pre>
  48. <c1>channel</c1> Signup {
  49. 	<c1>out</c1> accounts(accountDB:<c1>Map</c1>, signUp(accountId:<c1>Str</c1>, name:<c1>Str</c1>)) = insert(accountDB, accountId, {"name": name, "tweets": nil})
  50. }
  51.  
  52. <c1>channel</c1> Tweet(accountId:<c1>Str</c1>) {
  53. 	<c1>out</c1> accounts.{accountId}.tweets(tweetList:<c1>List</c1>, tweet(contents:<c1>Str</c1>)) = append(tweetList, contents)
  54. }
  55. 	</pre>
  56. </div>
  57. <hr/>
  58.  
  59. <h2>モデルの可視化</h2>
  60. <p>
  61. 	先ほどのSimpleTwitterのモデルのリソースとチャンネルを，DTRAMのモデリングツールを使用して可視化したものを以下の図に示します．<br>
  62. </p>
  63. <div class="img-center">
  64. 	<img src="../img/DTRAM/SimpleTwitter/DTRAM Ver SimpleTwitter architecture Visualize.png", class ="before-image-size"><br>
  65. </div>
  66. <p>
  67. 	この図がモデルの実行に依らない，リソースを表していることに注意して下さい．<br>
  68. 	図の中央にある <code>accounts</code> リソースは <code>Signup</code> チャンネルからアカウントを登録するメッセージを受け取ります．<br>
  69. 	<code>accounts</code> リソースの子リソースである，<code>accounts.{accountId}</code> リソースはアカウントを表しています．<br>
  70. 	リソース名に含まれる <code>accountId</code> はアカウントIDを表すパスパラメータで，一意なアカウントの特定を可能にしています．<br>
  71. 	<code>accounts.{accountId}</code> リソースの子リソースである <code>accounts.{accountId}.tweets</code> リソースは<code>accounts.{accountId}</code> のツイートリストを表しており，
  72. 	<code>Tweet</code> チャンネルからツイートを行うメッセージを受け取ります．
  73. </p>
  74. <hr/>
  75.  
  76. <h2>SimpleTwitterモデルの仮想実行について</h2>
  77. <p>
  78. 	ここでは，SimpleTwitterモデルの仮想実行について説明します．この仮想実行で用いるテストケースは次の通りです．<br>
  79. <ol>
  80. 	<li>accountsにアカウント名がSatouという新しいアカウントを登録します．</li>
  81. 	<li>登録したアカウント(アカウント名：Satou)で Hello という内容のツイートを行います．</li>
  82. </ol>
  83. </p>
  84.  
  85. <h3>仮想実行の可視化:</h3>
  86. <p>
  87. 	シミュレーションツールを使用すると与えられたモデルに対して，任意の仮想実行を行うことができます．<br>
  88. 	ここでは上で示したテストケースに従って行った仮想実行を可視化したものを示していきます．まず，システムの初期状態を可視化したものが以下の図です．
  89. </p>
  90.  
  91. <div class="img-center">
  92. 	<img src="../img/DTRAM/SimpleTwitter/DTRAM 1 VerSimpleTwitter.png", class ="before-image-size"><br>
  93. </div>
  94. <p>
  95. 	初期状態では，<code>accounts</code> リソースには何のアカウントも登録されていない状態になっています．<br>
  96. 	次に，<code>accounts</code> にアカウント名が Satou のアカウントを登録するため，<code>accounts</code> リソースをダブルクリックします．
  97. </p>
  98.  
  99. <div class="img-center">
  100. 	<img src="../img/DTRAM/SimpleTwitter/DTRAM 2 VerSimpleTwitter.png", class ="before-image-size"><br>
  101. </div>
  102. <p>
  103. 	<strong><code>signUp</code></strong> というアカウントを登録するためのメッセージを選択します．
  104. </p>
  105.  
  106. <div class="img-center">
  107. 	<img src="../img/DTRAM/SimpleTwitter/DTRAM 3 VerSimpleTwitter.png", class ="before-image-size"><br>
  108. </div>
  109. <p>
  110. 	<code>signUp</code> メッセージのシグニチャが表示されます．<br>
  111. 	<code>accountId</code> はアカウントID，<code>name</code> はアカウント名を表します．
  112. </p>
  113.  
  114. <div class="img-center">
  115. 	<img src="../img/DTRAM/SimpleTwitter/DTRAM 4 VerSimpleTwitter.png", class ="before-image-size"><br>
  116. </div>
  117. <p>
  118. 	ここでは，<code>signUp("@123", "Satou")</code> を入力します．
  119. </p>
  120.  
  121. <div class="img-center">
  122. 	<img src="../img/DTRAM/SimpleTwitter/DTRAM 5 VerSimpleTwitter.png", class ="before-image-size"><br>
  123. </div>
  124. <p>
  125. 	次の状態に遷移し，遷移後の状態が表示されます．@123というidを持つアカウント <code>accounts.@123</code> が <code>accounts</code> の子リソースとして生成されていることがわかります．<br>
  126. 	<code>accounts.@123</code> のツイートリスト <code>accounts.@123.tweets</code> が 空のリスト(nill)，アカウント名 <code>accounts.@123.name</code> が Satouとなっていることを確認できます．<br>
  127. 	次に，登録したアカウント <code>accounts.@123</code> でツイートを行いたいので，<code>accounts.@123.tweets</code> リソースをダブルクリックします．
  128. </p>
  129.  
  130. <div class="img-center">
  131. 	<img src="../img/DTRAM/SimpleTwitter/DTRAM 6 VerSimpleTwitter.png", class ="before-image-size"><br>
  132. </div>
  133. <p>
  134. 	メッセージを選択する画面が同様に表示されますので，ツイートを行う <strong><code>tweet</code></strong> というメッセージを選択します．
  135. </p>
  136.  
  137. <div class="img-center">
  138. 	<img src="../img/DTRAM/SimpleTwitter/DTRAM 7 VerSimpleTwitter.png", class ="before-image-size"><br>
  139. </div>
  140. <p>
  141. 	ツイート内容の入力が可能な画面が表示されますので，ここでは <code>tweet("Hello")</code> と入力して実行します．<br>
  142. </p>
  143.  
  144. <div class="img-center">
  145. 	<img src="../img/DTRAM/SimpleTwitter/DTRAM 9 VerSimpleTwitter.png", class ="before-image-size"><br>
  146. </div>
  147. <p>
  148. 	次の状態に遷移したため，Hello というツイート内容を持つツイート <code>accounts.@123.tweets.0</code> が <code>accounts.@123.tweets</code> の子リソースとしてツイートリストの0番目に生成されていることが確認できました．
  149. </p>
  150. <hr/>
  151.  
  152. <h2>
  153. 	課題概要
  154. </h2>
  155. <p>
  156. 	本課題ではまず，上記にて説明を行った <code>SimpleTwitter</code> の仕様に，ある機能を追加した仕様を考えます．<br>
  157. 	その仕様のモデルと，仮想実行の流れを可視化した以下の図を見ていただいた上で，２つの設問にお答えいただきます．<br>
  158. 	設問にお答えいただく際は，必ず設問１，設問２の順番でご解答下さい．以下の図と同じものが設問のページにも記載されているのでこのまま設問のページに飛んでいただいてもかまいません．
  159. </p>
  160. <div style="padding: 10px; margin-bottom: 10px; border: 1px solid #333333; border-radius: 10px;">
  161. <pre>
  162. <c1>channel</c1> Signup {
  163. 	<c1>out</c1> accounts(accountDB:<c1>Map</c1>, signUp(accountId:<c1>Str</c1>, name:<c1>Str</c1>)) = insert(accountDB, accountId, {"name": name, "tweets": nil})
  164. }
  165.  
  166. <c1>channel</c1> Tweet(accountId:<c1>Str</c1>) {
  167. 	<c1>out</c1> accounts.{accountId}.tweets(tweetList:<c1>List</c1>, tweet(contents:<c1>Str</c1>)) = append(tweetList, contents)
  168. }
  169.  
  170. <c1>channel</c1> ChangeName(accountId:<c1>Str</c1>) {
  171. 	<c1>out</c1> accounts.{accountId}.name(prevNamr:<c1>Str</c1>, changeName(name:<c1>Str</c1>)) = name
  172. }
  173.  
  174.  
  175. </pre>
  176. </div>
  177.  
  178. <h3>1:</h3>
  179. <div class="img-center">
  180. 	<img src="../img/DTRAM/SimpleTwitter/DTRAM 5 VerSimpleTwitter.png", class ="before-image-size"><br>
  181. </div>
  182. <h3>2:</h3>
  183. <div class="img-center">
  184. 	<img src="../img/DTRAM/SimpleTwitter/ChangeName/DTRAM_1_ChangeName_VerSimpleTwitter.png", class ="before-image-size"><br>
  185. </div>
  186.  
  187. <p>
  188. 	<strong>
  189. 		<a href="https://docs.google.com/forms/d/e/1FAIpQLSf5rIUfHnzsLMLPZ_KWnsukn3HcEGBSLN-BxzRPzqszyrlj8g/viewform?usp=sf_link" target="_blank" rel="noopener noreferrer">
  190. 			課題アンケート (別タブが開きます)
  191. 		</a>
  192. 	</strong>
  193. 	<br>
  194. 	<strong>
  195. 		<a href="https://docs.google.com/forms/d/e/1FAIpQLSf8Ex1RPzMRvyUYIRkCjcIY69fI74sNXK-m4rNAoAcR6_dm4g/viewform?usp=sf_link" target="_blank" rel="noopener noreferrer">
  196. 			課題終了後の評価アンケート (別タブが開きます)
  197. 		</a>
  198. 	</strong>
  199. </p>
  200.  
  201. <hr>
  202. <br>
  203. <a href="IM_DTRAM.html">【InventoryManagement(DTRAM)】へ</a>
  204. </body>
  205.  
  206. <style>
  207. 	.title{
  208. 		text-align: center;
  209. 	}
  210. 	.links-manual-A{
  211. 		display: flex;
  212. 		flex-direction: column;
  213. 	}
  214. 	.img-center{
  215. 		display: flex;
  216. 		justify-content: center;
  217. 		align-items: center;
  218. 	}
  219. 	.before-image-size{
  220. 		max-width: 100%;
  221. 		height: auto;
  222. 	}
  223. 	.after-image-size{
  224. 		max-width: 100%;
  225. 		height: auto;
  226. 	}
  227. </style>
  228.  
  229. </html>