diff --git a/.task/backlog.data b/.task/backlog.data index 17b2a33b0..8340767b2 100644 --- a/.task/backlog.data +++ b/.task/backlog.data @@ -44,3 +44,32 @@ {"description":"Research Approach First Draft","entry":"20250916T203815Z","modified":"20250916T203948Z","project":"ERLM","status":"pending","uuid":"c008dbde-ec2a-42f7-a34c-a6038e9d8cd4","tags":["writing"]} {"description":"Write research approach","due":"20250922T040000Z","entry":"20250916T203728Z","modified":"20250916T204121Z","project":"ERLM","status":"pending","uuid":"56c9b3cc-078e-4155-b4cd-f982ae23bd36","tags":["writing"],"depends":["c008dbde-ec2a-42f7-a34c-a6038e9d8cd4","e6cc0b14-6db4-4935-b19f-674c812aeda3"]} {"description":"Research Approach First Draft","entry":"20250916T203815Z","modified":"20250916T204135Z","project":"ERLM","status":"pending","uuid":"c008dbde-ec2a-42f7-a34c-a6038e9d8cd4","tags":["writing"],"depends":["e6cc0b14-6db4-4935-b19f-674c812aeda3"]} +{"description":"The Algorithmic Analysis of Hybrid Systems (1995)","entry":"20250917T160447Z","modified":"20250917T160447Z","project":"thesis","status":"pending","uuid":"b15bdc1a-205f-4489-a8fb-e9843306e40d","tags":["reading"]} +{"description":"Hybrid Automata: An Algorithmic Approach to the Specification and Verification of Hybrid Systems (1993)","entry":"20250917T160447Z","modified":"20250917T160447Z","project":"thesis","status":"pending","uuid":"6ed5ae99-0296-4011-bb90-39d97021d7ae","tags":["reading"]} +{"description":"Hybrid Systems: Review and Recent Progress (2003)","entry":"20250917T160447Z","modified":"20250917T160447Z","project":"thesis","status":"pending","uuid":"1d8043ca-e583-4835-9d77-65e0e92361c3","tags":["reading"]} +{"description":"Hamilton-Jacobi Reachability: A Brief Overview and Recent Advances (2017)","entry":"20250917T160447Z","modified":"20250917T160447Z","project":"thesis","status":"pending","uuid":"b44414db-b0cb-4ed8-9440-1e244f97438e","tags":["reading"]} +{"description":"Multiple Lyapunov Functions and Other Analysis Tools for Switched and Hybrid Systems (1998)","entry":"20250917T160447Z","modified":"20250917T160447Z","project":"thesis","status":"pending","uuid":"99890abe-04ab-4f9f-ab06-cd624071710b","tags":["reading"]} +{"description":"A Benchmark Suite for Hybrid Systems Reachability Analysis (2015)","entry":"20250917T160447Z","modified":"20250917T160447Z","project":"thesis","status":"pending","uuid":"69a98afe-71f0-45d8-9117-5011c553fb8f","tags":["reading"]} +{"description":"Flow*: An Analyzer for Non-linear Hybrid Systems (2013)","entry":"20250917T160447Z","modified":"20250917T160447Z","project":"thesis","status":"pending","uuid":"7f99edb5-4a1c-498b-894b-d2b66e484013","tags":["reading"]} +{"description":"A Complete Uniform Substitution Calculus for Differential Dynamic Logic | Journal of Automated Reasoning (2025)","entry":"20250917T160447Z","modified":"20250917T160447Z","project":"thesis","status":"pending","uuid":"5c8e94df-5d67-4614-bc28-0cf5eeb25175","tags":["reading"]} +{"description":"Robust Satisfaction of Temporal Logic over Real-Valued Signals (2010)","entry":"20250917T160447Z","modified":"20250917T160447Z","project":"thesis","status":"pending","uuid":"d5c545b7-6707-408d-b10d-54d425066de5","tags":["reading"]} +{"description":"SpaceEx: Scalable Verification of Hybrid Systems (2011)","entry":"20250917T160447Z","modified":"20250917T160447Z","project":"thesis","status":"pending","uuid":"477c1b57-2a64-484b-ad8c-14abaaa1fb8a","tags":["reading"]} +{"description":"KeYmaera~X: An Axiomatic Tactical Theorem Prover for Hybrid Systems (2015)","entry":"20250917T160447Z","modified":"20250917T160447Z","project":"thesis","status":"pending","uuid":"2a32c19c-d750-4e80-a3ed-51fec7a9e23f","tags":["reading"]} +{"description":"Stability and Stabilization of Continuous‐Time Switched Linear Systems (2006)","entry":"20250917T160447Z","modified":"20250917T160447Z","project":"thesis","status":"pending","uuid":"0d2797f6-63b6-41fb-b3de-5bc0cee27581","tags":["reading"]} +{"description":"Reachability Analysis of Hybrid Systems with Linear Continuous Dynamics (2009)","entry":"20250917T160447Z","modified":"20250917T160447Z","project":"thesis","status":"pending","uuid":"9e8cf332-f912-47da-abc6-89d01ddc1a92","tags":["reading"]} +{"description":"Supervisory Control of Hybrid Systems (2000)","entry":"20250917T160447Z","modified":"20250917T160447Z","project":"thesis","status":"pending","uuid":"613e4861-4cb0-4f5e-b930-41bec966b527","tags":["reading"]} +{"description":"Uppaal in a Nutshell (1997)","entry":"20250917T160447Z","modified":"20250917T160447Z","project":"thesis","status":"pending","uuid":"352739b9-a590-4399-8d8f-6240d5428479","tags":["reading"]} +{"description":"Switching in Systems and Control (2003)","entry":"20250917T160447Z","modified":"20250917T160447Z","project":"thesis","status":"pending","uuid":"e802f098-4639-45fb-8ea9-50052a2b3fe1","tags":["reading"]} +{"description":"Stability and Stabilizability of Switched Linear Systems: A Survey of Recent Results (2009)","entry":"20250917T160447Z","modified":"20250917T160447Z","project":"thesis","status":"pending","uuid":"e8183445-b696-4422-9b27-56ae3a82107f","tags":["reading"]} +{"description":"Capturing and Analyzing Requirements with FRET (2025)","entry":"20250917T160447Z","modified":"20250917T160447Z","project":"thesis","status":"pending","uuid":"ab74a0c5-3f93-497c-89ca-6bafb4a89507","tags":["reading"]} +{"description":"A Time-Dependent Hamilton-Jacobi Formulation of Reachable Sets for Continuous Dynamic Games (2005)","entry":"20250917T160447Z","modified":"20250917T160447Z","project":"thesis","status":"pending","uuid":"2eed0362-2b81-4378-a9f0-071ed62b8775","tags":["reading"]} +{"description":"Differential Dynamic Logic for Hybrid Systems (2008)","entry":"20250917T160447Z","modified":"20250917T160447Z","project":"thesis","status":"pending","uuid":"e05d336d-6174-4d5d-8c0c-868169c27e34","tags":["reading"]} +{"description":"Formal Verification of Avionics Software Products (2009)","entry":"20250917T160447Z","modified":"20250917T160447Z","project":"thesis","status":"pending","uuid":"3917b086-0c60-4044-b279-c6386878feb6","tags":["reading"]} +{"description":"Opportunities and Challenges for Remote Microreactor Operations (2023)","entry":"20250917T160447Z","modified":"20250917T160447Z","project":"thesis","status":"pending","uuid":"2febb36a-fe32-44f7-8eea-16683edfc6c0","tags":["reading"]} +{"description":"Switching Controller Synthesis for~Hybrid Systems Against STL Formulas (2025)","entry":"20250917T160447Z","modified":"20250917T160447Z","project":"thesis","status":"pending","uuid":"d45bc182-d7f3-4ab1-b654-852884f2b11c","tags":["reading"]} +{"description":"Learning Local Control Barrier Functions for Hybrid Systems (2024)","entry":"20250917T160447Z","modified":"20250917T160447Z","project":"thesis","status":"pending","uuid":"3abf4246-566a-4ba8-b392-cbab5d7a9aa0","tags":["reading"]} +{"description":"Model Predictive Control of Stochastic Hybrid Systems with Signal Temporal Logic Constraints (2025)","entry":"20250917T160447Z","modified":"20250917T160447Z","project":"thesis","status":"pending","uuid":"320ec48e-134f-462f-ac3c-ffaf70698691","tags":["reading"]} +{"description":"Online Control Synthesis for Uncertain Systems under Signal Temporal Logic Specifications (2024)","entry":"20250917T160447Z","modified":"20250917T160447Z","project":"thesis","status":"pending","uuid":"b47de464-8a66-45d2-b487-6588a60c8112","tags":["reading"]} +{"description":"Read Opportunities, Challenges, and Research Needs for Remote Microreactor Operations","entry":"20250910T150523Z","modified":"20250917T160629Z","project":"thesis","status":"pending","uuid":"96c76e6b-5c33-4f54-a156-5c59e718f01a","tags":["reading"]} +{"description":"Read Branicky Lyapunov paper","end":"20250911T214953Z","entry":"20250911T183429Z","modified":"20250917T160655Z","project":"thesis","status":"completed","uuid":"f4d32147-ec74-4f68-b8d5-146c0b6f35df","tags":["reading"]} +{"description":"Research Approach Outline","end":"20250917T203802Z","entry":"20250916T203752Z","modified":"20250917T203802Z","project":"ERLM","status":"completed","uuid":"e6cc0b14-6db4-4935-b19f-674c812aeda3","tags":["writing"]} diff --git a/.task/completed.data b/.task/completed.data index 13e718fff..9f18b243a 100644 --- a/.task/completed.data +++ b/.task/completed.data @@ -1,5 +1,6 @@ +[description:"Research Approach Outline" end:"1758141482" entry:"1758055072" modified:"1758141482" project:"ERLM" status:"completed" tags:"writing" tags_writing:"x" uuid:"e6cc0b14-6db4-4935-b19f-674c812aeda3"] [dep_8e7a8e19-9197-4008-b7d9-521ffcf7ba91:"x" dep_96c76e6b-5c33-4f54-a156-5c59e718f01a:"x" dep_f4d32147-ec74-4f68-b8d5-146c0b6f35df:"x" depends:"8e7a8e19-9197-4008-b7d9-521ffcf7ba91,96c76e6b-5c33-4f54-a156-5c59e718f01a,f4d32147-ec74-4f68-b8d5-146c0b6f35df" description:"Write first draft of state of the art" due:"1757649600" end:"1758040405" entry:"1757449978" modified:"1758040405" project:"ERLM" status:"completed" tags:"writing" tags_writing:"x" uuid:"4bec1530-18bc-43cb-9f0b-61e35dbf1730"] -[description:"Read Branicky Lyapunov paper" end:"1757627393" entry:"1757615669" modified:"1757627393" project:"Thesis" status:"completed" tags:"reading" tags_reading:"x" uuid:"f4d32147-ec74-4f68-b8d5-146c0b6f35df"] +[description:"Read Branicky Lyapunov paper" end:"1757627393" entry:"1757615669" modified:"1758125215" project:"thesis" status:"completed" tags:"reading" tags_reading:"x" uuid:"f4d32147-ec74-4f68-b8d5-146c0b6f35df"] [description:"Follow up with Daniel about controls bootcamp" due:"1757563200" end:"1757618582" entry:"1757449130" modified:"1757618582" project:"FSAE" status:"completed" uuid:"3eaadead-4e5e-4823-9077-16d6e1800862"] [description:"Follow up with Bajaj about writing TurboSAR paper" due:"1757563200" end:"1757618582" entry:"1757449286" modified:"1757618583" priority:"L" status:"completed" uuid:"fa2699f9-0082-433e-ae0d-cc2553db9865"] [description:"Write outline for state of the art" due:"1757476800" end:"1757516746" entry:"1757443175" modified:"1757516746" project:"ERLM" status:"completed" uuid:"8e7a8e19-9197-4008-b7d9-521ffcf7ba91"] diff --git a/.task/pending.data b/.task/pending.data index 226e1ebf4..c074dc860 100644 --- a/.task/pending.data +++ b/.task/pending.data @@ -3,8 +3,33 @@ [description:"Look over obsidian tasks and see if anything is worth moving over" entry:"1757443262" modified:"1757443262" status:"pending" tags:"taskwarrior" tags_taskwarrior:"x" uuid:"c1a5390d-5b84-4f9c-8acb-ffb970682660"] [description:"Look around for summer internships with national labs" entry:"1757449731" modified:"1757449731" status:"pending" uuid:"d3f3dc53-4feb-4b7e-8de5-86ebf3c535d5"] [description:"get FSAE COM and track data to Matt barry for statics problem. He also wants a cad model?" due:"1758254400" entry:"1757515988" modified:"1757515988" status:"pending" uuid:"48f997bf-b686-4c0b-bee5-ac8e5f874ad9"] -[description:"Read Opportunities, Challenges, and Research Needs for Remote Microreactor Operations" entry:"1757516723" modified:"1757516723" project:"Thesis" status:"pending" tags:"reading" tags_reading:"x" uuid:"96c76e6b-5c33-4f54-a156-5c59e718f01a"] +[description:"Read Opportunities, Challenges, and Research Needs for Remote Microreactor Operations" entry:"1757516723" modified:"1758125189" project:"thesis" status:"pending" tags:"reading" tags_reading:"x" uuid:"96c76e6b-5c33-4f54-a156-5c59e718f01a"] [description:"Write zettel about lipschitz continuity" entry:"1757625029" modified:"1757625029" status:"pending" tags:"zk" tags_zk:"x" uuid:"b7f68988-8c06-4d18-bf77-91d7e39fd55f"] [dep_c008dbde-ec2a-42f7-a34c-a6038e9d8cd4:"x" dep_e6cc0b14-6db4-4935-b19f-674c812aeda3:"x" depends:"c008dbde-ec2a-42f7-a34c-a6038e9d8cd4,e6cc0b14-6db4-4935-b19f-674c812aeda3" description:"Write research approach" due:"1758513600" entry:"1758055048" modified:"1758055281" project:"ERLM" status:"pending" tags:"writing" tags_writing:"x" uuid:"56c9b3cc-078e-4155-b4cd-f982ae23bd36"] -[description:"Research Approach Outline" entry:"1758055072" modified:"1758055144" project:"ERLM" status:"pending" tags:"writing" tags_writing:"x" uuid:"e6cc0b14-6db4-4935-b19f-674c812aeda3"] [dep_e6cc0b14-6db4-4935-b19f-674c812aeda3:"x" depends:"e6cc0b14-6db4-4935-b19f-674c812aeda3" description:"Research Approach First Draft" entry:"1758055095" modified:"1758055295" project:"ERLM" status:"pending" tags:"writing" tags_writing:"x" uuid:"c008dbde-ec2a-42f7-a34c-a6038e9d8cd4"] +[description:"The Algorithmic Analysis of Hybrid Systems (1995)" entry:"1758125087" modified:"1758125087" project:"thesis" status:"pending" tags:"reading" tags_reading:"x" uuid:"b15bdc1a-205f-4489-a8fb-e9843306e40d"] +[description:"Hybrid Automata: An Algorithmic Approach to the Specification and Verification of Hybrid Systems (1993)" entry:"1758125087" modified:"1758125087" project:"thesis" status:"pending" tags:"reading" tags_reading:"x" uuid:"6ed5ae99-0296-4011-bb90-39d97021d7ae"] +[description:"Hybrid Systems: Review and Recent Progress (2003)" entry:"1758125087" modified:"1758125087" project:"thesis" status:"pending" tags:"reading" tags_reading:"x" uuid:"1d8043ca-e583-4835-9d77-65e0e92361c3"] +[description:"Hamilton-Jacobi Reachability: A Brief Overview and Recent Advances (2017)" entry:"1758125087" modified:"1758125087" project:"thesis" status:"pending" tags:"reading" tags_reading:"x" uuid:"b44414db-b0cb-4ed8-9440-1e244f97438e"] +[description:"Multiple Lyapunov Functions and Other Analysis Tools for Switched and Hybrid Systems (1998)" entry:"1758125087" modified:"1758125087" project:"thesis" status:"pending" tags:"reading" tags_reading:"x" uuid:"99890abe-04ab-4f9f-ab06-cd624071710b"] +[description:"A Benchmark Suite for Hybrid Systems Reachability Analysis (2015)" entry:"1758125087" modified:"1758125087" project:"thesis" status:"pending" tags:"reading" tags_reading:"x" uuid:"69a98afe-71f0-45d8-9117-5011c553fb8f"] +[description:"Flow*: An Analyzer for Non-linear Hybrid Systems (2013)" entry:"1758125087" modified:"1758125087" project:"thesis" status:"pending" tags:"reading" tags_reading:"x" uuid:"7f99edb5-4a1c-498b-894b-d2b66e484013"] +[description:"A Complete Uniform Substitution Calculus for Differential Dynamic Logic | Journal of Automated Reasoning (2025)" entry:"1758125087" modified:"1758125087" project:"thesis" status:"pending" tags:"reading" tags_reading:"x" uuid:"5c8e94df-5d67-4614-bc28-0cf5eeb25175"] +[description:"Robust Satisfaction of Temporal Logic over Real-Valued Signals (2010)" entry:"1758125087" modified:"1758125087" project:"thesis" status:"pending" tags:"reading" tags_reading:"x" uuid:"d5c545b7-6707-408d-b10d-54d425066de5"] +[description:"SpaceEx: Scalable Verification of Hybrid Systems (2011)" entry:"1758125087" modified:"1758125087" project:"thesis" status:"pending" tags:"reading" tags_reading:"x" uuid:"477c1b57-2a64-484b-ad8c-14abaaa1fb8a"] +[description:"KeYmaera~X: An Axiomatic Tactical Theorem Prover for Hybrid Systems (2015)" entry:"1758125087" modified:"1758125087" project:"thesis" status:"pending" tags:"reading" tags_reading:"x" uuid:"2a32c19c-d750-4e80-a3ed-51fec7a9e23f"] +[description:"Stability and Stabilization of Continuous‐Time Switched Linear Systems (2006)" entry:"1758125087" modified:"1758125087" project:"thesis" status:"pending" tags:"reading" tags_reading:"x" uuid:"0d2797f6-63b6-41fb-b3de-5bc0cee27581"] +[description:"Reachability Analysis of Hybrid Systems with Linear Continuous Dynamics (2009)" entry:"1758125087" modified:"1758125087" project:"thesis" status:"pending" tags:"reading" tags_reading:"x" uuid:"9e8cf332-f912-47da-abc6-89d01ddc1a92"] +[description:"Supervisory Control of Hybrid Systems (2000)" entry:"1758125087" modified:"1758125087" project:"thesis" status:"pending" tags:"reading" tags_reading:"x" uuid:"613e4861-4cb0-4f5e-b930-41bec966b527"] +[description:"Uppaal in a Nutshell (1997)" entry:"1758125087" modified:"1758125087" project:"thesis" status:"pending" tags:"reading" tags_reading:"x" uuid:"352739b9-a590-4399-8d8f-6240d5428479"] +[description:"Switching in Systems and Control (2003)" entry:"1758125087" modified:"1758125087" project:"thesis" status:"pending" tags:"reading" tags_reading:"x" uuid:"e802f098-4639-45fb-8ea9-50052a2b3fe1"] +[description:"Stability and Stabilizability of Switched Linear Systems: A Survey of Recent Results (2009)" entry:"1758125087" modified:"1758125087" project:"thesis" status:"pending" tags:"reading" tags_reading:"x" uuid:"e8183445-b696-4422-9b27-56ae3a82107f"] +[description:"Capturing and Analyzing Requirements with FRET (2025)" entry:"1758125087" modified:"1758125087" project:"thesis" status:"pending" tags:"reading" tags_reading:"x" uuid:"ab74a0c5-3f93-497c-89ca-6bafb4a89507"] +[description:"A Time-Dependent Hamilton-Jacobi Formulation of Reachable Sets for Continuous Dynamic Games (2005)" entry:"1758125087" modified:"1758125087" project:"thesis" status:"pending" tags:"reading" tags_reading:"x" uuid:"2eed0362-2b81-4378-a9f0-071ed62b8775"] +[description:"Differential Dynamic Logic for Hybrid Systems (2008)" entry:"1758125087" modified:"1758125087" project:"thesis" status:"pending" tags:"reading" tags_reading:"x" uuid:"e05d336d-6174-4d5d-8c0c-868169c27e34"] +[description:"Formal Verification of Avionics Software Products (2009)" entry:"1758125087" modified:"1758125087" project:"thesis" status:"pending" tags:"reading" tags_reading:"x" uuid:"3917b086-0c60-4044-b279-c6386878feb6"] +[description:"Opportunities and Challenges for Remote Microreactor Operations (2023)" entry:"1758125087" modified:"1758125087" project:"thesis" status:"pending" tags:"reading" tags_reading:"x" uuid:"2febb36a-fe32-44f7-8eea-16683edfc6c0"] +[description:"Switching Controller Synthesis for~Hybrid Systems Against STL Formulas (2025)" entry:"1758125087" modified:"1758125087" project:"thesis" status:"pending" tags:"reading" tags_reading:"x" uuid:"d45bc182-d7f3-4ab1-b654-852884f2b11c"] +[description:"Learning Local Control Barrier Functions for Hybrid Systems (2024)" entry:"1758125087" modified:"1758125087" project:"thesis" status:"pending" tags:"reading" tags_reading:"x" uuid:"3abf4246-566a-4ba8-b392-cbab5d7a9aa0"] +[description:"Model Predictive Control of Stochastic Hybrid Systems with Signal Temporal Logic Constraints (2025)" entry:"1758125087" modified:"1758125087" project:"thesis" status:"pending" tags:"reading" tags_reading:"x" uuid:"320ec48e-134f-462f-ac3c-ffaf70698691"] +[description:"Online Control Synthesis for Uncertain Systems under Signal Temporal Logic Specifications (2024)" entry:"1758125087" modified:"1758125087" project:"thesis" status:"pending" tags:"reading" tags_reading:"x" uuid:"b47de464-8a66-45d2-b487-6588a60c8112"] diff --git a/.task/undo.data b/.task/undo.data index ea60b065f..c09400e32 100644 --- a/.task/undo.data +++ b/.task/undo.data @@ -157,3 +157,93 @@ time 1758055295 old [description:"Research Approach First Draft" entry:"1758055095" modified:"1758055188" project:"ERLM" status:"pending" tags:"writing" tags_writing:"x" uuid:"c008dbde-ec2a-42f7-a34c-a6038e9d8cd4"] new [dep_e6cc0b14-6db4-4935-b19f-674c812aeda3:"x" depends:"e6cc0b14-6db4-4935-b19f-674c812aeda3" description:"Research Approach First Draft" entry:"1758055095" modified:"1758055295" project:"ERLM" status:"pending" tags:"writing" tags_writing:"x" uuid:"c008dbde-ec2a-42f7-a34c-a6038e9d8cd4"] --- +time 1758125087 +new [description:"The Algorithmic Analysis of Hybrid Systems (1995)" entry:"1758125087" modified:"1758125087" project:"thesis" status:"pending" tags:"reading" tags_reading:"x" uuid:"b15bdc1a-205f-4489-a8fb-e9843306e40d"] +--- +time 1758125087 +new [description:"Hybrid Automata: An Algorithmic Approach to the Specification and Verification of Hybrid Systems (1993)" entry:"1758125087" modified:"1758125087" project:"thesis" status:"pending" tags:"reading" tags_reading:"x" uuid:"6ed5ae99-0296-4011-bb90-39d97021d7ae"] +--- +time 1758125087 +new [description:"Hybrid Systems: Review and Recent Progress (2003)" entry:"1758125087" modified:"1758125087" project:"thesis" status:"pending" tags:"reading" tags_reading:"x" uuid:"1d8043ca-e583-4835-9d77-65e0e92361c3"] +--- +time 1758125087 +new [description:"Hamilton-Jacobi Reachability: A Brief Overview and Recent Advances (2017)" entry:"1758125087" modified:"1758125087" project:"thesis" status:"pending" tags:"reading" tags_reading:"x" uuid:"b44414db-b0cb-4ed8-9440-1e244f97438e"] +--- +time 1758125087 +new [description:"Multiple Lyapunov Functions and Other Analysis Tools for Switched and Hybrid Systems (1998)" entry:"1758125087" modified:"1758125087" project:"thesis" status:"pending" tags:"reading" tags_reading:"x" uuid:"99890abe-04ab-4f9f-ab06-cd624071710b"] +--- +time 1758125087 +new [description:"A Benchmark Suite for Hybrid Systems Reachability Analysis (2015)" entry:"1758125087" modified:"1758125087" project:"thesis" status:"pending" tags:"reading" tags_reading:"x" uuid:"69a98afe-71f0-45d8-9117-5011c553fb8f"] +--- +time 1758125087 +new [description:"Flow*: An Analyzer for Non-linear Hybrid Systems (2013)" entry:"1758125087" modified:"1758125087" project:"thesis" status:"pending" tags:"reading" tags_reading:"x" uuid:"7f99edb5-4a1c-498b-894b-d2b66e484013"] +--- +time 1758125087 +new [description:"A Complete Uniform Substitution Calculus for Differential Dynamic Logic | Journal of Automated Reasoning (2025)" entry:"1758125087" modified:"1758125087" project:"thesis" status:"pending" tags:"reading" tags_reading:"x" uuid:"5c8e94df-5d67-4614-bc28-0cf5eeb25175"] +--- +time 1758125087 +new [description:"Robust Satisfaction of Temporal Logic over Real-Valued Signals (2010)" entry:"1758125087" modified:"1758125087" project:"thesis" status:"pending" tags:"reading" tags_reading:"x" uuid:"d5c545b7-6707-408d-b10d-54d425066de5"] +--- +time 1758125087 +new [description:"SpaceEx: Scalable Verification of Hybrid Systems (2011)" entry:"1758125087" modified:"1758125087" project:"thesis" status:"pending" tags:"reading" tags_reading:"x" uuid:"477c1b57-2a64-484b-ad8c-14abaaa1fb8a"] +--- +time 1758125087 +new [description:"KeYmaera~X: An Axiomatic Tactical Theorem Prover for Hybrid Systems (2015)" entry:"1758125087" modified:"1758125087" project:"thesis" status:"pending" tags:"reading" tags_reading:"x" uuid:"2a32c19c-d750-4e80-a3ed-51fec7a9e23f"] +--- +time 1758125087 +new [description:"Stability and Stabilization of Continuous‐Time Switched Linear Systems (2006)" entry:"1758125087" modified:"1758125087" project:"thesis" status:"pending" tags:"reading" tags_reading:"x" uuid:"0d2797f6-63b6-41fb-b3de-5bc0cee27581"] +--- +time 1758125087 +new [description:"Reachability Analysis of Hybrid Systems with Linear Continuous Dynamics (2009)" entry:"1758125087" modified:"1758125087" project:"thesis" status:"pending" tags:"reading" tags_reading:"x" uuid:"9e8cf332-f912-47da-abc6-89d01ddc1a92"] +--- +time 1758125087 +new [description:"Supervisory Control of Hybrid Systems (2000)" entry:"1758125087" modified:"1758125087" project:"thesis" status:"pending" tags:"reading" tags_reading:"x" uuid:"613e4861-4cb0-4f5e-b930-41bec966b527"] +--- +time 1758125087 +new [description:"Uppaal in a Nutshell (1997)" entry:"1758125087" modified:"1758125087" project:"thesis" status:"pending" tags:"reading" tags_reading:"x" uuid:"352739b9-a590-4399-8d8f-6240d5428479"] +--- +time 1758125087 +new [description:"Switching in Systems and Control (2003)" entry:"1758125087" modified:"1758125087" project:"thesis" status:"pending" tags:"reading" tags_reading:"x" uuid:"e802f098-4639-45fb-8ea9-50052a2b3fe1"] +--- +time 1758125087 +new [description:"Stability and Stabilizability of Switched Linear Systems: A Survey of Recent Results (2009)" entry:"1758125087" modified:"1758125087" project:"thesis" status:"pending" tags:"reading" tags_reading:"x" uuid:"e8183445-b696-4422-9b27-56ae3a82107f"] +--- +time 1758125087 +new [description:"Capturing and Analyzing Requirements with FRET (2025)" entry:"1758125087" modified:"1758125087" project:"thesis" status:"pending" tags:"reading" tags_reading:"x" uuid:"ab74a0c5-3f93-497c-89ca-6bafb4a89507"] +--- +time 1758125087 +new [description:"A Time-Dependent Hamilton-Jacobi Formulation of Reachable Sets for Continuous Dynamic Games (2005)" entry:"1758125087" modified:"1758125087" project:"thesis" status:"pending" tags:"reading" tags_reading:"x" uuid:"2eed0362-2b81-4378-a9f0-071ed62b8775"] +--- +time 1758125087 +new [description:"Differential Dynamic Logic for Hybrid Systems (2008)" entry:"1758125087" modified:"1758125087" project:"thesis" status:"pending" tags:"reading" tags_reading:"x" uuid:"e05d336d-6174-4d5d-8c0c-868169c27e34"] +--- +time 1758125087 +new [description:"Formal Verification of Avionics Software Products (2009)" entry:"1758125087" modified:"1758125087" project:"thesis" status:"pending" tags:"reading" tags_reading:"x" uuid:"3917b086-0c60-4044-b279-c6386878feb6"] +--- +time 1758125087 +new [description:"Opportunities and Challenges for Remote Microreactor Operations (2023)" entry:"1758125087" modified:"1758125087" project:"thesis" status:"pending" tags:"reading" tags_reading:"x" uuid:"2febb36a-fe32-44f7-8eea-16683edfc6c0"] +--- +time 1758125087 +new [description:"Switching Controller Synthesis for~Hybrid Systems Against STL Formulas (2025)" entry:"1758125087" modified:"1758125087" project:"thesis" status:"pending" tags:"reading" tags_reading:"x" uuid:"d45bc182-d7f3-4ab1-b654-852884f2b11c"] +--- +time 1758125087 +new [description:"Learning Local Control Barrier Functions for Hybrid Systems (2024)" entry:"1758125087" modified:"1758125087" project:"thesis" status:"pending" tags:"reading" tags_reading:"x" uuid:"3abf4246-566a-4ba8-b392-cbab5d7a9aa0"] +--- +time 1758125087 +new [description:"Model Predictive Control of Stochastic Hybrid Systems with Signal Temporal Logic Constraints (2025)" entry:"1758125087" modified:"1758125087" project:"thesis" status:"pending" tags:"reading" tags_reading:"x" uuid:"320ec48e-134f-462f-ac3c-ffaf70698691"] +--- +time 1758125087 +new [description:"Online Control Synthesis for Uncertain Systems under Signal Temporal Logic Specifications (2024)" entry:"1758125087" modified:"1758125087" project:"thesis" status:"pending" tags:"reading" tags_reading:"x" uuid:"b47de464-8a66-45d2-b487-6588a60c8112"] +--- +time 1758125189 +old [description:"Read Opportunities, Challenges, and Research Needs for Remote Microreactor Operations" entry:"1757516723" modified:"1757516723" project:"Thesis" status:"pending" tags:"reading" tags_reading:"x" uuid:"96c76e6b-5c33-4f54-a156-5c59e718f01a"] +new [description:"Read Opportunities, Challenges, and Research Needs for Remote Microreactor Operations" entry:"1757516723" modified:"1758125189" project:"thesis" status:"pending" tags:"reading" tags_reading:"x" uuid:"96c76e6b-5c33-4f54-a156-5c59e718f01a"] +--- +time 1758125215 +old [description:"Read Branicky Lyapunov paper" end:"1757627393" entry:"1757615669" modified:"1757627393" project:"Thesis" status:"completed" tags:"reading" tags_reading:"x" uuid:"f4d32147-ec74-4f68-b8d5-146c0b6f35df"] +new [description:"Read Branicky Lyapunov paper" end:"1757627393" entry:"1757615669" modified:"1758125215" project:"thesis" status:"completed" tags:"reading" tags_reading:"x" uuid:"f4d32147-ec74-4f68-b8d5-146c0b6f35df"] +--- +time 1758141482 +old [description:"Research Approach Outline" entry:"1758055072" modified:"1758055144" project:"ERLM" status:"pending" tags:"writing" tags_writing:"x" uuid:"e6cc0b14-6db4-4935-b19f-674c812aeda3"] +new [description:"Research Approach Outline" end:"1758141482" entry:"1758055072" modified:"1758141482" project:"ERLM" status:"completed" tags:"writing" tags_writing:"x" uuid:"e6cc0b14-6db4-4935-b19f-674c812aeda3"] +--- diff --git a/Writing/ERLM/main.aux b/Writing/ERLM/main.aux index c7806d68c..9bc64ba51 100644 --- a/Writing/ERLM/main.aux +++ b/Writing/ERLM/main.aux @@ -15,6 +15,9 @@ \@writefile{toc}{\contentsline {subsection}{\numberline {2.2}Formal Methods and Reactive Synthesis}{5}{}\protected@file@percent } \citation{platzer2008differential,platzer2017complete} \citation{fulton2015keymaera} +\@writefile{toc}{\contentsline {section}{\numberline {3}Research Approach}{7}{}\protected@file@percent } +\@writefile{toc}{\contentsline {subsection}{\numberline {3.1}\((Procedures \wedge FRET) \rightarrow Temporal Specifications\)}{7}{}\protected@file@percent } +\@writefile{toc}{\contentsline {subsection}{\numberline {3.2}\((TemporalLogic \wedge ReactiveSynthesis) \rightarrow DiscreteAutomata\) }{8}{}\protected@file@percent } \bibdata{references} \bibcite{geromel2006stability}{1} \bibcite{branicky1998multiple}{2} @@ -29,5 +32,5 @@ \bibcite{platzer2008differential}{11} \bibcite{platzer2017complete}{12} \bibcite{fulton2015keymaera}{13} -\@writefile{toc}{\contentsline {section}{References}{7}{}\protected@file@percent } -\gdef \@abspage@last{8} +\@writefile{toc}{\contentsline {section}{References}{9}{}\protected@file@percent } +\gdef \@abspage@last{10} diff --git a/Writing/ERLM/main.fdb_latexmk b/Writing/ERLM/main.fdb_latexmk index 0443a65b4..3bdd03913 100644 --- a/Writing/ERLM/main.fdb_latexmk +++ b/Writing/ERLM/main.fdb_latexmk @@ -1,14 +1,14 @@ # Fdb version 4 -["bibtex main"] 1757950472.75375 "main.aux" "main.bbl" "main" 1757950513.81669 0 - "./references.bib" 1757949790.55852 9415 fb740c67337f78e30e95f745a7cf3dae "" +["bibtex main"] 1758312160.31587 "main.aux" "main.bbl" "main" 1758313994.24344 0 + "./references.bib" 1757962977.69814 9415 fb740c67337f78e30e95f745a7cf3dae "" "/usr/share/texlive/texmf-dist/bibtex/bst/base/unsrt.bst" 1292289607 18030 1376b4b231b50c66211e47e42eda2875 "" - "main.aux" 1757950513.73578 1476 7b620cba913c1c5dec4a8772dfd69ad8 "pdflatex" + "main.aux" 1758313994.11955 1906 b2985f48fe3452882877d4466e7ee0d0 "pdflatex" (generated) "main.bbl" "main.blg" (rewritten before read) -["pdflatex"] 1757950513.33498 "main.tex" "main.pdf" "main" 1757950513.81684 0 - "/etc/texmf/web2c/texmf.cnf" 1726065852.27662 475 c0e671620eb5563b2130f56340a5fde8 "" +["pdflatex"] 1758313993.41574 "main.tex" "main.pdf" "main" 1758313994.24379 0 + "/etc/texmf/web2c/texmf.cnf" 1722610814.59577 475 c0e671620eb5563b2130f56340a5fde8 "" "/usr/share/texlive/texmf-dist/fonts/enc/dvips/base/8r.enc" 1165713224 4850 80dc9bab7f31fb78a000ccfed0e27cab "" "/usr/share/texlive/texmf-dist/fonts/map/fontname/texfonts.map" 1577235249 3524 cb3e574dea2d1052e39280babc910dc8 "" "/usr/share/texlive/texmf-dist/fonts/tfm/adobe/symbol/psyr.tfm" 1136768653 1408 5937f58aa508ea2cea4901c07d10f5fe "" @@ -231,15 +231,16 @@ "/usr/share/texlive/texmf-dist/tex/latex/xkeyval/xkeyval.sty" 1655411236 4937 4ce600ce9bd4ec84d0250eb6892fcf4f "" "/usr/share/texlive/texmf-dist/web2c/texmf.cnf" 1707919699 40399 f2c302f7d2af602abb742093540a5834 "" "/usr/share/texmf/web2c/texmf.cnf" 1707919699 40399 f2c302f7d2af602abb742093540a5834 "" - "/var/lib/texmf/fonts/map/pdftex/updmap/pdftex.map" 1726065856.46263 128028 f533b797fba58d231669ea19e894e23e "" - "/var/lib/texmf/web2c/pdftex/pdflatex.fmt" 1726065868 6800790 607442c924ed54405961d2b8ac2a25ae "" - "dane_proposal_format.cls" 1757942776.53402 2553 3bbf169a90a50515ed103fe388c111f0 "" - "goals-and-outcomes/v4.tex" 1757864250.3119 5764 a67e489f9ea8343564010d217ae37ec2 "" - "main.aux" 1757950513.73578 1476 7b620cba913c1c5dec4a8772dfd69ad8 "pdflatex" - "main.bbl" 1757950472.76375 3170 7f578afdcd1e73f308616474dc5a4003 "bibtex main" - "main.tex" 1757950471.85075 228 b8ce7b699dae6f4898d522c9ecfeff34 "" - "sabo-quad-chart.pdf" 1757950359.77272 133742 e107b1b92665ad28257256b818191f52 "" - "state-of-the-art/v2.tex" 1757950266.45116 10918 a65147e24336b6a318bf18223339313e "" + "/var/lib/texmf/fonts/map/pdftex/updmap/pdftex.map" 1722610820.43889 128028 f533b797fba58d231669ea19e894e23e "" + "/var/lib/texmf/web2c/pdftex/pdflatex.fmt" 1726005817 6800784 2b63e5a224c5ad740802d8f9921962c1 "" + "dane_proposal_format.cls" 1757904657.11823 2553 3bbf169a90a50515ed103fe388c111f0 "" + "goals-and-outcomes/v4.tex" 1757896122.20856 5764 a67e489f9ea8343564010d217ae37ec2 "" + "main.aux" 1758313994.11955 1906 b2985f48fe3452882877d4466e7ee0d0 "pdflatex" + "main.bbl" 1758312160.33144 3170 7f578afdcd1e73f308616474dc5a4003 "bibtex main" + "main.tex" 1758141512.11022 266 5fc203b73100922882e1cd826c363466 "" + "research-approach/v1.tex" 1758313992.54153 4328 61e2e0bafe86777bddb01aaa872e5430 "" + "sabo-quad-chart.pdf" 1757962977.69814 133742 e107b1b92665ad28257256b818191f52 "" + "state-of-the-art/v2.tex" 1757962977.69875 10918 a65147e24336b6a318bf18223339313e "" (generated) "main.aux" "main.log" diff --git a/Writing/ERLM/main.fls b/Writing/ERLM/main.fls index c0e63767a..4b3cc9a31 100644 --- a/Writing/ERLM/main.fls +++ b/Writing/ERLM/main.fls @@ -475,6 +475,11 @@ INPUT /usr/share/texlive/texmf-dist/tex/latex/psnfss/ts1ptm.fd INPUT /usr/share/texlive/texmf-dist/tex/latex/psnfss/ts1ptm.fd INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmr8c.tfm INPUT /usr/share/texlive/texmf-dist/fonts/vf/adobe/times/ptmr8c.vf +INPUT ./research-approach/v1.tex +INPUT ./research-approach/v1.tex +INPUT ./research-approach/v1.tex +INPUT ./research-approach/v1.tex +INPUT research-approach/v1.tex INPUT ./main.bbl INPUT ./main.bbl INPUT main.bbl diff --git a/Writing/ERLM/main.log b/Writing/ERLM/main.log index 4b4f3db04..36addc706 100644 --- a/Writing/ERLM/main.log +++ b/Writing/ERLM/main.log @@ -1,4 +1,4 @@ -This is pdfTeX, Version 3.141592653-2.6-1.40.25 (TeX Live 2023/Debian) (preloaded format=pdflatex 2024.9.11) 15 SEP 2025 11:35 +This is pdfTeX, Version 3.141592653-2.6-1.40.25 (TeX Live 2023/Debian) (preloaded format=pdflatex 2024.9.10) 19 SEP 2025 16:33 entering extended mode restricted \write18 enabled. file:line:error style messages enabled. @@ -931,25 +931,30 @@ LaTeX Font Info: Font shape `OT1/ptm/bx/n' in size <7> not available LaTeX Font Info: Trying to load font information for TS1+ptm on input line 168. (/usr/share/texlive/texmf-dist/tex/latex/psnfss/ts1ptm.fd File: ts1ptm.fd 2001/06/04 font definitions for TS1/ptm. -)) [6] (./main.bbl) [7] (./main.aux) +)) [6] (./research-approach/v1.tex +Overfull \hbox (2.08794pt too wide) in paragraph at lines 49--63 +[]\OT1/ptm/m/n/12 FRET pro-vides func-tion-al-ity to check the \OT1/ptm/m/it/12 re-al-iz-abil-ity \OT1/ptm/m/n/12 of a sys-tem. Re-al-iz-abil-ity checks whether + [] + +[7]) [8] (./main.bbl) [9] (./main.aux) *********** LaTeX2e <2023-11-01> patch level 1 L3 programming layer <2024-01-22> *********** ) Here is how much of TeX's memory you used: - 25421 strings out of 476182 - 528088 string characters out of 5795595 + 25430 strings out of 476182 + 528320 string characters out of 5795595 1934975 words of memory out of 5000000 - 46870 multiletter control sequences out of 15000+600000 + 46875 multiletter control sequences out of 15000+600000 590786 words of font info for 108 fonts, out of 8000000 for 9000 14 hyphenation exceptions out of 8191 110i,17n,107p,1008b,531s stack positions out of 10000i,1000n,20000p,200000b,200000s -Output written on main.pdf (8 pages, 233483 bytes). +Output written on main.pdf (10 pages, 238007 bytes). PDF statistics: - 128 PDF objects out of 1000 (max. 8388607) - 75 compressed objects within 1 object stream + 134 PDF objects out of 1000 (max. 8388607) + 79 compressed objects within 1 object stream 0 named destinations out of 1000 (max. 500000) 129 words of extra memory for PDF output out of 10000 (max. 10000000) diff --git a/Writing/ERLM/main.pdf b/Writing/ERLM/main.pdf index d2f0176a4..b7cfd75e0 100644 Binary files a/Writing/ERLM/main.pdf and b/Writing/ERLM/main.pdf differ diff --git a/Writing/ERLM/main.synctex.gz b/Writing/ERLM/main.synctex.gz index 3adfb0395..fc5ee9b1f 100644 Binary files a/Writing/ERLM/main.synctex.gz and b/Writing/ERLM/main.synctex.gz differ diff --git a/Writing/ERLM/main.tex b/Writing/ERLM/main.tex index 39890ddbf..c75ef3405 100644 --- a/Writing/ERLM/main.tex +++ b/Writing/ERLM/main.tex @@ -8,6 +8,8 @@ \input{goals-and-outcomes/v4} \newpage \input{state-of-the-art/v2} +\newpage +\input{research-approach/v1} \newpage \bibliography{references} diff --git a/Writing/ERLM/research-approach/outline.md b/Writing/ERLM/research-approach/outline.md index 1f2e4ab48..ea8a70728 100644 --- a/Writing/ERLM/research-approach/outline.md +++ b/Writing/ERLM/research-approach/outline.md @@ -26,3 +26,10 @@ Integrate V design into the workings here 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/Writing/ERLM/research-approach/v1.tex b/Writing/ERLM/research-approach/v1.tex new file mode 100644 index 000000000..d306fc013 --- /dev/null +++ b/Writing/ERLM/research-approach/v1.tex @@ -0,0 +1,85 @@ +\section{Research Approach} + +This research will overcome the limits of current practice to build high +assurance hybrid control systems for critical infrastructure. To do this, we +must accomplish 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 using reachability + +\end{enumerate} + +In the following sections I will discuss how these thrusts will be accomplished. + +\subsection{\((Procedures \wedge FRET) \rightarrow Temporal Specifications\)} + +The motivating factor behind this work is the fact that commercial nuclear power +operations have remained manually controlled by human operators, despite +advances in control systems sophistication. The frustrating part of this is that +the procedures performed by human operators are highly prescriptive. Human +operators in nuclear power plants may not be entirely necessary with the +technology we have today. + +Written procedures and requirements in nuclear power are descriptive enough we +may be able to translate them into logical formulae with little effort. If we +can accomplish this, we can automate existing procedures without inducing +reengineering. The easiest way to accomplish this task will be through the use +of automated translational tools. Tools like FRET can help accomplish this task. + +FRET uses a specialized requriements languaged called FRETish to restrict +requirements to be written in easy to understand components, but without leaving +room for ambiguity. FRET does this by forcing requirements to contain six +possible parts: %CITE FRET MANUAL + +\begin{enumerate} + \item Scope: \textit{What modes does this requirement hold?} + \item Condition: \textit{Scope + more specificity} + \item Component: \textit{What does this requirment affect?} + \item Shall + \item Timing: \textit{When does the response happen?} + \item Response: \textit{What should happen?} +\end{enumerate} + +FRET provides functionality to check the \textit{realizability} of a system. +Realizability checks whether or not the written requirements are complete by +examining the six components that make up requirements. +Complete requirements are those that do not conflict with one another, and do +not leave any behavior as undefined. Systems that are not realizable from the +procedure definitions and design requirements are problematic beyond realizing +autonomy. These systems have behavior in their systems that is a physical +equivalent of a software bug. With FRET, we can catch these errors while +building an autonomous controller. The second type of error including undefined +behaviors are those that may be left up to human judgement during control. This +is not desirable for high assurance systems, as however trained humans can be, +are still prone to errors. Addressing these vulnerabilities in FRET while +building an autonomous controller will deliver a controller free of these +vulnerabilities. + +%The above stuff about realizability should be checked out. + +FRET also provides the capability to export the requirements created in a +temporal logic format. This capability allows us to leave FRET and move onto the +next step of our approach, where we will synthesize the discrete mode switching +behavior. + +\subsection{\((TemporalLogic \wedge ReactiveSynthesis) \rightarrow +DiscreteAutomata\) } +In this section of our approach we describe how the discrete component of the +hybrid system will be created. The formal specifications created in FRET will be +used with reactive synthesis tools to generate the mode switching components. +These components effectively make up the human component of reactor operation by +automating the decision points typically specified in written procedures. By +removing the human component, we eliminate the possibility of human error and +advance hybrid system autonomy. + +Reactive synthesis is an active field in computer science that focuses on the +synthesis of discrete controllers created from temporal logic specifications. +Reactive defines that the system responds to inputs to create outputs. These +systems are finite in size, where each node represents a unique set of discrete +states \(q\). diff --git a/Writing/ERLM/state-of-the-art/v1.tex b/Writing/ERLM/state-of-the-art/v1.tex index 0be76dceb..ca5d3c587 100644 --- a/Writing/ERLM/state-of-the-art/v1.tex +++ b/Writing/ERLM/state-of-the-art/v1.tex @@ -15,9 +15,7 @@ the intellectual merit of this research. \subsection{Control Theory and Hybrid Systems} Hybrid systems have two components to their behavior. They have continuous -dynamics called 'flow', and have discrete dynamics called 'jumps'. Hybrid -systems can often be described as a set of differential and difference -equations. An hybrid system can be defined as follows: +dynamics called 'flow', and have discrete dynamics called 'jumps'. Hybrid systems can often be described as a set of differential and difference equations. An hybrid system can be defined as follows: \begin{align} \dot{x}(t) &= f(x(t), q(t), u(t)) \\ diff --git a/reading_tasks.py b/reading_tasks.py new file mode 100755 index 000000000..c70e5cfdb --- /dev/null +++ b/reading_tasks.py @@ -0,0 +1,124 @@ +#!/usr/bin/env python3 + +import sys +import re +import subprocess +import argparse + + +def parse_bibtex_entry(entry): + """Extract title and year from a BibTeX entry.""" + title = "" + year = "" + + # Extract title + title_match = re.search( + r"title\s*=\s*\{(.+?)\}\s*,", entry, re.DOTALL | re.IGNORECASE + ) + if title_match: + title = title_match.group(1) + # Clean up title - remove extra braces and LaTeX commands + title = re.sub(r"^\{+|\}+$", "", title) # Remove outer braces + title = re.sub(r"\{\{|\}\}", "", title) # Remove double braces + title = re.sub(r"\\textit\{([^}]+)\}", r"\1", title) # Remove \textit{} + title = re.sub(r"\\emph\{([^}]+)\}", r"\1", title) # Remove \emph{} + title = title.replace("â€", "-") # Fix encoding issues + title = title.strip() + + # Extract year from date field + date_match = re.search(r"date\s*=\s*\{(\d{4})", entry, re.IGNORECASE) + if date_match: + year = date_match.group(1) + + return title, year + + +def create_task(title, year): + """Create a TaskWarrior task for the paper.""" + if not title: + return False + + # Format: [title] ([year]) + task_desc = title + if year: + task_desc += f" ({year})" + + # Create the task command + cmd = ["task", "add", task_desc, "+reading", "project:thesis"] + + try: + subprocess.run(cmd, check=True, capture_output=True, text=True) + return True + except subprocess.CalledProcessError as e: + print(f"Error creating task: {e}") + return False + + +def main(): + parser = argparse.ArgumentParser( + description="Convert BibTeX entries to TaskWarrior reading tasks" + ) + parser.add_argument("bibtex_file", help="Path to the BibTeX file") + args = parser.parse_args() + + # Check if file exists + try: + with open(args.bibtex_file, "r", encoding="utf-8") as f: + content = f.read() + except FileNotFoundError: + print(f"Error: File '{args.bibtex_file}' not found.") + sys.exit(1) + except UnicodeDecodeError: + # Try with different encoding if UTF-8 fails + try: + with open(args.bibtex_file, "r", encoding="latin-1") as f: + content = f.read() + except Exception as e: + print(f"Error reading file: {e}") + sys.exit(1) + + # Check if taskwarrior is available + try: + subprocess.run(["task", "--version"], check=True, capture_output=True) + except (subprocess.CalledProcessError, FileNotFoundError): + print("Error: TaskWarrior (task) is not installed or not in PATH.") + sys.exit(1) + + print(f"Processing BibTeX file: {args.bibtex_file}") + print("Creating reading tasks in TaskWarrior...") + print() + + # Split content into individual entries + # Look for @type{key, patterns + entries = re.split(r"@\w+\{[^,]*,", content) + # Remove the first empty split + entries = [entry.strip() for entry in entries[1:] if entry.strip()] + + created_count = 0 + + for i, entry in enumerate(entries): + title, year = parse_bibtex_entry(entry) + + if title: + if create_task(title, year): + created_count += 1 + print( + f"✓ Created task {created_count}: {title}" + + (f" ({year})" if year else "") + ) + else: + print(f"✗ Failed to create task for: {title}") + + print() + print(f"Finished processing BibTeX file.") + print( + f"Created {created_count} reading tasks with tag 'reading' under project 'thesis'." + ) + print() + print("To view your reading tasks, use:") + print(" task +reading list") + print(" task project:thesis list") + + +if __name__ == "__main__": + main()