【SimpleTwitter(Alloy) の課題】

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

SimpleTwitter の Alloy による仕様記述についての説明

sig:

Alloy では，アカウントidの集合を AccountId ，アカウント名の集合を Name ， ツイートの集合を Tweet ，アカウント全体の集合を Accounts ，アカウントの集合を Account，リストの集合を List で表します．
以下のモデルでは sig を用いて，AccountId ，Name ，Tweet ，Accounts，Account，List の順番にこれらの集合を宣言しています．
Accounts には，AccountId から Account への対応関係がaccountDB フィールドとして定義されています．
Account の宣言では，アカウント名を表す name が Name のインスタンスとして， ツイートリストを表す tweets が List のインスタンスとして定義されています．

pred:

最初の述語として記述されている init は，Accounts の インスタンスである acs が初期化されていることを示しています．
次のsignUp は，id に対応するアカウントを登録する前の Accounts のインスタンス acs と， 登録した後のインスタンス acs' の関係を述語として定義しています．
ここで n はアカウント名を示しています．
tweet ではid で登録されているアカウントに対してツイートを行った際の操作前の Accounts のインスタンス acs と， 操作後のインスタンス acs' の関係を述語として定義しています．
ここで contents はツイートの内容を表しています．
最後の execute では，init ，signUp ，tweet を この順で呼び出す操作を定義しています．
run では，execute を呼び出して仮想実行を行います． 

sig AccountId, Name, Tweet { }
sig Accounts {
	accountDB: AccountId lone -> lone Account
}
sig Account {
	name: Name,
	tweets: List
}

sig List {
	size: Int,
	element: Int -> lone Tweet
}

pred init[acs: Accounts] {
	no acs.accountDB
}

pred signUp[acs, acs': Accounts, id: AccountId, n: Name] {
	some ac: Account | {
		no id2: AccountId | acs.accountDB[id2] = ac
		acs'.accountDB = acs.accountDB + id -> ac
		ac.name = n
		ac.tweets.size = 0
		no ac.tweets.element
	}
}

pred tweet[acs, acs': Accounts, id: AccountId, contents: Tweet] {
	some ac': Account | {
		no id2: AccountId | acs.accountDB[id2] = ac'
		acs'.accountDB = acs.accountDB ++ id -> ac'
		ac'.name = acs.accountDB[id].name
		ac'.tweets != acs.accountDB[id].tweets
		ac'.tweets.size = plus[acs.accountDB[id].tweets.size, 1]
		ac'.tweets.element[minus[ac'.tweets.size, 1]] = contents
		all n: Int | n != minus[ac'.tweets.size, 1] implies ac'.tweets.element[n] = acs.accountDB[id].tweets.element[n]
	}
}

pred execute[] {
	some disj acs, acs', acs'': Accounts, id: AccountId, n: Name, contents: Tweet | {
		init[acs]
		signUp[acs, acs', id, n]
		tweet[acs', acs'', id, contents]
	}
}

run execute for 2 but 3 Accounts

モデルの可視化

先ほどの SimpleTwitter のモデルの構造を，Alloy の可視化ツールを使用して可視化したものを以下の図に示します．


この図がモデルの実行に依らない，モデルそのものが持つ構造を表していることに注意して下さい．
Accounts が，AccountId のインスタンスを Account のインスタンスに対応させる accountDB というフィールドを持っており， Account が Name のインスタンスを参照する name フィールドと，List のインスタンスを参照する tweets フィールドを，
List が Int のインスタンスを参照する sizeフィールドと， Int のインスタンスを element のインスタンスに対応させる Tweet フィールドをもっていることがわかります．

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

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

  1. Accounts に新しいアカウントを登録します．
  2. ツイートを行います．

仮想実行の可視化:

このテストケースはモデル中の execute 述語で実装されています．
execute の仮想実行を可視化したものを以下に示します．


左下にある Accounts2($execute_acs) は execute 述語中の変数 acs で参照される Accounts のインスタンスであり，init 述語を満たしているため， まだ何のアカウント(Account)も登録されていない状態になっています．
次に，1番上の段の左にある Accounts1($execute_acs') は変数 acs' で参照されるインスタンスで， acs で参照されるインスタンスに対して，AccountId で参照される Account のインスタンスをツイートリストの要素数が0の状態で登録したインスタンスになっています．
Accounts1 の右にある Accounts0($execute_acs'') は少し複雑です．
まず，Accounts1 において，AccountId で参照される Account のインスタンスは Account1 です．このインスタンスに対してツイートを行った後の Account のインスタンスは Account0 になります．
ここで Account0 のツイートリストの要素数が1に増加していることに注意して下さい．
AccountId で参照される Account のインスタンスが Account1 から Account0 に変わるので，Account のインスタンスも Account1 から Account0 に変わります．

課題概要

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

sig AccountId, Name, Tweet { }
sig Accounts {
    accountDB: AccountId lone -> lone Account
}
sig Account {
    name: Name,
    tweets: List
}

sig List {
    size: Int,
    element: Int -> lone Tweet
}

pred init[acs: Accounts] {
    no acs.accountDB
}

pred signUp[acs, acs': Accounts, id: AccountId, n: Name] {
	some ac': Account | acs.accountDB[id] = ac' implies {
		all id': AccountId | acs'.accountDB[id'] = acs.accountDB[id']
	}
	else {
		some ac: Account | {
			no id2: AccountId | acs.accountDB[id2] = ac
			acs'.accountDB = acs.accountDB + id -> ac
			ac.name = n
			ac.tweets.size = 0
			no ac.tweets.element
		}
	}
}

pred tweet[acs, acs': Accounts, id: AccountId, contents: Tweet] {
    some ac': Account | {
		no id2: AccountId | acs.accountDB[id2] = ac'
		acs'.accountDB = acs.accountDB ++ id -> ac'
		ac'.name = acs.accountDB[id].name
		ac'.tweets != acs.accountDB[id].tweets
		ac'.tweets.size = plus[acs.accountDB[id].tweets.size, 1]
		ac'.tweets.element[minus[ac'.tweets.size, 1]] = contents
		all n: Int | n != minus[ac'.tweets.size, 1] implies ac'.tweets.element[n] = acs.accountDB[id].tweets.element[n]
	}
}

pred execute[] {
	some disj acs, acs', acs'', acs''': Accounts, id: AccountId, disj n, n': Name, contents: Tweet | {
		init[acs]
		signUp[acs, acs', id, n]
		signUp[acs', acs'', id, n']
		tweet[acs'', acs''', id, contents]
	}
}

run execute for 2 but 4 Accounts

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


【SimpleTwitter(DTRAM)】へ