exploit hipaa_training(a)=
	preconditions:
		quality:a,current_emp=true;
		quality:a,hipaa_training_date<=20210503;
	postconditions:
		update quality:a,compliance_vios+=1;
.

exploit pol_proc_attest(a)=
	preconditions:
		quality:a,current_emp=true;
		quality:a,pol_proc_attestation<=20210503;
	postconditions:
		update quality:a,compliance_vios+=1;
.

exploit comp_officer(a)=
	preconditions:
		quality:a,hipaa_compliance_officer=false;
	postconditions:
		update quality:a,compliance_vios+=1;
.

exploit priv_officer(a)=
	preconditions:
		quality:a,hipaa_privacy_officer=false;
	postconditions:
		update quality:a,compliance_vios+=1;
.

exploit sec_officer(a)=
	preconditions:
		quality:a,hipaa_security_officer=false;
	postconditions:
		update quality:a,compliance_vios+=1;
.

exploit access_control(a)=
	preconditions:
		quality:a,current_emp=true;
		quality:a,has_pin=false;
	postconditions:
		update quality:a,compliance_vios+=1;
.

exploit mobile(a)=
	preconditions:
		quality:a,uses_mobile=true;
		quality:a,mobile_regs=false;
	postconditions:
		update quality:a,compliance_vios+=1;
.

exploit lock(a)=
	preconditions:
		quality:a,ephi_lock!=true;
	postconditions:
		update quality:a,compliance_vios+=1;
.

exploit inventory(a)=
	preconditions:
		quality:a,hw_inventory=false;
	postconditions:
		update quality:a,compliance_vios+=1;
.

exploit risk_asses(a)=
	preconditions:
		quality:a,sec_risk_assessment<=20210503;
	postconditions:
		update quality:a,compliance_vios+=1;
.

exploit priv_asses(a)=
	preconditions:
		quality:a,priv_stand_audit<=20210503;
	postconditions:
		update quality:a,compliance_vios+=1;
.

exploit hitech_asses(a)=
	preconditions:
		quality:a,hitech_audit<=20210503;
	postconditions:
		update quality:a,compliance_vios+=1;
.

exploit sec_asses(a)=
	preconditions:
		quality:a,sec_stand_audit<=20210503;
	postconditions:
		update quality:a,compliance_vios+=1;
.

exploit dev_asses(a)=
	preconditions:
		quality:a,asset_dev_audit<=20210503;
	postconditions:
		update quality:a,compliance_vios+=1;
.

exploit phys_assess(a)=
	preconditions:
		quality:a,phys_audit<=20210503;
	postconditions:
		update quality:a,compliance_vios+=1;
.

exploit breach(a)=
	preconditions:
		quality:a,breach_process=false;
	postconditions:
		update quality:a,compliance_vios+=1;
.

exploit report(a)=
	preconditions:
		quality:a,anon_reports!=true;
	postconditions:
		update quality:a,compliance_vios+=1;
.

exploit insecure_data(a)=
	preconditions:
		quality:a,encryption!=true;
	postconditions:
		update quality:a,compliance_vios+=1;
.

exploit expired_c(a)=
	preconditions:
		quality:a,cert_expir<=20220503;
	postconditions:
		update quality:a,expired_cert=true;
.

exploit insecure_db(a)=
	preconditions:
		quality:a,expired_cert=true;
	postconditions:
		update quality:a,compliance_vios+=1;
.

exploit new_emp(a,b)=
	preconditions:
		quality:a,can_add_emp=true;
		topology:a<->b,comp;
	postconditions:
		update quality:a,can_add_emp=false;
		update quality:a,hw_inventory=false;
		update quality:b,mobile_regs=false;
.

exploit rm_emp(a)=
	preconditions:
		quality:a,can_rm_emp=true;
		quality:a,hipaa_compliance_officer=true;
	postconditions:
		update quality:a,hipaa_compliance_officer=false;
		update quality:a,current_emp=false;
.

exploit phys_vio(a)=
	preconditions:
		quality:a,ephi_lock=false;
	postconditions:
		update quality:a,compliance_vios+=1;
.

exploit break_lock(a)=
	preconditions:
		quality:a,ephi_lock=true;
	postconditions:
		update quality:a,ephi_lock=false;
.

time group exploit time_emp_advance(a)=
	preconditions:
		quality:a,TIME_ADVANCE_STEP<13;
		quality:a,current_emp=true;
	postconditions:
		update quality:a,hipaa_training_date-=100;
		update quality:a,pol_proc_attestation-=100;
.

time group exploit time_comp_advance(a)=
	preconditions:
		quality:a,TIME_ADVANCE_STEP<13;
		quality:a,date=05032022;
	postconditions:
		update quality:a,hw_inventory=true;
		update quality:a,sec_risk_assessment-=100;
		update quality:a,priv_stand_audit-=100;
		update quality:a,hitech_audit-=100;
		update quality:a,sec_stand_audit-=100;
		update quality:a,asset_dev_audit-=100;
		update quality:a,phys_audit-=100;
.