【SimpleTwitter(DTRAM) の課題】

ここでは，SimpleTwitter の DTRAM による仕様記述に関する課題に取り組んでいただきます．
以下に DTRAM で記述された SimpleTwitter のモデルを示します．こちらを適宜参照しながら課題を進めてください．

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

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

DTRAM では，SimpleTwitter のモデルを以下のようなチャンネル単位で記述していきます．
アカウント登録用のイベントチャンネルを Signup，accountId で登録されているアカウントに対してツイートを行うためのイベントチャンネルを Tweet(accountId:Str) として宣言しています．

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

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

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 モデルの仮想実行について説明します．この仮想実行で用いるテストケースは次の通りです．

  1. accounts にアカウント名が "Satou" という新しいアカウントをアカウントid @123 で登録します．
  2. 登録したアカウント(Satou)で "Hello" というツイートを行います．

仮想実行の可視化:

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


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


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


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


ここでは，signUp("@123", "Satou") を入力します．


次の状態に遷移し，遷移後の状態が表示されます．@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
}

1:


2:


3:


4:


5:


課題アンケート (別タブが開きます)
課題終了後の評価アンケート (別タブが開きます)


【SimpleTwitter(Alloy)】へ