/*
 * Protection of Privacy and Transborder Flows of Personal Data
 * Version simplified with one action for representing the purpose check
 * and one action for accuracy verification
 */

initial:

	cc(dc,asker,asked_data,sent_data).

constitutive:

/*
 *  Send of personal data
 */

ask_data
	means 
		asked_data
	if
		!asked_data.

send_data
	means 
		sent_data
	if
		asked_data &
		!sent_data &
		!refuse_data.

refuse_data
	means 
		refuse_data,
		cancel(c(dc,asker,sent_data))
	if
		asked_data &
		!sent_data &
		!refuse_data.

/*
 *  The following implements a simplified version of OECD Guidelines on the protection of privacy and
 *  transborder flows of personal data.
 */


//Pariodically check of the accuracy.
periodically_verify_accuracy
	means	
		accuracy_verified
	if 
		!asked_data &
		!accuracy_verified.

//Check of the accuracy before sending data if periodically check has not been done before
check_accuracy
	means	
		accuracy_verified
	if 
		asked_data &
		!accuracy_verified.

//Verify that the purpose for which data have been required agrees with the purpose for which
//data have been stored
verify_purpose
	means
		purpose_verified
	if
		asked_data &
		!purpose_verified.

//notify the data owner that his/her data have been sent
notify_owner
	means
		owner_notified
	if
		sent_data &
		!owner_notified.

regulative:

	purpose_verified ->. sent_data.
	accuracy_verified ->. sent_data.
	sent_data .-> owner_notified.
	purpose_verified ->. refuse_data.
	accuracy_verified ->. refuse_data.