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