diff --git a/.sessions/nvim_config.vim b/.sessions/nvim_config.vim index f65f9e7d..34a4189d 100644 --- a/.sessions/nvim_config.vim +++ b/.sessions/nvim_config.vim @@ -13,14 +13,33 @@ if &shortmess =~ 'A' else set shortmess=aoO endif -badd +12 ~/.config/nvim/lua/custom/plugins.lua badd +44 custom/configs/lspconfig.lua -badd +89 custom/journal.lua +badd +1 custom/taskwarrior.lua +badd +11 custom/init.lua +badd +203 ~/.config/nvim/lua/custom/plugins.lua argglobal %argdel -edit custom/journal.lua +edit ~/.config/nvim/lua/custom/plugins.lua +let s:save_splitbelow = &splitbelow +let s:save_splitright = &splitright +set splitbelow splitright +wincmd _ | wincmd | +vsplit +1wincmd h +wincmd w +let &splitbelow = s:save_splitbelow +let &splitright = s:save_splitright +wincmd t +let s:save_winminheight = &winminheight +let s:save_winminwidth = &winminwidth +set winminheight=0 +set winheight=1 +set winminwidth=0 +set winwidth=1 +exe 'vert 1resize ' . ((&columns * 95 + 95) / 190) +exe 'vert 2resize ' . ((&columns * 94 + 95) / 190) argglobal -balt ~/.config/nvim/lua/custom/plugins.lua +balt custom/configs/lspconfig.lua setlocal foldmethod=manual setlocal foldexpr=v:lua.vim.treesitter.foldexpr() setlocal foldmarker={{{,}}} @@ -31,12 +50,38 @@ setlocal foldnestmax=20 setlocal foldenable silent! normal! zE let &fdl = &fdl -let s:l = 89 - ((11 * winheight(0) + 23) / 47) +let s:l = 203 - ((53 * winheight(0) + 30) / 60) if s:l < 1 | let s:l = 1 | endif keepjumps exe s:l normal! zt -keepjumps 89 +keepjumps 203 normal! 016| +wincmd w +argglobal +if bufexists(fnamemodify("custom/taskwarrior.lua", ":p")) | buffer custom/taskwarrior.lua | else | edit custom/taskwarrior.lua | endif +if &buftype ==# 'terminal' + silent file custom/taskwarrior.lua +endif +balt custom/configs/lspconfig.lua +setlocal foldmethod=manual +setlocal foldexpr=v:lua.vim.treesitter.foldexpr() +setlocal foldmarker={{{,}}} +setlocal foldignore=# +setlocal foldlevel=0 +setlocal foldminlines=1 +setlocal foldnestmax=20 +setlocal foldenable +silent! normal! zE +let &fdl = &fdl +let s:l = 280 - ((43 * winheight(0) + 30) / 60) +if s:l < 1 | let s:l = 1 | endif +keepjumps exe s:l +normal! zt +keepjumps 280 +normal! 09| +wincmd w +exe 'vert 1resize ' . ((&columns * 95 + 95) / 190) +exe 'vert 2resize ' . ((&columns * 94 + 95) / 190) tabnext 1 if exists('s:wipebuf') && len(win_findbuf(s:wipebuf)) == 0 && getbufvar(s:wipebuf, '&buftype') isnot# 'terminal' silent exe 'bwipe ' . s:wipebuf @@ -44,6 +89,8 @@ endif unlet! s:wipebuf set winheight=1 winwidth=20 let &shortmess = s:shortmess_save +let &winminheight = s:save_winminheight +let &winminwidth = s:save_winminwidth let s:sx = expand(":p:r")."x.vim" if filereadable(s:sx) exe "source " . fnameescape(s:sx) diff --git a/.task/backlog.data b/.task/backlog.data new file mode 100644 index 00000000..0b512993 --- /dev/null +++ b/.task/backlog.data @@ -0,0 +1,24 @@ +{"description":"learn taskmaster","entry":"20250909T172539Z","modified":"20250909T172539Z","status":"pending","uuid":"b4945a12-909c-47cc-8779-e3f8f917181c"} +{"description":"try taskmaster","entry":"20250909T172547Z","modified":"20250909T172547Z","status":"pending","uuid":"a56a03cd-36ec-4786-907b-77d8d162426d"} +{"description":"learn taskmaster","end":"20250909T172616Z","entry":"20250909T172539Z","modified":"20250909T172616Z","status":"completed","uuid":"b4945a12-909c-47cc-8779-e3f8f917181c"} +{"description":"try taskmaster","end":"20250909T172619Z","entry":"20250909T172547Z","modified":"20250909T172619Z","status":"completed","uuid":"a56a03cd-36ec-4786-907b-77d8d162426d"} +{"description":"Write outline for SOTA project:ERLM due:today","entry":"20250909T180102Z","modified":"20250909T180102Z","status":"pending","uuid":"3dfe52e3-749b-4d6b-9a01-2b078ddd968a"} +{"description":"Write outline for SOTA project:ERLM due:today","due":"20250909T040000Z","entry":"20250909T180102Z","modified":"20250909T180217Z","project":"ERLM,","status":"pending","uuid":"3dfe52e3-749b-4d6b-9a01-2b078ddd968a"} +{"description":"Literature review of rchapter 2 project:dissertation priority:H +reading due:friday","entry":"20250909T180633Z","modified":"20250909T180633Z","status":"pending","uuid":"864d1a2e-7343-403a-80e6-d95bff22d90b"} +{"description":"Literature review","due":"20250912T040000Z","entry":"20250909T180832Z","modified":"20250909T180832Z","priority":"H","project":"dissertation","status":"pending","uuid":"670b304a-2f18-47b9-beb3-b0aa7eb38e57","tags":["reading"]} +{"description":"fix pid controller","entry":"20250909T181356Z","modified":"20250909T181356Z","project":"research","status":"pending","uuid":"91f80e7a-7a7b-4f45-9593-872ba04039d7","tags":["coding","urgent"]} +{"description":"hellow!","entry":"20250909T181900Z","modified":"20250909T181900Z","status":"pending","uuid":"1ee492ad-9e81-4b01-b062-2f4d166a7865"} +{"description":"hellow testing","entry":"20250909T182122Z","modified":"20250909T182122Z","status":"pending","uuid":"44d5c3a3-d97b-4ef2-a0ab-de5d562830d3"} +{"description":"testing","entry":"20250909T182418Z","modified":"20250909T182418Z","status":"pending","uuid":"9e4fb42e-8427-4f8a-9405-291de01f2425"} +{"description":"testing testing","entry":"20250909T183241Z","modified":"20250909T183241Z","project":"urmom","status":"pending","uuid":"5c094262-eb5e-4763-927b-1919c03d9790"} +{"description":"Write outline for state of the art","due":"20250910T040000Z","entry":"20250909T183935Z","modified":"20250909T183935Z","project":"ERLM","status":"pending","uuid":"8e7a8e19-9197-4008-b7d9-521ffcf7ba91"} +{"description":"Write zettels about Andre Platzer and differential dynamic logic","entry":"20250909T184010Z","modified":"20250909T184010Z","project":"zk","status":"pending","uuid":"74f33a56-3525-47d2-aa8c-fcb9488c7726"} +{"description":"Write zettels about webofscience database","entry":"20250909T184042Z","modified":"20250909T184042Z","project":"zk","status":"pending","uuid":"9cb17c85-f1e6-4280-86da-a5af8f229b15"} +{"description":"Look over obsidian tasks and see if anything is worth moving over","entry":"20250909T184102Z","modified":"20250909T184102Z","status":"pending","uuid":"c1a5390d-5b84-4f9c-8acb-ffb970682660","tags":["taskwarrior"]} +{"description":"Follow up with Daniel about controls bootcamp","due":"20250911T040000Z","entry":"20250909T201850Z","modified":"20250909T201850Z","project":"FSAE","status":"pending","uuid":"3eaadead-4e5e-4823-9077-16d6e1800862"} +{"description":"Follow up with Bajaj about writing TurboSAR paper","due":"20250911T040000Z","entry":"20250909T202126Z","modified":"20250909T202126Z","status":"pending","uuid":"fa2699f9-0082-433e-ae0d-cc2553db9865"} +{"description":"Follow up with Bajaj about writing TurboSAR paper","due":"20250911T040000Z","entry":"20250909T202126Z","modified":"20250909T202243Z","priority":"L","status":"pending","uuid":"fa2699f9-0082-433e-ae0d-cc2553db9865"} +{"description":"Look around for summer internships with national labs","entry":"20250909T202851Z","modified":"20250909T202851Z","status":"pending","uuid":"d3f3dc53-4feb-4b7e-8de5-86ebf3c535d5"} +{"description":"Write first draft of state of the art","due":"20250912T040000Z","entry":"20250909T203258Z","modified":"20250909T203258Z","project":"ERLM","status":"pending","uuid":"4bec1530-18bc-43cb-9f0b-61e35dbf1730","tags":["writing"],"depends":["8e7a8e19-9197-4008-b7d9-521ffcf7ba91"]} +{"description":"Write outline for state of the art","due":"20250910T040000Z","entry":"20250909T183935Z","modified":"20250909T203502Z","project":"ERLM","start":"20250909T203502Z","status":"pending","uuid":"8e7a8e19-9197-4008-b7d9-521ffcf7ba91"} +{"description":"Write outline for state of the art","due":"20250910T040000Z","entry":"20250909T183935Z","modified":"20250909T210227Z","project":"ERLM","status":"pending","uuid":"8e7a8e19-9197-4008-b7d9-521ffcf7ba91"} diff --git a/.task/completed.data b/.task/completed.data new file mode 100644 index 00000000..9816ab66 --- /dev/null +++ b/.task/completed.data @@ -0,0 +1,2 @@ +[description:"learn taskmaster" end:"1757438776" entry:"1757438739" modified:"1757438776" status:"completed" uuid:"b4945a12-909c-47cc-8779-e3f8f917181c"] +[description:"try taskmaster" end:"1757438779" entry:"1757438747" modified:"1757438779" status:"completed" uuid:"a56a03cd-36ec-4786-907b-77d8d162426d"] diff --git a/.task/pending.data b/.task/pending.data new file mode 100644 index 00000000..11c3e793 --- /dev/null +++ b/.task/pending.data @@ -0,0 +1,8 @@ +[description:"Write outline for state of the art" due:"1757476800" entry:"1757443175" modified:"1757451747" project:"ERLM" status:"pending" uuid:"8e7a8e19-9197-4008-b7d9-521ffcf7ba91"] +[description:"Write zettels about Andre Platzer and differential dynamic logic" entry:"1757443210" modified:"1757443210" project:"zk" status:"pending" uuid:"74f33a56-3525-47d2-aa8c-fcb9488c7726"] +[description:"Write zettels about webofscience database" entry:"1757443242" modified:"1757443242" project:"zk" status:"pending" uuid:"9cb17c85-f1e6-4280-86da-a5af8f229b15"] +[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:"Follow up with Daniel about controls bootcamp" due:"1757563200" entry:"1757449130" modified:"1757449130" project:"FSAE" status:"pending" uuid:"3eaadead-4e5e-4823-9077-16d6e1800862"] +[description:"Follow up with Bajaj about writing TurboSAR paper" due:"1757563200" entry:"1757449286" modified:"1757449363" priority:"L" status:"pending" uuid:"fa2699f9-0082-433e-ae0d-cc2553db9865"] +[description:"Look around for summer internships with national labs" entry:"1757449731" modified:"1757449731" status:"pending" uuid:"d3f3dc53-4feb-4b7e-8de5-86ebf3c535d5"] +[dep_8e7a8e19-9197-4008-b7d9-521ffcf7ba91:"x" depends:"8e7a8e19-9197-4008-b7d9-521ffcf7ba91" description:"Write first draft of state of the art" due:"1757649600" entry:"1757449978" modified:"1757449978" project:"ERLM" status:"pending" tags:"writing" tags_writing:"x" uuid:"4bec1530-18bc-43cb-9f0b-61e35dbf1730"] diff --git a/.task/undo.data b/.task/undo.data new file mode 100644 index 00000000..df3eedc1 --- /dev/null +++ b/.task/undo.data @@ -0,0 +1,78 @@ +time 1757438739 +new [description:"learn taskmaster" entry:"1757438739" modified:"1757438739" status:"pending" uuid:"b4945a12-909c-47cc-8779-e3f8f917181c"] +--- +time 1757438747 +new [description:"try taskmaster" entry:"1757438747" modified:"1757438747" status:"pending" uuid:"a56a03cd-36ec-4786-907b-77d8d162426d"] +--- +time 1757438776 +old [description:"learn taskmaster" entry:"1757438739" modified:"1757438739" status:"pending" uuid:"b4945a12-909c-47cc-8779-e3f8f917181c"] +new [description:"learn taskmaster" end:"1757438776" entry:"1757438739" modified:"1757438776" status:"completed" uuid:"b4945a12-909c-47cc-8779-e3f8f917181c"] +--- +time 1757438779 +old [description:"try taskmaster" entry:"1757438747" modified:"1757438747" status:"pending" uuid:"a56a03cd-36ec-4786-907b-77d8d162426d"] +new [description:"try taskmaster" end:"1757438779" entry:"1757438747" modified:"1757438779" status:"completed" uuid:"a56a03cd-36ec-4786-907b-77d8d162426d"] +--- +time 1757440862 +new [description:"Write outline for SOTA project:ERLM due:today" entry:"1757440862" modified:"1757440862" status:"pending" uuid:"3dfe52e3-749b-4d6b-9a01-2b078ddd968a"] +--- +time 1757440937 +old [description:"Write outline for SOTA project:ERLM due:today" entry:"1757440862" modified:"1757440862" status:"pending" uuid:"3dfe52e3-749b-4d6b-9a01-2b078ddd968a"] +new [description:"Write outline for SOTA project:ERLM due:today" due:"1757390400" entry:"1757440862" modified:"1757440937" project:"ERLM," status:"pending" uuid:"3dfe52e3-749b-4d6b-9a01-2b078ddd968a"] +--- +time 1757441193 +new [description:"Literature review of rchapter 2 project:dissertation priority:H +reading due:friday" entry:"1757441193" modified:"1757441193" status:"pending" uuid:"864d1a2e-7343-403a-80e6-d95bff22d90b"] +--- +time 1757441312 +new [description:"Literature review" due:"1757649600" entry:"1757441312" modified:"1757441312" priority:"H" project:"dissertation" status:"pending" tags:"reading" tags_reading:"x" uuid:"670b304a-2f18-47b9-beb3-b0aa7eb38e57"] +--- +time 1757441636 +new [description:"fix pid controller" entry:"1757441636" modified:"1757441636" project:"research" status:"pending" tags:"coding,urgent" tags_coding:"x" tags_urgent:"x" uuid:"91f80e7a-7a7b-4f45-9593-872ba04039d7"] +--- +time 1757441940 +new [description:"hellow!" entry:"1757441940" modified:"1757441940" status:"pending" uuid:"1ee492ad-9e81-4b01-b062-2f4d166a7865"] +--- +time 1757442082 +new [description:"hellow testing" entry:"1757442082" modified:"1757442082" status:"pending" uuid:"44d5c3a3-d97b-4ef2-a0ab-de5d562830d3"] +--- +time 1757442258 +new [description:"testing" entry:"1757442258" modified:"1757442258" status:"pending" uuid:"9e4fb42e-8427-4f8a-9405-291de01f2425"] +--- +time 1757442761 +new [description:"testing testing" entry:"1757442761" modified:"1757442761" project:"urmom" status:"pending" uuid:"5c094262-eb5e-4763-927b-1919c03d9790"] +--- +time 1757443175 +new [description:"Write outline for state of the art" due:"1757476800" entry:"1757443175" modified:"1757443175" project:"ERLM" status:"pending" uuid:"8e7a8e19-9197-4008-b7d9-521ffcf7ba91"] +--- +time 1757443210 +new [description:"Write zettels about Andre Platzer and differential dynamic logic" entry:"1757443210" modified:"1757443210" project:"zk" status:"pending" uuid:"74f33a56-3525-47d2-aa8c-fcb9488c7726"] +--- +time 1757443242 +new [description:"Write zettels about webofscience database" entry:"1757443242" modified:"1757443242" project:"zk" status:"pending" uuid:"9cb17c85-f1e6-4280-86da-a5af8f229b15"] +--- +time 1757443262 +new [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"] +--- +time 1757449130 +new [description:"Follow up with Daniel about controls bootcamp" due:"1757563200" entry:"1757449130" modified:"1757449130" project:"FSAE" status:"pending" uuid:"3eaadead-4e5e-4823-9077-16d6e1800862"] +--- +time 1757449286 +new [description:"Follow up with Bajaj about writing TurboSAR paper" due:"1757563200" entry:"1757449286" modified:"1757449286" status:"pending" uuid:"fa2699f9-0082-433e-ae0d-cc2553db9865"] +--- +time 1757449363 +old [description:"Follow up with Bajaj about writing TurboSAR paper" due:"1757563200" entry:"1757449286" modified:"1757449286" status:"pending" uuid:"fa2699f9-0082-433e-ae0d-cc2553db9865"] +new [description:"Follow up with Bajaj about writing TurboSAR paper" due:"1757563200" entry:"1757449286" modified:"1757449363" priority:"L" status:"pending" uuid:"fa2699f9-0082-433e-ae0d-cc2553db9865"] +--- +time 1757449731 +new [description:"Look around for summer internships with national labs" entry:"1757449731" modified:"1757449731" status:"pending" uuid:"d3f3dc53-4feb-4b7e-8de5-86ebf3c535d5"] +--- +time 1757449978 +new [dep_8e7a8e19-9197-4008-b7d9-521ffcf7ba91:"x" depends:"8e7a8e19-9197-4008-b7d9-521ffcf7ba91" description:"Write first draft of state of the art" due:"1757649600" entry:"1757449978" modified:"1757449978" project:"ERLM" status:"pending" tags:"writing" tags_writing:"x" uuid:"4bec1530-18bc-43cb-9f0b-61e35dbf1730"] +--- +time 1757450102 +old [description:"Write outline for state of the art" due:"1757476800" entry:"1757443175" modified:"1757443175" project:"ERLM" status:"pending" uuid:"8e7a8e19-9197-4008-b7d9-521ffcf7ba91"] +new [description:"Write outline for state of the art" due:"1757476800" entry:"1757443175" modified:"1757450102" project:"ERLM" start:"1757450102" status:"pending" uuid:"8e7a8e19-9197-4008-b7d9-521ffcf7ba91"] +--- +time 1757451747 +old [description:"Write outline for state of the art" due:"1757476800" entry:"1757443175" modified:"1757450102" project:"ERLM" start:"1757450102" status:"pending" uuid:"8e7a8e19-9197-4008-b7d9-521ffcf7ba91"] +new [description:"Write outline for state of the art" due:"1757476800" entry:"1757443175" modified:"1757451747" project:"ERLM" status:"pending" uuid:"8e7a8e19-9197-4008-b7d9-521ffcf7ba91"] +--- diff --git a/Writing/ERLM/state-of-the-art/outline.md b/Writing/ERLM/state-of-the-art/outline.md new file mode 100644 index 00000000..593b6c12 --- /dev/null +++ b/Writing/ERLM/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) +