diff --git a/.obsidian/plugins/colored-tags/data.json b/.obsidian/plugins/colored-tags/data.json index 43440cc4..06fb87ef 100755 --- a/.obsidian/plugins/colored-tags/data.json +++ b/.obsidian/plugins/colored-tags/data.json @@ -323,7 +323,8 @@ "Formal-Methods": 311, "admin": 312, "hub": 313, - "daily": 314 + "daily": 314, + "weekly": 315 }, "_version": 3 } \ No newline at end of file diff --git a/.sessions/nvim_config.vim b/.sessions/nvim_config.vim index 5220a3e1..30f65e40 100644 --- a/.sessions/nvim_config.vim +++ b/.sessions/nvim_config.vim @@ -18,11 +18,12 @@ badd +27 ~/.config/nvim/lua/custom/language_specific_commands/markdown_and_tex.l badd +37 ~/.config/nvim/lua/custom/configs/lspconfig.lua badd +2 custom/init.lua badd +11 custom/mappings.lua +badd +385 custom/zk.lua argglobal %argdel -edit ~/.config/nvim/lua/custom/configs/lspconfig.lua +edit custom/zk.lua argglobal -balt ~/.config/nvim/lua/custom/language_specific_commands/markdown_and_tex.lua +balt ~/.config/nvim/lua/custom/plugins.lua setlocal foldmethod=manual setlocal foldexpr=v:lua.vim.treesitter.foldexpr() setlocal foldmarker={{{,}}} @@ -33,12 +34,12 @@ setlocal foldnestmax=20 setlocal foldenable silent! normal! zE let &fdl = &fdl -let s:l = 37 - ((36 * winheight(0) + 28) / 57) +let s:l = 375 - ((40 * winheight(0) + 30) / 60) if s:l < 1 | let s:l = 1 | endif keepjumps exe s:l normal! zt -keepjumps 37 -normal! 059| +keepjumps 375 +normal! 067| tabnext 1 if exists('s:wipebuf') && len(win_findbuf(s:wipebuf)) == 0 && getbufvar(s:wipebuf, '&buftype') isnot# 'terminal' silent exe 'bwipe ' . s:wipebuf diff --git a/Projects/HX_PINN/HX_model.py b/Projects/HX_PINN/HX_model.py deleted file mode 100644 index 6f083f86..00000000 --- a/Projects/HX_PINN/HX_model.py +++ /dev/null @@ -1,235 +0,0 @@ -# PINN for a tube-in-tube heat exchanger (steady 2D xr) -# - Uses automatic differentiation for PDE residuals -# - Prescribes velocity fields u_h(x,r), u_c(x,r) -# - Solves for Th, Tw, Tc - -import torch -import torch.nn as nn - -# ====== User-configurable physical constants (nondimensional if you scaled) ====== -Pe_h = 100.0 # Peclet (hot side) = u_h*L/alpha_h -Pe_c = 120.0 # Peclet (cold side) = u_c*L/alpha_c -alpha_w_ratio = 1.0 # wall alpha relative to hot-side alpha if nondim -Ri = 1.0 # inner radius (nondim, after scaling) -Ro = 1.3 # outer radius - -device = "cuda" if torch.cuda.is_available() else "cpu" -dtype = torch.float32 # float32 is usually fine; use float64 if residuals are stiff - - -# ====== Velocity profiles (nondim) ====== -def u_h(x, r): - # Poiseuille in a circular tube: u_max*(1 - (r/Ri)^2). Here Ri=1 in nondim. - return 2.0 * (1.0 - r**2) # average=1 if scaled; adjust factor to match Pe_h - - -def u_c(x, r): - # Simple plug profile in annulus as a first approximation - return torch.ones_like(r) - - -# ====== Network ====== -class MLP(nn.Module): - def __init__(self, in_dim=2, hidden=128, depth=7, out_dim=3, act=nn.SiLU): - super().__init__() - layers = [nn.Linear(in_dim, hidden), act()] - for _ in range(depth - 1): - layers += [nn.Linear(hidden, hidden), act()] - # Separate heads for Th, Tw, Tc improves conditioning - self.backbone = nn.Sequential(*layers) - self.head_h = nn.Linear(hidden, 1) - self.head_w = nn.Linear(hidden, 1) - self.head_c = nn.Linear(hidden, 1) - - # Xavier init helps with tanh/SiLU nets - def init(m): - if isinstance(m, nn.Linear): - nn.init.xavier_uniform_(m.weight) - nn.init.zeros_(m.bias) - - self.apply(init) - - def forward(self, x, r): - z = torch.stack([x, r], dim=-1) - f = self.backbone(z) - Th = self.head_h(f) - Tw = self.head_w(f) - Tc = self.head_c(f) - return Th, Tw, Tc - - -net = MLP().to(device).to(dtype) - - -# ====== Utility: gradients via autograd ====== -def grads(y, x): - return torch.autograd.grad( - y, x, grad_outputs=torch.ones_like(y), create_graph=True - )[0] - - -# ====== Collocation samplers ====== -def sample_in_hot(N): - # x in [0,1], r in [0,Ri] - x = torch.rand(N, 1, device=device, dtype=dtype) - r = Ri * torch.sqrt(torch.rand(N, 1, device=device, dtype=dtype)) # area-uniform - return x.requires_grad_(True), r.requires_grad_(True) - - -def sample_in_wall(N): - x = torch.rand(N, 1, device=device, dtype=dtype) - r = torch.sqrt( - (Ro**2 - Ri**2) * torch.rand(N, 1, device=device, dtype=dtype) + Ri**2 - ) - return x.requires_grad_(True), r.requires_grad_(True) - - -def sample_in_cold(N): - x = torch.rand(N, 1, device=device, dtype=dtype) - r = (Ro + (Ro)) * 0.5 * 0 + ( - torch.rand(N, 1, device=device, dtype=dtype) * (Ro - Ri) + Ri - ) # simple annulus - return x.requires_grad_(True), r.requires_grad_(True) - - -def sample_interface_Ri(N): - x = torch.rand(N, 1, device=device, dtype=dtype) - r = torch.full_like(x, Ri, requires_grad=True) - return x, r - - -def sample_interface_Ro(N): - x = torch.rand(N, 1, device=device, dtype=dtype) - r = torch.full_like(x, Ro, requires_grad=True) - return x, r - - -def sample_inlet_hot(N): - x = torch.zeros(N, 1, device=device, dtype=dtype, requires_grad=True) - r = Ri * torch.sqrt(torch.rand(N, 1, device=device, dtype=dtype)) - return x, r - - -def sample_inlet_cold_counterflow(N): - x = torch.ones(N, 1, device=device, dtype=dtype, requires_grad=True) - r = torch.rand(N, 1, device=device, dtype=dtype) * (Ro - Ri) + Ri - return x, r - - -def sample_outlet_hot(N): - x = torch.ones(N, 1, device=device, dtype=dtype, requires_grad=True) - r = Ri * torch.sqrt(torch.rand(N, 1, device=device, dtype=dtype)) - return x, r - - -def sample_outlet_cold(N): - x = torch.zeros(N, 1, device=device, dtype=dtype, requires_grad=True) - r = torch.rand(N, 1, device=device, dtype=dtype) * (Ro - Ri) + Ri - return x, r - - -# ====== Boundary condition targets (nondim) ====== -T_h_in = 1.0 # scale so hot inlet is 1 -T_c_in = 0.0 # cold inlet is 0 - -# ====== Training loop ====== -opt = torch.optim.Adam(net.parameters(), lr=1e-3) - -for it in range(20000): - opt.zero_grad() - - # ----- Interior residuals ----- - Nh = Nw = Nc = 512 - xh, rh = sample_in_hot(Nh) - xw, rw = sample_in_wall(Nw) - xc, rc = sample_in_cold(Nc) - - Th, Tw, Tc = net(xh, rh) - Th_x = grads(Th, xh) - Th_r = grads(Th, rh) - Th_xx = grads(Th_x, xh) - Th_rr = grads(Th_r, rh) - # Hot PDE: u_h dTh/dx = (1/Pe_h)*(Th_rr + (1/r) Th_r + Th_xx) (choose to keep xx or drop) - uh = u_h(xh, rh) - hot_res = uh * Th_x - (1.0 / Pe_h) * (Th_rr + (1.0 / rh) * Th_r + Th_xx) - - (Tw_,) = net(xw, rw)[1:2] # only Tw - Tw_x = grads(Tw_, xw) - Tw_r = grads(Tw_, rw) - Tw_xx = grads(Tw_x, xw) - Tw_rr = grads(Tw_r, rw) - wall_res = Tw_rr + (1.0 / rw) * Tw_r + Tw_xx # alpha_w absorbed in scaling - - Tc = net(xc, rc)[2] - Tc_x = grads(Tc, xc) - Tc_r = grads(Tc, rc) - Tc_xx = grads(Tc_x, xc) - Tc_rr = grads(Tc_r, rc) - uc = u_c(xc, rc) - cold_res = uc * Tc_x - (1.0 / Pe_c) * (Tc_rr + (1.0 / rc) * Tc_r + Tc_xx) - - L_pde = hot_res.pow(2).mean() + wall_res.pow(2).mean() + cold_res.pow(2).mean() - - # ----- Interface continuity (temperature + flux) ----- - Ni = 256 - xi, rRi = sample_interface_Ri(Ni) - Th_i, Tw_i, _ = net(xi, rRi) - # fluxes: -k dT/dr. With nondim, use ratios; set k_w/k_h = kw_rel, etc. - dTh_dr = grads(Th_i, rRi) - dTw_dr = grads(Tw_i, rRi) - kw_over_kh = 1.0 - L_int_Ri = (Th_i - Tw_i).pow(2).mean() + (dTh_dr - kw_over_kh * dTw_dr).pow( - 2 - ).mean() - - xo, rRo = sample_interface_Ro(Ni) - _, Tw_o, Tc_o = net(xo, rRo) - dTw_dr_o = grads(Tw_o, rRo) - dTc_dr_o = grads(Tc_o, rRo) - kc_over_kw = 1.0 - L_int_Ro = (Tc_o - Tw_o).pow(2).mean() + (kc_over_kw * dTc_dr_o - dTw_dr_o).pow( - 2 - ).mean() - - # ----- Boundary conditions ----- - Nb = 256 - x_in_h, r_in_h = sample_inlet_hot(Nb) - Th_in_pred = net(x_in_h, r_in_h)[0] - L_in_h = (Th_in_pred - T_h_in).pow(2).mean() - - x_in_c, r_in_c = sample_inlet_cold_counterflow(Nb) - Tc_in_pred = net(x_in_c, r_in_c)[2] - L_in_c = (Tc_in_pred - T_c_in).pow(2).mean() - - # Outlets: convective (∂T/∂x ≈ 0) - x_out_h, r_out_h = sample_outlet_hot(Nb) - Th_out = net(x_out_h, r_out_h)[0] - L_out_h = grads(Th_out, x_out_h).pow(2).mean() - - x_out_c, r_out_c = sample_outlet_cold(Nb) - Tc_out = net(x_out_c, r_out_c)[2] - L_out_c = grads(Tc_out, x_out_c).pow(2).mean() - - # Symmetry at r=0: dTh/dr = 0 - Ns = 128 - xs = torch.rand(Ns, 1, device=device, dtype=dtype, requires_grad=True) - rs0 = torch.zeros_like(xs, requires_grad=True) - Th_axis = net(xs, rs0)[0] - L_sym = grads(Th_axis, rs0).pow(2).mean() - - # ----- Total loss with simple weights (tune these!) ----- - L = ( - 1.0 * L_pde - + 5.0 * (L_int_Ri + L_int_Ro) - + 2.0 * (L_in_h + L_in_c) - + 1.0 * (L_out_h + L_out_c) - + 1.0 * L_sym - ) - - L.backward() - opt.step() - - if it % 1000 == 0: - print( - f"it={it} L={L.item():.3e} PDE={L_pde.item():.3e} IF={L_int_Ri.item()+L_int_Ro.item():.3e}" - ) diff --git a/Zettelkasten/Fleeting Notes/Daily/2025-08-27.md b/Zettelkasten/Fleeting Notes/Daily/2025-08-27.md new file mode 100644 index 00000000..a9482941 --- /dev/null +++ b/Zettelkasten/Fleeting Notes/Daily/2025-08-27.md @@ -0,0 +1,32 @@ +--- +id: 2025-08-27 +title: Daily — 2025-08-27 +type: daily +created: 2025-08-27T18:33:33Z +modified: 2025-08-28T17:57:53Z +tags: [daily] +--- + +# Daily — 2025-08-27 + +## Quick capture + +COLE GROUP MEETING +Accomplishments: +- Quad chart +- writing more about LTL and building out some notes from +papers +- Found resources about temporal logic +- first nuce class has happened. Codes and standards were +cancelled + +to do: +- Write goals and outcomes +- Write more about approach. This is squishtastic +- Actually finalize some outcomes. How do i navigate the +fact that within switching mechanisms there is dynamics +happening +- I didn't say anything about what a hybrid system is. +That's kind of the whole point of the thing. + +## Notes diff --git a/Zettelkasten/Permanent Notes/20250826114550-heilmeier-catechism.md b/Zettelkasten/Permanent Notes/20250826114550-heilmeier-catechism.md new file mode 100644 index 00000000..edd0a271 --- /dev/null +++ b/Zettelkasten/Permanent Notes/20250826114550-heilmeier-catechism.md @@ -0,0 +1,40 @@ +--- +id: 20250826114550 +title: Heilmeier Catechism +type: permanent +created: 2025-08-26T15:45:50Z +modified: 2025-08-26T16:02:59Z +tags: [] +--- + +# Heilmeier Catechism + +George Heilmeier was a program manager at the Defense +Advanced Research Projects Administration (DARPA) who was +flummoxed with research proposals for artificial +intelligence. In order to quickly sort through the +proposals, he developed an 8 question system to quickly cut +through the muck. + +This is the Heilmeier Catechism: + +1. What are you trying to do? Articulate your research with + absolutely no jargon. + +2. How is it done today and what are the limits of current + practice? + +3. What's new in your approach and why will you be + successful? + +4. Who cares? If you're successful, what difference will it + make? + +5. What are the risks? + +6. How long will it take? + +7. How much will it cost? + +8. What are the midterm and final exams? How will you + measure success? diff --git a/Zettelkasten/Permanent Notes/Thesis/3100-erlm-quad-chart-template.odp b/Zettelkasten/Permanent Notes/Thesis/3100-erlm-quad-chart-template.odp new file mode 100644 index 00000000..caa13e36 Binary files /dev/null and b/Zettelkasten/Permanent Notes/Thesis/3100-erlm-quad-chart-template.odp differ diff --git a/Zettelkasten/Permanent Notes/Thesis/DR-20250826144307-heilmeier-questions.md b/Zettelkasten/Permanent Notes/Thesis/DR-20250826144307-heilmeier-questions.md new file mode 100644 index 00000000..4d28f076 --- /dev/null +++ b/Zettelkasten/Permanent Notes/Thesis/DR-20250826144307-heilmeier-questions.md @@ -0,0 +1,39 @@ +--- +id: DR-20250826144307 +title: Heilmeier Questions +type: thesis +created: 2025-08-26T18:43:07Z +modified: 2025-08-28T20:42:41Z +tags: [] +--- + +# Heilmeier Questions for my Thesis Topic + +**TITLE** +[[Thesis Title Ideas]] + +***High-Assurance Hybrid Controller Synthesis from Logical +Specifications*** + +## **What am I trying to do? No jargon!** + +The goal of this research is to use formal methods to create +hybrid controllers with provable guarantees of performance +and safety. Hybrid control systems are control systems that +have distinct changes in system dynamics under different +conditions, which are often called modes. Modes are often +defined by design requirements, and as such can be easily +translated into formal specifications. This research will +will eliminate the possible introduction of accidental +errors while building controllers by automatically +synthesizing the mode switching behavior from design +requirements. Controller behavior within modes will be +verified using reachability analysis. + +## **How is it done today?** + +## **What's new in my approach?** + +## **Who cares?** + + diff --git a/Zettelkasten/Permanent Notes/Thesis/DR-20250826145452-title-ideas.md b/Zettelkasten/Permanent Notes/Thesis/DR-20250826145452-title-ideas.md new file mode 100644 index 00000000..370e9b29 --- /dev/null +++ b/Zettelkasten/Permanent Notes/Thesis/DR-20250826145452-title-ideas.md @@ -0,0 +1,33 @@ +--- +id: DR-20250826145452 +title: Title Ideas +type: thesis +created: 2025-08-26T18:54:52Z +modified: 2025-08-26T19:03:19Z +tags: [] +--- + +# Thesis Title Ideas + +## August 26th +1. Hybrid Controller Synthesis from Logical Specifications + +2. Hybrid Mode Switching Controller Synthesis from + Regulatory Requirements as Logical Specifications + +3. Formally Verified Autonomous Hybrid Controller + Implementations Synthesized from Regulatory Requirements + +Okay so mixing these: + +*Formally Tractable Hybrid Controller Synthesis from Logical +Specifications of Regulatory Requirements* + +It's long. But Hybrid controller synthesis from logical +specifications might not be enough? Also 'logical +specifications of regulatory requirements' might not make +much sense either. Y'know what, I think I like the first one +best. I'm going with: + +***High-Assurance Hybrid Controller Synthesis from Logical +Specifications*** diff --git a/Zettelkasten/Permanent Notes/Thesis/sabo-quad-chart.pptx b/Zettelkasten/Permanent Notes/Thesis/sabo-quad-chart.pptx new file mode 100644 index 00000000..420e2584 Binary files /dev/null and b/Zettelkasten/Permanent Notes/Thesis/sabo-quad-chart.pptx differ