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;
.

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;
.

exploit ac_filter(a)=
	preconditions:
		quality:a,ac_odometer>=12000;
		quality:a,ac_vio=false;
	postconditions:
		insert quality:a,is_critical=true;
		update quality:a,compliance_vio=true;
		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,vacuum_vio=true;
.


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

exploit dummy_1(a)=
	preconditions:
		quality:a,can_fly=true;
	postconditions:
		insert quality:a,flying_car=true;
.

exploit dummy_2(a)=
	preconditions:
		quality:a,can_fly=true;
	postconditions:
		insert quality:a,flying_car=true;
.

exploit dummy_3(a)=
	preconditions:
		quality:a,can_fly=true;
	postconditions:
		insert quality:a,flying_car=true;
.

exploit dummy_4(a)=
	preconditions:
		quality:a,can_fly=true;
	postconditions:
		insert quality:a,flying_car=true;
.

exploit dummy_5(a)=
	preconditions:
		quality:a,can_fly=true;
	postconditions:
		insert quality:a,flying_car=true;
.

exploit dummy_6(a)=
	preconditions:
		quality:a,can_fly=true;
	postconditions:
		insert quality:a,flying_car=true;
.

exploit dummy_7(a)=
	preconditions:
		quality:a,can_fly=true;
	postconditions:
		insert quality:a,flying_car=true;
.

exploit dummy_8(a)=
	preconditions:
		quality:a,can_fly=true;
	postconditions:
		insert quality:a,flying_car=true;
.

exploit dummy_9(a)=
	preconditions:
		quality:a,can_fly=true;
	postconditions:
		insert quality:a,flying_car=true;
.

exploit dummy_10(a)=
	preconditions:
		quality:a,can_fly=true;
	postconditions:
		insert quality:a,flying_car=true;
.

exploit dummy_11(a)=
	preconditions:
		quality:a,can_fly=true;
	postconditions:
		insert quality:a,flying_car=true;
.

exploit dummy_12(a)=
	preconditions:
		quality:a,can_fly=true;
	postconditions:
		insert quality:a,flying_car=true;
.

exploit dummy_13(a)=
	preconditions:
		quality:a,can_fly=true;
	postconditions:
		insert quality:a,flying_car=true;
.

exploit dummy_14(a)=
	preconditions:
		quality:a,can_fly=true;
	postconditions:
		insert quality:a,flying_car=true;
.

exploit dummy_15(a)=
	preconditions:
		quality:a,can_fly=true;
	postconditions:
		insert quality:a,flying_car=true;
.

exploit dummy_16(a)=
	preconditions:
		quality:a,can_fly=true;
	postconditions:
		insert quality:a,flying_car=true;
.

exploit dummy_17(a)=
	preconditions:
		quality:a,can_fly=true;
	postconditions:
		insert quality:a,flying_car=true;
.

exploit dummy_18(a)=
	preconditions:
		quality:a,can_fly=true;
	postconditions:
		insert quality:a,flying_car=true;
.

exploit dummy_19(a)=
	preconditions:
		quality:a,can_fly=true;
	postconditions:
		insert quality:a,flying_car=true;
.

exploit dummy_20(a)=
	preconditions:
		quality:a,can_fly=true;
	postconditions:
		insert quality:a,flying_car=true;
.

exploit dummy_21(a)=
	preconditions:
		quality:a,can_fly=true;
	postconditions:
		insert quality:a,flying_car=true;
.

exploit dummy_22(a)=
	preconditions:
		quality:a,can_fly=true;
	postconditions:
		insert quality:a,flying_car=true;
.

exploit dummy_23(a)=
	preconditions:
		quality:a,can_fly=true;
	postconditions:
		insert quality:a,flying_car=true;
.

exploit dummy_24(a)=
	preconditions:
		quality:a,can_fly=true;
	postconditions:
		insert quality:a,flying_car=true;
.

exploit dummy_25(a)=
	preconditions:
		quality:a,can_fly=true;
	postconditions:
		insert quality:a,flying_car=true;
.

exploit dummy_26(a)=
	preconditions:
		quality:a,can_fly=true;
	postconditions:
		insert quality:a,flying_car=true;
.

exploit dummy_27(a)=
	preconditions:
		quality:a,can_fly=true;
	postconditions:
		insert quality:a,flying_car=true;
.

exploit dummy_28(a)=
	preconditions:
		quality:a,can_fly=true;
	postconditions:
		insert quality:a,flying_car=true;
.

exploit dummy_29(a)=
	preconditions:
		quality:a,can_fly=true;
	postconditions:
		insert quality:a,flying_car=true;
.

exploit dummy_30(a)=
	preconditions:
		quality:a,can_fly=true;
	postconditions:
		insert quality:a,flying_car=true;
.

exploit dummy_31(a)=
	preconditions:
		quality:a,can_fly=true;
	postconditions:
		insert quality:a,flying_car=true;
.

exploit dummy_32(a)=
	preconditions:
		quality:a,can_fly=true;
	postconditions:
		insert quality:a,flying_car=true;
.

exploit dummy_33(a)=
	preconditions:
		quality:a,can_fly=true;
	postconditions:
		insert quality:a,flying_car=true;
.

exploit dummy_34(a)=
	preconditions:
		quality:a,can_fly=true;
	postconditions:
		insert quality:a,flying_car=true;
.

exploit dummy_35(a)=
	preconditions:
		quality:a,can_fly=true;
	postconditions:
		insert quality:a,flying_car=true;
.

exploit dummy_36(a)=
	preconditions:
		quality:a,can_fly=true;
	postconditions:
		insert quality:a,flying_car=true;
.

exploit dummy_37(a)=
	preconditions:
		quality:a,can_fly=true;
	postconditions:
		insert quality:a,flying_car=true;
.

exploit dummy_38(a)=
	preconditions:
		quality:a,can_fly=true;
	postconditions:
		insert quality:a,flying_car=true;
.

exploit dummy_39(a)=
	preconditions:
		quality:a,can_fly=true;
	postconditions:
		insert quality:a,flying_car=true;
.

exploit dummy_40(a)=
	preconditions:
		quality:a,can_fly=true;
	postconditions:
		insert quality:a,flying_car=true;
.

exploit dummy_41(a)=
	preconditions:
		quality:a,can_fly=true;
	postconditions:
		insert quality:a,flying_car=true;
.

exploit dummy_42(a)=
	preconditions:
		quality:a,can_fly=true;
	postconditions:
		insert quality:a,flying_car=true;
.

time group exploit time_advance(a)=
	preconditions:
		quality:a,TIME_ADVANCE_STEP<13;
		quality:a,brake_months<6;
		quality:a,brake_vio=false;
	postconditions:		
		update quality:a,brake_months+=1;
		update quality:a,vacuum_odometer+=10000;
		update quality:a,ac_odometer+=10000;
		update quality:a,exhaust_months+=1;
		update quality:a,TIME_ADVANCE_STEP+=1;
.