【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

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


【InventoryManagement(DTRAM)】へ