properties:
  - id: P1
    kind: mutual_exclusion
    variables: [KM_CW, KM_CCW]
    justification: "Both contactors must never close together: that shorts two supply phases across the reversing contacts."