forked from UTulsa-Research/ag_gen
338 lines
8.8 KiB
Plaintext
338 lines
8.8 KiB
Plaintext
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 brake_service(a)=
|
|
preconditions:
|
|
quality:a,brake_months=1;
|
|
postconditions:
|
|
update quality:a,brake_vio=false;
|
|
update quality:a,brake_months=0;
|
|
.
|
|
|
|
exploit exhaust_service(a)=
|
|
preconditions:
|
|
quality:a,exhaust_months=1;
|
|
postconditions:
|
|
update quality:a,exhaust_vio=false;
|
|
update quality:a,exhaust_months=0;
|
|
.
|
|
|
|
exploit ac_service(a)=
|
|
preconditions:
|
|
quality:a,ac_odometer=10000;
|
|
postconditions:
|
|
update quality:a,ac_vio=false;
|
|
update quality:a,ac_odometer=0;
|
|
.
|
|
|
|
exploit vacuum_service(a)=
|
|
preconditions:
|
|
quality:a,vacuum_odometer=10000;
|
|
postconditions:
|
|
update quality:a,vacuum_vio=false;
|
|
update quality:a,vacuum_odometer=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;
|
|
.
|