【SimpleTwitter(DTRAM)】

ここでは，SimpleTwitter の DTRAM による仕様記述に関する課題に取り組んでいただきます．
以下に DTRAM で記述された SimpleTwitter のモデルを示します．こちらを適宜参照しながら課題を進めてください．
DTRAM の説明をもう一度ご覧になりたい方はこちらへ(別タブが開きます)．

SimpleTwitter の DTRAM による記述についての説明

DTRAM では，SimpleTwitter の仕様を以下のような階層化されたリソースで表します．

Signup チャンネルでは accounts リソースが，メッセージ signUp(accountId, name) を受け取ると，リソースの状態が accountDB から insert(accountDB, accountId, {"name": name, "tweets": nil}) に変わることを示しています．nil は空のマップやリストを表しています．
ここで，関数 insert(x, y, z) は，写像 x に対し，キー y と値 z の対応を追加した結果得られる写像を返す関数です．また {"name": name, "tweets": nil} は，"name" と "tweets" をキーに持つ JSON オブジェクトを表しています．

Tweet(accountId:Str) チャンネルでは accounts.{accountId}.tweets リソースがメッセージ tweet(contents) を受け取ると，遷移前の状態 tweetList が append(tweetList, contents) に変わることを示しています．
ここで，関数 append(x, y) は，リスト x に対し，オブジェクト y を末尾に追加した結果得られるリストを返す関数です．

channel Signup {
	out accounts(accountDB:Map, signUp(accountId:Str, name:Str)) = insert(accountDB, accountId, {"name": name, "tweets": nil})
}

channel Tweet(accountId:Str) {
	out accounts.{accountId}.tweets(tweetList:List, tweet(contents:Str)) = append(tweetList, contents)
}

モデルの可視化

先ほどの SimpleTwitter のモデルのリソースとチャンネルを，DTRAM のモデリングツールを使用して可視化したものを以下の図に示します．

この図がモデルの実行に依らない，リソースとチャンネルの関係を表していることに注意して下さい．
図の中央にある accounts リソースは Signup チャンネルからアカウントを登録するメッセージを受け取ります．
accounts リソースの子リソースである，accounts.{accountId} リソースはアカウントを表しています．
このリソース名に含まれる accountId はアカウントidを表すパスパラメータで，一意なアカウントの特定を可能にしています．
accounts.{accountId} リソースの子リソースである accounts.{accountId}.tweets リソースは accounts.{accountId} のツイートリストを表しており， Tweet チャンネルからツイートを行うメッセージを受け取ります．

SimpleTwitter モデルの仮想実行について

ここでは，SimpleTwitter モデルの仮想実行について説明します．この仮想実行で用いるテストケースは次の通りです．

仮想実行の可視化:

シミュレーションツールを使用すると与えられたモデルに対して，任意の仮想実行を行うことができます．
ここでは上で示したテストケースに従って行った仮想実行を可視化したものを示していきます．まず，システムの初期状態を可視化したものが以下の図です．

初期状態では，accounts リソースには何のアカウントも登録されていない状態になっています．
次に，accounts にアカウント名が "Satou" のアカウントを登録するため，accounts リソースをダブルクリックします．

signUp というアカウントを登録するためのメッセージを選択します．

signUp メッセージのシグニチャが表示されます．
accountId はアカウントid，name はアカウント名を表します．

次の状態に遷移し，遷移後の状態が表示されます．@123というidを持つアカウント accounts.@123 が accounts の子リソースとして生成されていることがわかります．
accounts.@123 のツイートリスト accounts.@123.tweets が空のリスト(nil)，アカウント名 accounts.@123.name が "Satou" となっていることを確認できます．
次に，登録したアカウント accounts.@123 でツイートを行いたいので，accounts.@123.tweets リソースをダブルクリックします．

メッセージを選択する画面が同様に表示されますので，ツイートを行う tweet というメッセージを選択します．

ツイート内容の入力が可能な画面が表示されますので，ここでは tweet("Hello") と入力して実行します．

次の状態に遷移したため，Hello というツイート内容を持つツイート accounts.@123.tweets.0 が accounts.@123.tweets の子リソースとしてツイートリストの0番目に生成されていることが確認できました．

課題概要

ここからが課題です．
本課題ではまず，上記にて説明を行った SimpleTwitter の仕様に，ある機能を追加した仕様を考えます．
その仕様のモデルを以下に示します．また，そのモデルの仮想実行を可視化したものをその下に示します．これらの図を見ていただいた上で，２つの設問にお答えいただきます．
設問にお答えいただく際は，必ず設問１，設問２の順番でご解答下さい．以下の図と同じものが設問のページにも記載されているのでこのまま設問のページに飛んでいただいてもかまいません．

channel Signup {
	out accounts(accountDB:Map, signUp(accountId:Str, name:Str)) = insert(accountDB, accountId, {"name": name, "tweets": nil})
}

channel Tweet(accountId:Str) {
	out accounts.{accountId}.tweets(tweetList:List, tweet(contents:Str)) = append(tweetList, contents)
}

channel ChangeName(accountId:Str) {
	out accounts.{accountId}.name(prevNamr:Str, changeName(name:Str)) = name
}

【SimpleTwitter(DTRAM) の課題】

SimpleTwitter の DTRAM による記述についての説明

モデルの可視化

SimpleTwitter モデルの仮想実行について

仮想実行の可視化:

課題概要

1:

2:

3:

4:

5:

6:

7: