Merge pull request #367 from JuliaReach/schillic/alg

Rename 'alg' and 'alg_nn' arguments

models/ACC/ACC.jl

@@ -147,18 +147,19 @@ T_warmup = 2 * period;  # shorter time horizon for warm-up run
 
 # To enclose the continuous dynamics, we use a Taylor-model-based algorithm:
 
-alg = TMJets(abstol=1e-6, orderT=6, orderQ=1);
+algorithm_plant = TMJets(abstol=1e-6, orderT=6, orderQ=1);
 
 # To propagate sets through the neural network, we use the `DeepZ` algorithm:
 
-alg_nn = DeepZ();
+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, alg_nn=alg_nn, alg=alg)
+    res = @timed solve(prob; T=T, algorithm_controller=algorithm_controller,
+                       algorithm_plant=algorithm_plant)
     sol = res.value
     silent || print_timed(res)
 

models/Airplane/Airplane.jl

@@ -208,18 +208,19 @@ T_warmup = 2 * period;  # shorter time horizon for warm-up run
 
 # To enclose the continuous dynamics, we use a Taylor-model-based algorithm:
 
-alg = TMJets(abstol=1e-10, orderT=7, orderQ=1);
+algorithm_plant = TMJets(abstol=1e-10, orderT=7, orderQ=1);
 
 # To propagate sets through the neural network, we use the `DeepZ` algorithm:
 
-alg_nn = DeepZ();
+algorithm_controller = DeepZ();
 
 # The falsification benchmark is given below:
 
 function benchmark(; T=T, silent::Bool=false)
     ## Solve the controlled system:
     silent || println("Flowpipe construction:")
-    res = @timed solve(prob; T=T, alg_nn=alg_nn, alg=alg)
+    res = @timed solve(prob; T=T, algorithm_controller=algorithm_controller,
+                       algorithm_plant=algorithm_plant)
     sol = res.value
     silent || print_timed(res)
 

models/AttitudeControl/AttitudeControl.jl

@@ -96,18 +96,19 @@ T_warmup = 2 * period;  # shorter time horizon for warm-up run
 
 # To enclose the continuous dynamics, we use a Taylor-model-based algorithm:
 
-alg = TMJets(abstol=1e-6, orderT=6, orderQ=1);
+algorithm_plant = TMJets(abstol=1e-6, orderT=6, orderQ=1);
 
 # To propagate sets through the neural network, we use the `DeepZ` algorithm:
 
-alg_nn = DeepZ();
+algorithm_controller = DeepZ();
 
 # The verification benchmark is given below:
 
 function benchmark(; T=T, silent::Bool=false)
     ## Solve the controlled system:
     silent || println("Flowpipe construction:")
-    res = @timed solve(prob; T=T, alg_nn=alg_nn, alg=alg)
+    res = @timed solve(prob; T=T, algorithm_controller=algorithm_controller,
+                       algorithm_plant=algorithm_plant)
     sol = res.value
     silent || print_timed(res)
 

models/InvertedPendulum/InvertedPendulum.jl

@@ -120,18 +120,19 @@ T_warmup = 2 * period;  # shorter time horizon for warm-up run
 
 # To enclose the continuous dynamics, we use a Taylor-model-based algorithm:
 
-alg = TMJets(abstol=1e-7, orderT=4, orderQ=1);
+algorithm_plant = TMJets(abstol=1e-7, orderT=4, orderQ=1);
 
 # To propagate sets through the neural network, we use the `DeepZ` algorithm:
 
-alg_nn = DeepZ();
+algorithm_controller = DeepZ();
 
 # The falsification benchmark is given below:
 
 function benchmark(; T=T, silent::Bool=false)
     ## Solve the controlled system:
     silent || println("Flowpipe construction:")
-    res = @timed solve(prob; T=T, alg_nn=alg_nn, alg=alg)
+    res = @timed solve(prob; T=T, algorithm_controller=algorithm_controller,
+                       algorithm_plant=algorithm_plant)
     sol = res.value
     silent || print_timed(res)
 

