format_version: "0.1"
properties:
  - id: P1
    kind: mutual_exclusion
    variables: [P1, P2]
    justification: "The two timed phases are mutually exclusive: a sequential chain never overlaps."