Adding a 6 Sync Option
This commit is contained in:
parent
7add771ac3
commit
8bcef4c98e
@ -0,0 +1,80 @@
|
||||
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 engine_oil(a)=
|
||||
preconditions:
|
||||
quality:a,oil_odom>=6000;
|
||||
quality:a,oil_vio=false;
|
||||
postconditions:
|
||||
update quality:a,oil_vio=true;
|
||||
update quality:a,compliance_vio=true;
|
||||
.
|
||||
|
||||
exploit driveshaft_boots(a)=
|
||||
preconditions:
|
||||
quality:a,driveshaft_odom>=12000;
|
||||
quality:a,driveshaft_vio=false;
|
||||
postconditions:
|
||||
update quality:a,driveshaft_vio=true;
|
||||
update quality:a,compliance_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 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,oil_odom+=10000;
|
||||
update quality:a,driveshaft_odom+=10000;
|
||||
update quality:a,TIME_ADVANCE_STEP+=1;
|
||||
.
|
||||
@ -0,0 +1,91 @@
|
||||
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 engine_oil(a)=
|
||||
preconditions:
|
||||
quality:a,oil_odom>=6000;
|
||||
quality:a,oil_vio=false;
|
||||
postconditions:
|
||||
update quality:a,oil_vio=true;
|
||||
update quality:a,compliance_vio=true;
|
||||
.
|
||||
|
||||
exploit driveshaft_boots(a)=
|
||||
preconditions:
|
||||
quality:a,driveshaft_odom>=12000;
|
||||
quality:a,driveshaft_vio=false;
|
||||
postconditions:
|
||||
update quality:a,driveshaft_vio=true;
|
||||
update quality:a,compliance_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 exhaust_service(a)=
|
||||
preconditions:
|
||||
quality:a,exhaust_months>=12;
|
||||
quality:a,exhaust_vio=true;
|
||||
postconditions:
|
||||
update quality:a,exhaust_months=0;
|
||||
update quality:a,exhaust_vio=false;
|
||||
.
|
||||
|
||||
exploit time_advance(a)=
|
||||
preconditions:
|
||||
quality:a,TIME_ADVANCE_STEP<13;
|
||||
quality:a,brake_months<6;
|
||||
quality:a,brake_vio=false;
|
||||
quality:a,exhaust_months<12;
|
||||
quality:a,exhaust_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,oil_odom+=10000;
|
||||
update quality:a,driveshaft_odom+=10000;
|
||||
update quality:a,TIME_ADVANCE_STEP+=1;
|
||||
.
|
||||
@ -0,0 +1,102 @@
|
||||
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 engine_oil(a)=
|
||||
preconditions:
|
||||
quality:a,oil_odom>=6000;
|
||||
quality:a,oil_vio=false;
|
||||
postconditions:
|
||||
update quality:a,oil_vio=true;
|
||||
update quality:a,compliance_vio=true;
|
||||
.
|
||||
|
||||
exploit driveshaft_boots(a)=
|
||||
preconditions:
|
||||
quality:a,driveshaft_odom>=12000;
|
||||
quality:a,driveshaft_vio=false;
|
||||
postconditions:
|
||||
update quality:a,driveshaft_vio=true;
|
||||
update quality:a,compliance_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 exhaust_service(a)=
|
||||
preconditions:
|
||||
quality:a,exhaust_months>=12;
|
||||
quality:a,exhaust_vio=true;
|
||||
postconditions:
|
||||
update quality:a,exhaust_months=0;
|
||||
update quality:a,exhaust_vio=false;
|
||||
.
|
||||
|
||||
exploit ac_service(a)=
|
||||
preconditions:
|
||||
quality:a,ac_odometer>=12000;
|
||||
quality:a,ac_vio=true;
|
||||
postconditions:
|
||||
update quality:a,ac_odometer=0;
|
||||
update quality:a,ac_vio=false;
|
||||
.
|
||||
|
||||
exploit time_advance(a)=
|
||||
preconditions:
|
||||
quality:a,TIME_ADVANCE_STEP<13;
|
||||
quality:a,brake_vio=false;
|
||||
quality:a,exhaust_vio=false;
|
||||
quality:a,ac_vio=false;
|
||||
quality:a,brake_months<6;
|
||||
quality:a,exhaust_months<12;
|
||||
quality:a,ac_odometer<12000;
|
||||
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,oil_odom+=10000;
|
||||
update quality:a,driveshaft_odom+=10000;
|
||||
update quality:a,TIME_ADVANCE_STEP+=1;
|
||||
.
|
||||
26075
Oct_2021/Non_Sync/6_Exploits/3_Serv/states.txt
Normal file
26075
Oct_2021/Non_Sync/6_Exploits/3_Serv/states.txt
Normal file
File diff suppressed because it is too large
Load Diff
@ -0,0 +1,114 @@
|
||||
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 engine_oil(a)=
|
||||
preconditions:
|
||||
quality:a,oil_odom>=6000;
|
||||
quality:a,oil_vio=false;
|
||||
postconditions:
|
||||
update quality:a,oil_vio=true;
|
||||
update quality:a,compliance_vio=true;
|
||||
.
|
||||
|
||||
exploit driveshaft_boots(a)=
|
||||
preconditions:
|
||||
quality:a,driveshaft_odom>=12000;
|
||||
quality:a,driveshaft_vio=false;
|
||||
postconditions:
|
||||
update quality:a,driveshaft_vio=true;
|
||||
update quality:a,compliance_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 exhaust_service(a)=
|
||||
preconditions:
|
||||
quality:a,exhaust_months>=12;
|
||||
quality:a,exhaust_vio=true;
|
||||
postconditions:
|
||||
update quality:a,exhaust_months=0;
|
||||
update quality:a,exhaust_vio=false;
|
||||
.
|
||||
|
||||
exploit ac_service(a)=
|
||||
preconditions:
|
||||
quality:a,ac_odometer>=12000;
|
||||
quality:a,ac_vio=true;
|
||||
postconditions:
|
||||
update quality:a,ac_odometer=0;
|
||||
update quality:a,ac_vio=false;
|
||||
.
|
||||
|
||||
exploit vacuum_service(a)=
|
||||
preconditions:
|
||||
quality:a,vacuum_odometer>=120000;
|
||||
quality:a,vacuum_vio=true;
|
||||
postconditions:
|
||||
update quality:a,vacuum_odometer=0;
|
||||
update quality:a,vacuum_vio=false;
|
||||
.
|
||||
|
||||
exploit time_advance(a)=
|
||||
preconditions:
|
||||
quality:a,TIME_ADVANCE_STEP<13;
|
||||
quality:a,brake_vio=false;
|
||||
quality:a,exhaust_vio=false;
|
||||
quality:a,ac_vio=false;
|
||||
quality:a,vacuum_vio=false;
|
||||
quality:a,brake_months<6;
|
||||
quality:a,exhaust_months<12;
|
||||
quality:a,ac_odometer<12000;
|
||||
quality:a,vacuum_odometer<120000;
|
||||
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,oil_odom+=10000;
|
||||
update quality:a,driveshaft_odom+=10000;
|
||||
update quality:a,TIME_ADVANCE_STEP+=1;
|
||||
.
|
||||
|
||||
@ -0,0 +1,124 @@
|
||||
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 engine_oil(a)=
|
||||
preconditions:
|
||||
quality:a,oil_odom>=6000;
|
||||
quality:a,oil_vio=false;
|
||||
postconditions:
|
||||
update quality:a,oil_vio=true;
|
||||
update quality:a,compliance_vio=true;
|
||||
.
|
||||
|
||||
exploit driveshaft_boots(a)=
|
||||
preconditions:
|
||||
quality:a,driveshaft_odom>=12000;
|
||||
quality:a,driveshaft_vio=false;
|
||||
postconditions:
|
||||
update quality:a,driveshaft_vio=true;
|
||||
update quality:a,compliance_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 exhaust_service(a)=
|
||||
preconditions:
|
||||
quality:a,exhaust_months>=12;
|
||||
quality:a,exhaust_vio=true;
|
||||
postconditions:
|
||||
update quality:a,exhaust_months=0;
|
||||
update quality:a,exhaust_vio=false;
|
||||
.
|
||||
|
||||
exploit ac_service(a)=
|
||||
preconditions:
|
||||
quality:a,ac_odometer>=12000;
|
||||
quality:a,ac_vio=true;
|
||||
postconditions:
|
||||
update quality:a,ac_odometer=0;
|
||||
update quality:a,ac_vio=false;
|
||||
.
|
||||
|
||||
exploit vacuum_service(a)=
|
||||
preconditions:
|
||||
quality:a,vacuum_odometer>=120000;
|
||||
quality:a,vacuum_vio=true;
|
||||
postconditions:
|
||||
update quality:a,vacuum_odometer=0;
|
||||
update quality:a,vacuum_vio=false;
|
||||
.
|
||||
|
||||
exploit oil_service(a)=
|
||||
preconditions:
|
||||
quality:a,oil_odom>=6000;
|
||||
quality:a,oil_vio=true;
|
||||
postconditions:
|
||||
update quality:a,oil_odom=0;
|
||||
update quality:a,oil_vio=false;
|
||||
.
|
||||
|
||||
exploit time_advance(a)=
|
||||
preconditions:
|
||||
quality:a,TIME_ADVANCE_STEP<13;
|
||||
quality:a,brake_vio=false;
|
||||
quality:a,exhaust_vio=false;
|
||||
quality:a,ac_vio=false;
|
||||
quality:a,vacuum_vio=false;
|
||||
quality:a,oil_vio=false;
|
||||
quality:a,brake_months<6;
|
||||
quality:a,exhaust_months<12;
|
||||
quality:a,ac_odometer<12000;
|
||||
quality:a,vacuum_odometer<120000;
|
||||
quality:a,oil_odom<6000;
|
||||
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,oil_odom+=10000;
|
||||
update quality:a,driveshaft_odom+=10000;
|
||||
update quality:a,TIME_ADVANCE_STEP+=1;
|
||||
.
|
||||
@ -0,0 +1,135 @@
|
||||
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 engine_oil(a)=
|
||||
preconditions:
|
||||
quality:a,oil_odom>=6000;
|
||||
quality:a,oil_vio=false;
|
||||
postconditions:
|
||||
update quality:a,oil_vio=true;
|
||||
update quality:a,compliance_vio=true;
|
||||
.
|
||||
|
||||
exploit driveshaft_boots(a)=
|
||||
preconditions:
|
||||
quality:a,driveshaft_odom>=12000;
|
||||
quality:a,driveshaft_vio=false;
|
||||
postconditions:
|
||||
update quality:a,driveshaft_vio=true;
|
||||
update quality:a,compliance_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 exhaust_service(a)=
|
||||
preconditions:
|
||||
quality:a,exhaust_months>=12;
|
||||
quality:a,exhaust_vio=true;
|
||||
postconditions:
|
||||
update quality:a,exhaust_months=0;
|
||||
update quality:a,exhaust_vio=false;
|
||||
.
|
||||
|
||||
exploit ac_service(a)=
|
||||
preconditions:
|
||||
quality:a,ac_odometer>=12000;
|
||||
quality:a,ac_vio=true;
|
||||
postconditions:
|
||||
update quality:a,ac_odometer=0;
|
||||
update quality:a,ac_vio=false;
|
||||
.
|
||||
|
||||
exploit vacuum_service(a)=
|
||||
preconditions:
|
||||
quality:a,vacuum_odometer>=120000;
|
||||
quality:a,vacuum_vio=true;
|
||||
postconditions:
|
||||
update quality:a,vacuum_odometer=0;
|
||||
update quality:a,vacuum_vio=false;
|
||||
.
|
||||
|
||||
exploit oil_service(a)=
|
||||
preconditions:
|
||||
quality:a,oil_odom>=6000;
|
||||
quality:a,oil_vio=true;
|
||||
postconditions:
|
||||
update quality:a,oil_odom=0;
|
||||
update quality:a,oil_vio=false;
|
||||
.
|
||||
|
||||
exploit driveshaft_service(a)=
|
||||
preconditions:
|
||||
quality:a,driveshaft_odom>=12000;
|
||||
quality:a,driveshaft_vio=true;
|
||||
postconditions:
|
||||
update quality:a,driveshaft_odom=0;
|
||||
update quality:a,driveshaft_vio=false;
|
||||
.
|
||||
|
||||
exploit time_advance(a)=
|
||||
preconditions:
|
||||
quality:a,TIME_ADVANCE_STEP<13;
|
||||
quality:a,brake_vio=false;
|
||||
quality:a,exhaust_vio=false;
|
||||
quality:a,ac_vio=false;
|
||||
quality:a,vacuum_vio=false;
|
||||
quality:a,oil_vio=false;
|
||||
quality:a,driveshaft_vio=false;
|
||||
quality:a,brake_months<6;
|
||||
quality:a,exhaust_months<12;
|
||||
quality:a,ac_odometer<12000;
|
||||
quality:a,vacuum_odometer<120000;
|
||||
quality:a,oil_odom<6000;
|
||||
quality:a,driveshaft_odom<12000;
|
||||
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,oil_odom+=10000;
|
||||
update quality:a,driveshaft_odom+=10000;
|
||||
update quality:a,TIME_ADVANCE_STEP+=1;
|
||||
.
|
||||
80
Oct_2021/Sync/6_Exploits/1_Serv/sync_timeline_maintenance.xp
Normal file
80
Oct_2021/Sync/6_Exploits/1_Serv/sync_timeline_maintenance.xp
Normal file
@ -0,0 +1,80 @@
|
||||
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 engine_oil(a)=
|
||||
preconditions:
|
||||
quality:a,oil_odom>=6000;
|
||||
quality:a,oil_vio=false;
|
||||
postconditions:
|
||||
update quality:a,oil_vio=true;
|
||||
update quality:a,compliance_vio=true;
|
||||
.
|
||||
|
||||
exploit driveshaft_boots(a)=
|
||||
preconditions:
|
||||
quality:a,driveshaft_odom>=12000;
|
||||
quality:a,driveshaft_vio=false;
|
||||
postconditions:
|
||||
update quality:a,driveshaft_vio=true;
|
||||
update quality:a,compliance_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;
|
||||
.
|
||||
|
||||
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,oil_odom+=10000;
|
||||
update quality:a,driveshaft_odom+=10000;
|
||||
update quality:a,TIME_ADVANCE_STEP+=1;
|
||||
.
|
||||
91
Oct_2021/Sync/6_Exploits/2_Serv/sync_timeline_maintenance.xp
Normal file
91
Oct_2021/Sync/6_Exploits/2_Serv/sync_timeline_maintenance.xp
Normal file
@ -0,0 +1,91 @@
|
||||
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 engine_oil(a)=
|
||||
preconditions:
|
||||
quality:a,oil_odom>=6000;
|
||||
quality:a,oil_vio=false;
|
||||
postconditions:
|
||||
update quality:a,oil_vio=true;
|
||||
update quality:a,compliance_vio=true;
|
||||
.
|
||||
|
||||
exploit driveshaft_boots(a)=
|
||||
preconditions:
|
||||
quality:a,driveshaft_odom>=12000;
|
||||
quality:a,driveshaft_vio=false;
|
||||
postconditions:
|
||||
update quality:a,driveshaft_vio=true;
|
||||
update quality:a,compliance_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 exhaust_service(a)=
|
||||
preconditions:
|
||||
quality:a,exhaust_months>=12;
|
||||
quality:a,exhaust_vio=true;
|
||||
postconditions:
|
||||
update quality:a,exhaust_months=0;
|
||||
update quality:a,exhaust_vio=false;
|
||||
.
|
||||
|
||||
time group exploit time_advance(a)=
|
||||
preconditions:
|
||||
quality:a,TIME_ADVANCE_STEP<13;
|
||||
quality:a,brake_months<6;
|
||||
quality:a,brake_vio=false;
|
||||
quality:a,exhaust_months<12;
|
||||
quality:a,exhaust_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,oil_odom+=10000;
|
||||
update quality:a,driveshaft_odom+=10000;
|
||||
update quality:a,TIME_ADVANCE_STEP+=1;
|
||||
.
|
||||
26075
Oct_2021/Sync/6_Exploits/3_Serv/states.txt
Normal file
26075
Oct_2021/Sync/6_Exploits/3_Serv/states.txt
Normal file
File diff suppressed because it is too large
Load Diff
102
Oct_2021/Sync/6_Exploits/3_Serv/sync_timeline_maintenance.xp
Normal file
102
Oct_2021/Sync/6_Exploits/3_Serv/sync_timeline_maintenance.xp
Normal file
@ -0,0 +1,102 @@
|
||||
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 engine_oil(a)=
|
||||
preconditions:
|
||||
quality:a,oil_odom>=6000;
|
||||
quality:a,oil_vio=false;
|
||||
postconditions:
|
||||
update quality:a,oil_vio=true;
|
||||
update quality:a,compliance_vio=true;
|
||||
.
|
||||
|
||||
exploit driveshaft_boots(a)=
|
||||
preconditions:
|
||||
quality:a,driveshaft_odom>=12000;
|
||||
quality:a,driveshaft_vio=false;
|
||||
postconditions:
|
||||
update quality:a,driveshaft_vio=true;
|
||||
update quality:a,compliance_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 exhaust_service(a)=
|
||||
preconditions:
|
||||
quality:a,exhaust_months>=12;
|
||||
quality:a,exhaust_vio=true;
|
||||
postconditions:
|
||||
update quality:a,exhaust_months=0;
|
||||
update quality:a,exhaust_vio=false;
|
||||
.
|
||||
|
||||
exploit ac_service(a)=
|
||||
preconditions:
|
||||
quality:a,ac_odometer>=12000;
|
||||
quality:a,ac_vio=true;
|
||||
postconditions:
|
||||
update quality:a,ac_odometer=0;
|
||||
update quality:a,ac_vio=false;
|
||||
.
|
||||
|
||||
time group exploit time_advance(a)=
|
||||
preconditions:
|
||||
quality:a,TIME_ADVANCE_STEP<13;
|
||||
quality:a,brake_vio=false;
|
||||
quality:a,exhaust_vio=false;
|
||||
quality:a,ac_vio=false;
|
||||
quality:a,brake_months<6;
|
||||
quality:a,exhaust_months<12;
|
||||
quality:a,ac_odometer<12000;
|
||||
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,oil_odom+=10000;
|
||||
update quality:a,driveshaft_odom+=10000;
|
||||
update quality:a,TIME_ADVANCE_STEP+=1;
|
||||
.
|
||||
114
Oct_2021/Sync/6_Exploits/4_Serv/sync_timeline_maintenance.xp
Normal file
114
Oct_2021/Sync/6_Exploits/4_Serv/sync_timeline_maintenance.xp
Normal file
@ -0,0 +1,114 @@
|
||||
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 engine_oil(a)=
|
||||
preconditions:
|
||||
quality:a,oil_odom>=6000;
|
||||
quality:a,oil_vio=false;
|
||||
postconditions:
|
||||
update quality:a,oil_vio=true;
|
||||
update quality:a,compliance_vio=true;
|
||||
.
|
||||
|
||||
exploit driveshaft_boots(a)=
|
||||
preconditions:
|
||||
quality:a,driveshaft_odom>=12000;
|
||||
quality:a,driveshaft_vio=false;
|
||||
postconditions:
|
||||
update quality:a,driveshaft_vio=true;
|
||||
update quality:a,compliance_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 exhaust_service(a)=
|
||||
preconditions:
|
||||
quality:a,exhaust_months>=12;
|
||||
quality:a,exhaust_vio=true;
|
||||
postconditions:
|
||||
update quality:a,exhaust_months=0;
|
||||
update quality:a,exhaust_vio=false;
|
||||
.
|
||||
|
||||
exploit ac_service(a)=
|
||||
preconditions:
|
||||
quality:a,ac_odometer>=12000;
|
||||
quality:a,ac_vio=true;
|
||||
postconditions:
|
||||
update quality:a,ac_odometer=0;
|
||||
update quality:a,ac_vio=false;
|
||||
.
|
||||
|
||||
exploit vacuum_service(a)=
|
||||
preconditions:
|
||||
quality:a,vacuum_odometer>=120000;
|
||||
quality:a,vacuum_vio=true;
|
||||
postconditions:
|
||||
update quality:a,vacuum_odometer=0;
|
||||
update quality:a,vacuum_vio=false;
|
||||
.
|
||||
|
||||
time group exploit time_advance(a)=
|
||||
preconditions:
|
||||
quality:a,TIME_ADVANCE_STEP<13;
|
||||
quality:a,brake_vio=false;
|
||||
quality:a,exhaust_vio=false;
|
||||
quality:a,ac_vio=false;
|
||||
quality:a,vacuum_vio=false;
|
||||
quality:a,brake_months<6;
|
||||
quality:a,exhaust_months<12;
|
||||
quality:a,ac_odometer<12000;
|
||||
quality:a,vacuum_odometer<120000;
|
||||
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,oil_odom+=10000;
|
||||
update quality:a,driveshaft_odom+=10000;
|
||||
update quality:a,TIME_ADVANCE_STEP+=1;
|
||||
.
|
||||
|
||||
124
Oct_2021/Sync/6_Exploits/5_Serv/sync_timeline_maintenance.xp
Normal file
124
Oct_2021/Sync/6_Exploits/5_Serv/sync_timeline_maintenance.xp
Normal file
@ -0,0 +1,124 @@
|
||||
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 engine_oil(a)=
|
||||
preconditions:
|
||||
quality:a,oil_odom>=6000;
|
||||
quality:a,oil_vio=false;
|
||||
postconditions:
|
||||
update quality:a,oil_vio=true;
|
||||
update quality:a,compliance_vio=true;
|
||||
.
|
||||
|
||||
exploit driveshaft_boots(a)=
|
||||
preconditions:
|
||||
quality:a,driveshaft_odom>=12000;
|
||||
quality:a,driveshaft_vio=false;
|
||||
postconditions:
|
||||
update quality:a,driveshaft_vio=true;
|
||||
update quality:a,compliance_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 exhaust_service(a)=
|
||||
preconditions:
|
||||
quality:a,exhaust_months>=12;
|
||||
quality:a,exhaust_vio=true;
|
||||
postconditions:
|
||||
update quality:a,exhaust_months=0;
|
||||
update quality:a,exhaust_vio=false;
|
||||
.
|
||||
|
||||
exploit ac_service(a)=
|
||||
preconditions:
|
||||
quality:a,ac_odometer>=12000;
|
||||
quality:a,ac_vio=true;
|
||||
postconditions:
|
||||
update quality:a,ac_odometer=0;
|
||||
update quality:a,ac_vio=false;
|
||||
.
|
||||
|
||||
exploit vacuum_service(a)=
|
||||
preconditions:
|
||||
quality:a,vacuum_odometer>=120000;
|
||||
quality:a,vacuum_vio=true;
|
||||
postconditions:
|
||||
update quality:a,vacuum_odometer=0;
|
||||
update quality:a,vacuum_vio=false;
|
||||
.
|
||||
|
||||
exploit oil_service(a)=
|
||||
preconditions:
|
||||
quality:a,oil_odom>=6000;
|
||||
quality:a,oil_vio=true;
|
||||
postconditions:
|
||||
update quality:a,oil_odom=0;
|
||||
update quality:a,oil_vio=false;
|
||||
.
|
||||
|
||||
time group exploit time_advance(a)=
|
||||
preconditions:
|
||||
quality:a,TIME_ADVANCE_STEP<13;
|
||||
quality:a,brake_vio=false;
|
||||
quality:a,exhaust_vio=false;
|
||||
quality:a,ac_vio=false;
|
||||
quality:a,vacuum_vio=false;
|
||||
quality:a,oil_vio=false;
|
||||
quality:a,brake_months<6;
|
||||
quality:a,exhaust_months<12;
|
||||
quality:a,ac_odometer<12000;
|
||||
quality:a,vacuum_odometer<120000;
|
||||
quality:a,oil_odom<6000;
|
||||
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,oil_odom+=10000;
|
||||
update quality:a,driveshaft_odom+=10000;
|
||||
update quality:a,TIME_ADVANCE_STEP+=1;
|
||||
.
|
||||
135
Oct_2021/Sync/6_Exploits/6_Serv/sync_timeline_maintenance.xp
Normal file
135
Oct_2021/Sync/6_Exploits/6_Serv/sync_timeline_maintenance.xp
Normal file
@ -0,0 +1,135 @@
|
||||
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 engine_oil(a)=
|
||||
preconditions:
|
||||
quality:a,oil_odom>=6000;
|
||||
quality:a,oil_vio=false;
|
||||
postconditions:
|
||||
update quality:a,oil_vio=true;
|
||||
update quality:a,compliance_vio=true;
|
||||
.
|
||||
|
||||
exploit driveshaft_boots(a)=
|
||||
preconditions:
|
||||
quality:a,driveshaft_odom>=12000;
|
||||
quality:a,driveshaft_vio=false;
|
||||
postconditions:
|
||||
update quality:a,driveshaft_vio=true;
|
||||
update quality:a,compliance_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 exhaust_service(a)=
|
||||
preconditions:
|
||||
quality:a,exhaust_months>=12;
|
||||
quality:a,exhaust_vio=true;
|
||||
postconditions:
|
||||
update quality:a,exhaust_months=0;
|
||||
update quality:a,exhaust_vio=false;
|
||||
.
|
||||
|
||||
exploit ac_service(a)=
|
||||
preconditions:
|
||||
quality:a,ac_odometer>=12000;
|
||||
quality:a,ac_vio=true;
|
||||
postconditions:
|
||||
update quality:a,ac_odometer=0;
|
||||
update quality:a,ac_vio=false;
|
||||
.
|
||||
|
||||
exploit vacuum_service(a)=
|
||||
preconditions:
|
||||
quality:a,vacuum_odometer>=120000;
|
||||
quality:a,vacuum_vio=true;
|
||||
postconditions:
|
||||
update quality:a,vacuum_odometer=0;
|
||||
update quality:a,vacuum_vio=false;
|
||||
.
|
||||
|
||||
exploit oil_service(a)=
|
||||
preconditions:
|
||||
quality:a,oil_odom>=6000;
|
||||
quality:a,oil_vio=true;
|
||||
postconditions:
|
||||
update quality:a,oil_odom=0;
|
||||
update quality:a,oil_vio=false;
|
||||
.
|
||||
|
||||
exploit driveshaft_service(a)=
|
||||
preconditions:
|
||||
quality:a,driveshaft_odom>=12000;
|
||||
quality:a,driveshaft_vio=true;
|
||||
postconditions:
|
||||
update quality:a,driveshaft_odom=0;
|
||||
update quality:a,driveshaft_vio=false;
|
||||
.
|
||||
|
||||
time group exploit time_advance(a)=
|
||||
preconditions:
|
||||
quality:a,TIME_ADVANCE_STEP<13;
|
||||
quality:a,brake_vio=false;
|
||||
quality:a,exhaust_vio=false;
|
||||
quality:a,ac_vio=false;
|
||||
quality:a,vacuum_vio=false;
|
||||
quality:a,oil_vio=false;
|
||||
quality:a,driveshaft_vio=false;
|
||||
quality:a,brake_months<6;
|
||||
quality:a,exhaust_months<12;
|
||||
quality:a,ac_odometer<12000;
|
||||
quality:a,vacuum_odometer<120000;
|
||||
quality:a,oil_odom<6000;
|
||||
quality:a,driveshaft_odom<12000;
|
||||
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,oil_odom+=10000;
|
||||
update quality:a,driveshaft_odom+=10000;
|
||||
update quality:a,TIME_ADVANCE_STEP+=1;
|
||||
.
|
||||
Loading…
x
Reference in New Issue
Block a user