infin.ele

-- signatures
sig Company {
	var users: set User,
	var invoices: set Invoice,
	var categories: set Category,
	var tags: set Tag
} 
var sig Registered in Company {}

sig User {}
sig Tag {}
sig Budget {} 

sig Category {
	var budget: lone Budget
} 


sig Invoice {
	var company: one Company,
	var category: one Category,
	var tags: set Tag
}

-- preds
pred emptyCompany[c : Company] {
	one c

	no c.tags 
	no c.categories
	no c.categories.budget -- redundant 
	no c.users 
	no c.invoices
}

pred emptyInvoice[i : Invoice] {
	one i

	no i.company
	no i.category
	no i.tags
}

pred emptyCategory[cat : Category] {
	one cat
	
	no cat.budget
}

pred userRegistered[u : User] {
	one u
	some c : Registered | u in c.users
}

pred companyRegistered[c : Company] {
	one c
	c in Registered
}

pred invoiceProcessed[i : Invoice] {
	one i
	some c : Registered | i in c.invoices
}

pred categoryRegistered[cat : Category] {
	one cat
	some c : Registered | cat in c.categories
}

pred companyCategory[cat : Category, c : Company] {
	one cat
 	cat in c.categories
}

pred tagsRegistered[t : Tag] {
	some c : Registered | t in c.tags
}

pred companyTags[t : Tag, c : Company] {
 	t in c.tags
}

-- actions
pred sameUsers {
	all c : Company | c.users' = c.users
}

pred sameInvoices {
	all c : Company | c.invoices' = c.invoices
	all c : Company | all i : c.invoices | i.company' = i.company and
				                        i.category' = i.category and
								i.tags' = i.tags
}

pred sameCategories {
	all c : Company | c.categories' = c.categories
}

pred sameTags {
	all c : Company | c.tags' = c.tags
}

pred sameBudgets {
	all cat : Category | cat.budget' = cat.budget
}

pred sameRegistered {
	Registered' = Registered
}

pred stutter {
	sameUsers
	sameInvoices
	sameCategories
	sameTags
	sameRegistered
	sameBudgets
}	

pred registerUser[u : User, c : Company] {
	emptyCompany[c]
	not companyRegistered[c]
	not userRegistered[u]
	
	c.users' = c.users + u
	Registered' = Registered + c
	
	sameInvoices
	sameCategories
	sameTags
	sameBudgets
	all c0 : Company | c != c0 implies c.users' = c.users
}

pred addUserToCompany[u : User, c : Company] {
	not userRegistered[u]
	companyRegistered[c]

	c.users' = c.users + u
	
	sameInvoices
	sameCategories
	sameTags
	sameBudgets
	sameRegistered
	all c0 : Company | c != c0 implies c0.users' = c0.users
}

pred addInvoiceToCompany[i : Invoice, c : Company, cat : Category, t : Tag] {
	companyRegistered[c]
	not invoiceProcessed[i]
	emptyInvoice[i]
	companyCategory[cat, c]
	companyTags[t, c]

	c.invoices' = c.invoices + i
	i.company' = c
	i.category' = cat
	i.tags' = i.tags
	
	sameUsers
	sameCategories
	sameTags
	sameBudgets
	sameRegistered
	all c0 : Company | c != c0 implies c0.invoices' = c0.invoices
	all i0 : Invoice | i != i0 implies i0.company' = i0.company and
                                            i0.category' = i0.category and
							  i0.tags' = i0.tags
}

pred changeInvoiceCategory[i : Invoice, cat : Category] {
	invoiceProcessed[i]
	companyCategory[cat, i.company]

	i.company' = i.company
	i.category' = cat
	i.tags' = i.tags
	
	sameUsers
	sameCategories
	sameTags
	sameBudgets
	sameRegistered
	all c : Company | c.invoices' = c.invoices
	all i0 : Invoice | i != i0 implies i0.company' = i0.company and
                                            i0.category' = i0.category and
							  i0.tags' = i0.tags
}

