forked from UTulsa-Research/ag_gen
69 lines
1.6 KiB
Plaintext
69 lines
1.6 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 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;
|
|
postconditions:
|
|
update quality:a,brake_months=1;
|
|
update quality:a,TIME_ADVANCE_FLAG=1;
|
|
update quality:a,TIME_ADVANCE_STEP+=1;
|
|
.
|
|
|
|
|