【SimpleTwitter(DTRAM) の課題】

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

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

  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 の仕様に，ある機能を追加した仕様を考えます．
その仕様のモデルを以下に示します．また，そのモデルの仮想実行を可視化したものをその下に示します．これらの図を見ていただいた上で，２つの設問にお答えいただきます．
なお，以下のモデル中にある関数 if(x, y, z) は，x が true のときは y を返し，false のときは z を返します． また関数 contains(x, y) は，写像 x のキーとして y が含まれているときは true を，そうでないときは false を返します．
設問にお答えいただく際は，必ず設問１，設問２の順番でご解答下さい．以下の図と同じものが設問のページにも記載されているのでこのまま設問のページに飛んでいただいてもかまいません． 

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

}

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

1:


2:


3:


4:


5:


6:


7:


設問１ (別タブが開きます)
設問２ (別タブが開きます)
課題評価アンケート (別タブが開きます)


【SimpleTwitter(Alloy)】へ