exploit brake_pads(a)=
	preconditions:
		quality:a,brake_months>=6;
		quality:a,brake_vio=false;
	postconditions:
		update quality:a,brake_vio=true;
		update quality:a,compliance_vio=true;
		update quality:a,TIME_ADVANCE_FLAG=0;
.

exploit exhaust_pipes(a)=
	preconditions:
		quality:a,exhaust_months>=12;
		quality:a,exhaust_vio=false;
	postconditions:
		update quality:a,compliance_vio=true;
		update quality:a,exhaust_vio=true;
		update quality:a,TIME_ADVANCE_FLAG=0;
.

exploit ac_filter(a)=
	preconditions:
		quality:a,ac_odometer>=120000;
		quality:a,ac_vio=false;
	postconditions:
		insert quality:a,is_critical=true;
		update quality:a,compliance_vio=true;
		update quality:a,TIME_ADVANCE_FLAG=0;
		update quality:a,ac_vio=true;
.

exploit vacuum_pump(a)=
	preconditions:
		quality:a,vacuum_odometer>=120000;
		quality:a,engine=diesel;
		quality:a,vacuum_vio=false;
	postconditions:
		insert quality:a,is_critical=true;
		update quality:a,compliance_vio=true;
		update quality:a,TIME_ADVANCE_FLAG=0;
		update quality:a,vacuum_vio=true;
.

exploit super_service(a)=
	preconditions:	
		quality:a,brake_months=1;
		quality:a,exhaust_months=1;
		quality:a,ac_odometer=10000;
		quality:a,vacuum_odometer=10000;
	postconditions:	
		update quality:a,brake_months=0;
		update quality:a,exhaust_months=0;
		update quality:a,ac_odometer=0;
		update quality:a,vacuum_odometer=0;
		update quality:a,brake_vio=false;
		update quality:a,exhaust_vio=false;
		update quality:a,ac_vio=false;
		update quality:a,vacuum_vio=false;
		update quality:a,TIME_ADVANCE_FLAG=0;
.


exploit time_advance_0(a)=
	preconditions:
		quality:a,brake_months=0;
		quality:a,exhaust_months=0;
		quality:a,ac_odometer=0;
		quality:a,vacuum_odometer=0;
		quality:a,brake_vio=false;
		quality:a,exhaust_vio=false;
		quality:a,ac_vio=false;
		quality:a,vacuum_vio=false;
		quality:a,TIME_ADVANCE_STEP=0;
	postconditions:		
		update quality:a,brake_months=1;
		update quality:a,exhaust_months=1;
		update quality:a,ac_odometer=10000;
		update quality:a,vacuum_odometer=10000;
		update quality:a,TIME_ADVANCE_FLAG=1;
		update quality:a,TIME_ADVANCE_STEP=1;
.


exploit time_advance_1(a)=
	preconditions:
		quality:a,brake_months=0;
		quality:a,exhaust_months=0;
		quality:a,ac_odometer=0;
		quality:a,vacuum_odometer=0;
		quality:a,brake_vio=false;
		quality:a,exhaust_vio=false;
		quality:a,ac_vio=false;
		quality:a,vacuum_vio=false;
		quality:a,TIME_ADVANCE_STEP=1;
	postconditions:		
		update quality:a,brake_months=1;
		update quality:a,exhaust_months=1;
		update quality:a,ac_odometer=10000;
		update quality:a,vacuum_odometer=10000;
		update quality:a,TIME_ADVANCE_FLAG=1;
		update quality:a,TIME_ADVANCE_STEP=2;
.


exploit time_advance_2(a)=
	preconditions:
		quality:a,brake_months=0;
		quality:a,exhaust_months=0;
		quality:a,ac_odometer=0;
		quality:a,vacuum_odometer=0;
		quality:a,brake_vio=false;
		quality:a,exhaust_vio=false;
		quality:a,ac_vio=false;
		quality:a,vacuum_vio=false;
		quality:a,TIME_ADVANCE_STEP=2;
	postconditions:		
		update quality:a,brake_months=1;
		update quality:a,exhaust_months=1;
		update quality:a,ac_odometer=10000;
		update quality:a,vacuum_odometer=10000;
		update quality:a,TIME_ADVANCE_FLAG=1;
		update quality:a,TIME_ADVANCE_STEP=3;
