load privacy.maude

mod PRIVACY-EXAMPLE-COMPANY is
	extending UNIVERSE .
	protecting PRIVACY-TYPE-CHECKER .
	protecting PRIVACY-CALCULUS-SEMANTICS .
	
	ops Company Comp&Clients DB MarketingDpt ThirdParty Server Clients : -> Role [ctor] .
	ops Alice : -> User [ctor] .
	ops purchase storage marketing : -> Purpose [ctor] .
	op OrderData : -> PrivateDataType [ctor] .
	
	sort OwnerConsentValue .
	subsort OwnerConsentValue < PrivateDataValue .
	op OwnerConsent : -> PrivateDataType [ctor] .
	ops yes no : -> OwnerConsentValue [ctor] .
	eq domain(OwnerConsent) = yes no .
	eq var(yes) = OwnerConsent .
	eq var(no) = OwnerConsent .

	sort AgeValues .
	subsort AgeValues < PrivateDataValue .
	op Age : -> PrivateDataType [ctor] .
	ops under13 over13 : -> AgeValues [ctor] .
	eq domain(Age) = under13 over13 .
	eq var(under13) = Age .
	eq var(over13) = Age .
	
	op H : -> Hierarchy .
	eq H = 
		Comp&Clients[
			Clients : purchase [
				Alice []
			],
			Company [
				DB : storage,
				Server : purchase,
				MarketingDpt : marketing
			],
			ThirdParty [MarketingDpt : marketing]
		 ].
	op sales-policy : -> Policy .
	eq sales-policy = 
		OrderData >> H,
			p(marketing, MarketingDpt) = access 
				disc ThirdParty if Age =/= under13 /\ OwnerConsent == yes,
			p(purchase, Server) = read access write disc Company,
			p(purchase, Alice) = read write access disc Comp&Clients
	 ;  Age >> H, 
			p(marketing, MarketingDpt) = access read,
			p(storage, DB) = access write disc Company,
			p(purchase, Alice) = read write access disc Comp&Clients
	 ;  OwnerConsent >> H,
			p(marketing, MarketingDpt) = access read,
			p(storage, DB) = access write disc Company,
			p(purchase, Alice) = read write access disc Comp&Clients . 
		
	op S : -> System .
	eq S = 
	Comp&Clients[(v 'order : Comp&Clients[Comp&Clients[OrderData]])(
		Company[
			(v 'userage : Company[Company[Age]])
			(v 'usercons : Company[Company[OwnerConsent]])
			(v 'orderdata : Company[Company[OrderData]])(
				DB : storage [ !(
					(v 'age : Company[Age])(v 'cons : Company[OwnerConsent])
					( out 'userage ('age). out 'age(under13). 0P
					| out 'usercons ('cons). out 'cons (yes). 0P)
				)]
			||	ThirdParty[MarketingDpt : marketing [
					in 'userage('age : Company[Age]). in 'age('x : Age).
					in 'usercons('cons : Company[OwnerConsent]).
					in 'cons('y : OwnerConsent). 
					['x =/= under13]['y == yes]  
						in 'orderdata('d : Company[OrderData]). 
						out 'linktotp('d). 0P 
				]]
			||	Server : purchase [ !(
					in 'order('d : Comp&Clients[OrderData]).
					in 'd('data : OrderData).
					(v 'd : Company[OrderData])
					out 'orderdata('d). out 'd('data). 0P
				)]
			)] 
	||	Clients[Alice : purchase[(v 'data : Comp&Clients[OrderData]) out 'order('data). 0P]]
	)] .
	
	op S' : -> System .
	eq S' = 
	Comp&Clients[(v 'order : Comp&Clients[Comp&Clients[OrderData]])(
		Company[
			(v 'userage : Company[Company[Age]])
			(v 'usercons : Company[Company[OwnerConsent]])
			(v 'orderdata : Company[Company[OrderData]])(
				DB : storage [ !(
					(v 'age : Company[Age])(v 'cons : Company[OwnerConsent])
					( out 'userage ('age). out 'age(under13). 0P
					| out 'usercons ('cons). out 'cons (yes). 0P)
				)]
			||	ThirdParty[MarketingDpt : marketing [
					in 'userage('age : Company[Age]). in 'age('x : Age).
					in 'usercons('cons : Company[OwnerConsent]).
					in 'cons('y : OwnerConsent). 
					in 'orderdata('d : Company[OrderData]). 
					out 'linktotp('d). 0P 
				]]
			||	Server : purchase [ !(
					in 'order('d : Comp&Clients[OrderData]).
					in 'd('data : OrderData).
					(v 'd : Company[OrderData])
					out 'orderdata('d). out 'd('data). 0P
				)]
			)] 
	||	Clients[Alice : purchase[(v 'data : Comp&Clients[OrderData]) out 'order('data). 0P]]
	)] .
	
	op Gamma : -> GEnvironment .
	eq Gamma = 'linktotp{0} : ThirdParty[Company[OrderData]] .
endm

red compatible(sales-policy, Gamma, S) .
red compatible(sales-policy, Gamma, S') .