open util/ordering[Date]

sig Date {}
sig Price {}
sig Client {}
sig Service {}
sig Package {
	services: set Service -> lone Price,
	incompatibles: set Package
}

sig Subscription {
	package: one Package,
	start: one Date,
	end: one Date
}

sig Operator {
	clients: set Client,
	packages: set Package,
	subscriptions: clients -> Subscription
}

fun IncompatibleSubscriptions[] : Subscription->Subscription {
	{ disj x, y:Subscription | lt[x.start, y.end] and lt[y.start, x.end] and x.package -> y.package in incompatibles }
}

/*
// A relação de incompatibilidade tem de ser simétrica e tem de conter elementos da identidade
fact {
	incompatibles = ~incompatibles
	all p:Package | p in p.incompatibles
}

// O cliente não pode ter pacotes incompatíveis
fact {
	all o:Operator |
		no (((~(o.subscriptions) . (o.subscriptions)) - iden) & { x, y:Subscription | lt[x.start, y.end] and lt[y.start, x.end] and x.package -> y.package in incompatibles } )
}

// Se dois pacotes contiverem o mesmo serviço, são incompatíveis
fact { services.Price.~(services.Price) - iden in incompatibles }

// Um pacote tem de ter pelo menos um serviço
fact { services.Price.Service = Package }

// A data inicial tem de ser anterior à data final
fact { (~start).end in ^next }

// Um cliente só pode estar subscrito a um pacote que esteja no operador
fact { all o:Operator | Client.(o.subscriptions).package in o.packages }

fact { some subscriptions }*/

pred inv[o:Operator] {
	incompatibles = ~incompatibles
	all p:Package | p in p.incompatibles
	services.Price.~(services.Price) - iden in incompatibles
	services.Price.Service = Package
	(~start).end in ^next

	no (((~(o.subscriptions) . (o.subscriptions)) - iden) & IncompatibleSubscriptions[] )
	Client.(o.subscriptions).package in o.packages
}

pred create_client[o,o':Operator, c:Client] {
	// pre-conditions
	c not in o.clients

	// frame-conditions
	o'.clients = o.clients + c
	o'.packages = o.packages
	o.subscriptions = o'.subscriptions
}

pred delete_client[o,o':Operator, c:Client] {
	// pre-conditions
	c in o.clients
	no c.(o.subscriptions)

	// frame-conditions
	o'.clients = o.clients - c
	o'.packages = o.packages
	o'.subscriptions = o.subscriptions
}

pred create_package[o,o':Operator, p:Package] {
	// pre-conditions
	p not in o.packages

	// frame-conditions
	o'.clients = o.clients
	o'.subscriptions = o.subscriptions
	o'.packages = o.packages + p
}

pred delete_package[o,o': Operator, p:Package] {
	// pre-conditions
	p in o.packages
	p not in Client.(o.subscriptions).package

	// frame-conditions
	o'.clients = o.clients
	o'.subscriptions = o.subscriptions
	o'.packages = o.packages - p
}

pred create_client_package[o,o':Operator, c:Client, s:Subscription] {
	// pre-conditions
	c in o.clients
	s.package in o.packages
	c->s not in o.subscriptions
	no (s -> c.(o.subscriptions)) & IncompatibleSubscriptions[]

	// frame-conditions
	o'.clients = o.clients
	o'.packages = o.packages
	o'.subscriptions = o.subscriptions + c->s
}

pred change_subscription_end_date[o,o':Operator, c:Client, s, s':Subscription] {
	// pre conditions
	c in o.clients
	c->s in o.subscriptions

	s.package = s'.package
	s.start = s'.start
	no (s' -> (c.(o.subscriptions) - s)) & IncompatibleSubscriptions[]

	// frame conditions
	o'.clients = o.clients
	o'.packages = o.packages
	o'.subscriptions = o.subscriptions - (c->s) + (c->s')
}

pred create_client_consistent[o,o':Operator, c:Client] { inv[o] && create_client[o,o',c] }
assert create_client_safe { all o,o':Operator, c:Client | inv[o] && create_client[o,o',c] => inv[o'] }

pred delete_client_consistent[o,o':Operator, c:Client] { inv[o] && delete_client[o,o',c] }
assert delete_client_safe { all o,o':Operator, c:Client | inv[o] && delete_client[o,o',c] => inv[o'] }

pred create_package_consistent[o,o':Operator, p:Package] { inv[o] && create_package[o,o',p] }
assert create_package_safe { all o,o':Operator, p:Package | inv[o] && create_package[o,o',p] => inv[o'] }

pred delete_package_consistent[o,o':Operator, p:Package] { inv[o] && delete_package[o,o',p] }
assert delete_package_safe { all o,o':Operator, p:Package | inv[o] && delete_package[o,o',p] => inv[o'] }

pred create_client_package_consistent[o,o':Operator, c:Client, s:Subscription] { inv[o] && create_client_package[o,o',c,s] }
assert create_client_package_safe { all o,o':Operator, c:Client, s:Subscription | inv[o] && create_client_package[o,o',c,s] => inv[o'] }

pred change_subscription_end_date_consistent[o,o':Operator, c:Client, s, s':Subscription] { inv[o] && change_subscription_end_date[o,o',c,s,s'] }
assert change_subscription_end_date_safe { all o,o':Operator, c:Client, s, s':Subscription | inv[o] && change_subscription_end_date[o,o',c,s,s'] => inv[o'] }

check create_client_safe for 5
check delete_client_safe for 5
check create_package_safe for 5
check delete_package_safe for 5
check create_client_package_safe for 5
check change_subscription_end_date_safe for 5

run create_client_consistent for 5
run delete_client_consistent for 5
run create_package_consistent for 5
run delete_package_consistent for 5
run create_client_package_consistent for 5
run change_subscription_end_date_consistent for 5