models/InvertedTwoLinkPendulum/InvertedTwoLinkPendulum.jl

@@ -170,18 +170,19 @@ end;
 
 # To enclose the continuous dynamics, we use a Taylor-model-based algorithm:
 
-alg = TMJets(abstol=1e-9, orderT=8, orderQ=1);
+algorithm_plant = TMJets(abstol=1e-9, orderT=8, orderQ=1);
 
 # To propagate sets through the neural network, we use the `DeepZ` algorithm:
 
-alg_nn = DeepZ();
+algorithm_controller = DeepZ();
 
 # The falsification benchmark is given below:
 
 function benchmark(prob, spec; T, silent::Bool=false)
     ## Solve the controlled system:
     silent || println("Flowpipe construction:")
-    res = @timed solve(prob; T=T, alg_nn=alg_nn, alg=alg)
+    res = @timed solve(prob; T=T, algorithm_controller=algorithm_controller,
+                       algorithm_plant=algorithm_plant)
     sol = res.value
     silent || print_timed(res)
 

models/Quadrotor/Quadrotor.jl

@@ -122,18 +122,19 @@ T_warmup = 2 * period;  # shorter time horizon for warm-up run
 
 # To enclose the continuous dynamics, we use a Taylor-model-based algorithm:
 
-alg = TMJets(abstol=1e-8, orderT=5, orderQ=1, adaptive=false);
+algorithm_plant = TMJets(abstol=1e-8, orderT=5, orderQ=1, adaptive=false);
 
 # To propagate sets through the neural network, we use the `DeepZ` algorithm:
 
-alg_nn = DeepZ();
+algorithm_controller = DeepZ();
 
 # The verification benchmark is given below:
 
 function benchmark(; T=T, silent::Bool=false)
     ## Solve the controlled system:
     silent || println("Flowpipe construction:")
-    res = @timed solve(prob; T=T, alg_nn=alg_nn, alg=alg)
+    res = @timed solve(prob; T=T, algorithm_controller=algorithm_controller,
+                       algorithm_plant=algorithm_plant)
     sol = res.value
     silent || print_timed(res)
 

models/SpacecraftDocking/SpacecraftDocking.jl

@@ -93,18 +93,19 @@ T_warmup = 2 * period;  # shorter time horizon for warm-up run
 
 # To enclose the continuous dynamics, we use a Taylor-model-based algorithm:
 
-alg = TMJets(abstol=1e-10, orderT=5, orderQ=1, adaptive=false);
+algorithm_plant = TMJets(abstol=1e-10, orderT=5, orderQ=1, adaptive=false);
 
 # To propagate sets through the neural network, we use the `DeepZ` algorithm:
 
-alg_nn = DeepZ();
+algorithm_controller = DeepZ();
 
 # The verification benchmark is given below:
 
 function benchmark(; T=T, silent::Bool=false)
     ## Solve the controlled system:
     silent || println("Flowpipe construction:")
-    res = @timed solve(prob; T=T, alg_nn=alg_nn, alg=alg)
+    res = @timed solve(prob; T=T, algorithm_controller=algorithm_controller,
+                       algorithm_plant=algorithm_plant)
     sol = res.value
     silent || print_timed(res)
 

models/TORA/TORA.jl

@@ -145,20 +145,21 @@ T2_warmup = 2 * period2;  # shorter time horizon for warm-up run
 
 # To enclose the continuous dynamics, we use a Taylor-model-based algorithm:
 
-alg = TMJets(abstol=1e-10, orderT=8, orderQ=3);
+algorithm_plant = TMJets(abstol=1e-10, orderT=8, orderQ=3);
 
 # To propagate sets through the neural network, we use the `DeepZ` algorithm.
 # For verification, we also use an additional splitting strategy to increase the
 # precision in scenario 1.
 
-alg_nn = DeepZ();
+algorithm_controller = DeepZ();
 
 # The verification benchmark is given below:
 
 function benchmark(prob; T=T, splitter, predicate, silent::Bool=false)
     ## Solve the controlled system:
     silent || println("Flowpipe construction:")
