Section 6: Warnings

• Type 7: Action Ac_controller_repair(a15) performs identity as state transformation to variable system_fail33(sv33).
• Type 7: Action Ac_controller_failure(a16) performs identity as state transformation to variable system_fail33(sv33).
• Type 7: Action Ac_disk_repair(a20) performs identity as state transformation to variable system_fail33(sv33).
• Type 7: Action Ac_disk_failure(a21) performs identity as state transformation to variable system_fail33(sv33).
• Type 7: Action Ac_disk_repair(a26) performs identity as state transformation to variable system_fail33(sv33).
• Type 7: Action Ac_disk_failure(a27) performs identity as state transformation to variable system_fail33(sv33).
• Type 7: Action Ac_processor_repair(a32) performs identity as state transformation to variable system_fail33(sv33).
• Type 7: Action Ac_processor_failure(a33) performs identity as state transformation to variable system_fail33(sv33).
• Type 7: Action Ac_disk_repair(a6) performs identity as state transformation to variable system_fail33(sv33).
• Type 7: Action Ac_disk_failure(a7) performs identity as state transformation to variable system_fail33(sv33).
• Type 11: Variable system_fail33(sv33) is not element of any variable invariant computed for the linear state transformations performed by the actions of this trace.