Add DAS reading comments as inline todonotes (cyan)

1-goals-and-outcomes/goals.tex

@@ -1,4 +1,9 @@
 \section{Goals and Outcomes}
+\dasinline{Research statement is very similar to GO
+because that's what I had when I prepared it.
+If it's going to be an executive summary, it
+should talk more about the other sections rather
+than just being a slightly different GO section.}
 
 % GOAL PARAGRAPH
 The goal of this research is to develop a methodology for creating autonomous
@@ -86,7 +91,9 @@ If this research is successful, we will be able to do the following:
     logic.
     % Outcome
     Control system engineers will generate verified mode-switching controllers
-    directly from regulatory procedures without formal methods expertise,
+    directly from regulatory procedures without formal methods 
+    expertise,\dasinline{Same comment as in executive
+    summary. Might not be true and is not the point.}
     lowering the barrier to high-assurance control systems.
 
     % OUTCOME 2 Title
@@ -131,7 +138,9 @@ autonomous control will become practical for safety-critical applications.
 This capability is essential for the economic viability of next-generation
 nuclear power. Small modular reactors offer a promising solution to growing
 energy demands, but their success depends on reducing per-megawatt operating
-costs through increased autonomy. This research will provide the tools to
+costs through increased autonomy.\dasinline{This paragraph is literally
+the same as the rest of the GO. Does not belong here
+and feels very redundant.} This research will provide the tools to
 achieve that autonomy while maintaining the exceptional safety record the