pred addCategoryToCompany[cat : Category, c : Company] {
	companyRegistered[c]
	not categoryRegistered[cat]
	emptyCategory[cat]

	c.categories' = c.categories + cat
	
	sameInvoices
	sameUsers
	sameTags
	sameBudgets
	sameRegistered
	all c0 : Company | c != c0 implies c0.categories' = c0.categories
}

pred addTagsToCompany[t : Tag, c : Company] {
	companyRegistered[c]
	some t
	not tagsRegistered[t]

	c.tags' = c.tags + t
	
	sameInvoices
	sameUsers
	sameCategories
	sameBudgets
	sameRegistered
	all c0 : Company | c != c0 implies c0.tags' = c0.tags
}

pred addInvoiceTags[i : Invoice, t : Tag] {
	invoiceProcessed[i]
	some t
	companyTags[t, i.company]
	t not in i.tags

	i.company' = i.company
	i.category' = i.category
	i.tags' = i.tags + t
	
	sameUsers
	sameCategories
	sameTags
	sameBudgets
	sameRegistered
	all c : Company | c.invoices' = c.invoices
	all i0 : Invoice | i != i0 implies i0.company' = i0.company and
                                            i0.category' = i0.category and
							  i0.tags' = i0.tags
}

pred removeInvoiceTags[i : Invoice, t : Tag] {
	invoiceProcessed[i]
	some t
	t in i.tags

	i.company' = i.company
	i.category' = i.category
	i.tags' = i.tags - t
	
	sameUsers
	sameCategories
	sameTags
	sameBudgets
	sameRegistered
	all c : Company | c.invoices' = c.invoices
	all i0 : Invoice | i != i0 implies i0.company' = i0.company and
                                            i0.category' = i0.category and
							  i0.tags' = i0.tags
}


fact traces {
	no Registered
	always (
		some u : User | some c : Company | some i : Invoice | some t : Tag | some cat : Category |
			registerUser[u, c] or addUserToCompany[u, c] or 
		      addInvoiceToCompany[i, c, cat, t] or addTagsToCompany[t, c] or addCategoryToCompany[cat, c] or
			changeInvoiceCategory[i, cat] or addInvoiceTags[i, t] or removeInvoiceTags[i, t] or
			stutter
	)
}

run { some c : Company | emptyCompany[c] } for 3


check UsersBelongToOnlyOneCompany {
	always (
 		all disj c1, c2 : Registered | no c1.users & c2.users
	)
}

check CompanyHasAtLeastOneUser {
	always (
		all c : Registered | some c.users
	)
}

check InvoicesBelongToOnlyOneCompany {
	always (
 		all disj c1, c2 : Registered | no c1.invoices & c2.invoices
	)
}

check CategoriesBelongToOnlyOneCompany {
	always (
 		all disj c1, c2 : Registered | no c1.categories & c2.categories
	)
}

check TagsBelongToOnlyOneCompany {
	always (
 		all disj c1, c2 : Registered | no c1.tags & c2.tags
	)
 }

check BudgetsBelongToOnlyOneCompany {
	always (
		all disj c1, c2 : Registered | all cat1 : c1.categories | all cat2 : c2.categories |
			no cat1.budget & cat2.budget
	)
}

check BudgetsBelongToOnlyOneCategory {
	always (
		all c : Registered | all disj cat1, cat2 : c.categories | no cat1.budget & cat2.budget
	)
}

check InvoiceCompanyIsConsistent {
	always (
		all c : Registered | all i : c.invoices | one i.company and i.company = c
	)
}

check InvoiceCategoryBelongsToCompany {
	always (
		all c : Registered | all i : c.invoices | one i.category and i.category in c.categories
	)
}

check InvoiceTagsBelongToCompany {
	always (
		all c : Registered | all i : c.invoices | i.tags in c.tags
	)
}

check UsersBelongsToOnlyOneCompany {
	always (
		all u : User | all c : Registered | u in c.users implies always u in c.users
	)
}