format_version: "0.1"
id: welder_gas_shield_interlock
name: "MIG welder shielding-gas interlock"
domain: manufacturing
language: ST
source:
  origin: authored
  reference: "Authored for the esbmc-plc-benchmark-suite to add a single-scan, single-output interlock example distinct from the corpus's dominant peer-actuator mutual_exclusion shape."
  license: CC-BY-4.0
properties_file: props.yaml
validation_status: candidate
variants:
  - file: clean.st
    expected_verdict: true
    ground_truth:
      method: expert
      confirmed_by: [Pierre Dantas]
  - file: bomb.st
    expected_verdict: false
    violated_properties: [P1]
    ground_truth:
      method: fault-injection
      base_variant: clean.st
      seeded_defect: "Split the single IF/ELSIF/ELSE dispatch into two independent IF statements, so the trigger branch no longer re-checks gas_flow_ok and overwrites the dropout branch's FALSE whenever it executes afterward."
      witness: "gas_flow_ok=0, trigger_pull=1 (single scan) reaches arc_on=1 with gas flow lost."
features: [contacts, coils, interlock]
difficulty: easy
tags: [safety, interlock, welding, arc-control]