.

exploit time_advance_3(a)=
	preconditions:
		quality:a,brake_months=0;
		quality:a,exhaust_months=0;
		quality:a,ac_odometer=0;
		quality:a,vacuum_odometer=0;
		quality:a,brake_vio=false;
		quality:a,exhaust_vio=false;
		quality:a,ac_vio=false;
		quality:a,vacuum_vio=false;
		quality:a,TIME_ADVANCE_STEP=3;
	postconditions:		
		update quality:a,brake_months=1;
		update quality:a,exhaust_months=1;
		update quality:a,ac_odometer=10000;
		update quality:a,vacuum_odometer=10000;
		update quality:a,TIME_ADVANCE_FLAG=1;
		update quality:a,TIME_ADVANCE_STEP=4;
.

exploit time_advance_4(a)=
	preconditions:
		quality:a,brake_months=0;
		quality:a,exhaust_months=0;
		quality:a,ac_odometer=0;
		quality:a,vacuum_odometer=0;
		quality:a,brake_vio=false;
		quality:a,exhaust_vio=false;
		quality:a,ac_vio=false;
		quality:a,vacuum_vio=false;
		quality:a,TIME_ADVANCE_STEP=4;
	postconditions:		
		update quality:a,brake_months=1;
		update quality:a,exhaust_months=1;
		update quality:a,ac_odometer=10000;
		update quality:a,vacuum_odometer=10000;
		update quality:a,TIME_ADVANCE_FLAG=1;
		update quality:a,TIME_ADVANCE_STEP=5;
.

exploit time_advance_5(a)=
	preconditions:
		quality:a,brake_months=0;
		quality:a,exhaust_months=0;
		quality:a,ac_odometer=0;
		quality:a,vacuum_odometer=0;
		quality:a,brake_vio=false;
		quality:a,exhaust_vio=false;
		quality:a,ac_vio=false;
		quality:a,vacuum_vio=false;
		quality:a,TIME_ADVANCE_STEP=5;
	postconditions:		
		update quality:a,brake_months=1;
		update quality:a,exhaust_months=1;
		update quality:a,ac_odometer=10000;
		update quality:a,vacuum_odometer=10000;
		update quality:a,TIME_ADVANCE_FLAG=1;
		update quality:a,TIME_ADVANCE_STEP=6;
.

exploit time_advance_6(a)=
	preconditions:
		quality:a,brake_months=0;
		quality:a,exhaust_months=0;
		quality:a,ac_odometer=0;
		quality:a,vacuum_odometer=0;
		quality:a,brake_vio=false;
		quality:a,exhaust_vio=false;
		quality:a,ac_vio=false;
		quality:a,vacuum_vio=false;
		quality:a,TIME_ADVANCE_STEP=6;
	postconditions:		
		update quality:a,brake_months=1;
		update quality:a,exhaust_months=1;
		update quality:a,ac_odometer=10000;
		update quality:a,vacuum_odometer=10000;
		update quality:a,TIME_ADVANCE_FLAG=1;
		update quality:a,TIME_ADVANCE_STEP=7;
.

exploit time_advance_7(a)=
	preconditions:
		quality:a,brake_months=0;
		quality:a,exhaust_months=0;
		quality:a,ac_odometer=0;
		quality:a,vacuum_odometer=0;
		quality:a,brake_vio=false;
		quality:a,exhaust_vio=false;
		quality:a,ac_vio=false;
		quality:a,vacuum_vio=false;
		quality:a,TIME_ADVANCE_STEP=7;
	postconditions:		
		update quality:a,brake_months=1;
		update quality:a,exhaust_months=1;
		update quality:a,ac_odometer=10000;
		update quality:a,vacuum_odometer=10000;
		update quality:a,TIME_ADVANCE_FLAG=1;
		update quality:a,TIME_ADVANCE_STEP=8;
