cebf8c167a
Folds three previously-separate pieces into one preliminary-example repo for the HAHACS thesis: - thesis/ (submodule) → gitea Thesis.git — the PhD proposal - fret-pipeline/ — FRET requirements to AIGER controller (was ~/Documents/fret_processing/; prior single-commit history abandoned per user decision) - plant-model/ — 10-state PKE + lumped T/H PWR model (was ~/Documents/PKE_Playground/; never version-controlled before) - presentations/2026DICE/ (submodule) → gitea 2026DICE.git - reachability/, hardware/ — empty placeholders for Thrust 3 and HIL - docs/architecture.md — how the discrete and continuous layers compose - claude_memory/ — session notes and scratch knowledge pattern Plant model refactored to thesis naming (x, plant, u, ref); pke_th_rhs now takes u as an explicit arg instead of reading rho_ext from the params struct. First two controllers built to the contract u = ctrl_<mode>(t, x, plant, ref): ctrl_null (baseline) and ctrl_operation (stabilizing, proportional on T_avg). Validated under a 100% -> 80% Q_sg step: ctrl_operation reduces steady-state T_avg drift ~47% vs. the unforced plant. Root CLAUDE.md emphasizes that CLAUDE.md files are living documents and that any knowledge not captured before a session ends is lost forever; claude_memory/ holds the session-level notes that haven't stabilized enough to graduate into a CLAUDE.md. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
144 lines
5.3 KiB
Markdown
144 lines
5.3 KiB
Markdown
# 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
|