fixed edit mode

This commit is contained in:
Dane Sabo 2026-03-10 17:17:50 -04:00
parent 77f361734b
commit cbc2467219
9 changed files with 136 additions and 426 deletions

View File

@ -427,11 +427,11 @@ reachable within time horizon $T$:
\text{Reach}(\mathcal{X}_{entry}, f_i, [0,T]) \cap \mathcal{X}_{exit} \neq \emptyset
\]
\textcolor{blue}{Because the discrete controller defines clear boundaries in continuous state
Because the discrete controller defines clear boundaries in continuous state
space, the verification problem for each transitory mode is well-posed. We know
the possible initial conditions, we know the target conditions, and we know the
safety envelope. The verification task is to confirm that the candidate
continuous controller achieves the objective from all possible starting points.}
continuous controller achieves the objective from all possible starting points.
Several tools exist for computing reachable sets of hybrid
systems, including CORA, Flow*, SpaceEx, and JuliaReach. The choice of tool

168
main.aux
View File

@ -5,147 +5,55 @@
\citation{NUREG-0899,10CFR50.34}
\citation{10CFR55.59}
\citation{WRPS.Description,gentillon_westinghouse_1999}
\@writefile{toc}{\contentsline {section}{\numberline {2}State of the Art and Limits of Current Practice}{3}{}\protected@file@percent }
\@writefile{tdo}{\contentsline {todo}{\fcolorbox {black}{green!40}{\textcolor {green!40}{o}}\ Good roadmap — tells reader exactly what's coming.}{3}{}\protected@file@percent }
\pgfsyspdfmark {pgfid1}{21980756}{40762302}
\pgfsyspdfmark {pgfid4}{31254300}{40736566}
\pgfsyspdfmark {pgfid5}{35899615}{40496882}
\@writefile{toc}{\contentsline {subsection}{\numberline {2.1}Current Reactor Procedures and Operation}{3}{}\protected@file@percent }
\@writefile{tdo}{\contentsline {todo}{\fcolorbox {black}{yellow!60}{\textcolor {yellow!60}{o}}\ This paragraph is doing a lot. Consider splitting: first paragraph on the hierarchy and compliance, second on the lack of formal verification. The ``No mathematical proof exists...'' sentence is powerful and deserves emphasis.}{3}{}\protected@file@percent }
\pgfsyspdfmark {pgfid6}{20423612}{24880744}
\pgfsyspdfmark {pgfid9}{31254300}{24855008}
\pgfsyspdfmark {pgfid10}{35899615}{24615324}
\@writefile{tdo}{\contentsline {todo}{\fcolorbox {black}{orange!50}{\textcolor {orange!50}{o}}\ This repeats the ``No mathematical proof exists...'' sentence almost verbatim from the paragraph above. Either cut it from the paragraph or from the LIMITATION box.}{3}{}\protected@file@percent }
\pgfsyspdfmark {pgfid11}{13626615}{17278568}
\pgfsyspdfmark {pgfid14}{31254300}{16022170}
\pgfsyspdfmark {pgfid15}{35899615}{15782486}
\citation{operator_statistics}
\citation{10CFR55}
\citation{10CFR50.54}
\citation{Kemeny1979}
\@writefile{toc}{\contentsline {section}{\numberline {2}State of the Art and Limits of Current Practice}{3}{}\protected@file@percent }
\@writefile{toc}{\contentsline {subsection}{\numberline {2.1}Current Reactor Procedures and Operation}{3}{}\protected@file@percent }
\@writefile{toc}{\contentsline {subsection}{\numberline {2.2}Human Factors in Nuclear Accidents}{3}{}\protected@file@percent }
\citation{WNA2020}
\citation{hogberg_root_2013}
\citation{zhang_analysis_2025}
\citation{Kiniry2024}
\@writefile{tdo}{\contentsline {todo}{\fcolorbox {black}{green!40}{\textcolor {green!40}{o}}\ This is the key insight — the hybrid nature is already there, just not formally verified.}{4}{}\protected@file@percent }
\pgfsyspdfmark {pgfid16}{14097656}{42090495}
\pgfsyspdfmark {pgfid19}{31254300}{42064759}
\pgfsyspdfmark {pgfid20}{35899615}{41825075}
\@writefile{toc}{\contentsline {subsection}{\numberline {2.2}Human Factors in Nuclear Accidents}{4}{}\protected@file@percent }
\@writefile{tdo}{\contentsline {todo}{\fcolorbox {black}{green!40}{\textcolor {green!40}{o}}\ Strong thesis for this subsection.}{4}{}\protected@file@percent }
\pgfsyspdfmark {pgfid21}{5927496}{30010025}
\pgfsyspdfmark {pgfid24}{31254300}{29984289}
\pgfsyspdfmark {pgfid25}{35899615}{29744605}
\@writefile{tdo}{\contentsline {todo}{\fcolorbox {black}{green!40}{\textcolor {green!40}{o}}\ ``the person responsible for reactor safety is often the root cause of failures'' — devastating summary. Very effective.}{4}{}\protected@file@percent }
\pgfsyspdfmark {pgfid26}{4915358}{19557033}
\pgfsyspdfmark {pgfid29}{31254300}{19531297}
\pgfsyspdfmark {pgfid30}{35899615}{19291613}
\@writefile{tdo}{\contentsline {todo}{\fcolorbox {black}{green!40}{\textcolor {green!40}{o}}\ Strong empirical grounding. The Chinese plant data is a nice addition — shows this isn't just a Western regulatory perspective.}{4}{}\protected@file@percent }
\pgfsyspdfmark {pgfid31}{4609444}{10054313}
\pgfsyspdfmark {pgfid34}{31254300}{10028577}
\pgfsyspdfmark {pgfid35}{35899615}{9788893}
\@writefile{tdo}{\contentsline {todo}{\fcolorbox {black}{green!40}{\textcolor {green!40}{o}}\ Well-stated. The ``four decades'' point drives it home.}{4}{}\protected@file@percent }
\pgfsyspdfmark {pgfid36}{4792689}{5302953}
\pgfsyspdfmark {pgfid39}{31254300}{4760899}
\pgfsyspdfmark {pgfid40}{35899615}{4521215}
\@writefile{toc}{\contentsline {subsection}{\numberline {2.3}Formal Methods}{4}{}\protected@file@percent }
\@writefile{toc}{\contentsline {subsubsection}{\numberline {2.3.1}HARDENS}{4}{}\protected@file@percent }
\citation{Kiniry2024}
\@writefile{toc}{\contentsline {subsection}{\numberline {2.3}Formal Methods}{5}{}\protected@file@percent }
\@writefile{toc}{\contentsline {subsubsection}{\numberline {2.3.1}HARDENS}{5}{}\protected@file@percent }
\@writefile{tdo}{\contentsline {todo}{\fcolorbox {black}{green!40}{\textcolor {green!40}{o}}\ Good technical depth on HARDENS toolchain.}{5}{}\protected@file@percent }
\pgfsyspdfmark {pgfid41}{20999294}{21457577}
\pgfsyspdfmark {pgfid44}{31254300}{21431841}
\pgfsyspdfmark {pgfid45}{35899615}{21192157}
\@writefile{tdo}{\contentsline {todo}{\fcolorbox {black}{green!40}{\textcolor {green!40}{o}}\ Clear articulation of the gap your work fills.}{5}{}\protected@file@percent }
\pgfsyspdfmark {pgfid46}{23128957}{11004585}
\pgfsyspdfmark {pgfid49}{31254300}{10978849}
\pgfsyspdfmark {pgfid50}{35899615}{10739165}
\@writefile{toc}{\contentsline {subsubsection}{\numberline {2.3.2}Sequent Calculus and Differential Dynamic Logic}{6}{}\protected@file@percent }
\@writefile{tdo}{\contentsline {todo}{\fcolorbox {black}{red!40}{\textcolor {red!40}{o}}\ Typo: ``ivariant'' should be ``invariant''}{6}{}\protected@file@percent }
\pgfsyspdfmark {pgfid51}{4749422}{20507305}
\pgfsyspdfmark {pgfid54}{31254300}{20481569}
\pgfsyspdfmark {pgfid55}{35899615}{20241885}
\@writefile{tdo}{\contentsline {todo}{\fcolorbox {black}{yellow!60}{\textcolor {yellow!60}{o}}\ Consider adding a concrete example here — ``For instance, a system with N modes and M continuous state variables...'' to give readers a sense of the scaling problem.}{6}{}\protected@file@percent }
\pgfsyspdfmark {pgfid56}{18750152}{12905129}
\pgfsyspdfmark {pgfid59}{31254300}{12879393}
\pgfsyspdfmark {pgfid60}{35899615}{12639709}
\@writefile{tdo}{\contentsline {todo}{\fcolorbox {black}{orange!50}{\textcolor {orange!50}{o}}\ ``but are far from a complete methodology to design systems with'' — awkward ending preposition. Try: ``but remain far from a complete design methodology'' or ``but do not yet constitute a complete design methodology.''}{6}{}\protected@file@percent }
\pgfsyspdfmark {pgfid61}{8940582}{10054313}
\pgfsyspdfmark {pgfid64}{31254300}{5829135}
\pgfsyspdfmark {pgfid65}{35899615}{5589451}
\@writefile{tdo}{\contentsline {todo}{\fcolorbox {black}{green!40}{\textcolor {green!40}{o}}\ Your comment here is spot-on. You should add a LIMITATION box: \textit {Differential dynamic logic has been used for post-hoc analysis of existing systems, not for the constructive design of autonomous controllers.} This is exactly the gap you're filling — you're doing synthesis, not just verification.}{6}{}\protected@file@percent }
\pgfsyspdfmark {pgfid66}{14192475}{45403152}
\citation{HANDBOOK ON HYBRID SYSTEMS}
\@writefile{toc}{\contentsline {section}{\numberline {3}Research Approach}{8}{}\protected@file@percent }
\@writefile{tdo}{\contentsline {todo}{\fcolorbox {black}{orange!50}{\textcolor {orange!50}{o}}\ Missing space before ``Our}{8}{}\protected@file@percent }
\pgfsyspdfmark {pgfid67}{21351522}{32209854}
\pgfsyspdfmark {pgfid70}{31254300}{32184118}
\pgfsyspdfmark {pgfid71}{35899615}{31944434}
\@writefile{lof}{\contentsline {figure}{\numberline {1}{\ignorespaces 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 state. Invariant violations ($\neg Inv_i$) trigger transitions to the SCRAM state. The operational level manages discrete transitions; the tactical level executes continuous control within each mode.}}{9}{}\protected@file@percent }
\newlabel{fig:hybrid_automaton}{{1}{9}{Research Approach}{figure.1}{}}
\@writefile{tdo}{\contentsline {todo}{\fcolorbox {black}{green!40}{\textcolor {green!40}{o}}\ This is your key insight — the novelty is compositional, not component-level.}{9}{}\protected@file@percent }
\pgfsyspdfmark {pgfid72}{5905037}{17221912}
\pgfsyspdfmark {pgfid75}{31254300}{17196176}
\pgfsyspdfmark {pgfid76}{35899615}{16956492}
\@writefile{toc}{\contentsline {subsection}{\numberline {3.1}System Requirements, Specifications, and Discrete Controllers}{9}{}\protected@file@percent }
\@writefile{lof}{\contentsline {figure}{\numberline {2}{\ignorespaces Control scope hierarchy in nuclear power operations. Strategic control (long-term planning) remains with human management. HAHACS addresses the operational level (discrete mode switching) and tactical level (continuous control within modes), which together form a hybrid control system.}}{10}{}\protected@file@percent }
\newlabel{fig:strat_op_tact}{{2}{10}{System Requirements, Specifications, and Discrete Controllers}{figure.2}{}}
\citation{MANYUS THESIS}
\@writefile{toc}{\contentsline {subsection}{\numberline {3.2}Continuous Control Modes}{13}{}\protected@file@percent }
\@writefile{tdo}{\contentsline {todo}{\fcolorbox {black}{green!40}{\textcolor {green!40}{o}}\ This three-mode taxonomy is elegant — maps verification tools to control objectives cleanly.}{14}{}\protected@file@percent }
\pgfsyspdfmark {pgfid79}{15985073}{33177599}
\pgfsyspdfmark {pgfid82}{31254300}{33151863}
\pgfsyspdfmark {pgfid83}{35899615}{32912179}
\@writefile{toc}{\contentsline {subsubsection}{\numberline {3.2.1}Transitory Modes}{14}{}\protected@file@percent }
\@writefile{toc}{\contentsline {subsubsection}{\numberline {3.2.2}Stabilizing Modes}{15}{}\protected@file@percent }
\@writefile{toc}{\contentsline {subsubsection}{\numberline {3.2.3}Expulsory Modes}{16}{}\protected@file@percent }
\@writefile{toc}{\contentsline {subsection}{\numberline {3.3}Industrial Implementation}{17}{}\protected@file@percent }
\@writefile{tdo}{\contentsline {todo}{\fcolorbox {black}{red!40}{\textcolor {red!40}{o}}\ Typo: ``excess should be ``access}{17}{}\protected@file@percent }
\pgfsyspdfmark {pgfid84}{25258844}{17656489}
\pgfsyspdfmark {pgfid87}{31254300}{17630753}
\pgfsyspdfmark {pgfid88}{35899615}{17391069}
\@writefile{toc}{\contentsline {section}{\numberline {4}Metrics for Success}{18}{}\protected@file@percent }
\@writefile{tdo}{\contentsline {todo}{\fcolorbox {black}{green!40}{\textcolor {green!40}{o}}\ TRL as primary metric is smart — speaks industry language.}{18}{}\protected@file@percent }
\pgfsyspdfmark {pgfid89}{6508678}{41712574}
\pgfsyspdfmark {pgfid92}{31254300}{41686838}
\pgfsyspdfmark {pgfid93}{35899615}{41447154}
\@writefile{tdo}{\contentsline {todo}{\fcolorbox {black}{green!40}{\textcolor {green!40}{o}}\ Good framing — explains why other metrics are insufficient.}{18}{}\protected@file@percent }
\pgfsyspdfmark {pgfid94}{7276206}{33160126}
\pgfsyspdfmark {pgfid97}{31254300}{33134390}
\pgfsyspdfmark {pgfid98}{35899615}{32894706}
\@writefile{toc}{\contentsline {paragraph}{TRL 3 \textit {Critical Function and Proof of Concept}}{18}{}\protected@file@percent }
\@writefile{toc}{\contentsline {paragraph}{TRL 4 \textit {Laboratory Testing of Integrated Components}}{18}{}\protected@file@percent }
\@writefile{toc}{\contentsline {paragraph}{TRL 5 \textit {Laboratory Testing in Relevant Environment}}{19}{}\protected@file@percent }
\@writefile{tdo}{\contentsline {todo}{\fcolorbox {black}{yellow!60}{\textcolor {yellow!60}{o}}\ Consider noting why graded responses are out of scope — is it time, complexity, or scope creep? Brief justification helps.}{19}{}\protected@file@percent }
\pgfsyspdfmark {pgfid99}{15785403}{27497812}
\pgfsyspdfmark {pgfid102}{31254300}{27472076}
\pgfsyspdfmark {pgfid103}{35899615}{27232392}
\@writefile{tdo}{\contentsline {todo}{\fcolorbox {black}{green!40}{\textcolor {green!40}{o}}\ Clear success criteria. Committee will know exactly what ``done'' looks like.}{19}{}\protected@file@percent }
\pgfsyspdfmark {pgfid104}{13547172}{12293460}
\pgfsyspdfmark {pgfid107}{31254300}{12267724}
\pgfsyspdfmark {pgfid108}{35899615}{12028040}
\@writefile{toc}{\contentsline {section}{\numberline {5}Risks and Contingencies}{20}{}\protected@file@percent }
\@writefile{tdo}{\contentsline {todo}{\fcolorbox {black}{green!40}{\textcolor {green!40}{o}}\ Honest acknowledgment of risks with clear contingencies — committee will appreciate this.}{20}{}\protected@file@percent }
\pgfsyspdfmark {pgfid109}{19227927}{44563390}
\pgfsyspdfmark {pgfid112}{31254300}{44537654}
\pgfsyspdfmark {pgfid113}{35899615}{44297970}
\@writefile{toc}{\contentsline {subsection}{\numberline {5.1}Computational Tractability of Synthesis}{20}{}\protected@file@percent }
\@writefile{toc}{\contentsline {subsection}{\numberline {5.2}Discrete-Continuous Interface Formalization}{20}{}\protected@file@percent }
\@writefile{toc}{\contentsline {subsection}{\numberline {5.3}Procedure Formalization Completeness}{22}{}\protected@file@percent }
\citation{platzer2018}
\citation{kapuria2025}
\@writefile{toc}{\contentsline {subsubsection}{\numberline {2.3.2}Sequent Calculus and Differential Dynamic Logic}{5}{}\protected@file@percent }
\citation{lunze2009}
\@writefile{toc}{\contentsline {section}{\numberline {3}Research Approach}{7}{}\protected@file@percent }
\@writefile{lof}{\contentsline {figure}{\numberline {1}{\ignorespaces 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 state. Invariant violations ($\neg Inv_i$) trigger transitions to the SCRAM state. The operational level manages discrete transitions; the tactical level executes continuous control within each mode.}}{8}{}\protected@file@percent }
\newlabel{fig:hybrid_automaton}{{1}{8}{Research Approach}{figure.1}{}}
\@writefile{toc}{\contentsline {subsection}{\numberline {3.1}System Requirements, Specifications, and Discrete Controllers}{8}{}\protected@file@percent }
\@writefile{lof}{\contentsline {figure}{\numberline {2}{\ignorespaces Control scope hierarchy in nuclear power operations. Strategic control (long-term planning) remains with human management. HAHACS addresses the operational level (discrete mode switching) and tactical level (continuous control within modes), which together form a hybrid control system.}}{9}{}\protected@file@percent }
\newlabel{fig:strat_op_tact}{{2}{9}{System Requirements, Specifications, and Discrete Controllers}{figure.2}{}}
\citation{kapuria2025,lang2021}
\@writefile{toc}{\contentsline {subsection}{\numberline {3.2}Continuous Control Modes}{11}{}\protected@file@percent }
\@writefile{toc}{\contentsline {subsubsection}{\numberline {3.2.1}Transitory Modes}{12}{}\protected@file@percent }
\@writefile{toc}{\contentsline {subsubsection}{\numberline {3.2.2}Stabilizing Modes}{12}{}\protected@file@percent }
\@writefile{toc}{\contentsline {subsubsection}{\numberline {3.2.3}Expulsory Modes}{13}{}\protected@file@percent }
\@writefile{toc}{\contentsline {subsection}{\numberline {3.3}Industrial Implementation}{14}{}\protected@file@percent }
\@writefile{toc}{\contentsline {section}{\numberline {4}Metrics for Success}{15}{}\protected@file@percent }
\@writefile{toc}{\contentsline {paragraph}{TRL 3 \textit {Critical Function and Proof of Concept}}{15}{}\protected@file@percent }
\@writefile{toc}{\contentsline {paragraph}{TRL 4 \textit {Laboratory Testing of Integrated Components}}{15}{}\protected@file@percent }
\@writefile{toc}{\contentsline {paragraph}{TRL 5 \textit {Laboratory Testing in Relevant Environment}}{15}{}\protected@file@percent }
\@writefile{toc}{\contentsline {section}{\numberline {5}Risks and Contingencies}{17}{}\protected@file@percent }
\@writefile{toc}{\contentsline {subsection}{\numberline {5.1}Computational Tractability of Synthesis}{17}{}\protected@file@percent }
\@writefile{toc}{\contentsline {subsection}{\numberline {5.2}Discrete-Continuous Interface Formalization}{17}{}\protected@file@percent }
\@writefile{toc}{\contentsline {subsection}{\numberline {5.3}Procedure Formalization Completeness}{18}{}\protected@file@percent }
\citation{eia_lcoe_2022}
\citation{eesi_datacenter_2024}
\citation{eia_lcoe_2022}
\@writefile{toc}{\contentsline {section}{\numberline {6}Broader Impacts}{24}{}\protected@file@percent }
\@writefile{tdo}{\contentsline {todo}{\fcolorbox {black}{green!40}{\textcolor {green!40}{o}}\ ``If it works here, it works anywhere — strong closing argument.}{25}{}\protected@file@percent }
\pgfsyspdfmark {pgfid114}{19399794}{25935871}
\pgfsyspdfmark {pgfid117}{31254300}{25910135}
\pgfsyspdfmark {pgfid118}{35899615}{25670451}
\@writefile{toc}{\contentsline {section}{\numberline {6}Broader Impacts}{20}{}\protected@file@percent }
\bibstyle{ieeetr}
\bibdata{references}
\@writefile{toc}{\contentsline {section}{\numberline {7}Schedule, Milestones, and Deliverables}{26}{}\protected@file@percent }
\@writefile{toc}{\contentsline {section}{\numberline {7}Schedule, Milestones, and Deliverables}{22}{}\protected@file@percent }
\gtt@chartextrasize{0}{164.1287pt}
\@writefile{lof}{\contentsline {figure}{\numberline {3}{\ignorespaces Project schedule showing major research thrusts, milestones (orange row), and publications (green row). Red diamonds indicate completion points. Overlapping bars indicate parallel work where appropriate.}}{26}{}\protected@file@percent }
\newlabel{fig:gantt}{{3}{26}{Schedule, Milestones, and Deliverables}{figure.3}{}}
\@writefile{toc}{\contentsline {subsection}{\numberline {7.1}Milestones and Deliverables}{26}{}\protected@file@percent }
\@writefile{lof}{\contentsline {figure}{\numberline {3}{\ignorespaces Project schedule showing major research thrusts, milestones (orange row), and publications (green row). Red diamonds indicate completion points. Overlapping bars indicate parallel work where appropriate.}}{22}{}\protected@file@percent }
\newlabel{fig:gantt}{{3}{22}{Schedule, Milestones, and Deliverables}{figure.3}{}}
\@writefile{toc}{\contentsline {subsection}{\numberline {7.1}Milestones and Deliverables}{22}{}\protected@file@percent }
\bibcite{NUREG-0899}{1}
\bibcite{10CFR50.34}{2}
\bibcite{10CFR55.59}{3}
@ -156,14 +64,10 @@
\bibcite{10CFR50.54}{8}
\bibcite{Kemeny1979}{9}
\bibcite{WNA2020}{10}
\@writefile{tdo}{\contentsline {todo}{\fcolorbox {black}{green!40}{\textcolor {green!40}{o}}\ Clear timeline with publication targets — shows you have a plan.}{27}{}\protected@file@percent }
\pgfsyspdfmark {pgfid120}{4865044}{36388863}
\pgfsyspdfmark {pgfid123}{31254300}{36363127}
\pgfsyspdfmark {pgfid124}{35899615}{36123443}
\@writefile{toc}{\contentsline {section}{References}{27}{}\protected@file@percent }
\bibcite{hogberg_root_2013}{11}
\bibcite{zhang_analysis_2025}{12}
\bibcite{Kiniry2024}{13}
\bibcite{eia_lcoe_2022}{14}
\bibcite{eesi_datacenter_2024}{15}
\gdef \@abspage@last{30}
\@writefile{toc}{\contentsline {section}{References}{23}{}\protected@file@percent }
\gdef \@abspage@last{26}

View File

@ -1,14 +1,6 @@
This is BibTeX, Version 0.99d (TeX Live 2025)
Capacity: max_strings=200000, hash_size=200000, hash_prime=170003
The top-level auxiliary file: main.aux
White space in argument---line 77 of file main.aux
: \citation{HANDBOOK
: ON HYBRID SYSTEMS}
I'm skipping whatever remains of this command
White space in argument---line 92 of file main.aux
: \citation{MANYUS
: THESIS}
I'm skipping whatever remains of this command
The style file: ieeetr.bst
Database file #1: references.bib
Warning--entry type for "gentillon_westinghouse_1999" isn't style-file defined
@ -17,6 +9,10 @@ Warning--entry type for "operator_statistics" isn't style-file defined
--line 45 of file references.bib
Warning--entry type for "10CFR50.54" isn't style-file defined
--line 59 of file references.bib
Warning--I didn't find a database entry for "platzer2018"
Warning--I didn't find a database entry for "kapuria2025"
Warning--I didn't find a database entry for "lunze2009"
Warning--I didn't find a database entry for "lang2021"
Warning--empty author in WRPS.Description
Warning--empty year in WRPS.Description
Warning--empty journal in hogberg_root_2013
@ -25,7 +21,7 @@ Warning--empty journal in zhang_analysis_2025
Warning--empty year in zhang_analysis_2025
You've used 15 entries,
1876 wiz_defined-function locations,
555 strings with 5820 characters,
559 strings with 5859 characters,
and the built_in function-call counts, 2404 in all, are:
= -- 221
> -- 100
@ -64,4 +60,4 @@ warning$ -- 6
while$ -- 18
width$ -- 17
write$ -- 128
(There were 2 error messages)
(There were 13 warnings)

View File

@ -1,13 +1,13 @@
# Fdb version 4
["bibtex main"] 1773173597.9699 "main.aux" "main.bbl" "main" 1773173598.03253 2
["bibtex main"] 1773177450.85029 "main.aux" "main.bbl" "main" 1773177452.67459 0
"./references.bib" 1765591319.20023 14069 2a4f74c587187a8a71049043171eb0fe ""
"/usr/local/texlive/2025/texmf-dist/bibtex/bst/base/ieeetr.bst" 1292289607 18361 1a00e58565e7f19bf2b3e1bfb82254ae ""
"main.aux" 1773173597.75702 14664 f3280fe42bd32be7039c7ddcbc5aad8b "pdflatex"
"main.aux" 1773177452.46663 5783 39c4bb56f879a56ba6d791d37cde8cad "pdflatex"
(generated)
"main.bbl"
"main.blg"
(rewritten before read)
["pdflatex"] 1773173595.85606 "main.tex" "main.pdf" "main" 1773173598.03262 0
["pdflatex"] 1773177450.91171 "main.tex" "main.pdf" "main" 1773177452.67469 0
"/usr/local/texlive/2025/texmf-dist/fonts/enc/dvips/base/8r.enc" 1165713224 4850 80dc9bab7f31fb78a000ccfed0e27cab ""
"/usr/local/texlive/2025/texmf-dist/fonts/map/fontname/texfonts.map" 1577235249 3524 cb3e574dea2d1052e39280babc910dc8 ""
"/usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/symbol/psyr.tfm" 1136768653 1408 5937f58aa508ea2cea4901c07d10f5fe ""
@ -243,19 +243,18 @@
"/usr/local/texlive/2025/texmf-var/fonts/map/pdftex/updmap/pdftex.map" 1765668892 5467155 19efa205003f9ecad95fbbaa6ff24da1 ""
"/usr/local/texlive/2025/texmf-var/web2c/pdftex/pdflatex.fmt" 1741450574 3345740 46b66fdb0378f7bf5921b5eabf1762b8 ""
"/usr/local/texlive/2025/texmf.cnf" 1741450484 577 418a7058ec8e006d8704f60ecd22c938 ""
"1-goals-and-outcomes/goals.tex" 1773173595.19694 5785 7b5e137b620440854e7e220d58ca9872 ""
"2-state-of-the-art/state-of-art.tex" 1773107148.30113 14525 3b8c13d63175e6d9fd1a60995e47777f ""
"3-research-approach/approach.tex" 1773107148.30209 36035 28bfba4166bebc2d97137ab44e7cb41c ""
"4-metrics-of-success/metrics.tex" 1773107148.30251 5967 9d1414599bd374b4166fcce4de6e6644 ""
"5-risks-and-contingencies/risks.tex" 1773107148.30287 10515 44f5f800e1332517ebfe61e7db38b7cc ""
"6-broader-impacts/impacts.tex" 1773107148.30317 4912 c7ccb2b7aade93b198e985e4832fd6a8 ""
"8-schedule/schedule.tex" 1773107148.30345 4551 57e4fef2d56e8d84227d70745141e7eb ""
"1-goals-and-outcomes/goals.tex" 1773177195.1925 5785 7b5e137b620440854e7e220d58ca9872 ""
"2-state-of-the-art/state-of-art.tex" 1773177195.19317 12924 6e52fa774614756b8af3b82fa7adde74 ""
"3-research-approach/approach.tex" 1773177386.2222 32542 80e4854cc28bbad356601a10bc00bf04 ""
"4-metrics-of-success/metrics.tex" 1773177195.194 5823 5aeed4c076d6018267d9b6761018160a ""
"5-risks-and-contingencies/risks.tex" 1773177195.1943 8503 8cd69dffaaec9b0959eb2a05abb71e54 ""
"6-broader-impacts/impacts.tex" 1773177195.1946 4834 418aae223b778759691eaf9124a5360c ""
"8-schedule/schedule.tex" 1773177195.19496 4472 0e3b9ee552e03d9ad2ebaf93f6ed4502 ""
"dane_proposal_format.cls" 1769715785.9835 2883 ea175794171aa0291ef71716b2190bf0 ""
"main.aux" 1773173597.75702 14664 f3280fe42bd32be7039c7ddcbc5aad8b "pdflatex"
"main.bbl" 1773173598.03178 2919 0ea026a17b15c1ad2ed657bdbf26dfdc "bibtex main"
"main.tex" 1773173556.09967 2437 582e7a1c0b549a31e0ee40a98d020260 ""
"main.toc" 1773173597.76091 2128 2d6213c87e5e84ae87ae7dcb05dc4ca7 "pdflatex"
"todonotes.sty" 1773106207.6557 21404 916e19cbd009b6d289c8194b313d3895 ""
"main.aux" 1773177452.46663 5783 39c4bb56f879a56ba6d791d37cde8cad "pdflatex"
"main.bbl" 1773177450.90947 2919 0ea026a17b15c1ad2ed657bdbf26dfdc "bibtex main"
"main.tex" 1773177447.22721 2437 33a321fad9e5904787dda1d77a6aa5fd ""
"main.toc" 1773177452.47076 2128 300b94770f256c2d9bd0452dc1abac5e "pdflatex"
(generated)
"main.aux"
"main.log"

View File

@ -336,8 +336,6 @@ INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/utilities/pgfcalendar.c
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/colortbl/colortbl.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/colortbl/colortbl.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/graphics/color.sty
INPUT ./todonotes.sty
INPUT todonotes.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/psnfss/ot1ptm.fd
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/psnfss/ot1ptm.fd
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/psnfss/ot1ptm.fd
@ -469,8 +467,6 @@ INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/public/cm/cmr10.tfm
INPUT /usr/local/texlive/2025/texmf-dist/fonts/vf/adobe/times/zptmcm7m.vf
INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/psyro.tfm
INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/public/cm/cmmi10.tfm
INPUT /usr/local/texlive/2025/texmf-dist/fonts/vf/adobe/times/ptmri7t.vf
INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/ptmri8r.tfm
INPUT ./3-research-approach/approach.tex
INPUT ./3-research-approach/approach.tex
INPUT ./3-research-approach/approach.tex
@ -509,6 +505,7 @@ INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/public/rsfs/rsfs5.tfm
INPUT /usr/local/texlive/2025/texmf-dist/fonts/vf/adobe/times/zptmcm7m.vf
INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/psyro.tfm
INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/public/cm/cmmi10.tfm
INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/ptmri8r.tfm
INPUT /usr/local/texlive/2025/texmf-dist/fonts/vf/adobe/times/zptmcm7t.vf
INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/symbol/psyr.tfm
INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/ptmr8r.tfm
@ -528,10 +525,11 @@ INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/symbol/psyr.tfm
INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/ptmr8r.tfm
INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/public/cm/cmr10.tfm
INPUT /usr/local/texlive/2025/texmf-dist/fonts/vf/adobe/times/ptmr7t.vf
INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/ptmr7t.tfm
INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/ptmr7t.tfm
INPUT /usr/local/texlive/2025/texmf-dist/fonts/vf/adobe/times/ptmb7t.vf
INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/ptmb8r.tfm
INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/ptmr7t.tfm
INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/ptmr7t.tfm
INPUT /usr/local/texlive/2025/texmf-dist/fonts/vf/adobe/times/ptmri7t.vf
INPUT /usr/local/texlive/2025/texmf-dist/fonts/vf/adobe/times/zptmcm7t.vf
INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/symbol/psyr.tfm
INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/ptmr8r.tfm

287
main.log
View File

@ -1,4 +1,4 @@
This is pdfTeX, Version 3.141592653-2.6-1.40.27 (TeX Live 2025) (preloaded format=pdflatex 2025.3.8) 10 MAR 2026 16:13
This is pdfTeX, Version 3.141592653-2.6-1.40.27 (TeX Live 2025) (preloaded format=pdflatex 2025.3.8) 10 MAR 2026 17:17
entering extended mode
restricted \write18 enabled.
file:line:error style messages enabled.
@ -775,17 +775,13 @@ Package: colortbl 2024/07/06 v1.0i Color table columns (DPC)
\everycr=\toks52
\minrowclearance=\skip68
\rownum=\count391
) (./todonotes.sty
Package: todonotes 2024/01/05 v1.1.7 Todonotes source and documentation.
Package: todonotes 2024/01/05
\c@@todonotes@numberoftodonotes=\count392
)
LaTeX Font Info: Trying to load font information for OT1+ptm on input line 45.
(/usr/local/texlive/2025/texmf-dist/tex/latex/psnfss/ot1ptm.fd
File: ot1ptm.fd 2001/06/04 font definitions for OT1/ptm.
) (/usr/local/texlive/2025/texmf-dist/tex/latex/l3backend/l3backend-pdftex.def
File: l3backend-pdftex.def 2024-05-08 L3 backend support: PDF output (pdfTeX)
\l__color_backend_stack_int=\count393
\l__color_backend_stack_int=\count392
\l__pdf_internal_box=\box100
) (./main.aux)
\openout1 = `main.aux'.
@ -817,7 +813,7 @@ LaTeX Font Info: ... okay on input line 45.
* v-part:(T,H,B)=(72.26999pt, 650.43001pt, 72.26999pt)
* \paperwidth=614.295pt
* \paperheight=794.96999pt
* \textwidth=361.34999pt
* \textwidth=469.75502pt
* \textheight=650.43001pt
* \oddsidemargin=0.0pt
* \evensidemargin=0.0pt
@ -826,11 +822,11 @@ LaTeX Font Info: ... okay on input line 45.
* \headsep=25.0pt
* \topskip=12.0pt
* \footskip=30.0pt
* \marginparwidth=142.26378pt
* \marginparsep=8.5359pt
* \marginparwidth=44.0pt
* \marginparsep=10.0pt
* \columnsep=10.0pt
* \skip\footins=10.8pt plus 4.0pt minus 2.0pt
* \hoffset=-36.135pt
* \hoffset=0.0pt
* \voffset=0.0pt
* \mag=1000
* \@twocolumnfalse
@ -843,16 +839,16 @@ LaTeX Font Info: ... okay on input line 45.
File: fc-english.def 2016/01/12
) (/usr/local/texlive/2025/texmf-dist/tex/context/base/mkii/supp-pdf.mkii
[Loading MPS to PDF converter (version 2006.09.02).]
\scratchcounter=\count394
\scratchcounter=\count393
\scratchdimen=\dimen332
\scratchbox=\box101
\nofMPsegments=\count395
\nofMParguments=\count396
\nofMPsegments=\count394
\nofMParguments=\count395
\everyMPshowfont=\toks53
\MPscratchCnt=\count397
\MPscratchCnt=\count396
\MPscratchDim=\dimen333
\MPnumerator=\count398
\makeMPintoPDFobject=\count399
\MPnumerator=\count397
\makeMPintoPDFobject=\count398
\everyMPtoPDFconversion=\toks54
) (/usr/local/texlive/2025/texmf-dist/tex/latex/epstopdf-pkg/epstopdf-base.sty
Package: epstopdf-base 2020-01-24 v2.11 Base part for package epstopdf
@ -865,7 +861,7 @@ Package: pdflscape 2022-10-27 v0.13 Display of landscape pages in PDF
Package: pdflscape-nometadata 2022-10-28 v0.13 Display of landscape pages in PDF (HO)
Package pdflscape Info: Auto-detected driver: pdftex on input line 81.
))
\c@lstlisting=\count400
\c@lstlisting=\count399
LaTeX Font Info: Trying to load font information for OT1+ztmcm on input line 48.
(/usr/local/texlive/2025/texmf-dist/tex/latex/psnfss/ot1ztmcm.fd
File: ot1ztmcm.fd 2000/01/03 Fontinst v1.801 font definitions for OT1/ztmcm.
@ -902,11 +898,6 @@ LaTeX Font Info: Font shape `OT1/ptm/bx/n' in size <9> not available
(Font) Font shape `OT1/ptm/b/n' tried instead on input line 4.
LaTeX Font Info: Font shape `OT1/ptm/bx/n' in size <7> not available
(Font) Font shape `OT1/ptm/b/n' tried instead on input line 4.
Overfull \hbox (1.1784pt too wide) in paragraph at lines 10--10
[][] []\OT1/ptm/m/n/12 System Re-quire-ments, Spec-i-fi-ca-tions, and Dis-crete Con-trollers [][]
[]
)
\tf@toc=\write4
\openout4 = `main.toc'.
@ -915,261 +906,86 @@ Overfull \hbox (1.1784pt too wide) in paragraph at lines 10--10
[1] (./1-goals-and-outcomes/goals.tex
[1]
Overfull \hbox (3.71007pt too wide) in paragraph at lines 86--98
[]\OT1/ptm/b/n/12 Demonstrate au-tonomous re-ac-tor startup con-trol with safety guar-
[]
)
Overfull \hbox (1.53879pt too wide) in paragraph at lines 102--56
\OT1/ptm/m/n/12 from ex-ist-ing pro-ce-dures with math-e-mat-i-cal proof of cor-rect be-hav-ior. High-
[]
[1])
[2] (./2-state-of-the-art/state-of-art.tex
LaTeX Warning: Citation `NUREG-0899' on page 3 undefined on input line 19.
LaTeX Warning: Citation `10CFR50.34' on page 3 undefined on input line 19.
LaTeX Warning: Citation `10CFR55.59' on page 3 undefined on input line 23.
Overfull \hbox (2.2587pt too wide) in paragraph at lines 13--32
\OT1/ptm/m/n/12 Se-vere Ac-ci-dent Man-age-ment Guide-lines (SAMGs) for beyond-design-basis
[]
LaTeX Warning: Marginpar on page 3 moved.
LaTeX Warning: Citation `WRPS.Description' on page 3 undefined on input line 59.
LaTeX Warning: Citation `gentillon_westinghouse_1999' on page 3 undefined on input line 59.
[3]
LaTeX Warning: Citation `operator_statistics' on page 4 undefined on input line 68.
LaTeX Warning: Citation `10CFR55' on page 4 undefined on input line 71.
LaTeX Warning: Citation `10CFR50.54' on page 4 undefined on input line 72.
LaTeX Warning: Citation `Kemeny1979' on page 4 undefined on input line 84.
Overfull \hbox (6.91362pt too wide) in paragraph at lines 75--92
\OT1/ptm/m/n/12 com-pelling mo-ti-va-tion for for-mal au-to-mated con-trol with math-e-mat-i-cal safety
[]
LaTeX Warning: Citation `WNA2020' on page 4 undefined on input line 95.
LaTeX Warning: Citation `hogberg_root_2013' on page 4 undefined on input line 98.
LaTeX Warning: Citation `zhang_analysis_2025' on page 4 undefined on input line 100.
LaTeX Warning: Marginpar on page 4 moved.
LaTeX Warning: Citation `Kiniry2024' on page 4 undefined on input line 118.
Overfull \hbox (12.42279pt too wide) in paragraph at lines 116--119
\OT1/ptm/m/n/12 The High As-sur-ance Rig-or-ous Dig-i-tal En-gi-neer-ing for Nu-clear Safety (HARD-
[]
[4]
Overfull \hbox (4.45078pt too wide) in paragraph at lines 156--161
[]\OT1/ptm/b/n/12 LIMITATION: \OT1/ptm/m/it/12 HARD-ENS ad-dressed dis-crete con-trol logic with-out con-
[]
LaTeX Warning: Citation `platzer2018' on page 5 undefined on input line 181.
LaTeX Warning: Citation `Kiniry2024' on page 5 undefined on input line 165.
LaTeX Warning: Citation `kapuria2025' on page 5 undefined on input line 198.
[5]
Overfull \hbox (1.39072pt too wide) in paragraph at lines 176--184
[]\OT1/ptm/b/n/12 LIMITATION: \OT1/ptm/m/it/12 HARD-ENS achieved TRL 2--3 with-out ex-per-i-men-tal val-
[]
[5])
[6] (./3-research-approach/approach.tex
LaTeX Warning: Marginpar on page 6 moved.
)
[6]
[7] (./3-research-approach/approach.tex
LaTeX Warning: Citation `HANDBOOK ON HYBRID SYSTEMS' on page 8 undefined on input line 50.
Overfull \hbox (5.73631pt too wide) in paragraph at lines 41--52
[]\OT1/ptm/m/n/12 To build a high-assurance hy-brid au-tonomous con-trol sys-tem (HA-HACS),
[]
LaTeX Warning: Citation `lunze2009' on page 7 undefined on input line 50.
LaTeX Font Info: Trying to load font information for TS1+ptm on input line 60.
(/usr/local/texlive/2025/texmf-dist/tex/latex/psnfss/ts1ptm.fd
File: ts1ptm.fd 2001/06/04 font definitions for TS1/ptm.
)
[8]
[7]
LaTeX Font Info: Font shape `OT1/ptm/bx/n' in size <6> not available
(Font) Font shape `OT1/ptm/b/n' tried instead on input line 103.
(Font) Font shape `OT1/ptm/b/n' tried instead on input line 104.
LaTeX Font Info: Font shape `OT1/ptm/bx/n' in size <5> not available
(Font) Font shape `OT1/ptm/b/n' tried instead on input line 109.
Overfull \hbox (47.01094pt too wide) in paragraph at lines 128--134
[][]
[]
(Font) Font shape `OT1/ptm/b/n' tried instead on input line 110.
[8]
[9]
Overfull \hbox (104.18398pt too wide) in paragraph at lines 203--207
[][]
[]
[10]
LaTeX Warning: Citation `kapuria2025' on page 11 undefined on input line 367.
LaTeX Warning: Citation `lang2021' on page 11 undefined on input line 367.
[11]
[12]
LaTeX Warning: Citation `MANYUS THESIS' on page 13 undefined on input line 383.
[13])
[14] (./4-metrics-of-success/metrics.tex
[15])
[13]
[14]
[15]
Overfull \hbox (2.1067pt too wide) in paragraph at lines 578--584
[]\OT1/ptm/m/n/12 Traditional safety anal-y-sis tech-niques in-form the con-struc-tion of $\OT1/ztmcm/m/n/12 ^^B[]$\OT1/ptm/m/n/12 .
[]
[16])
[17] (./4-metrics-of-success/metrics.tex
Overfull \hbox (3.50658pt too wide) in paragraph at lines 25--35
\OT1/ptm/m/n/12 is in-suf-fi-cient for adop-tion; con-versely, show-ing em-pir-i-cal per-for-mance with-
[]
[16] (./5-risks-and-contingencies/risks.tex
[17]
[18])
[19] (./5-risks-and-contingencies/risks.tex
Overfull \hbox (0.96176pt too wide) in paragraph at lines 3--13
\OT1/ptm/m/n/12 This re-search re-lies on sev-eral crit-i-cal as-sump-tions that, if in-val-i-dated, would
[]
Overfull \hbox (8.87949pt too wide) in paragraph at lines 27--36
[]\OT1/ptm/m/n/12 Several in-di-ca-tors would pro-vide early warn-ing of com-pu-ta-tional tractabil-
[]
Overfull \hbox (3.75879pt too wide) in paragraph at lines 49--62
\OT1/ptm/m/n/12 The sec-ond crit-i-cal as-sump-tion con-cerns the map-ping be-tween boolean guard
[]
[19] (./6-broader-impacts/impacts.tex)
[20]
[21]
Overfull \hbox (2.96642pt too wide) in paragraph at lines 130--145
\OT1/ptm/m/n/12 FRETish or sim-i-lar spec-i-fi-ca-tion lan-guages would demon-strate how to bridge
[]
Overfull \hbox (2.61935pt too wide) in paragraph at lines 130--145
\OT1/ptm/m/n/12 the gap be-tween cur-rent pro-ce-dures and the pre-ci-sion needed for au-tonomous
[]
[22])
[23] (./6-broader-impacts/impacts.tex
LaTeX Warning: Citation `eia_lcoe_2022' on page 24 undefined on input line 13.
LaTeX Warning: Citation `eesi_datacenter_2024' on page 24 undefined on input line 15.
LaTeX Warning: Citation `eia_lcoe_2022' on page 24 undefined on input line 20.
[24])
[25] (./8-schedule/schedule.tex
Overfull \hbox (0.69846pt too wide) in paragraph at lines 8--18
\OT1/ptm/m/n/12 guage pro-ce-dures into machine-readable re-quire-ments. The sec-ond semester
[]
[21] (./8-schedule/schedule.tex
Missing character: There is no , in font nullfont!
Overfull \hbox (75.92079pt too wide) in paragraph at lines 71--72
[][]
[]
) (./main.bbl
Overfull \hbox (0.29076pt too wide) in paragraph at lines 78--1
\OT1/ptm/m/n/12 M1 (Month 4) con-firms that startup pro-ce-dures have been suc-cess-fully trans-
[]
[26]
Underfull \hbox (badness 1360) in paragraph at lines 23--24
[]\OT1/ptm/m/n/12 U.S. Nu-clear Reg-u-la-tory Com-mis-sion, ``Part 55|Op-er-a-tors' Li-
[]
[22]
Underfull \hbox (badness 10000) in paragraph at lines 32--33
[]\OT1/ptm/m/n/12 World Nu-clear As-so-ci-a-tion, ``Safety of nu-clear power re-
[]
Underfull \hbox (badness 10000) in paragraph at lines 32--33
\OT1/ptm/m/n/12 ac-tors.'' $\OT1/cmtt/m/n/12 https : / / www . world -[] nuclear . org / information -[]
[]
Underfull \hbox (badness 10000) in paragraph at lines 32--33
\OT1/cmtt/m/n/12 library / safety -[] and -[] security / safety -[] of -[] plants / safety -[]
\OT1/cmtt/m/n/12 nuclear . org / information -[] library / safety -[] and -[] security / safety -[] of -[]
[]
[27])
[23])
[28] (./main.aux)
[24] (./main.aux)
***********
LaTeX2e <2024-11-01> patch level 2
L3 programming layer <2025-01-18>
@ -1178,23 +994,20 @@ L3 programming layer <2025-01-18>
LaTeX Warning: There were undefined references.
LaTeX Warning: Label(s) may have changed. Rerun to get cross-references right.
)
Here is how much of TeX's memory you used:
26786 strings out of 473190
559578 string characters out of 5715801
1022906 words of memory out of 5000000
49422 multiletter control sequences out of 15000+600000
26271 strings out of 473190
547172 string characters out of 5715801
964020 words of memory out of 5000000
48910 multiletter control sequences out of 15000+600000
614280 words of font info for 155 fonts, out of 8000000 for 9000
1141 hyphenation exceptions out of 8191
110i,9n,107p,1062b,966s stack positions out of 10000i,1000n,20000p,200000b,200000s
110i,9n,107p,1062b,965s stack positions out of 10000i,1000n,20000p,200000b,200000s
</usr/local/texlive/2025/texmf-dist/fonts/type1/public/amsfonts/cm/cmmi10.pfb></usr/local/texlive/2025/texmf-dist/fonts/type1/public/amsfonts/cm/cmr10.pfb></usr/local/texlive/2025/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy10.pfb></usr/local/texlive/2025/texmf-dist/fonts/type1/public/amsfonts/cm/cmtt12.pfb></usr/local/texlive/2025/texmf-dist/fonts/type1/public/amsfonts/symbols/msbm10.pfb></usr/local/texlive/2025/texmf-dist/fonts/type1/public/rsfs/rsfs10.pfb></usr/local/texlive/2025/texmf-dist/fonts/type1/urw/symbol/usyr.pfb></usr/local/texlive/2025/texmf-dist/fonts/type1/urw/symbol/usyr.pfb></usr/local/texlive/2025/texmf-dist/fonts/type1/urw/times/utmb8a.pfb></usr/local/texlive/2025/texmf-dist/fonts/type1/urw/times/utmbi8a.pfb></usr/local/texlive/2025/texmf-dist/fonts/type1/urw/times/utmr8a.pfb></usr/local/texlive/2025/texmf-dist/fonts/type1/urw/times/utmri8a.pfb>
Output written on main.pdf (30 pages, 199129 bytes).
Output written on main.pdf (26 pages, 184723 bytes).
PDF statistics:
189 PDF objects out of 1000 (max. 8388607)
115 compressed objects within 2 object streams
177 PDF objects out of 1000 (max. 8388607)
107 compressed objects within 2 object streams
0 named destinations out of 1000 (max. 500000)
109 words of extra memory for PDF output out of 10000 (max. 10000000)

BIN
main.pdf

Binary file not shown.

View File

@ -10,7 +10,7 @@
% === SPLIT'S EDITING COMMENTS ===
% Set to 1 for edit mode (wider margins, visible comments)
% Set to 0 for final mode (normal margins, comments hidden)
\newcommand{\editmode}{1}
\newcommand{\editmode}{0}
\ifnum\editmode=1
% Edit mode: load todonotes, adjust margins

View File

@ -2,26 +2,26 @@
\contentsline {section}{\numberline {1}Goals and Outcomes}{1}{}%
\contentsline {section}{\numberline {2}State of the Art and Limits of Current Practice}{3}{}%
\contentsline {subsection}{\numberline {2.1}Current Reactor Procedures and Operation}{3}{}%
\contentsline {subsection}{\numberline {2.2}Human Factors in Nuclear Accidents}{4}{}%
\contentsline {subsection}{\numberline {2.3}Formal Methods}{5}{}%
\contentsline {subsubsection}{\numberline {2.3.1}HARDENS}{5}{}%
\contentsline {subsubsection}{\numberline {2.3.2}Sequent Calculus and Differential Dynamic Logic}{6}{}%
\contentsline {section}{\numberline {3}Research Approach}{8}{}%
\contentsline {subsection}{\numberline {3.1}System Requirements, Specifications, and Discrete Controllers}{9}{}%
\contentsline {subsection}{\numberline {3.2}Continuous Control Modes}{13}{}%
\contentsline {subsubsection}{\numberline {3.2.1}Transitory Modes}{14}{}%
\contentsline {subsubsection}{\numberline {3.2.2}Stabilizing Modes}{15}{}%
\contentsline {subsubsection}{\numberline {3.2.3}Expulsory Modes}{16}{}%
\contentsline {subsection}{\numberline {3.3}Industrial Implementation}{17}{}%
\contentsline {section}{\numberline {4}Metrics for Success}{18}{}%
\contentsline {paragraph}{TRL 3 \textit {Critical Function and Proof of Concept}}{18}{}%
\contentsline {paragraph}{TRL 4 \textit {Laboratory Testing of Integrated Components}}{18}{}%
\contentsline {paragraph}{TRL 5 \textit {Laboratory Testing in Relevant Environment}}{19}{}%
\contentsline {section}{\numberline {5}Risks and Contingencies}{20}{}%
\contentsline {subsection}{\numberline {5.1}Computational Tractability of Synthesis}{20}{}%
\contentsline {subsection}{\numberline {5.2}Discrete-Continuous Interface Formalization}{20}{}%
\contentsline {subsection}{\numberline {5.3}Procedure Formalization Completeness}{22}{}%
\contentsline {section}{\numberline {6}Broader Impacts}{24}{}%
\contentsline {section}{\numberline {7}Schedule, Milestones, and Deliverables}{26}{}%
\contentsline {subsection}{\numberline {7.1}Milestones and Deliverables}{26}{}%
\contentsline {section}{References}{27}{}%
\contentsline {subsection}{\numberline {2.2}Human Factors in Nuclear Accidents}{3}{}%
\contentsline {subsection}{\numberline {2.3}Formal Methods}{4}{}%
\contentsline {subsubsection}{\numberline {2.3.1}HARDENS}{4}{}%
\contentsline {subsubsection}{\numberline {2.3.2}Sequent Calculus and Differential Dynamic Logic}{5}{}%
\contentsline {section}{\numberline {3}Research Approach}{7}{}%
\contentsline {subsection}{\numberline {3.1}System Requirements, Specifications, and Discrete Controllers}{8}{}%
\contentsline {subsection}{\numberline {3.2}Continuous Control Modes}{11}{}%
\contentsline {subsubsection}{\numberline {3.2.1}Transitory Modes}{12}{}%
\contentsline {subsubsection}{\numberline {3.2.2}Stabilizing Modes}{12}{}%
\contentsline {subsubsection}{\numberline {3.2.3}Expulsory Modes}{13}{}%
\contentsline {subsection}{\numberline {3.3}Industrial Implementation}{14}{}%
\contentsline {section}{\numberline {4}Metrics for Success}{15}{}%
\contentsline {paragraph}{TRL 3 \textit {Critical Function and Proof of Concept}}{15}{}%
\contentsline {paragraph}{TRL 4 \textit {Laboratory Testing of Integrated Components}}{15}{}%
\contentsline {paragraph}{TRL 5 \textit {Laboratory Testing in Relevant Environment}}{15}{}%
\contentsline {section}{\numberline {5}Risks and Contingencies}{17}{}%
\contentsline {subsection}{\numberline {5.1}Computational Tractability of Synthesis}{17}{}%
\contentsline {subsection}{\numberline {5.2}Discrete-Continuous Interface Formalization}{17}{}%
\contentsline {subsection}{\numberline {5.3}Procedure Formalization Completeness}{18}{}%
\contentsline {section}{\numberline {6}Broader Impacts}{20}{}%
\contentsline {section}{\numberline {7}Schedule, Milestones, and Deliverables}{22}{}%
\contentsline {subsection}{\numberline {7.1}Milestones and Deliverables}{22}{}%
\contentsline {section}{References}{23}{}%