# DRC Spec Redesign -- Matching Figure 1 Hybrid Automaton

## Naming Convention

**Format: `DRC_XNNN_name`** where X is a category letter:

| Prefix | Category | Purpose |
|--------|----------|---------|
| `DRC_A___` | Architecture | Mode validity, structural constraints |
| `DRC_I___` | Initialization | Initial conditions |
| `DRC_S___` | Stay | Self-loop / remain-in-mode |
| `DRC_T___` | Transition | Mode-to-mode edges |

## Variable Mapping

### Outputs
| Variable | Type | Description |
|----------|------|-------------|
| `control_mode` | integer | Current discrete state (0-3) |

### Internal (enum constants)
| Variable | Type | Assignment | Description |
|----------|------|------------|-------------|
| `q_shutdown` | integer | 0 | Cold Shutdown mode |
| `q_heatup` | integer | 1 | Heatup mode |
| `q_operation` | integer | 2 | Power Operation mode |
| `q_scram` | integer | 3 | SCRAM mode |

### Inputs (boolean predicates over continuous state)
| Variable | Type | Description | Maps to |
|----------|------|-------------|---------|
| `t_avg_above_min` | boolean | T_avg > T_min | Guard: Shutdown -> Heatup |
| `t_avg_in_range` | boolean | T_avg in [T_op +/- delta] | Guard: Heatup -> Operation |
| `p_above_crit` | boolean | P > P_crit | Guard: Heatup -> Operation |
| `inv1_holds` | boolean | Invariant 1 OK | Safety: Heatup |
| `inv2_holds` | boolean | Invariant 2 OK | Safety: Operation |
| `manual_reset` | boolean | Operator reset command | Guard: SCRAM -> Shutdown |

## FRETish Requirements

### Architecture
```
DRC_A001_MODE_VALID:
  DRC shall always satisfy
  control_mode = q_shutdown | control_mode = q_heatup | control_mode = q_operation | control_mode = q_scram
```

### Initialization
```
DRC_I001_INIT_SHUTDOWN:
  DRC shall immediately satisfy control_mode = q_shutdown
```

### Stay Conditions (self-loops)
```
DRC_S001_SHUTDOWN_STAY:
  Whenever control_mode = q_shutdown & !t_avg_above_min
  DRC shall at the next timepoint satisfy control_mode = q_shutdown

DRC_S002_HEATUP_STAY:
  Whenever control_mode = q_heatup & inv1_holds & !(t_avg_in_range & p_above_crit)
  DRC shall at the next timepoint satisfy control_mode = q_heatup

DRC_S003_OPERATION_STAY:
  Whenever control_mode = q_operation & inv2_holds
  DRC shall at the next timepoint satisfy control_mode = q_operation

DRC_S004_SCRAM_STAY:
  Whenever control_mode = q_scram & !manual_reset
  DRC shall at the next timepoint satisfy control_mode = q_scram
```

### Transitions (edges in Figure 1)
```
DRC_T001_SHUTDOWN_TO_HEATUP:
  Upon control_mode = q_shutdown & t_avg_above_min
  DRC shall at the next timepoint satisfy control_mode = q_heatup

DRC_T002_HEATUP_TO_OPERATION:
  Upon control_mode = q_heatup & t_avg_in_range & p_above_crit
  DRC shall at the next timepoint satisfy control_mode = q_operation

DRC_T003_HEATUP_TO_SCRAM:
  Upon control_mode = q_heatup & !inv1_holds
  DRC shall at the next timepoint satisfy control_mode = q_scram

DRC_T004_OPERATION_TO_SCRAM:
  Upon control_mode = q_operation & !inv2_holds
  DRC shall at the next timepoint satisfy control_mode = q_scram

DRC_T005_SCRAM_TO_SHUTDOWN:
  Upon control_mode = q_scram & manual_reset
  DRC shall at the next timepoint satisfy control_mode = q_shutdown
```

## Transition Priority Note

DRC_S002 and DRC_T003 overlap when `control_mode = q_heatup & !inv1_holds &
!(t_avg_in_range & p_above_crit)`. Both fire -- S002 says stay in heatup,
T003 says go to scram. T003 should win (safety takes priority). To resolve:

**Option A:** Strengthen S002 to include inv1_holds (already done above).
When inv1 fails, S002 doesn't fire, only T003 does.

**Option B:** Add explicit priority requirement:
```
DRC_A002_SCRAM_PRIORITY:
  Whenever control_mode = q_heatup & !inv1_holds
  DRC shall at the next timepoint satisfy control_mode = q_scram
```

Similarly, DRC_S003 and DRC_T004: when `control_mode = q_operation & !inv2_holds`,
S003 doesn't fire (requires inv2_holds), only T004 fires. This is already
correct in the spec above.

## Key Differences from Original DRC Spec

1. **Single integer mode variable** instead of 5 independent boolean outputs
   - Mutual exclusivity is automatic
   - No vacuous satisfaction of scoped requirements

2. **Guard conditions as boolean inputs** instead of output variables
   - `t_avg_above_min` replaces continuous T_avg comparison
   - These are computed by the tactical (continuous) layer

3. **Complete transition coverage** -- every mode has explicit stay + transition rules
   - Original spec had no "stay" requirements, allowing trivial mode avoidance

4. **SCRAM is recoverable** (via manual_reset) instead of permanent latch
   - Matches Figure 1 which shows SCRAM -> Cold Shutdown recovery
   - Original PWR-0102 "If SCRAM always SCRAM" made op_mode unreachable

5. **Invariant violations as inputs** -- the environment reports invariant status
   - Original spec had sensor triggers (t_dot_exceeded) as inputs, which is the
     same concept but more directly connected to the automaton structure

## Boolean Abstraction for Synthesis

For ltlsynt, this translates directly:
- Inputs (6): t_avg_above_min, t_avg_in_range, p_above_crit, inv1_holds, inv2_holds, manual_reset
- Outputs (4): in_shutdown, in_heatup, in_operation, in_scram (with exclusivity)
- Environment assumptions: physical constraints on input combinations
- Guarantees: mode transitions from FRET requirements above