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 changeName[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 = acs.accountDB[id].tweets			
	}
}

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

run execute for 2 but 4 Accounts, 3 Account