-    res = @timed solve(prob; T=T, alg_nn=alg_nn, alg=alg, splitter=splitter)
+    res = @timed solve(prob; T=T, algorithm_controller=algorithm_controller,
+                       algorithm_plant=algorithm_plant, splitter=splitter)
     sol = res.value
     silent || print_timed(res)
 

models/Unicycle/Unicycle.jl

@@ -100,20 +100,21 @@ T_warmup = 2 * period;  # shorter time horizon for warm-up run
 
 # To enclose the continuous dynamics, we use a Taylor-model-based algorithm:
 
-alg = TMJets(abstol=1e-15, orderT=10, orderQ=1);
+algorithm_plant = TMJets(abstol=1e-15, orderT=10, orderQ=1);
 
 # To propagate sets through the neural network, we use the `DeepZ` algorithm. We
 # also use an additional splitting strategy to increase the precision.
 
-alg_nn = DeepZ()
+algorithm_controller = DeepZ()
 splitter = BoxSplitter([3, 1, 7, 1]);
 
 # The verification benchmark is given below:
 
 function benchmark(; T=T, silent::Bool=false)
     ## Solve the controlled system:
     silent || println("Flowpipe construction:")
-    res = @timed solve(prob; T=T, alg_nn=alg_nn, alg=alg, splitter=splitter)
+    res = @timed solve(prob; T=T, algorithm_controller=algorithm_controller,
+                       algorithm_plant=algorithm_plant, splitter=splitter)
     sol = res.value
     silent || print_timed(res)
 

models/VerticalCAS/VerticalCAS.jl

@@ -115,15 +115,15 @@ end;
 # $\textit{adv}$ is computed as the argmax of the output score of
 # $N_{\textit{adv}}$ on $(h, \dot{h}_0, τ)$:
 
-function next_adv(X::LazySet, τ, adv; alg_nn=DeepZ())
+function next_adv(X::LazySet, τ, adv; algorithm_controller=DeepZ())
     Y = cartesian_product(X, Singleton([τ]))
     Y = normalize(Y)
-    out = forward(Y, advisory2controller[adv], alg_nn)
+    out = forward(Y, advisory2controller[adv], algorithm_controller)
     imax = argmax(high(out))
     return index2advisory[imax]
 end
 
-function next_adv(X::Singleton, τ, adv; alg_nn=nothing)
+function next_adv(X::Singleton, τ, adv; algorithm_controller=nothing)
     v = vcat(element(X), τ)
     v = normalize(v)
     u = forward(v, advisory2controller[adv])
@@ -195,7 +195,7 @@ end;
 const Δτ = 1.0
 const A = [1 -Δτ; 0 1]  # dynamics matrix (h, \dot{h}_0)
 
-function VerticalCAS!(out::Vector{<:State}, kmax::Int; acc, alg_nn)
+function VerticalCAS!(out::Vector{<:State}, kmax::Int; acc, algorithm_controller)
     ## Unpack the initial state:
     X0 = first(out)
     S = X0.state
@@ -204,7 +204,7 @@ function VerticalCAS!(out::Vector{<:State}, kmax::Int; acc, alg_nn)
 
     for k in 1:kmax
         ## Get the next advisory and acceleration:
-        adv′ = next_adv(S, τ, adv; alg_nn=alg_nn)
+        adv′ = next_adv(S, τ, adv; algorithm_controller=algorithm_controller)
         X = State(S, τ, adv′)
         hddot = next_acc(X, adv; acc=acc)
 
@@ -284,7 +284,7 @@ end;
 function simulate_VerticalCAS(X0::State; kmax)
     out = [X0]
     sizehint!(out, kmax + 1)
-    VerticalCAS!(out, kmax; acc=acc_central, alg_nn=DeepZ())
+    VerticalCAS!(out, kmax; acc=acc_central, algorithm_controller=DeepZ())
     return out
 end;