Adaptive Cruise Control (ACC)
The Adaptive Cruise Control (ACC) benchmark models a car that drives at a set velocity and maintains a safe distance from a lead car by adjusting the longitudinal acceleration [TCL+19].
using ClosedLoopReachability
import OrdinaryDiffEq, Plots, DisplayAs
using ReachabilityBase.CurrentPath: @current_path
using ReachabilityBase.Timing: print_timed
using ClosedLoopReachability: FunctionPreprocessing
using Plots: plot, plot!Precompiling packages...
Info Given TaylorIntegrationDiffEqExt was explicitly requested, output will be shown live
WARNING: Imported binding OrdinaryDiffEq.OrdinaryDiffEqAdaptiveAlgorithm was undeclared at import time during import to TaylorIntegrationDiffEqExt.
WARNING: Imported binding OrdinaryDiffEq.OrdinaryDiffEqConstantCache was undeclared at import time during import to TaylorIntegrationDiffEqExt.
WARNING: Imported binding OrdinaryDiffEq.OrdinaryDiffEqMutableCache was undeclared at import time during import to TaylorIntegrationDiffEqExt.
ERROR: LoadError: UndefVarError: `OrdinaryDiffEqAdaptiveAlgorithm` not defined in `TaylorIntegrationDiffEqExt`
Suggestion: this global was defined as `OrdinaryDiffEq.OrdinaryDiffEqAdaptiveAlgorithm` but not assigned a value.
Stacktrace:
[1] top-level scope
@ ~/.julia/packages/TaylorIntegration/THG4G/ext/TaylorIntegrationDiffEqExt.jl:36
[2] include(mod::Module, _path::String)
@ Base ./Base.jl:306
[3] include_package_for_output(pkg::Base.PkgId, input::String, depot_path::Vector{String}, dl_load_path::Vector{String}, load_path::Vector{String}, concrete_deps::Vector{Pair{Base.PkgId, UInt128}}, source::Nothing)
@ Base ./loading.jl:3021
[4] top-level scope
@ stdin:5
[5] eval(m::Module, e::Any)
@ Core ./boot.jl:489
[6] include_string(mapexpr::typeof(identity), mod::Module, code::String, filename::String)
@ Base ./loading.jl:2867
[7] include_string
@ ./loading.jl:2877 [inlined]
[8] exec_options(opts::Base.JLOptions)
@ Base ./client.jl:315
[9] _start()
@ Base ./client.jl:550
in expression starting at /home/runner/.julia/packages/TaylorIntegration/THG4G/ext/TaylorIntegrationDiffEqExt.jl:3
in expression starting at stdin:5
✗ TaylorIntegration → TaylorIntegrationDiffEqExt
0 dependencies successfully precompiled in 6 seconds. 249 already precompiled.
WARNING: Imported binding OrdinaryDiffEq.OrdinaryDiffEqAdaptiveAlgorithm was undeclared at import time during import to TaylorIntegrationDiffEqExt.
WARNING: Imported binding OrdinaryDiffEq.OrdinaryDiffEqConstantCache was undeclared at import time during import to TaylorIntegrationDiffEqExt.
WARNING: Imported binding OrdinaryDiffEq.OrdinaryDiffEqMutableCache was undeclared at import time during import to TaylorIntegrationDiffEqExt.
ERROR: LoadError: UndefVarError: `OrdinaryDiffEqAdaptiveAlgorithm` not defined in `TaylorIntegrationDiffEqExt`
Suggestion: this global was defined as `OrdinaryDiffEq.OrdinaryDiffEqAdaptiveAlgorithm` but not assigned a value.
Stacktrace:
[1] top-level scope
@ ~/.julia/packages/TaylorIntegration/THG4G/ext/TaylorIntegrationDiffEqExt.jl:36
[2] include(mod::Module, _path::String)
@ Base ./Base.jl:306
[3] include_package_for_output(pkg::Base.PkgId, input::String, depot_path::Vector{String}, dl_load_path::Vector{String}, load_path::Vector{String}, concrete_deps::Vector{Pair{Base.PkgId, UInt128}}, source::String)
@ Base ./loading.jl:3021
[4] top-level scope
@ stdin:5
[5] eval(m::Module, e::Any)
@ Core ./boot.jl:489
[6] include_string(mapexpr::typeof(identity), mod::Module, code::String, filename::String)
@ Base ./loading.jl:2867
[7] include_string
@ ./loading.jl:2877 [inlined]
[8] exec_options(opts::Base.JLOptions)
@ Base ./client.jl:315
[9] _start()
@ Base ./client.jl:550
in expression starting at /home/runner/.julia/packages/TaylorIntegration/THG4G/ext/TaylorIntegrationDiffEqExt.jl:3
in expression starting at stdin:5
┌ Error: Error during loading of extension TaylorIntegrationDiffEqExt of TaylorIntegration, use `Base.retry_load_extensions()` to retry.
│ exception =
│ 1-element ExceptionStack:
│ Failed to precompile TaylorIntegrationDiffEqExt [21fdf329-9f0e-520d-ae26-dab38dab1a79] to "/home/runner/.julia/compiled/v1.12/TaylorIntegrationDiffEqExt/jl_auGcoi".
│ Stacktrace:
│ [1] error(s::String)
│ @ Base ./error.jl:44
│ [2] compilecache(pkg::Base.PkgId, path::String, internal_stderr::IO, internal_stdout::IO, keep_loaded_modules::Bool; flags::Cmd, cacheflags::Base.CacheFlags, reasons::Dict{String, Int64}, loadable_exts::Vector{Base.PkgId})
│ @ Base ./loading.jl:3308
│ [3] (::Base.var"#__require_prelocked##0#__require_prelocked##1"{Base.PkgId, String, Dict{String, Int64}})()
│ @ Base ./loading.jl:2676
│ [4] mkpidlock(f::Base.var"#__require_prelocked##0#__require_prelocked##1"{Base.PkgId, String, Dict{String, Int64}}, at::String, pid::Int32; kwopts::@Kwargs{stale_age::Int64, wait::Bool})
│ @ FileWatching.Pidfile /opt/hostedtoolcache/julia/1.12.2/x64/share/julia/stdlib/v1.12/FileWatching/src/pidfile.jl:93
│ [5] #mkpidlock#7
│ @ /opt/hostedtoolcache/julia/1.12.2/x64/share/julia/stdlib/v1.12/FileWatching/src/pidfile.jl:88 [inlined]
│ [6] trymkpidlock(::Function, ::Vararg{Any}; kwargs::@Kwargs{stale_age::Int64})
│ @ FileWatching.Pidfile /opt/hostedtoolcache/julia/1.12.2/x64/share/julia/stdlib/v1.12/FileWatching/src/pidfile.jl:114
│ [7] #invokelatest_gr#232
│ @ ./reflection.jl:1297 [inlined]
│ [8] invokelatest_gr
│ @ ./reflection.jl:1289 [inlined]
│ [9] maybe_cachefile_lock(f::Base.var"#__require_prelocked##0#__require_prelocked##1"{Base.PkgId, String, Dict{String, Int64}}, pkg::Base.PkgId, srcpath::String; stale_age::Int64)
│ @ Base ./loading.jl:3879
│ [10] maybe_cachefile_lock(f::Function, pkg::Base.PkgId, srcpath::String)
│ @ Base ./loading.jl:3876
│ [11] __require_prelocked(pkg::Base.PkgId, env::Nothing)
│ @ Base ./loading.jl:2662
│ [12] _require_prelocked(uuidkey::Base.PkgId, env::Nothing)
│ @ Base ./loading.jl:2490
│ [13] _require_prelocked(uuidkey::Base.PkgId)
│ @ Base ./loading.jl:2484
│ [14] run_extension_callbacks(extid::Base.ExtensionId)
│ @ Base ./loading.jl:1604
│ [15] run_extension_callbacks(pkgid::Base.PkgId)
│ @ Base ./loading.jl:1641
│ [16] run_package_callbacks(modkey::Base.PkgId)
│ @ Base ./loading.jl:1457
│ [17] _require_prelocked(uuidkey::Base.PkgId, env::String)
│ @ Base ./loading.jl:2498
│ [18] macro expansion
│ @ ./loading.jl:2418 [inlined]
│ [19] macro expansion
│ @ ./lock.jl:376 [inlined]
│ [20] __require(into::Module, mod::Symbol)
│ @ Base ./loading.jl:2383
│ [21] require(into::Module, mod::Symbol)
│ @ Base ./loading.jl:2359
│ [22] eval(m::Module, e::Any)
│ @ Core ./boot.jl:489
│ [23] #61
│ @ ~/.julia/packages/Documenter/xvqbW/src/expander_pipeline.jl:879 [inlined]
│ [24] cd(f::Documenter.var"#61#62"{Module, Expr}, dir::String)
│ @ Base.Filesystem ./file.jl:112
│ [25] (::Documenter.var"#59#60"{Documenter.Page, Module, Expr})()
│ @ Documenter ~/.julia/packages/Documenter/xvqbW/src/expander_pipeline.jl:878
│ [26] (::IOCapture.var"#12#13"{Type{InterruptException}, Documenter.var"#59#60"{Documenter.Page, Module, Expr}, IOContext{Base.PipeEndpoint}, IOContext{Base.PipeEndpoint}, Base.PipeEndpoint, Base.PipeEndpoint})()
│ @ IOCapture ~/.julia/packages/IOCapture/MR051/src/IOCapture.jl:170
│ [27] with_logstate(f::IOCapture.var"#12#13"{Type{InterruptException}, Documenter.var"#59#60"{Documenter.Page, Module, Expr}, IOContext{Base.PipeEndpoint}, IOContext{Base.PipeEndpoint}, Base.PipeEndpoint, Base.PipeEndpoint}, logstate::Base.CoreLogging.LogState)
│ @ Base.CoreLogging ./logging/logging.jl:540
│ [28] with_logger(f::Function, logger::Base.CoreLogging.ConsoleLogger)
│ @ Base.CoreLogging ./logging/logging.jl:651
│ [29] capture(f::Documenter.var"#59#60"{Documenter.Page, Module, Expr}; rethrow::Type, color::Bool, passthrough::Bool, capture_buffer::IOBuffer, io_context::Vector{Any})
│ @ IOCapture ~/.julia/packages/IOCapture/MR051/src/IOCapture.jl:167
│ [30] runner(::Type{Documenter.Expanders.ExampleBlocks}, node::MarkdownAST.Node{Nothing}, page::Documenter.Page, doc::Documenter.Document)
│ @ Documenter ~/.julia/packages/Documenter/xvqbW/src/expander_pipeline.jl:877
│ [31] dispatch(::Type{Documenter.Expanders.ExpanderPipeline}, ::MarkdownAST.Node{Nothing}, ::Vararg{Any})
│ @ Documenter.Selectors ~/.julia/packages/Documenter/xvqbW/src/utilities/Selectors.jl:170
│ [32] expand(doc::Documenter.Document)
│ @ Documenter ~/.julia/packages/Documenter/xvqbW/src/expander_pipeline.jl:60
│ [33] runner(::Type{Documenter.Builder.ExpandTemplates}, doc::Documenter.Document)
│ @ Documenter ~/.julia/packages/Documenter/xvqbW/src/builder_pipeline.jl:224
│ [34] dispatch(::Type{Documenter.Builder.DocumentPipeline}, x::Documenter.Document)
│ @ Documenter.Selectors ~/.julia/packages/Documenter/xvqbW/src/utilities/Selectors.jl:170
│ [35] #89
│ @ ~/.julia/packages/Documenter/xvqbW/src/makedocs.jl:283 [inlined]
│ [36] withenv(::Documenter.var"#89#90"{Documenter.Document}, ::Pair{String, Nothing}, ::Vararg{Pair{String, Nothing}})
│ @ Base ./env.jl:265
│ [37] #87
│ @ ~/.julia/packages/Documenter/xvqbW/src/makedocs.jl:282 [inlined]
│ [38] cd(f::Documenter.var"#87#88"{Documenter.Document}, dir::String)
│ @ Base.Filesystem ./file.jl:112
│ [39] makedocs(; debug::Bool, format::Documenter.HTMLWriter.HTML, kwargs::@Kwargs{sitename::String, modules::Vector{Module}, pagesonly::Bool, plugins::Vector{CitationBibliography}, pages::Vector{Pair{String, Any}}})
│ @ Documenter ~/.julia/packages/Documenter/xvqbW/src/makedocs.jl:281
│ [40] top-level scope
│ @ ~/work/ClosedLoopReachability.jl/ClosedLoopReachability.jl/docs/make.jl:11
│ [41] include(mod::Module, _path::String)
│ @ Base ./Base.jl:306
│ [42] exec_options(opts::Base.JLOptions)
│ @ Base ./client.jl:317
│ [43] _start()
│ @ Base ./client.jl:550
└ @ Base loading.jl:1614Model
The cars' dynamics are modeled as follows:
\[\begin{aligned} \dot{x}_{lead} &= v_{lead} \\ \dot{v}_{lead} &= γ_{lead} \\ \dot{γ}_{lead} &= -2 γ_{lead} + 2 a_{lead} - u v_{lead}^2 \\ \dot{x}_{ego} &= v_{ego} \\ \dot{v}_{ego} &= γ_{ego} \\ \dot{γ}_{ego} &= -2 γ_{ego} + 2 a_{ego} - u v_{ego}^2 \end{aligned}\]
where $u = 0.0001$ is the friction parameter, and for each car $i ∈ \{ego, lead\}$ we have that $x_i$ is the position, $v_i$ is the velocity, $γ_i$ is the acceleration, and $a_i$ is the control input for the acceleration.
vars_idx = Dict(:states => 1:6, :controls => 7)
const u = 0.0001
const a_lead = -2.0
@taylorize function ACC!(dx, x, p, t)
v_lead = x[2] # lead car velocity
γ_lead = x[3] # lead car acceleration
v_ego = x[5] # ego car velocity
γ_ego = x[6] # ego car acceleration
a_ego = x[7] # ego car acceleration control input
# Lead-car dynamics:
dx[1] = v_lead
dx[2] = γ_lead
dx[3] = 2 * (a_lead - γ_lead) - u * v_lead^2
# Ego-car dynamics:
dx[4] = v_ego
dx[5] = γ_ego
dx[6] = 2 * (a_ego - γ_ego) - u * v_ego^2
dx[7] = zero(a_ego)
return dx
end;We are given two neural-network controllers with 5 hidden layers of 20 neurons each. One controller uses ReLU activations and the other controller uses tanh activations. Both controllers have 5 inputs $(v_{set}, T_{gap}, v_{ego}, D_{rel}, v_{rel})$ and one output ($a_{ego}$), where $v_{set} = 30$ is the ego car's set velocity, $T_{gap} = 1.4$, $D_{rel} = x_{lead} - x_{ego}$ is the distance between the cars, and $v_{rel} = v_{lead} - v_{ego}$ is the distance between the velocities.
path = @current_path("ACC", "ACC_controller_relu.polar")
controller_relu = read_POLAR(path)
path = @current_path("ACC", "ACC_controller_tanh.polar")
controller_tanh = read_POLAR(path);The controller input is $(v_{set}, T_{gap}, v_{ego}, D_{rel}, v_{rel})$, for which we define a transformation matrix $M$.
v_set = 30.0
T_gap = 1.4
M = zeros(3, 6)
M[1, 5] = 1.0
M[2, 1] = 1.0
M[2, 4] = -1.0
M[3, 2] = 1.0
M[3, 5] = -1.0
function preprocess(X::LazySet) # version for set computations
Y1 = Singleton([v_set, T_gap])
Y2 = linear_map(M, X)
return cartesian_product(Y1, Y2)
end
function preprocess(X::AbstractVector) # version for simulations
Y1 = [v_set, T_gap]
Y2 = M * X
return vcat(Y1, Y2)
end
control_preprocessing = FunctionPreprocessing(preprocess);The control period is 0.1 time units.
period = 0.1;Specification
The uncertain initial condition is:
\[\begin{aligned} x_{lead} &∈ [90, 110],& v_{lead} &∈ [32, 32.2],& γ_{lead} &= 0, \\ x_{ego} &∈ [10, 11],& v_{ego} &∈ [30, 30.2],& γ_{ego} &= 0 \end{aligned}\]
X₀ = Hyperrectangle(low=[90, 32, 0, 10, 30, 0],
high=[110, 32.2, 0, 11, 30.2, 0])
U₀ = ZeroSet(1);The control problem (parametric in the controller) is:
ivp = @ivp(x' = ACC!(x), dim: 7, x(0) ∈ X₀ × U₀)
problem(controller) = ControlledPlant(ivp, controller, vars_idx, period;
preprocessing=control_preprocessing);We consider a scenario where both cars are driving safely and the lead car suddenly slows down with $a_{lead} = -2$. We want to verify that there is no collision in the following 5 time units, i.e., the ego car must maintain a safe distance $D_{safe}$ from the lead car. Formally, the safety specification is $D_{rel} ≥ D_{safe}$, where $D_{safe} = D_{default} + T_{gap} · v_{ego}$ and $D_{default} = 10$. After substitution, the specification reduces to $x_{lead} - x_{ego} - T_{gap} · v_{ego} ≥ D_{default}$. A sufficient condition for guaranteed verification is to overapproximate the result with hyperrectangles.
D_default = 10.0
d_rel = [1.0, 0, 0, -1, 0, 0, 0]
d_safe = [0, 0, 0, 0, T_gap, 0, 0]
d_prop = d_rel - d_safe
safe_states = HalfSpace(-d_prop, -D_default)
predicate(sol) = overapproximate(sol, Hyperrectangle) ⊆ safe_states
T = 5.0
T_warmup = 2 * period; # shorter time horizon for warm-up runAnalysis
To enclose the continuous dynamics, we use a Taylor-model-based algorithm:
algorithm_plant = TMJets(abstol=1e-3, orderT=5, orderQ=1);To propagate sets through the neural network, we use the DeepZ algorithm:
algorithm_controller = DeepZ();The verification benchmark is given below:
function benchmark(prob; T=T, silent::Bool=false)
# Solve the controlled system:
silent || println("Flowpipe construction:")
res = @timed solve(prob; T=T, algorithm_controller=algorithm_controller,
algorithm_plant=algorithm_plant)
sol = res.value
silent || print_timed(res)
# Check the property:
silent || println("Property checking:")
res = @timed predicate(sol)
silent || print_timed(res)
if res.value
silent || println(" The property is satisfied.")
result = "verified"
else
silent || println(" The property may be violated.")
result = "not verified"
end
return sol, result
end;For each controller we execute the same analysis script, which runs the verification benchmark and computes simulations:
function run(; use_relu_controller::Bool)
if use_relu_controller
println("# Running analysis with ReLU controller")
prob = problem(controller_relu)
else
println("# Running analysis with tanh controller")
prob = problem(controller_tanh)
end
# Run the verification benchmark:
benchmark(prob; T=T_warmup, silent=true) # warm-up
res = @timed benchmark(prob; T=T) # benchmark
sol, result = res.value
@assert (result == "verified") "verification failed"
println("Total analysis time:")
print_timed(res)
# Compute some simulations:
println("Simulation:")
res = @timed simulate(prob; T=T, trajectories=10, include_vertices=true)
sim = res.value
print_timed(res)
return sol, sim
end;Run the analysis script for the ReLU controller:
sol_relu, sim_relu = run(use_relu_controller=true);# Running analysis with ReLU controller
Flowpipe construction:
0.570511 seconds (5.62 M allocations: 342.885 MiB, 9.47% gc time)
Property checking:
0.042565 seconds (384.68 k allocations: 24.102 MiB)
The property is satisfied.
Total analysis time:
0.710049 seconds (6.11 M allocations: 372.899 MiB, 7.61% gc time, 0.00% compilation time)
Simulation:
4.909132 seconds (16.48 M allocations: 825.057 MiB, 1.82% gc time, 0.00% compilation time: 2% of which was recompilation)Run the analysis script for the tanh controller:
sol_tanh, sim_tanh = run(use_relu_controller=false);# Running analysis with tanh controller
Flowpipe construction:
1.176027 seconds (5.64 M allocations: 345.785 MiB, 54.07% gc time)
Property checking:
0.041856 seconds (384.68 k allocations: 24.102 MiB)
The property is satisfied.
Total analysis time:
1.218896 seconds (6.02 M allocations: 370.614 MiB, 52.16% gc time)
Simulation:
0.100701 seconds (304.95 k allocations: 20.071 MiB, 0.00% compilation time)Results
Script to plot the results:
function plot_helper(sol, sim)
fig = plot(leg=(0.4, 0.3))
for F in sol, R in F
# Subdivide the reach sets in time to obtain more precise plots:
R = overapproximate(R, Zonotope; ntdiv=5)
R_rel = linear_map(Matrix(d_rel'), R)
plot!(fig, R_rel; vars=(0, 1), c=:red, lw=0, alpha=0.4)
end
solz = overapproximate(flowpipe(sol), Zonotope)
fp_safe = affine_map(Matrix(d_safe'), solz, [D_default])
plot!(fig, fp_safe; vars=(0, 1), c=:blue, lw=0, alpha=0.4)
output_map_rel = x -> dot(d_rel, x)
plot_simulation!(fig, sim; output_map=output_map_rel, color=:red, lab="Drel")
output_map_safe = x -> dot(d_safe, x) + D_default
plot_simulation!(fig, sim; output_map=output_map_safe, color=:blue, lab="Dsafe")
plot!(fig; xlab="time")
return fig
end;Plot the results:
fig = plot_helper(sol_relu, sim_relu)
# Plots.savefig(fig, "ACC-ReLU.png") # command to save the plot to a file
fig = DisplayAs.Text(DisplayAs.PNG(fig))
fig = plot_helper(sol_tanh, sim_tanh)
fig = DisplayAs.Text(DisplayAs.PNG(fig))
# savefig(fig, "ACC-tanh.png") # command to save the plot to a file