[Dev] Interface MTK

[jbcaillau]

FTR:

• https://discourse.julialang.org/t/mtk-and-jump/58161/4
• MathematicalSystems #159

Latest devs, interfacing InfiniteOpt (direct) / CasaDi (direct shooting): https://docs.sciml.ai/ModelingToolkit/stable/tutorials/dynamic_optimization

[jbcaillau]

• prioritise direct translation from math (text / TeX or Markdown like sources) by LLMs
• MTK or other DSLs are particular targets for which translations should be automated

[ocots]

Claude test

Learn the syntax of OptimalControl.jl DSL described at the link below to translate math into this DSL (Julia language): https://control-toolbox.org/OptimalControl.jl/stable/manual-abstract.html.

Can you rewrite the problem formulated in ModelingToolKit from https://raw.githubusercontent.com/SciML/ModelingToolkit.jl/master/docs/src/tutorials/dynamic_optimization.md into OptimalControl DSL?

using OptimalControl

# Problem 1: Rocket Launch - Maximize final height
# ================================================

# Parameters (these would be provided when solving)
h_c = 500; m₀ = 1.0; h₀ = 1; g₀ = 1; D_c = 0.5 * 620 * m₀ / g₀
c = 0.5 * √(g₀ * h₀); Tₘ = 3.5 * g₀ * m₀; m_c = 0.6

# Helper functions for drag and gravity
drag(h, v, h_c, h₀, D_c) = D_c * v^2 * exp(-h_c * (h - h₀) / h₀)
gravity(h, g₀, h₀) = g₀ * (h₀ / h)

rocket = @def begin
    # Time interval
    t ∈ [0.0, 0.2], time
    
    # State variables: height, velocity, mass
    x = (h, v, m) ∈ R³, state
    
    # Control variable: thrust (bounded)
    T ∈ R, control
    
    # Dynamics
    ∂(h)(t) == v(t)
    ∂(v)(t) == (T(t) - drag(h(t), v(t), h_c, h₀, D_c)) / m(t) - gravity(h(t), g₀, h₀)
    ∂(m)(t) == -T(t) / c
    
    # Control bounds
    0 ≤ T(t) ≤ Tₘ
    
    # State bounds (mass must stay between m_c and 1.0)
    m_c ≤ m(t) ≤ 1.0
    
    # Boundary conditions
    h(0) == h₀
    v(0) == 0
    m(0) == m₀
    
    # Terminal constraints
    T(0.2) == 0
    m(0.2) == m_c
    
    # Objective: maximize final height (minimize negative height)
    -h(0.2) → min
end

# Problem 2: Double Integrator - Minimum Time Problem
# ===================================================

block = @def begin
    # Variable: free final time
    tf ∈ R, variable
    
    # Time interval with variable final time
    t ∈ [0.0, tf], time
    
    # State variables: position, velocity
    x = (pos, vel) ∈ R², state
    
    # Control variable: acceleration (bounded)
    u ∈ R, control
    
    # Dynamics
    ∂(pos)(t) == vel(t)
    ∂(vel)(t) == u(t)
    
    # Control bounds
    -1.0 ≤ u(t) ≤ 1.0
    
    # Initial conditions
    pos(0) == 1.0
    vel(0) == 0.0
    
    # Terminal constraints
    pos(tf) == 0.0
    vel(tf) == 0.0
    
    # Variable constraint (tf must be positive)
    tf ≥ 0.0
    
    # Objective: minimize time
    tf → min
end

[jbcaillau]

@ocots @gergaud pour le projet n7, autre piste complémentaire :

• faire des transfos formelles (= au niveau du DSL), par ex. pour traiter tf libre, des contraintes ponctuelles intérieures, du loss control, plus généralement du multi-phase...
• y ajouter une vérification formelle de la correction du code DSL généré par des outils de preuve type coq / lean (là encore, les LLM peuvent aider)

[jbcaillau]

@ocots example of that: https://claude.ai/share/bbd6f4fd-64d4-4b20-b6fa-634aef5111cc

@ocots @gergaud pour le projet n7, autre piste complémentaire :

• faire des transfos formelles (= au niveau du DSL), par ex. pour traiter tf libre, des contraintes ponctuelles intérieures, du loss control, plus généralement du multi-phase...
• y ajouter une vérification formelle de la correction du code DSL généré par des outils de preuve type coq / lean (là encore, les LLM peuvent aider)