Remove CLAUDE.md from tracking, add to gitignore
Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
This commit is contained in:
parent
d03604c363
commit
e9ed9e252e
3
.gitignore
vendored
3
.gitignore
vendored
@ -36,6 +36,9 @@ Thumbs.db
|
|||||||
*.swo
|
*.swo
|
||||||
.vscode/
|
.vscode/
|
||||||
.idea/
|
.idea/
|
||||||
|
|
||||||
|
# Claude Code
|
||||||
|
CLAUDE.md
|
||||||
*.sty
|
*.sty
|
||||||
.DS_Store
|
.DS_Store
|
||||||
*.aux
|
*.aux
|
||||||
|
|||||||
133
CLAUDE.md
133
CLAUDE.md
@ -1,133 +0,0 @@
|
|||||||
# CLAUDE.md
|
|
||||||
|
|
||||||
This file provides guidance to Claude Code (claude.ai/code) when working with code in this repository.
|
|
||||||
|
|
||||||
## Project Overview
|
|
||||||
|
|
||||||
This is a PhD thesis proposal for developing a methodology to build High-Assurance Hybrid Autonomous Control Systems (HAHACS) for critical infrastructure. The proposal is titled "From Cold Start to Critical: Formal Synthesis of Autonomous Hybrid Controllers."
|
|
||||||
|
|
||||||
**Intellectual Merit**: The contribution is architectural unification rather than algorithmic novelty. The methodology provides a systematic decomposition mapping verification techniques to control mode types, composing existing formal methods into a complete framework where none existed.
|
|
||||||
|
|
||||||
**Key Insight**: The methodology formalizes EXISTING discrete abstractions from operating procedures (especially nuclear) rather than imposing arbitrary ones. Operating procedures already define go/no-go conditions as discrete predicates - this work provides the formalization and verification framework.
|
|
||||||
|
|
||||||
## Document Structure
|
|
||||||
|
|
||||||
The proposal uses a modular LaTeX structure with numbered section directories:
|
|
||||||
- `main.tex` - Root document that inputs all sections
|
|
||||||
- `1-goals-and-outcomes/` - Research statement and goals
|
|
||||||
- `2-state-of-the-art/` - Literature review
|
|
||||||
- `3-research-approach/` - Core methodology (CURRENTLY ACTIVE WORK)
|
|
||||||
- `4-metrics-of-success/` - Success criteria
|
|
||||||
- `5-risks-and-contingencies/` - Risk analysis
|
|
||||||
- `6-broader-impacts/` - Broader impacts
|
|
||||||
- `8-schedule/` - Timeline
|
|
||||||
|
|
||||||
Each section directory contains:
|
|
||||||
- `v1.tex` (or `v2.tex` for actively revised sections) - Main content
|
|
||||||
- `outline.md` (optional) - Planning notes and structure
|
|
||||||
|
|
||||||
**IMPORTANT**: Section 3 (research-approach) is currently being revised. `main.tex` inputs `v2.tex` for this section, which contains extensive inline comments and questions prefixed with `%` and `% Q:`.
|
|
||||||
|
|
||||||
## Building the Document
|
|
||||||
|
|
||||||
```bash
|
|
||||||
# Full build with bibliography
|
|
||||||
pdflatex main.tex
|
|
||||||
bibtex main
|
|
||||||
pdflatex main.tex
|
|
||||||
pdflatex main.tex
|
|
||||||
|
|
||||||
# Quick build (no bibliography updates)
|
|
||||||
pdflatex main.tex
|
|
||||||
|
|
||||||
# Use latexmk for automated builds
|
|
||||||
latexmk -pdf main.tex
|
|
||||||
|
|
||||||
# Clean auxiliary files
|
|
||||||
latexmk -c
|
|
||||||
```
|
|
||||||
|
|
||||||
The output is `main.pdf`.
|
|
||||||
|
|
||||||
## Key Technical Concepts
|
|
||||||
|
|
||||||
### Mathematical Notation
|
|
||||||
- **Continuous state space**: X ⊆ ℝⁿ
|
|
||||||
- **Discrete modes**: Q = {q₁, q₂, ...}
|
|
||||||
- **Per-mode continuous regions**: X_entry,i, X_exit,i, X_safe,i
|
|
||||||
- **Discrete predicates**: pᵢ: X → {true, false} (Boolean functions over continuous state)
|
|
||||||
|
|
||||||
### Three Control Mode Types
|
|
||||||
Each mode type has distinct control objectives and verification methods:
|
|
||||||
|
|
||||||
1. **Transitory modes**: Transition between discrete states
|
|
||||||
- Objective: reach(X_entry) → reach(X_exit) while maintaining x(t) ∈ X_safe
|
|
||||||
- Verification: Reachability analysis
|
|
||||||
- Formal: Reach(X_entry, f(x,u), T) ⊆ X_exit ∪ X_safe
|
|
||||||
|
|
||||||
2. **Stabilizing modes**: Maintain steady state
|
|
||||||
- Objective: remain(X_target) where X_target ⊂ X_safe
|
|
||||||
- Verification: Barrier certificates
|
|
||||||
- Formal: ∇B(x)·f(x,u) ≤ 0 on boundary ∂X_safe
|
|
||||||
|
|
||||||
3. **Expulsory modes**: Safe shutdown under failures
|
|
||||||
- Objective: reach(X_current) → reach(X_safe_shutdown) under parametric uncertainty
|
|
||||||
- Verification: Parametric robust reachability
|
|
||||||
- Formal: Reach(X_current, f(x,u,θ), T) ⊆ X_safe_shutdown for all θ ∈ Θ_failure
|
|
||||||
|
|
||||||
### Scope Boundaries
|
|
||||||
- **Verify** continuous controllers, not **synthesize** them (analogous to model checking)
|
|
||||||
- Assume controllers can be designed using standard control theory
|
|
||||||
- Contribution is verification that candidate controllers compose correctly with discrete layer
|
|
||||||
|
|
||||||
## Active Development Context
|
|
||||||
|
|
||||||
### Current Focus (as of 2026-01-26)
|
|
||||||
Editing the research approach section (`3-research-approach/v2.tex`) with a Wednesday (2026-01-28) draft deadline.
|
|
||||||
|
|
||||||
### Open Technical Questions
|
|
||||||
Questions are embedded in `v2.tex` comments. Key unresolved issues:
|
|
||||||
|
|
||||||
**Easier to address:**
|
|
||||||
- Hysteresis and sensor noise handling (standard control theory)
|
|
||||||
- Mealy machine formalization (presentation issue)
|
|
||||||
- Failure detection scope boundaries (precision in claims)
|
|
||||||
|
|
||||||
**More challenging:**
|
|
||||||
- Timing constraint verification (timed automata integration)
|
|
||||||
- Parametric uncertainty bounds methodology
|
|
||||||
- Numerical precision in discrete abstraction (task 36 in taskwarrior)
|
|
||||||
- Controller design gap (scope vulnerability)
|
|
||||||
|
|
||||||
### Taskwarrior Integration
|
|
||||||
The user tracks tasks in taskwarrior. The Thesis project has ~45 tasks including:
|
|
||||||
- 9 writing tasks for research approach sections (due 2026-01-28)
|
|
||||||
- Multiple reading tasks on hybrid systems, reachability, formal methods
|
|
||||||
- Outstanding question (task 36): "How do we handle numerical barriers when creating discrete automata?"
|
|
||||||
|
|
||||||
Use `task list project:Thesis` to see current tasks.
|
|
||||||
|
|
||||||
## Bibliography
|
|
||||||
|
|
||||||
References are in `references.bib` using IEEE transaction format. The bibliography includes:
|
|
||||||
- Hybrid systems theory and verification
|
|
||||||
- Formal methods (reactive synthesis, temporal logic)
|
|
||||||
- Control theory (reachability, barrier certificates)
|
|
||||||
- Nuclear regulatory documents (NUREG, 10 CFR)
|
|
||||||
- Industrial control systems
|
|
||||||
|
|
||||||
## Custom LaTeX Class
|
|
||||||
|
|
||||||
`dane_proposal_format.cls` provides:
|
|
||||||
- NSF-compliant formatting (Times New Roman, 1" margins)
|
|
||||||
- Custom `\task{title}{description}` command for numbered tasks
|
|
||||||
- TikZ libraries for diagrams
|
|
||||||
- Table and figure formatting
|
|
||||||
- Default metadata (title, author, advisor)
|
|
||||||
|
|
||||||
## Writing Style Notes
|
|
||||||
|
|
||||||
- Inline comments in `.tex` files starting with `%` are working notes
|
|
||||||
- Comments with `% Q:` indicate open questions requiring research/decisions
|
|
||||||
- Sections marked with `\iffalse ... \fi` are draft text, not compiled
|
|
||||||
- Text after `\iffalse` blocks are outlines/notes for future writing
|
|
||||||
Loading…
x
Reference in New Issue
Block a user