【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 フィールドとして定義されています．
ここで，AccountId の右側の lone は１つの Account に対応する AccountId がたかだか１つしかないことを示しています．

Account の宣言では，アカウント名を表す name が Name のインスタンスとして， ツイートリストを表す tweets が List のインスタンスとして定義されています．

pred:

最初の述語として記述されている init は，Accounts の インスタンスである acs が初期化されていることを示しています．

次の signUp は，id に対応するアカウントを登録する前の Accounts のインスタンス acs と， 登録した後のインスタンス acs' の関係を述語として定義しています．ここで n はアカウント名を示しています．
また，述語定義中の some ac: Account は，acs のデータベースに登録されていない Account のインスタンス (ac) が存在していることを示しており， 直観的には Account のインスタンスが生成されたことを示しています．

tweet ではid で登録されているアカウントに対してツイートを行った際の操作前の Accounts のインスタンス acs と， 操作後のインスタンス acs' の関係を述語として定義しています．ここで contents はツイートの内容を表しています．
述語定義中の some ac': Account は，acs のデータベースに登録されていない Account のインスタンス (ac') が存在していることを示しており， 直観的には Account のインスタンスが，ツイートを行うことによって複製されたことを示しています．
また implies は，その前に記述されている条件が成り立っているときは，その後に記述されている論理式または論理式の集合が成り立ち，条件が成り立っていないときは else の後ろに記述されている論理式または論理式の集合が成り立つことを示しています．

最後の 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 のインスタンスを Tweet のインスタンスに対応させる element フィールドをもっていることがわかります．

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

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

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

仮想実行の可視化:

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

左下にある Accounts2($execute_acs) は execute 述語中の変数 acs で参照される Accounts のインスタンスであり，init 述語を満たしているため， まだ何のアカウント(Account)も登録されていない状態になっています．

次に，1番上の段の左にある Accounts1($execute_acs') は変数 acs' で参照される Account のインスタンスで， acs で参照される Account のインスタンスに対して，Account のインスタンス Account1($signUp_ac) をツイートリストの要素数が0の状態で登録したインスタンスになっています．

Accounts1 の右にある Accounts0($execute_acs'') は少し複雑です．
まず，Accounts1 において，AccountId で参照される Account のインスタンスは Account1 です．このインスタンスに対してツイートを行った後の Account のインスタンスは Account0 になります．
ここで Account0 のツイートリストの要素数が1に増加していることに注意して下さい．
AccountId で参照される Account のインスタンスが Account1 から Account0 に変わるので，Accounts のインスタンスも Accounts1 から Accounts0 に変わります．

課題概要

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

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

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