format_version: "0.1"
properties:
  - id: P1
    kind: invariant
    expression: "!pressure_high || vent_valve"
    justification: "The independent high-pressure trip must vent whenever pressure is high, regardless of what the batch sequencer is doing."