.


exploit time_advance_8(a)=
	preconditions:
		quality:a,brake_months=0;
		quality:a,exhaust_months=0;
		quality:a,ac_odometer=0;
		quality:a,vacuum_odometer=0;
		quality:a,brake_vio=false;
		quality:a,exhaust_vio=false;
		quality:a,ac_vio=false;
		quality:a,vacuum_vio=false;
		quality:a,TIME_ADVANCE_STEP=8;
	postconditions:		
		update quality:a,brake_months=1;
		update quality:a,exhaust_months=1;
		update quality:a,ac_odometer=10000;
		update quality:a,vacuum_odometer=10000;
		update quality:a,TIME_ADVANCE_FLAG=1;
		update quality:a,TIME_ADVANCE_STEP=9;
.

exploit time_advance_9(a)=
	preconditions:
		quality:a,brake_months=0;
		quality:a,exhaust_months=0;
		quality:a,ac_odometer=0;
		quality:a,vacuum_odometer=0;
		quality:a,brake_vio=false;
		quality:a,exhaust_vio=false;
		quality:a,ac_vio=false;
		quality:a,vacuum_vio=false;
		quality:a,TIME_ADVANCE_STEP=9;
	postconditions:		
		update quality:a,brake_months=1;
		update quality:a,exhaust_months=1;
		update quality:a,ac_odometer=10000;
		update quality:a,vacuum_odometer=10000;
		update quality:a,TIME_ADVANCE_FLAG=1;
		update quality:a,TIME_ADVANCE_STEP=10;
.

exploit time_advance_10(a)=
	preconditions:
		quality:a,brake_months=0;
		quality:a,exhaust_months=0;
		quality:a,ac_odometer=0;
		quality:a,vacuum_odometer=0;
		quality:a,brake_vio=false;
		quality:a,exhaust_vio=false;
		quality:a,ac_vio=false;
		quality:a,vacuum_vio=false;
		quality:a,TIME_ADVANCE_STEP=10;
	postconditions:		
		update quality:a,brake_months=1;
		update quality:a,exhaust_months=1;
		update quality:a,ac_odometer=10000;
		update quality:a,vacuum_odometer=10000;
		update quality:a,TIME_ADVANCE_FLAG=1;
		update quality:a,TIME_ADVANCE_STEP=11;
.

exploit time_advance_11(a)=
	preconditions:
		quality:a,brake_months=0;
		quality:a,exhaust_months=0;
		quality:a,ac_odometer=0;
		quality:a,vacuum_odometer=0;
		quality:a,brake_vio=false;
		quality:a,exhaust_vio=false;
		quality:a,ac_vio=false;
		quality:a,vacuum_vio=false;
		quality:a,TIME_ADVANCE_STEP=11;
	postconditions:		
		update quality:a,brake_months=1;
		update quality:a,exhaust_months=1;
		update quality:a,ac_odometer=10000;
		update quality:a,vacuum_odometer=10000;
		update quality:a,TIME_ADVANCE_FLAG=1;
		update quality:a,TIME_ADVANCE_STEP=12;
.

exploit time_advance_12(a)=
	preconditions:
		quality:a,brake_months=0;
		quality:a,exhaust_months=0;
		quality:a,ac_odometer=0;
		quality:a,vacuum_odometer=0;
		quality:a,brake_vio=false;
		quality:a,exhaust_vio=false;
		quality:a,ac_vio=false;
		quality:a,vacuum_vio=false;
		quality:a,TIME_ADVANCE_STEP=12;
	postconditions:		
		update quality:a,brake_months=1;
		update quality:a,exhaust_months=1;
		update quality:a,ac_odometer=10000;
		update quality:a,vacuum_odometer=10000;
		update quality:a,TIME_ADVANCE_FLAG=1;
		update quality:a,TIME_ADVANCE_STEP=13;
.