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