18 lines
393 B
Plaintext
18 lines
393 B
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;
|
|
.
|
|
|
|
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;
|
|
.
|