commit c5e7784810c9ba7f78f37a050cc7da6309fe7703 Author: Dane Sabo Date: Fri Feb 6 20:23:52 2026 -0500 first commit diff --git a/.DS_Store b/.DS_Store new file mode 100644 index 0000000..5611d09 Binary files /dev/null and b/.DS_Store differ diff --git a/1-goals-and-outcomes/research_statement_v1.tex b/1-goals-and-outcomes/research_statement_v1.tex new file mode 100644 index 0000000..0a09d93 --- /dev/null +++ b/1-goals-and-outcomes/research_statement_v1.tex @@ -0,0 +1,82 @@ +% GOAL PARAGRAPH +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. + +% INTRODUCTORY PARAGRAPH Hook +Nuclear power relies on extensively trained operators who follow detailed +written procedures to manage reactor control. Based on these procedures and +operators' interpretation of plant conditions, operators make critical decisions +about when to switch between control objectives. +% Gap +But, reliance on human operators has created an economic challenge for +next-generation nuclear power plants. Small modular reactors face significantly +higher per-megawatt staffing costs than conventional plants. Autonomous control +systems are needed that can safely manage complex operational sequences with the +same assurance as human-operated systems, but without constant supervision. + +% 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. +% Rationale +Hybrid systems use discrete logic to switch between continuous control modes, +similar to how operators change control strategies. Existing formal methods +generate provably correct switching logic but cannot handle continuous dynamics +during transitions, while traditional control theory verifies continuous +behavior but lacks tools for proving discrete switching correctness. +% Hypothesis and Technical Approach +We will bridge this gap through a three-stage methodology. First, we will +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 +discrete mode switching logic using reactive synthesis +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 +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. +% Pay-off +This approach will demonstrate autonomous control can be used for complex +nuclear power operations while maintaining safety guarantees. + +% OUTCOMES PARAGRAPHS +If this research is successful, we will be able to do the following: +\begin{enumerate} + % OUTCOME 1 Title + \item \textit{Synthesize written procedures into verified control logic.} + % Strategy + We will develop a methodology for converting written operating procedures + into formal specifications. These specifications will be synthesized into + 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 + barriers to high-assurance control systems. + + % OUTCOME 2 Title + \item \textit{Verify continuous control behavior across mode transitions. } + % Strategy + We will develop methods using reachability analysis to ensure continuous control modes + satisfy discrete transition requirements. + % Outcome + Engineers will be able to design continuous controllers using standard + practices while ensuring system correctness and proving mode transitions + occur safely at the right times. + + % OUTCOME 3 Title + \item \textit{Demonstrate autonomous reactor startup control with safety + guarantees. } + % Strategy + We will implement this methodology on a small modular reactor simulation + using industry-standard control hardware. % Outcome + 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. + +\end{enumerate} diff --git a/1-goals-and-outcomes/v1.tex b/1-goals-and-outcomes/v1.tex new file mode 100644 index 0000000..566c66b --- /dev/null +++ b/1-goals-and-outcomes/v1.tex @@ -0,0 +1,114 @@ +\section{Goals and Outcomes} + +% GOAL PARAGRAPH +The goal of this research is to develop a methodology for creating autonomous +hybrid control systems with mathematical guarantees of safe and correct +behavior. + +% INTRODUCTORY PARAGRAPH Hook +Nuclear power plants require the highest levels of control system reliability, +where failures can result in significant economic losses, service interruptions, +or radiological release. +% Known information +Currently, nuclear plant operations rely on extensively trained human operators +who follow detailed written procedures and strict regulatory requirements to +manage reactor control. These operators make critical decisions about when to +switch between different control modes based on their interpretation of plant +conditions and procedural guidance. +% Gap +This reliance on human operators prevents autonomous control capabilities and +creates a fundamental economic challenge for next-generation reactor designs. +Small modular reactors, in particular, face per-megawatt staffing costs far +exceeding those of conventional plants and threaten their economic viability. + +% Critical Need +What is needed is a method to create autonomous control systems that safely +manage complex operational sequences with the same assurance as human-operated +systems, but without constant human supervision. +% APPROACH PARAGRAPH Solution +To address this need, we will combine formal methods with control theory to +build hybrid control systems that are correct by construction. +% Rationale +Hybrid systems use discrete logic to switch between continuous control modes, +mirroring how operators change control strategies. Existing formal methods can +generate provably correct switching logic from written requirements, but they +cannot handle the continuous dynamics that occur during transitions between +modes. Meanwhile, traditional control theory can verify continuous behavior but +lacks tools for proving correctness of discrete switching decisions. +% Hypothesis +By synthesizing discrete mode transitions directly from written operating +procedures and verifying continuous behavior between transitions, we can create +hybrid control systems with end-to-end correctness guarantees. If existing +procedures can be formalized into logical specifications and continuous dynamics +verified against transition requirements, then autonomous controllers can be +built that are provably free from design defects. +% Pay-off +This approach will enable autonomous control in nuclear power plants while +maintaining the high safety standards required by the industry. + +% Qualifications +This work is conducted within the University of Pittsburgh Cyber Energy Center, +which provides access to industry collaboration and Emerson control hardware, +ensuring that developed solutions align with practical implementation +requirements. + +% OUTCOMES PARAGRAPHS +If this research is successful, we will be able to do the following: + +\begin{enumerate} + + % OUTCOME 1 Title + \item \textbf{Translate written procedures into verified control logic.} + % Strategy + We will develop a methodology for converting existing written operating + procedures into formal specifications that can be automatically synthesized + into discrete control logic. This process will use structured intermediate + representations to bridge natural language procedures and mathematical + logic. + % Outcome + Control system engineers will generate verified mode-switching controllers + directly from regulatory procedures without formal methods expertise, + lowering the barrier to high-assurance control systems. + + % OUTCOME 2 Title + \item \textbf{Verify continuous control behavior across mode transitions.} + % Strategy + We will establish methods for analyzing continuous control modes to ensure + they satisfy discrete transition requirements. Using classical control + theory for linear systems and reachability analysis for nonlinear dynamics, + we will verify that each continuous mode safely reaches its intended + transitions. + Engineers will design continuous controllers using standard practices while + iterating to ensure broader system correctness, proving that mode + transitions occur safely and at the correct times. + + % OUTCOME 3 Title + \item \textbf{Demonstrate autonomous reactor startup control with safety + guarantees.} + % Strategy + We will apply this methodology to develop an autonomous controller for + nuclear reactor startup procedures, implementing it on a small modular + reactor simulation using industry-standard control hardware. This + demonstration will prove correctness across multiple coordinated control + modes from cold shutdown through criticality to power operation. + % Outcome + We will demonstrate that autonomous hybrid control can be realized in the + nuclear industry with current equipment, establishing a path toward reduced + operator staffing while maintaining safety. + +\end{enumerate} + +% IMPACT PARAGRAPH Innovation +The innovation in this work is unifying discrete synthesis with continuous +verification to enable end-to-end correctness guarantees for hybrid systems. +% Outcome Impact +If successful, control engineers will create autonomous controllers from +existing procedures with mathematical proof of correct behavior. High-assurance +autonomous control will become practical for safety-critical applications. +% Impact/Pay-off +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 +achieve that autonomy while maintaining the exceptional safety record the +nuclear industry requires. diff --git a/2-state-of-the-art/outline.md b/2-state-of-the-art/outline.md new file mode 100644 index 0000000..593b6c1 --- /dev/null +++ b/2-state-of-the-art/outline.md @@ -0,0 +1,138 @@ +# Outline of State of the Art + +## Writing is thinking, and this is like journaling + +This research is really about using techniques that we +already have to make hybrid systems that from the jump are +provably adherent to requirements and in general that we can +say what they're gonna do fo sho. Does that make any sense? + +The critical technologies to do this are as follows, in no +particular order: discrete system theory and reactive +synthesis, temporal logics, reachability for hybrid systems. + +Things that are adjacent to what I'm doing but aren't what +I'm doing include stuff by Platzer and all the differential +dynamic logic stuff. His stuff looks like another way of +conquering this problem but adds a whole lot of complexity +and makes synthesis ambiguous. Great at checking, but what +does that mean for designing? + +I feel like I should get more sources on designing hybrid +systems. I think there are some books out there about this +maybe. + +---- +**Outline** +---- + +## 1. Hybrid Control Systems Foundations +- **Classical hybrid systems theory** (Branicky, Liberzon, +Morse - switching systems) +- **Hybrid automata and modeling** (Henzinger, Alur, Dill) +- **Stability analysis for switching systems** (Shorten, +Narendra, Lin & Antsaklis) + +**Key points to include:** +- Definition of hybrid systems and why they're needed for +complex control +- Challenges in stability analysis when switching between +controllers +- Gap between individual mode stability and overall system +stability +- Motivate why traditional control theory alone is +insufficient + +## 2. Discrete Controller Synthesis +- **Reactive synthesis from temporal logic** (Pnueli, Bloem, +Ehlers) +- **Tools like Strix, TuLiP, SLUGS** - emphasize their +discrete-only assumptions +- **LTL/GR(1) synthesis** and why these assume instantaneous +transitions + +**Key points to include:** +- Power of temporal logic for specifying complex behaviors +- Success of reactive synthesis in discrete domains +- Correctness-by-construction guarantees from synthesis +tools +- Critical limitation: assumption of instantaneous state +changes +- Why this breaks down for physical systems with continuous +dynamics + +## 3. Continuous System Verification +- **Reachability analysis** (Girard, Le Guernic, Althoff - +especially for nonlinear systems) +- **Linear system verification** (Boyd, Dullerud - classical +control meets verification) +- **Set-based methods** (Mitchell, Tomlin for +Hamilton-Jacobi reachability) + +**Key points to include:** +- Mature tools for analyzing continuous dynamics +- Reachability as the fundamental verification problem +- Computational challenges for nonlinear systems +- Gap: these are analysis tools, not synthesis tools +- They tell you if a controller works, but don't help design +it + +## 4. Existing Hybrid Verification Approaches +- **Platzer's differential dynamic logic** (as you noted - +good for verification, unclear for synthesis) +- **SpaceEx, Flow*, dReach** - model checking tools that +don't synthesize +- **Contract-based design** (Benveniste, +Sangiovanni-Vincentelli) + +**Key points to include:** +- Current approaches focus on verification after design +- Platzer's dL: powerful for proving correctness, but +synthesis unclear +- Model checking tools require pre-designed controllers +- Contract-based approaches: compositional but still +verification-focused +- Missing: unified synthesis framework that handles both +discrete and continuous + +## 5. The Gap You're Filling +- **Why discrete synthesis + continuous verification hasn't +been unified** +- **Challenges with non-instantaneous transitions** +- **The synthesis vs. verification divide** + +**Key points to include:** +- Fundamental mismatch: discrete synthesis assumes instant +transitions +- Physical reality: transitions take time and follow +continuous trajectories +- Current workflow: synthesize discrete, design continuous, +then verify +- Your contribution: unified framework for +correct-by-construction hybrid synthesis +- Nuclear startup as ideal testbed: well-defined continuous +dynamics + explicit procedural requirements + +## Key Sources to Hunt Down + +**Foundational hybrid systems:** +- Branicky's "Multiple Lyapunov functions and other analysis +tools" +- Liberzon's "Switching in Systems and Control" +- Antsaklis & Koutsoukos survey papers + +**Reactive synthesis:** +- Ehlers & Topcu on GR(1) synthesis +- Recent Strix papers (Meyer, Sickert, Luttenberger) +- Wongpiromsarn's work on TuLiP + +**Hybrid verification:** +- Althoff's reachability analysis work +- Girard's papers on abstraction-based verification +- Any recent survey on hybrid system verification tools + +**Nuclear/critical systems control:** +- Look for papers on autonomous nuclear plant operation +- Regulatory papers on control system requirements (might be +more engineering sources) + diff --git a/2-state-of-the-art/v1.tex b/2-state-of-the-art/v1.tex new file mode 100644 index 0000000..307278c --- /dev/null +++ b/2-state-of-the-art/v1.tex @@ -0,0 +1,165 @@ +\section{State of the Art and Limits of Current Practice} + +The principal aim of this research is to create autonomous reactor control +systems that are tractably safe. To understand what is being automated, we must +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. + +\subsection{Current Reactor Procedures and Operation} + +Nuclear plant procedures exist in a hierarchy: normal operating procedures for +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 +developed using guidance from NUREG-0900~\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 +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 invariants. + +\textbf{LIMITATION:} \textit{Procedures lack formal verification of correctness +and completeness.} Current procedure development relies on expert judgment and +simulator validation. 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 +invariants. Paper-based procedures cannot ensure correct application, and even +computer-based procedure systems lack the formal guarantees that automated +reasoning could provide. + +Nuclear plants operate with multiple control modes: automatic control, where the +reactor control system maintains target parameters through continuous reactivity +adjustment; manual control, where operators directly manipulate the reactor; and +various intermediate modes. In typical pressurized water reactor operation, the +reactor control system automatically maintains a floating average temperature +and compensates for power demand changes through reactivity feedback loops +alone. Safety systems, by contrast, operate with implemented automation. Reactor +Protection Systems trip automatically on safety signals with millisecond +response times, and engineered safety features actuate automatically on accident +signals without operator action required. + +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 +actuation, containment isolation, and basic process +control~\cite{WRPS.Description, gentillon_westinghouse_1999}. Human operators, +however, retain control of strategic decision-making: power level changes, +startup/shutdown sequences, mode transitions, and procedure implementation. + +\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 +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 +and one SRO for current-generation units~\cite{10CFR50.54}. Becoming a reactor +operator requires several years of training. + +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. +Operators hold legal authority under 10 CFR Part 55 to make critical decisions, +including departing from normal regulations during emergencies. 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 +system~\cite{Kemeny1979}. The President's Commission on TMI identified a +fundamental ambiguity: placing responsibility for safe power plant operations on +the licensee without formal verification that operators can fulfill this +responsibility does not guarantee safety. This tension between operational +flexibility and safety assurance remains unresolved: the person responsible for +reactor safety is often the root cause of failures. + +Multiple independent analyses converge on a striking statistic: 70--80\% of +nuclear power plant events are attributed to human error, versus approximately +20\% to equipment failures~\cite{WNA2020}. More significantly, the root cause of +all severe accidents at nuclear power plants---Three Mile Island, Chernobyl, and +Fukushima Daiichi---has been identified as poor safety management and safety +culture: primarily human factors~\cite{hogberg_root_2013}. A detailed analysis +of 190 events at Chinese nuclear power plants from +2007--2020~\cite{zhang_analysis_2025} found that 53\% of events involved active +errors, while 92\% were associated with latent errors---organizational and +systemic weaknesses that create conditions for failure. + + +\textbf{LIMITATION:} \textit{Human factors impose fundamental reliability limits +that cannot be overcome through training alone.} The persistent human +error contribution despite four decades of improvements demonstrates that these +limitations are fundamental rather than a remediable part of human-driven control. + +\subsection{HARDENS and Formal Methods} + +The High Assurance Rigorous Digital Engineering for Nuclear Safety (HARDENS) +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 +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. + +HARDENS employed formal methods tools and techniques across the verification +hierarchy. 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 +solvers. Executable formal models used Cryptol to create a behavioral model of +the entire RTS, including all subsystems, components, and limited digital twin +models of sensors, actuators, and compute infrastructure. Automatic code +synthesis generated verifiable C implementations and SystemVerilog hardware +implementations directly from Cryptol models---eliminating the traditional gap +between specification and implementation where errors commonly arise. + +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. +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 +project did not address continuous dynamics of nuclear reactor physics. Real +reactor safety depends on the interaction between continuous +processes---temperature, pressure, neutron flux---evolving in response to +discrete control decisions. HARDENS verified the discrete controller in +isolation but not the closed-loop hybrid system behavior. + +\textbf{LIMITATION:} \textit{HARDENS addressed discrete control logic without +continuous dynamics or hybrid system verification.} Verifying discrete control +logic alone provides no guarantee that the closed-loop system exhibits desired +continuous behavior such as stability, convergence to setpoints, or maintained +safety margins. + +HARDENS produced a demonstrator system at Technology Readiness Level 2--3 +(analytical proof of concept with laboratory breadboard validation) rather than +a deployment-ready system validated through extended operational testing. The +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 +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 +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 +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 +under harsh environments, human-system interaction in realistic +operational contexts, and regulatory acceptance of formal methods as +primary assurance evidence. diff --git a/3-research-approach/Untitled.canvas b/3-research-approach/Untitled.canvas new file mode 100644 index 0000000..be01c0d --- /dev/null +++ b/3-research-approach/Untitled.canvas @@ -0,0 +1,53 @@ +{ + "nodes":[ + {"id":"aed191c3719f280b","x":-500,"y":520,"width":250,"height":60,"type":"text","text":"Discrete automata"}, + {"id":"5ca8709465aa1eb8","x":-945,"y":550,"width":400,"height":375,"color":"4","type":"file","file":"Zettelkasten/Permanent Notes/20250821123741-syntcomp.md"}, + {"id":"e9c5745032b1dd06","x":-1360,"y":470,"width":340,"height":400,"color":"4","type":"file","file":"Zettelkasten/Permanent Notes/20250819103208-strix.md"}, + {"id":"a54ef0f53d23c989","x":-995,"y":-620,"width":675,"height":80,"type":"text","text":"# WHAT BELONGS IN THE RESEARCH APPROACH?"}, + {"id":"0124a70ed7d9dde1","x":-995,"y":-500,"width":250,"height":60,"type":"text","text":"What is the problem?"}, + {"id":"94ace1bf38c73a00","x":-670,"y":-500,"width":230,"height":60,"type":"text","text":"We want to automote complex systems"}, + {"id":"482ca00bb17abaf7","x":-364,"y":-500,"width":250,"height":60,"color":"1","type":"text","text":"Ultimately we're replacing human tasks"}, + {"id":"af23f539c0d2c8a8","x":-995,"y":-400,"width":250,"height":60,"type":"text","text":"We can leverage prescriptive procedures for this"}, + {"id":"3d90877135704e66","x":-995,"y":-270,"width":250,"height":60,"type":"text","text":"translation of procedures"}, + {"id":"89aac0a009838655","x":-50,"y":-500,"width":250,"height":60,"color":"1","type":"text","text":"We're doing this needing guarantees of behavior"}, + {"id":"5467e220d316b68e","x":-50,"y":-340,"width":250,"height":60,"color":"5","type":"text","text":"Formal Methods"}, + {"id":"47816cf87b1f4d37","x":-489,"y":330,"width":250,"height":60,"type":"text","text":"Reactive Synthesis"}, + {"id":"1f085c02451b41bf","x":-100,"y":640,"width":250,"height":60,"type":"text","text":"Continuous systems as transitions"}, + {"id":"7e9c528ccdb4a1d3","x":-100,"y":500,"width":250,"height":60,"type":"text","text":"Guard conditions between switching"}, + {"id":"cb089746088729eb","x":200,"y":-110,"width":250,"height":60,"color":"3","type":"text","text":"Automated translation?"}, + {"id":"80d6b5c2f79c7f50","x":-632,"y":-270,"width":250,"height":60,"type":"text","text":"FRET"}, + {"id":"a5e0333a1fd97c8e","x":-670,"y":-140,"width":325,"height":270,"type":"file","file":"Zettelkasten/Permanent Notes/20250818132022-temporal-logic.md"}, + {"id":"04df937be9ee9d65","x":280,"y":460,"width":250,"height":60,"type":"text","text":"Reachability / Barrier certificates"}, + {"id":"d10e5739a9b02d59","x":500,"y":738,"width":250,"height":60,"color":"3","type":"text","text":"Can this checking be done automatically?"}, + {"id":"92b9577c4ad80dfb","x":375,"y":603,"width":250,"height":67,"type":"text","text":"Stabilizing, Transitory, and Expulsory Modes"}, + {"id":"40c1a6ca6bb2a079","x":530,"y":160,"width":250,"height":60,"color":"2","type":"text","text":"Emerson Ovation buildout"} + ], + "edges":[ + {"id":"f0c616247ef362b8","fromNode":"47816cf87b1f4d37","fromSide":"bottom","toNode":"aed191c3719f280b","toSide":"top"}, + {"id":"68c2c4285845f3f5","fromNode":"aed191c3719f280b","fromSide":"right","toNode":"7e9c528ccdb4a1d3","toSide":"left"}, + {"id":"3071e0f7125058a4","fromNode":"47816cf87b1f4d37","fromSide":"right","toNode":"7e9c528ccdb4a1d3","toSide":"top"}, + {"id":"909f7eb2167c285a","fromNode":"7e9c528ccdb4a1d3","fromSide":"bottom","toNode":"1f085c02451b41bf","toSide":"top"}, + {"id":"00f7c15f8f153793","fromNode":"aed191c3719f280b","fromSide":"right","toNode":"1f085c02451b41bf","toSide":"left"}, + {"id":"6dabdb83917f1676","fromNode":"47816cf87b1f4d37","fromSide":"right","toNode":"cb089746088729eb","toSide":"left"}, + {"id":"7a14b61146a640dd","fromNode":"cb089746088729eb","fromSide":"right","toNode":"40c1a6ca6bb2a079","toSide":"top"}, + {"id":"373a8bc63b77ed85","fromNode":"1f085c02451b41bf","fromSide":"right","toNode":"04df937be9ee9d65","toSide":"left"}, + {"id":"6e9387d64739205d","fromNode":"5467e220d316b68e","fromSide":"bottom","toNode":"47816cf87b1f4d37","toSide":"top"}, + {"id":"c5d073eba30e1a37","fromNode":"5467e220d316b68e","fromSide":"bottom","toNode":"04df937be9ee9d65","toSide":"top"}, + {"id":"e4acffa12fc95726","fromNode":"47816cf87b1f4d37","fromSide":"bottom","toNode":"e9c5745032b1dd06","toSide":"top"}, + {"id":"5d0ea7af94f651a9","fromNode":"47816cf87b1f4d37","fromSide":"bottom","toNode":"5ca8709465aa1eb8","toSide":"top"}, + {"id":"0b6dace9fb98e600","fromNode":"e9c5745032b1dd06","fromSide":"right","toNode":"5ca8709465aa1eb8","toSide":"left"}, + {"id":"850b211b8ecde5ac","fromNode":"5ca8709465aa1eb8","fromSide":"left","toNode":"e9c5745032b1dd06","toSide":"right"}, + {"id":"d9ae9a8976519272","fromNode":"a5e0333a1fd97c8e","fromSide":"bottom","toNode":"47816cf87b1f4d37","toSide":"top"}, + {"id":"03a9e226f2d2aa09","fromNode":"3d90877135704e66","fromSide":"right","toNode":"80d6b5c2f79c7f50","toSide":"left"}, + {"id":"87fc0d0886d181eb","fromNode":"80d6b5c2f79c7f50","fromSide":"bottom","toNode":"a5e0333a1fd97c8e","toSide":"top"}, + {"id":"66a86ae15f229f63","fromNode":"0124a70ed7d9dde1","fromSide":"right","toNode":"94ace1bf38c73a00","toSide":"left"}, + {"id":"2f42c8e21d248d8f","fromNode":"af23f539c0d2c8a8","fromSide":"bottom","toNode":"3d90877135704e66","toSide":"top"}, + {"id":"6cdfe28f96ff5711","fromNode":"482ca00bb17abaf7","fromSide":"bottom","toNode":"af23f539c0d2c8a8","toSide":"right"}, + {"id":"ee4864d5b86a989b","fromNode":"94ace1bf38c73a00","fromSide":"right","toNode":"482ca00bb17abaf7","toSide":"left"}, + {"id":"1ae35a126fc91ed2","fromNode":"482ca00bb17abaf7","fromSide":"right","toNode":"89aac0a009838655","toSide":"left"}, + {"id":"ffc24ca21b2b87be","fromNode":"89aac0a009838655","fromSide":"bottom","toNode":"5467e220d316b68e","toSide":"top"}, + {"id":"af0ec4d18e1c7771","fromNode":"04df937be9ee9d65","fromSide":"top","toNode":"40c1a6ca6bb2a079","toSide":"bottom"}, + {"id":"d3dc6a0f7afb009e","fromNode":"04df937be9ee9d65","fromSide":"bottom","toNode":"92b9577c4ad80dfb","toSide":"top"}, + {"id":"e93c36e60eba4a8b","fromNode":"92b9577c4ad80dfb","fromSide":"bottom","toNode":"d10e5739a9b02d59","toSide":"top"} + ] +} \ No newline at end of file diff --git a/3-research-approach/outline.md b/3-research-approach/outline.md new file mode 100644 index 0000000..ea8a707 --- /dev/null +++ b/3-research-approach/outline.md @@ -0,0 +1,35 @@ +Okay so here's how things will go: + +Integrate V design into the workings here + +1. Requirement identification and translation + 1. Point towards hardens lando thing + 2. we're going to do a nuclear start up sequence + +2. Synthesize requirements into a discrete automata + 1. this makes up our mode switching behavior + 2. There's probably going to be a serious amount of + refinement required here + 3. Figure out by the structure of the nodes what the + purpose of the mode is + 1. Do all traces leave? Do any traces leave? What + does this mean for the FUNCTION of the node? + +3. Build controllers that satisfy each mode requirement + 1. Reachability to ensure valid input and output sets? + 2. We can ensure zeno behavior won't happen by looking + at the interface between modes + 3. We should also see based on reachability that a well + built controller ONLY can enter the modes as + specified by the discrete automata + 4. Contract based methods? + +4. Fuck it man, that's like your provability or whatever + man. + +What are the critical needs? +1. We need a way to build some operating procedures into + controllers for autonomy +2. How the hell do we know what the goals of each mode are? +3. How do we know for sure the continuous dynamics will + actually get us there? diff --git a/3-research-approach/v1.tex b/3-research-approach/v1.tex new file mode 100644 index 0000000..25de1a4 --- /dev/null +++ b/3-research-approach/v1.tex @@ -0,0 +1,285 @@ +\section{Research Approach} + +This research will overcome the limitations of current practice to build +high-assurance hybrid control systems for critical infrastructure. Building +these systems with formal correctness guarantees requires three main thrusts: + +\begin{enumerate} + \item Translate operating procedures and requirements into temporal logic + formulae + + \item Create the discrete half of a hybrid controller using reactive synthesis + + \item Develop continuous controllers to operate between modes, and verify + their correctness + +\end{enumerate} + +Commercial nuclear power operations remain manually controlled by human +operators, yet the procedures they follow are highly prescriptive and +well-documented. This suggests that human operators may not be entirely +necessary given current technology. Written procedures and requirements are +sufficiently detailed that they may be translatable into logical formulae with +minimal effort. If successful, this approach enables automation of existing +procedures without system reengineering. To formalize these procedures, we will +use temporal logic, which captures system behaviors through temporal relations. + +The most efficient path for this translation is NASA's Formal Requirements +Elicitation Tool (FRET). FRET employs a specialized requirements language called +FRETish that restricts requirements to easily understood components while +eliminating ambiguity~\cite{katis_capture_2022}. FRETish bridges natural language +and mathematical specifications through a structured English-like syntax +automatically translatable to temporal logic. + +FRET enforces this structure by requiring all requirements to contain six +components: %CITE FRET MANUAL + +\begin{enumerate} + \item Scope: \textit{What modes does this requirement apply to?} + \item Condition: \textit{Scope plus additional specificity} + \item Component: \textit{What system element does this requirement affect?} + \item Shall + \item Timing: \textit{When does the response occur?} + \item Response: \textit{What action should be taken?} +\end{enumerate} + +FRET provides functionality to check system \textit{realizability}. Realizability +analysis determines whether written requirements are complete by examining the +six structural components. Complete requirements neither conflict with one +another nor leave any behavior undefined. Systems that are not realizable from +their procedure definitions and design requirements present problems beyond +autonomous control implementation. Such systems contain behavioral +inconsistencies---the physical equivalent of software bugs. Using FRET during +autonomous controller development allows systematic identification and +resolution of these errors. + +The second category of realizability issues involves undefined behaviors +typically left to human judgment during operations. This ambiguity is +undesirable for high-assurance systems, since even well-trained humans remain +prone to errors. Addressing these specification gaps in FRET during development +yields controllers free from these vulnerabilities. + +FRET exports requirements in temporal logic format compatible with reactive +synthesis tools. Linear Temporal Logic (LTL) builds upon modal logic's +foundational operators for necessity ($\Box$, ``box'') and possibility +($\Diamond$, ``diamond''), extending them to reason about temporal +behavior~\cite{baier_principles_2008}. The box operator $\Box$ expresses that a +property holds at all future times (necessarily always), while the diamond +operator $\Diamond$ expresses that a property holds at some future time +(possibly eventually). These are complemented by the next operator ($X$) for the +immediate successor state and the until operator ($U$) for expressing +persistence conditions. + +Consider a nuclear reactor SCRAM requirement expressed in natural language: +\textit{``If a high temperature alarm triggers, control rods must immediately +insert and remain inserted until operator reset.''} This plain language +requirement can be translated into a rigorous logical specification: + +\begin{equation} + \Box(HighTemp \rightarrow X(RodsInserted \wedge (\neg + RodsWithdrawn\ U\ OperatorReset))) +\end{equation} + +This specification precisely captures the temporal relationship between the +alarm condition, the required response, and the persistence requirement. The +necessity operator $\Box$ ensures this safety property holds throughout all +possible future system executions, while the next operator $X$ enforces +immediate response. The until operator $U$ maintains the state constraint until +the reset condition occurs. No ambiguity exists in this scenario because all +decisions are represented by discrete variables. Formulating operating rules in +this logic enforces finite, correct operation. + +Reactive synthesis is an active research field focused on generating discrete +controllers from temporal logic specifications. The term ``reactive'' indicates +that the system responds to environmental inputs to produce control outputs. +These synthesized systems are finite, with each node representing a unique +discrete state. The connections between nodes, called \textit{state +transitions}, specify the conditions under which the discrete controller moves +from state to state. This complete mapping of possible states and transitions +constitutes a \textit{discrete automaton}. Discrete automata can be represented +graphically as nodes (discrete states) with edges indicating transitions between +them. From the automaton graph, one can fully describe discrete system dynamics +and develop intuitive understanding of system behavior. Hybrid systems naturally +exhibit discrete behavior amenable to formal analysis through these finite state +representations. + +We will employ state-of-the-art reactive synthesis tools, particularly Strix, +which has demonstrated superior performance in the Reactive Synthesis +Competition (SYNTCOMP) through efficient parity game solving +algorithms~\cite{meyer_strix_2018,jacobs_reactive_2024}. Strix translates linear +temporal logic specifications into deterministic automata automatically while +maximizing generated automata quality. Once constructed, the automaton can be +implemented using standard programming control flow constructs. The graphical +representation enables inspection and facilitates communication with controls +programmers who lack formal methods expertise. + +We will use discrete automata to represent the switching behavior of our hybrid +system. This approach yields an important theoretical guarantee: because the +discrete automaton is synthesized entirely through automated tools from design +requirements and operating procedures, the automaton---and therefore our hybrid +switching behavior---is \textit{correct by construction}. Correctness of the +switching controller is paramount. Mode switching represents the primary +responsibility of human operators in control rooms today. Human operators +possess the advantage of real-time judgment: when mistakes occur, they can +correct them dynamically with capabilities extending beyond written procedures. +Autonomous control lacks this adaptive advantage. Instead, autonomous +controllers replacing human operators must not make switching errors between +continuous modes. Synthesizing controllers from logical specifications with +guaranteed correctness eliminates the possibility of switching errors. + +While discrete system components will be synthesized with correctness +guarantees, they represent only half of the complete system. Autonomous +controllers like those we are developing exhibit continuous dynamics within +discrete states. These systems, called hybrid systems, combine continuous +dynamics (flows) with discrete transitions (jumps). These dynamics can be +formally expressed as~\cite{branicky_multiple_1998}: + +\begin{equation} +\dot{x}(t) = f(x(t),q(t),u(t)) +\end{equation} + +\begin{equation} +q(k+1) = \nu(x(k),q(k),u(k)) +\end{equation} + +Here, $f(\cdot)$ defines the continuous dynamics while $\nu(\cdot)$ governs +discrete transitions. The continuous states $x$, discrete state $q$, and +control input $u$ interact to produce hybrid behavior. The discrete state $q$ +defines which continuous dynamics mode is currently active. Our focus centers +on continuous autonomous hybrid systems, where continuous states remain +unchanged during jumps---a property naturally exhibited by physical systems. For +example, a nuclear reactor switching from warm-up to load-following control +cannot instantaneously change its temperature or control rod position, but can +instantaneously change control laws. + +The approach described for producing discrete automata yields physics-agnostic +specifications representing only half of a complete hybrid autonomous +controller. These automata alone cannot define the full behavior of the control +systems we aim to construct. The continuous modes will be developed after +discrete automaton construction, leveraging the automaton structure and +transitions to design multiple smaller, specialized continuous controllers. + +Notably, translation into linear temporal logic creates barriers between +different control modes. Switching from one mode to another becomes a discrete +boolean variable. \(RodsInserted\) or \(HighTemp\) in the temporal +specifications are booleans, but in the real system they represent physical +features in the state space. These features mark where continuous control modes +end and begin; their definition is critical for determining which control mode +is active at any given time. Information about where in the state space these +conditions exist will be preserved from the original requirements and included +in continuous control mode development, but will not appear as numeric values in +discrete mode switching synthesis. + +The discrete automaton transitions are key to the supervisory behavior of the +autonomous controller. These transitions mark decision points for switching +between continuous control modes and define their strategic objectives. We +will classify three types of high-level continuous controller objectives based +on discrete mode transitions: + +\begin{enumerate} + \item \textbf{Stabilizing:} A stabilizing control mode has one primary + objective: maintaining the hybrid system within its current discrete mode. + This corresponds to steady-state normal operating modes, such as a + full-power load-following controller in a nuclear power plant. Stabilizing + modes can be identified from discrete automata as nodes with only incoming + transitions. + + \item \textbf{Transitory:} A transitory control mode has the primary goal of + transitioning the hybrid system from one discrete state to another. In + nuclear applications, this might represent a controlled warm-up procedure. + Transitory modes ultimately drive the system toward a stabilizing + steady-state mode. These modes may have secondary objectives within a + discrete state, such as maintaining specific temperature ramp rates before + reaching full-power operation. + + \item \textbf{Expulsory:} An expulsory mode is a specialized transitory mode + with additional safety constraints. Expulsory modes ensure the system is + directed to a safe stabilizing mode during failure conditions. For example, + if a transitory mode fails to achieve its intended transition, the + expulsory mode activates to immediately and irreversibly guide the system + toward a globally safe state. A reactor SCRAM exemplifies an expulsory + continuous mode: when initiated, it must reliably terminate the nuclear + reaction and direct the reactor toward stabilizing decay heat removal. + +\end{enumerate} + +Building continuous modes after constructing discrete automata enables local +controller design focused on satisfying discrete transitions. The primary +challenge in hybrid system verification is ensuring global stability across +transitions~\cite{branicky_multiple_1998}. Current techniques struggle with this +problem because dynamic discontinuities complicate +verification~\cite{bansal_hamilton-jacobi_2017,guernic_reachability_2009}. This +work alleviates these problems by designing continuous controllers specifically +with transitions in mind. Decomposing continuous modes according to their +required behavior at transition points avoids solving trajectories through the +entire hybrid system. Instead, local behavior information at transition +boundaries suffices. To ensure continuous modes satisfy their requirements, we +employ three main techniques: reachability analysis, assume-guarantee contracts, +and barrier certificates. + +Reachability analysis computes the reachable set of states for a given input +set. While trivial for linear continuous systems, recent advances have extended +reachability to complex nonlinear +systems~\cite{frehse_spaceex_2011,mitchell_time-dependent_2005}. We use +reachability to define continuous state ranges at discrete transition boundaries +and verify that requirements are satisfied within continuous modes. +Assume-guarantee contracts apply when continuous state boundaries are not +explicitly defined. For any given mode, the input range for reachability +analysis is defined by the output ranges of discrete modes that transition to +it. This compositional approach ensures each continuous controller is prepared +for its possible input range, enabling reachability analysis without global +system analysis. Finally, barrier certificates prove that mode transitions are +satisfied. Barrier certificates ensure that continuous modes on either side of a +transition behave appropriately by preventing system trajectories from crossing +a given barrier. Control barrier functions certify safety by establishing +differential inequality conditions that guarantee forward invariance of safe +sets~\cite{prajna_safety_2004}. For example, a barrier certificate can guarantee +that a transitory mode transferring control to a stabilizing mode will always +move away from the transition boundary, rather than destabilizing the target +stabilizing mode. + +This compositional approach has several advantages. First, this approach breaks +down autonomous controller design into smaller pieces. For designers of future +autonomous control systems, the barrier to entry is low, and design milestones +are clear due to the procedural nature of this research plan. Second, measurable +design progress also enables measurement of regulatory adherence. Each step in +this development procedure generates an artifact that can be independently +evaluated as proof of safety and performance. Finally, the compositional nature +of this development plan enables incremental refinement between control system +layers. For example, difficulty developing a continuous mode may reflect a +discrete automaton that is too restrictive, prompting refinement of system +design requirements. This synthesis between levels promotes broader +understanding of the autonomous controller. + +To demonstrate this methodology, we will develop an autonomous startup +controller for a Small Modular Advanced High Temperature Reactor (SmAHTR). We +have already developed a high-fidelity SmAHTR model in Simulink that captures +the thermal-hydraulic and neutron kinetics behavior essential for verifying +continuous controller performance under realistic plant dynamics. The +synthesized hybrid controller will be implemented on an Emerson Ovation control +system platform, representative of industry-standard control hardware deployed +in modern nuclear facilities. The Advanced Reactor Cyber Analysis and +Development Environment (ARCADE) suite will serve as the integration layer, +managing real-time communication between the Simulink simulation and the Ovation +controller. This hardware-in-the-loop configuration enables validation of the +controller implementation on actual industrial control equipment interfacing +with a realistic reactor simulation, assessing computational performance, +real-time execution constraints, and communication latency effects. +Demonstrating autonomous startup control on this representative platform will +establish both the theoretical validity and practical feasibility of the +synthesis methodology for deployment in actual small modular reactor systems. + +This unified approach addresses a fundamental gap in hybrid system design by +bridging formal methods and control theory through a systematic, tool-supported +methodology. Translating existing nuclear procedures into temporal logic, +synthesizing provably correct discrete switching logic, and developing verified +continuous controllers creates a complete framework for autonomous hybrid +control with mathematical guarantees. The result is an autonomous controller +that not only replicates human operator decision-making but does so with formal +assurance that switching logic is correct by construction and continuous +behavior satisfies safety requirements. This methodology transforms nuclear +reactor control from a manually intensive operation requiring constant human +oversight into a fully autonomous system with higher reliability than +human-operated alternatives. More broadly, this approach establishes a +replicable framework for developing high-assurance autonomous controllers in any +domain where operating procedures are well-documented and safety is paramount. diff --git a/3-research-approach/v2.tex b/3-research-approach/v2.tex new file mode 100644 index 0000000..f06e08b --- /dev/null +++ b/3-research-approach/v2.tex @@ -0,0 +1,429 @@ +\section{Research Approach} +\iffalse + + HACS: hybrid autonomous control system + HAHACS: High-Assurance Hybrid AUtonomous Control System + + +The research approach here needs to clearly outline the solution the the problem +and identify the actions taken that will advance knowledge and solve the +problem. + +First, what is the problem? + +\textit{ + + Inhibition to adopt hybrid autonomous control in critical infrastructure is + rooted in safety concerns of system stability. Without a human in the loop + with general intelligence, HACS have not been trusted where failure modes can + be unique and novel. + +} + +So, what's the solution? + +\textit{ + + This research approach develops a methodology to build HACS that are provably + safe. This methodology builds on existing technologies, and unifies different + research thrusts to build a complete hybrid control system. To do this, the + problem of a HAHCS is broken into three distinct pieces: + + \begin{enumerate} + + \item System specification: properties of the HAHaCS such as transition + between control modes and system invariants are specified using a formal + methods tool. + - This provides exact behavior + - allows realizabillity checking of controller specs. Can a controller + actually be built from these specs? + - ? + - ? + + \item Discrete Behavior Synthesis: The discrete component of the controller + is synthesized directly from system specifications using reactive + synthesis. + - This ELIMINATES wholesale the possibility of introducing logical bugs + in the creation of the strategic part of the HAHCS. Critical decisions + that are normally made by a human are automated directly from the + formal specifications. + - This does two critical things: + - It makes the creation of the controller tractable. The reasons the + controller changes between modes acn be traced back to the + specification (and thus any requirements), which is a trace for + liability and justification of system behavior + - Discrete control decisions made by humans are reliant on the human + operator operating correctly. Humans are intrinsically probabalistic + creatures who cannot eliminate human error. By defining the behavior + of this system using temporal logics and synthesizing the controller + using deterministic algorithims, we are assured that strategic + decisions will always be made as according to operating procedures. + + \item Continuous Behavior Synthesis and Verification: The continuous + components of the controller are built using existing dynamics and control + theory but then verified using reachability and barrier certificats. + - It's very challenging (nigh impossible) to say for certain how to + build any continuous control mode. That is honestly going to be have to + left to the specific control system and its objectives. It's not really + the point of this PhD to say how to do that. For that reason, I'm going + to assume that controllers between modes are generally possible to + build. That is to say that there exists a controller that can transition + between modes, but it is a human hunt to find it. + - To check if a candidate controller does transition between discrete + modes, we do two things: + - Check invariants using reachability. Specifications will require + that control modes transiiton from one mode to the next, where + appropriate. When this is the case, these invariants are extracted to + be checked using reachability. The control mode is given the possible + entry conditions of the 'entry' mode, and the possible 'exit' states + are analyzed. A cont. controller passes this reachability test if + there is no reachable state that is not at the exit condition of the + state transition. + + --- This needs flushed out more. I think this can really be clarified + using entry and exit conditions of Mealy machines. The continuous + system IS the transition, and the reachabililty test is saying whether + or not the physical system actually satisfies the entry and exit + conditions. + + - Then, for systems that need to STAY within one mode, we will use + barrier certificates. These can let us define a continuous state + boundary, and define for a discrete controller state, the total + controller will NOT leave the continuous boundary. + + - One thing that must be considered is the idea that this analysis is + predicated on the physical system being correct to the model. If this + isn't true, we must define continuous modes that catch failure states. + If transition invariants are violated, we must shut down the system, and + build safety oriented control modes that we can be sure with a much + broader set of entry conditions will safely shut down the plant. + + -- Q for dan: is it critical to really have software to namedrop or is it + better to stay amorphous on the technology? Iirc Manyu did a little bit of + both. + + \end{enumerate} + + + What's the intellectual merit? + + \textit{ + + There is no outstanding way to build HAHACS. This methodology provides a + basis for systems engineers to think about the components of a HAHACS as + interlocking pieces whos verification interlinks into a broader system. + This will also motivate the adoption of temporal logic to define autonomous + control systems, by allowing a close connection and tracability between + requirements from regulations to system specifications. + + } + +} + +Some thoughts on invariants, and how they fit here: There are several types of +safety invariants that HAHACS might have. + +1. Conditions that initiate a switch between control modes (reactiive synthesis +relevant) + +2. Invariants about the stability of discrete states (barrier certificates) + +3. Invariants ensuring the transition between discrete states (reachability) + +4. Invariants about the timeliness of discrete transitions (??? Reachability?) + +How do we reason about all of these invariants. Well, fundamentally they can +all be reasoned about with temporal logic statements. Using next and eventually +operators, we can get to the fundamental behavior of all of these modes. What's +challenging is the fact that we ensure that all of these specifications are +validated differs between the type of invariant. This is really the beauty of +this approach, and the intellectual merit. This proposal provides a way for +hybrid control systems to be verified for autonomous control systems by +diversifying the way that the invariants are checked. + +Reactive synthesis helps us build discrete controllers using specifications +that have conditons that don't depend on time. These invariants generally are +strategic decisions, such as changing between operating modes, initiating power +level changes, or perhaps doing a refueling or shutdown routine. These +specifications are able to be nearly directly drawn from operating procedures, +and should be closely tied to instructions that would be used for human +operators. They have checkpoints for the continuous system in between different +control implements. An example is, raise power at a certain rate while ensure +temperature remains between certain bounds. These conditions are physical +states, but they are a binary result. The condition is really binary, desipite +perhaps having units of celsius or %power. When we build discrete controllers +from these specifications, we get the validation of the controller of these +specs for free by nature of reactive synthesis tools. We get direct +traceability from the operating procedure to the discrete controller +implementation with minimal human effort. + +That being said, there are no free lunches here. Ultimately, we're controlling +physical systems, and while we can automate the controller building between +stratgic objectives, it is not trivial to do so for the controller of the +physical process. These controllers are going to have to be built manually, +with the continuous dynamics of the system in mind. Helpfully, if +specifications are complete first, one can obtain discrete controller before +building physical controllers. The result of this is a simplification of +controller design, becuase the operational goals of each continuous controller +is clearly outlined by the invariants that define the goal of each discrete +mode. While for reactive synthesis purposes conditions such as a certain +temperature being reached or power level attained are binary variables, the +continuous physical meaning becomes important in the design and analysis of the +physical controllers. The continuous value of these conditions becomes the goal +of the continuous controller design, while also providing a basis to check +controller performance. + +To check continuous controllers are valid, we can split continuous controller +objectives into two types. First, we have continuous controllers that are +designed to move the plant between two different discrete modes. These will be +called 'transitory' controllers, because their entire purpose is to transition +the plant betweeen between discrete control modes. Because of the specification +of the hybrid control system a priori, we will have defined what the invariants +of these transitions are in continuous state space. Then, once a continuosu +controller design is developed, it can be validated using reachability +analysis. The input set for the analysis is the possible states that enter this +transitory mode, while the reachable states must be entirely contained within +the exit invariant for the controller to pass. At the time of writing this +proposal, it is not clear what the most efficient way to obetain this +continuous controller is, but is generally beyond the scope of this work. It is +assumed that they generally won't be so difficult to find for most systems, as +the refinement of the discrete controller should simplify the control +objectives of the physical controllers significantly. + +The second type of continuous controller that may be utilized in a HAHAHCS is a +controller that tries to maintaine a continuous steady state, such that no +discrete transitions are triggered. Reachability on these systems may not prove +a prudent approach to validating this behavior for a candidate continuous +controller, and instead, barrier certificates must be used. Barrier +certificates analyze the dynamics of the system to say whether or not flux +across a given boudnary exists. That is to say that they evaluate whether or +not there is a trajectory or not that leaves a given boundary. This definition +is exactly what defines the validity of a stabilizing continuous control mode. +Once again, because the design of the discrete controller defines careful +boundaries in continuous state space, the barrier is known a priori of which we +must satisfy this condition. This will eliminate the search for such a barrier, +and minimze complicatoin in validating stabilizing continuous control modes. + +Finally, consideration must be paid for when errors occur. The validation of +these continuous control modes hinges upon having an assumption ofcorrect +model, which in the case of a mechanical failure will almsot certainly be +invalidated. Special continuous controllers for these conditions must be +created, called 'explusory' control modes. These controllers will be +responsible for ensuring safety in case of failure, and will be designed with +reachability, but in this case, additional allocation for the allowing of +physical parameters will be allowed in the analysis. Traditional safety +analysis will also be used to identify potential failure modes, and the +modelling of their worst case dynamics. The HAHCS will be able to idenfity why +such a fault occors because an discrte boundary condition will be violated by +the continuous physical controller. That is to say, since we will have +validated the continuous control modes using reachability and barrier +certificates a priori, we will know with certainty that the only room for +dynamics to change is a shift in the plant dynamics, not that of the proven +controller. + +\fi + +%%%%%%%%%% TABLESETTING + +% what is a hybrid system really for this proposal +% Define: A hybrid system with continuous state space X ⊆ ℝⁿ and discrete modes Q = {q₁, q₂, ..., qₘ} +% Each discrete mode qᵢ has an associated continuous state region Xᵢ ⊆ X +% The discrete controller manages transitions between modes based on continuous state thresholds + +% what are requirements, anyways? + +% why do we care about defining the whole hybrid system into requirements? + +% How do different requirements line up into different parts of the system? +% (operational vs strategic requirements and their relevance to different parts +% of our system) + +Autonomous control systems are fundamentally different from automatic control +systems. The difference between these systems is the level at which +they operate. Automatic control systems are purely operational systems, + +To build a high-assurance hybrid autonomous control system (HAHACS), a +mathematical description of the system must be established. This work will make +use of automata theory while including logical statements and control theory. +The nomenclature and lexicon between these fields is far from homogenous, and +the reviewer of this proposal is not expected to be an expert in all fields +simultaneously. To present the research ideas as clearly as possible in this +section, the following syntax is explained. + +A hybrid system is a dynamical system that has both continuous and discrete +states. The specific type of system discussed in this proposal are continuous +autonomous hybrid systems. This means that these systems a) do not have +external input \footnote{This is not strictly true in our case because we allow +strategic inputs. For example, a remote powerplant may receive a start-up or +shutdown command from a different location, but only this binary high level +input is a strategic input.} and b) continuous states do not change +instantaneously when discrete states change. For our systems of interest, the +continuous states are physical, and are always Lipschitz continuous. This +nomenclature is heavily borrowed from \cite{HANDBOOK ON HYBRID SYSTEMS CONTROL}, +but is redefined here for convenience: + +\begin{equation} + H = (\mathcal{Q}, \mathcal{X}, \mathbf{f}, Init, \mathcal{G}, \mathcal{R}, Inv) +\end{equation} + +where: + +\begin{itemize} + \item \( \mathcal{Q}\): is the discrete states of the system + \item \( \mathcal{X}\): is the continuous states of the system + \item \(\mathbf{f}: \mathcal{Q} \times \mathbb{R} \rightarrow \mathbb{R} \), where + \(\mathbf{f}_i\) is a + vector field that defines the continuous dynamics for each \(q_i\) + \item \(Init\): the initial states of \(q\) and \(x\) + \item \( G\): guard + conditions that define when discrete state transitions occur + \item \(\delta: \mathcal{Q} \times G \rightarrow \mathcal{Q}\), are the + discrete state transition functions + \item \mathcal{R}: Reset maps that define state 'jumps' + \item \(Inv\): Safety invariants on the continuous dynamics +\end{itemize} + +The creation of a HAHACS essentially boils down to the creation of such a tuple +where there are proof artifacts that the intended behavior of the control system +are satisfied by the actual implementation of the control systems. But to create +such a HAHACS, we must first completely describe its behavior. + +%% Brief discussion on what each part of this tuple means for us + +\subsection{System Requirement and Specifications} + +Temporal logic is a powerful set of semantics to build systems that can have +complex but deterministic behavior. + + +%%%%%%%%%%% Building discrete controllers + +% Buildout of requirements from written procedures (this is easy for critical +% systems - we already have the requirements) + +% What happens to the invariants that specify a continuous space? Save em for +% later. Here they become binary for our purposes +% KEY POINT: We don't IMPOSE discrete abstraction - we FORMALIZE existing practice +% Operating procedures (esp. nuclear) already define go/no-go conditions as discrete predicates +% e.g., "WHEN coolant temp >315°C AND pressurizer level 30-60% THEN MAY initiate load following" +% These thresholds come from design-basis safety analysis, validated over decades +% Our methodology assumes this domain knowledge exists and provides formalization framework +% The discrete predicates p₁, p₂, ... are Boolean functions over continuous state: pᵢ: X → {true, false} +% Q: How do we rigorously set thresholds for continuous→discrete abstraction? +% Q: How do we handle hysteresis to prevent mode chattering near boundaries? +% Q: How do we account for sensor noise and measurement uncertainty? +% Q: How do we handle numerical precision issues when creating discrete automata? (relates to task 36) + +% Discrete controller implementation can be realized with reactive synthesis. +% LTL specs to automata + +% talk a bit about tools here like FRET. Talk about previous attempts. + +%%%%%%%%%%%% Building continuous controllers + +% The whole point of a hybrid system is that there are continuous components +% underneath the digital system. We built the discrete like the physical doesn't +% exist, but it really does. So how do we capture the physical system too? + +% SCOPE FRAMING: This methodology VERIFIES continuous controllers, not SYNTHESIZES them +% Compare to model checking: doesn't tell you HOW to design software, verifies if it satisfies specs +% We assume controllers can be designed using standard control theory techniques +% Our contribution: verification that candidate controllers compose correctly with discrete layer + +% What are the main different kinds of continuous modes we may see? +% Mathematical structure: Each discrete mode qᵢ provides three key pieces of information: +% 1. Entry conditions: X_entry,i ⊆ X (initial state set) +% 2. Exit conditions: X_exit,i ⊆ X (target state set) +% 3. Invariants: X_safe,i ⊆ X (safety envelope during operation) +% These come from the discrete controller synthesis and define objectives for continuous control +% Q: Who designs the continuous controllers and how? This methodology verifies +% them, but doesn't synthesize them. Is this a scope problem? + +%%%%%% Transitory modes + +% entry and exit conditions +% the goal is getting from one physical state to another +% MATHEMATICAL FORMULATION: +% Control objective: reach(X_entry,i) → reach(X_exit,i) while maintaining x(t) ∈ X_safe,i +% Standard control techniques (LQR, MPC, trajectory optimization) applied with these constraints +% +% VERIFICATION: Reachability analysis confirms ALL trajectories starting in X_entry,i +% reach X_exit,i without violating X_safe,i +% Formally: Reach(X_entry,i, f(x,u), T) ⊆ X_exit,i ∪ X_safe,i +% where f(x,u) is the closed-loop continuous dynamics +% +% we have the physical requirements from earlier specifications. Here we use +% them in a reachability analysis. This time, we use the actual physical values +% instead of the binary yes/no we used for discrete +% Q: How do we verify timing constraints? If a transitory controller eventually +% reaches the exit condition but takes too long, that violates safety. Timed +% automata? Timed reachability? +% Q: Should formalize the Mealy machine perspective - continuous system IS the +% transition, and entry/exit conditions are the discrete states. This could be +% a unifying conceptual framework. + +%%%%%% stabilizing modes + +% these are control modes with an objective of KEEPING a certain discrete state +% stable +% +% MATHEMATICAL FORMULATION: +% Control objective: remain(X_target,i) where X_target,i ⊂ X_safe,i +% Standard feedback control (PID, state feedback, LQG) applied to maintain equilibrium +% +% VERIFICATION: Barrier certificates prove closed-loop dynamics cannot escape X_safe,i +% Formally: Find B(x) s.t. ∇B(x)·f(x,u) ≤ 0 for all x ∈ ∂X_safe,i +% This proves no trajectory can cross the boundary (no flux out of safety region) +% +% we also have the physical requirements for this. These can be used for barrier +% certificates. We can prove that our model won't leave a given area without +% some disturbance. + +%%%%%% expulsory modes +% I've made an implicit assumption when talking about transitory and stabilizing +% modes. That our model is correct. This might not be true + +% In the case of a failure, our model will almost certainly be incorrect. For +% this, we have to build safe shutdown modes too, since a human won't be in the +% loop to shut things down. +% +% MATHEMATICAL FORMULATION: +% Control objective: reach(X_current) → reach(X_safe_shutdown) under parameter uncertainty +% where X_current may be anywhere in X (worst-case entry conditions) +% Dynamics have parametric uncertainty: f(x,u,θ) where θ ∈ Θ_failure +% +% VERIFICATION: Parametric reachability analysis with robustness margins +% Reach(X_current, f(x,u,θ), T) ⊆ X_safe_shutdown for all θ ∈ Θ_failure +% Conservative bounds on Θ_failure come from FMEA/traditional safety analysis + +% WE can detect physical failures exist because our physical controllers have +% previously been proven as correct by reachability and barrier certificates. We +% KNOW our controller cannot be incorrect for the plant, so if an invariant is +% violated, we KNOW it's the plant that has changed. +% Q: What about sensor failures (wrong readings vs actual plant failure)? +% Q: What about unmodeled disturbances that aren't failures? +% Q: What if model uncertainty was too optimistic to begin with? +% Need to be more precise about what "model failure" means and detect-ability. + +% We do this using continuous modes that shutdown the system, and using +% reachability analysis with parametric uncertainty, we can prove for a range of +% error conditions we can maintain safe shutdown. +% Q: How much parametric uncertainty is enough? How do we determine bounds for +% worst-case failure dynamics? Need methodology for this. + +%%%%%%%%%%%% Implementation with industrial partnerships +%%%%%%% Emerson +%talk about this +% ovation system +% scenic? Is that what they call it? +% ripe partnership with Westinghouse +% Likely build a model with a ccng plant. They already have sophisticated models +% of them +% build controller with simplified model, then test with high fidelity digital +% twin + + + + +% +%%%%%%%%%% diff --git a/4-metrics-of-success/v1.tex b/4-metrics-of-success/v1.tex new file mode 100644 index 0000000..74956ce --- /dev/null +++ b/4-metrics-of-success/v1.tex @@ -0,0 +1,88 @@ +\section{Metrics for Success} + +This research will be measured by advancement through Technology Readiness +Levels, progressing from fundamental concepts to validated prototype +demonstration. This work begins at TRL 2--3 and aims to reach TRL 5, where +system components operate successfully in a relevant laboratory environment. +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 +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 +demonstrate theoretical rigor. TRLs measure both dimensions simultaneously. +Advancing from TRL 3 to TRL 5 requires maintaining theoretical rigor while +progressively demonstrating practical feasibility. Formal verification must +remain valid as the system moves from individual components to integrated +hardware testing. + +The nuclear industry requires extremely high assurance before deploying new +control technologies. Demonstrating theoretical correctness alone is +insufficient for adoption; conversely, showing empirical performance without +formal guarantees fails to meet regulatory requirements. TRLs capture this dual +requirement naturally. Each level represents both increased practical maturity +and sustained theoretical validity. Furthermore, TRL assessment forces explicit +identification of remaining barriers to deployment. The nuclear industry already +uses TRLs for technology assessment, making this metric directly relevant to +potential adopters. Reaching TRL 5 provides a clear answer to industry questions +about feasibility and maturity that academic publications alone cannot. + +Moving from current state to target requires achieving three intermediate +levels, each representing a distinct validation milestone: + +\paragraph{TRL 3 \textit{Critical Function and Proof of Concept}} + +For this research, TRL 3 means demonstrating that each component of the +methodology works in isolation. Startup procedures must be translated into +temporal logic specifications that pass realizability analysis. A discrete +automaton must be synthesized with interpretable structure. At least one +continuous controller must be designed with reachability analysis proving +transition requirements are satisfied. Independent review must confirm that +specifications match intended procedural behavior. This proves the fundamental +approach on a simplified startup sequence. + +\paragraph{TRL 4 \textit{Laboratory Testing of Integrated Components}} + +For this research, TRL 4 means demonstrating a complete integrated hybrid +controller in simulation. All startup procedures must be formalized with a +synthesized automaton covering all operational modes. Continuous controllers +must exist for all discrete modes. Verification must be complete for all mode +transitions using reachability analysis, barrier certificates, and +assume-guarantee contracts. The integrated controller must execute complete +startup sequences in software simulation with zero safety violations across +multiple consecutive runs. This proves that formal correctness guarantees can be +maintained throughout system integration. + +\paragraph{TRL 5 \textit{Laboratory Testing in Relevant Environment}} + +For this research, TRL 5 means demonstrating the verified controller on +industrial control hardware through hardware-in-the-loop testing. The discrete +automaton must be implemented on the Emerson Ovation control system and verified +to match synthesized specifications exactly. Continuous controllers must execute +at required rates. The ARCADE interface must establish stable real-time +communication between the Emerson Ovation hardware and SmAHTR simulation. +Complete autonomous startup sequences must execute via hardware-in-the-loop +across the full operational envelope. The controller must handle off-nominal +scenarios to validate that expulsory modes function correctly. For example, +simulated sensor failures must trigger appropriate fault detection and mode +transitions, and loss-of-cooling scenarios must activate SCRAM procedures as +specified. Graded responses to minor disturbances are outside this work's scope. +Formal verification results must remain valid, with discrete behavior matching +specifications and continuous trajectories remaining within verified bounds. +This proves that the methodology produces verified controllers implementable on +industrial hardware. + +Progress will be assessed quarterly through collection of specific data +comparing actual results against TRL advancement criteria. Specification +development status indicates progress toward TRL 3. Synthesis results and +verification coverage indicate progress toward TRL 4. Simulation performance +metrics and hardware integration milestones indicate progress toward TRL 5. The +research plan will be revised only when new data invalidates fundamental +assumptions. This research succeeds if it achieves TRL 5 by demonstrating a +complete autonomous hybrid controller with formal correctness guarantees +operating on industrial control hardware through hardware-in-the-loop testing in +a relevant laboratory environment. This establishes both theoretical validity +and practical feasibility, proving that the methodology produces verified +controllers and that implementation is achievable with current technology. diff --git a/5-risks-and-contingencies/assumptions.md b/5-risks-and-contingencies/assumptions.md new file mode 100644 index 0000000..f7ee3d9 --- /dev/null +++ b/5-risks-and-contingencies/assumptions.md @@ -0,0 +1,67 @@ +# Risk and Contingencies Assumptions Exercise + +**The outcome I want to achieve is?** +- Turn written reqs into discrete controller +- Build continuous modes that ensure hybrid stability +- Implement on industrial controller with HIL simulation + +**What can't anyone solve this today?** +- Nobody has tried to build system like this with stability + in mind from the ground up. NUCE is a specific domain this + is useful. Reliance on human operators for safety. + +**The research approach I am using is?** +- Formal Methods + Control Theory +- FRET - Reachability +- Reactive Synthesis + +**This research approach relies on these fundamental +principles?** +- Temporal logic precision +- automata +- differential and difference equations +- procedure writing + +**The experiment that I will perform is?** +- trying to make an autonomous start up procedure for a +SmAHTR reactor + +**The equipment I will use is?** +1. FRET +2. STRIX +3. Simulink +4. Reachability tools +5. Ovation + +**I will analyze the results using?** +1. Prose. How hard was this to do, what MacGuyvering needed + done? What TRL? + +**The expected outcome of this experiment is?** +1. A working autonomous start up controller can take a + simulation from cold to critical without needing a human + operator to intervene. + +**What happens if this experiment does not work?** +1. We'll shift to a smaller, simpler problem where we can + overcome the limits. + +**What happens if the hypothesis or prediction is false?** +1. We'll show the gap between current procedure writing and + where we need to be to actually do synthesis. + +**What assumptions do I have that, if proven wrong, would +derail this project?** +1. Temporal logic from FRET is easy to synthesize with STRIX +2. I'm not going to have state-space explosion happen +3. Writing a start-up procedure for SmAHTR isn't that hard +4. People give a crap about molten salt reactors +5. This whole discrete boundary thing is not going to be + really hard to implement. The idea is conditions for the + transitions between modes to be boolean variables for +the temporal lgoic, but that they correspond to some surface +in the continuous state space. How am I going to keep track +of that? +6. Computational cost. Center for Research Computing is the + answer. + diff --git a/5-risks-and-contingencies/v1.tex b/5-risks-and-contingencies/v1.tex new file mode 100644 index 0000000..ea75d0e --- /dev/null +++ b/5-risks-and-contingencies/v1.tex @@ -0,0 +1,158 @@ +\section{Risks and Contingencies} + +This research relies on several critical assumptions that, if invalidated, would +require scope adjustment or methodological revision. The primary risks to +successful completion fall into four categories: computational tractability of +synthesis and verification, complexity of the discrete-continuous interface, +completeness of procedure formalization, and hardware-in-the-loop integration +challenges. Each risk has associated indicators for early detection and +contingency plans that preserve research value even if core assumptions prove +false. The staged project structure ensures that partial success yields +publishable results and clear identification of remaining barriers to +deployment. + +\subsection{Computational Tractability of Synthesis} + +The first major assumption is that formalized startup procedures will yield +automata small enough for efficient synthesis and verification. Reactive +synthesis scales exponentially with specification complexity, creating risk that +temporal logic specifications derived from complete startup procedures may +produce automata with thousands of states. Such large automata would require +synthesis times exceeding days or weeks, preventing demonstration of the +complete methodology within project timelines. Reachability analysis for +continuous modes with high-dimensional state spaces may similarly prove +computationally intractable. Either barrier would constitute a fundamental +obstacle to achieving the research objectives. + +Several indicators would provide early warning of computational tractability +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. +Reachability analysis failing to converge within reasonable time bounds would +show that continuous mode verification cannot be completed with available +computational resources. + +The contingency plan for computational intractability is to reduce scope to a +minimal viable startup sequence. This reduced sequence would cover only cold +shutdown to criticality to low-power hold, omitting power ascension and other +operational phases. The subset would still demonstrate the complete methodology +while reducing computational burden. The research contribution would remain +valid even with reduced scope, proving that formal hybrid control synthesis is +achievable for safety-critical nuclear applications. The limitation to +simplified operational sequences would be explicitly documented as a constraint +rather than a failure. + +\subsection{Discrete-Continuous Interface Formalization} + +The second critical assumption concerns the mapping between boolean guard +conditions in temporal logic and continuous state boundaries required for mode +transitions. This interface represents the fundamental challenge of hybrid +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 +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 +proposed transitions, or continuous modes may be unable to guarantee convergence +to discrete transition boundaries. + +Early indicators of interface formalization problems would appear during both +synthesis and verification phases. Guard conditions requiring complex nonlinear +predicates that resist boolean abstraction would suggest fundamental misalignment +between discrete specifications and continuous realities. Continuous safety +regions that cannot be expressed as conjunctions of half-spaces or polynomial +inequalities would indicate the interface between discrete guards and continuous +invariants is too complex. Failure to construct barrier certificates proving +safety across mode transitions would reveal that continuous dynamics cannot be +formally related to discrete switching logic. Reachability analysis showing that +continuous modes cannot reach intended transition boundaries from all possible +initial conditions would demonstrate the synthesized discrete controller is +incompatible with achievable continuous behavior. + +The primary contingency for interface complexity is restricting continuous modes +to operate within polytopic invariants. Polytopes are state regions defined as +intersections of linear half-spaces, which map directly to boolean predicates +through linear inequality checks. This restriction ensures tractable synthesis +while maintaining theoretical rigor, though at the cost of limiting +expressiveness compared to arbitrary nonlinear regions. The discrete-continuous +interface remains well-defined and verifiable with polytopic restrictions, +providing a clear fallback position that preserves the core methodology. +Conservative over-approximations offer an alternative approach: a nonlinear safe +region can be inner-approximated by a polytope, sacrificing operational +flexibility to maintain formal guarantees. The three-mode classification already +structures the problem to minimize complex transitions, with critical safety +properties concentrated in expulsory modes that can receive additional design +attention. + +Mitigation strategies focus on designing continuous controllers with discrete +transitions as primary objectives from the outset. Rather than designing +continuous control laws independently and verifying transitions post-hoc, the +approach uses transition requirements as design constraints. Control barrier +functions provide a systematic method to synthesize controllers that guarantee +forward invariance of safe sets and convergence to transition boundaries. This +design-for-verification approach reduces the likelihood that interface +complexity becomes insurmountable. Focusing verification effort on expulsory +modes---where safety is most critical---allows more complex analysis to be +applied selectively rather than uniformly across all modes, concentrating +computational resources where they matter most for safety assurance. + +\subsection{Procedure Formalization Completeness} + +The third assumption is that existing startup procedures contain sufficient +detail and clarity for translation into temporal logic specifications. Nuclear +operating procedures, while extensively detailed, were written for human +operators who bring contextual understanding and adaptive reasoning to their +interpretation. Procedures may contain implicit knowledge, ambiguous directives, +or references to operator judgment that resist formalization in current +specification languages. Underspecified timing constraints, ambiguous condition +definitions, or gaps in operational coverage would cause synthesis to fail or +produce incorrect automata. The risk is not merely that formalization is +difficult, but that current procedures fundamentally lack the precision required +for autonomous control, revealing a gap between human-oriented documentation and +machine-executable specifications. + +Several indicators would reveal formalization completeness problems early in the +project. FRET realizability checks failing due to underspecified behaviors or +conflicting requirements would indicate procedures do not form a complete +specification. Multiple valid interpretations of procedural steps with no clear +resolution would demonstrate procedure language is insufficiently precise for +automated synthesis. Procedures referencing ``operator judgment,'' ``as +appropriate,'' or similar discretionary language for critical decisions would +explicitly identify points where human reasoning cannot be directly formalized. +Domain experts unable to provide crisp answers to specification questions about +edge cases would suggest the procedures themselves do not fully define system +behavior, relying instead on operator training and experience to fill gaps. + +The contingency plan treats inadequate specification as itself a research +contribution rather than a project failure. Documenting specific ambiguities +encountered would create a taxonomy of formalization barriers: timing +underspecification, missing preconditions, discretionary actions, and undefined +failure modes. Each category would be analyzed to understand why current +procedure-writing practices produce these gaps and what specification languages +would need to address them. Proposed extensions to FRETish or similar +specification languages would demonstrate how to bridge the gap between current +procedures and the precision needed for autonomous control. The research output +would shift from ``here is a complete autonomous controller'' to ``here is what +formal autonomous control requires that current procedures do not provide, and +here are language extensions to bridge that gap.'' This contribution remains +valuable to both the nuclear industry and formal methods community, establishing +clear requirements for next-generation procedure development and autonomous +control specification languages. + +Early-stage procedure analysis with domain experts provides the primary +mitigation strategy. Collaboration through the University of Pittsburgh Cyber +Energy Center enables identification and resolution of ambiguities before +synthesis attempts, rather than discovering them during failed synthesis runs. +Iterative refinement with reactor operators and control engineers can clarify +procedural intent before formalization begins, reducing the risk of discovering +insurmountable specification gaps late in the project. Comparison with +procedures from multiple reactor designs---pressurized water reactors, boiling +water reactors, and advanced designs---may reveal common patterns and standard +ambiguities amenable to systematic resolution. This cross-design analysis would +strengthen the generalizability of any proposed specification language +extensions, ensuring they address industry-wide practices rather than specific +quirks. diff --git a/6-broader-impacts/v1.tex b/6-broader-impacts/v1.tex new file mode 100644 index 0000000..6d75f42 --- /dev/null +++ b/6-broader-impacts/v1.tex @@ -0,0 +1,71 @@ +\section{Broader Impacts} + +Nuclear power presents both a compelling application domain and an urgent +economic challenge. Recent interest in powering artificial intelligence +infrastructure has renewed focus on small modular reactors (SMRs), particularly +for hyperscale datacenters requiring hundreds of megawatts of continuous power. +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 +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 +2030~\cite{eesi_datacenter_2024}. If this demand were supplied by nuclear power, +the total annual cost of power generation would exceed \$92 billion. Within this +figure, operations and maintenance represents a substantial component. The EIA +estimates that fixed O\&M costs alone account for \$16.15 per megawatt-hour, +with additional variable O\&M costs embedded in fuel and operating +expenses~\cite{eia_lcoe_2022}. Combined, O\&M-related costs represent +approximately 23--30\% of the total levelized cost of electricity, translating +to \$21--28 billion annually for projected datacenter demand. + +This research directly addresses the multi-billion-dollar O\&M cost challenge +through high-assurance autonomous control. Current nuclear operations require +full control room staffing for each reactor, whether large conventional units or +small modular designs. These staffing requirements drive the high O\&M costs +that make nuclear power economically challenging, particularly for smaller +reactor designs where the same staffing overhead must be spread across lower +power output. Synthesizing provably correct hybrid controllers from formal +specifications can automate routine operational sequences that currently require +constant human oversight. This enables a fundamental shift from direct operator +control to supervisory monitoring, where operators oversee multiple autonomous +reactors rather than manually controlling individual units. + +The correct-by-construction methodology is critical for this transition. +Traditional automation approaches cannot provide sufficient safety guarantees +for nuclear applications, where regulatory requirements and public safety +concerns demand the highest levels of assurance. Formally verifying both the +discrete mode-switching logic and the continuous control behavior, this research +will produce controllers with mathematical proofs of correctness. These +guarantees enable automation to safely handle routine operations---startup +sequences, power level changes, and normal operational transitions---that +currently require human operators to follow written procedures. Operators will +remain in supervisory roles to handle off-normal conditions and provide +authorization for major operational changes, but the routine cognitive burden of +procedure execution shifts to provably correct automated systems that are much +cheaper to operate. + +SMRs represent an ideal deployment target for this technology. Nuclear +Regulatory Commission certification requires extensive documentation of control +procedures, operational requirements, and safety analyses written in structured +natural language. As described in our approach, these regulatory documents can +be translated into temporal logic specifications using tools like FRET, then +synthesized into discrete switching logic using reactive synthesis tools, and +finally verified using reachability analysis and barrier certificates for the +continuous control modes. The infrastructure of requirements and specifications +already exists as part of the licensing process, creating a direct pathway from +existing regulatory documentation to formally verified autonomous controllers. + +Beyond reducing operating costs for new reactors, this research will establish a +generalizable framework for autonomous control of safety-critical systems. The +methodology of translating operational procedures into formal specifications, +synthesizing discrete switching logic, and verifying continuous mode behavior +applies to any hybrid system with documented operational requirements. Potential +applications include chemical process control, aerospace systems, and autonomous +transportation, where similar economic and safety considerations favor increased +autonomy with provable correctness guarantees. Demonstrating this approach in +nuclear power---one of the most regulated and safety-critical domains---will +establish both the technical feasibility and regulatory pathway for broader +adoption across critical infrastructure. diff --git a/8-schedule/v1.tex b/8-schedule/v1.tex new file mode 100644 index 0000000..415f6e8 --- /dev/null +++ b/8-schedule/v1.tex @@ -0,0 +1,96 @@ +\section{Schedule, Milestones, and Deliverables} + +This research will be conducted over six trimesters (24 months) of full-time +effort following the proposal defense in Spring 2026. The work progresses +sequentially through three main research thrusts before culminating in +integrated demonstration and validation. + +The first semester (Spring 2026) focuses on Thrust 1, translating startup +procedures into formal temporal logic specifications using FRET. This +establishes the foundation for automated synthesis by converting natural +language procedures into machine-readable requirements. The second semester +(Summer 2026) addresses Thrust 2, using Strix to synthesize the discrete +automaton that defines mode-switching behavior. With the discrete structure +established, the third semester (Fall 2026) develops the continuous controllers +for each operational mode through Thrust 3, employing reachability analysis and +barrier certificates to verify that each mode satisfies its transition +requirements. Integration and validation occupy the remaining three semesters. + +Figure \ref{fig:gantt} shows the complete project schedule including research thrusts, major milestones, and planned publications. + +\begin{figure}[htbp] + \centering + \begin{ganttchart}[ + hgrid, + vgrid={*{4}{draw=none}, dotted}, + x unit=0.4cm, + y unit title=0.6cm, + y unit chart=0.4cm, + title/.append style={fill=gray!30}, + title height=1, + bar/.append style={fill=blue!50}, + bar height=0.5, + bar label font=\small, + milestone/.append style={fill=red, shape=diamond}, + milestone height=0.5 + ]{1}{24} + + % Timeline headers + \gantttitle{2026}{12} + \gantttitle{2027}{12} \\ + \gantttitle{Spring}{4} + \gantttitle{Summer}{4} + \gantttitle{Fall}{4} + \gantttitle{Spring}{4} + \gantttitle{Summer}{4} + \gantttitle{Fall}{4} \\ + + % Major thrusts + \ganttbar{Thrust 1: Procedure Translation}{1}{5} \\ + \ganttbar{Thrust 2: Discrete Synthesis}{4}{10} \\ + \ganttbar{Thrust 3: Continuous Control}{9}{15} \\ + \ganttbar{Integration \& Simulation (TRL 4)}{13}{17} \\ + \ganttbar{Hardware-in-Loop Testing (TRL 5)}{16}{21} \\ + \ganttbar{Dissertation Writing}{18}{24} \\[grid] + + % Milestones row + \ganttbar[bar/.append style={fill=orange!50}]{Milestones}{1}{24} + \ganttmilestone{}{4} + \ganttmilestone{}{8} + \ganttmilestone{}{12} + \ganttmilestone{}{16} + \ganttmilestone{}{20} + \ganttmilestone{}{24} \\ + + % Publications row + \ganttbar[bar/.append style={fill=green!50}]{Publications}{1}{24} + \ganttmilestone{}{8} + \ganttmilestone{}{16} + \ganttmilestone{}{20} + + \end{ganttchart} + \caption{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.} + \label{fig:gantt} +\end{figure} + +\subsection{Milestones and Deliverables} + +Six major milestones mark critical validation points throughout the research. M1 +(Month 4) confirms that startup procedures have been successfully translated to +temporal logic using FRET with realizability analysis demonstrating consistent +and complete specifications. M2 (Month 8) validates computational tractability +by demonstrating that Strix can synthesize a complete discrete automaton from +the formalized specifications. This milestone delivers a conference paper +submission to NPIC\&HMIT documenting the procedure-to-specification translation +methodology. M3 (Month 12) achieves TRL 3 by proving that continuous controllers +can be designed and verified to satisfy discrete transition requirements. This +milestone delivers an internal technical report demonstrating component-level +verification. M4 (Month 16) achieves TRL 4 through integrated simulation +demonstrating that component-level correctness composes to system-level +correctness. This milestone delivers a journal paper submission to IEEE +Transactions on Automatic Control presenting the complete hybrid synthesis +methodology. M5 (Month 20) achieves TRL 5 by demonstrating practical +implementability on industrial hardware. This milestone delivers a conference +paper submission to NPIC\&HMIT or CDC documenting hardware implementation and +experimental validation. M6 (Month 24) completes the dissertation documenting +the entire methodology, experimental results, and research contributions. diff --git a/CLAUDE.md b/CLAUDE.md new file mode 100644 index 0000000..5f4c440 --- /dev/null +++ b/CLAUDE.md @@ -0,0 +1,133 @@ +# 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 diff --git a/ERLM_Request_for_Proposals.pdf b/ERLM_Request_for_Proposals.pdf new file mode 100644 index 0000000..ca9ab63 Binary files /dev/null and b/ERLM_Request_for_Proposals.pdf differ diff --git a/README.md b/README.md new file mode 100644 index 0000000..e69de29 diff --git a/biblatex.sty b/biblatex.sty new file mode 100644 index 0000000..e69de29 diff --git a/dane_proposal_format.cls b/dane_proposal_format.cls new file mode 100644 index 0000000..a25a243 --- /dev/null +++ b/dane_proposal_format.cls @@ -0,0 +1,116 @@ +\NeedsTeXFormat{LaTeX2e} +\ProvidesClass{prayer_circle}[2025/09/02 Custom class for academic documents] + +% Pass options and load base class +\PassOptionsToClass{12pt,titlepage}{article} +\LoadClass{article} + +% Core packages +\RequirePackage[utf8]{inputenc} +\RequirePackage[margin=1.0in]{geometry} +\RequirePackage[hyphens]{url} + +% Font selection (NSF compliant) +% Uncomment ONE of the following font options: + \RequirePackage{mathptmx} % Times New Roman (11pt minimum) +% \RequirePackage{mathpazo} % Palatino (10pt minimum) +% \RequirePackage{helvet}\renewcommand{\familydefault}{\sfdefault} % Arial (10pt minimum) +% Default: Computer Modern (11pt minimum) - current 12pt is compliant + +% Document formatting +\RequirePackage[small,compact]{titlesec} +\RequirePackage{setspace} +\RequirePackage{datetime} +\RequirePackage{cite} +\RequirePackage{tocbibind} + +% Set spacing and numbering +\singlespacing +\setcounter{secnumdepth}{3} +\setcounter{tocdepth}{5} + +% Graphics and figures +\RequirePackage{graphicx} +\RequirePackage{pdfpages} +\RequirePackage{rotating} +% \RequirePackage[nolists,nomarkers]{endfloat} % Commented out - uncomment if needed + +% TikZ libraries +\RequirePackage{tikz} +\usetikzlibrary{% + positioning,% + shapes,% + arrows,% + graphs,% + calc,% + chains,% + decorations.markings,% + shadows,% + shapes.arrows,% + arrows.meta% +} + +% Standalone documents +\RequirePackage{standalone} + +% Tables +\RequirePackage{booktabs} +\RequirePackage{tabularx} +\RequirePackage{makecell} +\RequirePackage{dcolumn} +\RequirePackage{multirow} +\RequirePackage{lscape} +\setlength{\belowcaptionskip}{\abovecaptionskip} + +% Mathematics +\RequirePackage{amsmath} +\RequirePackage{amssymb} +\RequirePackage{mathrsfs} + +% Lists and code +\RequirePackage[inline]{enumitem} +\RequirePackage{listings} +\setlist{noitemsep,listparindent=24pt} + +% Specialized packages +\RequirePackage{pgfgantt} + +% Custom lengths +\newlength{\figurewidth} +\setlength{\figurewidth}{0.9\textwidth} +\newlength{\figureheight} +\setlength{\figureheight}{0.75\textheight} + +% Custom commands and counters +\newcounter{task} +\setcounter{task}{0} + +\newcommand{\task}[2]{% + \stepcounter{task}% + \subsubsection{Task \arabic{task}: #1}% + \begin{quote}% + \textit{#2}% + \end{quote}% +} + +\newcommand{\emphitem}[1]{\item \emph{#1:}} + +% Mathematical notation shortcuts +\newcommand{\mc}[1]{\mathcal{#1}} % calligraphic (Q, X, etc.) +\newcommand{\ms}[1]{\mathscr{#1}} % script +\newcommand{\mf}[1]{\mathfrak{#1}} % Fraktur/Gothic +\newcommand{\bb}[1]{\mathbb{#1}} % blackboard bold (ℝ, ℚ, etc.) + +% Default document metadata (can be overridden) +\title{From Cold Start to Critical:\\ Formal Synthesis of Autonomous Hybrid Controllers} +\author{% + PI: Dane A. Sabo\\ + dane.sabo@pitt.edu\\ + \\ + Advisor: Dr. Daniel G. Cole\\ + dgcole@pitt.edu\\ +\\ + Track: PhD Mechanical Engineering +} + +\date{\today} diff --git a/main.aux b/main.aux new file mode 100644 index 0000000..11237d0 --- /dev/null +++ b/main.aux @@ -0,0 +1,59 @@ +\relax +\providecommand \oddpage@label [2]{} +\@writefile{toc}{\contentsline {section}{Contents}{ii}{}\protected@file@percent } +\@writefile{toc}{\contentsline {section}{\numberline {1}Goals and Outcomes}{1}{}\protected@file@percent } +\citation{NUREG-0899,10CFR50.34} +\citation{10CFR55.59} +\citation{WRPS.Description,gentillon_westinghouse_1999} +\citation{operator_statistics} +\citation{10CFR55} +\citation{10CFR50.54} +\@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{Kemeny1979} +\citation{WNA2020} +\citation{hogberg_root_2013} +\citation{zhang_analysis_2025} +\citation{Kiniry2024} +\@writefile{toc}{\contentsline {subsection}{\numberline {2.3}HARDENS and Formal Methods}{4}{}\protected@file@percent } +\citation{Kiniry2024} +\citation{HANDBOOK ON HYBRID SYSTEMS CONTROL} +\@writefile{toc}{\contentsline {section}{\numberline {3}Research Approach}{6}{}\protected@file@percent } +\@writefile{toc}{\contentsline {subsection}{\numberline {3.1}System Requirement and Specifications}{6}{}\protected@file@percent } +\@writefile{toc}{\contentsline {section}{\numberline {4}Metrics for Success}{7}{}\protected@file@percent } +\@writefile{toc}{\contentsline {paragraph}{TRL 3 \textit {Critical Function and Proof of Concept}}{7}{}\protected@file@percent } +\@writefile{toc}{\contentsline {paragraph}{TRL 4 \textit {Laboratory Testing of Integrated Components}}{7}{}\protected@file@percent } +\@writefile{toc}{\contentsline {paragraph}{TRL 5 \textit {Laboratory Testing in Relevant Environment}}{7}{}\protected@file@percent } +\@writefile{toc}{\contentsline {section}{\numberline {5}Risks and Contingencies}{9}{}\protected@file@percent } +\@writefile{toc}{\contentsline {subsection}{\numberline {5.1}Computational Tractability of Synthesis}{9}{}\protected@file@percent } +\@writefile{toc}{\contentsline {subsection}{\numberline {5.2}Discrete-Continuous Interface Formalization}{9}{}\protected@file@percent } +\@writefile{toc}{\contentsline {subsection}{\numberline {5.3}Procedure Formalization Completeness}{10}{}\protected@file@percent } +\citation{eia_lcoe_2022} +\citation{eesi_datacenter_2024} +\citation{eia_lcoe_2022} +\@writefile{toc}{\contentsline {section}{\numberline {6}Broader Impacts}{12}{}\protected@file@percent } +\bibstyle{ieeetr} +\bibdata{references} +\@writefile{toc}{\contentsline {section}{\numberline {7}Schedule, Milestones, and Deliverables}{14}{}\protected@file@percent } +\gtt@chartextrasize{0}{164.1287pt} +\@writefile{lof}{\contentsline {figure}{\numberline {1}{\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.}}{14}{}\protected@file@percent } +\newlabel{fig:gantt}{{1}{14}{Schedule, Milestones, and Deliverables}{figure.1}{}} +\@writefile{toc}{\contentsline {subsection}{\numberline {7.1}Milestones and Deliverables}{14}{}\protected@file@percent } +\bibcite{NUREG-0899}{1} +\bibcite{10CFR50.34}{2} +\bibcite{10CFR55.59}{3} +\bibcite{WRPS.Description}{4} +\bibcite{gentillon_westinghouse_1999}{5} +\bibcite{operator_statistics}{6} +\bibcite{10CFR55}{7} +\bibcite{10CFR50.54}{8} +\bibcite{Kemeny1979}{9} +\bibcite{WNA2020}{10} +\bibcite{hogberg_root_2013}{11} +\bibcite{zhang_analysis_2025}{12} +\bibcite{Kiniry2024}{13} +\bibcite{eia_lcoe_2022}{14} +\bibcite{eesi_datacenter_2024}{15} +\@writefile{toc}{\contentsline {section}{References}{15}{}\protected@file@percent } +\gdef \@abspage@last{19} diff --git a/main.bbl b/main.bbl new file mode 100644 index 0000000..6fba831 --- /dev/null +++ b/main.bbl @@ -0,0 +1,52 @@ +\begin{thebibliography}{10} + +\bibitem{NUREG-0899} +{U.S. Nuclear Regulatory Commission}, ``Guidelines for the preparation of emergency operating procedures,'' Tech. Rep. NUREG-0899, U.S. Nuclear Regulatory Commission, 1982. + +\bibitem{10CFR50.34} +{U.S. Nuclear Regulatory Commission}, ``{10 CFR Part 50.34}.'' Code of Federal Regulations. + +\bibitem{10CFR55.59} +{U.S. Nuclear Regulatory Commission}, ``{10 CFR Part 55.59}.'' Code of Federal Regulations. + +\bibitem{WRPS.Description} +``{Westinghouse RPS System Description},'' tech. rep., Westinghouse Electric Corporation. + +\bibitem{gentillon_westinghouse_1999} +C.~D. Gentillon, D.~Marksberry, D.~Rasmuson, M.~B. Calley, S.~A. Eide, and T.~Wierman, ``Westinghouse reactor protection system unavailability, 1984-1995.'' +\newblock Number: {INEEL}/{CON}-99-00374 Publisher: Idaho National Engineering and Environmental Laboratory. + +\bibitem{operator_statistics} +{U.S. Nuclear Regulatory Commission}, ``{Operator Licensing}.'' \url{https://www.nrc.gov/reactors/operator-licensing}. + +\bibitem{10CFR55} +{U.S. Nuclear Regulatory Commission}, ``{Part 55—Operators' Licenses}.'' \url{https://www.nrc.gov/reading-rm/doc-collections/cfr/part055/full-text}. + +\bibitem{10CFR50.54} +{U.S. Nuclear Regulatory Commission}, ``{§ 50.54 Conditions of Licenses}.'' \url{https://www.nrc.gov/reading-rm/doc-collections/cfr/part050/part050-0054}. + +\bibitem{Kemeny1979} +J.~G. Kemeny {\em et~al.}, ``Report of the president's commission on the accident at three mile island,'' tech. rep., President's Commission on the Accident at Three Mile Island, October 1979. + +\bibitem{WNA2020} +{World Nuclear Association}, ``Safety of nuclear power reactors.'' \url{https://www.world-nuclear.org/information-library/safety-and-security/safety-of-plants/safety-of-nuclear-power-reactors.aspx}, 2020. + +\bibitem{hogberg_root_2013} +L.~Högberg, ``Root causes and impacts of severe accidents at large nuclear power plants,'' vol.~42, no.~3, pp.~267--284. + +\bibitem{zhang_analysis_2025} +M.~Zhang, L.~Dai, W.~Chen, and E.~Pang, ``Analysis of human errors in nuclear power plant event reports,'' vol.~57, no.~10, p.~103687. + +\bibitem{Kiniry2024} +J.~Kiniry, A.~Bakst, S.~Hansen, M.~Podhradsky, and A.~Bivin, ``High assurance rigorous digital engineering for nuclear safety (hardens) final technical report,'' Tech. Rep. TLR-RES-RES/DE-2024-005, Galois, Inc. / U.S. Nuclear Regulatory Commission, 2024. +\newblock NRC Contract 31310021C0014. + +\bibitem{eia_lcoe_2022} +{U.S. Energy Information Administration}, ``Levelized costs of new generation resources in the annual energy outlook 2022,'' report, U.S. Energy Information Administration, March 2022. +\newblock See Table 1b, page 9. + +\bibitem{eesi_datacenter_2024} +{Environmental and Energy Study Institute}, ``Data center energy needs are upending power grids and threatening the climate.'' Web article, 2024. +\newblock Accessed: 2025-09-29. + +\end{thebibliography} diff --git a/main.blg b/main.blg new file mode 100644 index 0000000..1dd9ec5 --- /dev/null +++ b/main.blg @@ -0,0 +1,63 @@ +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 21 of file main.aux + : \citation{HANDBOOK + : ON HYBRID SYSTEMS CONTROL} +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 +--line 32 of file references.bib +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--empty author in WRPS.Description +Warning--empty year in WRPS.Description +Warning--empty journal in hogberg_root_2013 +Warning--empty year in hogberg_root_2013 +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, +and the built_in function-call counts, 2404 in all, are: += -- 221 +> -- 100 +< -- 2 ++ -- 42 +- -- 27 +* -- 143 +:= -- 371 +add.period$ -- 18 +call.type$ -- 15 +change.case$ -- 18 +chr.to.int$ -- 0 +cite$ -- 21 +duplicate$ -- 102 +empty$ -- 259 +format.name$ -- 27 +if$ -- 575 +int.to.chr$ -- 0 +int.to.str$ -- 15 +missing$ -- 2 +newline$ -- 52 +num.names$ -- 14 +pop$ -- 64 +preamble$ -- 1 +purify$ -- 0 +quote$ -- 0 +skip$ -- 78 +stack$ -- 0 +substring$ -- 44 +swap$ -- 22 +text.length$ -- 2 +text.prefix$ -- 0 +top$ -- 0 +type$ -- 0 +warning$ -- 6 +while$ -- 18 +width$ -- 17 +write$ -- 128 +(There was 1 error message) diff --git a/main.fdb_latexmk b/main.fdb_latexmk new file mode 100644 index 0000000..64b3ab5 --- /dev/null +++ b/main.fdb_latexmk @@ -0,0 +1,264 @@ +# Fdb version 4 +["bibtex main"] 1769715964.87129 "main.aux" "main.bbl" "main" 1770062339.7998 2 + "./references.bib" 1765591319.20023 14069 2a4f74c587187a8a71049043171eb0fe "" + "/usr/local/texlive/2025/texmf-dist/bibtex/bst/base/ieeetr.bst" 1292289607 18361 1a00e58565e7f19bf2b3e1bfb82254ae "" + "main.aux" 1770062339.59974 3798 3e4f846d5a63c369ad994a87de4a30be "pdflatex" + (generated) + "main.bbl" + "main.blg" + (rewritten before read) +["pdflatex"] 1770062338.22246 "main.tex" "main.pdf" "main" 1770062339.79991 2 + "/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 "" + "/usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/psyro.tfm" 1136768653 1544 23a042a74981a3e4b6ce2e350e390409 "" + "/usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/ptmb7t.tfm" 1136768653 2172 fd0c924230362ff848a33632ed45dc23 "" + "/usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/ptmb8r.tfm" 1136768653 4524 6bce29db5bc272ba5f332261583fee9c "" + "/usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/ptmbi7t.tfm" 1136768653 2228 e564491c42a4540b5ebb710a75ff306c "" + "/usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/ptmbi8r.tfm" 1136768653 4480 10409ed8bab5aea9ec9a78028b763919 "" + "/usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/ptmr7t.tfm" 1136768653 2124 2601a75482e9426d33db523edf23570a "" + "/usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/ptmr8c.tfm" 1136768653 1352 fa28a7e6d323c65ce7d13d5342ff6be2 "" + "/usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/ptmr8r.tfm" 1136768653 4408 25b74d011a4c66b7f212c0cc3c90061b "" + "/usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/ptmri7t.tfm" 1136768653 2288 f478fc8fed18759effb59f3dad7f3084 "" + "/usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/ptmri8r.tfm" 1136768653 4640 532ca3305aad10cc01d769f3f91f1029 "" + "/usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/zptmcm7m.tfm" 1136768653 2232 db256afffc8202da192b4641df14d602 "" + "/usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/zptmcm7t.tfm" 1136768653 2172 1d00c2a0d10f23031be62329457a870c "" + "/usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/zptmcm7v.tfm" 1136768653 1032 20febbd0f0c9a48eb78616f897008286 "" + "/usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/zptmcm7y.tfm" 1136768653 1520 ad7b3c1a480a03b3e41b5fbb13d938f2 "" + "/usr/local/texlive/2025/texmf-dist/fonts/tfm/public/amsfonts/symbols/msam10.tfm" 1246382020 916 f87d7c45f9c908e672703b83b72241a3 "" + "/usr/local/texlive/2025/texmf-dist/fonts/tfm/public/amsfonts/symbols/msbm10.tfm" 1246382020 908 2921f8a10601f252058503cc6570e581 "" + "/usr/local/texlive/2025/texmf-dist/fonts/tfm/public/cm/cmmi10.tfm" 1136768653 1528 abec98dbc43e172678c11b3b9031252a "" + "/usr/local/texlive/2025/texmf-dist/fonts/tfm/public/cm/cmr10.tfm" 1136768653 1296 45809c5a464d5f32c8f98ba97c1bb47f "" + "/usr/local/texlive/2025/texmf-dist/fonts/tfm/public/cm/cmr12.tfm" 1136768653 1288 655e228510b4c2a1abe905c368440826 "" + "/usr/local/texlive/2025/texmf-dist/fonts/tfm/public/cm/cmsy10.tfm" 1136768653 1124 6c73e740cf17375f03eec0ee63599741 "" + "/usr/local/texlive/2025/texmf-dist/fonts/tfm/public/cm/cmtt12.tfm" 1136768653 772 9a936b7f5e2ff0557fce0f62822f0bbf "" + "/usr/local/texlive/2025/texmf-dist/fonts/tfm/public/rsfs/rsfs10.tfm" 1229303445 688 37338d6ab346c2f1466b29e195316aa4 "" + "/usr/local/texlive/2025/texmf-dist/fonts/tfm/public/rsfs/rsfs5.tfm" 1229303445 684 3a51bd4fd9600428d5264cf25f04bb9a "" + "/usr/local/texlive/2025/texmf-dist/fonts/tfm/public/rsfs/rsfs7.tfm" 1229303445 692 1b6510779f0f05e9cbf03e0f6c8361e6 "" + "/usr/local/texlive/2025/texmf-dist/fonts/type1/public/amsfonts/cm/cmmi10.pfb" 1248133631 36299 5f9df58c2139e7edcf37c8fca4bd384d "" + "/usr/local/texlive/2025/texmf-dist/fonts/type1/public/amsfonts/cm/cmr10.pfb" 1248133631 35752 024fb6c41858982481f6968b5fc26508 "" + "/usr/local/texlive/2025/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy10.pfb" 1248133631 32569 5e5ddc8df908dea60932f3c484a54c0d "" + "/usr/local/texlive/2025/texmf-dist/fonts/type1/public/amsfonts/cm/cmtt12.pfb" 1248133631 24252 1e4e051947e12dfb50fee0b7f4e26e3a "" + "/usr/local/texlive/2025/texmf-dist/fonts/type1/public/amsfonts/symbols/msbm10.pfb" 1248133631 34694 ad62b13721ee8eda1dcc8993c8bd7041 "" + "/usr/local/texlive/2025/texmf-dist/fonts/type1/public/rsfs/rsfs10.pfb" 1229303445 16077 4737ac34f0fb5608550f3780a0202c22 "" + "/usr/local/texlive/2025/texmf-dist/fonts/type1/urw/symbol/usyr.pfb" 1136849748 33709 b09d2e140b7e807d3a97058263ab6693 "" + "/usr/local/texlive/2025/texmf-dist/fonts/type1/urw/times/utmb8a.pfb" 1136849748 44729 811d6c62865936705a31c797a1d5dada "" + "/usr/local/texlive/2025/texmf-dist/fonts/type1/urw/times/utmbi8a.pfb" 1136849748 44656 0cbca70e0534538582128f6b54593cca "" + "/usr/local/texlive/2025/texmf-dist/fonts/type1/urw/times/utmr8a.pfb" 1136849748 46026 6dab18b61c907687b520c72847215a68 "" + "/usr/local/texlive/2025/texmf-dist/fonts/type1/urw/times/utmri8a.pfb" 1136849748 45458 a3faba884469519614ca56ba5f6b1de1 "" + "/usr/local/texlive/2025/texmf-dist/fonts/vf/adobe/times/ptmb7t.vf" 1136768653 1372 788387fea833ef5963f4c5bffe33eb89 "" + "/usr/local/texlive/2025/texmf-dist/fonts/vf/adobe/times/ptmbi7t.vf" 1136768653 1384 6ac0f8b839230f5d9389287365b243c0 "" + "/usr/local/texlive/2025/texmf-dist/fonts/vf/adobe/times/ptmr7t.vf" 1136768653 1380 0ea3a3370054be6da6acd929ec569f06 "" + "/usr/local/texlive/2025/texmf-dist/fonts/vf/adobe/times/ptmr8c.vf" 1136768653 3556 8a9a6dcbcd146ef985683f677f4758a6 "" + "/usr/local/texlive/2025/texmf-dist/fonts/vf/adobe/times/ptmri7t.vf" 1136768653 1384 a9d8adaf491ce34e5fba99dc7bbe5f39 "" + "/usr/local/texlive/2025/texmf-dist/fonts/vf/adobe/times/zptmcm7m.vf" 1136768653 1132 27520247d3fe18d4266a226b461885c2 "" + "/usr/local/texlive/2025/texmf-dist/fonts/vf/adobe/times/zptmcm7t.vf" 1136768653 1108 d271d6f9de4122c3f8d3b65666167fac "" + "/usr/local/texlive/2025/texmf-dist/fonts/vf/adobe/times/zptmcm7y.vf" 1136768653 964 5673178ff30617b900214de28ab32b38 "" + "/usr/local/texlive/2025/texmf-dist/tex/context/base/mkii/supp-pdf.mkii" 1461363279 71627 94eb9990bed73c364d7f53f960cc8c5b "" + "/usr/local/texlive/2025/texmf-dist/tex/generic/iftex/iftex.sty" 1734129479 7984 7dbb9280f03c0a315425f1b4f35d43ee "" + "/usr/local/texlive/2025/texmf-dist/tex/generic/iftex/ifvtex.sty" 1572645307 1057 525c2192b5febbd8c1f662c9468335bb "" + "/usr/local/texlive/2025/texmf-dist/tex/generic/ltxcmds/ltxcmds.sty" 1701727651 17865 1a9bd36b4f98178fa551aca822290953 "" + "/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/basiclayer/pgfcore.code.tex" 1673816307 1016 1c2b89187d12a2768764b83b4945667c "" + "/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/basiclayer/pgfcorearrows.code.tex" 1601326656 43820 1fef971b75380574ab35a0d37fd92608 "" + "/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/basiclayer/pgfcoreexternal.code.tex" 1601326656 19324 f4e4c6403dd0f1605fd20ed22fa79dea "" + "/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/basiclayer/pgfcoregraphicstate.code.tex" 1601326656 6038 ccb406740cc3f03bbfb58ad504fe8c27 "" + "/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/basiclayer/pgfcoreimage.code.tex" 1673816307 6911 f6d4cf5a3fef5cc879d668b810e82868 "" + "/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/basiclayer/pgfcorelayers.code.tex" 1601326656 4883 42daaf41e27c3735286e23e48d2d7af9 "" + "/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/basiclayer/pgfcoreobjects.code.tex" 1601326656 2544 8c06d2a7f0f469616ac9e13db6d2f842 "" + "/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/basiclayer/pgfcorepathconstruct.code.tex" 1601326656 44195 5e390c414de027626ca5e2df888fa68d "" + "/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/basiclayer/pgfcorepathprocessing.code.tex" 1601326656 17311 2ef6b2e29e2fc6a2fc8d6d652176e257 "" + "/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/basiclayer/pgfcorepathusage.code.tex" 1601326656 21302 788a79944eb22192a4929e46963a3067 "" + "/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/basiclayer/pgfcorepatterns.code.tex" 1673816307 9691 3d42d89522f4650c2f3dc616ca2b925e "" + "/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/basiclayer/pgfcorepoints.code.tex" 1601326656 33335 dd1fa4814d4e51f18be97d88bf0da60c "" + "/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/basiclayer/pgfcorequick.code.tex" 1601326656 2965 4c2b1f4e0826925746439038172e5d6f "" + "/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/basiclayer/pgfcorerdf.code.tex" 1601326656 5196 2cc249e0ee7e03da5f5f6589257b1e5b "" + "/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/basiclayer/pgfcorescopes.code.tex" 1673816307 20821 7579108c1e9363e61a0b1584778804aa "" + "/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/basiclayer/pgfcoreshade.code.tex" 1601326656 35249 abd4adf948f960299a4b3d27c5dddf46 "" + "/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/basiclayer/pgfcoretransformations.code.tex" 1673816307 22012 81b34a0aa8fa1a6158cc6220b00e4f10 "" + "/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/basiclayer/pgfcoretransparency.code.tex" 1601326656 8893 e851de2175338fdf7c17f3e091d94618 "" + "/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/graphs/tikzlibrarygraphs.code.tex" 1673816307 86723 0209bbf0dbb55cd8213ecb06ebea3349 "" + "/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibraryarrows.code.tex" 1601326656 319 225dfe354ba678ff3c194968db39d447 "" + "/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibrarybackgrounds.code.tex" 1601326656 4572 4a19637ef65ce88ad2f2d5064b69541d "" + "/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibrarycalc.code.tex" 1601326656 15929 463535aa2c4268fead6674a75c0e8266 "" + "/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibrarychains.code.tex" 1673816307 6816 d02c83dff7646998a96988d92df7f6f4 "" + "/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibrarydecorations.code.tex" 1673816307 5628 dc0ee4ba7f3e40acae5600067ce833de "" + "/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibrarydecorations.markings.code.tex" 1601326656 788 fb28645a91ec7448ebe79bee60965a88 "" + "/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibraryfadings.code.tex" 1601326656 1179 5483d86c1582c569e665c74efab6281f "" + "/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibrarypatterns.code.tex" 1601326656 770 82e332cc9cc48e06b8070d74393a185a "" + "/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibrarypositioning.code.tex" 1601326656 3937 3f208572dd82c71103831da976d74f1a "" + "/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibraryshadows.code.tex" 1601326656 2889 d698e3a959304efa342d47e3bb86da5b "" + "/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibraryshapes.arrows.code.tex" 1601326656 410 048d1174dabde96757a5387b8f23d968 "" + "/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibraryshapes.callouts.code.tex" 1601326656 1201 8bd51e254d3ecf0cd2f21edd9ab6f1bb "" + "/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibraryshapes.code.tex" 1601326656 494 8de62576191924285b021f4fc4292e16 "" + "/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibraryshapes.geometric.code.tex" 1601326656 339 be0fe46d92a80e3385dd6a83511a46f2 "" + "/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibraryshapes.misc.code.tex" 1601326656 329 ba6d5440f8c16779c2384e0614158266 "" + "/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibraryshapes.multipart.code.tex" 1673816307 923 c7a223b32ffdeb1c839d97935eee61ff "" + "/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibraryshapes.symbols.code.tex" 1601326656 475 4b4056fe07caa0603fede9a162fe666d "" + "/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibrarytopaths.code.tex" 1608933718 11518 738408f795261b70ce8dd47459171309 "" + "/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/frontendlayer/tikz/tikz.code.tex" 1673816307 186782 af500404a9edec4d362912fe762ded92 "" + "/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/libraries/decorations/pgflibrarydecorations.markings.code.tex" 1601326656 5220 c70346acb7ff99702098460fd6c18993 "" + "/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/libraries/pgflibraryarrows.code.tex" 1601326656 31874 89148c383c49d4c72114a76fd0062299 "" + "/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/libraries/pgflibraryarrows.meta.code.tex" 1601326656 58801 1e750fb0692eb99aaac45698bbec96b1 "" + "/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/libraries/pgflibraryfadings.code.tex" 1601326656 2563 d5b174eb7709fd6bdcc2f70953dbdf8e "" + "/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/libraries/pgflibrarypatterns.code.tex" 1601326656 7936 49e55444d57eb69a380c6baa35094828 "" + "/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/libraries/pgflibraryplothandlers.code.tex" 1601326656 32995 ac577023e12c0e4bd8aa420b2e852d1a "" + "/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/libraries/shapes/pgflibraryshapes.arrows.code.tex" 1673816307 91587 d9b31a3e308b08833e4528a7b4484b4a "" + "/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/libraries/shapes/pgflibraryshapes.callouts.code.tex" 1601326656 33336 427c354e28a4802ffd781da22ae9f383 "" + "/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/libraries/shapes/pgflibraryshapes.geometric.code.tex" 1673816307 161011 76ab54df0aa1a9d3b27a94864771d38d "" + "/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/libraries/shapes/pgflibraryshapes.misc.code.tex" 1673816307 46249 d1f322c52d26cf506b4988f31902cd5d "" + "/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/libraries/shapes/pgflibraryshapes.multipart.code.tex" 1601326656 62281 aff261ef10ba6cbe8e3c872a38c05a61 "" + "/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/libraries/shapes/pgflibraryshapes.symbols.code.tex" 1673816307 90521 9d46d4504c2ffed28ff5ef3c43d15f21 "" + "/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/math/pgfint.code.tex" 1557692582 3063 8c415c68a0f3394e45cfeca0b65f6ee6 "" + "/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/math/pgfmath.code.tex" 1673816307 949 cea70942e7b7eddabfb3186befada2e6 "" + "/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/math/pgfmathcalc.code.tex" 1673816307 13270 2e54f2ce7622437bf37e013d399743e3 "" + "/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/math/pgfmathfloat.code.tex" 1673816307 104717 9b2393fbf004a0ce7fa688dbce423848 "" + "/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/math/pgfmathfunctions.base.code.tex" 1601326656 10165 cec5fa73d49da442e56efc2d605ef154 "" + "/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/math/pgfmathfunctions.basic.code.tex" 1601326656 28178 41c17713108e0795aac6fef3d275fbca "" + "/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/math/pgfmathfunctions.code.tex" 1673816307 9649 85779d3d8d573bfd2cd4137ba8202e60 "" + "/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/math/pgfmathfunctions.comparison.code.tex" 1601326656 3865 ac538ab80c5cf82b345016e474786549 "" + "/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/math/pgfmathfunctions.integerarithmetics.code.tex" 1557692582 3177 27d85c44fbfe09ff3b2cf2879e3ea434 "" + "/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/math/pgfmathfunctions.misc.code.tex" 1621110968 11024 0179538121bc2dba172013a3ef89519f "" + "/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/math/pgfmathfunctions.random.code.tex" 1673816307 7890 0a86dbf4edfd88d022e0d889ec78cc03 "" + "/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/math/pgfmathfunctions.round.code.tex" 1601326656 3379 781797a101f647bab82741a99944a229 "" + "/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/math/pgfmathfunctions.trigonometric.code.tex" 1601326656 92405 f515f31275db273f97b9d8f52e1b0736 "" + "/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/math/pgfmathparser.code.tex" 1673816307 37466 97b0a1ba732e306a1a2034f5a73e239f "" + "/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/math/pgfmathutil.code.tex" 1601326656 8471 c2883569d03f69e8e1cabfef4999cfd7 "" + "/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/modules/pgfmoduledecorations.code.tex" 1673816307 71742 3da44a8be6626eef1c400c68776c7a0f "" + "/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/modules/pgfmodulematrix.code.tex" 1673816307 21211 1e73ec76bd73964d84197cc3d2685b01 "" + "/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/modules/pgfmoduleplot.code.tex" 1601326656 16121 346f9013d34804439f7436ff6786cef7 "" + "/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/modules/pgfmoduleshapes.code.tex" 1673816307 44792 271e2e1934f34c759f4dedb1e14a5015 "" + "/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/pgf.revision.tex" 1673816307 114 e6d443369d0673933b38834bf99e422d "" + "/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/systemlayer/pgf.cfg" 1601326656 926 2963ea0dcf6cc6c0a770b69ec46a477b "" + "/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/systemlayer/pgfsys-common-pdf.def" 1673816307 5542 32f75a31ea6c3a7e1148cd6d5e93dbb7 "" + "/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/systemlayer/pgfsys-pdftex.def" 1673816307 12612 7774ba67bfd72e593c4436c2de6201e3 "" + "/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/systemlayer/pgfsys.code.tex" 1673816307 61351 bc5f86e0355834391e736e97a61abced "" + "/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/systemlayer/pgfsysprotocol.code.tex" 1601326656 1896 b8e0ca0ac371d74c0ca05583f6313c91 "" + "/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/systemlayer/pgfsyssoftpath.code.tex" 1601326656 7778 53c8b5623d80238f6a20aa1df1868e63 "" + "/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/utilities/pgfcalendar.code.tex" 1673816307 24149 056c3eb5ebac53bc396649bc52434c12 "" + "/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/utilities/pgffor.code.tex" 1673816307 24033 d8893a1ec4d1bfa101b172754743d340 "" + "/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/utilities/pgfkeys.code.tex" 1673816307 39784 414c54e866ebab4b801e2ad81d9b21d8 "" + "/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/utilities/pgfkeyslibraryfiltered.code.tex" 1673816307 37433 940bc6d409f1ffd298adfdcaf125dd86 "" + "/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/utilities/pgfrcs.code.tex" 1673816307 4385 510565c2f07998c8a0e14f0ec07ff23c "" + "/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/utilities/pgfutil-common.tex" 1673816307 29239 22e8c7516012992a49873eff0d868fed "" + "/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/utilities/pgfutil-latex.def" 1673816307 6950 8524a062d82b7afdc4a88a57cb377784 "" + "/usr/local/texlive/2025/texmf-dist/tex/generic/xkeyval/xkeyval.tex" 1655411236 19231 27205ee17aaa2902aea3e0c07a3cfc65 "" + "/usr/local/texlive/2025/texmf-dist/tex/generic/xkeyval/xkvutils.tex" 1655411236 7677 9cb1a74d945bc9331f2181c0a59ff34a "" + "/usr/local/texlive/2025/texmf-dist/tex/latex/adjustbox/adjcalc.sty" 1666037967 5598 c49b91713cbe5e50a1fabefb733eda0d "" + "/usr/local/texlive/2025/texmf-dist/tex/latex/adjustbox/adjustbox.sty" 1740604409 56907 b74d2bd6fed8dc761953edb2fbea781b "" + "/usr/local/texlive/2025/texmf-dist/tex/latex/adjustbox/tc-pdftex.def" 1740604409 4304 461724faa0dfbdec2d80de16c11f407c "" + "/usr/local/texlive/2025/texmf-dist/tex/latex/adjustbox/trimclip.sty" 1740176375 7245 2bf1779563af51e666da8f26ea1f8455 "" + "/usr/local/texlive/2025/texmf-dist/tex/latex/amsfonts/amsfonts.sty" 1359763108 5949 3f3fd50a8cc94c3d4cbf4fc66cd3df1c "" + "/usr/local/texlive/2025/texmf-dist/tex/latex/amsfonts/amssymb.sty" 1359763108 13829 94730e64147574077f8ecfea9bb69af4 "" + "/usr/local/texlive/2025/texmf-dist/tex/latex/amsmath/amsbsy.sty" 1717359999 2222 2166a1f7827be30ddc30434e5efcee1b "" + "/usr/local/texlive/2025/texmf-dist/tex/latex/amsmath/amsgen.sty" 1717359999 4173 d22509bc0c91281d991b2de7c88720dd "" + "/usr/local/texlive/2025/texmf-dist/tex/latex/amsmath/amsmath.sty" 1730928152 88370 c780f23aea0ece6add91e09b44dca2cd "" + "/usr/local/texlive/2025/texmf-dist/tex/latex/amsmath/amsopn.sty" 1717359999 4474 23ca1d3a79a57b405388059456d0a8df "" + "/usr/local/texlive/2025/texmf-dist/tex/latex/amsmath/amstext.sty" 1717359999 2444 71618ea5f2377e33b04fb97afdd0eac2 "" + "/usr/local/texlive/2025/texmf-dist/tex/latex/base/article.cls" 1738182759 20144 63d8bacaf52e5abf4db3bc322373e1d4 "" + "/usr/local/texlive/2025/texmf-dist/tex/latex/base/ifthen.sty" 1738182759 5525 9dced5929f36b19fa837947f5175b331 "" + "/usr/local/texlive/2025/texmf-dist/tex/latex/base/inputenc.sty" 1738182759 5048 0270515b828149155424600fd2d58ac5 "" + "/usr/local/texlive/2025/texmf-dist/tex/latex/base/size12.clo" 1738182759 8449 ffe4ba2166a344827c3a832d1d5e0a91 "" + "/usr/local/texlive/2025/texmf-dist/tex/latex/booktabs/booktabs.sty" 1579038678 6078 f1cb470c9199e7110a27851508ed7a5c "" + "/usr/local/texlive/2025/texmf-dist/tex/latex/cite/cite.sty" 1425427964 26218 19edeff8cdc2bcb704e8051dc55eb5a7 "" + "/usr/local/texlive/2025/texmf-dist/tex/latex/collectbox/collectbox.sty" 1666037909 9124 59c3b56f1a073de66e3eea35f9c173c8 "" + "/usr/local/texlive/2025/texmf-dist/tex/latex/colortbl/colortbl.sty" 1720383029 12726 67708fc852a887b2ba598148f60c3756 "" + "/usr/local/texlive/2025/texmf-dist/tex/latex/currfile/currfile.sty" 1710537833 11079 d0660dd7678e4c3c56d9890bce94a3e5 "" + "/usr/local/texlive/2025/texmf-dist/tex/latex/datetime/datetime-defaults.sty" 1427500626 4105 4c80eaed8cd4f9a80cc6244c0adeb81f "" + "/usr/local/texlive/2025/texmf-dist/tex/latex/datetime/datetime.sty" 1427500626 27587 b023ffe1328fa89e7f133201d87029de "" + "/usr/local/texlive/2025/texmf-dist/tex/latex/enumitem/enumitem.sty" 1738874546 52272 63d293bc0d496619edb57585740861a2 "" + "/usr/local/texlive/2025/texmf-dist/tex/latex/epstopdf-pkg/epstopdf-base.sty" 1579991033 13886 d1306dcf79a944f6988e688c1785f9ce "" + "/usr/local/texlive/2025/texmf-dist/tex/latex/eso-pic/eso-pic.sty" 1683144721 11876 6ef493863ae0d7a984706973240c2237 "" + "/usr/local/texlive/2025/texmf-dist/tex/latex/etoolbox/etoolbox.sty" 1739306980 46850 d87daedc2abdc653769a6f1067849fe0 "" + "/usr/local/texlive/2025/texmf-dist/tex/latex/filehook/filehook-2020.sty" 1666814490 9005 c47d9138e4a690658bcefab0dd0af8d7 "" + "/usr/local/texlive/2025/texmf-dist/tex/latex/filehook/filehook.sty" 1666814490 1210 95c2d0abf75beadf7e7547b73b345c24 "" + "/usr/local/texlive/2025/texmf-dist/tex/latex/filemod/filemod-expmin.sty" 1316560476 2845 2b7393c472a738889b77cb266b9ef35d "" + "/usr/local/texlive/2025/texmf-dist/tex/latex/fmtcount/fc-english.def" 1739135561 13002 b14af1bcf50fb2c1b95ba5f32e7fc962 "" + "/usr/local/texlive/2025/texmf-dist/tex/latex/fmtcount/fcnumparser.sty" 1739135561 11038 6f51846fb936ca8566fb2a1c957c6dab "" + "/usr/local/texlive/2025/texmf-dist/tex/latex/fmtcount/fcprefix.sty" 1739135561 10747 3648e4fffb9f130ffceebed92b30d963 "" + "/usr/local/texlive/2025/texmf-dist/tex/latex/fmtcount/fmtcount.sty" 1739135561 29567 3875eaa69e0aae20dbf9ea7da73cb26a "" + "/usr/local/texlive/2025/texmf-dist/tex/latex/geometry/geometry.sty" 1578002852 41601 9cf6c5257b1bc7af01a58859749dd37a "" + "/usr/local/texlive/2025/texmf-dist/tex/latex/gincltex/gincltex.sty" 1315265409 3594 7c105130ddd1211e8275b3c1288d84c8 "" + "/usr/local/texlive/2025/texmf-dist/tex/latex/graphics-cfg/color.cfg" 1459978653 1213 620bba36b25224fa9b7e1ccb4ecb76fd "" + "/usr/local/texlive/2025/texmf-dist/tex/latex/graphics-cfg/graphics.cfg" 1465944070 1224 978390e9c2234eab29404bc21b268d1e "" + "/usr/local/texlive/2025/texmf-dist/tex/latex/graphics-def/pdftex.def" 1713382759 19440 9da9dcbb27470349a580fca7372d454b "" + "/usr/local/texlive/2025/texmf-dist/tex/latex/graphics/color.sty" 1730496337 7245 57f7defed4fb41562dc4b6ca13958ca9 "" + "/usr/local/texlive/2025/texmf-dist/tex/latex/graphics/graphics.sty" 1730496337 18363 dee506cb8d56825d8a4d020f5d5f8704 "" + "/usr/local/texlive/2025/texmf-dist/tex/latex/graphics/graphicx.sty" 1717359999 8010 6f2ad8c2b2ffbd607af6475441c7b5e4 "" + "/usr/local/texlive/2025/texmf-dist/tex/latex/graphics/keyval.sty" 1717359999 2671 70891d50dac933918b827d326687c6e8 "" + "/usr/local/texlive/2025/texmf-dist/tex/latex/graphics/lscape.sty" 1717359999 1822 ce7e39e35ea3027d24b527bd5c5034d5 "" + "/usr/local/texlive/2025/texmf-dist/tex/latex/graphics/mathcolor.ltx" 1667332637 2885 9c645d672ae17285bba324998918efd8 "" + "/usr/local/texlive/2025/texmf-dist/tex/latex/graphics/rotating.sty" 1717359999 7060 c21bdf2a03ef9298ad94a39d4110f07c "" + "/usr/local/texlive/2025/texmf-dist/tex/latex/graphics/trig.sty" 1717359999 4023 2c9f39712cf7b43d3eb93a8bbd5c8f67 "" + "/usr/local/texlive/2025/texmf-dist/tex/latex/ifoddpage/ifoddpage.sty" 1666126449 2142 eae42205b97b7a3ad0e58db5fe99e3e6 "" + "/usr/local/texlive/2025/texmf-dist/tex/latex/jknapltx/mathrsfs.sty" 1137110241 300 12fa6f636b617656f2810ee82cb05015 "" + "/usr/local/texlive/2025/texmf-dist/tex/latex/jknapltx/ursfs.fd" 1137110241 548 cc4e3557704bfed27c7002773fad6c90 "" + "/usr/local/texlive/2025/texmf-dist/tex/latex/kvoptions/kvoptions.sty" 1655478651 22555 6d8e155cfef6d82c3d5c742fea7c992e "" + "/usr/local/texlive/2025/texmf-dist/tex/latex/kvsetkeys/kvsetkeys.sty" 1665067230 13815 760b0c02f691ea230f5359c4e1de23a7 "" + "/usr/local/texlive/2025/texmf-dist/tex/latex/l3backend/l3backend-pdftex.def" 1716410060 29785 9f93ab201fe5dd053afcc6c1bcf7d266 "" + "/usr/local/texlive/2025/texmf-dist/tex/latex/latexconfig/epstopdf-sys.cfg" 1279039959 678 4792914a8f45be57bb98413425e4c7af "" + "/usr/local/texlive/2025/texmf-dist/tex/latex/listings/listings.cfg" 1727126400 1865 301ae3c26fb8c0243307b619a6aa2dd3 "" + "/usr/local/texlive/2025/texmf-dist/tex/latex/listings/listings.sty" 1727126400 81640 997090b6c021dc4af9ee00a97b85c5b4 "" + "/usr/local/texlive/2025/texmf-dist/tex/latex/listings/lstmisc.sty" 1727126400 77051 be68720e5402397a830abb9eed5a2cb4 "" + "/usr/local/texlive/2025/texmf-dist/tex/latex/listings/lstpatch.sty" 1710360531 353 9024412f43e92cd5b21fe9ded82d0610 "" + "/usr/local/texlive/2025/texmf-dist/tex/latex/makecell/makecell.sty" 1249334690 15773 2dd7dde1ec1c2a3d0c85bc3b273e04d8 "" + "/usr/local/texlive/2025/texmf-dist/tex/latex/multirow/multirow.sty" 1731446765 6696 886c9f3087d0b973ed2c19aa79cb3023 "" + "/usr/local/texlive/2025/texmf-dist/tex/latex/pdflscape/pdflscape-nometadata.sty" 1667072951 6572 ea530fbbe537629fd97736d33babc07d "" + "/usr/local/texlive/2025/texmf-dist/tex/latex/pdflscape/pdflscape.sty" 1667072951 2224 1230ab76aa62221ccbd90bca8c8c015e "" + "/usr/local/texlive/2025/texmf-dist/tex/latex/pdfpages/pdfpages.sty" 1738442568 56557 52caee30c1fe86973ee17a572171abb0 "" + "/usr/local/texlive/2025/texmf-dist/tex/latex/pdfpages/pppdftex.def" 1738442568 6446 d89a65b3f6b4b32146b499348640e1cf "" + "/usr/local/texlive/2025/texmf-dist/tex/latex/pgf/basiclayer/pgf.sty" 1601326656 1090 bae35ef70b3168089ef166db3e66f5b2 "" + "/usr/local/texlive/2025/texmf-dist/tex/latex/pgf/basiclayer/pgfcore.sty" 1673816307 373 00b204b1d7d095b892ad31a7494b0373 "" + "/usr/local/texlive/2025/texmf-dist/tex/latex/pgf/compatibility/pgfcomp-version-0-65.sty" 1601326656 21013 f4ff83d25bb56552493b030f27c075ae "" + "/usr/local/texlive/2025/texmf-dist/tex/latex/pgf/compatibility/pgfcomp-version-1-18.sty" 1601326656 989 c49c8ae06d96f8b15869da7428047b1e "" + "/usr/local/texlive/2025/texmf-dist/tex/latex/pgf/frontendlayer/tikz.sty" 1601326656 339 c2e180022e3afdb99c7d0ea5ce469b7d "" + "/usr/local/texlive/2025/texmf-dist/tex/latex/pgf/math/pgfmath.sty" 1601326656 306 c56a323ca5bf9242f54474ced10fca71 "" + "/usr/local/texlive/2025/texmf-dist/tex/latex/pgf/systemlayer/pgfsys.sty" 1601326656 443 8c872229db56122037e86bcda49e14f3 "" + "/usr/local/texlive/2025/texmf-dist/tex/latex/pgf/utilities/pgfcalendar.sty" 1601326656 328 7411531f2e9e5c6aa139c84fbe10702e "" + "/usr/local/texlive/2025/texmf-dist/tex/latex/pgf/utilities/pgffor.sty" 1601326656 348 ee405e64380c11319f0e249fed57e6c5 "" + "/usr/local/texlive/2025/texmf-dist/tex/latex/pgf/utilities/pgfkeys.sty" 1601326656 274 5ae372b7df79135d240456a1c6f2cf9a "" + "/usr/local/texlive/2025/texmf-dist/tex/latex/pgf/utilities/pgfrcs.sty" 1601326656 325 f9f16d12354225b7dd52a3321f085955 "" + "/usr/local/texlive/2025/texmf-dist/tex/latex/pgfgantt/pgfgantt.sty" 1718825887 47792 a7e008294ecd88e823d949404eb72b1c "" + "/usr/local/texlive/2025/texmf-dist/tex/latex/psnfss/mathptmx.sty" 1586716065 4631 6e41de2b7a83dfa5d2c4b0a2fe01f046 "" + "/usr/local/texlive/2025/texmf-dist/tex/latex/psnfss/omlztmcm.fd" 1137110629 411 12564a37a279e4e0b533cdf5e03eeb7c "" + "/usr/local/texlive/2025/texmf-dist/tex/latex/psnfss/omsztmcm.fd" 1137110629 348 f4ce75d394e7d9ac12ca7aac4045ed77 "" + "/usr/local/texlive/2025/texmf-dist/tex/latex/psnfss/omxztmcm.fd" 1137110629 329 c8cddcc90b6f567b28408eb374773c9c "" + "/usr/local/texlive/2025/texmf-dist/tex/latex/psnfss/ot1ptm.fd" 1137110629 961 15056f4a61917ceed3a44e4ac11fcc52 "" + "/usr/local/texlive/2025/texmf-dist/tex/latex/psnfss/ot1ztmcm.fd" 1137110629 329 aee7226812ba4138ac67a018466b488d "" + "/usr/local/texlive/2025/texmf-dist/tex/latex/psnfss/ts1ptm.fd" 1137110629 619 96f56dc5d1ef1fe1121f1cfeec70ee0c "" + "/usr/local/texlive/2025/texmf-dist/tex/latex/setspace/setspace.sty" 1670275497 22490 8cac309b79a4c53a4ffce4b1b07aead0 "" + "/usr/local/texlive/2025/texmf-dist/tex/latex/standalone/standalone.sty" 1740345147 34855 da6c70080898b3166f2c1d8f28ed2602 "" + "/usr/local/texlive/2025/texmf-dist/tex/latex/svn-prov/svn-prov.sty" 1272330018 6852 44ea8d7e58290cde708a34ebf3953571 "" + "/usr/local/texlive/2025/texmf-dist/tex/latex/titlesec/titlesec.sty" 1736023606 48766 87a17a4ef312a39cd43896e34a679a56 "" + "/usr/local/texlive/2025/texmf-dist/tex/latex/tocbibind/tocbibind.sty" 1287012853 8927 46f54e33fc9cef24f78ab3bc811cb63f "" + "/usr/local/texlive/2025/texmf-dist/tex/latex/tools/array.sty" 1730496337 14552 27664839421e418b87f56fa4c6f66b1a "" + "/usr/local/texlive/2025/texmf-dist/tex/latex/tools/calc.sty" 1717359999 10214 61188260d324e94bc2f66825d7d3fdf4 "" + "/usr/local/texlive/2025/texmf-dist/tex/latex/tools/dcolumn.sty" 1717359999 2758 86fa9d68b26327d0f1d7a6c34674f4f8 "" + "/usr/local/texlive/2025/texmf-dist/tex/latex/tools/shellesc.sty" 1717359999 4121 6039ae6d0916154d7ba5f20a77b9ab2c "" + "/usr/local/texlive/2025/texmf-dist/tex/latex/tools/tabularx.sty" 1717359999 7243 e5dac1240636811edb77568b81818372 "" + "/usr/local/texlive/2025/texmf-dist/tex/latex/url/url.sty" 1388531844 12796 8edb7d69a20b857904dd0ea757c14ec9 "" + "/usr/local/texlive/2025/texmf-dist/tex/latex/varwidth/varwidth.sty" 1238697683 10894 d359a13923460b2a73d4312d613554c8 "" + "/usr/local/texlive/2025/texmf-dist/tex/latex/xcolor/xcolor.sty" 1727642399 55384 b454dec21c2d9f45ec0b793f0995b992 "" + "/usr/local/texlive/2025/texmf-dist/tex/latex/xkeyval/xkeyval.sty" 1655411236 4937 4ce600ce9bd4ec84d0250eb6892fcf4f "" + "/usr/local/texlive/2025/texmf-dist/web2c/texmf.cnf" 1739380943 42148 61becc7c670cd061bb319c643c27fdd4 "" + "/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/research_statement_v1.tex" 1765591319.18896 4450 070caee751214eaddffa6b3403f8ed43 "" + "1-goals-and-outcomes/v1.tex" 1765591319.1893 5825 07f6fba24cfa050a3b2b00c416f0f45f "" + "2-state-of-the-art/v1.tex" 1765591319.1898 10609 44863eb08e23052a1623ef3ebcb1e3ae "" + "3-research-approach/v2.tex" 1770062336.52686 22203 b3b90c4fbb94cd85cdcce085ec1b2a8a "" + "4-metrics-of-success/v1.tex" 1765591319.19036 5586 e5fb80ced00bcdc318ffe3861b0064bc "" + "5-risks-and-contingencies/v1.tex" 1765591319.19058 10412 17e755aa8451c45198372af7afe3c500 "" + "6-broader-impacts/v1.tex" 1765591319.19072 4834 418aae223b778759691eaf9124a5360c "" + "8-schedule/v1.tex" 1765591319.19095 4473 8ad96bbf9cedf2ea09298ecbd4e01b83 "" + "dane_proposal_format.cls" 1769715785.9835 2883 ea175794171aa0291ef71716b2190bf0 "" + "main.aux" 1770062339.59974 3798 3e4f846d5a63c369ad994a87de4a30be "pdflatex" + "main.bbl" 1769715964.93568 2919 0ea026a17b15c1ad2ed657bdbf26dfdc "bibtex main" + "main.tex" 1769453692.01808 954 ea089365572626745e262fed177e4fa3 "" + "main.toc" 1770062339.60048 1565 b9f0d6ea3d8646810f16fc895e4d44da "pdflatex" + (generated) + "main.aux" + "main.log" + "main.pdf" + "main.toc" + (rewritten before read) diff --git a/main.fls b/main.fls new file mode 100644 index 0000000..248e23f --- /dev/null +++ b/main.fls @@ -0,0 +1,564 @@ +PWD /Users/danesabo/Documents/Dane's Vault/Writing/THESIS_PROPOSAL +INPUT /usr/local/texlive/2025/texmf.cnf +INPUT /usr/local/texlive/2025/texmf-dist/web2c/texmf.cnf +INPUT /usr/local/texlive/2025/texmf-var/web2c/pdftex/pdflatex.fmt +INPUT main.tex +OUTPUT main.log +INPUT ./dane_proposal_format.cls +INPUT dane_proposal_format.cls +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/base/article.cls +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/base/article.cls +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/base/size12.clo +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/base/size12.clo +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/base/size12.clo +INPUT /usr/local/texlive/2025/texmf-dist/fonts/map/fontname/texfonts.map +INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/public/cm/cmr12.tfm +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/base/inputenc.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/base/inputenc.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/geometry/geometry.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/geometry/geometry.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/graphics/keyval.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/graphics/keyval.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/iftex/ifvtex.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/iftex/ifvtex.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/iftex/iftex.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/iftex/iftex.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/url/url.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/url/url.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/psnfss/mathptmx.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/psnfss/mathptmx.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/titlesec/titlesec.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/titlesec/titlesec.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/setspace/setspace.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/setspace/setspace.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/datetime/datetime.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/datetime/datetime.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/etoolbox/etoolbox.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/etoolbox/etoolbox.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/fmtcount/fmtcount.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/fmtcount/fmtcount.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/base/ifthen.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/base/ifthen.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/xkeyval/xkeyval.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/xkeyval/xkeyval.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/xkeyval/xkeyval.tex +INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/xkeyval/xkvutils.tex +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/fmtcount/fcprefix.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/fmtcount/fcprefix.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/fmtcount/fcnumparser.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/fmtcount/fcnumparser.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/amsmath/amsgen.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/amsmath/amsgen.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/datetime/datetime-defaults.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/datetime/datetime-defaults.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/cite/cite.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/cite/cite.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/tocbibind/tocbibind.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/tocbibind/tocbibind.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/graphics/graphicx.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/graphics/graphicx.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/graphics/graphics.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/graphics/graphics.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/graphics/trig.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/graphics/trig.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/graphics-cfg/graphics.cfg +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/graphics-cfg/graphics.cfg +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/graphics-cfg/graphics.cfg +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/graphics-def/pdftex.def +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/graphics-def/pdftex.def +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/graphics-def/pdftex.def +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/pdfpages/pdfpages.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/pdfpages/pdfpages.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/tools/calc.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/tools/calc.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/eso-pic/eso-pic.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/eso-pic/eso-pic.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/xcolor/xcolor.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/xcolor/xcolor.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/xcolor/xcolor.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/graphics-cfg/color.cfg +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/graphics-cfg/color.cfg +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/graphics-cfg/color.cfg +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/graphics/mathcolor.ltx +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/graphics/mathcolor.ltx +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/graphics/mathcolor.ltx +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/pdfpages/pppdftex.def +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/pdfpages/pppdftex.def +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/pdfpages/pppdftex.def +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/graphics/rotating.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/graphics/rotating.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/pgf/frontendlayer/tikz.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/pgf/frontendlayer/tikz.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/pgf/basiclayer/pgf.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/pgf/basiclayer/pgf.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/pgf/utilities/pgfrcs.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/pgf/utilities/pgfrcs.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/utilities/pgfutil-common.tex +INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/utilities/pgfutil-latex.def +INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/utilities/pgfrcs.code.tex +INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/utilities/pgfrcs.code.tex +INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/utilities/pgfrcs.code.tex +INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/pgf.revision.tex +INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/pgf.revision.tex +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/pgf/basiclayer/pgfcore.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/pgf/basiclayer/pgfcore.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/pgf/systemlayer/pgfsys.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/pgf/systemlayer/pgfsys.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/systemlayer/pgfsys.code.tex +INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/systemlayer/pgfsys.code.tex +INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/systemlayer/pgfsys.code.tex +INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/utilities/pgfkeys.code.tex +INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/utilities/pgfkeyslibraryfiltered.code.tex +INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/systemlayer/pgf.cfg +INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/systemlayer/pgfsys-pdftex.def +INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/systemlayer/pgfsys-pdftex.def +INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/systemlayer/pgfsys-common-pdf.def +INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/systemlayer/pgfsyssoftpath.code.tex +INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/systemlayer/pgfsyssoftpath.code.tex +INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/systemlayer/pgfsyssoftpath.code.tex +INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/systemlayer/pgfsysprotocol.code.tex +INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/systemlayer/pgfsysprotocol.code.tex +INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/systemlayer/pgfsysprotocol.code.tex +INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/basiclayer/pgfcore.code.tex +INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/basiclayer/pgfcore.code.tex +INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/basiclayer/pgfcore.code.tex +INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/math/pgfmath.code.tex +INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/math/pgfmathutil.code.tex +INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/math/pgfmathparser.code.tex +INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/math/pgfmathfunctions.code.tex +INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/math/pgfmathfunctions.basic.code.tex +INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/math/pgfmathfunctions.trigonometric.code.tex +INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/math/pgfmathfunctions.random.code.tex +INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/math/pgfmathfunctions.comparison.code.tex +INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/math/pgfmathfunctions.base.code.tex +INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/math/pgfmathfunctions.round.code.tex +INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/math/pgfmathfunctions.misc.code.tex +INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/math/pgfmathfunctions.integerarithmetics.code.tex +INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/math/pgfmathcalc.code.tex +INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/math/pgfmathfloat.code.tex +INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/math/pgfint.code.tex +INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/basiclayer/pgfcorepoints.code.tex +INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/basiclayer/pgfcorepathconstruct.code.tex +INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/basiclayer/pgfcorepathusage.code.tex +INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/basiclayer/pgfcorescopes.code.tex +INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/basiclayer/pgfcoregraphicstate.code.tex +INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/basiclayer/pgfcoretransformations.code.tex +INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/basiclayer/pgfcorequick.code.tex +INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/basiclayer/pgfcoreobjects.code.tex +INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/basiclayer/pgfcorepathprocessing.code.tex +INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/basiclayer/pgfcorearrows.code.tex +INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/basiclayer/pgfcoreshade.code.tex +INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/basiclayer/pgfcoreimage.code.tex +INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/basiclayer/pgfcoreexternal.code.tex +INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/basiclayer/pgfcorelayers.code.tex +INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/basiclayer/pgfcoretransparency.code.tex +INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/basiclayer/pgfcorepatterns.code.tex +INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/basiclayer/pgfcorerdf.code.tex +INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/modules/pgfmoduleshapes.code.tex +INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/modules/pgfmoduleplot.code.tex +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/pgf/compatibility/pgfcomp-version-0-65.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/pgf/compatibility/pgfcomp-version-0-65.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/pgf/compatibility/pgfcomp-version-1-18.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/pgf/compatibility/pgfcomp-version-1-18.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/pgf/utilities/pgffor.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/pgf/utilities/pgffor.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/pgf/utilities/pgfkeys.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/pgf/utilities/pgfkeys.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/utilities/pgfkeys.code.tex +INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/utilities/pgfkeys.code.tex +INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/utilities/pgfkeys.code.tex +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/pgf/math/pgfmath.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/pgf/math/pgfmath.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/math/pgfmath.code.tex +INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/math/pgfmath.code.tex +INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/math/pgfmath.code.tex +INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/utilities/pgffor.code.tex +INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/utilities/pgffor.code.tex +INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/utilities/pgffor.code.tex +INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/frontendlayer/tikz/tikz.code.tex +INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/frontendlayer/tikz/tikz.code.tex +INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/frontendlayer/tikz/tikz.code.tex +INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/libraries/pgflibraryplothandlers.code.tex +INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/libraries/pgflibraryplothandlers.code.tex +INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/modules/pgfmodulematrix.code.tex +INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibrarytopaths.code.tex +INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibrarytopaths.code.tex +INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibrarypositioning.code.tex +INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibrarypositioning.code.tex +INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibraryshapes.code.tex +INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibraryshapes.code.tex +INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibraryshapes.geometric.code.tex +INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibraryshapes.geometric.code.tex +INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/libraries/shapes/pgflibraryshapes.geometric.code.tex +INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/libraries/shapes/pgflibraryshapes.geometric.code.tex +INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibraryshapes.misc.code.tex +INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibraryshapes.misc.code.tex +INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/libraries/shapes/pgflibraryshapes.misc.code.tex +INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/libraries/shapes/pgflibraryshapes.misc.code.tex +INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibraryshapes.symbols.code.tex +INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibraryshapes.symbols.code.tex +INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/libraries/shapes/pgflibraryshapes.symbols.code.tex +INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/libraries/shapes/pgflibraryshapes.symbols.code.tex +INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibraryshapes.arrows.code.tex +INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibraryshapes.arrows.code.tex +INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/libraries/shapes/pgflibraryshapes.arrows.code.tex +INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/libraries/shapes/pgflibraryshapes.arrows.code.tex +INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibraryshapes.callouts.code.tex +INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibraryshapes.callouts.code.tex +INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/libraries/shapes/pgflibraryshapes.callouts.code.tex +INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/libraries/shapes/pgflibraryshapes.callouts.code.tex +INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibraryshapes.multipart.code.tex +INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibraryshapes.multipart.code.tex +INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/libraries/shapes/pgflibraryshapes.multipart.code.tex +INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/libraries/shapes/pgflibraryshapes.multipart.code.tex +INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibraryarrows.code.tex +INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibraryarrows.code.tex +INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/libraries/pgflibraryarrows.code.tex +INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/libraries/pgflibraryarrows.code.tex +INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/graphs/tikzlibrarygraphs.code.tex +INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/graphs/tikzlibrarygraphs.code.tex +INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibrarycalc.code.tex +INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibrarycalc.code.tex +INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibrarychains.code.tex +INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibrarychains.code.tex +INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibrarydecorations.markings.code.tex +INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibrarydecorations.markings.code.tex +INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibrarydecorations.code.tex +INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibrarydecorations.code.tex +INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/modules/pgfmoduledecorations.code.tex +INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/libraries/decorations/pgflibrarydecorations.markings.code.tex +INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/libraries/decorations/pgflibrarydecorations.markings.code.tex +INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibraryshadows.code.tex +INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibraryshadows.code.tex +INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibraryfadings.code.tex +INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibraryfadings.code.tex +INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/libraries/pgflibraryfadings.code.tex +INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/libraries/pgflibraryfadings.code.tex +OUTPUT main.pdf +INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/libraries/pgflibraryarrows.meta.code.tex +INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/libraries/pgflibraryarrows.meta.code.tex +INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/libraries/pgflibraryarrows.meta.code.tex +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/standalone/standalone.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/standalone/standalone.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/tools/shellesc.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/tools/shellesc.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/tools/shellesc.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/currfile/currfile.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/currfile/currfile.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/kvoptions/kvoptions.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/kvoptions/kvoptions.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/ltxcmds/ltxcmds.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/ltxcmds/ltxcmds.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/kvsetkeys/kvsetkeys.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/kvsetkeys/kvsetkeys.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/filehook/filehook.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/filehook/filehook.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/filehook/filehook-2020.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/filehook/filehook-2020.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/gincltex/gincltex.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/gincltex/gincltex.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/gincltex/gincltex.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/svn-prov/svn-prov.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/svn-prov/svn-prov.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/adjustbox/adjustbox.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/adjustbox/adjustbox.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/adjustbox/adjcalc.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/adjustbox/adjcalc.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/adjustbox/trimclip.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/adjustbox/trimclip.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/collectbox/collectbox.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/collectbox/collectbox.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/adjustbox/tc-pdftex.def +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/adjustbox/tc-pdftex.def +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/adjustbox/tc-pdftex.def +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/ifoddpage/ifoddpage.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/ifoddpage/ifoddpage.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/ifoddpage/ifoddpage.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/varwidth/varwidth.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/varwidth/varwidth.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/varwidth/varwidth.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/filemod/filemod-expmin.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/filemod/filemod-expmin.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/booktabs/booktabs.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/booktabs/booktabs.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/tools/tabularx.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/tools/tabularx.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/tools/array.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/tools/array.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/makecell/makecell.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/makecell/makecell.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/tools/dcolumn.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/tools/dcolumn.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/multirow/multirow.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/multirow/multirow.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/graphics/lscape.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/graphics/lscape.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/amsmath/amsmath.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/amsmath/amsmath.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/amsmath/amsopn.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/amsmath/amstext.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/amsmath/amstext.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/amsmath/amsbsy.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/amsmath/amsbsy.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/amsmath/amsopn.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/amsfonts/amssymb.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/amsfonts/amssymb.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/amsfonts/amsfonts.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/amsfonts/amsfonts.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/jknapltx/mathrsfs.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/jknapltx/mathrsfs.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/enumitem/enumitem.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/enumitem/enumitem.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/listings/listings.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/listings/listings.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/listings/lstpatch.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/listings/lstpatch.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/listings/lstpatch.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/listings/lstmisc.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/listings/lstmisc.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/listings/lstmisc.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/listings/listings.cfg +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/listings/listings.cfg +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/listings/listings.cfg +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/pgfgantt/pgfgantt.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/pgfgantt/pgfgantt.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibrarybackgrounds.code.tex +INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibrarybackgrounds.code.tex +INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibrarypatterns.code.tex +INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibrarypatterns.code.tex +INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/libraries/pgflibrarypatterns.code.tex +INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/libraries/pgflibrarypatterns.code.tex +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/pgf/utilities/pgfcalendar.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/pgf/utilities/pgfcalendar.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/utilities/pgfcalendar.code.tex +INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/utilities/pgfcalendar.code.tex +INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/utilities/pgfcalendar.code.tex +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 /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 +INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/ptmr7t.tfm +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/l3backend/l3backend-pdftex.def +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/l3backend/l3backend-pdftex.def +INPUT ./main.aux +INPUT ./main.aux +INPUT main.aux +OUTPUT main.aux +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/fmtcount/fc-english.def +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/fmtcount/fc-english.def +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/fmtcount/fc-english.def +INPUT /usr/local/texlive/2025/texmf-dist/tex/context/base/mkii/supp-pdf.mkii +INPUT /usr/local/texlive/2025/texmf-dist/tex/context/base/mkii/supp-pdf.mkii +INPUT /usr/local/texlive/2025/texmf-dist/tex/context/base/mkii/supp-pdf.mkii +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/epstopdf-pkg/epstopdf-base.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/epstopdf-pkg/epstopdf-base.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/latexconfig/epstopdf-sys.cfg +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/latexconfig/epstopdf-sys.cfg +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/latexconfig/epstopdf-sys.cfg +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/pdflscape/pdflscape.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/pdflscape/pdflscape.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/pdflscape/pdflscape-nometadata.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/pdflscape/pdflscape-nometadata.sty +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/tex/latex/psnfss/ot1ztmcm.fd +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/psnfss/ot1ztmcm.fd +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/psnfss/ot1ztmcm.fd +INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/zptmcm7t.tfm +INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/zptmcm7t.tfm +INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/zptmcm7t.tfm +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/psnfss/omlztmcm.fd +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/psnfss/omlztmcm.fd +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/psnfss/omlztmcm.fd +INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/zptmcm7m.tfm +INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/zptmcm7m.tfm +INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/zptmcm7m.tfm +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/psnfss/omsztmcm.fd +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/psnfss/omsztmcm.fd +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/psnfss/omsztmcm.fd +INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/zptmcm7y.tfm +INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/zptmcm7y.tfm +INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/zptmcm7y.tfm +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/psnfss/omxztmcm.fd +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/psnfss/omxztmcm.fd +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/psnfss/omxztmcm.fd +INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/zptmcm7v.tfm +INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/zptmcm7v.tfm +INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/zptmcm7v.tfm +INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/ptmb7t.tfm +INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/ptmb7t.tfm +INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/ptmb7t.tfm +INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/ptmri7t.tfm +INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/ptmri7t.tfm +INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/ptmri7t.tfm +INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/public/amsfonts/symbols/msam10.tfm +INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/public/amsfonts/symbols/msam10.tfm +INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/public/amsfonts/symbols/msam10.tfm +INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/public/amsfonts/symbols/msbm10.tfm +INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/public/amsfonts/symbols/msbm10.tfm +INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/public/amsfonts/symbols/msbm10.tfm +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/jknapltx/ursfs.fd +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/jknapltx/ursfs.fd +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/jknapltx/ursfs.fd +INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/public/rsfs/rsfs10.tfm +INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/public/rsfs/rsfs10.tfm +INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/public/rsfs/rsfs10.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/ptmr7t.vf +INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/ptmr8r.tfm +INPUT /usr/local/texlive/2025/texmf-var/fonts/map/pdftex/updmap/pdftex.map +INPUT /usr/local/texlive/2025/texmf-dist/fonts/enc/dvips/base/8r.enc +INPUT /usr/local/texlive/2025/texmf-dist/fonts/vf/adobe/times/ptmr7t.vf +INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/ptmr8r.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/ptmr8r.tfm +INPUT ./1-goals-and-outcomes/research_statement_v1.tex +INPUT ./1-goals-and-outcomes/research_statement_v1.tex +INPUT 1-goals-and-outcomes/research_statement_v1.tex +INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/ptmri7t.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/ptmr8r.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 /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/ptmb7t.tfm +INPUT ./main.toc +INPUT ./main.toc +INPUT main.toc +INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/zptmcm7t.tfm +INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/zptmcm7t.tfm +INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/zptmcm7t.tfm +INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/zptmcm7m.tfm +INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/zptmcm7m.tfm +INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/zptmcm7m.tfm +INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/zptmcm7y.tfm +INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/zptmcm7y.tfm +INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/zptmcm7y.tfm +INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/zptmcm7v.tfm +INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/zptmcm7v.tfm +INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/zptmcm7v.tfm +INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/ptmb7t.tfm +INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/ptmb7t.tfm +INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/ptmri7t.tfm +INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/ptmri7t.tfm +INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/public/amsfonts/symbols/msam10.tfm +INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/public/amsfonts/symbols/msam10.tfm +INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/public/amsfonts/symbols/msam10.tfm +INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/public/amsfonts/symbols/msbm10.tfm +INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/public/amsfonts/symbols/msbm10.tfm +INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/public/amsfonts/symbols/msbm10.tfm +INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/public/rsfs/rsfs10.tfm +INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/public/rsfs/rsfs10.tfm +INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/public/rsfs/rsfs7.tfm +OUTPUT main.toc +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/vf/adobe/times/ptmb7t.vf +INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/ptmb8r.tfm +INPUT ./1-goals-and-outcomes/v1.tex +INPUT ./1-goals-and-outcomes/v1.tex +INPUT ./1-goals-and-outcomes/v1.tex +INPUT ./1-goals-and-outcomes/v1.tex +INPUT 1-goals-and-outcomes/v1.tex +INPUT ./2-state-of-the-art/v1.tex +INPUT ./2-state-of-the-art/v1.tex +INPUT ./2-state-of-the-art/v1.tex +INPUT ./2-state-of-the-art/v1.tex +INPUT 2-state-of-the-art/v1.tex +INPUT ./3-research-approach/v2.tex +INPUT ./3-research-approach/v2.tex +INPUT ./3-research-approach/v2.tex +INPUT ./3-research-approach/v2.tex +INPUT 3-research-approach/v2.tex +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/tfm/adobe/times/zptmcm7t.tfm +INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/zptmcm7t.tfm +INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/zptmcm7t.tfm +INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/zptmcm7m.tfm +INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/zptmcm7m.tfm +INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/zptmcm7m.tfm +INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/zptmcm7y.tfm +INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/zptmcm7y.tfm +INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/zptmcm7y.tfm +INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/zptmcm7v.tfm +INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/zptmcm7v.tfm +INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/zptmcm7v.tfm +INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/ptmb7t.tfm +INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/ptmb7t.tfm +INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/ptmb7t.tfm +INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/ptmri7t.tfm +INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/ptmri7t.tfm +INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/ptmri7t.tfm +INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/public/amsfonts/symbols/msam10.tfm +INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/public/amsfonts/symbols/msam10.tfm +INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/public/amsfonts/symbols/msam10.tfm +INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/public/amsfonts/symbols/msbm10.tfm +INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/public/amsfonts/symbols/msbm10.tfm +INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/public/amsfonts/symbols/msbm10.tfm +INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/public/rsfs/rsfs10.tfm +INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/public/rsfs/rsfs5.tfm +INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/ptmr7t.tfm +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/psnfss/ts1ptm.fd +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/psnfss/ts1ptm.fd +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/psnfss/ts1ptm.fd +INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/ptmr8c.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/ptmr8r.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/zptmcm7t.vf +INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/symbol/psyr.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/zptmcm7y.vf +INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/public/cm/cmsy10.tfm +INPUT /usr/local/texlive/2025/texmf-dist/fonts/vf/adobe/times/ptmr8c.vf +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/ptmr7t.vf +INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/ptmr8r.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/ptmr8r.tfm +INPUT ./4-metrics-of-success/v1.tex +INPUT ./4-metrics-of-success/v1.tex +INPUT ./4-metrics-of-success/v1.tex +INPUT ./4-metrics-of-success/v1.tex +INPUT 4-metrics-of-success/v1.tex +INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/ptmbi7t.tfm +INPUT /usr/local/texlive/2025/texmf-dist/fonts/vf/adobe/times/ptmbi7t.vf +INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/ptmbi8r.tfm +INPUT ./5-risks-and-contingencies/v1.tex +INPUT ./5-risks-and-contingencies/v1.tex +INPUT ./5-risks-and-contingencies/v1.tex +INPUT ./5-risks-and-contingencies/v1.tex +INPUT 5-risks-and-contingencies/v1.tex +INPUT ./6-broader-impacts/v1.tex +INPUT ./6-broader-impacts/v1.tex +INPUT ./6-broader-impacts/v1.tex +INPUT ./6-broader-impacts/v1.tex +INPUT 6-broader-impacts/v1.tex +INPUT ./8-schedule/v1.tex +INPUT ./8-schedule/v1.tex +INPUT ./8-schedule/v1.tex +INPUT ./8-schedule/v1.tex +INPUT 8-schedule/v1.tex +INPUT ./main.bbl +INPUT ./main.bbl +INPUT main.bbl +INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/public/cm/cmtt12.tfm +INPUT main.aux +INPUT /usr/local/texlive/2025/texmf-dist/fonts/type1/public/amsfonts/cm/cmmi10.pfb +INPUT /usr/local/texlive/2025/texmf-dist/fonts/type1/public/amsfonts/cm/cmr10.pfb +INPUT /usr/local/texlive/2025/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy10.pfb +INPUT /usr/local/texlive/2025/texmf-dist/fonts/type1/public/amsfonts/cm/cmtt12.pfb +INPUT /usr/local/texlive/2025/texmf-dist/fonts/type1/public/amsfonts/symbols/msbm10.pfb +INPUT /usr/local/texlive/2025/texmf-dist/fonts/type1/public/rsfs/rsfs10.pfb +INPUT /usr/local/texlive/2025/texmf-dist/fonts/type1/urw/symbol/usyr.pfb +INPUT /usr/local/texlive/2025/texmf-dist/fonts/type1/urw/times/utmb8a.pfb +INPUT /usr/local/texlive/2025/texmf-dist/fonts/type1/urw/times/utmbi8a.pfb +INPUT /usr/local/texlive/2025/texmf-dist/fonts/type1/urw/times/utmr8a.pfb +INPUT /usr/local/texlive/2025/texmf-dist/fonts/type1/urw/times/utmri8a.pfb diff --git a/main.log b/main.log new file mode 100644 index 0000000..5bdba60 --- /dev/null +++ b/main.log @@ -0,0 +1,1000 @@ +This is pdfTeX, Version 3.141592653-2.6-1.40.27 (TeX Live 2025) (preloaded format=pdflatex 2025.3.8) 2 FEB 2026 14:58 +entering extended mode + restricted \write18 enabled. + file:line:error style messages enabled. + %&-line parsing enabled. +**main.tex +(./main.tex +LaTeX2e <2024-11-01> patch level 2 +L3 programming layer <2025-01-18> +(./dane_proposal_format.cls + +LaTeX Warning: You have requested document class `dane_proposal_format', + but the document class provides `prayer_circle'. + +Document Class: prayer_circle 2025/09/02 Custom class for academic documents +(/usr/local/texlive/2025/texmf-dist/tex/latex/base/article.cls +Document Class: article 2024/06/29 v1.4n Standard LaTeX document class +(/usr/local/texlive/2025/texmf-dist/tex/latex/base/size12.clo +File: size12.clo 2024/06/29 v1.4n Standard LaTeX file (size option) +) +\c@part=\count196 +\c@section=\count197 +\c@subsection=\count198 +\c@subsubsection=\count199 +\c@paragraph=\count266 +\c@subparagraph=\count267 +\c@figure=\count268 +\c@table=\count269 +\abovecaptionskip=\skip49 +\belowcaptionskip=\skip50 +\bibindent=\dimen141 +) (/usr/local/texlive/2025/texmf-dist/tex/latex/base/inputenc.sty +Package: inputenc 2024/02/08 v1.3d Input encoding file +\inpenc@prehook=\toks17 +\inpenc@posthook=\toks18 +) (/usr/local/texlive/2025/texmf-dist/tex/latex/geometry/geometry.sty +Package: geometry 2020/01/02 v5.9 Page Geometry + (/usr/local/texlive/2025/texmf-dist/tex/latex/graphics/keyval.sty +Package: keyval 2022/05/29 v1.15 key=value parser (DPC) +\KV@toks@=\toks19 +) (/usr/local/texlive/2025/texmf-dist/tex/generic/iftex/ifvtex.sty +Package: ifvtex 2019/10/25 v1.7 ifvtex legacy package. Use iftex instead. + (/usr/local/texlive/2025/texmf-dist/tex/generic/iftex/iftex.sty +Package: iftex 2024/12/12 v1.0g TeX engine tests +)) +\Gm@cnth=\count270 +\Gm@cntv=\count271 +\c@Gm@tempcnt=\count272 +\Gm@bindingoffset=\dimen142 +\Gm@wd@mp=\dimen143 +\Gm@odd@mp=\dimen144 +\Gm@even@mp=\dimen145 +\Gm@layoutwidth=\dimen146 +\Gm@layoutheight=\dimen147 +\Gm@layouthoffset=\dimen148 +\Gm@layoutvoffset=\dimen149 +\Gm@dimlist=\toks20 +) (/usr/local/texlive/2025/texmf-dist/tex/latex/url/url.sty +\Urlmuskip=\muskip17 +Package: url 2013/09/16 ver 3.4 Verb mode for urls, etc. +) (/usr/local/texlive/2025/texmf-dist/tex/latex/psnfss/mathptmx.sty +Package: mathptmx 2020/03/25 PSNFSS-v9.3 Times w/ Math, improved (SPQR, WaS) +LaTeX Font Info: Redeclaring symbol font `operators' on input line 28. +LaTeX Font Info: Overwriting symbol font `operators' in version `normal' +(Font) OT1/cmr/m/n --> OT1/ztmcm/m/n on input line 28. +LaTeX Font Info: Overwriting symbol font `operators' in version `bold' +(Font) OT1/cmr/bx/n --> OT1/ztmcm/m/n on input line 28. +LaTeX Font Info: Redeclaring symbol font `letters' on input line 29. +LaTeX Font Info: Overwriting symbol font `letters' in version `normal' +(Font) OML/cmm/m/it --> OML/ztmcm/m/it on input line 29. +LaTeX Font Info: Overwriting symbol font `letters' in version `bold' +(Font) OML/cmm/b/it --> OML/ztmcm/m/it on input line 29. +LaTeX Font Info: Redeclaring symbol font `symbols' on input line 30. +LaTeX Font Info: Overwriting symbol font `symbols' in version `normal' +(Font) OMS/cmsy/m/n --> OMS/ztmcm/m/n on input line 30. +LaTeX Font Info: Overwriting symbol font `symbols' in version `bold' +(Font) OMS/cmsy/b/n --> OMS/ztmcm/m/n on input line 30. +LaTeX Font Info: Redeclaring symbol font `largesymbols' on input line 31. +LaTeX Font Info: Overwriting symbol font `largesymbols' in version `normal' +(Font) OMX/cmex/m/n --> OMX/ztmcm/m/n on input line 31. +LaTeX Font Info: Overwriting symbol font `largesymbols' in version `bold' +(Font) OMX/cmex/m/n --> OMX/ztmcm/m/n on input line 31. +\symbold=\mathgroup4 +\symitalic=\mathgroup5 +LaTeX Font Info: Redeclaring math alphabet \mathbf on input line 34. +LaTeX Font Info: Overwriting math alphabet `\mathbf' in version `normal' +(Font) OT1/cmr/bx/n --> OT1/ptm/bx/n on input line 34. +LaTeX Font Info: Overwriting math alphabet `\mathbf' in version `bold' +(Font) OT1/cmr/bx/n --> OT1/ptm/bx/n on input line 34. +LaTeX Font Info: Redeclaring math alphabet \mathit on input line 35. +LaTeX Font Info: Overwriting math alphabet `\mathit' in version `normal' +(Font) OT1/cmr/m/it --> OT1/ptm/m/it on input line 35. +LaTeX Font Info: Overwriting math alphabet `\mathit' in version `bold' +(Font) OT1/cmr/bx/it --> OT1/ptm/m/it on input line 35. +LaTeX Info: Redefining \hbar on input line 50. +) (/usr/local/texlive/2025/texmf-dist/tex/latex/titlesec/titlesec.sty +Package: titlesec 2025/01/04 v2.17 Sectioning titles +\ttl@box=\box52 +\beforetitleunit=\skip51 +\aftertitleunit=\skip52 +\ttl@plus=\dimen150 +\ttl@minus=\dimen151 +\ttl@toksa=\toks21 +\titlewidth=\dimen152 +\titlewidthlast=\dimen153 +\titlewidthfirst=\dimen154 +) (/usr/local/texlive/2025/texmf-dist/tex/latex/setspace/setspace.sty +Package: setspace 2022/12/04 v6.7b set line spacing +) (/usr/local/texlive/2025/texmf-dist/tex/latex/datetime/datetime.sty +Package: datetime 2015/03/20 v2.60 Date Time Package + (/usr/local/texlive/2025/texmf-dist/tex/latex/etoolbox/etoolbox.sty +Package: etoolbox 2025/02/11 v2.5l e-TeX tools for LaTeX (JAW) +\etb@tempcnta=\count273 +) (/usr/local/texlive/2025/texmf-dist/tex/latex/fmtcount/fmtcount.sty +Package: fmtcount 2025/02/09 v3.10 Displaying the values of LaTeX counters (NT,VB,NE) + (/usr/local/texlive/2025/texmf-dist/tex/latex/base/ifthen.sty +Package: ifthen 2024/03/16 v1.1e Standard LaTeX ifthen package (DPC) +) (/usr/local/texlive/2025/texmf-dist/tex/latex/xkeyval/xkeyval.sty +Package: xkeyval 2022/06/16 v2.9 package option processing (HA) + (/usr/local/texlive/2025/texmf-dist/tex/generic/xkeyval/xkeyval.tex (/usr/local/texlive/2025/texmf-dist/tex/generic/xkeyval/xkvutils.tex +\XKV@toks=\toks22 +\XKV@tempa@toks=\toks23 +) +\XKV@depth=\count274 +File: xkeyval.tex 2014/12/03 v2.7a key=value parser (HA) +)) (/usr/local/texlive/2025/texmf-dist/tex/latex/fmtcount/fcprefix.sty +Package: fcprefix 2012/09/28 + (/usr/local/texlive/2025/texmf-dist/tex/latex/fmtcount/fcnumparser.sty +Package: fcnumparser 2017/06/15 +\fc@digit@counter=\count275 +)) (/usr/local/texlive/2025/texmf-dist/tex/latex/amsmath/amsgen.sty +File: amsgen.sty 1999/11/30 v2.0 generic functions +\@emptytoks=\toks24 +\ex@=\dimen155 +) +\c@padzeroesN=\count276 +\fc@tmpcatcode=\count277 +\@DT@modctr=\count278 +\@ordinalctr=\count279 +\@orgargctr=\count280 +\@strctr=\count281 +\@tmpstrctr=\count282 +\@DT@loopN=\count283 +\@DT@X=\count284 +) (/usr/local/texlive/2025/texmf-dist/tex/latex/datetime/datetime-defaults.sty +Package: datetime-defaults 2013/09/10 +) +\@day=\count285 +\@month=\count286 +\@year=\count287 +\c@HOUR=\count288 +\c@HOURXII=\count289 +\c@MINUTE=\count290 +\c@TOHOUR=\count291 +\c@TOMINUTE=\count292 +\c@SECOND=\count293 +\currenthour=\count294 +\currentminute=\count295 +\currentsecond=\count296 +Package datetime Info: No datetime.cfg file found, using default settings on input line 308. +\@dtctr=\count297 +\dayofyear=\count298 +\dayofweek=\count299 +LaTeX Info: Redefining \today on input line 736. +\dt@a=\toks25 +\dt@b=\toks26 +) (/usr/local/texlive/2025/texmf-dist/tex/latex/cite/cite.sty +LaTeX Info: Redefining \cite on input line 302. +LaTeX Info: Redefining \nocite on input line 332. +Package: cite 2015/02/27 v 5.5 +) (/usr/local/texlive/2025/texmf-dist/tex/latex/tocbibind/tocbibind.sty +Package: tocbibind 2010/10/13 v1.5k extra ToC listings +Package tocbibind Info: The document has section divisions on input line 50. + + +Package tocbibind Note: Using section or other style headings. + +) (/usr/local/texlive/2025/texmf-dist/tex/latex/graphics/graphicx.sty +Package: graphicx 2021/09/16 v1.2d Enhanced LaTeX Graphics (DPC,SPQR) + (/usr/local/texlive/2025/texmf-dist/tex/latex/graphics/graphics.sty +Package: graphics 2024/08/06 v1.4g Standard LaTeX Graphics (DPC,SPQR) + (/usr/local/texlive/2025/texmf-dist/tex/latex/graphics/trig.sty +Package: trig 2023/12/02 v1.11 sin cos tan (DPC) +) (/usr/local/texlive/2025/texmf-dist/tex/latex/graphics-cfg/graphics.cfg +File: graphics.cfg 2016/06/04 v1.11 sample graphics configuration +) +Package graphics Info: Driver file: pdftex.def on input line 106. + (/usr/local/texlive/2025/texmf-dist/tex/latex/graphics-def/pdftex.def +File: pdftex.def 2024/04/13 v1.2c Graphics/color driver for pdftex +)) +\Gin@req@height=\dimen156 +\Gin@req@width=\dimen157 +) (/usr/local/texlive/2025/texmf-dist/tex/latex/pdfpages/pdfpages.sty +Package: pdfpages 2025/01/30 v0.6e Insert pages of external PDF documents (AM) + (/usr/local/texlive/2025/texmf-dist/tex/latex/tools/calc.sty +Package: calc 2023/07/08 v4.3 Infix arithmetic (KKT,FJ) +\calc@Acount=\count300 +\calc@Bcount=\count301 +\calc@Adimen=\dimen158 +\calc@Bdimen=\dimen159 +\calc@Askip=\skip53 +\calc@Bskip=\skip54 +LaTeX Info: Redefining \setlength on input line 80. +LaTeX Info: Redefining \addtolength on input line 81. +\calc@Ccount=\count302 +\calc@Cskip=\skip55 +) (/usr/local/texlive/2025/texmf-dist/tex/latex/eso-pic/eso-pic.sty +Package: eso-pic 2023/05/03 v3.0c eso-pic (RN) +\ESO@tempdima=\dimen160 +\ESO@tempdimb=\dimen161 + (/usr/local/texlive/2025/texmf-dist/tex/latex/xcolor/xcolor.sty +Package: xcolor 2024/09/29 v3.02 LaTeX color extensions (UK) + (/usr/local/texlive/2025/texmf-dist/tex/latex/graphics-cfg/color.cfg +File: color.cfg 2016/01/02 v1.6 sample color configuration +) +Package xcolor Info: Driver file: pdftex.def on input line 274. + (/usr/local/texlive/2025/texmf-dist/tex/latex/graphics/mathcolor.ltx) +Package xcolor Info: Model `cmy' substituted by `cmy0' on input line 1349. +Package xcolor Info: Model `hsb' substituted by `rgb' on input line 1353. +Package xcolor Info: Model `RGB' extended on input line 1365. +Package xcolor Info: Model `HTML' substituted by `rgb' on input line 1367. +Package xcolor Info: Model `Hsb' substituted by `hsb' on input line 1368. +Package xcolor Info: Model `tHsb' substituted by `hsb' on input line 1369. +Package xcolor Info: Model `HSB' substituted by `hsb' on input line 1370. +Package xcolor Info: Model `Gray' substituted by `gray' on input line 1371. +Package xcolor Info: Model `wave' substituted by `hsb' on input line 1372. +)) +\AM@pagewidth=\dimen162 +\AM@pageheight=\dimen163 +\AM@fboxrule=\dimen164 + (/usr/local/texlive/2025/texmf-dist/tex/latex/pdfpages/pppdftex.def +File: pppdftex.def 2025/01/30 v0.6e Pdfpages driver for pdfTeX (AM) +) +\pdfpages@includegraphics@status=\count303 +\AM@pagebox=\box53 +\AM@global@opts=\toks27 +\AM@pagecnt=\count304 +\AM@toc@title=\toks28 +\AM@lof@heading=\toks29 +\c@AM@survey=\count305 +\AM@templatesizebox=\box54 +) (/usr/local/texlive/2025/texmf-dist/tex/latex/graphics/rotating.sty +Package: rotating 2016/08/11 v2.16d rotated objects in LaTeX +\c@r@tfl@t=\count306 +\rotFPtop=\skip56 +\rotFPbot=\skip57 +\rot@float@box=\box55 +\rot@mess@toks=\toks30 +) (/usr/local/texlive/2025/texmf-dist/tex/latex/pgf/frontendlayer/tikz.sty (/usr/local/texlive/2025/texmf-dist/tex/latex/pgf/basiclayer/pgf.sty (/usr/local/texlive/2025/texmf-dist/tex/latex/pgf/utilities/pgfrcs.sty (/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/utilities/pgfutil-common.tex +\pgfutil@everybye=\toks31 +\pgfutil@tempdima=\dimen165 +\pgfutil@tempdimb=\dimen166 +) (/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/utilities/pgfutil-latex.def +\pgfutil@abb=\box56 +) (/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/utilities/pgfrcs.code.tex (/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/pgf.revision.tex) +Package: pgfrcs 2023-01-15 v3.1.10 (3.1.10) +)) +Package: pgf 2023-01-15 v3.1.10 (3.1.10) + (/usr/local/texlive/2025/texmf-dist/tex/latex/pgf/basiclayer/pgfcore.sty (/usr/local/texlive/2025/texmf-dist/tex/latex/pgf/systemlayer/pgfsys.sty (/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/systemlayer/pgfsys.code.tex +Package: pgfsys 2023-01-15 v3.1.10 (3.1.10) + (/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/utilities/pgfkeys.code.tex +\pgfkeys@pathtoks=\toks32 +\pgfkeys@temptoks=\toks33 + (/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/utilities/pgfkeyslibraryfiltered.code.tex +\pgfkeys@tmptoks=\toks34 +)) +\pgf@x=\dimen167 +\pgf@y=\dimen168 +\pgf@xa=\dimen169 +\pgf@ya=\dimen170 +\pgf@xb=\dimen171 +\pgf@yb=\dimen172 +\pgf@xc=\dimen173 +\pgf@yc=\dimen174 +\pgf@xd=\dimen175 +\pgf@yd=\dimen176 +\w@pgf@writea=\write3 +\r@pgf@reada=\read2 +\c@pgf@counta=\count307 +\c@pgf@countb=\count308 +\c@pgf@countc=\count309 +\c@pgf@countd=\count310 +\t@pgf@toka=\toks35 +\t@pgf@tokb=\toks36 +\t@pgf@tokc=\toks37 +\pgf@sys@id@count=\count311 + (/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/systemlayer/pgf.cfg +File: pgf.cfg 2023-01-15 v3.1.10 (3.1.10) +) +Driver file for pgf: pgfsys-pdftex.def + (/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/systemlayer/pgfsys-pdftex.def +File: pgfsys-pdftex.def 2023-01-15 v3.1.10 (3.1.10) + +(/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/systemlayer/pgfsys-common-pdf.def +File: pgfsys-common-pdf.def 2023-01-15 v3.1.10 (3.1.10) +))) (/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/systemlayer/pgfsyssoftpath.code.tex +File: pgfsyssoftpath.code.tex 2023-01-15 v3.1.10 (3.1.10) +\pgfsyssoftpath@smallbuffer@items=\count312 +\pgfsyssoftpath@bigbuffer@items=\count313 +) (/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/systemlayer/pgfsysprotocol.code.tex +File: pgfsysprotocol.code.tex 2023-01-15 v3.1.10 (3.1.10) +)) (/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/basiclayer/pgfcore.code.tex +Package: pgfcore 2023-01-15 v3.1.10 (3.1.10) + (/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/math/pgfmath.code.tex (/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/math/pgfmathutil.code.tex) (/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/math/pgfmathparser.code.tex +\pgfmath@dimen=\dimen177 +\pgfmath@count=\count314 +\pgfmath@box=\box57 +\pgfmath@toks=\toks38 +\pgfmath@stack@operand=\toks39 +\pgfmath@stack@operation=\toks40 +) (/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/math/pgfmathfunctions.code.tex) (/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/math/pgfmathfunctions.basic.code.tex) (/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/math/pgfmathfunctions.trigonometric.code.tex) (/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/math/pgfmathfunctions.random.code.tex) (/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/math/pgfmathfunctions.comparison.code.tex) (/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/math/pgfmathfunctions.base.code.tex) (/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/math/pgfmathfunctions.round.code.tex) (/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/math/pgfmathfunctions.misc.code.tex) (/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/math/pgfmathfunctions.integerarithmetics.code.tex) (/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/math/pgfmathcalc.code.tex) (/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/math/pgfmathfloat.code.tex +\c@pgfmathroundto@lastzeros=\count315 +)) (/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/math/pgfint.code.tex) (/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/basiclayer/pgfcorepoints.code.tex +File: pgfcorepoints.code.tex 2023-01-15 v3.1.10 (3.1.10) +\pgf@picminx=\dimen178 +\pgf@picmaxx=\dimen179 +\pgf@picminy=\dimen180 +\pgf@picmaxy=\dimen181 +\pgf@pathminx=\dimen182 +\pgf@pathmaxx=\dimen183 +\pgf@pathminy=\dimen184 +\pgf@pathmaxy=\dimen185 +\pgf@xx=\dimen186 +\pgf@xy=\dimen187 +\pgf@yx=\dimen188 +\pgf@yy=\dimen189 +\pgf@zx=\dimen190 +\pgf@zy=\dimen191 +) (/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/basiclayer/pgfcorepathconstruct.code.tex +File: pgfcorepathconstruct.code.tex 2023-01-15 v3.1.10 (3.1.10) +\pgf@path@lastx=\dimen192 +\pgf@path@lasty=\dimen193 +) (/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/basiclayer/pgfcorepathusage.code.tex +File: pgfcorepathusage.code.tex 2023-01-15 v3.1.10 (3.1.10) +\pgf@shorten@end@additional=\dimen194 +\pgf@shorten@start@additional=\dimen195 +) +(/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/basiclayer/pgfcorescopes.code.tex +File: pgfcorescopes.code.tex 2023-01-15 v3.1.10 (3.1.10) +\pgfpic=\box58 +\pgf@hbox=\box59 +\pgf@layerbox@main=\box60 +\pgf@picture@serial@count=\count316 +) (/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/basiclayer/pgfcoregraphicstate.code.tex +File: pgfcoregraphicstate.code.tex 2023-01-15 v3.1.10 (3.1.10) +\pgflinewidth=\dimen196 +) (/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/basiclayer/pgfcoretransformations.code.tex +File: pgfcoretransformations.code.tex 2023-01-15 v3.1.10 (3.1.10) +\pgf@pt@x=\dimen197 +\pgf@pt@y=\dimen198 +\pgf@pt@temp=\dimen199 +) (/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/basiclayer/pgfcorequick.code.tex +File: pgfcorequick.code.tex 2023-01-15 v3.1.10 (3.1.10) +) (/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/basiclayer/pgfcoreobjects.code.tex +File: pgfcoreobjects.code.tex 2023-01-15 v3.1.10 (3.1.10) +) (/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/basiclayer/pgfcorepathprocessing.code.tex +File: pgfcorepathprocessing.code.tex 2023-01-15 v3.1.10 (3.1.10) +) (/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/basiclayer/pgfcorearrows.code.tex +File: pgfcorearrows.code.tex 2023-01-15 v3.1.10 (3.1.10) +\pgfarrowsep=\dimen256 +) (/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/basiclayer/pgfcoreshade.code.tex +File: pgfcoreshade.code.tex 2023-01-15 v3.1.10 (3.1.10) +\pgf@max=\dimen257 +\pgf@sys@shading@range@num=\count317 +\pgf@shadingcount=\count318 +) (/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/basiclayer/pgfcoreimage.code.tex +File: pgfcoreimage.code.tex 2023-01-15 v3.1.10 (3.1.10) +) (/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/basiclayer/pgfcoreexternal.code.tex +File: pgfcoreexternal.code.tex 2023-01-15 v3.1.10 (3.1.10) +\pgfexternal@startupbox=\box61 +) (/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/basiclayer/pgfcorelayers.code.tex +File: pgfcorelayers.code.tex 2023-01-15 v3.1.10 (3.1.10) +) (/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/basiclayer/pgfcoretransparency.code.tex +File: pgfcoretransparency.code.tex 2023-01-15 v3.1.10 (3.1.10) +) (/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/basiclayer/pgfcorepatterns.code.tex +File: pgfcorepatterns.code.tex 2023-01-15 v3.1.10 (3.1.10) +) (/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/basiclayer/pgfcorerdf.code.tex +File: pgfcorerdf.code.tex 2023-01-15 v3.1.10 (3.1.10) +))) (/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/modules/pgfmoduleshapes.code.tex +File: pgfmoduleshapes.code.tex 2023-01-15 v3.1.10 (3.1.10) +\pgfnodeparttextbox=\box62 +) (/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/modules/pgfmoduleplot.code.tex +File: pgfmoduleplot.code.tex 2023-01-15 v3.1.10 (3.1.10) +) (/usr/local/texlive/2025/texmf-dist/tex/latex/pgf/compatibility/pgfcomp-version-0-65.sty +Package: pgfcomp-version-0-65 2023-01-15 v3.1.10 (3.1.10) +\pgf@nodesepstart=\dimen258 +\pgf@nodesepend=\dimen259 +) (/usr/local/texlive/2025/texmf-dist/tex/latex/pgf/compatibility/pgfcomp-version-1-18.sty +Package: pgfcomp-version-1-18 2023-01-15 v3.1.10 (3.1.10) +)) (/usr/local/texlive/2025/texmf-dist/tex/latex/pgf/utilities/pgffor.sty (/usr/local/texlive/2025/texmf-dist/tex/latex/pgf/utilities/pgfkeys.sty (/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/utilities/pgfkeys.code.tex)) (/usr/local/texlive/2025/texmf-dist/tex/latex/pgf/math/pgfmath.sty (/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/math/pgfmath.code.tex)) +(/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/utilities/pgffor.code.tex +Package: pgffor 2023-01-15 v3.1.10 (3.1.10) +\pgffor@iter=\dimen260 +\pgffor@skip=\dimen261 +\pgffor@stack=\toks41 +\pgffor@toks=\toks42 +)) (/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/frontendlayer/tikz/tikz.code.tex +Package: tikz 2023-01-15 v3.1.10 (3.1.10) + (/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/libraries/pgflibraryplothandlers.code.tex +File: pgflibraryplothandlers.code.tex 2023-01-15 v3.1.10 (3.1.10) +\pgf@plot@mark@count=\count319 +\pgfplotmarksize=\dimen262 +) +\tikz@lastx=\dimen263 +\tikz@lasty=\dimen264 +\tikz@lastxsaved=\dimen265 +\tikz@lastysaved=\dimen266 +\tikz@lastmovetox=\dimen267 +\tikz@lastmovetoy=\dimen268 +\tikzleveldistance=\dimen269 +\tikzsiblingdistance=\dimen270 +\tikz@figbox=\box63 +\tikz@figbox@bg=\box64 +\tikz@tempbox=\box65 +\tikz@tempbox@bg=\box66 +\tikztreelevel=\count320 +\tikznumberofchildren=\count321 +\tikznumberofcurrentchild=\count322 +\tikz@fig@count=\count323 + (/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/modules/pgfmodulematrix.code.tex +File: pgfmodulematrix.code.tex 2023-01-15 v3.1.10 (3.1.10) +\pgfmatrixcurrentrow=\count324 +\pgfmatrixcurrentcolumn=\count325 +\pgf@matrix@numberofcolumns=\count326 +) +\tikz@expandcount=\count327 + (/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibrarytopaths.code.tex +File: tikzlibrarytopaths.code.tex 2023-01-15 v3.1.10 (3.1.10) +))) (/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibrarypositioning.code.tex +File: tikzlibrarypositioning.code.tex 2023-01-15 v3.1.10 (3.1.10) +) (/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibraryshapes.code.tex +File: tikzlibraryshapes.code.tex 2023-01-15 v3.1.10 (3.1.10) + (/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibraryshapes.geometric.code.tex +File: tikzlibraryshapes.geometric.code.tex 2023-01-15 v3.1.10 (3.1.10) + (/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/libraries/shapes/pgflibraryshapes.geometric.code.tex +File: pgflibraryshapes.geometric.code.tex 2023-01-15 v3.1.10 (3.1.10) +)) (/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibraryshapes.misc.code.tex +File: tikzlibraryshapes.misc.code.tex 2023-01-15 v3.1.10 (3.1.10) + (/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/libraries/shapes/pgflibraryshapes.misc.code.tex +File: pgflibraryshapes.misc.code.tex 2023-01-15 v3.1.10 (3.1.10) +)) (/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibraryshapes.symbols.code.tex +File: tikzlibraryshapes.symbols.code.tex 2023-01-15 v3.1.10 (3.1.10) + (/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/libraries/shapes/pgflibraryshapes.symbols.code.tex +File: pgflibraryshapes.symbols.code.tex 2023-01-15 v3.1.10 (3.1.10) +)) (/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibraryshapes.arrows.code.tex +File: tikzlibraryshapes.arrows.code.tex 2023-01-15 v3.1.10 (3.1.10) + (/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/libraries/shapes/pgflibraryshapes.arrows.code.tex +File: pgflibraryshapes.arrows.code.tex 2023-01-15 v3.1.10 (3.1.10) +)) (/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibraryshapes.callouts.code.tex (/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/libraries/shapes/pgflibraryshapes.callouts.code.tex)) (/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibraryshapes.multipart.code.tex +File: tikzlibraryshapes.multipart.code.tex 2023-01-15 v3.1.10 (3.1.10) + +(/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/libraries/shapes/pgflibraryshapes.multipart.code.tex +File: pgflibraryshapes.multipart.code.tex 2023-01-15 v3.1.10 (3.1.10) +\pgfnodepartlowerbox=\box67 +\pgfnodeparttwobox=\box68 +\pgfnodepartthreebox=\box69 +\pgfnodepartfourbox=\box70 +\pgfnodeparttwentybox=\box71 +\pgfnodepartnineteenbox=\box72 +\pgfnodeparteighteenbox=\box73 +\pgfnodepartseventeenbox=\box74 +\pgfnodepartsixteenbox=\box75 +\pgfnodepartfifteenbox=\box76 +\pgfnodepartfourteenbox=\box77 +\pgfnodepartthirteenbox=\box78 +\pgfnodeparttwelvebox=\box79 +\pgfnodepartelevenbox=\box80 +\pgfnodeparttenbox=\box81 +\pgfnodepartninebox=\box82 +\pgfnodeparteightbox=\box83 +\pgfnodepartsevenbox=\box84 +\pgfnodepartsixbox=\box85 +\pgfnodepartfivebox=\box86 +))) (/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibraryarrows.code.tex +File: tikzlibraryarrows.code.tex 2023-01-15 v3.1.10 (3.1.10) + (/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/libraries/pgflibraryarrows.code.tex +File: pgflibraryarrows.code.tex 2023-01-15 v3.1.10 (3.1.10) +\arrowsize=\dimen271 +)) (/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/graphs/tikzlibrarygraphs.code.tex +File: tikzlibrarygraphs.code.tex 2023-01-15 v3.1.10 (3.1.10) +\tikz@lib@auto@number=\count328 +\tikz@qnode@count=\count329 +) (/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibrarycalc.code.tex +File: tikzlibrarycalc.code.tex 2023-01-15 v3.1.10 (3.1.10) +) (/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibrarychains.code.tex +File: tikzlibrarychains.code.tex 2023-01-15 v3.1.10 (3.1.10) +) (/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibrarydecorations.markings.code.tex (/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibrarydecorations.code.tex (/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/modules/pgfmoduledecorations.code.tex +\pgfdecoratedcompleteddistance=\dimen272 +\pgfdecoratedremainingdistance=\dimen273 +\pgfdecoratedinputsegmentcompleteddistance=\dimen274 +\pgfdecoratedinputsegmentremainingdistance=\dimen275 +\pgf@decorate@distancetomove=\dimen276 +\pgf@decorate@repeatstate=\count330 +\pgfdecorationsegmentamplitude=\dimen277 +\pgfdecorationsegmentlength=\dimen278 +) +\tikz@lib@dec@box=\box87 +) (/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/libraries/decorations/pgflibrarydecorations.markings.code.tex)) (/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibraryshadows.code.tex +File: tikzlibraryshadows.code.tex 2023-01-15 v3.1.10 (3.1.10) + (/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibraryfadings.code.tex +File: tikzlibraryfadings.code.tex 2023-01-15 v3.1.10 (3.1.10) + (/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/libraries/pgflibraryfadings.code.tex +File: pgflibraryfadings.code.tex 2023-01-15 v3.1.10 (3.1.10) +))) (/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/libraries/pgflibraryarrows.meta.code.tex +File: pgflibraryarrows.meta.code.tex 2023-01-15 v3.1.10 (3.1.10) +\pgfarrowinset=\dimen279 +\pgfarrowlength=\dimen280 +\pgfarrowwidth=\dimen281 +\pgfarrowlinewidth=\dimen282 +) (/usr/local/texlive/2025/texmf-dist/tex/latex/standalone/standalone.sty +Package: standalone 2025/02/22 v1.5a Package to include TeX sub-files with preambles + (/usr/local/texlive/2025/texmf-dist/tex/latex/tools/shellesc.sty +Package: shellesc 2023/07/08 v1.0d unified shell escape interface for LaTeX +Package shellesc Info: Restricted shell escape enabled on input line 77. +) (/usr/local/texlive/2025/texmf-dist/tex/latex/currfile/currfile.sty +Package: currfile 2024/03/14 v1.0 Provides the file path elements of the current input file + (/usr/local/texlive/2025/texmf-dist/tex/latex/kvoptions/kvoptions.sty +Package: kvoptions 2022-06-15 v3.15 Key value format for package options (HO) + (/usr/local/texlive/2025/texmf-dist/tex/generic/ltxcmds/ltxcmds.sty +Package: ltxcmds 2023-12-04 v1.26 LaTeX kernel commands for general use (HO) +) (/usr/local/texlive/2025/texmf-dist/tex/latex/kvsetkeys/kvsetkeys.sty +Package: kvsetkeys 2022-10-05 v1.19 Key value parser (HO) +)) (/usr/local/texlive/2025/texmf-dist/tex/latex/filehook/filehook.sty +Package: filehook 2022/10/25 v0.8b Hooks for input files + +(/usr/local/texlive/2025/texmf-dist/tex/latex/filehook/filehook-2020.sty +Package: filehook-2020 2022/10/25 v0.8b Hooks for input files +)) +\c@currfiledepth=\count331 +) (/usr/local/texlive/2025/texmf-dist/tex/latex/gincltex/gincltex.sty (/usr/local/texlive/2025/texmf-dist/tex/latex/svn-prov/svn-prov.sty +Package: svn-prov 2010/04/24 v3.1862 Package Date/Version from SVN Keywords +) +Package: gincltex 2011/09/04 v0.3 Include external LaTeX files like graphics + (/usr/local/texlive/2025/texmf-dist/tex/latex/adjustbox/adjustbox.sty +Package: adjustbox 2025/02/26 v1.3c Adjusting TeX boxes (trim, clip, ...) + (/usr/local/texlive/2025/texmf-dist/tex/latex/adjustbox/adjcalc.sty +Package: adjcalc 2012/05/16 v1.1 Provides advanced setlength with multiple back-ends (calc, etex, pgfmath) +) (/usr/local/texlive/2025/texmf-dist/tex/latex/adjustbox/trimclip.sty +Package: trimclip 2025/02/21 v1.2a Trim and clip general TeX material + (/usr/local/texlive/2025/texmf-dist/tex/latex/collectbox/collectbox.sty +Package: collectbox 2022/10/17 v0.4c Collect macro arguments as boxes +\collectedbox=\box88 +) +\tc@llx=\dimen283 +\tc@lly=\dimen284 +\tc@urx=\dimen285 +\tc@ury=\dimen286 +Package trimclip Info: Using driver 'tc-pdftex.def'. + (/usr/local/texlive/2025/texmf-dist/tex/latex/adjustbox/tc-pdftex.def +File: tc-pdftex.def 2025/02/26 v2.3 Clipping driver for pdftex +)) +\adjbox@Width=\dimen287 +\adjbox@Height=\dimen288 +\adjbox@Depth=\dimen289 +\adjbox@Totalheight=\dimen290 +\adjbox@pwidth=\dimen291 +\adjbox@pheight=\dimen292 +\adjbox@pdepth=\dimen293 +\adjbox@ptotalheight=\dimen294 + (/usr/local/texlive/2025/texmf-dist/tex/latex/ifoddpage/ifoddpage.sty +Package: ifoddpage 2022/10/18 v1.2 Conditionals for odd/even page detection +\c@checkoddpage=\count332 +) (/usr/local/texlive/2025/texmf-dist/tex/latex/varwidth/varwidth.sty +Package: varwidth 2009/03/30 ver 0.92; Variable-width minipages +\@vwid@box=\box89 +\sift@deathcycles=\count333 +\@vwid@loff=\dimen295 +\@vwid@roff=\dimen296 +)) +\gincltex@box=\box90 +) (/usr/local/texlive/2025/texmf-dist/tex/latex/filemod/filemod-expmin.sty +Package: filemod-expmin 2011/09/19 v1.2 Get and compare file modification times (expandable; minimal) +)) (/usr/local/texlive/2025/texmf-dist/tex/latex/booktabs/booktabs.sty +Package: booktabs 2020/01/12 v1.61803398 Publication quality tables +\heavyrulewidth=\dimen297 +\lightrulewidth=\dimen298 +\cmidrulewidth=\dimen299 +\belowrulesep=\dimen300 +\belowbottomsep=\dimen301 +\aboverulesep=\dimen302 +\abovetopsep=\dimen303 +\cmidrulesep=\dimen304 +\cmidrulekern=\dimen305 +\defaultaddspace=\dimen306 +\@cmidla=\count334 +\@cmidlb=\count335 +\@aboverulesep=\dimen307 +\@belowrulesep=\dimen308 +\@thisruleclass=\count336 +\@lastruleclass=\count337 +\@thisrulewidth=\dimen309 +) (/usr/local/texlive/2025/texmf-dist/tex/latex/tools/tabularx.sty +Package: tabularx 2023/12/11 v2.12a `tabularx' package (DPC) + (/usr/local/texlive/2025/texmf-dist/tex/latex/tools/array.sty +Package: array 2024/10/17 v2.6g Tabular extension package (FMi) +\col@sep=\dimen310 +\ar@mcellbox=\box91 +\extrarowheight=\dimen311 +\NC@list=\toks43 +\extratabsurround=\skip58 +\backup@length=\skip59 +\ar@cellbox=\box92 +) +\TX@col@width=\dimen312 +\TX@old@table=\dimen313 +\TX@old@col=\dimen314 +\TX@target=\dimen315 +\TX@delta=\dimen316 +\TX@cols=\count338 +\TX@ftn=\toks44 +) (/usr/local/texlive/2025/texmf-dist/tex/latex/makecell/makecell.sty +Package: makecell 2009/08/03 V0.1e Managing of Tab Column Heads and Cells +\rotheadsize=\dimen317 +\c@nlinenum=\count339 +\TeXr@lab=\toks45 +) (/usr/local/texlive/2025/texmf-dist/tex/latex/tools/dcolumn.sty +Package: dcolumn 2023/07/08 v1.06 decimal alignment package (DPC) +) (/usr/local/texlive/2025/texmf-dist/tex/latex/multirow/multirow.sty +Package: multirow 2024/11/12 v2.9 Span multiple rows of a table +\multirow@colwidth=\skip60 +\multirow@cntb=\count340 +\multirow@dima=\skip61 +\bigstrutjot=\dimen318 +) (/usr/local/texlive/2025/texmf-dist/tex/latex/graphics/lscape.sty +Package: lscape 2020/05/28 v3.02 Landscape Pages (DPC) +) (/usr/local/texlive/2025/texmf-dist/tex/latex/amsmath/amsmath.sty +Package: amsmath 2024/11/05 v2.17t AMS math features +\@mathmargin=\skip62 + +For additional information on amsmath, use the `?' option. +(/usr/local/texlive/2025/texmf-dist/tex/latex/amsmath/amstext.sty +Package: amstext 2021/08/26 v2.01 AMS text +) (/usr/local/texlive/2025/texmf-dist/tex/latex/amsmath/amsbsy.sty +Package: amsbsy 1999/11/29 v1.2d Bold Symbols +\pmbraise@=\dimen319 +) (/usr/local/texlive/2025/texmf-dist/tex/latex/amsmath/amsopn.sty +Package: amsopn 2022/04/08 v2.04 operator names +) +\inf@bad=\count341 +LaTeX Info: Redefining \frac on input line 233. +\uproot@=\count342 +\leftroot@=\count343 +LaTeX Info: Redefining \overline on input line 398. +LaTeX Info: Redefining \colon on input line 409. +\classnum@=\count344 +\DOTSCASE@=\count345 +LaTeX Info: Redefining \ldots on input line 495. +LaTeX Info: Redefining \dots on input line 498. +LaTeX Info: Redefining \cdots on input line 619. +\Mathstrutbox@=\box93 +\strutbox@=\box94 +LaTeX Info: Redefining \big on input line 721. +LaTeX Info: Redefining \Big on input line 722. +LaTeX Info: Redefining \bigg on input line 723. +LaTeX Info: Redefining \Bigg on input line 724. +\big@size=\dimen320 +LaTeX Font Info: Redeclaring font encoding OML on input line 742. +LaTeX Font Info: Redeclaring font encoding OMS on input line 743. +\macc@depth=\count346 +LaTeX Info: Redefining \bmod on input line 904. +LaTeX Info: Redefining \pmod on input line 909. +LaTeX Info: Redefining \smash on input line 939. +LaTeX Info: Redefining \relbar on input line 969. +LaTeX Info: Redefining \Relbar on input line 970. +\c@MaxMatrixCols=\count347 +\dotsspace@=\muskip18 +\c@parentequation=\count348 +\dspbrk@lvl=\count349 +\tag@help=\toks46 +\row@=\count350 +\column@=\count351 +\maxfields@=\count352 +\andhelp@=\toks47 +\eqnshift@=\dimen321 +\alignsep@=\dimen322 +\tagshift@=\dimen323 +\tagwidth@=\dimen324 +\totwidth@=\dimen325 +\lineht@=\dimen326 +\@envbody=\toks48 +\multlinegap=\skip63 +\multlinetaggap=\skip64 +\mathdisplay@stack=\toks49 +LaTeX Info: Redefining \[ on input line 2953. +LaTeX Info: Redefining \] on input line 2954. +) (/usr/local/texlive/2025/texmf-dist/tex/latex/amsfonts/amssymb.sty +Package: amssymb 2013/01/14 v3.01 AMS font symbols + (/usr/local/texlive/2025/texmf-dist/tex/latex/amsfonts/amsfonts.sty +Package: amsfonts 2013/01/14 v3.01 Basic AMSFonts support +\symAMSa=\mathgroup6 +\symAMSb=\mathgroup7 +LaTeX Font Info: Overwriting math alphabet `\mathfrak' in version `bold' +(Font) U/euf/m/n --> U/euf/b/n on input line 106. +)) (/usr/local/texlive/2025/texmf-dist/tex/latex/jknapltx/mathrsfs.sty +Package: mathrsfs 1996/01/01 Math RSFS package v1.0 (jk) +\symrsfs=\mathgroup8 +) (/usr/local/texlive/2025/texmf-dist/tex/latex/enumitem/enumitem.sty +Package: enumitem 2025/02/06 v3.11 Customized lists +\labelindent=\skip65 +\enit@outerparindent=\dimen327 +\enit@toks=\toks50 +\enit@inbox=\box95 +\enit@count@id=\count353 +\enitdp@description=\count354 +) (/usr/local/texlive/2025/texmf-dist/tex/latex/listings/listings.sty +\lst@mode=\count355 +\lst@gtempboxa=\box96 +\lst@token=\toks51 +\lst@length=\count356 +\lst@currlwidth=\dimen328 +\lst@column=\count357 +\lst@pos=\count358 +\lst@lostspace=\dimen329 +\lst@width=\dimen330 +\lst@newlines=\count359 +\lst@lineno=\count360 +\lst@maxwidth=\dimen331 + (/usr/local/texlive/2025/texmf-dist/tex/latex/listings/lstpatch.sty +File: lstpatch.sty 2024/09/23 1.10c (Carsten Heinz) +) (/usr/local/texlive/2025/texmf-dist/tex/latex/listings/lstmisc.sty +File: lstmisc.sty 2024/09/23 1.10c (Carsten Heinz) +\c@lstnumber=\count361 +\lst@skipnumbers=\count362 +\lst@framebox=\box97 +) (/usr/local/texlive/2025/texmf-dist/tex/latex/listings/listings.cfg +File: listings.cfg 2024/09/23 1.10c listings configuration +)) +Package: listings 2024/09/23 1.10c (Carsten Heinz) + (/usr/local/texlive/2025/texmf-dist/tex/latex/pgfgantt/pgfgantt.sty +Package: pgfgantt 2024/06/19 v5.0a Draw Gantt diagrams with TikZ + (/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibrarybackgrounds.code.tex +File: tikzlibrarybackgrounds.code.tex 2023-01-15 v3.1.10 (3.1.10) +\pgf@layerbox@background=\box98 +\pgf@layerboxsaved@background=\box99 +) (/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibrarypatterns.code.tex +File: tikzlibrarypatterns.code.tex 2023-01-15 v3.1.10 (3.1.10) + (/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/libraries/pgflibrarypatterns.code.tex +File: pgflibrarypatterns.code.tex 2023-01-15 v3.1.10 (3.1.10) +)) (/usr/local/texlive/2025/texmf-dist/tex/latex/pgf/utilities/pgfcalendar.sty (/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/utilities/pgfcalendar.code.tex +File: pgfcalendar.code.tex 2023-01-15 v3.1.10 (3.1.10) +\pgfcalendarcurrentjulian=\count363 +\pgf@cal@easter@Y=\count364 +\pgf@cal@easter@G=\count365 +\pgf@cal@easter@C=\count366 +\pgf@cal@easter@X=\count367 +\pgf@cal@easter@Z=\count368 +\pgf@cal@easter@D=\count369 +\pgf@cal@easter@E=\count370 +\pgf@cal@easter@N=\count371 +\pgf@cal@easter@M=\count372 +\pgf@cal@easter@julianday=\count373 +)) +\gtt@currentline=\count374 +\gtt@lasttitleline=\count375 +\gtt@currgrid=\count376 +\gtt@chartwidth=\count377 +\gtt@lasttitleslot=\count378 +\gtt@elementid=\count379 +\gtt@today@slot=\count380 +\gtt@startjulian=\count381 +\gtt@endjulian=\count382 +\gtt@chartid=\count383 +\gtt@vrule@slot=\count384 +\gtt@calendar@slots=\count385 +\gtt@calendar@weeknumber=\count386 +\gtt@calendar@startofweek=\count387 +\gtt@left@slot=\count388 +\gtt@right@slot=\count389 +) +\figurewidth=\skip66 +\figureheight=\skip67 +\c@task=\count390 +) (/usr/local/texlive/2025/texmf-dist/tex/latex/colortbl/colortbl.sty +Package: colortbl 2024/07/06 v1.0i Color table columns (DPC) +\everycr=\toks52 +\minrowclearance=\skip68 +\rownum=\count391 +) +LaTeX Font Info: Trying to load font information for OT1+ptm on input line 10. + (/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=\count392 +\l__pdf_internal_box=\box100 +) (./main.aux) +\openout1 = `main.aux'. + +LaTeX Font Info: Checking defaults for OML/cmm/m/it on input line 10. +LaTeX Font Info: ... okay on input line 10. +LaTeX Font Info: Checking defaults for OMS/cmsy/m/n on input line 10. +LaTeX Font Info: ... okay on input line 10. +LaTeX Font Info: Checking defaults for OT1/cmr/m/n on input line 10. +LaTeX Font Info: ... okay on input line 10. +LaTeX Font Info: Checking defaults for T1/cmr/m/n on input line 10. +LaTeX Font Info: ... okay on input line 10. +LaTeX Font Info: Checking defaults for TS1/cmr/m/n on input line 10. +LaTeX Font Info: ... okay on input line 10. +LaTeX Font Info: Checking defaults for OMX/cmex/m/n on input line 10. +LaTeX Font Info: ... okay on input line 10. +LaTeX Font Info: Checking defaults for U/cmr/m/n on input line 10. +LaTeX Font Info: ... okay on input line 10. + +*geometry* driver: auto-detecting +*geometry* detected driver: pdftex +*geometry* verbose mode - [ preamble ] result: +* driver: pdftex +* paper: +* layout: +* layoutoffset:(h,v)=(0.0pt,0.0pt) +* modes: +* h-part:(L,W,R)=(72.26999pt, 469.75502pt, 72.26999pt) +* v-part:(T,H,B)=(72.26999pt, 650.43001pt, 72.26999pt) +* \paperwidth=614.295pt +* \paperheight=794.96999pt +* \textwidth=469.75502pt +* \textheight=650.43001pt +* \oddsidemargin=0.0pt +* \evensidemargin=0.0pt +* \topmargin=-37.0pt +* \headheight=12.0pt +* \headsep=25.0pt +* \topskip=12.0pt +* \footskip=30.0pt +* \marginparwidth=44.0pt +* \marginparsep=10.0pt +* \columnsep=10.0pt +* \skip\footins=10.8pt plus 4.0pt minus 2.0pt +* \hoffset=0.0pt +* \voffset=0.0pt +* \mag=1000 +* \@twocolumnfalse +* \@twosidefalse +* \@mparswitchfalse +* \@reversemarginfalse +* (1in=72.27pt=25.4mm, 1cm=28.453pt) + +(/usr/local/texlive/2025/texmf-dist/tex/latex/fmtcount/fc-english.def +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=\count393 +\scratchdimen=\dimen332 +\scratchbox=\box101 +\nofMPsegments=\count394 +\nofMParguments=\count395 +\everyMPshowfont=\toks53 +\MPscratchCnt=\count396 +\MPscratchDim=\dimen333 +\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 +Package epstopdf-base Info: Redefining graphics rule for `.eps' on input line 485. + (/usr/local/texlive/2025/texmf-dist/tex/latex/latexconfig/epstopdf-sys.cfg +File: epstopdf-sys.cfg 2010/07/13 v1.3 Configuration of (r)epstopdf for TeX Live +)) (/usr/local/texlive/2025/texmf-dist/tex/latex/pdflscape/pdflscape.sty +Package: pdflscape 2022-10-27 v0.13 Display of landscape pages in PDF + (/usr/local/texlive/2025/texmf-dist/tex/latex/pdflscape/pdflscape-nometadata.sty +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=\count399 +LaTeX Font Info: Trying to load font information for OT1+ztmcm on input line 13. + (/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. +) +LaTeX Font Info: Trying to load font information for OML+ztmcm on input line 13. + (/usr/local/texlive/2025/texmf-dist/tex/latex/psnfss/omlztmcm.fd +File: omlztmcm.fd 2000/01/03 Fontinst v1.801 font definitions for OML/ztmcm. +) +LaTeX Font Info: Trying to load font information for OMS+ztmcm on input line 13. + (/usr/local/texlive/2025/texmf-dist/tex/latex/psnfss/omsztmcm.fd +File: omsztmcm.fd 2000/01/03 Fontinst v1.801 font definitions for OMS/ztmcm. +) +LaTeX Font Info: Trying to load font information for OMX+ztmcm on input line 13. + (/usr/local/texlive/2025/texmf-dist/tex/latex/psnfss/omxztmcm.fd +File: omxztmcm.fd 2000/01/03 Fontinst v1.801 font definitions for OMX/ztmcm. +) +LaTeX Font Info: Font shape `OT1/ptm/bx/n' in size <14.4> not available +(Font) Font shape `OT1/ptm/b/n' tried instead on input line 13. +LaTeX Font Info: Font shape `OT1/ptm/bx/n' in size <10.95> not available +(Font) Font shape `OT1/ptm/b/n' tried instead on input line 13. +LaTeX Font Info: Font shape `OT1/ptm/bx/n' in size <8> not available +(Font) Font shape `OT1/ptm/b/n' tried instead on input line 13. +LaTeX Font Info: Trying to load font information for U+rsfs on input line 13. + (/usr/local/texlive/2025/texmf-dist/tex/latex/jknapltx/ursfs.fd +File: ursfs.fd 1998/03/24 rsfs font definition file (jk) +) + +[1 + +{/usr/local/texlive/2025/texmf-var/fonts/map/pdftex/updmap/pdftex.map}{/usr/local/texlive/2025/texmf-dist/fonts/enc/dvips/base/8r.enc}] (./1-goals-and-outcomes/research_statement_v1.tex) + +[1] (./main.toc +LaTeX Font Info: Font shape `OT1/ptm/bx/n' in size <12> 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 <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. +) +\tf@toc=\write4 +\openout4 = `main.toc'. + + + +[2] (./1-goals-and-outcomes/v1.tex + +[1]) + +[2] (./2-state-of-the-art/v1.tex + +[3] + +[4]) + +[5] (./3-research-approach/v2.tex +LaTeX Font Info: Font shape `OT1/ptm/bx/n' in size <10> not available +(Font) Font shape `OT1/ptm/b/n' tried instead on input line 255. +LaTeX Font Info: Font shape `OT1/ptm/bx/n' in size <7.4> not available +(Font) Font shape `OT1/ptm/b/n' tried instead on input line 255. +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 255. + + +LaTeX Warning: Citation `HANDBOOK ON HYBRID SYSTEMS CONTROL' on page 6 undefined on input line 258. + +LaTeX Font Info: Trying to load font information for TS1+ptm on input line 268. +(/usr/local/texlive/2025/texmf-dist/tex/latex/psnfss/ts1ptm.fd +File: ts1ptm.fd 2001/06/04 font definitions for TS1/ptm. +) + +./3-research-approach/v2.tex:278: LaTeX Error: \mathcal allowed only in math mode. + +See the LaTeX manual or LaTeX Companion for explanation. +Type H for immediate help. + ... + +l.278 \item \mathcal + {R}: Reset maps that define state 'jumps' +You're in trouble here. Try typing to proceed. +If that doesn't work, type X to quit. + +) + +[6] (./4-metrics-of-success/v1.tex + +[7]) + +[8] (./5-risks-and-contingencies/v1.tex + +[9] + +[10]) + +[11] (./6-broader-impacts/v1.tex) + +[12] + +[13] (./8-schedule/v1.tex +Missing character: There is no , in font nullfont! +) (./main.bbl + +[14] +Underfull \hbox (badness 10000) in paragraph at lines 32--33 +\OT1/cmtt/m/n/12 nuclear . org / information -[] library / safety -[] and -[] security / safety -[] of -[] + [] + + + +[15]) + +[16] (./main.aux) + *********** +LaTeX2e <2024-11-01> patch level 2 +L3 programming layer <2025-01-18> + *********** + + +LaTeX Warning: There were undefined references. + + ) +Here is how much of TeX's memory you used: + 26141 strings out of 473190 + 544988 string characters out of 5715801 + 963880 words of memory out of 5000000 + 48799 multiletter control sequences out of 15000+600000 + 608553 words of font info for 146 fonts, out of 8000000 for 9000 + 1141 hyphenation exceptions out of 8191 + 110i,9n,107p,1062b,952s stack positions out of 10000i,1000n,20000p,200000b,200000s + +Output written on main.pdf (19 pages, 153240 bytes). +PDF statistics: + 149 PDF objects out of 1000 (max. 8388607) + 89 compressed objects within 1 object stream + 0 named destinations out of 1000 (max. 500000) + 109 words of extra memory for PDF output out of 10000 (max. 10000000) + diff --git a/main.pdf b/main.pdf new file mode 100644 index 0000000..aa5ddf7 Binary files /dev/null and b/main.pdf differ diff --git a/main.synctex.gz b/main.synctex.gz new file mode 100644 index 0000000..2ae458c Binary files /dev/null and b/main.synctex.gz differ diff --git a/main.tex b/main.tex new file mode 100644 index 0000000..dbd49d8 --- /dev/null +++ b/main.tex @@ -0,0 +1,45 @@ +\documentclass{dane_proposal_format} +\usepackage{booktabs} % For professional tables +\usepackage{tabularx} % For flexible table columns +\usepackage{multirow} % For multi-row cells +\usepackage{array} % Enhanced table formatting +\usepackage[table]{xcolor} % For colored tables (optional) +\usepackage{pgfgantt} +\usepackage{pdfpages} % For including PDF files + +\begin{document} + +\pagenumbering{roman} +\maketitle +\input{1-goals-and-outcomes/research_statement_v1.tex} +\newpage +\tableofcontents +\newpage +\pagenumbering{arabic} + +\input{1-goals-and-outcomes/v1} +\newpage + +\input{2-state-of-the-art/v1} +\newpage + +\input{3-research-approach/v2} +\newpage + +\input{4-metrics-of-success/v1} +\newpage + +\input{5-risks-and-contingencies/v1} +\newpage + +\input{6-broader-impacts/v1} +\newpage + +\input{8-schedule/v1} +\bibliographystyle{ieeetr} +\bibliography{references} + +% White Paper (optional) +% \input{whitepaper/v1} + +\end{document} diff --git a/main.toc b/main.toc new file mode 100644 index 0000000..a40a59b --- /dev/null +++ b/main.toc @@ -0,0 +1,20 @@ +\contentsline {section}{Contents}{ii}{}% +\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}{3}{}% +\contentsline {subsection}{\numberline {2.3}HARDENS and Formal Methods}{4}{}% +\contentsline {section}{\numberline {3}Research Approach}{6}{}% +\contentsline {subsection}{\numberline {3.1}System Requirement and Specifications}{6}{}% +\contentsline {section}{\numberline {4}Metrics for Success}{7}{}% +\contentsline {paragraph}{TRL 3 \textit {Critical Function and Proof of Concept}}{7}{}% +\contentsline {paragraph}{TRL 4 \textit {Laboratory Testing of Integrated Components}}{7}{}% +\contentsline {paragraph}{TRL 5 \textit {Laboratory Testing in Relevant Environment}}{7}{}% +\contentsline {section}{\numberline {5}Risks and Contingencies}{9}{}% +\contentsline {subsection}{\numberline {5.1}Computational Tractability of Synthesis}{9}{}% +\contentsline {subsection}{\numberline {5.2}Discrete-Continuous Interface Formalization}{9}{}% +\contentsline {subsection}{\numberline {5.3}Procedure Formalization Completeness}{10}{}% +\contentsline {section}{\numberline {6}Broader Impacts}{12}{}% +\contentsline {section}{\numberline {7}Schedule, Milestones, and Deliverables}{14}{}% +\contentsline {subsection}{\numberline {7.1}Milestones and Deliverables}{14}{}% +\contentsline {section}{References}{15}{}% diff --git a/references.bib b/references.bib new file mode 100644 index 0000000..b932bd6 --- /dev/null +++ b/references.bib @@ -0,0 +1,311 @@ +@techreport{NUREG-0899, + title = {Guidelines for the Preparation of Emergency Operating Procedures}, + author = {{U.S. Nuclear Regulatory Commission}}, + institution = {U.S. Nuclear Regulatory Commission}, + year = {1982}, + number = {NUREG-0899} +} + +@misc{10CFR50.34, + title = {{10 CFR Part 50.34}}, + author = {{U.S. Nuclear Regulatory Commission}}, + howpublished = {Code of Federal Regulations}, + urldate = {2025-12-05}, + url = {https://www.nrc.gov/reading-rm/doc-collections/cfr/part050/part050-0034} +} + +@misc{10CFR55.59, + title = {{10 CFR Part 55.59}}, + author = {{U.S. Nuclear Regulatory Commission}}, + howpublished = {Code of Federal Regulations}, + urldate = {2025-12-05}, + url = {https://www.nrc.gov/reading-rm/doc-collections/cfr/part055/part055-0059} +} + +@techreport{WRPS.Description, + title = {{Westinghouse RPS System Description}}, + institution = {Westinghouse Electric Corporation}, + url = {https://nrcoe.inl.gov/publicdocs/SystemStudies/rps-w-description.pdf}, + urldate = {2025-12-05} +} + +@online{gentillon_westinghouse_1999, + title = {Westinghouse Reactor Protection System Unavailability, 1984-1995}, + url = {https://digital.library.unt.edu/ark:/67531/metadc620476/}, + titleaddon = {{PSA} '99, Washington, {DC} ({US}), 08/22/1999--08/25/1999}, + type = {Article}, + author = {Gentillon, C. D. and Marksberry, D. and Rasmuson, D. and Calley, M. B. and Eide, S. A. and Wierman, T.}, + urldate = {2025-12-05}, + date = {1999-08-01}, + note = {Number: {INEEL}/{CON}-99-00374 +Publisher: Idaho National Engineering and Environmental Laboratory}, + file = {Full Text PDF:/home/danesabo/Zotero/storage/7QKWQ8NI/Gentillon et al. - 1999 - Westinghouse Reactor Protection System Unavailability, 1984-1995.pdf:application/pdf}, +} + +@online{operator_statistics, + title = {{Operator Licensing}}, + author = {{U.S. Nuclear Regulatory Commission}}, + howpublished = {\url{https://www.nrc.gov/reactors/operator-licensing}}, + urldate = {2025-11-28}, + file = {Operator Licensing | Nuclear Regulatory Commission:/home/danesabo/Zotero/storage/KUP9B5GH/operator-licensing.html:text/html}, +} + +@misc{10CFR55, + title = {{Part 55—Operators' Licenses}}, + author = {{U.S. Nuclear Regulatory Commission}}, + howpublished = {\url{https://www.nrc.gov/reading-rm/doc-collections/cfr/part055/full-text}}, +} + +@online{10CFR50.54, + title = {{§ 50.54 Conditions of Licenses}}, + author = {{U.S. Nuclear Regulatory Commission}}, + howpublished = {\url{https://www.nrc.gov/reading-rm/doc-collections/cfr/part050/part050-0054}}, + urldate = {2025-11-28}, + file = {§ 50.54 Conditions of licenses. | Nuclear Regulatory Commission:/home/danesabo/Zotero/storage/THTZUD3T/part050-0054.html:text/html}, +} + +@techreport{Kemeny1979, + title = {Report of the President's Commission on the Accident at Three Mile Island}, + author = {Kemeny, John G. and others}, + institution = {President's Commission on the Accident at Three Mile Island}, + year = {1979}, + month = {October} +} + +@misc{WNA2020, + title = {Safety of Nuclear Power Reactors}, + author = {{World Nuclear Association}}, + year = {2020}, + howpublished = {\url{https://www.world-nuclear.org/information-library/safety-and-security/safety-of-plants/safety-of-nuclear-power-reactors.aspx}} +} + +@article{hogberg_root_2013, + title = {Root Causes and Impacts of Severe Accidents at Large Nuclear Power Plants}, + volume = {42}, + issn = {0044-7447}, + url = {https://pmc.ncbi.nlm.nih.gov/articles/PMC3606704/}, + doi = {10.1007/s13280-013-0382-x}, + pages = {267--284}, + number = {3}, + journaltitle = {Ambio}, + shortjournal = {Ambio}, + author = {Högberg, Lars}, + urldate = {2025-12-05}, + date = {2013-04}, + pmid = {23423737}, + pmcid = {PMC3606704}, + file = {Full Text:/home/danesabo/Zotero/storage/E8F2QZGR/Högberg - 2013 - Root Causes and Impacts of Severe Accidents at Large Nuclear Power Plants.pdf:application/pdf}, +} + +@article{zhang_analysis_2025, + title = {Analysis of human errors in nuclear power plant event reports}, + volume = {57}, + issn = {1738-5733}, + url = {https://www.sciencedirect.com/science/article/pii/S1738573325002554}, + doi = {10.1016/j.net.2025.103687}, + pages = {103687}, + number = {10}, + journaltitle = {Nuclear Engineering and Technology}, + shortjournal = {Nuclear Engineering and Technology}, + author = {Zhang, Meihui and Dai, Licao and Chen, Wenming and Pang, Ensheng}, + urldate = {2025-12-05}, + date = {2025-10-01}, + keywords = {Active errors, {HFACS} model, Latent errors, Licensee event reports}, + file = {ScienceDirect Snapshot:/home/danesabo/Zotero/storage/N5R2Z3GL/S1738573325002554.html:text/html}, +} + +@techreport{Kiniry2024, + title = {High Assurance Rigorous Digital Engineering for Nuclear Safety (HARDENS) Final Technical Report}, + author = {Kiniry, Joseph and Bakst, Alexander and Hansen, Simon and Podhradsky, Michal and Bivin, Andrew}, + institution = {Galois, Inc. / U.S. Nuclear Regulatory Commission}, + year = {2024}, + number = {TLR-RES-RES/DE-2024-005}, + note = {NRC Contract 31310021C0014} +} + +@techreport{eia_lcoe_2022, + author = {{U.S. Energy Information Administration}}, + title = {Levelized Costs of New Generation Resources in the Annual Energy Outlook 2022}, + institution = {U.S. Energy Information Administration}, + year = {2022}, + month = {March}, + type = {Report}, + url = {https://www.eia.gov/outlooks/aeo/pdf/electricity_generation.pdf}, + note = {See Table 1b, page 9} +} + +@misc{eesi_datacenter_2024, + author = {{Environmental and Energy Study Institute}}, + title = {Data Center Energy Needs Are Upending Power Grids and Threatening the Climate}, + howpublished = {Web article}, + year = {2024}, + url = {https://www.eesi.org/articles/view/data-center-energy-needs-are-upending-power-grids-and-threatening-the-climate}, + note = {Accessed: 2025-09-29} +} + +@book{baier_principles_2008, + location = {Cambridge, {MA}, {USA}}, + title = {Principles of Model Checking}, + isbn = {978-0-262-02649-9}, + abstract = {A comprehensive introduction to the foundations of model checking, a fully automated technique for finding flaws in hardware and software; with extensive examples and both practical and theoretical exercises.}, + pagetotal = {984}, + publisher = {{MIT} Press}, + author = {Baier, Christel and Katoen, Joost-Pieter}, + date = {2008-04-25}, + langid = {english}, +} + +@inproceedings{katis_capture_2022, + location = {Cham}, + title = {Capture, Analyze, Diagnose: Realizability Checking Of Requirements in {FRET}}, + isbn = {978-3-031-13188-2}, + doi = {10.1007/978-3-031-13188-2_24}, + shorttitle = {Capture, Analyze, Diagnose}, + pages = {490--504}, + booktitle = {Computer Aided Verification}, + publisher = {Springer International Publishing}, + author = {Katis, Andreas and Mavridou, Anastasia and Giannakopoulou, Dimitra and Pressburger, Thomas and Schumann, Johann}, + editor = {Shoham, Sharon and Vizel, Yakir}, + date = {2022}, + langid = {english}, + file = {Full Text PDF:/home/danesabo/Zotero/storage/3JPVH8U2/Katis et al. - 2022 - Capture, Analyze, Diagnose Realizability Checking Of Requirements in FRET.pdf:application/pdf}, +} + +@inproceedings{meyer_strix_2018, + location = {Cham}, + title = {Strix: Explicit Reactive Synthesis Strikes Back!}, + isbn = {978-3-319-96145-3}, + doi = {10.1007/978-3-319-96145-3_31}, + shorttitle = {Strix}, + pages = {578--586}, + booktitle = {Computer Aided Verification}, + publisher = {Springer International Publishing}, + author = {Meyer, Philipp J. and Sickert, Salomon and Luttenberger, Michael}, + editor = {Chockler, Hana and Weissenbacher, Georg}, + date = {2018}, + langid = {english}, +} + +@misc{jacobs_reactive_2024, + title = {The Reactive Synthesis Competition ({SYNTCOMP}): 2018-2021}, + url = {http://arxiv.org/abs/2206.00251}, + doi = {10.48550/arXiv.2206.00251}, + shorttitle = {The Reactive Synthesis Competition ({SYNTCOMP})}, + number = {{arXiv}:2206.00251}, + publisher = {{arXiv}}, + author = {Jacobs, Swen and others}, + urldate = {2025-12-06}, + date = {2024-05-06}, + eprinttype = {arxiv}, + eprint = {2206.00251 [cs]}, + keywords = {Computer Science - Logic in Computer Science}, + file = {Preprint PDF:/home/danesabo/Zotero/storage/GU6W5UH4/Jacobs et al. - 2024 - The Reactive Synthesis Competition (SYNTCOMP) 2018-2021.pdf:application/pdf;Snapshot:/home/danesabo/Zotero/storage/57UPK6A5/2206.html:text/html}, +} + +@article{branicky_multiple_1998, + title = {Multiple Lyapunov functions and other analysis tools for switched and hybrid systems}, + volume = {43}, + issn = {1558-2523}, + url = {https://ieeexplore.ieee.org/document/664150}, + doi = {10.1109/9.664150}, + pages = {475--482}, + number = {4}, + journaltitle = {{IEEE} Transactions on Automatic Control}, + author = {Branicky, M.S.}, + urldate = {2025-09-10}, + date = {1998-04}, + keywords = {Automata, Control systems, Difference equations, Differential equations, Lagrangian functions, Limit-cycles, Lyapunov method, Stability analysis, Switched systems, Switches}, + file = {PDF:/home/danesabo/Zotero/storage/5AQWDPAA/Branicky - 1998 - Multiple Lyapunov functions and other analysis tools for switched and hybrid systems.pdf:application/pdf}, +} + +@thesis{guernic_reachability_2009, + title = {Reachability Analysis of Hybrid Systems with Linear Continuous Dynamics}, + url = {https://theses.hal.science/tel-00422569}, + institution = {Université Joseph-Fourier - Grenoble I}, + type = {phdthesis}, + author = {Guernic, Colas Le}, + urldate = {2025-09-14}, + date = {2009-10-28}, + langid = {english}, + file = {Full Text PDF:/home/danesabo/Zotero/storage/A5XNTDZ9/Guernic - 2009 - Reachability Analysis of Hybrid Systems with Linear Continuous Dynamics.pdf:application/pdf}, +} + +@inproceedings{alur_hybrid_1993, + location = {Berlin, Heidelberg}, + title = {Hybrid automata: An algorithmic approach to the specification and verification of hybrid systems}, + isbn = {978-3-540-48060-0}, + doi = {10.1007/3-540-57318-6_30}, + shorttitle = {Hybrid automata}, + pages = {209--229}, + booktitle = {Hybrid Systems}, + publisher = {Springer}, + author = {Alur, Rajeev and Courcoubetis, Costas and Henzinger, Thomas A. and Ho, Pei -Hsin}, + editor = {Grossman, Robert L. and Nerode, Anil and Ravn, Anders P. and Rischel, Hans}, + date = {1993}, + langid = {english}, + keywords = {Acceptance Condition, Hybrid Automaton, Hybrid System, Mutual Exclusion, Reachability Problem}, + file = {Full Text PDF:/home/danesabo/Zotero/storage/WBXYUC86/Alur et al. - 1993 - Hybrid automata An algorithmic approach to the specification and verification of hybrid systems.pdf:application/pdf}, +} + +@article{mitchell_time-dependent_2005, + title = {A time-dependent Hamilton-Jacobi formulation of reachable sets for continuous dynamic games}, + volume = {50}, + issn = {1558-2523}, + url = {https://ieeexplore.ieee.org/abstract/document/1463302}, + doi = {10.1109/TAC.2005.851439}, + pages = {947--957}, + number = {7}, + journaltitle = {{IEEE} Transactions on Automatic Control}, + author = {Mitchell, I.M. and Bayen, A.M. and Tomlin, C.J.}, + urldate = {2025-09-15}, + date = {2005-07}, + keywords = {Aircraft, Collaborative software, Collision avoidance, Computational modeling, Differential games, Hamilton–Jacobi equations, Nonlinear equations, Nonlinear systems, Partial differential equations, reachability, Trajectory, Vehicle dynamics, verification, Viscosity}, + file = {Snapshot:/home/danesabo/Zotero/storage/SLKV9PEI/1463302.html:text/html;Submitted Version:/home/danesabo/Zotero/storage/9YWL2UDH/Mitchell et al. - 2005 - A time-dependent Hamilton-Jacobi formulation of reachable sets for continuous dynamic games.pdf:application/pdf}, +} + +@inproceedings{frehse_spaceex_2011, + location = {Berlin, Heidelberg}, + title = {{SpaceEx}: Scalable Verification of Hybrid Systems}, + isbn = {978-3-642-22110-1}, + doi = {10.1007/978-3-642-22110-1_30}, + shorttitle = {{SpaceEx}}, + pages = {379--395}, + booktitle = {Computer Aided Verification}, + publisher = {Springer}, + author = {Frehse, Goran and Le Guernic, Colas and Donzé, Alexandre and Cotton, Scott and Ray, Rajarshi and Lebeltel, Olivier and Ripado, Rodolfo and Girard, Antoine and Dang, Thao and Maler, Oded}, + editor = {Gopalakrishnan, Ganesh and Qadeer, Shaz}, + date = {2011}, + langid = {english}, + keywords = {Hybrid Automaton, Hybrid System, Reachability Analysis, Reachable State, Support Function}, + file = {Full Text PDF:/home/danesabo/Zotero/storage/LPQK8GY2/Frehse et al. - 2011 - SpaceEx Scalable Verification of Hybrid Systems.pdf:application/pdf}, +} + +@inproceedings{bansal_hamilton-jacobi_2017, + title = {Hamilton-Jacobi reachability: A brief overview and recent advances}, + url = {https://ieeexplore.ieee.org/abstract/document/8263977}, + doi = {10.1109/CDC.2017.8263977}, + shorttitle = {Hamilton-Jacobi reachability}, + eventtitle = {2017 {IEEE} 56th Annual Conference on Decision and Control ({CDC})}, + pages = {2242--2253}, + booktitle = {2017 {IEEE} 56th Annual Conference on Decision and Control ({CDC})}, + author = {Bansal, Somil and Chen, Mo and Herbert, Sylvia and Tomlin, Claire J.}, + urldate = {2025-09-15}, + date = {2017-12}, + keywords = {Aircraft, Games, Level set, Safety, Tools, Trajectory, Tutorials}, + file = {Snapshot:/home/danesabo/Zotero/storage/EEK5IE93/8263977.html:text/html;Submitted Version:/home/danesabo/Zotero/storage/BMNLZ9DW/Bansal et al. - 2017 - Hamilton-Jacobi reachability A brief overview and recent advances.pdf:application/pdf}, +} + +@inproceedings{prajna_safety_2004, + location = {Berlin, Heidelberg}, + title = {Safety Verification of Hybrid Systems Using Barrier Certificates}, + isbn = {978-3-540-24743-2}, + doi = {10.1007/978-3-540-24743-2_32}, + pages = {477--492}, + booktitle = {Hybrid Systems: Computation and Control}, + publisher = {Springer}, + author = {Prajna, Stephen and Jadbabaie, Ali}, + editor = {Alur, Rajeev and Pappas, George J.}, + date = {2004}, + langid = {english}, + keywords = {Continuous State, Discrete Transition, Hybrid System, Integral Constraint, Reachability Analysis}, +}