-nuclear industry requires.\splitnote{Strong closing — ties technical work to 
+nuclear industry requires.\splitnote{Strong closing --- ties technical work to 
 real-world impact and economic necessity.}

1-goals-and-outcomes/research-statement.tex

@@ -2,10 +2,13 @@
 The goal of this research is to develop a methodology for creating autonomous
 control systems with event-driven control laws that have guarantees of safe and
 correct behavior.\splitnote{Strong, direct opening. Sets scope immediately.}
+\dasinline{Title needs updated to High Assurance Hybrid
+Control Systems. Maybe removal of `formal'?}
 
 % INTRODUCTORY PARAGRAPH Hook
 Nuclear power relies on extensively trained operators who follow detailed
-written procedures to manage reactor control. Based on these procedures and
+written procedures to manage reactor control.\dasinline{Why is there any
+hyphenation at all? Why not full justification?} Based on these procedures and
 operators' interpretation of plant conditions, operators make critical decisions
 about when to switch between control objectives.
 \splitinline{Consider: ``operators'' appears 3x in two sentences. Maybe: 
@@ -17,18 +20,24 @@ next-generation nuclear power plants.
 \splitinline{``But, reliance'' — the comma after ``But'' is unusual. Either 
 drop it or restructure: ``However, this reliance...'' or ``This reliance, 
 however, has created...''}
+\dasinline{Or just straight up ``this reliance''.
+Right to the topic.}
 Small modular reactors face significantly higher per-megawatt staffing costs 
 than conventional 
-plants. Autonomous control systems are needed that can safely manage complex 
+plants.\dasinline{Obvious but source required.} Autonomous control systems are
+needed that can safely manage complex 
 operational sequences with the same assurance as human-operated systems, but 
 without constant supervision.
-\splitinline{``are needed that can'' — passive. Try: ``Autonomous control 
+\splitinline{``are needed that can'' --- passive. Try: ``Autonomous control 
 systems must safely manage...''}
 
 % APPROACH PARAGRAPH Solution
 To address this need, we will combine formal methods from computer science with
 control theory to build hybrid control systems that are correct by 
-construction.\splitnote{Clear statement of approach.}
+construction.\splitnote{Clear statement of approach.}\dasinline{Add
+``and leverage existing domain knowledge'' or similar.
+Industry knowledge can be reused here --- less like
+starting from scratch.}
 % Rationale
 Hybrid systems use discrete logic to switch between continuous control modes,
 similar to how operators change control strategies. Existing formal methods
@@ -42,18 +51,24 @@ translate written operating procedures into temporal logic specifications using
 NASA's Formal Requirements Elicitation Tool (FRET), which structures
 requirements into scope, condition, component, timing, and response elements.
 This structured approach enables realizability checking to identify conflicts
-and ambiguities in procedures before implementation. Second, we will synthesize
+and ambiguities in procedures before 
-discrete mode switching logic using reactive synthesis
+implementation.\dasinline{Had to read this twice.} Second, we will synthesize
+discrete mode switching logic using reactive 
+synthesis\dasinline{Also had to read this twice. A lot of
+jargon. Check topic stress.}
 to generate deterministic automata that are provably
 correct by construction. Third, we will develop continuous
 controllers for each discrete mode using standard control theory and
 reachability analysis. We will classify continuous modes based on their
-transition objectives, and then employ assume-guarantee contracts and barrier
+transition objectives, and then employ assume-guarantee contracts\dasinline{I don't think
+I ever mention this phrase again specifically. Might be a
+dogwhistle to other work unintentionally. Must be
+careful.} and barrier
 certificates to prove that mode transitions occur safely and as defined by the
 deterministic automata. This compositional approach enables local verification
 of continuous modes without requiring global trajectory analysis across the
 entire hybrid system. We will demonstrate this on an Emerson Ovation control 
-system.
+system.\dasinline{Where did this come from? Needs context.}
 \splitinline{This paragraph is dense. Consider breaking after the three 
 stages, then a new paragraph for the compositional verification point and 
 Emerson demo.}
@@ -77,9 +92,11 @@ If this research is successful, we will be able to do the following:
     discrete control logic using reactive synthesis tools.     
     % Outcome
     Control engineers will be able to generate mode-switching controllers from
-    regulatory procedures with little formal methods expertise, reducing
+    regulatory procedures with little formal methods 
+    expertise,\dasinline{This may not be true, and perhaps
+    does not belong.} reducing
     barriers to high-assurance control 
-    systems.\splitnote{Good practical framing — emphasizes accessibility.}
+    systems.\splitnote{Good practical framing --- emphasizes accessibility.}
 
     % OUTCOME 2 Title
   \item \textit{Verify continuous control behavior across mode transitions. }
@@ -100,7 +117,11 @@ If this research is successful, we will be able to do the following:
     Control engineers will be able to implement high-assurance autonomous
     controls on industrial platforms they already use, enabling users to
     achieve autonomy without retraining costs or developing new 
-    equipment.\splitnote{Strong industrial grounding — the ``platforms they 
+    equipment.\splitnote{Strong industrial grounding --- the ``platforms they 
-    already use'' point is compelling for adoption.}
+    already use'' point is compelling for 
+    adoption.}\dasinline{Flip the clauses. Put retraining
+    and new equipment before the comma, end with building
+    HAHACs with control hardware they already use.
+    That's the more important part.}
 
 \end{enumerate}

2-state-of-the-art/state-of-art.tex

@@ -6,7 +6,12 @@ first understand how nuclear reactors are operated today. This section examines
 reactor operators and the operating procedures we aim to leverage, then
 investigates limitations of human-based operation, and concludes with current
 formal methods approaches to reactor control 
-systems.\splitnote{Good roadmap — tells reader exactly what's coming.}
+systems.\splitnote{Good roadmap --- tells reader exactly what's 
+coming.}\dasinline{Don't like ``we'' here. Sounds like
+``we're going on an adventure!'' and feels jocular.
+Maybe: ``To motivate this proposal, the state of
+the art of nuclear reactor control, blah, and blah,
+are discussed in this section.''}
 
 \subsection{Current Reactor Procedures and Operation}
 
@@ -15,13 +20,20 @@ routine operations, abnormal operating procedures for off-normal conditions,
 Emergency Operating Procedures (EOPs) for design-basis accidents, Severe
 Accident Management Guidelines (SAMGs) for beyond-design-basis events, and
 Extensive Damage Mitigation Guidelines (EDMGs) for catastrophic damage
-scenarios. These procedures must comply with 10 CFR 50.34(b)(6)(ii) and are
+scenarios.\dasinline{This sentence is MASSIVE. Why is
+there 6 lines describing different types of
+procedures? WHO CARES? Need a sentence after saying
+why we have these procedures.} These procedures must comply with 10 CFR 50.34(b)(6)(ii) and are
 developed using guidance from NUREG-0899~\cite{NUREG-0899, 10CFR50.34}, but their
 development relies fundamentally on expert judgment and simulator validation
 rather than formal verification. Procedures undergo technical evaluation,
 simulator validation testing, and biennial review as part of operator
 requalification under 10 CFR 55.59~\cite{10CFR55.59}. Despite this rigor,
-procedures fundamentally lack formal verification of key safety properties. No
+procedures fundamentally lack formal verification of key safety 
+properties.\dasinline{Does the audience know what formal
+verification is at this point? Probably, but should
+say differently. Maybe `exhaustive' or
+`definitive'.} No
 mathematical proof exists that procedures cover all possible plant states, that
 required actions can be completed within available timeframes, or that
 transitions between procedure sets maintain safety 
@@ -52,6 +64,10 @@ Protection Systems trip automatically on safety signals with millisecond
 response times, and engineered safety features actuate automatically on accident
 signals without operator action required.
 
+\dasinline{After reading the next sentence, ``key safety''
+can honestly just be a semicolon.}
+\dasinline{Not sure what the challenge actually is
+as this paragraph is written. What's the point?}
 The division between automated and human-controlled functions reveals the
 fundamental challenge of hybrid control. Highly automated systems handle reactor
 protection---automatic trips on safety parameters, emergency core cooling
@@ -65,7 +81,10 @@ already there, just not formally verified.}
 \subsection{Human Factors in Nuclear Accidents}
 
 Current-generation nuclear power plants employ over 3,600 active NRC-licensed
-reactor operators in the United States~\cite{operator_statistics}. These
+reactor operators in the United 
+States~\cite{operator_statistics}.\dasinline{Why is this here? Should this
+be in broader impacts about running out of ROs?
+As it is here I have no idea why this is here.} These
 operators divide into Reactor Operators (ROs), who manipulate reactor controls,
 and Senior Reactor Operators (SROs), who direct plant operations and serve as
 shift supervisors~\cite{10CFR55}. Staffing typically requires at least two ROs
@@ -76,8 +95,12 @@ The persistent role of human error in nuclear safety incidents---despite decades
 of improvements in training and procedures---provides the most compelling
 motivation for formal automated control with mathematical safety 
 guarantees.\splitnote{Strong thesis for this subsection.}
-Operators hold legal authority under 10 CFR Part 55 to make critical decisions,
+Operators hold legal authority under 10 CFR Part 55 to make critical 
-including departing from normal regulations during emergencies. The Three Mile
+decisions,\dasinline{Cite.}
+including departing from normal regulations during emergencies. 
+\dasinline{Needs a connector here. Like ``But this can
+in and of itself prime plants for an accident.''
+Then continue.}The Three Mile
 Island (TMI) accident demonstrated how a combination of personnel error, design
 deficiencies, and component failures led to partial meltdown when operators
 misread confusing and contradictory readings and shut off the emergency water
@@ -118,17 +141,24 @@ project represents the most advanced application of formal methods to nuclear
 reactor control systems to date~\cite{Kiniry2024}.
 
 HARDENS aimed to address a fundamental dilemma: existing U.S. nuclear control
-rooms rely on analog technologies from the 1950s--60s. This technology is
+rooms rely on analog technologies from the 1950s--60s.\dasinline{Source?}
+This technology is
 obsolete compared to modern control systems and incurs significant risk and
 cost. The NRC contracted Galois, a formal methods firm, to demonstrate that
 Model-Based Systems Engineering and formal methods could design, verify, and
 implement a complex protection system meeting regulatory criteria at a fraction
 of typical cost. The project delivered a Reactor Trip System (RTS)
 implementation with full traceability from NRC Request for Proposals and IEEE
-standards through formal architecture specifications to verified software.
+standards through formal architecture specifications to verified 
+software.\dasinline{Wordsmith this to remove the RFP and
+IEEE standards language. Should just say
+requirements.}
 
 HARDENS employed formal methods tools and techniques across the verification
-hierarchy. High-level specifications used Lando, SysMLv2, and FRET (NASA Formal
+hierarchy.\dasinline{Zero discussion about what the
+verification hierarchy is. What is a specification
+or a requirement to someone who hasn't heard of
+one before?} High-level specifications used Lando, SysMLv2, and FRET (NASA Formal
 Requirements Elicitation Tool) to capture stakeholder requirements, domain
 engineering, certification requirements, and safety requirements. Requirements
 were analyzed for consistency, completeness, and realizability using SAT and SMT
@@ -142,7 +172,10 @@ arise.\splitnote{Good technical depth on HARDENS toolchain.}
 
 Despite its accomplishments, HARDENS has a fundamental limitation directly
 relevant to hybrid control synthesis: the project addressed only discrete
-digital control logic without modeling or verifying continuous reactor dynamics.
+digital control logic without modeling or verifying continuous reactor 
+dynamics.\dasinline{Edit these to more clearly separate
+the context from the limit. The limitation should
+be in the limitation.}
 The Reactor Trip System specification and verification covered discrete state
 transitions (trip/no-trip decisions), digital sensor input processing through
 discrete logic, and discrete actuation outputs (reactor trip commands). The
@@ -166,7 +199,10 @@ NRC Final Report explicitly notes~\cite{Kiniry2024} that all material is
 considered in development, not a finalized product, and that ``The demonstration
 of its technical soundness was to be at a level consistent with satisfaction of
 the current regulatory criteria, although with no explicit demonstration of how
-regulatory requirements are met.'' The project did not include deployment in
+regulatory requirements are 
+met.''\dasinline{Check this quote. Absolutely damning
+for HARDENS if true and hilarious Galois said
+this.} The project did not include deployment in
 actual nuclear facilities, testing with real reactor systems under operational
 conditions, side-by-side validation with operational analog RTS systems,
 systematic failure mode testing (radiation effects, electromagnetic
@@ -174,7 +210,8 @@ interference, temperature extremes), NRC licensing review, or human factors
 validation with licensed operators in realistic control room scenarios.
 
 \textbf{LIMITATION:} \textit{HARDENS achieved TRL 2--3 without experimental
-validation.} While formal verification provides mathematical correctness
+validation.}\dasinline{Same as before. Separate limit
+from context better.} While formal verification provides mathematical correctness
 guarantees for the implemented discrete logic, the gap between formal
 verification and actual system deployment involves myriad practical
 considerations: integration with legacy systems, long-term reliability
@@ -184,7 +221,9 @@ primary assurance evidence.
 
 \subsubsection{Sequent Calculus and Differential Dynamic Logic}
 There has been additional work to do verification of hybrid systems by extending
-the temporal logics directly. The result has been the field of differential
+the temporal logics 
+directly.\dasinline{Need to introduce temporal logic
+and FRET here first.} The result has been the field of differential
 dynamic logic (dL). dL introduces two additional operators
 into temporal logic: the box operator and the diamond operator. The box operator
 \([\alpha]\phi\) states that for some region \(\phi\), the hybrid system

3-research-approach/approach.tex

@@ -17,7 +17,8 @@
 % ----------------------------------------------------------------------------
 Previous approaches to autonomous control have verified
 discrete switching logic or continuous control behavior, but not both
-simultaneously. Validation of continuous controllers today consists of
+simultaneously.\dasinline{Honestly just get rid of this
+whole paragraph.} Validation of continuous controllers today consists of
 extensive simulation trials. Discrete switching logic for routine operation
 has been driven by human operators, whose evaluation includes simulated
 control room testing and human factors research. Neither method, despite
@@ -27,10 +28,15 @@ computer science with control-theoretic verification, formalizing reactor
 operations using the framework of hybrid automata.
 
 The challenge of hybrid system verification lies in the interaction between
-discrete and continuous dynamics. Discrete transitions change the governing
+discrete and continuous dynamics. Discrete transitions change the 
+governing\dasinline{Governing what? People? Whos in
+Whoville?}
 vector field, creating discontinuities in the system's behavior. Traditional
 verification techniques designed for purely discrete or purely continuous
-systems cannot handle this interaction directly.\splitpolish{Missing space before ``Our} Our methodology addresses this
+systems cannot handle this interaction directly.\splitpolish{Missing space before ``Our}\dasinline{This whole paragraph
+should just be after the definition of the tuple.
+First sentence can stay, but all this explanation
+should move.} Our methodology addresses this
 challenge through decomposition. We verify discrete switching logic and
 continuous mode behavior separately, then compose these guarantees to reason
 about the complete hybrid system.\splitsuggest{Compositional verification claim 
@@ -76,7 +82,9 @@ where:
 
 The creation of a HAHACS amounts to the construction of such a tuple together
 with proof artifacts demonstrating that the intended behavior of the control
-system is satisfied by its actual implementation. This approach is tractable now
+system is satisfied by its actual 
+implementation.\dasinline{Add a sentence explaining what
+this actually means.} This approach is tractable now
 because the infrastructure for each component has matured. The novelty is not in
 the individual pieces, but in the architecture that connects them.\splitnote{This is your key insight --- the novelty is compositional, not component-level.} By defining
 entry, exit, and safety conditions at the discrete level first, we transform the
@@ -129,6 +137,9 @@ complex reactor operations.
     \node[dynamics] at (5,-4.9) {$\dot{x} = f_3(x)$};
     
   \end{tikzpicture}
+\dasinline{Figure dynamics show control inputs u,
+but these systems are autonomous. What's up
+with that?}
   \caption{Simplified hybrid automaton for reactor startup. Each discrete state 
     $q_i$ has associated continuous dynamics $f_i$. Guard conditions on 
     transitions (e.g., $T_{avg} > T_{min}$) are predicates over continuous 
@@ -158,11 +169,14 @@ tactical level. This is the individual control of pumps, turbines, and
 chemistry. Tactical control has already been somewhat automated in nuclear power
 plants today, and is generally considered ``automatic control'' when autonomous.
 These controls are almost always continuous systems with a direct impact on the
-physical state of the plant. Tactical control objectives include maintaining
+physical state of the plant.\dasinline{This should be
+written to be clear this isn't an exhaustive
+list.} Tactical control objectives include maintaining
 pressurizer level, maintaining core temperature, or adjusting reactivity with a
 chemical shim.
 
-The level of control linking these two extremes is the operational control
+The level of control linking\dasinline{Linking of these
+two extremes. Don't even say control here.} these two extremes is the operational control
 scope. Operational control is the primary responsibility of human operators
 today. Operational control takes the current strategic objective and implements
 tactical control objectives to drive the plant towards strategic goals. In this
@@ -170,7 +184,8 @@ way, it bridges high-level and low-level goals. A strategic goal may be to
 perform refueling at a certain time, while the tactical level of the plant is
 currently focused on maintaining a certain core temperature. The operational
 level issues the shutdown procedure, using several smaller tactical goals along
-the way to achieve this objective. Thus, the combination of the operational and
+the way to achieve this 
+objective.\dasinline{This STRATEGIC objective.} Thus, the combination of the operational and
 tactical levels fundamentally forms a hybrid controller. The tactical level is
 the continuous evolution of the plant according to the control input and control
 law, while the operational level is a discrete state evolution that determines
@@ -213,14 +228,23 @@ which tactical control law to apply.
 
 
 This operational control level is the main reason for the requirement of human
-operators in nuclear control today. The hybrid nature of this control system
+operators in nuclear control today.\dasinline{Just chop
+this.} The hybrid nature of this control system
 makes it difficult to prove that a controller will perform according to
 strategic requirements, as unified infrastructure for building and verifying
 hybrid systems does not currently exist. Humans have been used for this layer
 because their general intelligence has been relied upon as a safe way to manage
-the hybrid nature of this system. But these operators use prescriptive operating
+the hybrid nature of this system.\dasinline{Add a sentence
+why. Because the hybrid dynamics have previously
+been `unknowable', it's been assumed that a human
+operator could figure it out on the fly. Or
+similar.} But these operators use prescriptive operating
 manuals to perform their control with strict procedures on what control to
-implement at a given time. These procedures are the key to the operational
+implement at a given 
+time.\dasinline{Say but human factors has been seeking
+to eliminate the need for general human behavior
+by creating extremely prescriptive operating
+manuals. This is our leverage.} These procedures are the key to the operational
 control scope.
 
 The method of constructing a HAHACS in this proposal leverages two key
@@ -234,7 +258,9 @@ these requirements derive from multiple sources including regulatory mandates,
 design basis analyses, and operating procedures. The challenge is formalizing
 these requirements with sufficient precision that they can serve as the
 foundation for autonomous control system synthesis and verification. We can
-build these requirements using temporal logic.
+build these requirements using temporal 
+logic.\dasinline{We definitely need some temporal logic
+juice in the SOTA.}
 
 Temporal logic is a powerful set of semantics for building systems with complex
 but deterministic behavior. Temporal logic extends classical propositional logic
@@ -260,7 +286,12 @@ why the approach is feasible for nuclear applications specifically: the hard
 work of defining safe operating boundaries has already been done by generations
 of nuclear engineers. 
 
-Linear temporal logic (LTL) is particularly well-suited for
+Linear temporal logic (LTL) is particularly well-suited 
+for\dasinline{Some of this could be in SOTA vs here.
+Examples in nuclear space should be in RA, but
+the general idea of temporal logic and where it
+came from in the context of computers could be
+in SOTA.}
 specifying reactive systems. LTL formulas are built from atomic propositions
 (our discrete predicates) using Boolean connectives and temporal operators.
 The key temporal operators are:
@@ -334,7 +365,8 @@ of the discrete automaton is human engineering of the implementation required.
 The resultant automaton is correct by construction. This method of construction
 eliminates the possibility of human error at the implementation stage entirely.
 Instead, the effort on the human designer is directed at the specification of
-system behavior itself. This has two critical implications. First, it makes the
+system behavior itself.\dasinline{Some goofy issue-point
+stuff going on in this paragraph.} This has two critical implications. First, it makes the
 creation of the discrete controller tractable. The reasons the controller
 changes between modes can be traced back to the specification and thus to any
 requirements, which provides a trace for liability and justification of system
@@ -367,7 +399,7 @@ continuous components. This section describes the continuous control modes that
 execute within each discrete state, and how we verify that they satisfy the
 requirements imposed by the discrete layer. It is important to clarify the scope
 of this methodology with respect to continuous controller design. This work
-verifies continuous controllers; it does not synthesize them. The distinction
+\dasinline{Verb tense: ``will verify''.}verifies continuous controllers; it does not synthesize them. The distinction
 parallels model checking in software verification: model checking does not tell
 engineers how to write correct software, but it verifies whether a given
 implementation satisfies its specification. Similarly, we assume that continuous
@@ -405,7 +437,10 @@ controller design:
     from invariants \(Inv\).
 \end{enumerate}
 These sets come directly from the discrete controller synthesis and define
-precise objectives for continuous control. The continuous controller for mode
+precise objectives for continuous 
+control.\dasinline{This SOUNDS like assume-guarantee
+stuff. Maybe make that connection formal and cite
+it?} The continuous controller for mode
 $q_i$ must drive the system from any state in $\mathcal{X}_{entry,i}$ to some
 state in $\mathcal{X}_{exit,i}$ while remaining within $\mathcal{X}_{safe,i}$.\splitnote{This compositional approach is formalized in Kapuria 2025 (pp.17-24, Section 2.4): component proofs via differential cuts reduce state-space (DC rule, p.20), then system proof composes via differential invariants (DI rule, pp.22-24). Kapuria proves SmAHTR safety by verifying 6 components in isolation then system---your three-mode structure maps perfectly to this decomposition, reducing verification complexity from curse of dimensionality.}
 
@@ -486,7 +521,8 @@ appropriate to the fidelity of the reactor models available.\splitnote{Your tool
 
 Stabilizing modes are continuous controllers with an objective of maintaining a
 particular discrete state indefinitely. Rather than driving the system toward an
-exit condition, they keep the system within a safe operating region. Examples
+exit condition,\dasinline{``mode'' --- ``condition'' here
+sounds goofy.} they keep the system within a safe operating region. Examples
 include steady-state power operation, hot standby, and load-following at
 constant power level. Reachability analysis for stabilizing modes may not be a
 suitable approach to validation. Instead, we plan to use barrier certificates.
@@ -500,7 +536,10 @@ scalar function $B: \mathcal{X} \rightarrow \mathbb{R}$ that certifies forward
 invariance of a safe set. The idea is analogous to Lyapunov functions for
 stability: rather than computing trajectories explicitly, we find a certificate
 function whose properties guarantee the desired behavior. For a safe set
-$\mathcal{C} = \{x : B(x) \geq 0\}$ and dynamics $\dot{x} = f(x,u)$, the
+$\mathcal{C} = \{x : B(x) \geq 0\}$ and dynamics $\dot{x} = f(x,u)$, 
+the\dasinline{Should clarify that the safe set C is not
+the entire continuous region. It's just the
+boundary of the region.}
 barrier certificate condition requires:
 \[
 \forall x \in \partial\mathcal{C}: \dot{B}(x) = \nabla B(x) \cdot f(x,u(x)) \geq 0
@@ -553,7 +592,9 @@ been previously proven correct by reachability and barrier certificates. We know
 our controller cannot be incorrect for the nominal plant model, so if an
 invariant is violated, we know the plant dynamics have changed. The HAHACS can
 identify that a fault occurred because a discrete boundary condition was
-violated by the continuous physical controller. This is a direct consequence of
+violated by the continuous physical 
+controller.\dasinline{This says the same thing as the
+sentence right before it.} This is a direct consequence of
 having verified the nominal continuous control modes: unexpected behavior
 implies off-nominal conditions.
 
@@ -618,7 +659,8 @@ compiled to run on Ovation controllers, with verification that the implemented
 behavior matches the synthesized specification exactly.
 
 For the continuous dynamics, we will use a small modular
-reactor simulation. The SmAHTR (Small modular Advanced High Temperature
+reactor simulation.\dasinline{Are we REALLY going to do
+this? Maybe not.} The SmAHTR (Small modular Advanced High Temperature
 Reactor) model provides a relevant testbed for startup and shutdown procedures.
 The ARCADE (Advanced Reactor Control Architecture Development Environment)
 interface will establish communication between the Emerson Ovation hardware and

4-metrics-of-success/metrics.tex

@@ -10,7 +10,8 @@ This section explains why TRL advancement provides the most appropriate success
 metric and defines the specific criteria required to achieve TRL 5.
 
 Technology Readiness Levels provide the ideal success metric because they
-explicitly measure the gap between academic proof-of-concept and practical
+explicitly measure the gap between academic proof-of-concept and 
+practical\dasinline{Chop. No likey.}
 deployment---precisely what this work aims to bridge. Academic metrics like
 papers published or theorems proved cannot capture practical feasibility.
 Empirical metrics like simulation accuracy or computational speed cannot

5-risks-and-contingencies/risks.tex

@@ -29,7 +29,8 @@ problems. Synthesis times exceeding 24 hours for simplified procedure subsets
 would suggest complete procedures are intractable. Generated automata containing
 more than 1,000 discrete states would indicate the discrete state space is too
 large for efficient verification. Specifications flagged as unrealizable by FRET
-or Strix would reveal fundamental conflicts in the formalized procedures.
+or Strix\dasinline{Strix may not be the reactive synth
+tool anymore. Be more general.} would reveal fundamental conflicts in the formalized procedures.
 Reachability analysis failing to converge within reasonable time bounds would
 show that continuous mode verification cannot be completed with available
 computational resources.
@@ -53,7 +54,7 @@ systems: relating discrete switching logic to continuous dynamics. Temporal
 logic operates on boolean predicates, while continuous control requires
 reasoning about differential equations and reachable sets. Guard conditions
 requiring complex nonlinear predicates may resist boolean abstraction, making
-synthesis intractable. Continuous safety regions that cannot be expressed as
+synthesis intractable.\dasinline{What does this mean?} Continuous safety regions that cannot be expressed as
 conjunctions of verifiable constraints would similarly create insurmountable
 verification challenges. The risk extends beyond static interface definition to
 dynamic behavior across transitions: barrier certificates may fail to exist for

6-broader-impacts/impacts.tex

@@ -8,7 +8,9 @@ Deploying SMRs at datacenter sites would minimize transmission losses and
 eliminate emissions from hydrocarbon-based alternatives. However, nuclear power
 economics at this scale demand careful attention to operating costs.
 
-According to the U.S. Energy Information Administration's Annual Energy Outlook
+According to the U.S. Energy Information 
+Administration's\dasinline{Check all of this math and
+update if newer sources exist.} Annual Energy Outlook
 2022, advanced nuclear power entering service in 2027 is projected to cost
 \$88.24 per megawatt-hour~\cite{eia_lcoe_2022}. Datacenter electricity demand is
 projected to reach 1,050 terawatt-hours annually by

main.tex

@@ -6,6 +6,7 @@
 \usepackage[table]{xcolor}   % For colored tables (optional)
 \usepackage{pgfgantt}
 \usepackage{pdfpages}        % For including PDF files
+% Strikethrough without soul/ulem (manual rule-based)
 
 % === SPLIT'S EDITING COMMENTS ===
 % Set to 1 for edit mode (wider margins, visible comments)
@@ -32,6 +33,14 @@
   \newcommand{\splitfix}[1]{\todo[color=red!40]{#1}}
   % Inline versions
   \newcommand{\splitinline}[1]{\todo[inline,color=green!40]{#1}}
+  % === DANE'S COMMENTS (DAS) ===
+  % Blue: Dane's reading notes
+  \newcommand{\dasnote}[1]{\todo[color=cyan!40]{DAS - #1}}
+  \newcommand{\dasinline}[1]{\todo[inline,color=cyan!40]{DAS - #1}}
+  % === EDIT MARKUP ===
+  % Strikethrough old text, red for new text
+  \newcommand{\oldt}[1]{\textcolor{gray}{#1}}
+  \newcommand{\newt}[1]{\textcolor{red}{#1}}
 \else
   % Final mode: no comments, normal margins
   \newcommand{\splitnote}[1]{}
@@ -39,6 +48,10 @@
   \newcommand{\splitpolish}[1]{}
   \newcommand{\splitfix}[1]{}
   \newcommand{\splitinline}[1]{}
+  \newcommand{\dasnote}[1]{}
+  \newcommand{\dasinline}[1]{}
+  \newcommand{\oldt}[1]{#1}
+  \newcommand{\newt}[1]{}
 \fi
 % ================================